# HG changeset patch # User Christian Urban # Date 1264533161 -3600 # Node ID 25c4223635f4a4010aad336e154d4ff596d888d8 # Parent fa810f01f7b5e20d40643acb19d1cb8d04eec744 just moved obsolete material into Attic diff -r fa810f01f7b5 -r 25c4223635f4 Attic/Prove.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/Prove.thy Tue Jan 26 20:12:41 2010 +0100 @@ -0,0 +1,28 @@ +theory Prove +imports Plain +begin + +ML {* +val r = Unsynchronized.ref (NONE:(unit -> term) option) +*} + +ML {* +let + fun after_qed thm_name thms lthy = + Local_Theory.note (thm_name, (flat thms)) lthy |> snd + + fun setup_proof (name_spec, (txt, pos)) lthy = + let + val trm = ML_Context.evaluate lthy true ("r", r) txt + in + Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy + end + + val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source +in + OuterSyntax.local_theory_to_proof "prove" "proving a proposition" + OuterKeyword.thy_goal (parser >> setup_proof) +end +*} + +end diff -r fa810f01f7b5 -r 25c4223635f4 Attic/Unused.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/Unused.thy Tue Jan 26 20:12:41 2010 +0100 @@ -0,0 +1,161 @@ +(*notation ( output) "prop" ("#_" [1000] 1000) *) +notation ( output) "Trueprop" ("#_" [1000] 1000) + +lemma regularize_to_injection: + shows "(QUOT_TRUE l \ y) \ (l = r) \ y" + by(auto simp add: QUOT_TRUE_def) + +syntax + "Bexeq" :: "id \ ('a \ 'a \ bool) \ ('a \ bool) \ bool" ("(3\!!_\_./ _)" [0, 0, 10] 10) +translations + "\!!x\A. P" == "Bexeq 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; + val eqn1i = Thm.prop_of (symmetric eqn1pre) + val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5; + val eqn2i = Thm.prop_of (symmetric eqn2pre) + + val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6)); + val exp_term = Morphism.term exp_morphism; + val exp = Morphism.thm exp_morphism; + + val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN + ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) + val mthdt = Method.Basic (fn _ => mthd) + val bymt = Proof.global_terminal_proof (mthdt, NONE) + val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), + Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*) + +(*||> Local_Theory.theory (fn thy => + let + val global_eqns = map exp_term [eqn2i, eqn1i]; + (* Not sure if the following context should not be used *) + val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; + val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; + in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*) diff -r fa810f01f7b5 -r 25c4223635f4 Attic/UnusedQuotMain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/UnusedQuotMain.thy Tue Jan 26 20:12:41 2010 +0100 @@ -0,0 +1,687 @@ +(* 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) +*} + + +(* 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 + + + + diff -r fa810f01f7b5 -r 25c4223635f4 Quot/Prove.thy --- a/Quot/Prove.thy Tue Jan 26 20:07:50 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -theory Prove -imports Plain -begin - -ML {* -val r = Unsynchronized.ref (NONE:(unit -> term) option) -*} - -ML {* -let - fun after_qed thm_name thms lthy = - Local_Theory.note (thm_name, (flat thms)) lthy |> snd - - fun setup_proof (name_spec, (txt, pos)) lthy = - let - val trm = ML_Context.evaluate lthy true ("r", r) txt - in - Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy - end - - val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source -in - OuterSyntax.local_theory_to_proof "prove" "proving a proposition" - OuterKeyword.thy_goal (parser >> setup_proof) -end -*} - -end diff -r fa810f01f7b5 -r 25c4223635f4 Unused.thy --- a/Unused.thy Tue Jan 26 20:07:50 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,161 +0,0 @@ -(*notation ( output) "prop" ("#_" [1000] 1000) *) -notation ( output) "Trueprop" ("#_" [1000] 1000) - -lemma regularize_to_injection: - shows "(QUOT_TRUE l \ y) \ (l = r) \ y" - by(auto simp add: QUOT_TRUE_def) - -syntax - "Bexeq" :: "id \ ('a \ 'a \ bool) \ ('a \ bool) \ bool" ("(3\!!_\_./ _)" [0, 0, 10] 10) -translations - "\!!x\A. P" == "Bexeq 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; - val eqn1i = Thm.prop_of (symmetric eqn1pre) - val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5; - val eqn2i = Thm.prop_of (symmetric eqn2pre) - - val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6)); - val exp_term = Morphism.term exp_morphism; - val exp = Morphism.thm exp_morphism; - - val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN - ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) - val mthdt = Method.Basic (fn _ => mthd) - val bymt = Proof.global_terminal_proof (mthdt, NONE) - val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), - Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*) - -(*||> Local_Theory.theory (fn thy => - let - val global_eqns = map exp_term [eqn2i, eqn1i]; - (* Not sure if the following context should not be used *) - val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; - val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; - in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*) diff -r fa810f01f7b5 -r 25c4223635f4 UnusedQuotMain.thy --- a/UnusedQuotMain.thy Tue Jan 26 20:07:50 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,687 +0,0 @@ -(* 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) -*} - - -(* 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 - - - -