# HG changeset patch # User Cezary Kaliszyk # Date 1259145702 -3600 # Node ID 57bde65f6eb23c0bb750339190ff2c1394c465c1 # Parent 86fba2c4eeef345fa7b36f3412d846d812a6078c Removed unused things from QuotMain. diff -r 86fba2c4eeef -r 57bde65f6eb2 FSet.thy --- a/FSet.thy Wed Nov 25 10:52:21 2009 +0100 +++ b/FSet.thy Wed Nov 25 11:41:42 2009 +0100 @@ -176,8 +176,6 @@ term fmap thm fmap_def -ML {* prop_of @{thm fmap_def} *} - ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} lemma memb_rsp: @@ -303,8 +301,6 @@ @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} @ @{thms ho_all_prs ho_ex_prs} *} -ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} -ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} ML {* val consts = lookup_quot_consts defs *} @@ -378,9 +374,6 @@ ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} - -ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} -ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} @@ -397,9 +390,6 @@ ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *} ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} - - -ML {* map (lift_thm_fset @{context}) @{thms list.cases(2)} *} lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) @@ -417,100 +407,14 @@ done - -(* Construction site starts here *) - +ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -ML {* val consts = lookup_quot_consts defs *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} - -ML {* val t_a = atomize_thm @{thm list_induct_part} *} -(* prove {* build_regularize_goal t_a rty rel @{context} *} - ML_prf {* fun tac ctxt = FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - //comented out rtac @{thm equality_twice}, // - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]; *} - apply (atomize(full)) - apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) - done *) -ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} -ML {* - val rt = build_repabs_term @{context} t_r consts rty qty - val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); -*} -prove {* Syntax.check_term @{context} rg *} -ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -apply(atomize(full)) -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -done -ML {* -val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms -*} - -ML {* val abs = findabs rty (prop_of (t_a)) *} -ML {* val aps = findaps rty (prop_of (t_a)) *} -ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} -ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} -ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} -ML {* t_t *} -ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} -ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} -ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_t *} -ML app_prs_thms -ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *} -ML lam_prs_thms -ML {* val t_id = simp_ids @{context} t_l *} -thm INSERT_def -ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} -ML allthms -thm FORALL_PRS -ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} -ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} -ML {* ObjectLogic.rulify t_s *} - -ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l"} *} -ML {* val gla = atomize_goal @{theory} gl *} - -prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) gla *} - -ML_prf {* fun tac ctxt = FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - (*rtac @{thm equality_twice},*) - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]; *} - - apply (atomize(full)) - apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) - done - -ML {* val t_r = @{thm t_r} OF [t_a] *} - -ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, gla) *} -ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *} -prove t_t: {* term_of si *} -ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -apply(atomize(full)) +(* Construction site starts here *) +lemma "P (x :: 'a list) (EMPTY :: 'a fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) +apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) apply (rule FUN_QUOTIENT) apply (rule FUN_QUOTIENT) @@ -579,13 +483,7 @@ apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) +apply (tactic {* clean_tac @{context} quot defs reps_same 1 *}) done -thm t_t -ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *} -ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} -ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} -ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} - end diff -r 86fba2c4eeef -r 57bde65f6eb2 IntEx.thy --- a/IntEx.thy Wed Nov 25 10:52:21 2009 +0100 +++ b/IntEx.thy Wed Nov 25 11:41:42 2009 +0100 @@ -141,10 +141,6 @@ ML {* val consts = lookup_quot_consts defs *} ML {* -fun lift_thm_my_int lthy t = - lift_thm lthy qty ty_name rsp_thms defs t -fun lift_thm_g_my_int lthy t g = - lift_thm_goal lthy qty ty_name rsp_thms defs t g fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} @@ -164,6 +160,21 @@ by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *}) +lemma ho_tst: "foldl my_plus x [] = x" +apply simp +done + +lemma "foldl PLUS x [] = x" +apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) +prefer 3 +apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) +sorry + +(* + FIXME: All below is your construction code; mostly commented out as it + does not work. +*) + ML {* mk_REGULARIZE_goal @{context} @{term "\i j k. my_plus (my_plus i j) k \ my_plus i (my_plus j k)"} @@ -172,13 +183,6 @@ |> writeln *} - -ML {* -val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} -val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" -*} - - lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) @@ -188,7 +192,7 @@ (* -does not work. + ML {* fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (REPEAT1 o FIRST1) @@ -209,14 +213,6 @@ DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] *} -*) - -ML {* -val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} -val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" -val consts = lookup_quot_consts defs -*} - ML {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) @@ -238,66 +234,6 @@ |> writeln *} - -lemma ho_tst: "foldl my_plus x [] = x" -apply simp -done - -text {* Below is the construction site code used if things do not work *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *} -(* ML {* val consts = [@{const_name my_plus}] *}*) -ML {* val consts = lookup_quot_consts defs *} -ML {* val t_a = atomize_thm @{thm ho_tst} *} - -(* -prove t_r: {* build_regularize_goal t_a rty rel @{context} *} -ML_prf {* fun tac ctxt = - (ObjectLogic.full_atomize_tac) THEN' - REPEAT_ALL_NEW (FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - (*rtac @{thm equality_twice},*) - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]);*} -apply (atomize(full)) -apply (tactic {* tac @{context} 1 *}) -apply (auto) -done -ML {* val t_r = @{thm t_r} OF [t_a] *}*) -ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} -ML {* - val rt = build_repabs_term @{context} t_r consts rty qty - val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); -*} +*) - -prove t_t: rg -apply(atomize(full)) -ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_int @{context}) 1 *}) -done -ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t},t_r] *} -ML {* val abs = findabs rty (prop_of t_a) *} -ML {* val aps = findaps rty (prop_of t_a); *} -ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} - -(*ML {* val t_t = repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms *}*) -ML findallex -ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a) *} -ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} -ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} -ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} -ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} -ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} -ML {* ObjectLogic.rulify t_r *} -ML {* @{term "Trueprop"} *} - diff -r 86fba2c4eeef -r 57bde65f6eb2 LamEx.thy --- a/LamEx.thy Wed Nov 25 10:52:21 2009 +0100 +++ b/LamEx.thy Wed Nov 25 11:41:42 2009 +0100 @@ -176,7 +176,6 @@ ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *} -ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val consts = lookup_quot_consts defs *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} @@ -268,101 +267,6 @@ (* Construction Site code *) -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val consts = lookup_quot_consts defs *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} - -ML {* val t_a = atomize_thm @{thm alpha.cases} *} -(* prove {* build_regularize_goal t_a rty rel @{context} *} -ML_prf {* fun tac ctxt = - (FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]); - *} - apply (tactic {* tac @{context} 1 *}) *) -ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} - -ML {* - val rt = build_repabs_term @{context} t_r consts rty qty - val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); -*} -prove rg -apply(atomize(full)) -(*ML_prf {* -fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = - (FIRST' [ - rtac trans_thm, - LAMBDA_RES_TAC ctxt, - res_forall_rsp_tac ctxt, - res_exists_rsp_tac ctxt, - ( - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) - THEN_ALL_NEW (fn _ => no_tac) - ), - (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), - rtac refl, - (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), - Cong_Tac.cong_tac @{thm cong}, - rtac @{thm ext}, - rtac reflex_thm, - atac, - ( - (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) - THEN_ALL_NEW (fn _ => no_tac) - ), - WEAK_LAMBDA_RES_TAC ctxt - ]); -*}*) -ML_prf {* - fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms -*} -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) - - - - - - -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) - - -ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} -ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} -ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} -ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} -ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS} ) alls *} -ML {* val exthms = map (make_allex_prs_thm @{context} quot @{thm EXISTS_PRS} ) exs *} -ML {* val t_a = MetaSimplifier.rewrite_rule allthms t_t *} -ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} -ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} -ML {* val t_l = repeat_eqsubst_thm @{context} (simp_lam_prs_thms) t_a *} -ML {* val t_l1 = repeat_eqsubst_thm @{context} simp_app_prs_thms t_l *} -ML {* val defs_sym = add_lower_defs @{context} defs; *} -ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} -ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l1 *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} -ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} -ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} -ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} -ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *} -ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} - -(*local_setup {* - Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd -*}*) - -thm alpha_induct -thm alpha.induct - @@ -384,6 +288,9 @@ declare [[map noption = (option_map, option_rel)]] +lemma "option_map id = id" +sorry + lemma OPT_QUOTIENT: assumes q: "QUOTIENT R Abs Rep" shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)" diff -r 86fba2c4eeef -r 57bde65f6eb2 QuotMain.thy --- a/QuotMain.thy Wed Nov 25 10:52:21 2009 +0100 +++ b/QuotMain.thy Wed Nov 25 11:41:42 2009 +0100 @@ -227,35 +227,6 @@ *) -text {* tyRel takes a type and builds a relation that a quantifier over this - type needs to respect. *} -ML {* -fun tyRel ty rty rel lthy = - if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) - then rel - else (case ty of - Type (s, tys) => - let - val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; - val ty_out = ty --> ty --> @{typ bool}; - val tys_out = tys_rel ---> ty_out; - in - (case (maps_lookup (ProofContext.theory_of lthy) s) of - SOME (info) => list_comb (Const (#relfun info, tys_out), - map (fn ty => tyRel ty rty rel lthy) tys) - | NONE => HOLogic.eq_const ty - ) - end - | _ => HOLogic.eq_const ty) -*} - -(* -ML {* cterm_of @{theory} - (tyRel @{typ "'a \ 'a list \ 't \ 't"} (Logic.varifyT @{typ "'a list"}) - @{term "f::('a list \ 'a list \ bool)"} @{context}) -*} -*) - definition Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" where @@ -273,94 +244,6 @@ *} -ML {* -fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) -fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) -fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) -fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) -*} - -(* applies f to the subterm of an abstractions, otherwise to the given term *) -ML {* -fun apply_subt f trm = - case trm of - Abs (x, T, t) => - let - val (x', t') = Term.dest_abs (x, T, t) - in - Term.absfree (x', T, f t') - end - | _ => f trm -*} - -(* FIXME: if there are more than one quotient, then you have to look up the relation *) -ML {* -fun my_reg lthy rel rty trm = - case trm of - Abs (x, T, t) => - if (needs_lift rty T) then - let - val rrel = tyRel T rty rel lthy - in - (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm) - end - else - Abs(x, T, (apply_subt (my_reg lthy rel rty) t)) - | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) => - let - val ty1 = domain_type ty - val ty2 = domain_type ty1 - val rrel = tyRel T rty rel lthy - in - if (needs_lift rty T) then - (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) - else - Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t - end - | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) => - let - val ty1 = domain_type ty - val ty2 = domain_type ty1 - val rrel = tyRel T rty rel lthy - in - if (needs_lift rty T) then - (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) - else - Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t - end - | Const (@{const_name "op ="}, ty) $ t => - if needs_lift rty (fastype_of t) then - (tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *) - else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) - | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) - | _ => trm -*} - -(* For polymorphic types we need to find the type of the Relation term. *) -(* TODO: we assume that the relation is a Constant. Is this always true? *) -ML {* -fun my_reg_inst lthy rel rty trm = - case rel of - Const (n, _) => Syntax.check_term lthy - (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) -*} - -(* -ML {* - val r = Free ("R", dummyT); - val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\(x::'b list). P x"}); - val t2 = Syntax.check_term @{context} t; - cterm_of @{theory} t2 -*} -*) - -text {* Assumes that the given theorem is atomized *} -ML {* - fun build_regularize_goal thm rty rel lthy = - Logic.mk_implies - ((prop_of thm), - (my_reg_inst lthy rel rty (prop_of thm))) -*} lemma universal_twice: assumes *: "\x. (P x \ Q x)" @@ -373,32 +256,6 @@ shows "(a \ b) \ (c \ d)" using a b by auto -ML {* -fun regularize thm rty rel rel_eqv rel_refl lthy = - let - val goal = build_regularize_goal thm rty rel lthy; - fun tac ctxt = - (ObjectLogic.full_atomize_tac) THEN' - REPEAT_ALL_NEW (FIRST' [ - rtac rel_refl, - atac, - rtac @{thm universal_twice}, - (rtac @{thm impI} THEN' atac), - rtac @{thm implication_twice}, - EqSubst.eqsubst_tac ctxt [0] - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])], - (* For a = b \ a \ b *) - (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), - (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]); - val cthm = Goal.prove lthy [] [] goal - (fn {context, ...} => tac context 1); - in - cthm OF [thm] - end -*} - section {* RepAbs injection *} (* @@ -473,16 +330,6 @@ handle TYPE _ => ty (* for dest_Type *) *} -(*consts Rl :: "'a list \ 'a list \ bool" -axioms Rl_eq: "EQUIV Rl" - -quotient ql = "'a list" / "Rl" - by (rule Rl_eq) -ML {* - ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \ (nat \ nat) list"}); - ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \ nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \ (nat \ nat) list"}) -*} -*) ML {* fun find_matching_types rty ty = @@ -535,19 +382,6 @@ | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) | _ => error ("no type variables allowed")) end - -(* returns all subterms where two types differ *) -fun diff (T, S) Ds = - case (T, S) of - (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds - | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds - | (Type (a, Ts), Type (b, Us)) => - if a = b then diffs (Ts, Us) Ds else (T, S)::Ds - | _ => (T, S)::Ds -and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) - | diffs ([], []) Ds = Ds - | diffs _ _ = error "Unequal length of type arguments" - *} ML {* @@ -609,73 +443,6 @@ ML {* symmetric (eq_reflection OF @{thms id_def}) *} ML {* -fun build_repabs_term lthy thm consts rty qty = - let - (* TODO: The rty and qty stored in the quotient_info should - be varified, so this will soon not be needed *) - val rty = Logic.varifyT rty; - val qty = Logic.varifyT qty; - - fun mk_abs tm = - let - val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end - fun mk_repabs tm = - let - val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end - - fun is_lifted_const (Const (x, _)) = member (op =) consts x - | is_lifted_const _ = false; - - fun build_aux lthy tm = - case tm of - Abs (a as (_, vty, _)) => - let - val (vs, t) = Term.dest_abs a; - val v = Free(vs, vty); - val t' = lambda v (build_aux lthy t) - in - if (not (needs_lift rty (fastype_of tm))) then t' - else mk_repabs ( - if not (needs_lift rty vty) then t' - else - let - val v' = mk_repabs v; - (* TODO: I believe 'beta' is not needed any more *) - val t1 = (* Envir.beta_norm *) (t' $ v') - in - lambda v t1 - end) - end - | x => - case Term.strip_comb tm of - (Const(@{const_name Respects}, _), _) => tm - | (opp, tms0) => - let - val tms = map (build_aux lthy) tms0 - val ty = fastype_of tm - in - if (is_lifted_const opp andalso needs_lift rty ty) then - mk_repabs (list_comb (opp, tms)) - else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then - mk_repabs (list_comb (opp, tms)) - else if tms = [] then opp - else list_comb(opp, tms) - end - in - repeat_eqsubst_prop lthy @{thms id_def_sym} - (build_aux lthy (Thm.prop_of thm)) - end -*} - -text {* Builds provable goals for regularized theorems *} -ML {* -fun build_repabs_goal ctxt thm cons rty qty = - Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) -*} - -ML {* fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => let val pat = Drule.strip_imp_concl (cprop_of thm) @@ -801,19 +568,6 @@ ]) *} -ML {* -fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = - let - val rt = build_repabs_term lthy thm consts rty qty; - val rg = Logic.mk_equals ((Thm.prop_of thm), rt); - fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' - (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); - val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); - in - @{thm Pure.equal_elim_rule1} OF [cthm, thm] - end -*} - section {* Cleaning the goal *} @@ -854,22 +608,6 @@ end *} -(* TODO: Check if it behaves properly with varifyed rty *) -ML {* -fun findabs_all rty tm = - case tm of - Abs(_, T, b) => - let - val b' = subst_bound ((Free ("x", T)), b); - val tys = findabs_all rty b' - val ty = fastype_of tm - in if needs_lift rty ty then (ty :: tys) else tys - end - | f $ a => (findabs_all rty f) @ (findabs_all rty a) - | _ => []; -fun findabs rty tm = distinct (op =) (findabs_all rty tm) -*} - ML {* fun findaps_all rty tm = case tm of @@ -882,83 +620,6 @@ fun findaps rty tm = distinct (op =) (findaps_all rty tm) *} -(* Currently useful only for LAMBDA_PRS *) -ML {* -fun make_simp_prs_thm lthy quot_thm thm typ = - let - val (_, [lty, rty]) = dest_Type typ; - val thy = ProofContext.theory_of lthy; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [SOME lcty, NONE, SOME rcty]; - val lpi = Drule.instantiate' inst [] thm; - val tac = - (compose_tac (false, lpi, 2)) THEN_ALL_NEW - (quotient_tac quot_thm); - val gc = Drule.strip_imp_concl (cprop_of lpi); - val t = Goal.prove_internal [] gc (fn _ => tac 1) - in - MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t - end -*} - -ML {* -fun findallex_all rty qty tm = - case tm of - Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => - let - val (tya, tye) = findallex_all rty qty s - in if needs_lift rty T then - ((T :: tya), tye) - else (tya, tye) end - | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => - let - val (tya, tye) = findallex_all rty qty s - in if needs_lift rty T then - (tya, (T :: tye)) - else (tya, tye) end - | Abs(_, T, b) => - findallex_all rty qty (subst_bound ((Free ("x", T)), b)) - | f $ a => - let - val (a1, e1) = findallex_all rty qty f; - val (a2, e2) = findallex_all rty qty a; - in (a1 @ a2, e1 @ e2) end - | _ => ([], []); -*} - -ML {* -fun findallex lthy rty qty tm = - let - val (a, e) = findallex_all rty qty tm; - val (ad, ed) = (map domain_type a, map domain_type e); - val (au, eu) = (distinct (op =) ad, distinct (op =) ed); - val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) - in - (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) - end -*} - -ML {* -fun make_allex_prs_thm lthy quot_thm thm typ = - let - val (_, [lty, rty]) = dest_Type typ; - val thy = ProofContext.theory_of lthy; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [NONE, SOME lcty]; - val lpi = Drule.instantiate' inst [] thm; - val tac = - (compose_tac (false, lpi, 1)) THEN_ALL_NEW - (quotient_tac quot_thm); - val gc = Drule.strip_imp_concl (cprop_of lpi); - val t = Goal.prove_internal [] gc (fn _ => tac 1) - val t_noid = MetaSimplifier.rewrite_rule - [@{thm eq_reflection} OF @{thms id_apply}] t; - val t_sym = @{thm "HOL.sym"} OF [t_noid]; - val t_eq = @{thm "eq_reflection"} OF [t_sym] - in - t_eq - end -*} ML {* fun applic_prs lthy rty qty absrep ty = @@ -1035,76 +696,6 @@ *} -ML {* -fun lift_thm lthy qty qty_name rsp_thms defs rthm = -let - val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) - - val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; - val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; - val consts = lookup_quot_consts defs; - val t_a = atomize_thm rthm; - - val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) - - val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; - - val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) - - val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; - - val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) - - val (alls, exs) = findallex lthy rty qty (prop_of t_a); - val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls - val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs - val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t - - val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) - - val abs = findabs rty (prop_of t_a); - val aps = findaps rty (prop_of t_a); - val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; - val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; - val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; - - val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) - - val defs_sym = flat (map (add_lower_defs lthy) defs); - val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; - val t_id = simp_ids lthy t_l; - - val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) - - val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; - - val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) - - val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; - - val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) - - val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; - - val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) - - val t_rv = ObjectLogic.rulify t_r - - val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv)) -in - Thm.varifyT t_rv -end -*} - -ML {* -fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = - let - val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; - val (_, lthy2) = note (name, lifted_thm) lthy; - in - lthy2 - end -*} (******************************************) (******************************************) @@ -1461,70 +1052,6 @@ *} ML {* -fun regularize_goal lthy thm rel_eqv rel_refl qtrm = - let - val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; - fun tac lthy = regularize_tac lthy rel_eqv rel_refl; - val cthm = Goal.prove lthy [] [] reg_trm - (fn {context, ...} => tac context 1); - in - cthm OF [thm] - end -*} - -ML {* -fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = - let - val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); - fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' - (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); - val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); - in - @{thm Pure.equal_elim_rule1} OF [cthm, thm] - end -*} - -ML {* -fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = -let - val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; - val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; - val t_a = atomize_thm rthm; - val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; - val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; - val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; - val (alls, exs) = findallex lthy rty qty (prop_of t_a); - val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls - val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs - val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t - val abs = findabs rty (prop_of t_a); - val aps = findaps rty (prop_of t_a); - val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; - val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; - val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; - val defs_sym = flat (map (add_lower_defs lthy) defs); - val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; - val t_id = simp_ids lthy t_l; - val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; - val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; - val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; - val t_rv = ObjectLogic.rulify t_r -in - Thm.varifyT t_rv -end -*} - -ML {* -fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = - let - val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; - val (_, lthy2) = note (name, lifted_thm) lthy; - in - lthy2 - end -*} - -ML {* fun inst_spec ctrm = let val cty = ctyp_of_term ctrm diff -r 86fba2c4eeef -r 57bde65f6eb2 UnusedQuotMain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/UnusedQuotMain.thy Wed Nov 25 11:41:42 2009 +0100 @@ -0,0 +1,486 @@ + +text {* tyRel takes a type and builds a relation that a quantifier over this + type needs to respect. *} +ML {* +fun tyRel ty rty rel lthy = + if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) + then rel + else (case ty of + Type (s, tys) => + let + val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; + val ty_out = ty --> ty --> @{typ bool}; + val tys_out = tys_rel ---> ty_out; + in + (case (maps_lookup (ProofContext.theory_of lthy) s) of + SOME (info) => list_comb (Const (#relfun info, tys_out), + map (fn ty => tyRel ty rty rel lthy) tys) + | NONE => HOLogic.eq_const ty + ) + end + | _ => HOLogic.eq_const ty) +*} + +(* +ML {* cterm_of @{theory} + (tyRel @{typ "'a \ 'a list \ 't \ 't"} (Logic.varifyT @{typ "'a list"}) + @{term "f::('a list \ 'a list \ bool)"} @{context}) +*} +*) + + +ML {* +fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) +fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) +fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) +fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) +*} + +(* applies f to the subterm of an abstractions, otherwise to the given term *) +ML {* +fun apply_subt f trm = + case trm of + Abs (x, T, t) => + let + val (x', t') = Term.dest_abs (x, T, t) + in + Term.absfree (x', T, f t') + end + | _ => f trm +*} + + + +(* FIXME: if there are more than one quotient, then you have to look up the relation *) +ML {* +fun my_reg lthy rel rty trm = + case trm of + Abs (x, T, t) => + if (needs_lift rty T) then + let + val rrel = tyRel T rty rel lthy + in + (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm) + end + else + Abs(x, T, (apply_subt (my_reg lthy rel rty) t)) + | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) => + let + val ty1 = domain_type ty + val ty2 = domain_type ty1 + val rrel = tyRel T rty rel lthy + in + if (needs_lift rty T) then + (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) + else + Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t + end + | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) => + let + val ty1 = domain_type ty + val ty2 = domain_type ty1 + val rrel = tyRel T rty rel lthy + in + if (needs_lift rty T) then + (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) + else + Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t + end + | Const (@{const_name "op ="}, ty) $ t => + if needs_lift rty (fastype_of t) then + (tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *) + else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) + | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) + | _ => trm +*} + +(* For polymorphic types we need to find the type of the Relation term. *) +(* TODO: we assume that the relation is a Constant. Is this always true? *) +ML {* +fun my_reg_inst lthy rel rty trm = + case rel of + Const (n, _) => Syntax.check_term lthy + (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) +*} + +(* +ML {* + val r = Free ("R", dummyT); + val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\(x::'b list). P x"}); + val t2 = Syntax.check_term @{context} t; + cterm_of @{theory} t2 +*} +*) + +text {* Assumes that the given theorem is atomized *} +ML {* + fun build_regularize_goal thm rty rel lthy = + Logic.mk_implies + ((prop_of thm), + (my_reg_inst lthy rel rty (prop_of thm))) +*} + +ML {* +fun regularize thm rty rel rel_eqv rel_refl lthy = + let + val goal = build_regularize_goal thm rty rel lthy; + fun tac ctxt = + (ObjectLogic.full_atomize_tac) THEN' + REPEAT_ALL_NEW (FIRST' [ + rtac rel_refl, + atac, + rtac @{thm universal_twice}, + (rtac @{thm impI} THEN' atac), + rtac @{thm implication_twice}, + EqSubst.eqsubst_tac ctxt [0] + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])], + (* For a = b \ a \ b *) + (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + (rtac @{thm RIGHT_RES_FORALL_REGULAR}) + ]); + val cthm = Goal.prove lthy [] [] goal + (fn {context, ...} => tac context 1); + in + cthm OF [thm] + end +*} + +(*consts Rl :: "'a list \ 'a list \ bool" +axioms Rl_eq: "EQUIV Rl" + +quotient ql = "'a list" / "Rl" + by (rule Rl_eq) +ML {* + ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \ (nat \ nat) list"}); + ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \ nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \ (nat \ nat) list"}) +*} +*) + +ML {* +(* returns all subterms where two types differ *) +fun diff (T, S) Ds = + case (T, S) of + (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds + | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds + | (Type (a, Ts), Type (b, Us)) => + if a = b then diffs (Ts, Us) Ds else (T, S)::Ds + | _ => (T, S)::Ds +and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) + | diffs ([], []) Ds = Ds + | diffs _ _ = error "Unequal length of type arguments" + +*} + +ML {* +fun build_repabs_term lthy thm consts rty qty = + let + (* TODO: The rty and qty stored in the quotient_info should + be varified, so this will soon not be needed *) + val rty = Logic.varifyT rty; + val qty = Logic.varifyT qty; + + fun mk_abs tm = + let + val ty = fastype_of tm + in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end + fun mk_repabs tm = + let + val ty = fastype_of tm + in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end + + fun is_lifted_const (Const (x, _)) = member (op =) consts x + | is_lifted_const _ = false; + + fun build_aux lthy tm = + case tm of + Abs (a as (_, vty, _)) => + let + val (vs, t) = Term.dest_abs a; + val v = Free(vs, vty); + val t' = lambda v (build_aux lthy t) + in + if (not (needs_lift rty (fastype_of tm))) then t' + else mk_repabs ( + if not (needs_lift rty vty) then t' + else + let + val v' = mk_repabs v; + (* TODO: I believe 'beta' is not needed any more *) + val t1 = (* Envir.beta_norm *) (t' $ v') + in + lambda v t1 + end) + end + | x => + case Term.strip_comb tm of + (Const(@{const_name Respects}, _), _) => tm + | (opp, tms0) => + let + val tms = map (build_aux lthy) tms0 + val ty = fastype_of tm + in + if (is_lifted_const opp andalso needs_lift rty ty) then + mk_repabs (list_comb (opp, tms)) + else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then + mk_repabs (list_comb (opp, tms)) + else if tms = [] then opp + else list_comb(opp, tms) + end + in + repeat_eqsubst_prop lthy @{thms id_def_sym} + (build_aux lthy (Thm.prop_of thm)) + end +*} + +text {* Builds provable goals for regularized theorems *} +ML {* +fun build_repabs_goal ctxt thm cons rty qty = + Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) +*} + +ML {* +fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = + let + val rt = build_repabs_term lthy thm consts rty qty; + val rg = Logic.mk_equals ((Thm.prop_of thm), rt); + fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' + (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); + val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); + in + @{thm Pure.equal_elim_rule1} OF [cthm, thm] + end +*} + + +(* TODO: Check if it behaves properly with varifyed rty *) +ML {* +fun findabs_all rty tm = + case tm of + Abs(_, T, b) => + let + val b' = subst_bound ((Free ("x", T)), b); + val tys = findabs_all rty b' + val ty = fastype_of tm + in if needs_lift rty ty then (ty :: tys) else tys + end + | f $ a => (findabs_all rty f) @ (findabs_all rty a) + | _ => []; +fun findabs rty tm = distinct (op =) (findabs_all rty tm) +*} + + +(* Currently useful only for LAMBDA_PRS *) +ML {* +fun make_simp_prs_thm lthy quot_thm thm typ = + let + val (_, [lty, rty]) = dest_Type typ; + val thy = ProofContext.theory_of lthy; + val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) + val inst = [SOME lcty, NONE, SOME rcty]; + val lpi = Drule.instantiate' inst [] thm; + val tac = + (compose_tac (false, lpi, 2)) THEN_ALL_NEW + (quotient_tac quot_thm); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + in + MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t + end +*} + +ML {* +fun findallex_all rty qty tm = + case tm of + Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + ((T :: tya), tye) + else (tya, tye) end + | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + (tya, (T :: tye)) + else (tya, tye) end + | Abs(_, T, b) => + findallex_all rty qty (subst_bound ((Free ("x", T)), b)) + | f $ a => + let + val (a1, e1) = findallex_all rty qty f; + val (a2, e2) = findallex_all rty qty a; + in (a1 @ a2, e1 @ e2) end + | _ => ([], []); +*} + +ML {* +fun findallex lthy rty qty tm = + let + val (a, e) = findallex_all rty qty tm; + val (ad, ed) = (map domain_type a, map domain_type e); + val (au, eu) = (distinct (op =) ad, distinct (op =) ed); + val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) + in + (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) + end +*} + +ML {* +fun make_allex_prs_thm lthy quot_thm thm typ = + let + val (_, [lty, rty]) = dest_Type typ; + val thy = ProofContext.theory_of lthy; + val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) + val inst = [NONE, SOME lcty]; + val lpi = Drule.instantiate' inst [] thm; + val tac = + (compose_tac (false, lpi, 1)) THEN_ALL_NEW + (quotient_tac quot_thm); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + val t_noid = MetaSimplifier.rewrite_rule + [@{thm eq_reflection} OF @{thms id_apply}] t; + val t_sym = @{thm "HOL.sym"} OF [t_noid]; + val t_eq = @{thm "eq_reflection"} OF [t_sym] + in + t_eq + end +*} + +ML {* +fun lift_thm lthy qty qty_name rsp_thms defs rthm = +let + val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) + + val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; + val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; + val consts = lookup_quot_consts defs; + val t_a = atomize_thm rthm; + + val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) + + val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; + + val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) + + val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; + + val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) + + val (alls, exs) = findallex lthy rty qty (prop_of t_a); + val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls + val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs + val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) + + val abs = findabs rty (prop_of t_a); + val aps = findaps rty (prop_of t_a); + val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; + val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; + val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) + + val defs_sym = flat (map (add_lower_defs lthy) defs); + val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; + val t_id = simp_ids lthy t_l; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) + + val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) + + val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) + + val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) + + val t_rv = ObjectLogic.rulify t_r + + val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv)) +in + Thm.varifyT t_rv +end +*} + +ML {* +fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = + let + val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; + val (_, lthy2) = note (name, lifted_thm) lthy; + in + lthy2 + end +*} + + +ML {* +fun regularize_goal lthy thm rel_eqv rel_refl qtrm = + let + val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; + fun tac lthy = regularize_tac lthy rel_eqv rel_refl; + val cthm = Goal.prove lthy [] [] reg_trm + (fn {context, ...} => tac context 1); + in + cthm OF [thm] + end +*} + +ML {* +fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = + let + val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); + fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' + (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); + val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); + in + @{thm Pure.equal_elim_rule1} OF [cthm, thm] + end +*} + +ML {* +fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = +let + val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; + val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; + val t_a = atomize_thm rthm; + val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; + val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; + val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; + val (alls, exs) = findallex lthy rty qty (prop_of t_a); + val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls + val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs + val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t + val abs = findabs rty (prop_of t_a); + val aps = findaps rty (prop_of t_a); + val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; + val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; + val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; + val defs_sym = flat (map (add_lower_defs lthy) defs); + val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; + val t_id = simp_ids lthy t_l; + val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; + val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; + val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; + val t_rv = ObjectLogic.rulify t_r +in + Thm.varifyT t_rv +end +*} + +ML {* +fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = + let + val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; + val (_, lthy2) = note (name, lifted_thm) lthy; + in + lthy2 + end +*} +