46 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric]) |
48 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric]) |
47 apply(fold supp_def) |
49 apply(fold supp_def) |
48 apply(simp add: supp_atm) |
50 apply(simp add: supp_atm) |
49 done |
51 done |
50 |
52 |
|
53 declare set_diff_eqvt[eqvt] |
|
54 |
|
55 lemma rfv_eqvt[eqvt]: |
|
56 fixes pi::"name prm" |
|
57 shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)" |
|
58 apply(induct t) |
|
59 apply(simp_all) |
|
60 apply(simp add: perm_set_eq) |
|
61 apply(simp add: union_eqvt) |
|
62 apply(simp add: set_diff_eqvt) |
|
63 apply(simp add: perm_set_eq) |
|
64 done |
|
65 |
51 inductive |
66 inductive |
52 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
67 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
53 where |
68 where |
54 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
55 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
70 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
56 | a3: "\<lbrakk>t \<approx> ([(a,b)] \<bullet> s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s" |
71 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
57 |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
58 lemma helper: |
73 |
59 fixes t::"rlam" |
74 (* should be automatic with new version of eqvt-machinery *) |
60 and a::"name" |
75 lemma alpha_eqvt: |
61 shows "[(a, a)] \<bullet> t = t" |
76 fixes pi::"name prm" |
62 by (induct t) |
77 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
63 (auto simp add: calc_atm) |
78 apply(induct rule: alpha.induct) |
|
79 apply(simp add: a1) |
|
80 apply(simp add: a2) |
|
81 apply(simp) |
|
82 apply(rule a3) |
|
83 apply(erule conjE) |
|
84 apply(erule exE) |
|
85 apply(erule conjE) |
|
86 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
87 apply(rule conjI) |
|
88 apply(rule_tac pi1="rev pi" in perm_bij[THEN iffD1]) |
|
89 apply(perm_simp add: eqvts) |
|
90 apply(rule conjI) |
|
91 apply(rule_tac pi1="rev pi" in pt_fresh_star_bij(1)[OF pt_name_inst at_name_inst, THEN iffD1]) |
|
92 apply(perm_simp add: eqvts) |
|
93 apply(rule conjI) |
|
94 apply(subst perm_compose[symmetric]) |
|
95 apply(simp) |
|
96 apply(subst perm_compose[symmetric]) |
|
97 apply(simp) |
|
98 done |
64 |
99 |
65 lemma alpha_refl: |
100 lemma alpha_refl: |
66 fixes t::"rlam" |
|
67 shows "t \<approx> t" |
101 shows "t \<approx> t" |
68 apply(induct t rule: rlam.induct) |
102 apply(induct t rule: rlam.induct) |
69 apply(simp add: a1) |
103 apply(simp add: a1) |
70 apply(simp add: a2) |
104 apply(simp add: a2) |
71 apply(rule a3) |
105 apply(rule a3) |
72 apply(simp add: helper) |
106 apply(rule_tac x="[]" in exI) |
73 apply(simp) |
107 apply(simp_all add: fresh_star_def fresh_list_nil) |
74 done |
108 done |
|
109 |
|
110 lemma alpha_sym: |
|
111 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
|
112 apply(induct rule: alpha.induct) |
|
113 apply(simp add: a1) |
|
114 apply(simp add: a2) |
|
115 apply(rule a3) |
|
116 apply(erule exE) |
|
117 apply(rule_tac x="rev pi" in exI) |
|
118 apply(simp) |
|
119 apply(simp add: fresh_star_def fresh_list_rev) |
|
120 apply(rule conjI) |
|
121 apply(erule conjE)+ |
|
122 apply(rotate_tac 3) |
|
123 apply(drule_tac pi="rev pi" in alpha_eqvt) |
|
124 apply(perm_simp) |
|
125 apply(rule pt_bij2[OF pt_name_inst at_name_inst]) |
|
126 apply(simp) |
|
127 done |
|
128 |
|
129 lemma alpha_trans: |
|
130 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
|
131 apply(induct arbitrary: t3 rule: alpha.induct) |
|
132 apply(erule alpha.cases) |
|
133 apply(simp_all) |
|
134 apply(simp add: a1) |
|
135 apply(rotate_tac 4) |
|
136 apply(erule alpha.cases) |
|
137 apply(simp_all) |
|
138 apply(simp add: a2) |
|
139 apply(rotate_tac 1) |
|
140 apply(erule alpha.cases) |
|
141 apply(simp_all) |
|
142 apply(erule conjE)+ |
|
143 apply(erule exE)+ |
|
144 apply(erule conjE)+ |
|
145 apply(rule a3) |
|
146 apply(rule_tac x="pia @ pi" in exI) |
|
147 apply(simp add: fresh_star_def fresh_list_append) |
|
148 apply(simp add: pt_name2) |
|
149 apply(drule_tac x="rev pia \<bullet> sa" in spec) |
|
150 apply(drule mp) |
|
151 apply(rotate_tac 8) |
|
152 apply(drule_tac pi="rev pia" in alpha_eqvt) |
|
153 apply(perm_simp) |
|
154 apply(rotate_tac 11) |
|
155 apply(drule_tac pi="pia" in alpha_eqvt) |
|
156 apply(perm_simp) |
|
157 done |
75 |
158 |
76 lemma alpha_equivp: |
159 lemma alpha_equivp: |
77 shows "equivp alpha" |
160 shows "equivp alpha" |
78 sorry |
161 apply(rule equivpI) |
|
162 unfolding reflp_def symp_def transp_def |
|
163 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
|
164 done |
|
165 |
|
166 lemma alpha_rfv: |
|
167 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
|
168 apply(induct rule: alpha.induct) |
|
169 apply(simp) |
|
170 apply(simp) |
|
171 apply(simp) |
|
172 done |
79 |
173 |
80 quotient_type lam = rlam / alpha |
174 quotient_type lam = rlam / alpha |
81 by (rule alpha_equivp) |
175 by (rule alpha_equivp) |
82 |
176 |
83 |
177 |
141 by (auto intro: a2) |
228 by (auto intro: a2) |
142 |
229 |
143 lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam" |
230 lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam" |
144 apply(auto) |
231 apply(auto) |
145 apply(rule a3) |
232 apply(rule a3) |
146 apply(simp add: helper) |
233 apply(rule_tac x="[]" in exI) |
147 apply(simp) |
234 unfolding fresh_star_def |
|
235 apply(simp add: fresh_list_nil) |
|
236 apply(simp add: alpha_rfv) |
148 done |
237 done |
149 |
238 |
150 lemma rfv_rsp[quot_respect]: |
239 lemma rfv_rsp[quot_respect]: |
151 "(alpha ===> op =) rfv rfv" |
240 "(alpha ===> op =) rfv rfv" |
152 sorry |
241 apply(simp add: alpha_rfv) |
153 |
242 done |
154 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
243 |
155 apply (auto) |
244 section {* lifted theorems *} |
156 apply (erule alpha.cases) |
|
157 apply (simp_all add: rlam.inject alpha_refl) |
|
158 done |
|
159 |
|
160 |
245 |
161 lemma lam_induct: |
246 lemma lam_induct: |
162 "\<lbrakk>\<And>name. P (Var name); |
247 "\<lbrakk>\<And>name. P (Var name); |
163 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
248 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
164 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
249 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
194 lemma a2: |
279 lemma a2: |
195 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
280 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
196 by (lifting a2) |
281 by (lifting a2) |
197 |
282 |
198 lemma a3: |
283 lemma a3: |
199 "\<lbrakk>x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa" |
284 "\<lbrakk>\<exists>pi::name prm. (fv t - {a} = fv s - {b} \<and> (fv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk> |
|
285 \<Longrightarrow> Lam a t = Lam b s" |
200 by (lifting a3) |
286 by (lifting a3) |
201 |
287 |
202 lemma alpha_cases: |
288 lemma alpha_cases: |
203 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
289 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
204 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
290 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
205 \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
291 \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
|
292 \<exists>pi::name prm. fv t - {a} = fv s - {b} \<and> (fv t - {a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> \<Longrightarrow> P\<rbrakk> |
206 \<Longrightarrow> P" |
293 \<Longrightarrow> P" |
207 by (lifting alpha.cases) |
294 by (lifting alpha.cases) |
208 |
295 |
209 lemma alpha_induct: |
296 lemma alpha_induct: |
210 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
297 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
211 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
298 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
212 \<And>x a b xa. |
299 \<And>t a s b. |
213 \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk> |
300 \<lbrakk>\<exists>pi::name prm. fv t - {a} = fv s - {b} \<and> |
|
301 (fv t - {a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk> \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
214 \<Longrightarrow> qxb qx qxa" |
302 \<Longrightarrow> qxb qx qxa" |
215 by (lifting alpha.induct) |
303 by (lifting alpha.induct) |
216 |
304 |
217 lemma var_inject: |
305 lemma lam_inject [simp]: |
218 "(Var a = Var b) = (a = b)" |
306 shows "(Var a = Var b) = (a = b)" |
219 by (lifting rvar_inject) |
307 and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
220 |
308 apply(lifting rlam.inject(1) rlam.inject(2)) |
221 |
309 apply(auto) |
222 lemma app_inject: |
310 apply(drule alpha.cases) |
223 "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
311 apply(simp_all) |
224 sorry |
312 apply(simp add: alpha.a1) |
|
313 apply(drule alpha.cases) |
|
314 apply(simp_all) |
|
315 apply(drule alpha.cases) |
|
316 apply(simp_all) |
|
317 apply(rule alpha.a2) |
|
318 apply(simp_all) |
|
319 done |
225 |
320 |
226 lemma var_supp1: |
321 lemma var_supp1: |
227 shows "(supp (Var a)) = ((supp a)::name set)" |
322 shows "(supp (Var a)) = ((supp a)::name set)" |
228 apply(simp add: supp_def var_inject) |
323 apply(simp add: supp_def) |
229 done |
324 done |
230 |
325 |
231 lemma var_supp: |
326 lemma var_supp: |
232 shows "(supp (Var a)) = {a::name}" |
327 shows "(supp (Var a)) = {a::name}" |
233 using var_supp1 |
328 using var_supp1 |
234 apply(simp add: supp_atm) |
329 apply(simp add: supp_atm) |
235 done |
330 done |
236 |
331 |
237 lemma app_supp: |
332 lemma app_supp: |
238 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
333 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
239 apply(simp only: perm_lam supp_def app_inject) |
334 apply(simp only: perm_lam supp_def lam_inject) |
240 apply(simp add: Collect_imp_eq Collect_neg_eq) |
335 apply(simp add: Collect_imp_eq Collect_neg_eq) |
241 done |
336 done |
242 |
337 |
243 lemma lam_supp: |
338 lemma lam_supp: |
244 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
339 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
245 apply(simp add: supp_def) |
340 apply(simp add: supp_def) |
|
341 apply(simp add: abs_perm) |
246 sorry |
342 sorry |
247 |
343 |
248 |
344 |
249 instance lam::fs_name |
345 instance lam::fs_name |
250 apply(default) |
346 apply(default) |
251 apply(induct_tac x rule: lam_induct) |
347 apply(induct_tac x rule: lam_induct) |
252 apply(simp add: var_supp) |
348 apply(simp add: var_supp) |
253 apply(simp add: app_supp) |
349 apply(simp add: app_supp) |
254 sorry |
350 apply(simp add: lam_supp abs_supp) |
|
351 done |
255 |
352 |
256 lemma fresh_lam: |
353 lemma fresh_lam: |
257 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
354 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
258 apply(simp add: fresh_def) |
355 apply(simp add: fresh_def) |
259 apply(simp add: lam_supp abs_supp) |
356 apply(simp add: lam_supp abs_supp) |