53 declare set_diff_eqvt[eqvt] |
53 declare set_diff_eqvt[eqvt] |
54 |
54 |
55 lemma rfv_eqvt[eqvt]: |
55 lemma rfv_eqvt[eqvt]: |
56 fixes pi::"name prm" |
56 fixes pi::"name prm" |
57 shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)" |
57 shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)" |
58 apply(induct t) |
58 apply(induct t) |
59 apply(simp_all) |
59 apply(simp_all) |
60 apply(simp add: perm_set_eq) |
60 apply(simp add: perm_set_eq) |
61 apply(simp add: union_eqvt) |
61 apply(simp add: union_eqvt) |
62 apply(simp add: set_diff_eqvt) |
62 apply(simp add: set_diff_eqvt) |
63 apply(simp add: perm_set_eq) |
63 apply(simp add: perm_set_eq) |
64 done |
64 done |
65 |
65 |
66 inductive |
66 inductive |
67 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
67 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
68 where |
68 where |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
70 | 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" |
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) |
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) |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
74 |
74 |
75 (* should be automatic with new version of eqvt-machinery *) |
75 (* should be automatic with new version of eqvt-machinery *) |
76 lemma alpha_eqvt: |
76 lemma alpha_eqvt: |
77 fixes pi::"name prm" |
77 fixes pi::"name prm" |
78 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
78 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
79 apply(induct rule: alpha.induct) |
79 apply(induct rule: alpha.induct) |
80 apply(simp add: a1) |
80 apply(simp add: a1) |
81 apply(simp add: a2) |
81 apply(simp add: a2) |
82 apply(simp) |
82 apply(simp) |
83 apply(rule a3) |
83 apply(rule a3) |
84 apply(erule conjE) |
84 apply(erule conjE) |
85 apply(erule exE) |
85 apply(erule exE) |
86 apply(erule conjE) |
86 apply(erule conjE) |
87 apply(rule_tac x="pi \<bullet> pia" in exI) |
87 apply(rule_tac x="pi \<bullet> pia" in exI) |
88 apply(rule conjI) |
88 apply(rule conjI) |
89 apply(rule_tac pi1="rev pi" in perm_bij[THEN iffD1]) |
89 apply(rule_tac pi1="rev pi" in perm_bij[THEN iffD1]) |
90 apply(perm_simp add: eqvts) |
90 apply(perm_simp add: eqvts) |
91 apply(rule conjI) |
91 apply(rule conjI) |
92 apply(rule_tac pi1="rev pi" in pt_fresh_star_bij(1)[OF pt_name_inst at_name_inst, THEN iffD1]) |
92 apply(rule_tac pi1="rev pi" in pt_fresh_star_bij(1)[OF pt_name_inst at_name_inst, THEN iffD1]) |
93 apply(perm_simp add: eqvts) |
93 apply(perm_simp add: eqvts) |
94 apply(rule conjI) |
94 apply(rule conjI) |
95 apply(subst perm_compose[symmetric]) |
95 apply(subst perm_compose[symmetric]) |
96 apply(simp) |
96 apply(simp) |
97 apply(subst perm_compose[symmetric]) |
97 apply(subst perm_compose[symmetric]) |
98 apply(simp) |
98 apply(simp) |
99 done |
99 done |
100 |
100 |
101 lemma alpha_refl: |
101 lemma alpha_refl: |
102 shows "t \<approx> t" |
102 shows "t \<approx> t" |
103 apply(induct t rule: rlam.induct) |
103 apply(induct t rule: rlam.induct) |
104 apply(simp add: a1) |
104 apply(simp add: a1) |
105 apply(simp add: a2) |
105 apply(simp add: a2) |
106 apply(rule a3) |
106 apply(rule a3) |
107 apply(rule_tac x="[]" in exI) |
107 apply(rule_tac x="[]" in exI) |
108 apply(simp_all add: fresh_star_def fresh_list_nil) |
108 apply(simp_all add: fresh_star_def fresh_list_nil) |
109 done |
109 done |
110 |
110 |
111 lemma alpha_sym: |
111 lemma alpha_sym: |
112 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
112 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
113 apply(induct rule: alpha.induct) |
113 apply(induct rule: alpha.induct) |
114 apply(simp add: a1) |
114 apply(simp add: a1) |
115 apply(simp add: a2) |
115 apply(simp add: a2) |
116 apply(rule a3) |
116 apply(rule a3) |
117 apply(erule exE) |
117 apply(erule exE) |
118 apply(rule_tac x="rev pi" in exI) |
118 apply(rule_tac x="rev pi" in exI) |
119 apply(simp) |
119 apply(simp) |
120 apply(simp add: fresh_star_def fresh_list_rev) |
120 apply(simp add: fresh_star_def fresh_list_rev) |
121 apply(rule conjI) |
121 apply(rule conjI) |
122 apply(erule conjE)+ |
122 apply(erule conjE)+ |
123 apply(rotate_tac 3) |
123 apply(rotate_tac 3) |
124 apply(drule_tac pi="rev pi" in alpha_eqvt) |
124 apply(drule_tac pi="rev pi" in alpha_eqvt) |
125 apply(perm_simp) |
125 apply(perm_simp) |
126 apply(rule pt_bij2[OF pt_name_inst at_name_inst]) |
126 apply(rule pt_bij2[OF pt_name_inst at_name_inst]) |
127 apply(simp) |
127 apply(simp) |
128 done |
128 done |
129 |
129 |
130 lemma alpha_trans: |
130 lemma alpha_trans: |
131 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
131 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
132 apply(induct arbitrary: t3 rule: alpha.induct) |
132 apply(induct arbitrary: t3 rule: alpha.induct) |
133 apply(erule alpha.cases) |
133 apply(erule alpha.cases) |
134 apply(simp_all) |
134 apply(simp_all) |
135 apply(simp add: a1) |
135 apply(simp add: a1) |
136 apply(rotate_tac 4) |
136 apply(rotate_tac 4) |
137 apply(erule alpha.cases) |
137 apply(erule alpha.cases) |
138 apply(simp_all) |
138 apply(simp_all) |
139 apply(simp add: a2) |
139 apply(simp add: a2) |
140 apply(rotate_tac 1) |
140 apply(rotate_tac 1) |
141 apply(erule alpha.cases) |
141 apply(erule alpha.cases) |
142 apply(simp_all) |
142 apply(simp_all) |
143 apply(erule conjE)+ |
143 apply(erule conjE)+ |
144 apply(erule exE)+ |
144 apply(erule exE)+ |
145 apply(erule conjE)+ |
145 apply(erule conjE)+ |
146 apply(rule a3) |
146 apply(rule a3) |
147 apply(rule_tac x="pia @ pi" in exI) |
147 apply(rule_tac x="pia @ pi" in exI) |
148 apply(simp add: fresh_star_def fresh_list_append) |
148 apply(simp add: fresh_star_def fresh_list_append) |
149 apply(simp add: pt_name2) |
149 apply(simp add: pt_name2) |
150 apply(drule_tac x="rev pia \<bullet> sa" in spec) |
150 apply(drule_tac x="rev pia \<bullet> sa" in spec) |
151 apply(drule mp) |
151 apply(drule mp) |
152 apply(rotate_tac 8) |
152 apply(rotate_tac 8) |
153 apply(drule_tac pi="rev pia" in alpha_eqvt) |
153 apply(drule_tac pi="rev pia" in alpha_eqvt) |
154 apply(perm_simp) |
154 apply(perm_simp) |
155 apply(rotate_tac 11) |
155 apply(rotate_tac 11) |
156 apply(drule_tac pi="pia" in alpha_eqvt) |
156 apply(drule_tac pi="pia" in alpha_eqvt) |
157 apply(perm_simp) |
157 apply(perm_simp) |
158 done |
158 done |
159 |
159 |
160 lemma alpha_equivp: |
160 lemma alpha_equivp: |
161 shows "equivp alpha" |
161 shows "equivp alpha" |
162 apply(rule equivpI) |
162 apply(rule equivpI) |
163 unfolding reflp_def symp_def transp_def |
163 unfolding reflp_def symp_def transp_def |
164 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
164 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
165 done |
165 done |
166 |
166 |
167 lemma alpha_rfv: |
167 lemma alpha_rfv: |
168 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
168 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
169 apply(induct rule: alpha.induct) |
169 apply(induct rule: alpha.induct) |
170 apply(simp) |
170 apply(simp) |
171 apply(simp) |
171 apply(simp) |
172 apply(simp) |
172 apply(simp) |
173 done |
173 done |
174 |
174 |
175 quotient_type lam = rlam / alpha |
175 quotient_type lam = rlam / alpha |
176 by (rule alpha_equivp) |
176 by (rule alpha_equivp) |
177 |
177 |
178 |
178 |
237 apply(simp add: alpha_rfv) |
231 apply(simp add: alpha_rfv) |
238 done |
232 done |
239 |
233 |
240 lemma rfv_rsp[quot_respect]: |
234 lemma rfv_rsp[quot_respect]: |
241 "(alpha ===> op =) rfv rfv" |
235 "(alpha ===> op =) rfv rfv" |
242 apply(simp add: alpha_rfv) |
236 apply(simp add: alpha_rfv) |
243 done |
237 done |
244 |
238 |
245 section {* lifted theorems *} |
239 section {* lifted theorems *} |
246 |
240 |
247 lemma lam_induct: |
241 lemma lam_induct: |
248 "\<lbrakk>\<And>name. P (Var name); |
242 "\<lbrakk>\<And>name. P (Var name); |
249 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
243 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
250 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
244 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
251 \<Longrightarrow> P lam" |
245 \<Longrightarrow> P lam" |
252 by (lifting rlam.induct) |
246 by (lifting rlam.induct) |
253 |
247 |
254 ML {* show_all_types := true *} |
|
255 |
|
256 lemma perm_lam [simp]: |
248 lemma perm_lam [simp]: |
257 fixes pi::"'a prm" |
249 fixes pi::"name prm" |
258 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
250 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
259 and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
251 and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
260 and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)" |
252 and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)" |
261 apply(lifting perm_rlam.simps) |
253 by (lifting perm_rlam.simps[where 'a="name"]) |
262 ML_prf {* |
|
263 List.last (map (symmetric o #def) (Quotient_Info.qconsts_dest @{context})); |
|
264 List.last (map (Thm.varifyT o symmetric o #def) (Quotient_Info.qconsts_dest @{context})) |
|
265 *} |
|
266 done |
|
267 |
254 |
268 instance lam::pt_name |
255 instance lam::pt_name |
269 apply(default) |
256 apply(default) |
270 apply(induct_tac [!] x rule: lam_induct) |
257 apply(induct_tac [!] x rule: lam_induct) |
271 apply(simp_all add: pt_name2 pt_name3) |
258 apply(simp_all add: pt_name2 pt_name3) |
272 done |
259 done |
273 |
260 |
274 lemma fv_lam [simp]: |
261 lemma fv_lam [simp]: |
275 shows "fv (Var a) = {a}" |
262 shows "fv (Var a) = {a}" |
276 and "fv (App t1 t2) = fv t1 \<union> fv t2" |
263 and "fv (App t1 t2) = fv t1 \<union> fv t2" |
277 and "fv (Lam a t) = fv t - {a}" |
264 and "fv (Lam a t) = fv t - {a}" |
278 apply(lifting rfv_var rfv_app rfv_lam) |
265 by(lifting rfv_var rfv_app rfv_lam) |
279 done |
266 |
280 |
267 lemma a1: |
281 |
|
282 lemma a1: |
|
283 "a = b \<Longrightarrow> Var a = Var b" |
268 "a = b \<Longrightarrow> Var a = Var b" |
284 by (lifting a1) |
269 by (lifting a1) |
285 |
270 |
286 lemma a2: |
271 lemma a2: |
287 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
272 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
288 by (lifting a2) |
273 by (lifting a2) |
289 |
274 |
290 lemma a3: |
275 lemma a3: |
291 "\<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> |
276 "\<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> |
292 \<Longrightarrow> Lam a t = Lam b s" |
277 \<Longrightarrow> Lam a t = Lam b s" |
293 by (lifting a3) |
278 by (lifting a3) |
294 |
279 |
295 lemma alpha_cases: |
280 lemma alpha_cases: |
296 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
281 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
297 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
282 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
298 \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
283 \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
299 \<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> |
284 \<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> |
300 \<Longrightarrow> P" |
285 \<Longrightarrow> P" |
301 by (lifting alpha.cases) |
286 by (lifting alpha.cases) |
302 |
287 |
303 lemma alpha_induct: |
288 lemma alpha_induct: |
304 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
289 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
305 \<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); |
290 \<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); |
306 \<And>t a s b. |
291 \<And>t a s b. |
307 \<lbrakk>\<exists>pi::name prm. fv t - {a} = fv s - {b} \<and> |
292 \<lbrakk>\<exists>pi::name prm. fv t - {a} = fv s - {b} \<and> |
308 (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> |
293 (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> |
310 by (lifting alpha.induct) |
295 by (lifting alpha.induct) |
311 |
296 |
312 lemma lam_inject [simp]: |
297 lemma lam_inject [simp]: |
313 shows "(Var a = Var b) = (a = b)" |
298 shows "(Var a = Var b) = (a = b)" |
314 and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
299 and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
315 apply(lifting rlam.inject(1) rlam.inject(2)) |
300 apply(lifting rlam.inject(1) rlam.inject(2)) |
316 apply(auto) |
301 apply(auto) |
317 apply(drule alpha.cases) |
302 apply(drule alpha.cases) |
318 apply(simp_all) |
303 apply(simp_all) |
319 apply(simp add: alpha.a1) |
304 apply(simp add: alpha.a1) |
320 apply(drule alpha.cases) |
305 apply(drule alpha.cases) |
321 apply(simp_all) |
306 apply(simp_all) |
322 apply(drule alpha.cases) |
307 apply(drule alpha.cases) |
323 apply(simp_all) |
308 apply(simp_all) |
324 apply(rule alpha.a2) |
309 apply(rule alpha.a2) |
325 apply(simp_all) |
310 apply(simp_all) |
326 done |
311 done |
327 |
312 |
328 lemma rlam_distinct: |
313 lemma rlam_distinct: |
329 shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
314 shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
330 and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
315 and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
331 and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
316 and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
332 and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
317 and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
333 and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
318 and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
334 and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
319 and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
335 apply auto |
320 apply auto |
336 apply(erule alpha.cases) |
321 apply(erule alpha.cases) |
337 apply simp_all |
322 apply simp_all |
338 apply(erule alpha.cases) |
323 apply(erule alpha.cases) |
339 apply simp_all |
324 apply simp_all |
340 apply(erule alpha.cases) |
325 apply(erule alpha.cases) |
341 apply simp_all |
326 apply simp_all |
342 apply(erule alpha.cases) |
327 apply(erule alpha.cases) |
343 apply simp_all |
328 apply simp_all |
344 apply(erule alpha.cases) |
329 apply(erule alpha.cases) |
345 apply simp_all |
330 apply simp_all |
346 apply(erule alpha.cases) |
331 apply(erule alpha.cases) |
347 apply simp_all |
332 apply simp_all |
348 done |
333 done |
349 |
334 |
350 lemma lam_distinct[simp]: |
335 lemma lam_distinct[simp]: |
351 shows "Var nam \<noteq> App lam1' lam2'" |
336 shows "Var nam \<noteq> App lam1' lam2'" |
352 and "App lam1' lam2' \<noteq> Var nam" |
337 and "App lam1' lam2' \<noteq> Var nam" |
353 and "Var nam \<noteq> Lam nam' lam'" |
338 and "Var nam \<noteq> Lam nam' lam'" |
354 and "Lam nam' lam' \<noteq> Var nam" |
339 and "Lam nam' lam' \<noteq> Var nam" |
355 and "App lam1 lam2 \<noteq> Lam nam' lam'" |
340 and "App lam1 lam2 \<noteq> Lam nam' lam'" |
356 and "Lam nam' lam' \<noteq> App lam1 lam2" |
341 and "Lam nam' lam' \<noteq> App lam1 lam2" |
357 apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6)) |
342 by(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6)) |
358 done |
|
359 |
343 |
360 lemma var_supp1: |
344 lemma var_supp1: |
361 shows "(supp (Var a)) = ((supp a)::name set)" |
345 shows "(supp (Var a)) = ((supp a)::name set)" |
362 by (simp add: supp_def) |
346 by (simp add: supp_def) |
363 |
347 |
365 shows "(supp (Var a)) = {a::name}" |
349 shows "(supp (Var a)) = {a::name}" |
366 using var_supp1 by (simp add: supp_atm) |
350 using var_supp1 by (simp add: supp_atm) |
367 |
351 |
368 lemma app_supp: |
352 lemma app_supp: |
369 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
353 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
370 apply(simp only: perm_lam supp_def lam_inject) |
354 apply(simp only: perm_lam supp_def lam_inject) |
371 apply(simp add: Collect_imp_eq Collect_neg_eq) |
355 apply(simp add: Collect_imp_eq Collect_neg_eq) |
372 done |
356 done |
373 |
357 |
374 lemma lam_supp: |
358 lemma lam_supp: |
375 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
359 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
376 apply(simp add: supp_def) |
360 apply(simp add: supp_def) |
377 apply(simp add: abs_perm) |
361 apply(simp add: abs_perm) |
378 sorry |
362 sorry |
379 |
|
380 |
363 |
381 instance lam::fs_name |
364 instance lam::fs_name |
382 apply(default) |
365 apply(default) |
383 apply(induct_tac x rule: lam_induct) |
366 apply(induct_tac x rule: lam_induct) |
384 apply(simp add: var_supp) |
367 apply(simp add: var_supp) |
385 apply(simp add: app_supp) |
368 apply(simp add: app_supp) |
386 apply(simp add: lam_supp abs_supp) |
369 apply(simp add: lam_supp abs_supp) |
387 done |
370 done |
388 |
371 |
389 lemma fresh_lam: |
372 lemma fresh_lam: |
390 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
373 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
391 apply(simp add: fresh_def) |
374 apply(simp add: fresh_def) |
392 apply(simp add: lam_supp abs_supp) |
375 apply(simp add: lam_supp abs_supp) |
393 apply(auto) |
376 apply(auto) |
394 done |
377 done |
395 |
378 |
396 lemma lam_induct_strong: |
379 lemma lam_induct_strong: |
397 fixes a::"'a::fs_name" |
380 fixes a::"'a::fs_name" |
398 assumes a1: "\<And>name b. P b (Var name)" |
381 assumes a1: "\<And>name b. P b (Var name)" |
399 and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |
382 and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |