equal
deleted
inserted
replaced
72 apply(simp add: permute_eqvt[symmetric]) |
72 apply(simp add: permute_eqvt[symmetric]) |
73 apply(simp add: fresh_star_permute_iff) |
73 apply(simp add: fresh_star_permute_iff) |
74 apply(clarsimp) |
74 apply(clarsimp) |
75 done |
75 done |
76 |
76 |
77 (* introduced for examples *) |
77 lemma alpha_gen_compose_sym: |
78 lemma alpha_gen_atom_sym: |
78 assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
79 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
79 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
80 shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow> |
80 shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
81 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
81 using b apply - |
82 apply(erule exE) |
82 apply(erule exE) |
83 apply(rule_tac x="- pi" in exI) |
83 apply(rule_tac x="- pi" in exI) |
84 apply(simp add: alpha_gen.simps) |
84 apply(simp add: alpha_gen.simps) |
85 apply(erule conjE)+ |
85 apply(erule conjE)+ |
86 apply(rule conjI) |
86 apply(rule conjI) |
89 apply simp |
89 apply simp |
90 apply(rule a) |
90 apply(rule a) |
91 apply assumption |
91 apply assumption |
92 done |
92 done |
93 |
93 |
94 lemma alpha_gen_atom_trans: |
94 lemma alpha_gen_compose_trans: |
95 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
95 assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
96 shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta); |
96 and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)" |
97 \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk> |
97 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
98 \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)" |
98 shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)" |
|
99 using b c apply - |
99 apply(simp add: alpha_gen.simps) |
100 apply(simp add: alpha_gen.simps) |
100 apply(erule conjE)+ |
101 apply(erule conjE)+ |
101 apply(erule exE)+ |
102 apply(erule exE)+ |
102 apply(erule conjE)+ |
103 apply(erule conjE)+ |
103 apply(rule_tac x="pia + pi" in exI) |
104 apply(rule_tac x="pia + pi" in exI) |