--- /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
--- /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 \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+ by(auto simp add: QUOT_TRUE_def)
+
+syntax
+ "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
+translations
+ "\<exists>!!x\<in>A. P" == "Bexeq A (%x. P)"
+
+
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
+lemma atomize_eqv:
+ shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+ assume "A \<equiv> B"
+ then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+ assume *: "Trueprop A \<equiv> 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 "\<not>A" by fact
+ then show "A = B" using * by auto
+ qed
+ then show "A \<equiv> 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 \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
+ by auto
+
+lemma list_induct_hol4:
+ fixes P :: "'a list \<Rightarrow> bool"
+ assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+ shows "\<forall>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 \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> 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)*)
--- /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 \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"})
+ @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> 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 "\<forall>(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 \<longrightarrow> a \<approx> 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 \<Rightarrow> 'a list \<Rightarrow> 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 \<Rightarrow> (nat \<times> nat) list"});
+ ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> 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) \<equiv> (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) \<equiv> (a = b)" by simp
+qed
+
+
+
+
--- 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
--- 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 \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
- by(auto simp add: QUOT_TRUE_def)
-
-syntax
- "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
-translations
- "\<exists>!!x\<in>A. P" == "Bexeq A (%x. P)"
-
-
-(* Atomize infrastructure *)
-(* FIXME/TODO: is this really needed? *)
-(*
-lemma atomize_eqv:
- shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-proof
- assume "A \<equiv> B"
- then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
- assume *: "Trueprop A \<equiv> 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 "\<not>A" by fact
- then show "A = B" using * by auto
- qed
- then show "A \<equiv> 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 \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
- by auto
-
-lemma list_induct_hol4:
- fixes P :: "'a list \<Rightarrow> bool"
- assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
- shows "\<forall>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 \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> 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)*)
--- 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 \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"})
- @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> 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 "\<forall>(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 \<longrightarrow> a \<approx> 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 \<Rightarrow> 'a list \<Rightarrow> 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 \<Rightarrow> (nat \<times> nat) list"});
- ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> 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) \<equiv> (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) \<equiv> (a = b)" by simp
-qed
-
-
-
-