Nominal/Ex/Pi.thy
changeset 3183 313e6f2cdd89
parent 3097 b27e94db1b8a
child 3191 0440bc1a2438
--- a/Nominal/Ex/Pi.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -35,11 +35,11 @@
   apply(auto)
   apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)")
   unfolding eqvt_def
+  apply(simp only: permute_fun_def)
   apply(rule allI)
-  apply(simp add: permute_fun_def)
   apply(rule ext)
   apply(rule ext)
-  apply(simp add: permute_bool_def)
+  apply(simp only: permute_bool_def)
   apply(rule iffI)
   apply(drule_tac x="p" in meta_spec)
   apply(drule_tac x="- p \<bullet> x" in meta_spec)
@@ -183,10 +183,10 @@
   apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")
   unfolding eqvt_def
   apply(rule allI)
-  apply(simp add: permute_fun_def)
+  apply(simp only: permute_fun_def)
   apply(rule ext)
   apply(rule ext)
-  apply(simp add: permute_bool_def)
+  apply(simp only: permute_bool_def)
   apply(rule iffI)
   apply(drule_tac x="p" in meta_spec)
   apply(drule_tac x="- p \<bullet> x" in meta_spec)
@@ -303,13 +303,14 @@
   apply(simp)
   apply(blast)
   --"compatibility"
-  apply (simp add: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
   apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
   apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
   apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
   prefer 2
-  apply (simp add: eqvt_at_def subs_mix_def)
+  apply (simp only: eqvt_at_def subs_mix_def)
   apply rule
+  apply(simp (no_asm))
   apply (subst testrr)
   apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
   apply (simp add: THE_default_def)
@@ -389,7 +390,11 @@
   apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
   apply simp
   apply (erule fresh_eqvt_at)
-  apply (simp_all add: fresh_Pair finite_supp eqvts eqvt_at_def fresh_Pair swap_fresh_fresh)
+  apply(simp add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def)
+  apply(drule_tac x="(atom b \<rightleftharpoons> atom ba)" in spec)
+  apply(simp)
   done
 
 termination (eqvt)