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 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> \<Longrightarrow> P lam" |
248 by (lifting rlam.induct) |
248 by (lifting rlam.induct) |
|
249 |
|
250 lemma lam_induct_strong_pre: |
|
251 "\<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); |
|
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" |
|
254 sorry |
|
255 |
|
256 lemma lam_induct_strong: |
|
257 "\<lbrakk>\<And>name. P (Var name); |
|
258 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
|
259 \<And>name lam. P lam \<Longrightarrow> name \<sharp> lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam" |
|
260 sorry |
|
261 |
249 |
262 |
250 lemma var_supp: |
263 lemma var_supp: |
251 shows "supp (Var a) = ((supp a)::name set)" |
264 shows "supp (Var a) = ((supp a)::name set)" |
252 apply(simp add: supp_def) |
265 apply(simp add: supp_def) |
253 apply(simp add: pi_var2) |
266 apply(simp add: pi_var2) |