# HG changeset patch # User Cezary Kaliszyk # Date 1308527413 -32400 # Node ID b58073719b0686807a9a5c05356e4f6022df2ff7 # Parent b9a16d627bfde9a71aabb8d375f2244841762669 Update Quotient/TODO and remove some attic code diff -r b9a16d627bfd -r b58073719b06 Attic/FIXME-TODO --- a/Attic/FIXME-TODO Sun Jun 19 13:14:37 2011 +0900 +++ b/Attic/FIXME-TODO Mon Jun 20 08:50:13 2011 +0900 @@ -8,22 +8,14 @@ Higher Priority =============== - -- Also, in the interest of making nicer generated documentation, you - might want to change all your "section" headings in Quotient.thy to - "subsection", and add a "header" statement to the top of the file. - Otherwise, each "section" gets its own chapter in the generated pdf, - when the rest of HOL has one chapter per theory file (the chapter - title comes from the "header" statement). - - If the constant definition gives the wrong definition term, one gets a cryptic message about absrep_fun -- Handle theorems that include Ball/Bex. For this, would - it help if we introduced separate Bex and Ball constants - for quotienting? +- Handle theorems that include Ball/Bex. + Workaround: Unfolding Ball_def/Bex_def is enough to lift, + in some cases regularization is harder though. -- The user should be able to give quotient_respects and +- The user should be able to give quotient_respects and preserves theorems in a more natural form. Lower Priority @@ -32,8 +24,6 @@ - the quot_lifted attribute should rename variables so they do not suggest that they talk about raw terms. -- accept partial equivalence relations - - think about what happens if things go wrong (like theorem cannot be lifted) / proper diagnostic messages for the user @@ -52,7 +42,7 @@ [QuotList, QuotOption, QuotPair...] could be automatically proven? -- Examples: Finite multiset. +- Examples: Finite multiset, Dlist. - The current syntax of the quotient_definition is diff -r b9a16d627bfd -r b58073719b06 Attic/Unused.thy --- a/Attic/Unused.thy Sun Jun 19 13:14:37 2011 +0900 +++ b/Attic/Unused.thy Mon Jun 20 08:50:13 2011 +0900 @@ -1,164 +1,11 @@ (*notation ( output) "prop" ("#_" [1000] 1000) *) notation ( output) "Trueprop" ("#_" [1000] 1000) -function(sequential) - akind :: "kind \ kind \ bool" ("_ \ki _" [100, 100] 100) -and aty :: "ty \ ty \ bool" ("_ \ty _" [100, 100] 100) -and atrm :: "trm \ trm \ bool" ("_ \tr _" [100, 100] 100) -where - a1: "(Type) \ki (Type) = True" -| a2: "(KPi A x K) \ki (KPi A' x' K') = (A \ty A' \ (\pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \ (rfv_kind K - {atom x})\* pi \ (pi \ K) \ki K' \ (pi \ x) = x')))" -| "_ \ki _ = False" -| a3: "(TConst i) \ty (TConst j) = (i = j)" -| a4: "(TApp A M) \ty (TApp A' M') = (A \ty A' \ M \tr M')" -| a5: "(TPi A x B) \ty (TPi A' x' B') = ((A \ty A') \ (\pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \ (rfv_ty B - {atom x})\* pi \ (pi \ B) \ty B' \ (pi \ x) = x'))" -| "_ \ty _ = False" -| a6: "(Const i) \tr (Const j) = (i = j)" -| a7: "(Var x) \tr (Var y) = (x = y)" -| a8: "(App M N) \tr (App M' N') = (M \tr M' \ N \tr N')" -| a9: "(Lam A x M) \tr (Lam A' x' M') = (A \ty A' \ (\pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \ (rfv_trm M - {atom x})\* pi \ (pi \ M) \tr M' \ (pi \ x) = x'))" -| "_ \tr _ = False" -apply (pat_completeness) -apply simp_all -done -termination -by (size_change) - - - -lemma regularize_to_injection: - shows "(QUOT_TRUE l \ y) \ (l = r) \ y" - by(auto simp add: QUOT_TRUE_def) - syntax "Bex1_rel" :: "id \ ('a \ 'a \ bool) \ ('a \ bool) \ bool" ("(3\!!_\_./ _)" [0, 0, 10] 10) translations "\!!x\A. P" == "Bex1_rel A (%x. P)" - -(* Atomize infrastructure *) -(* FIXME/TODO: is this really needed? *) -(* -lemma atomize_eqv: - shows "(Trueprop A \ Trueprop B) \ (A \ B)" -proof - assume "A \ B" - then show "Trueprop A \ Trueprop B" by unfold -next - assume *: "Trueprop A \ Trueprop B" - have "A = B" - proof (cases A) - case True - have "A" by fact - then show "A = B" using * by simp - next - case False - have "\A" by fact - then show "A = B" using * by auto - qed - then show "A \ B" by (rule eq_reflection) -qed -*) - - -ML {* - fun dest_cbinop t = - let - val (t2, rhs) = Thm.dest_comb t; - val (bop, lhs) = Thm.dest_comb t2; - in - (bop, (lhs, rhs)) - end -*} - -ML {* - fun dest_ceq t = - let - val (bop, pair) = dest_cbinop t; - val (bop_s, _) = Term.dest_Const (Thm.term_of bop); - in - if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) - end -*} - -ML {* - fun split_binop_conv t = - let - val (lhs, rhs) = dest_ceq t; - val (bop, _) = dest_cbinop lhs; - val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; - val [cmT, crT] = Thm.dest_ctyp cr2; - in - Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2} - end -*} - - -ML {* - fun split_arg_conv t = - let - val (lhs, rhs) = dest_ceq t; - val (lop, larg) = Thm.dest_comb lhs; - val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; - in - Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong} - end -*} - -ML {* - fun split_binop_tac n thm = - let - val concl = Thm.cprem_of thm n; - val (_, cconcl) = Thm.dest_comb concl; - val rewr = split_binop_conv cconcl; - in - rtac rewr n thm - end - handle CTERM _ => Seq.empty -*} - - -ML {* - fun split_arg_tac n thm = - let - val concl = Thm.cprem_of thm n; - val (_, cconcl) = Thm.dest_comb concl; - val rewr = split_arg_conv cconcl; - in - rtac rewr n thm - end - handle CTERM _ => Seq.empty -*} - - -lemma trueprop_cong: - shows "(a \ b) \ (Trueprop a \ Trueprop b)" - by auto - -lemma list_induct_hol4: - fixes P :: "'a list \ bool" - assumes a: "((P []) \ (\t. (P t) \ (\h. (P (h # t)))))" - shows "\l. (P l)" - using a - apply (rule_tac allI) - apply (induct_tac "l") - apply (simp) - apply (metis) - done - -ML {* -val no_vars = Thm.rule_attribute (fn context => fn th => - let - val ctxt = Variable.set_body false (Context.proof_of context); - val ((_, [th']), _) = Variable.import true [th] ctxt; - in th' end); -*} - -(*lemma equality_twice: - "a = c \ b = d \ (a = b \ c = d)" -by auto*) - - (*interpretation code *) (*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; diff -r b9a16d627bfd -r b58073719b06 Attic/UnusedQuotMain.thy --- a/Attic/UnusedQuotMain.thy Sun Jun 19 13:14:37 2011 +0900 +++ b/Attic/UnusedQuotMain.thy Mon Jun 20 08:50:13 2011 +0900 @@ -1,687 +1,3 @@ -(* Code for getting the goal *) -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 ())))) *} - - -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 -*} - - - -ML {* -fun repeat_eqsubst_thm ctxt thms thm = - repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) - handle _ => thm -*} - - -ML {* -fun eqsubst_prop ctxt thms t = - let - val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t) - val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of - NONE => error "eqsubst_prop" - | SOME th => cprem_of th 1 - in term_of a' end -*} - -ML {* - fun repeat_eqsubst_prop ctxt thms t = - repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t) - handle _ => t -*} - - -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) -*} +(* Could go in the programming tutorial *) - -(* 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 atomize_goal thy gl = - let - val vars = map Free (Term.add_frees gl []); - val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all; - fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm; - val glv = fold lambda_all vars gl - val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv)) - val glf = Type.legacy_freeze gla - in - if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf - end -*} - - -ML {* atomize_goal @{theory} @{term "x memb [] = False"} *} -ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *} - - -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 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 simp_ids_trm trm = - trm |> - MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} - |> cprop_of |> Thm.dest_equals |> snd - -*} - -(* Unused part of the locale *) - -lemma R_trans: - assumes ab: "R a b" - and bc: "R b c" - shows "R a c" -proof - - have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp - moreover have ab: "R a b" by fact - moreover have bc: "R b c" by fact - ultimately show "R a c" unfolding transp_def by blast -qed - -lemma R_sym: - assumes ab: "R a b" - shows "R b a" -proof - - have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp - then show "R b a" using ab unfolding symp_def by blast -qed - -lemma R_trans2: - assumes ac: "R a c" - and bd: "R b d" - shows "R a b = R c d" -using ac bd -by (blast intro: R_trans R_sym) - -lemma REPS_same: - shows "R (REP a) (REP b) \ (a = b)" -proof - - have "R (REP a) (REP b) = (a = b)" - proof - assume as: "R (REP a) (REP b)" - from rep_prop - obtain x y - where eqs: "Rep a = R x" "Rep b = R y" by blast - from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp - then have "R x (Eps (R y))" using lem9 by simp - then have "R (Eps (R y)) x" using R_sym by blast - then have "R y x" using lem9 by simp - then have "R x y" using R_sym by blast - then have "ABS x = ABS y" using thm11 by simp - then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp - then show "a = b" using rep_inverse by simp - next - assume ab: "a = b" - have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp - then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto - qed - then show "R (REP a) (REP b) \ (a = b)" by simp -qed - - - - +ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}