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