# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269619282 -3600
# Node ID aacab5f67333e69fab9fef00f1e1cd75e401f596
# Parent  d7dc35222afc86f96368a24ff7d217b7854aec8c
Fixed renamings.

diff -r d7dc35222afc -r aacab5f67333 Nominal/ExCoreHaskell.thy
--- 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+)
diff -r d7dc35222afc -r aacab5f67333 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Fri Mar 26 16:46:40 2010 +0100
+++ b/Nominal/ExLet.thy	Fri Mar 26 17:01:22 2010 +0100
@@ -87,7 +87,7 @@
   apply (simp add: permute_bn_alpha_bn)
   apply (simp add: perm_bn[symmetric])
   apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_Abs)
+  apply (simp add: supp_abs)
   apply (simp add: trm_lts.supp)
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
@@ -157,10 +157,10 @@
     apply(rule at_set_avoiding2)
     apply(rule fin_bn)
     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)
+    apply(simp add: fresh_star_def fresh_def supp_abs)
     apply(simp add: eqvts permute_bn)
     apply(rule a5)
     apply(simp add: permute_bn)
diff -r d7dc35222afc -r aacab5f67333 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Fri Mar 26 16:46:40 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 26 17:01:22 2010 +0100
@@ -872,7 +872,7 @@
 *}
 
 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
-  apply (simp add: supp_Abs supp_Pair)
+  apply (simp add: supp_abs supp_Pair)
   apply blast
   done
 
@@ -880,10 +880,10 @@
 fun supp_eq_tac ind fv perm eqiff ctxt =
   rel_indtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW