diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -32,29 +32,9 @@
 where
   "subst_name_list a [] = a"
 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
+  apply(simp add: eqvt_def subst_name_list_graph_aux_def)
+  apply(simp)
   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(rule ext)
-  apply(rule ext)
-  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)
-  apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-  apply(simp)
-  apply(drule_tac x="-p" in meta_spec)
-  apply(drule_tac x="x" in meta_spec)
-  apply(drule_tac x="xa" in meta_spec)
-  apply(simp)
-  apply(erule subst_name_list_graph.induct)
-  apply(perm_simp)
-  apply(rule subst_name_list_graph.intros)
-  apply(perm_simp)
-  apply(rule subst_name_list_graph.intros)
-  apply(simp)
   apply(rule_tac y="b" in list.exhaust)
   by(auto)
 
@@ -181,97 +161,7 @@
 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
   using [[simproc del: alpha_lst]]
   apply(auto simp add: piMix_distinct piMix_eq_iff)
-  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 only: permute_fun_def)
-  apply(rule ext)
-  apply(rule ext)
-  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)
-  apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-  apply(simp)
-  apply(drule_tac x="-p" in meta_spec)
-  apply(drule_tac x="x" in meta_spec)
-  apply(drule_tac x="xa" in meta_spec)
-  apply(simp)
-  --"Equivariance"
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.induct)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp (no_asm_use) only: eqvts)  
-  apply(subst testl)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(subst testlr)
-  apply(rotate_tac 2)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(perm_simp)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
-  apply(simp)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(subst testrr)
-  apply(rotate_tac 2)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(perm_simp)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testlr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(blast)
-  apply(simp (no_asm_use) only: eqvts)
-  apply(subst testrr)
-  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-  apply(blast)+
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
-  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)
-  apply(blast)
-  apply(perm_simp)
-  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)
+  apply(simp add: eqvt_def  subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
   --"Covered all cases"
   apply(case_tac x)
   apply(simp)
@@ -398,6 +288,99 @@
   apply(simp add: eqvt_at_def)
   apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
   apply(simp)
+  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+  apply(rename_tac b P ba xa ya Pa)
+ 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 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)
+apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
+apply simp_all[2]
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply (thin_tac "\<forall>p\<Colon>perm.
+           p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
+           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+            else Inr (Inr undefined))")
+apply (thin_tac "\<forall>p\<Colon>perm.
+           p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                      subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                        subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                else Inr (Inr undefined)) =
+           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
+                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+            else Inr (Inr undefined))")
+apply (thin_tac "atom b \<sharp> (xa, ya)")
+apply (thin_tac "atom ba \<sharp> (xa, ya)")
+apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
+apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
+apply assumption
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
+                            (Sum_Type.Projr
+                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="Sum_Type.Projr
+                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+                      Sum_Type.Projr
+                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
+                                                    (Sum_Type.Projr
+(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
+                          (Sum_Type.Projr
+                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
+                                           (Sum_Type.Projr
+                                             (subsGuard_mix_subsList_mix_subs_mix_sum
+                                               (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="succ\<onesuperior>" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply simp
+(* Here the only real goal compatibility is left *)
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+  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 add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def)
+  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
+  apply(simp)
   done
 
 termination (eqvt)