301 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
301 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} |
302 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
302 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
303 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
303 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
304 prefer 2 |
304 prefer 2 |
305 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
305 ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} |
306 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
307 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
|
308 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
|
309 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
|
310 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) |
|
311 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
312 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
313 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} |
|
314 apply (tactic {* simp_tac (HOL_ss addsimps reps_same) 1 *}) |
|
315 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
|
316 ML_prf {* |
306 ML_prf {* |
317 val rrr1 = ref @{cterm "0"} |
307 fun make_inst lhs t = |
318 val rrr2 = ref @{cterm "0"} |
308 let |
319 val rrrt = ref @{thm refl} |
309 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
|
310 val _ $ (Abs (_, _, g)) = t; |
|
311 fun mk_abs i t = |
|
312 if incr_boundvars i u aconv t then Bound i |
|
313 else (case t of |
|
314 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
315 | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t') |
|
316 | Bound j => if i = j then error "make_inst" else t |
|
317 | _ => t); |
|
318 in (f, Abs ("x", T, mk_abs 0 g)) end; |
320 *} |
319 *} |
321 |
320 |
322 ML_prf {* |
321 ML_prf {* |
323 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
322 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
324 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
323 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
336 val gc = Drule.strip_imp_concl (cprop_of lpi); |
335 val gc = Drule.strip_imp_concl (cprop_of lpi); |
337 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
336 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
338 val te = @{thm eq_reflection} OF [t] |
337 val te = @{thm eq_reflection} OF [t] |
339 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
338 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
340 val tl = Thm.lhs_of ts; |
339 val tl = Thm.lhs_of ts; |
341 val _ = rrrt := ts; |
340 (* val _ = rrrt := ts; |
342 val _ = rrr1 := ctrm; |
341 val _ = rrr1 := ctrm; |
343 val _ = rrr2 := tl; |
342 val _ = rrr2 := tl;*) |
344 (* val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); |
343 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
345 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
344 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
346 val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
345 (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
347 in |
346 in |
348 Conv.all_conv ctrm |
347 (* Conv.all_conv ctrm*) |
349 (* Conv.rewr_conv ti ctrm *) |
348 Conv.rewr_conv ti ctrm |
350 end |
349 end |
351 (* TODO: We can add a proper error message... *) |
350 (* TODO: We can add a proper error message... *) |
352 handle Bind => Conv.all_conv ctrm |
351 handle Bind => Conv.all_conv ctrm |
353 |
352 |
354 *} |
353 *} |
372 (Conv.params_conv ~1 (fn ctxt => |
371 (Conv.params_conv ~1 (fn ctxt => |
373 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
372 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
374 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
373 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
375 *} |
374 *} |
376 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
375 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
377 ML_prf {* !rrr1 *} |
376 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
378 ML_prf {* val rrr1' = @{cterm "((ABS_KIND ---> ABS_KIND ---> Fun.id) ---> Fun.id) |
377 ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} |
379 (\<lambda>P1\<Colon>kind \<Rightarrow> kind \<Rightarrow> bool. |
378 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} |
380 All (((ABS_TY ---> ABS_TY ---> Fun.id) ---> Fun.id) |
379 ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} |
381 (\<lambda>P2\<Colon>ty \<Rightarrow> ty \<Rightarrow> bool. |
380 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) |
382 \<forall>(a\<Colon>TRM \<Rightarrow> TRM \<Rightarrow> bool) (b\<Colon>KIND) (c\<Colon>KIND) (d\<Colon>TY) (e\<Colon>TY) (f\<Colon>TRM) g\<Colon>TRM. |
381 thm FORALL_PRS[symmetric] |
383 (REP_KIND ---> REP_KIND ---> Fun.id) P1 TYP TYP \<longrightarrow> |
|
384 (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow> |
|
385 (\<forall>x\<Colon>KIND. |
|
386 (REP_KIND ---> REP_KIND ---> Fun.id) P1 x x \<longrightarrow> |
|
387 (\<forall>xa\<Colon>name. (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a xa x) (KPI a xa x)))) \<longrightarrow> |
|
388 (\<forall>a\<Colon>TY. (REP_TY ---> REP_TY ---> Fun.id) P2 a a \<longrightarrow> |
|
389 (\<forall>(x\<Colon>name) (x'\<Colon>name) xa\<Colon>KIND. |
|
390 (REP_KIND ---> REP_KIND ---> Fun.id) P1 ([(x, x')] \<bullet> xa) ([(x, x')] \<bullet> xa) \<longrightarrow> |
|
391 x \<notin> FV_ty a \<longrightarrow> |
|
392 x \<notin> FV_kind xa - {x'} \<longrightarrow> |
|
393 (REP_KIND ---> REP_KIND ---> Fun.id) P1 (KPI a x ([(x, x')] \<bullet> xa)) (KPI a x' xa))) \<longrightarrow> |
|
394 (b = c \<longrightarrow> (REP_KIND ---> REP_KIND ---> Fun.id) P1 c c) \<and> |
|
395 (d = e \<longrightarrow> (REP_TY ---> REP_TY ---> Fun.id) P2 e e) \<and> (f = g \<longrightarrow> a g g))))"} *} |
|
396 ML_prf {* (!rrrt); rrr1'; (!rrr1) *} |
|
397 |
|
398 ML_prf {* |
382 ML_prf {* |
399 fun make_inst lhs t = |
383 fun allex_prs_tac lthy quot = |
400 let |
384 (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
401 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
385 THEN' (quotient_tac quot); |
402 val _ $ (Abs (_, _, g)) = t; |
386 *} |
403 fun mk_abs i t = |
387 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
404 if incr_boundvars i u aconv t then Bound i |
388 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} |
405 else (case t of |
389 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} |
406 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
390 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
407 | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t') |
391 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
408 | Bound j => if i = j then error "make_inst" else t |
392 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
409 | _ => t); |
393 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
410 in (f, Abs ("x", T, mk_abs 0 g)) end; |
394 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
411 *} |
395 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
412 |
396 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
413 ML_prf {* cterm_of @{theory} (snd (make_inst (term_of (!rrr2)) (term_of (!rrr1)))) *} |
397 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
414 ML_prf {* val betaeta = Conv.fconv_rule Drule.beta_eta_conversion *} |
398 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) |
415 ML_prf {* val rr = betaeta (Drule.instantiate' [] [SOME it] (!rrrt)) *} |
399 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) |
416 ML_prf {* (term_of (Thm.lhs_of rr)) aconv (term_of (!rrr1)) *} |
400 apply (rule refl) |
417 ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (rrr1')) *} |
401 |
418 ML_prf {* matching_prs @{theory} (term_of (!rrr2)) (term_of (!rrr1)) *} |
402 |
419 |
403 |
420 apply (tactic {* clean_tac @{context} defs aps 1 *}) |
404 |
421 ML_prf {* *} |
405 |
422 print_quotients |
406 print_quotients |
423 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*}) |
407 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*}) |
424 |
408 |
425 |
409 |
426 ML {* val consts = lookup_quot_consts defs *} |
410 ML {* val consts = lookup_quot_consts defs *} |