more

Author: Andrei Popescu

thys/POPLmark/POPLmark_1A.thy

@@ -8,7 +8,7 @@ declare ty.intros[intro]
 
 lemma well_scoped:
   assumes "\<Gamma> \<turnstile> S <: T"
-  shows "S closed_in \<Gamma>" "T closed_in \<Gamma>"
+  shows "FFVars_sftypeP S \<subseteq> dom \<Gamma>" "FFVars_sftypeP T \<subseteq> dom \<Gamma>"
 using assms proof (induction \<Gamma> S T rule: ty.induct)
   case (SA_Trans_TVar x U \<Gamma> T) {
   case 1 then show ?case using SA_Trans_TVar
@@ -17,11 +17,12 @@ next
   case 2 then show ?case using SA_Trans_TVar by simp
 } qed auto
 
+declare SA_Refl_TVar[intro!]
 
-lemma ty_refl: "\<lbrakk>wf \<Gamma> ; T closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T <: T"
+lemma ty_refl: "\<lbrakk>wf \<Gamma> ; FFVars_sftypeP T \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T <: T"
 proof (binder_induction T arbitrary: \<Gamma> avoiding: "dom \<Gamma>" rule: sftypeP.strong_induct)
   case (TVr x \<Gamma>)
-  then show ?case by blast
+  then show ?case by (simp add: SA_Refl_TVar)  
 qed (auto simp: Diff_single_insert SA_All wf_Cons)
 
 lemma ty_permute: "\<lbrakk> \<Gamma> \<turnstile> S <: T ; wf \<Delta> ; set \<Gamma> = set \<Delta> \<rbrakk> \<Longrightarrow> \<Delta> \<turnstile> S <: T"
@@ -43,7 +44,7 @@ proof (induction \<Delta> rule: wf.induct)
     using wf_Cons by auto
 qed auto
 
-lemma weaken_closed: "\<lbrakk> S closed_in \<Gamma> ; \<Gamma> \<bottom> \<Delta> \<rbrakk> \<Longrightarrow> S closed_in \<Gamma>,,\<Delta>"
+lemma weaken_closed: "\<lbrakk> FFVars_sftypeP S \<subseteq> dom \<Gamma> ; \<Gamma> \<bottom> \<Delta> \<rbrakk> \<Longrightarrow> FFVars_sftypeP S \<subseteq> dom (\<Gamma>,,\<Delta>)"
   by auto
 
 lemma wf_concat_disjoint: "wf (\<Gamma>,, \<Delta>) \<Longrightarrow> \<Gamma> \<bottom> \<Delta>"
@@ -53,7 +54,7 @@ proof (induction \<Delta>)
     by (smt (verit, del_insts) Un_iff append_Cons disjoint_iff fst_conv image_iff inf.idem insertE list.inject list.simps(15) set_append set_empty2 wf.cases)
 qed simp
 
-lemma wf_insert: "\<lbrakk> wf (\<Gamma>,,\<Delta>); x \<notin> dom \<Gamma> ; x \<notin> dom \<Delta> ; T closed_in \<Gamma> \<rbrakk> \<Longrightarrow> wf (\<Gamma>,,x<:T,,\<Delta>)"
+lemma wf_insert: "\<lbrakk> wf (\<Gamma>,,\<Delta>); x \<notin> dom \<Gamma> ; x \<notin> dom \<Delta> ; FFVars_sftypeP T \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> wf (\<Gamma>,,x<:T,,\<Delta>)"
   by (induction \<Delta>) auto
 
 lemma ty_weakening:
