# HG changeset patch # User Christian Urban # Date 1259535577 -3600 # Node ID 9cb45d02252411e85c0d61418456dbab54aadd1f # Parent cc0b9cb367cd6c5b91dad784b1d7c687b56aa1f9 tried to improve the inj_repabs_trm function but left the new part commented out diff -r cc0b9cb367cd -r 9cb45d022524 FSet.thy --- a/FSet.thy Sun Nov 29 19:48:55 2009 +0100 +++ b/FSet.thy Sun Nov 29 23:59:37 2009 +0100 @@ -303,8 +303,20 @@ ML {* val consts = lookup_quot_consts defs *} ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} +thm m1 + lemma "IN x EMPTY = False" -by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) +apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) +ML_prf {* + val rtrm = @{term "\x. IN x EMPTY = False"} + val qtrm = @{term "\x. x memb [] = False"} + val aps = find_aps rtrm qtrm +*} +unfolding IN_def EMPTY_def +apply(tactic {* clean_tac @{context} [quot] defs aps 1*}) +done lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) diff -r cc0b9cb367cd -r 9cb45d022524 IntEx.thy --- a/IntEx.thy Sun Nov 29 19:48:55 2009 +0100 +++ b/IntEx.thy Sun Nov 29 23:59:37 2009 +0100 @@ -153,6 +153,9 @@ ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) +apply(simp add: id_def) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) @@ -189,6 +192,7 @@ lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(simp) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} @@ -227,6 +231,7 @@ lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(simp) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} diff -r cc0b9cb367cd -r 9cb45d022524 LFex.thy --- a/LFex.thy Sun Nov 29 19:48:55 2009 +0100 +++ b/LFex.thy Sun Nov 29 23:59:37 2009 +0100 @@ -221,64 +221,47 @@ FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} *} -lemma "\P1 TYP TYP; \A A' K K' x. \(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\ \ P1 (KPI A x K) (KPI A' x K'); - \A A' K x x' K'. - \(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \ K'); P1 K ([(x, x')] \ K'); x \ FV_ty A'; x \ FV_kind K' - {x'}\ - \ P1 (KPI A x K) (KPI A' x' K'); - \i j. i = j \ P2 (TCONST i) (TCONST j); - \A A' M M'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P2 (TAPP A M) (TAPP A' M'); - \A A' B B' x. \(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\ \ P2 (TPI A x B) (TPI A' x B'); - \A A' B x x' B'. - \(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \ B'); P2 B ([(x, x')] \ B'); x \ FV_ty B'; x \ FV_ty B' - {x'}\ - \ P2 (TPI A x B) (TPI A' x' B'); - \i j m. i = j \ P3 (CONS i) (m (CONS j)); \x y m. x = y \ P3 (VAR x) (m (VAR y)); - \M m M' N N'. \(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\ \ P3 (APP M N) (APP M' N'); - \A A' M M' x. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P3 (LAM A x M) (LAM A' x M'); - \A A' M x x' M' B'. - \(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \ M'); P3 M ([(x, x')] \ M'); x \ FV_ty B'; x \ FV_trm M' - {x'}\ - \ P3 (LAM A x M) (LAM A' x' M')\ -\ ((x1 :: KIND) = x2 \ P1 x1 x2) \ - ((x3 ::TY) = x4 \ P2 x3 x4) \ ((x5 :: TRM) = x6 \ P3 x5 x6)" +lemma + assumes a0: + "P1 TYP TYP" + and a1: + "\A A' K K' x. \(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\ + \ P1 (KPI A x K) (KPI A' x K')" + and a2: + "\A A' K K' x x'. \(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \ K'); P1 K ([(x, x')] \ K'); + x \ FV_ty A'; x \ FV_kind K' - {x'}\ \ P1 (KPI A x K) (KPI A' x' K')" + and a3: + "\i j. i = j \ P2 (TCONST i) (TCONST j)" + and a4: + "\A A' M M'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P2 (TAPP A M) (TAPP A' M')" + and a5: + "\A A' B B' x. \(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\ \ P2 (TPI A x B) (TPI A' x B')" + and a6: + "\A A' B x x' B'. \(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \ B'); P2 B ([(x, x')] \ B'); + x \ FV_ty B'; x \ FV_ty B' - {x'}\ \ P2 (TPI A x B) (TPI A' x' B')" + and a7: + "\i j m. i = j \ P3 (CONS i) (m (CONS j))" + and a8: + "\x y m. x = y \ P3 (VAR x) (m (VAR y))" + and a9: + "\M m M' N N'. \(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\ \ P3 (APP M N) (APP M' N')" + and a10: + "\A A' M M' x. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P3 (LAM A x M) (LAM A' x M')" + and a11: + "\A A' M x x' M' B'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \ M'); P3 M ([(x, x')] \ M'); + x \ FV_ty B'; x \ FV_trm M' - {x'}\ \ P3 (LAM A x M) (LAM A' x' M')" + shows "((x1 :: KIND) = x2 \ P1 x1 x2) \ + ((x3 ::TY) = x4 \ P2 x3 x4) \ + ((x5 :: TRM) = x6 \ P3 x5 x6)" +using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 +apply - apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *} apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) -prefer 2 +(* injecting *) ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} -(*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *) -apply (tactic {* lambda_prs_tac @{context} quot 1 *}) -ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} -ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} -ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} -ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} -apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) -apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) -ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} -ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) -apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) 1 *}) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) -apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) ML_prf {* val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs} @@ -474,6 +457,41 @@ apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) +(* cleaning *) +ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *} +(*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *) +apply (tactic {* lambda_prs_tac @{context} quot 1 *}) +ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} +ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *} +ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *} +ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} +apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *}) +apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) +ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *} +ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *} +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext) +apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl) done print_quotients diff -r cc0b9cb367cd -r 9cb45d022524 QuotMain.thy --- a/QuotMain.thy Sun Nov 29 19:48:55 2009 +0100 +++ b/QuotMain.thy Sun Nov 29 23:59:37 2009 +0100 @@ -343,64 +343,6 @@ end *} -section {* Infrastructure for special quotient identity *} - -definition - "qid TYPE('a) TYPE('b) x \ x" - -ML {* -fun get_typ1 (Type ("itself", [T])) = T -fun get_typ2 (Const ("TYPE", T)) = get_typ1 T -fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) = - (get_typ2 ty1, get_typ2 ty2) - -fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true - | is_qid _ = false - - -fun mk_itself ty = Type ("itself", [ty]) -fun mk_TYPE ty = Const ("TYPE", mk_itself ty) -fun mk_qid (rty, qty, trm) = - Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) - $ mk_TYPE rty $ mk_TYPE qty $ trm -*} - -ML {* -fun insertion_aux rtrm qtrm = - case (rtrm, qtrm) of - (Abs (x, ty, t), Abs (x', ty', t')) => - let - val (y, s) = Term.dest_abs (x, ty, t) - val (_, s') = Term.dest_abs (x', ty', t') - val yvar = Free (y, ty) - val result = Term.lambda_name (y, yvar) (insertion_aux s s') - in - if ty = ty' - then result - else mk_qid (ty, ty', result) - end - | (t1 $ t2, t1' $ t2') => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - val subtrm1 = insertion_aux t1 t1' - val subtrm2 = insertion_aux t2 t2' - in - if rty = qty - then subtrm1 $ subtrm2 - else mk_qid (rty, qty, subtrm1 $ subtrm2) - end - | (Free (_, ty), Free (_, ty')) => - if ty = ty' - then rtrm - else mk_qid (ty, ty', rtrm) - | (Const (s, ty), Const (s', ty')) => - if s = s' andalso ty = ty' - then rtrm - else mk_qid (ty, ty', rtrm) - | (_, _) => raise (LIFT_MATCH "insertion") -*} - section {* Regularization *} (* @@ -794,10 +736,38 @@ else mk_repabs lthy (rty, qty) result end | _ => - (* FIXME / TODO: this is a case that needs to be looked at *) - (* - variables get a rep-abs insde and outside an application *) - (* - constants only get a rep-abs on the outside of the application *) - (* - applications get a rep-abs insde and outside an application *) + (**************************************************) + (* new + let + val (rhead, rargs) = strip_comb rtrm + val (qhead, qargs) = strip_comb qtrm + val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) + in + case (rhead, qhead, length rargs') of + (Const (_, T), Const (_, T'), 0) => + if T = T' + then rhead + else mk_repabs lthy (T, T') rhead + | (Free (_, T), Free (_, T'), 0) => + if T = T' + then rhead + else mk_repabs lthy (T, T') rhead + | (Const (_, T), Const (_, T'), _) => (* FIXME/TODO: check this case exactly*) + if rty = qty + then list_comb (rhead, rargs') + else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) + | (Free (x, T), Free (x', T'), _) => + if T = T' + then list_comb (rhead, rargs') + else list_comb (mk_repabs lthy (T, T') rhead, rargs') + | (Abs _, Abs _, _ ) => + list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') + | _ => raise (LIFT_MATCH "injection") + end + *) + + (*************************************************) + (* old *) let val (rhead, rargs) = strip_comb rtrm val (qhead, qargs) = strip_comb qtrm @@ -821,6 +791,7 @@ mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) | _ => raise (LIFT_MATCH "injection") end + (**) end *} diff -r cc0b9cb367cd -r 9cb45d022524 QuotMainNew.thy --- a/QuotMainNew.thy Sun Nov 29 19:48:55 2009 +0100 +++ b/QuotMainNew.thy Sun Nov 29 23:59:37 2009 +0100 @@ -1,4 +1,4 @@ -theory QuotMain +theory QuotMainNew imports QuotScript QuotList Prove uses ("quotient_info.ML") ("quotient.ML") @@ -259,90 +259,6 @@ *} -section {* Infrastructure about definitions *} - -(* Does the same as 'subst' in a given theorem *) -ML {* -fun eqsubst_thm ctxt thms thm = - let - val goalstate = Goal.init (Thm.cprop_of thm) - val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of - NONE => error "eqsubst_thm" - | SOME th => cprem_of th 1 - val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 - val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); - val cgoal = cterm_of (ProofContext.theory_of ctxt) goal - val rt = Goal.prove_internal [] cgoal (fn _ => tac); - in - @{thm equal_elim_rule1} OF [rt, thm] - end -*} - -(* expects atomized definitions *) -ML {* -fun add_lower_defs_aux lthy thm = - let - val e1 = @{thm fun_cong} OF [thm]; - val f = eqsubst_thm lthy @{thms fun_map.simps} e1; - val g = simp_ids f - in - (simp_ids thm) :: (add_lower_defs_aux lthy g) - end - handle _ => [simp_ids thm] -*} - -ML {* -fun add_lower_defs lthy def = - let - val def_pre_sym = symmetric def - val def_atom = atomize_thm def_pre_sym - val defs_all = add_lower_defs_aux lthy def_atom - in - map Thm.varifyT defs_all - end -*} - -section {* Infrastructure for collecting theorems for starting the lifting *} - -ML {* -fun lookup_quot_data lthy qty = - let - val qty_name = fst (dest_Type qty) - val SOME quotdata = quotdata_lookup lthy qty_name - (* cu: Changed the lookup\not sure whether this works *) - (* TODO: Should no longer be needed *) - val rty = Logic.unvarifyT (#rtyp quotdata) - val rel = #rel quotdata - val rel_eqv = #equiv_thm quotdata - val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] - in - (rty, rel, rel_refl, rel_eqv) - end -*} - -ML {* -fun lookup_quot_thms lthy qty_name = - let - val thy = ProofContext.theory_of lthy; - val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") - val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") - val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") - val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name) - in - (trans2, reps_same, absrep, quot) - end -*} - -ML {* -fun lookup_quot_consts defs = - let - fun dest_term (a $ b) = (a, b); - val def_terms = map (snd o Logic.dest_equals o concl_of) defs; - in - map (fst o dest_Const o snd o dest_term) def_terms - end -*} - section {* Infrastructure for special quotient identity *} definition @@ -366,41 +282,87 @@ *} ML {* -fun insertion_aux rtrm qtrm = +fun insertion_aux (rtrm, qtrm) = case (rtrm, qtrm) of (Abs (x, ty, t), Abs (x', ty', t')) => let val (y, s) = Term.dest_abs (x, ty, t) val (_, s') = Term.dest_abs (x', ty', t') val yvar = Free (y, ty) - val result = Term.lambda_name (y, yvar) (insertion_aux s s') + val result = Term.lambda_name (y, yvar) (insertion_aux (s, s')) in if ty = ty' then result else mk_qid (ty, ty', result) end - | (t1 $ t2, t1' $ t2') => + | (_ $ _, _ $ _) => let val rty = fastype_of rtrm - val qty = fastype_of qtrm - val subtrm1 = insertion_aux t1 t1' - val subtrm2 = insertion_aux t2 t2' + val qty = fastype_of qtrm + val (rhead, rargs) = strip_comb rtrm + val (qhead, qargs) = strip_comb qtrm + val rargs' = map insertion_aux (rargs ~~ qargs) + val rhead' = insertion_aux (rhead, qhead) + val result = list_comb (rhead', rargs') in if rty = qty - then subtrm1 $ subtrm2 - else mk_qid (rty, qty, subtrm1 $ subtrm2) + then result + else mk_qid (rty, qty, result) end | (Free (_, ty), Free (_, ty')) => if ty = ty' then rtrm else mk_qid (ty, ty', rtrm) | (Const (s, ty), Const (s', ty')) => - if s = s' andalso ty = ty' + if s = s' then rtrm else mk_qid (ty, ty', rtrm) | (_, _) => raise (LIFT_MATCH "insertion") *} +ML {* +fun insertion ctxt rtrm qtrm = + Syntax.check_term ctxt (insertion_aux (rtrm, qtrm)) +*} + + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient my_int = "nat \ nat" / intrel + apply(unfold EQUIV_def) + apply(auto simp add: mem_def expand_fun_eq) + done + +fun + my_plus :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "my_plus (x, y) (u, v) = (x + u, y + v)" + +quotient_def + PLUS::"my_int \ my_int \ my_int" +where + "PLUS \ my_plus" + +thm PLUS_def + +ML {* MetaSimplifier.rewrite_term *} + +ML {* +let + val rtrm = @{term "\a b. my_plus a b \ my_plus b a"} + val qtrm = @{term "\a b. PLUS a b = PLUS b a"} + val ctxt = @{context} +in + insertion ctxt rtrm qtrm + (*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*) + |> Syntax.string_of_term ctxt + |> writeln +end +*} + section {* Regularization *} (* @@ -554,188 +516,6 @@ *) -(* FIXME: they should be in in the new Isabelle *) -lemma [mono]: - "(\x. P x \ Q x) \ (Ex P) \ (Ex Q)" -by blast - -lemma [mono]: "P \ Q \ \Q \ \P" -by auto - -(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) -ML {* -fun equiv_tac rel_eqvs = - REPEAT_ALL_NEW (FIRST' - [resolve_tac rel_eqvs, - rtac @{thm IDENTITY_EQUIV}, - rtac @{thm LIST_EQUIV}]) -*} - -ML {* -fun ball_reg_eqv_simproc rel_eqvs ss redex = - let - val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt - in - case redex of - (ogl as ((Const (@{const_name "Ball"}, _)) $ - ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => - (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; - val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); - val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); -(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) - in - SOME thm - end - handle _ => NONE - ) - | _ => NONE - end -*} - -ML {* -fun bex_reg_eqv_simproc rel_eqvs ss redex = - let - val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt - in - case redex of - (ogl as ((Const (@{const_name "Bex"}, _)) $ - ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => - (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; - val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); - val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); -(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) - in - SOME thm - end - handle _ => NONE - ) - | _ => NONE - end -*} - -ML {* -fun prep_trm thy (x, (T, t)) = - (cterm_of thy (Var (x, T)), cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) -*} - -ML {* -fun matching_prs thy pat trm = -let - val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ - val tenv = Vartab.dest (Envir.term_env env) - val tyenv = Vartab.dest (Envir.type_env env) -in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) -end -*} - -ML {* -fun ball_reg_eqv_range_simproc rel_eqvs ss redex = - let - val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt - in - case redex of - (ogl as ((Const (@{const_name "Ball"}, _)) $ - ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => - (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; - val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val _ = tracing (Syntax.string_of_term ctxt glc); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); - val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); - val R1c = cterm_of thy R1; - val thmi = Drule.instantiate' [] [SOME R1c] thm; -(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) - val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl - val _ = tracing "AAA"; - val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); - val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); - in - SOME thm2 - end - handle _ => NONE - - ) - | _ => NONE - end -*} - -ML {* -fun bex_reg_eqv_range_simproc rel_eqvs ss redex = - let - val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt - in - case redex of - (ogl as ((Const (@{const_name "Bex"}, _)) $ - ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => - (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; - val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val _ = tracing (Syntax.string_of_term ctxt glc); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); - val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); - val R1c = cterm_of thy R1; - val thmi = Drule.instantiate' [] [SOME R1c] thm; -(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) - val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl - val _ = tracing "AAA"; - val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); - val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); - in - SOME thm2 - end - handle _ => NONE - - ) - | _ => NONE - end -*} - -lemma eq_imp_rel: "EQUIV R \ a = b \ R a b" -by (simp add: EQUIV_REFL) - -ML {* -fun regularize_tac ctxt rel_eqvs = - let - val pat1 = [@{term "Ball (Respects R) P"}]; - val pat2 = [@{term "Bex (Respects R) P"}]; - val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; - val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; - val thy = ProofContext.theory_of ctxt - val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) - val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) - val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) - val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) - val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] - (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs - in - ObjectLogic.full_atomize_tac THEN' - simp_tac simp_ctxt THEN' - REPEAT_ALL_NEW (FIRST' [ - rtac @{thm ball_reg_right}, - rtac @{thm bex_reg_left}, - resolve_tac (Inductive.get_monos ctxt), - rtac @{thm ball_all_comm}, - rtac @{thm bex_ex_comm}, - resolve_tac eq_eqvs, - simp_tac simp_ctxt - ]) - end -*} - section {* Injections of REP and ABSes *} (* @@ -824,332 +604,6 @@ end *} -section {* RepAbs Injection Tactic *} - -ML {* -fun stripped_term_of ct = - ct |> term_of |> HOLogic.dest_Trueprop -*} - -ML {* -fun instantiate_tac thm = - Subgoal.FOCUS (fn {concl, ...} => - let - val pat = Drule.strip_imp_concl (cprop_of thm) - val insts = Thm.match (pat, concl) - in - rtac (Drule.instantiate insts thm) 1 - end - handle _ => no_tac) -*} - -ML {* -fun quotient_tac quot_thms = - REPEAT_ALL_NEW (FIRST' - [rtac @{thm FUN_QUOTIENT}, - resolve_tac quot_thms, - rtac @{thm IDENTITY_QUOTIENT}, - (* For functional identity quotients, (op = ---> op =) *) - (* TODO: think about the other way around, if we need to shorten the relation *) - CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))]) -*} - -lemma FUN_REL_I: - assumes a: "\x y. R1 x y \ R2 (f x) (g y)" - shows "(R1 ===> R2) f g" -using a by (simp add: FUN_REL.simps) - -ML {* -val lambda_res_tac = - Subgoal.FOCUS (fn {concl, ...} => - case (stripped_term_of concl) of - (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1 - | _ => no_tac) -*} - -ML {* -val weak_lambda_res_tac = - Subgoal.FOCUS (fn {concl, ...} => - case (stripped_term_of concl) of - (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1 - | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1 - | _ => no_tac) -*} - -ML {* -val ball_rsp_tac = - Subgoal.FOCUS (fn {concl, ...} => - case (stripped_term_of concl) of - (_ $ (Const (@{const_name Ball}, _) $ _) - $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1 - |_ => no_tac) -*} - -ML {* -val bex_rsp_tac = - Subgoal.FOCUS (fn {concl, context = ctxt, ...} => - case (stripped_term_of concl) of - (_ $ (Const (@{const_name Bex}, _) $ _) - $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1 - | _ => no_tac) -*} - -ML {* (* Legacy *) -fun needs_lift (rty as Type (rty_s, _)) ty = - case ty of - Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) - | _ => false - -*} - -ML {* -fun APPLY_RSP_TAC rty = - Subgoal.FOCUS (fn {concl, ...} => - case (stripped_term_of concl) of - (_ $ (f $ _) $ (_ $ _)) => - let - val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); - val insts = Thm.match (pat, concl) - in - if needs_lift rty (fastype_of f) - then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 - else no_tac - end - | _ => no_tac) -*} - -ML {* -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) -*} - -(* -To prove that the regularised theorem implies the abs/rep injected, -we try: - - 1) theorems 'trans2' from the appropriate QUOT_TYPE - 2) remove lambdas from both sides: lambda_res_tac - 3) remove Ball/Bex from the right hand side - 4) use user-supplied RSP theorems - 5) remove rep_abs from the right side - 6) reflexivity of equality - 7) split applications of lifted type (apply_rsp) - 8) split applications of non-lifted type (cong_tac) - 9) apply extentionality - A) reflexivity of the relation - B) assumption - (Lambdas under respects may have left us some assumptions) - C) proving obvious higher order equalities by simplifying fun_rel - (not sure if it is still needed?) - D) unfolding lambda on one side - E) simplifying (= ===> =) for simpler respectfulness - -*) - -ML {* -fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = - (FIRST' [ - (* "cong" rule of the of the relation / transitivity*) - (* (op =) (R a b) (R c d) ----> \R a c; R b d\ *) - NDT ctxt "1" (resolve_tac trans2), - - (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) - NDT ctxt "2" (lambda_res_tac ctxt), - - (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) - NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), - - (* (R1 ===> R2) (Ball\) (Ball\) ----> \R1 x y\ \ R2 (Ball\x) (Ball\y) *) - NDT ctxt "4" (ball_rsp_tac ctxt), - - (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) - NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), - - (* (R1 ===> R2) (Bex\) (Bex\) ----> \R1 x y\ \ R2 (Bex\x) (Bex\y) *) - NDT ctxt "6" (bex_rsp_tac ctxt), - - (* respectfulness of constants *) - NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), - - (* reflexivity of operators arising from Cong_tac *) - NDT ctxt "8" (rtac @{thm refl}), - - (* R (\) (Rep (Abs \)) ----> R (\) (\) *) - (* observe ---> *) - NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt - THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), - - (* R (t $ \) (t' $ \) ----> APPLY_RSP provided type of t needs lifting *) - NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' - (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), - - (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) - (* merge with previous tactic *) - NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), - - (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) - NDT ctxt "C" (rtac @{thm ext}), - - (* reflexivity of the basic relations *) - (* R \ \ *) - NDT ctxt "D" (resolve_tac rel_refl), - - (* resolving with R x y assumptions *) - NDT ctxt "E" (atac), - - (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) - - (* (R1 ===> R2) (\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) - (* (R1 ===> R2) (\x\) (\) ----> \R1 x y\ \ R2 (\x) (\y) *) - (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*) - - (* (op =) ===> (op =) \ (op =), needed in order to apply respectfulness theorems *) - (* global simplification *) - NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) -*} - -ML {* -fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = - REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) -*} - - -section {* Cleaning of the theorem *} - -ML {* -fun applic_prs lthy absrep (rty, qty) = - let - fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm; - fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm; - val (raty, rgty) = Term.strip_type rty; - val (qaty, qgty) = Term.strip_type qty; - val vs = map (fn _ => "x") qaty; - val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; - val f = Free (fname, qaty ---> qgty); - val args = map Free (vfs ~~ qaty); - val rhs = list_comb(f, args); - val largs = map2 mk_rep (raty ~~ qaty) args; - val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); - val llhs = Syntax.check_term lthy lhs; - val eq = Logic.mk_equals (llhs, rhs); - val ceq = cterm_of (ProofContext.theory_of lthy') eq; - val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep); - val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) - val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; - in - singleton (ProofContext.export lthy' lthy) t_id - end -*} - -ML {* -fun find_aps_all rtm qtm = - case (rtm, qtm) of - (Abs(_, T1, s1), Abs(_, T2, s2)) => - find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2)) - | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) => - let - val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2) - in - if T1 = T2 then sub else (T1, T2) :: sub - end - | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2) - | _ => []; - -fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) -*} - -ML {* -fun allex_prs_tac lthy quot = - (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) - THEN' (quotient_tac quot) -*} - -(* Rewrites the term with LAMBDA_PRS thm. - -Replaces: (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) - with: f - -It proves the QUOTIENT assumptions by calling quotient_tac - *) -ML {* -fun make_inst lhs t = - let - val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; - val _ $ (Abs (_, _, g)) = t; - fun mk_abs i t = - if incr_boundvars i u aconv t then Bound i - else (case t of - t1 $ t2 => mk_abs i t1 $ mk_abs i t2 - | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t') - | Bound j => if i = j then error "make_inst" else t - | _ => t); - in (f, Abs ("x", T, mk_abs 0 g)) end; - -fun lambda_prs_conv1 ctxt quot_thms ctrm = - case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => - let - val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); - val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); - val thy = ProofContext.theory_of ctxt; - val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] - val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; - val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] - val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; - val tac = - (compose_tac (false, lpi, 2)) THEN_ALL_NEW - (quotient_tac quot_thms); - val gc = Drule.strip_imp_concl (cprop_of lpi); - val t = Goal.prove_internal [] gc (fn _ => tac 1) - val te = @{thm eq_reflection} OF [t] - val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te - val tl = Thm.lhs_of ts; - val (insp, inst) = make_inst (term_of tl) (term_of ctrm); - val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; -(* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) - in - Conv.rewr_conv ti ctrm - end -*} - -(* quot stands for the QUOTIENT theorems: *) -(* could be potentially all of them *) -ML {* -fun lambda_prs_conv ctxt quot ctrm = - case (term_of ctrm) of - (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) => - (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) - then_conv (lambda_prs_conv1 ctxt quot)) ctrm - | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm - | _ => Conv.all_conv ctrm -*} - -ML {* -fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => - CONVERSION - (Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv - Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) -*} - -ML {* -fun clean_tac lthy quot defs aps = - let - val lower = flat (map (add_lower_defs lthy) defs) - val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower - val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot - val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot - val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same - val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower) - val aps_thms = map (applic_prs lthy absrep) aps - in - EVERY' [lambda_prs_tac lthy quot, - TRY o simp_tac simp_ctxt, - TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), - TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), - TRY o rtac refl] - end -*} - section {* Genralisation of free variables in a goal *} ML {* @@ -1260,11 +714,7 @@ val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv in EVERY1 - [rtac rule, - RANGE [rtac rthm', - regularize_tac lthy rel_eqv, - all_inj_repabs_tac lthy rty quot rel_refl trans2, - clean_tac lthy quot defs aps]] + [rtac rule, rtac rthm'] end) lthy *}