equal
deleted
inserted
replaced
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" |
73 |
|
74 |
|
75 |
73 |
76 |
74 |
77 (* should be automatic with new version of eqvt-machinery *) |
75 (* should be automatic with new version of eqvt-machinery *) |
78 lemma alpha_eqvt: |
76 lemma alpha_eqvt: |
79 fixes pi::"name prm" |
77 fixes pi::"name prm" |
251 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
249 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
252 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
250 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
253 \<Longrightarrow> P lam" |
251 \<Longrightarrow> P lam" |
254 by (lifting rlam.induct) |
252 by (lifting rlam.induct) |
255 |
253 |
|
254 ML {* show_all_types := true *} |
|
255 |
256 lemma perm_lam [simp]: |
256 lemma perm_lam [simp]: |
257 fixes pi::"'a prm" |
257 fixes pi::"'a prm" |
258 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
258 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
259 and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
259 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)" |
260 and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)" |
261 apply(lifting perm_rlam.simps) |
261 apply(lifting perm_rlam.simps) |
|
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 *} |
262 done |
266 done |
263 |
267 |
264 instance lam::pt_name |
268 instance lam::pt_name |
265 apply(default) |
269 apply(default) |
266 apply(induct_tac [!] x rule: lam_induct) |
270 apply(induct_tac [!] x rule: lam_induct) |