Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/CoreHaskell.thy
changeset 2142 c39d4fe31100
parent 2120 2786ff1df475
child 2213 231a20534950
child 2308 387fcbd33820 
--- a/Nominal/Ex/CoreHaskell.thy	Sun May 16 11:00:44 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Sun May 16 12:41:27 2010 +0100
@@ -84,7 +84,7 @@
 | "bv_tvs TvsNil = []"
 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
 | "bv_cvs CvsNil = []"
-| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"    
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
@@ -191,13 +191,13 @@
   done
 
 lemma alpha_perm_bn:
-  "alpha_bv pat (permute_bv q pat)"
-  apply(induct pat rule: inducts(9))
+  "alpha_bv pt (permute_bv q pt)"
+  apply(induct pt rule: inducts(9))
   apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
   done
 
 lemma ACons_subst:
-  "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
+  "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"
   apply (simp only: eq_iff)
   apply (simp add: alpha_perm_bn)
   apply (rule_tac x="q" in exI)
@@ -352,8 +352,8 @@
   and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
   and a37: "\<And>b. P8 b ANil"
-  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
-    \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
+  and a38: "\<And>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk>
+    \<Longrightarrow> P8 b (ACons pt trm assoc_lst)"
   and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
     \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
   and a40: "\<And>b. P10 b VsNil"
@@ -372,12 +372,12 @@
          P6 (f :: 'f :: pt) co_lst \<and>
          P7 (g :: 'g :: {pt,fs}) trm \<and>
          P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
-         P9 (i :: 'i :: pt) pat \<and>
+         P9 (i :: 'i :: pt) pt \<and>
          P10 (j :: 'j :: pt) vars \<and>
          P11 (k :: 'k :: pt) tvars \<and>
          P12 (l :: 'l :: pt) cvars"
 proof -
-  have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
+  have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
     apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
@@ -637,7 +637,7 @@
     apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
     done
   then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
-  moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
+  moreover have "P9  i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
nominal2