242 by (lifting rvar_inject) |
242 by (lifting rvar_inject) |
243 |
243 |
244 lemma lam_induct: |
244 lemma lam_induct: |
245 "\<lbrakk>\<And>name. P (Var name); |
245 "\<lbrakk>\<And>name. P (Var name); |
246 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
246 \<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> \<Longrightarrow> P lam" |
247 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
|
248 \<Longrightarrow> P lam" |
248 by (lifting rlam.induct) |
249 by (lifting rlam.induct) |
249 |
250 |
250 lemma lam_induct_strong_pre: |
251 instance lam::pt_name |
251 "\<lbrakk>\<And>name b. P b (Var name); |
252 apply(default) |
|
253 sorry |
|
254 |
|
255 instance lam::fs_name |
|
256 apply(default) |
|
257 sorry |
|
258 |
|
259 lemma lam_induct_strong: |
|
260 fixes a::"'a::fs_name" |
|
261 shows |
|
262 "\<lbrakk>\<And>name b. P b (Var name); |
252 \<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2); |
263 \<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2); |
253 \<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> (c \<bullet> lam)\<rbrakk> \<Longrightarrow> P b (Lam name lam)\<rbrakk> \<Longrightarrow> P a lam" |
264 \<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)\<rbrakk> |
254 sorry |
265 \<Longrightarrow> P a lam" |
255 |
266 proof - |
256 lemma lam_induct_strong: |
267 have "\<And>(pi::name prm). P a (pi \<bullet> lam)" |
257 "\<lbrakk>\<And>name. P (Var name); |
268 proof (induct lam rule: lam_induct) |
258 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
269 case (1 name pi) |
259 \<And>name lam. P lam \<Longrightarrow> name \<sharp> lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam" |
270 show "P a (pi \<bullet> Var name)" |
260 sorry |
271 apply - |
|
272 sorry |
|
273 next |
|
274 case (2 lam1 lam2 pi) |
|
275 show "P a (pi \<bullet> App lam1 lam2)" sorry |
|
276 next |
|
277 case (3 name lam pi) |
|
278 show "P a (pi \<bullet> Lam name lam)" sorry |
|
279 qed |
|
280 then have "P a (([]::name prm) \<bullet> lam)" by blast |
|
281 then show "P a lam" by simp |
|
282 qed |
261 |
283 |
262 |
284 |
263 lemma var_supp: |
285 lemma var_supp: |
264 shows "supp (Var a) = ((supp a)::name set)" |
286 shows "supp (Var a) = ((supp a)::name set)" |
265 apply(simp add: supp_def) |
287 apply(simp add: supp_def) |