177 @{thms ho_all_prs ho_ex_prs} *} |
177 @{thms ho_all_prs ho_ex_prs} *} |
178 |
178 |
179 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
179 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
180 ML {* val consts = lookup_quot_consts defs *} |
180 ML {* val consts = lookup_quot_consts defs *} |
181 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
181 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
182 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
182 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} |
183 |
183 |
184 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
184 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
185 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
185 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
186 done |
186 done |
187 |
187 |
222 \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
222 \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
223 \<Longrightarrow> P" |
223 \<Longrightarrow> P" |
224 apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) |
224 apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) |
225 done |
225 done |
226 |
226 |
227 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
|
228 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
229 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b); |
227 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b); |
230 \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
228 \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
231 \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. |
229 \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. |
232 \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk> |
230 \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk> |
233 \<Longrightarrow> qxb qx qxa" |
231 \<Longrightarrow> qxb qx qxa" |
234 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) |
232 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) |
235 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
|
236 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
237 done |
233 done |
238 |
234 |
239 lemma var_inject: "(Var a = Var b) = (a = b)" |
235 lemma var_inject: "(Var a = Var b) = (a = b)" |
240 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
236 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
241 done |
237 done |