239 |
239 |
240 lemma var_inject: |
240 lemma var_inject: |
241 "(Var a = Var b) = (a = b)" |
241 "(Var a = Var b) = (a = b)" |
242 by (lifting rvar_inject) |
242 by (lifting rvar_inject) |
243 |
243 |
|
244 |
|
245 lemma app_inject: |
|
246 "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
|
247 sorry |
|
248 |
|
249 lemma var_supp1: |
|
250 shows "(supp (Var a)) = ((supp a)::name set)" |
|
251 apply(simp add: supp_def pi_var1 var_inject) |
|
252 done |
|
253 |
|
254 lemma var_supp: |
|
255 shows "(supp (Var a)) = {a::name}" |
|
256 using var_supp1 |
|
257 apply(simp add: supp_atm) |
|
258 done |
|
259 |
|
260 lemma app_supp: |
|
261 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
|
262 apply(simp only: supp_def pi_app app_inject) |
|
263 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
264 done |
|
265 |
|
266 lemma lam_supp: |
|
267 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
|
268 apply(simp add: supp_def pi_lam) |
|
269 sorry |
|
270 |
244 lemma lam_induct: |
271 lemma lam_induct: |
245 "\<lbrakk>\<And>name. P (Var name); |
272 "\<lbrakk>\<And>name. P (Var name); |
246 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
273 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
247 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
274 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
248 \<Longrightarrow> P lam" |
275 \<Longrightarrow> P lam" |
249 by (lifting rlam.induct) |
276 by (lifting rlam.induct) |
250 |
277 |
251 instance lam::pt_name |
278 instance lam::pt_name |
252 apply(default) |
279 apply(default) |
253 sorry |
280 apply(induct_tac x rule: lam_induct) |
|
281 apply(simp add: pi_var1) |
|
282 apply(simp add: pi_app) |
|
283 apply(simp add: pi_lam) |
|
284 apply(induct_tac x rule: lam_induct) |
|
285 apply(simp add: pi_var1 pt_name2) |
|
286 apply(simp add: pi_app) |
|
287 apply(simp add: pi_lam pt_name2) |
|
288 apply(induct_tac x rule: lam_induct) |
|
289 apply(simp add: pi_var1 pt_name3) |
|
290 apply(simp add: pi_app) |
|
291 apply(simp add: pi_lam pt_name3) |
|
292 done |
254 |
293 |
255 instance lam::fs_name |
294 instance lam::fs_name |
256 apply(default) |
295 apply(default) |
|
296 apply(induct_tac x rule: lam_induct) |
|
297 apply(simp add: var_supp) |
|
298 apply(simp add: app_supp) |
257 sorry |
299 sorry |
258 |
300 |
259 lemma fresh_lam: |
301 lemma fresh_lam: |
260 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
302 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
261 sorry |
303 apply(simp add: fresh_def) |
|
304 apply(simp add: lam_supp abs_supp) |
|
305 apply(auto) |
|
306 done |
262 |
307 |
263 lemma lam_induct_strong: |
308 lemma lam_induct_strong: |
264 fixes a::"'a::fs_name" |
309 fixes a::"'a::fs_name" |
265 assumes a1: "\<And>name b. P b (Var name)" |
310 assumes a1: "\<And>name b. P b (Var name)" |
266 and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |
311 and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |