equal
deleted
inserted
replaced
118 assumes "rLam a t \<approx> rLam b s" |
118 assumes "rLam a t \<approx> rLam b s" |
119 shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))" |
119 shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))" |
120 using assms |
120 using assms |
121 apply(erule_tac alpha.cases) |
121 apply(erule_tac alpha.cases) |
122 apply(auto) |
122 apply(auto) |
123 done |
|
124 |
|
125 lemma alpha_gen_eqvt_atom: |
|
126 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
|
127 shows "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s) \<Longrightarrow> \<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
|
128 apply(erule exE) |
|
129 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
130 apply(simp add: alpha_gen.simps) |
|
131 apply(erule conjE)+ |
|
132 apply(rule conjI)+ |
|
133 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
134 apply(simp add: a[symmetric] atom_eqvt eqvts) |
|
135 apply(rule conjI) |
|
136 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
137 apply(simp add: a[symmetric] eqvts atom_eqvt) |
|
138 apply(subst permute_eqvt[symmetric]) |
|
139 apply(simp) |
|
140 done |
123 done |
141 |
124 |
142 text {* should be automatic with new version of eqvt-machinery *} |
125 text {* should be automatic with new version of eqvt-machinery *} |
143 lemma alpha_eqvt: |
126 lemma alpha_eqvt: |
144 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
127 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |