equal
deleted
inserted
replaced
93 | a2: "\<lbrakk>t1 \<approx>a t2; s1 \<approx>a s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a rApp t2 s2" |
93 | a2: "\<lbrakk>t1 \<approx>a t2; s1 \<approx>a s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a rApp t2 s2" |
94 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s) |
94 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s) |
95 \<Longrightarrow> rLam a t \<approx>a rLam b s" |
95 \<Longrightarrow> rLam a t \<approx>a rLam b s" |
96 |
96 |
97 lemma a3_inverse: |
97 lemma a3_inverse: |
98 assumes "rLam a t \<approx> rLam b s" |
98 assumes "rLam a t \<approx>a rLam b s" |
99 shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)" |
99 shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s)" |
100 using assms |
100 using assms |
101 apply(erule_tac alpha.cases) |
101 apply(erule_tac alpha.cases) |
102 apply(auto) |
102 apply(auto) |
103 done |
103 done |
104 |
104 |
105 text {* should be automatic with new version of eqvt-machinery *} |
105 text {* should be automatic with new version of eqvt-machinery *} |
106 lemma alpha_eqvt: |
106 lemma alpha_eqvt: |
107 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
107 shows "t \<approx>a s \<Longrightarrow> (pi \<bullet> t) \<approx>a (pi \<bullet> s)" |
108 apply(induct rule: alpha.induct) |
108 apply(induct rule: alpha.induct) |
109 apply(simp add: a1) |
109 apply(simp add: a1) |
110 apply(simp add: a2) |
110 apply(simp add: a2) |
111 apply(simp) |
111 apply(simp) |
112 apply(rule a3) |
112 apply(rule a3) |
124 apply(subst permute_eqvt[symmetric]) |
124 apply(subst permute_eqvt[symmetric]) |
125 apply(simp) |
125 apply(simp) |
126 done |
126 done |
127 |
127 |
128 lemma alpha_refl: |
128 lemma alpha_refl: |
129 shows "t \<approx> t" |
129 shows "t \<approx>a t" |
130 apply(induct t rule: rlam.induct) |
130 apply(induct t rule: rlam.induct) |
131 apply(simp add: a1) |
131 apply(simp add: a1) |
132 apply(simp add: a2) |
132 apply(simp add: a2) |
133 apply(rule a3) |
133 apply(rule a3) |
134 apply(rule_tac x="0" in exI) |
134 apply(rule_tac x="0" in exI) |
135 apply(simp_all add: fresh_star_def fresh_zero_perm) |
135 apply(simp_all add: fresh_star_def fresh_zero_perm) |
136 done |
136 done |
137 |
137 |
138 lemma alpha_sym: |
138 lemma alpha_sym: |
139 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
139 shows "t \<approx>a s \<Longrightarrow> s \<approx>a t" |
140 apply(induct rule: alpha.induct) |
140 apply(induct rule: alpha.induct) |
141 apply(simp add: a1) |
141 apply(simp add: a1) |
142 apply(simp add: a2) |
142 apply(simp add: a2) |
143 apply(rule a3) |
143 apply(rule a3) |
144 apply(erule exE) |
144 apply(erule exE) |
150 apply(drule_tac pi="- pi" in alpha_eqvt) |
150 apply(drule_tac pi="- pi" in alpha_eqvt) |
151 apply(simp) |
151 apply(simp) |
152 done |
152 done |
153 |
153 |
154 lemma alpha_trans: |
154 lemma alpha_trans: |
155 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
155 shows "t1 \<approx>a t2 \<Longrightarrow> t2 \<approx>a t3 \<Longrightarrow> t1 \<approx>a t3" |
156 apply(induct arbitrary: t3 rule: alpha.induct) |
156 apply(induct arbitrary: t3 rule: alpha.induct) |
157 apply(erule alpha.cases) |
157 apply(erule alpha.cases) |
158 apply(simp_all) |
158 apply(simp_all) |
159 apply(simp add: a1) |
159 apply(simp add: a1) |
160 apply(rotate_tac 4) |
160 apply(rotate_tac 4) |
186 unfolding reflp_def symp_def transp_def |
186 unfolding reflp_def symp_def transp_def |
187 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
187 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
188 done |
188 done |
189 |
189 |
190 lemma alpha_rfv: |
190 lemma alpha_rfv: |
191 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
191 shows "t \<approx>a s \<Longrightarrow> rfv t = rfv s" |
192 apply(induct rule: alpha.induct) |
192 apply(induct rule: alpha.induct) |
193 apply(simp_all) |
193 apply(simp_all) |
194 done |
194 done |
195 |
195 |
196 inductive |
196 inductive |
197 alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
197 alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a2 _" [100, 100] 100) |
198 where |
198 where |
199 a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)" |
199 a21: "a = b \<Longrightarrow> (rVar a) \<approx>a2 (rVar b)" |
200 | a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2" |
200 | a22: "\<lbrakk>t1 \<approx>a2 t2; s1 \<approx>a2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a2 rApp t2 s2" |
201 | a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s" |
201 | a23: "(a = b \<and> t \<approx>a2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>a2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>a2 rLam b s" |
202 |
202 |
203 lemma fv_vars: |
203 lemma fv_vars: |
204 fixes a::name |
204 fixes a::name |
205 assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x" |
205 assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x" |
206 shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)" |
206 shows "(pi \<bullet> t) \<approx>a2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)" |
207 using a1 |
207 using a1 |
208 apply(induct t) |
208 apply(induct t) |
209 apply(auto) |
209 apply(auto) |
210 apply(rule a21) |
210 apply(rule a21) |
211 apply(case_tac "name = a") |
211 apply(case_tac "name = a") |
220 apply(simp) |
220 apply(simp) |
221 oops |
221 oops |
222 |
222 |
223 |
223 |
224 lemma |
224 lemma |
225 assumes a1: "t \<approx>2 s" |
225 assumes a1: "t \<approx>a2 s" |
226 shows "t \<approx> s" |
226 shows "t \<approx>a s" |
227 using a1 |
227 using a1 |
228 apply(induct) |
228 apply(induct) |
229 apply(rule alpha.intros) |
229 apply(rule alpha.intros) |
230 apply(simp) |
230 apply(simp) |
231 apply(rule alpha.intros) |
231 apply(rule alpha.intros) |
252 |
252 |
253 defer |
253 defer |
254 sorry |
254 sorry |
255 |
255 |
256 lemma |
256 lemma |
257 assumes a1: "t \<approx> s" |
257 assumes a1: "t \<approx>a s" |
258 shows "t \<approx>2 s" |
258 shows "t \<approx>a2 s" |
259 using a1 |
259 using a1 |
260 apply(induct) |
260 apply(induct) |
261 apply(rule alpha2.intros) |
261 apply(rule alpha2.intros) |
262 apply(simp) |
262 apply(simp) |
263 apply(rule alpha2.intros) |
263 apply(rule alpha2.intros) |
443 apply(rule a3) |
443 apply(rule a3) |
444 apply(assumption) |
444 apply(assumption) |
445 done |
445 done |
446 |
446 |
447 lemma rlam_distinct: |
447 lemma rlam_distinct: |
448 shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
448 shows "\<not>(rVar nam \<approx>a rApp rlam1' rlam2')" |
449 and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
449 and "\<not>(rApp rlam1' rlam2' \<approx>a rVar nam)" |
450 and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
450 and "\<not>(rVar nam \<approx>a rLam nam' rlam')" |
451 and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
451 and "\<not>(rLam nam' rlam' \<approx>a rVar nam)" |
452 and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
452 and "\<not>(rApp rlam1 rlam2 \<approx>a rLam nam' rlam')" |
453 and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
453 and "\<not>(rLam nam' rlam' \<approx>a rApp rlam1 rlam2)" |
454 apply auto |
454 apply auto |
455 apply (erule alpha.cases) |
455 apply (erule alpha.cases) |
456 apply (simp_all only: rlam.distinct) |
456 apply (simp_all only: rlam.distinct) |
457 apply (erule alpha.cases) |
457 apply (erule alpha.cases) |
458 apply (simp_all only: rlam.distinct) |
458 apply (simp_all only: rlam.distinct) |