@@ -64,7 +65,8 @@ using assms proof (binder_induction \<Gamma> S T avoiding: "dom \<Delta>" \<Gamm
   then show ?case using ty.SA_Top weaken_closed wf_concat_disjoint by presburger
 next
   case (SA_Refl_TVar \<Gamma> x)
-  then show ?case using ty.SA_Refl_TVar weaken_closed wf_concat_disjoint by presburger
+  then show ?case using ty.SA_Refl_TVar weaken_closed wf_concat_disjoint  
+    by (meson ty_refl well_scoped(1))   
 next
   case (SA_All \<Gamma> T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2)
   have 1: "wf (\<Gamma>,, x <: T\<^sub>1,, \<Delta>)"
@@ -74,7 +76,7 @@ next
   show ?case using ty_permute[OF _ 2] 1 SA_All by auto
 qed auto
 
-corollary ty_weakening_extend: "\<lbrakk> \<Gamma> \<turnstile> S <: T ; X \<notin> dom \<Gamma> ; Q closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma>,,X<:Q \<turnstile> S <: T"
+corollary ty_weakening_extend: "\<lbrakk> \<Gamma> \<turnstile> S <: T ; X \<notin> dom \<Gamma> ; FFVars_sftypeP Q \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma>,,X<:Q \<turnstile> S <: T"
   using ty_weakening[of _ _ _ "[(X, Q)]"] by (metis append_Cons append_Nil wf_Cons wf_context)
 
 lemma wf_concatD: "wf (\<Gamma>,, \<Delta>) \<Longrightarrow> wf \<Gamma>"
@@ -87,7 +89,7 @@ proof (induction \<Delta>)
     by (metis Pair_inject append_Nil fst_conv image_eqI set_ConsD wf_ConsE)
 qed auto
 
-lemma narrow_wf: "\<lbrakk> wf ((\<Gamma> ,, X <: Q),, \<Delta>) ; R closed_in \<Gamma> \<rbrakk> \<Longrightarrow> wf ((\<Gamma>,, X <: R),, \<Delta>)"
+lemma narrow_wf: "\<lbrakk> wf ((\<Gamma> ,, X <: Q),, \<Delta>) ; FFVars_sftypeP R \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> wf ((\<Gamma>,, X <: R),, \<Delta>)"
 proof (induction \<Delta>)
   case (Cons a \<Delta>)
   then have "wf (\<Gamma>,, X <: R,, \<Delta>)" by auto
@@ -99,7 +101,7 @@ qed auto
 
 lemma SA_AllE1[consumes 2, case_names SA_Trans_TVar SA_All]:
   assumes "\<Gamma> \<turnstile> \<forall>X<:S\<^sub>1. S\<^sub>2 <: T" "X \<notin> dom \<Gamma>"
-    and Top: "\<And>\<Gamma>. \<lbrakk>wf \<Gamma>; \<forall>X<:S\<^sub>1. S\<^sub>2 closed_in \<Gamma> \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) Top"
+    and Top: "\<And>\<Gamma>. \<lbrakk>wf \<Gamma>;   FFVars_sftypeP (\<forall>X<:S\<^sub>1. S\<^sub>2) \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) Top"
     and Forall: "\<And>\<Gamma> T\<^sub>1 T\<^sub>2. \<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) (\<forall>X<:T\<^sub>1 . T\<^sub>2)"
   shows "R \<Gamma> (\<forall>X<:S\<^sub>1. S\<^sub>2) T"
 using assms(1,2) proof (binder_induction \<Gamma> "\<forall>X<:S\<^sub>1. S\<^sub>2" T avoiding: \<Gamma> "\<forall>X<:S\<^sub>1. S\<^sub>2" T rule: ty.strong_induct)
@@ -173,7 +175,7 @@ proof -
   have
     ty_trans: "\<lbrakk> \<Gamma> \<turnstile> S <: Q ; \<Gamma> \<turnstile> Q <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
   and ty_narrow: "\<lbrakk> (\<Gamma>,, X <: Q),, \<Delta> \<turnstile> M <: N ; \<Gamma> \<turnstile> R <: Q ; wf (\<Gamma>,, X <: R,, \<Delta>) ; 
-    M closed_in (\<Gamma>,, X <: R,, \<Delta>) ; N closed_in (\<Gamma>,, X <: R,, \<Delta>) \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
+   FFVars_sftypeP M \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>) ; FFVars_sftypeP N \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>) \<rbrakk> \<Longrightarrow> (\<Gamma>,, X <: R),, \<Delta> \<turnstile> M <: N"
   proof (binder_induction Q arbitrary: \<Gamma> \<Delta> S T M N X R avoiding: X "dom \<Gamma>" "dom \<Delta>" rule: sftypeP.strong_induct)
     case (TVr Y \<Gamma> \<Delta> S T M N X R)
     {
@@ -190,15 +192,15 @@ proof -
         proof (cases "X = Z")
           case True
           then have u: "U = TVr Y" using SA_Trans_TVar(1,2) context_determ wf_context by blast
-          have "TVr Y closed_in (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
+          have "FFVars_sftypeP (TVr Y) \<subseteq> dom (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
           then have "\<Gamma>,, Z <: R ,, \<Delta>' \<turnstile> TVr Y <: T" using SA_Trans_TVar True u by auto
           moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: TVr Y" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
             by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)
           ultimately have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: T" using ty_trans by blast
           then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
         next
           case False
-          have x: "U closed_in (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
+          have x: "FFVars_sftypeP (U) \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
           show ?thesis
             apply (rule ty.SA_Trans_TVar)
             using SA_Trans_TVar False x by auto
@@ -234,7 +236,7 @@ proof -
           then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
         next
           case False
-          have x: "U closed_in (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
+          have x: "FFVars_sftypeP (U) \<subseteq> dom (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
           show ?thesis
             apply (rule ty.SA_Trans_TVar)
             using SA_Trans_TVar False x by auto
@@ -279,15 +281,15 @@ proof -
         proof (cases "X = Z")
           case True
           then have u: "U = (Q\<^sub>1 \<rightarrow> Q\<^sub>2)" using SA_Trans_TVar(1,2) context_determ wf_context by blast
-          have "(Q\<^sub>1 \<rightarrow> Q\<^sub>2) closed_in (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
+          have "FFVars_sftypeP (Q\<^sub>1 \<rightarrow> Q\<^sub>2) \<subseteq> dom (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
           then have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> (Q\<^sub>1 \<rightarrow> Q\<^sub>2) <: T" using SA_Trans_TVar True u by auto
           moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: (Q\<^sub>1 \<rightarrow> Q\<^sub>2)" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
             by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)
           ultimately have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: T" using ty_trans by blast
           then show ?thesis unfolding True u using ty.SA_Trans_TVar by auto
         next
           case False
-          have x: "U closed_in (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
+          have x: "FFVars_sftypeP U \<subseteq> dom  (\<Gamma>,, X <: R,, \<Delta>')" using SA_Trans_TVar(2) well_scoped(1) by fastforce
           show ?thesis
             apply (rule ty.SA_Trans_TVar)
             using SA_Trans_TVar False x by auto
@@ -340,7 +342,7 @@ proof -
         proof (cases "Y = Z")
           case True
           then have u: "U = \<forall> X <: Q\<^sub>1 . Q\<^sub>2" using SA_Trans_TVar(1,2) context_determ wf_context by blast
-          have "\<forall> X <: Q\<^sub>1 . Q\<^sub>2 closed_in \<Gamma>,, Z <: R,, \<Delta>'" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
+          have "FFVars_sftypeP (\<forall> X <: Q\<^sub>1 . Q\<^sub>2) \<subseteq> dom (\<Gamma>,, Z <: R,, \<Delta>')" using SA_Trans_TVar(2) True u well_scoped(1) by fastforce
           then have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> \<forall> X <: Q\<^sub>1 . Q\<^sub>2 <: T" using SA_Trans_TVar True u by auto
           moreover have "\<Gamma>,, Z <: R,, \<Delta>' \<turnstile> R <: \<forall> X <: Q\<^sub>1 . Q\<^sub>2" using ty_weakening[OF ty_weakening_extend[OF SA_Trans_TVar(4)]]
             by (metis SA_Trans_TVar(5) True wf_ConsE wf_concatD)

thys/POPLmark/SystemFSub.thy

@@ -3,14 +3,17 @@ theory SystemFSub
   imports "SystemFSub_Types"
 begin
 
+
 abbreviation in_context :: "var \<Rightarrow> sftype \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> bool" ("_ <: _ \<in> _" [55,55,55] 60) where
   "x <: t \<in> \<Gamma> \<equiv> (x, t) \<in> set \<Gamma>"
+
 abbreviation well_scoped :: "sftype \<Rightarrow> \<Gamma>\<^sub>\<tau> \<Rightarrow> bool" ("_ closed'_in _" [55, 55] 60) where
   "well_scoped S \<Gamma> \<equiv> FFVars_sftypeP S \<subseteq> dom \<Gamma>"
 
+
 inductive wf :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> bool"  where
   wf_Nil[intro]: "wf []"
-| wf_Cons[intro!]: "\<lbrakk> x \<notin> dom \<Gamma> ; T closed_in \<Gamma> ; wf \<Gamma>\<rbrakk> \<Longrightarrow> wf (\<Gamma>,,x<:T)"
+| wf_Cons[intro!]: "\<lbrakk> x \<notin> dom \<Gamma> ; FFVars_sftypeP T \<subseteq> dom \<Gamma> ; wf \<Gamma>\<rbrakk> \<Longrightarrow> wf (\<Gamma>,,x<:T)"
 
 inductive_cases
   wfE[elim]: "wf \<Gamma>"
@@ -29,7 +32,7 @@ lemma extend_eqvt:
 
 lemma closed_in_eqvt:
   assumes "bij f" "|supp f| <o |UNIV::var set|"
-  shows "S closed_in \<Gamma> \<Longrightarrow> rrename_sftypeP f S closed_in map_context f \<Gamma>"
+  shows "FFVars_sftypeP S \<subseteq> dom \<Gamma> \<Longrightarrow> FFVars_sftypeP (rrename_sftypeP f S) \<subseteq> dom (map_context f \<Gamma>)"
   using assms by (auto simp: sftypeP.FFVars_rrenames)
 
 lemma wf_eqvt:
@@ -74,8 +77,8 @@ qed
 (* *)
 
 inductive ty :: "\<Gamma>\<^sub>\<tau> \<Rightarrow> sftype \<Rightarrow> sftype \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [55,55,55] 60) where
-  SA_Top: "\<lbrakk>wf \<Gamma>; S closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
-| SA_Refl_TVar: "\<lbrakk>wf \<Gamma>; TVr x closed_in \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TVr x <: TVr x"
+  SA_Top: "\<lbrakk>wf \<Gamma>; FFVars_sftypeP S \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
+| SA_Refl_TVar: "\<lbrakk>wf \<Gamma>;  FFVars_sftypeP  (TVr x) \<subseteq> dom \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TVr x <: TVr x"
 | SA_Trans_TVar: "\<lbrakk> X<:U \<in> \<Gamma> ; \<Gamma> \<turnstile> U <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TVr X <: T"
 | SA_Arrow: "\<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2"
 | SA_All: "\<lbrakk> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 ; \<Gamma>,, X<:T\<^sub>1 \<turnstile> S\<^sub>2 <: T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> \<forall>X<:S\<^sub>1. S\<^sub>2 <: \<forall>X<:T\<^sub>1 .T\<^sub>2"