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/ExCoreHaskell.thy
changeset 1658 aacab5f67333
parent 1656 c9d3dda79fe3
child 1667 2922b04d9545 
--- a/Nominal/ExCoreHaskell.thy	Fri Mar 26 16:46:40 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Fri Mar 26 17:01:22 2010 +0100
@@ -194,7 +194,7 @@
   apply (simp add: alphas)
   apply (simp add: perm_bv2[symmetric])
   apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_Abs)
+  apply (simp add: supp_abs)
   apply (simp add: fv_supp)
   apply (simp add: alpha_perm_bn)
   apply (rule supp_perm_eq[symmetric])
@@ -394,7 +394,7 @@
                and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
@@ -422,7 +422,7 @@
     apply (simp add: finite_supp)
     apply (simp add: finite_supp)
     apply (simp add: fresh_def)
-    apply (simp only: supp_Abs eqvts)
+    apply (simp only: supp_abs eqvts)
     apply blast
 
 (* GOAL2 *)
@@ -434,7 +434,7 @@
                and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
@@ -462,7 +462,7 @@
     apply (simp add: finite_supp)
     apply (simp add: finite_supp)
     apply (simp add: fresh_def)
-    apply (simp only: supp_Abs eqvts)
+    apply (simp only: supp_abs eqvts)
     apply blast
 
 
@@ -475,7 +475,7 @@
                and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
@@ -503,7 +503,7 @@
     apply (simp add: finite_supp)
     apply (simp add: finite_supp)
     apply (simp add: fresh_def)
-    apply (simp only: supp_Abs eqvts)
+    apply (simp only: supp_abs eqvts)
     apply blast
 
 (* GOAL4 a copy-and-paste *)
@@ -515,7 +515,7 @@
                and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
@@ -543,7 +543,7 @@
     apply (simp add: finite_supp)
     apply (simp add: finite_supp)
     apply (simp add: fresh_def)
-    apply (simp only: supp_Abs eqvts)
+    apply (simp only: supp_abs eqvts)
     apply blast
 
 
@@ -556,7 +556,7 @@
                and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
     apply (simp add: eqvts)
@@ -584,7 +584,7 @@
     apply (simp add: finite_supp)
     apply (simp add: finite_supp)
     apply (simp add: fresh_def)
-    apply (simp only: supp_Abs eqvts)
+    apply (simp only: supp_abs eqvts)
     apply blast
 
 
@@ -597,7 +597,7 @@
                and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
     apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
                 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
     apply (simp add: eqvts)
@@ -626,7 +626,7 @@
     apply (simp add: finite_supp)
     apply (simp add: finite_supp)
     apply (simp add: fresh_def)
-    apply (simp only: supp_Abs eqvts)
+    apply (simp only: supp_abs eqvts)
     apply blast
 
 (* MAIN ACons Goal *)
@@ -647,10 +647,10 @@
     apply (rule at_set_avoiding2)
     apply (simp add: fin_bv)
     apply (simp add: finite_supp)
-    apply (simp add: supp_Abs)
+    apply (simp add: supp_abs)
     apply (rule finite_Diff)
     apply (simp add: finite_supp)
-    apply (simp add: fresh_star_def fresh_def supp_Abs eqvts)
+    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_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+)
nominal2