33 "subst_name_list a [] = a" |
33 "subst_name_list a [] = a" |
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
35 apply(auto) |
35 apply(auto) |
36 apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)") |
36 apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)") |
37 unfolding eqvt_def |
37 unfolding eqvt_def |
|
38 apply(simp only: permute_fun_def) |
38 apply(rule allI) |
39 apply(rule allI) |
39 apply(simp add: permute_fun_def) |
|
40 apply(rule ext) |
40 apply(rule ext) |
41 apply(rule ext) |
41 apply(rule ext) |
42 apply(simp add: permute_bool_def) |
42 apply(simp only: permute_bool_def) |
43 apply(rule iffI) |
43 apply(rule iffI) |
44 apply(drule_tac x="p" in meta_spec) |
44 apply(drule_tac x="p" in meta_spec) |
45 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
45 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
46 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
46 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
47 apply(simp) |
47 apply(simp) |
181 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>" |
181 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>" |
182 apply(auto simp add: piMix_distinct piMix_eq_iff) |
182 apply(auto simp add: piMix_distinct piMix_eq_iff) |
183 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)") |
183 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)") |
184 unfolding eqvt_def |
184 unfolding eqvt_def |
185 apply(rule allI) |
185 apply(rule allI) |
186 apply(simp add: permute_fun_def) |
186 apply(simp only: permute_fun_def) |
187 apply(rule ext) |
187 apply(rule ext) |
188 apply(rule ext) |
188 apply(rule ext) |
189 apply(simp add: permute_bool_def) |
189 apply(simp only: permute_bool_def) |
190 apply(rule iffI) |
190 apply(rule iffI) |
191 apply(drule_tac x="p" in meta_spec) |
191 apply(drule_tac x="p" in meta_spec) |
192 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
192 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
193 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
193 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
194 apply(simp) |
194 apply(simp) |
301 apply(auto simp add: fresh_star_def)[1] |
301 apply(auto simp add: fresh_star_def)[1] |
302 apply(blast) |
302 apply(blast) |
303 apply(simp) |
303 apply(simp) |
304 apply(blast) |
304 apply(blast) |
305 --"compatibility" |
305 --"compatibility" |
306 apply (simp add: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
306 apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
307 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
307 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
308 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
308 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
309 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |
309 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |
310 prefer 2 |
310 prefer 2 |
311 apply (simp add: eqvt_at_def subs_mix_def) |
311 apply (simp only: eqvt_at_def subs_mix_def) |
312 apply rule |
312 apply rule |
|
313 apply(simp (no_asm)) |
313 apply (subst testrr) |
314 apply (subst testrr) |
314 apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def) |
315 apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def) |
315 apply (simp add: THE_default_def) |
316 apply (simp add: THE_default_def) |
316 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
317 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
317 apply simp_all[2] |
318 apply simp_all[2] |
387 apply (erule Abs_lst1_fcb) |
388 apply (erule Abs_lst1_fcb) |
388 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
389 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
389 apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)") |
390 apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)") |
390 apply simp |
391 apply simp |
391 apply (erule fresh_eqvt_at) |
392 apply (erule fresh_eqvt_at) |
392 apply (simp_all add: fresh_Pair finite_supp eqvts eqvt_at_def fresh_Pair swap_fresh_fresh) |
393 apply(simp add: finite_supp) |
|
394 apply(simp) |
|
395 apply(simp add: eqvt_at_def) |
|
396 apply(drule_tac x="(atom b \<rightleftharpoons> atom ba)" in spec) |
|
397 apply(simp) |
393 done |
398 done |
394 |
399 |
395 termination (eqvt) |
400 termination (eqvt) |
396 by (lexicographic_order) |
401 by (lexicographic_order) |
397 |
402 |