187 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
187 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
188 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
188 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
189 @{thms ho_all_prs ho_ex_prs} *} |
189 @{thms ho_all_prs ho_ex_prs} *} |
190 |
190 |
191 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
191 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
192 |
192 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
193 ML {* val pi_var = lift_thm_lam @{context} @{thm pi_var_com} *} |
193 ML {* val consts = lookup_quot_consts defs *} |
|
194 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
|
195 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
|
196 |
|
197 lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
|
198 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
|
199 done |
|
200 |
194 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *} |
201 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *} |
|
202 lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)" |
|
203 apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *}) |
|
204 done |
195 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *} |
205 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *} |
|
206 lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)" |
|
207 apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *}) |
|
208 done |
196 |
209 |
197 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *} |
210 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *} |
|
211 lemma "\<forall>a. fv (Var (a\<Colon>name)) = {a}" |
|
212 apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) |
|
213 done |
198 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *} |
214 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *} |
|
215 lemma "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa" |
|
216 (*apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})*) |
|
217 sorry |
199 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
218 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} |
|
219 lemma "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}" |
|
220 (*apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})*) |
|
221 sorry |
200 |
222 |
201 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
223 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
|
224 lemma "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b" |
|
225 apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *}) |
|
226 done |
202 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
227 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} |
|
228 lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
|
229 apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) |
|
230 done |
203 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
231 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
204 |
232 lemma "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa" |
205 thm a2 |
233 (*apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})*) |
206 ML {* val t_a = atomize_thm @{thm a2} *} |
234 sorry |
207 ML {* val t_r = regularize t_a @{typ rlam} @{term alpha} @{thm alpha_EQUIV} @{thm alpha_refl} @{context} *} |
|
208 |
235 |
209 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
236 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} |
|
237 lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. \<lbrakk>x = Var a; xa = Var b; a = b\<rbrakk> \<Longrightarrow> P\<Colon>bool; |
|
238 \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = App x xb; xa = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
|
239 \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. \<lbrakk>x = Lam a x; xa = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
|
240 \<Longrightarrow> P" |
|
241 (* apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) *) |
|
242 sorry |
210 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
243 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} |
211 |
244 lemma "\<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); |
212 ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *} |
245 \<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); |
|
246 \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. |
|
247 \<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> |
|
248 \<Longrightarrow> qxb qx qxa" |
|
249 (* apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) *) |
|
250 sorry |
|
251 |
|
252 lemma "(Var a = Var b) = (a = b)" |
|
253 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
|
254 done |
213 |
255 |
214 local_setup {* |
256 local_setup {* |
215 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
257 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
216 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
258 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
217 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
259 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |