--- 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)