--- a/src/FOL/ex/LocaleTest.thy Wed Mar 19 18:15:25 2008 +0100
+++ b/src/FOL/ex/LocaleTest.thy Wed Mar 19 22:27:57 2008 +0100
@@ -19,7 +19,7 @@
ML {*
fun check_thm name = let
val thy = the_context ();
- val thm = get_thm thy (Name name);
+ val thm = get_thm thy (Facts.Named (name, NONE));
val {prop, hyps, ...} = rep_thm thm;
val prems = Logic.strip_imp_prems prop;
val _ = if null hyps then ()
--- a/src/HOL/Import/proof_kernel.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Import/proof_kernel.ML Wed Mar 19 22:27:57 2008 +0100
@@ -1277,10 +1277,10 @@
case get_hol4_mapping thyname thmname thy of
SOME (SOME thmname) =>
let
- val th1 = (SOME (PureThy.get_thm thy (Name thmname))
+ val th1 = (SOME (PureThy.get_thm thy (Facts.Named (thmname, NONE)))
handle ERROR _ =>
(case split_name thmname of
- SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx-1))
+ SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Facts.Named (listname, NONE)),idx-1))
handle _ => NONE)
| NONE => NONE))
in
@@ -2168,7 +2168,7 @@
fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
case HOL4DefThy.get thy of
Replaying _ => (thy,
- HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
+ HOLThm([], PureThy.get_thm thy (Facts.Named (thmname^"_@intern", NONE))) handle ERROR _ => hth)
| _ =>
let
val _ = message "TYPE_INTRO:"
--- a/src/HOL/Matrix/cplex/matrixlp.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Wed Mar 19 22:27:57 2008 +0100
@@ -78,7 +78,7 @@
"SparseMatrix.sorted_sp_simps",
"ComputeNumeral.number_norm",
"ComputeNumeral.natnorm"]
- fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Name n))
+ fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Facts.Named (n, NONE)))
val ths = List.concat (map get_thms matrix_lemmas)
val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
in
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:27:57 2008 +0100
@@ -977,8 +977,9 @@
val s = post_last_dot(fst(qtn a));
fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t |
param_types _ = error "malformed induct-theorem in preprocess_td";
- val pl = param_types (concl_of (get_thm sg (Name (s ^ ".induct"))));
- val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (Name (s ^ ".induct"))));
+ val induct_rule = PureThy.get_thm sg (Facts.Named (s ^ ".induct", NONE));
+ val pl = param_types (concl_of induct_rule);
+ val l = split_constrs sg (snd(qtn a)) pl (prems_of induct_rule);
val ntl = new_types l;
in
((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
--- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Mar 19 22:27:57 2008 +0100
@@ -339,7 +339,7 @@
fun neq_x_y ctxt x y name =
(let
- val dist_thm = the (try (ProofContext.get_thm ctxt) (PureThy.Name name));
+ val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val tree = term_of ctree;
val x_path = the (find_tree x tree);
--- a/src/HOL/Statespace/state_space.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML Wed Mar 19 22:27:57 2008 +0100
@@ -270,7 +270,7 @@
fun solve_tac ctxt (_,i) st =
let
- val distinct_thm = ProofContext.get_thm ctxt (Name dist_thm_name);
+ val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE));
val goal = List.nth (cprems_of st,i-1);
val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
in EVERY [rtac rule i] st
--- a/src/HOL/Tools/datatype_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -48,8 +48,8 @@
split_thms : (thm * thm) list,
induction : thm,
simps : thm list} * theory
- val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
- (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
+ val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list ->
+ (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -391,7 +391,7 @@
| ManyConstrs (thm, simpset) =>
let
val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
- map (get_thm (ThyInfo.the_theory "Datatype" thy) o Name)
+ map (fn a => get_thm (ThyInfo.the_theory "Datatype" thy) (Facts.Named (a, NONE)))
["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
in
Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Mar 19 22:27:57 2008 +0100
@@ -57,7 +57,8 @@
val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
In0_eq, In1_eq, In0_not_In1, In1_not_In0,
- Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o Name)
+ Lim_inject, Suml_inject, Sumr_inject] =
+ map (fn a => get_thm Datatype_thy (Facts.Named (a, NONE)))
["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
"In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
"Lim_inject", "Suml_inject", "Sumr_inject"];
--- a/src/HOL/Tools/inductive_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -45,7 +45,7 @@
local_theory -> inductive_result * local_theory
val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
(string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+ ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> inductive_result * local_theory
val add_inductive_global: string ->
{verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
@@ -76,7 +76,7 @@
val gen_add_inductive: add_ind_def ->
bool -> bool -> (string * string option * mixfix) list ->
(string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+ ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def ->
bool -> OuterParse.token list ->
--- a/src/HOL/Tools/inductive_realizer.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Mar 19 22:27:57 2008 +0100
@@ -276,8 +276,7 @@
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
let
val qualifier = NameSpace.qualifier (name_of_thm induct);
- val inducts = PureThy.get_thms thy (Name
- (NameSpace.qualified qualifier "inducts"));
+ val inducts = PureThy.get_thms thy (Facts.Named (NameSpace.qualified qualifier "inducts", NONE));
val iTs = term_tvars (prop_of (hd intrs));
val ar = length vs + length iTs;
val params = InductivePackage.params_of raw_induct;
--- a/src/HOL/Tools/inductive_set_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -18,7 +18,7 @@
local_theory -> InductivePackage.inductive_result * local_theory
val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
(string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+ ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> InductivePackage.inductive_result * local_theory
val setup: theory -> theory
end;
--- a/src/HOL/Tools/recdef_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/recdef_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -22,7 +22,7 @@
* {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val defer_recdef: xstring -> string list -> (thmref * Attrib.src list) list
+ val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
-> theory -> theory * {induct_rules: thm}
val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
-> theory -> theory * {induct_rules: thm}
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -98,7 +98,7 @@
fun unqualify s = implode(rev(afpl(rev(explode s))));
val q_atypstr = act_name thy atyp;
val uq_atypstr = unqualify q_atypstr;
-val prem = prems_of (get_thm thy (Name (uq_atypstr ^ ".induct")));
+val prem = prems_of (PureThy.get_thm thy (Facts.Named (uq_atypstr ^ ".induct", NONE)));
in
extract_constrs thy prem
handle malformed =>
@@ -284,7 +284,7 @@
let
fun left_of (( _ $ left) $ _) = left |
left_of _ = raise malformed;
-val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def")));
+val aut_def = concl_of (PureThy.get_thm thy (Facts.Named (aut_name ^ "_def", NONE)));
in
(#T(rep_cterm(cterm_of thy (left_of aut_def))))
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Mar 19 22:27:57 2008 +0100
@@ -126,7 +126,7 @@
(* ----- getting the axioms and definitions --------------------------------- *)
local
- fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
+ fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
in
val ax_abs_iso = ga "abs_iso" dname;
val ax_rep_iso = ga "rep_iso" dname;
@@ -142,7 +142,7 @@
fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
in
- List.concat (map defs_of_con cons)
+ maps defs_of_con cons
end;
val ax_copy_def = ga "copy_def" dname;
end; (* local *)
@@ -281,7 +281,7 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs_dis_def goal tacs end;
- val dis_apps = List.concat (map (fn (c,_) => map (dis_app c) cons) cons);
+ val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
fun dis_defin (con, args) =
let
@@ -320,7 +320,7 @@
in pg axs_mat_def goal tacs end;
val mat_apps =
- List.concat (map (fn (c,_) => map (one_mat c) cons) cons);
+ maps (fn (c,_) => map (one_mat c) cons) cons;
in
val mat_rews = mat_stricts @ mat_apps;
end;
@@ -352,7 +352,7 @@
in pg axs goal tacs end;
val pat_stricts = map pat_strict cons;
- val pat_apps = List.concat (map (fn c => map (pat_app c) cons) cons);
+ val pat_apps = maps (fn c => map (pat_app c) cons) cons;
in
val pat_rews = pat_stricts @ pat_apps;
end;
@@ -379,7 +379,7 @@
asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
in
- val con_stricts = List.concat (map con_strict cons);
+ val con_stricts = maps con_strict cons;
val con_defins = map con_defin cons;
val con_rews = con_stricts @ con_defins;
end;
@@ -407,7 +407,7 @@
fun sel_strict (_, args) =
List.mapPartial (Option.map one_sel o sel_of) args;
in
- val sel_stricts = List.concat (map sel_strict cons);
+ val sel_stricts = maps sel_strict cons;
end;
local
@@ -442,9 +442,9 @@
fun one_sel c n sel = map (sel_app c n sel) cons;
fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
fun one_con (c, args) =
- List.concat (List.mapPartial I (mapn (one_sel' c) 0 args));
+ flat (map_filter I (mapn (one_sel' c) 0 args));
in
- val sel_apps = List.concat (map one_con cons);
+ val sel_apps = maps one_con cons;
end;
local
@@ -491,7 +491,7 @@
fun distincts [] = []
| distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
in distincts cons end;
-val dist_les = List.concat (List.concat distincts_le);
+val dist_les = flat (flat distincts_le);
val dist_eqs =
let
fun distinct (_,args1) ((_,args2), leqs) =
@@ -504,7 +504,7 @@
[eq1, eq2]
end;
fun distincts [] = []
- | distincts ((c,leqs)::cs) = List.concat
+ | distincts ((c,leqs)::cs) = flat
(ListPair.map (distinct c) ((map #1 cs),leqs)) @
distincts cs;
in map standard (distincts (cons ~~ distincts_le)) end;
@@ -612,7 +612,7 @@
(* ----- getting the composite axiom and definitions ------------------------ *)
local
- fun ga s dn = get_thm thy (Name (dn ^ "." ^ s));
+ fun ga s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
in
val axs_reach = map (ga "reach" ) dnames;
val axs_take_def = map (ga "take_def" ) dnames;
@@ -622,12 +622,12 @@
end;
local
- fun gt s dn = get_thm thy (Name (dn ^ "." ^ s));
- fun gts s dn = get_thms thy (Name (dn ^ "." ^ s));
+ fun gt s dn = PureThy.get_thm thy (Facts.Named (dn ^ "." ^ s, NONE));
+ fun gts s dn = PureThy.get_thms thy (Facts.Named (dn ^ "." ^ s, NONE));
in
val cases = map (gt "casedist" ) dnames;
- val con_rews = List.concat (map (gts "con_rews" ) dnames);
- val copy_rews = List.concat (map (gts "copy_rews") dnames);
+ val con_rews = maps (gts "con_rews" ) dnames;
+ val copy_rews = maps (gts "copy_rews") dnames;
end;
fun dc_take dn = %%:(dn^"_take");
@@ -668,7 +668,7 @@
val rhs = con_app2 con (app_rec_arg mk_take) args;
in Library.foldr mk_all (map vname args, lhs === rhs) end;
fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
- val goal = mk_trp (foldr1 mk_conj (List.concat (map mk_eqns eqs)));
+ val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
val simps = List.filter (has_fewer_prems 1) copy_rews;
fun con_tac (con, args) =
if nonlazy_rec args = []
@@ -682,7 +682,7 @@
simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
TRY (safe_tac HOL_cs) ::
- List.concat (map eq_tacs eqs);
+ maps eq_tacs eqs;
in pg copy_take_defs goal tacs end;
in
val take_rews = map standard
@@ -709,14 +709,14 @@
(mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
fun ind_prems_tac prems = EVERY
- (List.concat (map (fn cons =>
+ (maps (fn cons =>
(resolve_tac prems 1 ::
- List.concat (map (fn (_,args) =>
+ maps (fn (_,args) =>
resolve_tac prems 1 ::
map (K(atac 1)) (nonlazy args) @
map (K(atac 1)) (List.filter is_rec args))
- cons)))
- conss));
+ cons))
+ conss);
local
(* check whether every/exists constructor of the n-th part of the equation:
it has a possibly indirectly recursive argument that isn't/is possibly
@@ -765,9 +765,9 @@
fun cases_tacs (cons, cases) =
res_inst_tac [("x","x")] cases 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
- List.concat (map con_tacs cons);
+ maps con_tacs cons;
in
- tacs1 @ List.concat (map cases_tacs (conss ~~ cases))
+ tacs1 @ maps cases_tacs (conss ~~ cases)
end;
in pg'' thy [] goal tacf end;
@@ -836,19 +836,19 @@
asm_simp_tac take_ss 1];
fun con_tacs (con, args) =
asm_simp_tac take_ss 1 ::
- List.concat (map arg_tacs (nonlazy_rec args));
+ maps arg_tacs (nonlazy_rec args);
fun foo_tacs n (cons, cases) =
simp_tac take_ss 1 ::
rtac allI 1 ::
res_inst_tac [("x",x_name n)] cases 1 ::
asm_simp_tac take_ss 1 ::
- List.concat (map con_tacs cons);
+ maps con_tacs cons;
val tacs =
rtac allI 1 ::
induct_tac "n" 1 ::
simp_tac take_ss 1 ::
TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
- List.concat (mapn foo_tacs 1 (conss ~~ cases));
+ flat (mapn foo_tacs 1 (conss ~~ cases));
in pg [] goal tacs end;
fun one_finite (dn, l1b) =
@@ -876,7 +876,7 @@
ind_prems_tac prems];
in
TRY (safe_tac HOL_cs) ::
- List.concat (map finite_tacs (finites ~~ atomize finite_ind))
+ maps finite_tacs (finites ~~ atomize finite_ind)
end;
in pg'' thy [] (ind_term concf) tacf end;
in (finites, ind) end (* let *)
@@ -941,7 +941,7 @@
induct_tac "n" 1,
simp_tac take_ss 1,
safe_tac HOL_cs] @
- List.concat (mapn x_tacs 0 xs);
+ flat (mapn x_tacs 0 xs);
in pg [ax_bisim_def] goal tacs end;
in
val coind =
@@ -954,11 +954,11 @@
mk_trp (foldr1 mk_conj (map mk_eqn xs)));
val tacs =
TRY (safe_tac HOL_cs) ::
- List.concat (map (fn take_lemma => [
+ maps (fn take_lemma => [
rtac take_lemma 1,
cut_facts_tac [coind_lemma] 1,
fast_tac HOL_cs 1])
- take_lemmas);
+ take_lemmas;
in pg [] goal tacs end;
end; (* local *)
--- a/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -267,7 +267,7 @@
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
val cname = case chead_of t of Const(c,_) => c | _ =>
fixrec_err "function is not declared as constant in theory";
- val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
+ val unfold_thm = PureThy.get_thm thy (Facts.Named (cname^"_unfold", NONE));
val simp = Goal.prove_global thy [] [] eq
(fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
in simp end;
--- a/src/Pure/Isar/args.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/args.ML Wed Mar 19 22:27:57 2008 +0100
@@ -82,7 +82,7 @@
val tyname: Context.generic * T list -> string * (Context.generic * T list)
val const: Context.generic * T list -> string * (Context.generic * T list)
val const_proper: Context.generic * T list -> string * (Context.generic * T list)
- val thm_sel: T list -> PureThy.interval list * T list
+ val thm_sel: T list -> Facts.interval list * T list
val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
-> ((int -> tactic) -> tactic) * ('a * T list)
@@ -344,9 +344,9 @@
(* misc *)
val thm_sel = parens (list1
- (nat --| $$$ "-" -- nat >> PureThy.FromTo ||
- nat --| $$$ "-" >> PureThy.From ||
- nat >> PureThy.Single));
+ (nat --| $$$ "-" -- nat >> Facts.FromTo ||
+ nat --| $$$ "-" >> Facts.From ||
+ nat >> Facts.Single));
val bang_facts = Scan.peek (fn context =>
$$$ "!" >> (fn _ => (warning "use of prems in proof method";
--- a/src/Pure/Isar/attrib.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Mar 19 22:27:57 2008 +0100
@@ -19,7 +19,7 @@
val pretty_attribs: Proof.context -> src list -> Pretty.T list
val attribute: theory -> src -> attribute
val attribute_i: theory -> src -> attribute
- val eval_thms: Proof.context -> (thmref * src list) list -> thm list
+ val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val map_specs: ('a -> 'att) ->
(('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
val map_facts: ('a -> 'att) ->
@@ -157,34 +157,36 @@
local
-val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
-
val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
-fun gen_thm pick = Scan.depend (fn st =>
- Args.$$$ "[" |-- Args.attribs (intern (Context.theory_of st)) --| Args.$$$ "]"
- >> (fn srcs =>
+fun gen_thm pick = Scan.depend (fn context =>
+ let
+ val thy = Context.theory_of context;
+ val get = Context.cases PureThy.get_thms ProofContext.get_thms context;
+ fun get_fact s = get (Facts.Fact s);
+ fun get_named s = get (Facts.Named (s, NONE));
+ in
+ Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
let
- val atts = map (attribute_i (Context.theory_of st)) srcs;
- val (st', th') = Library.apply atts (st, Drule.dummy_thm);
- in (st', pick "" [th']) end) ||
- (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
- >> (fn (s, fact) => ("", Fact s, fact)) ||
- Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
- >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
- Scan.ahead fact_name -- Args.named_fact (get_thms st o Name)
- >> (fn (name, fact) => (name, Name name, fact)))
- -- Args.opt_attribs (intern (Context.theory_of st))
- >> (fn ((name, thmref, fact), srcs) =>
- let
- val ths = PureThy.select_thm thmref fact;
- val atts = map (attribute_i (Context.theory_of st)) srcs;
- val (st', ths') = foldl_map (Library.apply atts) (st, ths);
- in (st', pick name ths') end));
+ val atts = map (attribute_i thy) srcs;
+ val (context', th') = Library.apply atts (context, Drule.dummy_thm);
+ in (context', pick "" [th']) end)
+ ||
+ (Scan.ahead Args.alt_name -- Args.named_fact get_fact
+ >> (fn (s, fact) => ("", Facts.Fact s, fact))
+ || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
+ >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
+ -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
+ let
+ val ths = Facts.select thmref fact;
+ val atts = map (attribute_i thy) srcs;
+ val (context', ths') = foldl_map (Library.apply atts) (context, ths);
+ in (context', pick name ths') end)
+ end);
in
-val thm = gen_thm PureThy.single_thm;
+val thm = gen_thm Facts.the_single;
val multi_thm = gen_thm (K I);
val thms = Scan.repeat multi_thm >> flat;
--- a/src/Pure/Isar/calculation.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Mar 19 22:27:57 2008 +0100
@@ -14,9 +14,9 @@
val sym_add: attribute
val sym_del: attribute
val symmetric: attribute
- val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
- val finally_: (thmref * Attrib.src list) list option -> bool ->
+ val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
Proof.state -> Proof.state Seq.seq
val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
val moreover: bool -> Proof.state -> Proof.state
--- a/src/Pure/Isar/element.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/element.ML Wed Mar 19 22:27:57 2008 +0100
@@ -11,16 +11,16 @@
datatype ('typ, 'term) stmt =
Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
Obtains of (string * ((string * 'typ option) list * 'term list)) list
- type statement (*= (string, string) stmt*)
- type statement_i (*= (typ, term) stmt*)
+ type statement = (string, string) stmt
+ type statement_i = (typ, term) stmt
datatype ('typ, 'term, 'fact) ctxt =
Fixes of (string * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
- type context (*= (string, string, thmref) ctxt*)
- type context_i (*= (typ, term, thm list) ctxt*)
+ type context = (string, string, Facts.ref) ctxt
+ type context_i = (typ, term, thm list) ctxt
val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
((string * Attrib.src list) * ('fact * Attrib.src list) list) list ->
((string * Attrib.src list) * ('c * Attrib.src list) list) list
@@ -99,7 +99,7 @@
Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
Notes of string * ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
-type context = (string, string, thmref) ctxt;
+type context = (string, string, Facts.ref) ctxt;
type context_i = (typ, term, thm list) ctxt;
fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
--- a/src/Pure/Isar/find_theorems.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/find_theorems.ML Wed Mar 19 22:27:57 2008 +0100
@@ -49,7 +49,7 @@
(** search criterion filters **)
(*generated filters are to be of the form
- input: (thmref * thm)
+ input: (Facts.ref * thm)
output: (p:int, s:int) option, where
NONE indicates no match
p is the primary sorting criterion
@@ -107,7 +107,7 @@
in match (space_explode "*" pat) str end;
fun filter_name str_pat (thmref, _) =
- if match_string str_pat (PureThy.name_of_thmref thmref)
+ if match_string str_pat (Facts.name_of_ref thmref)
then SOME (0, 0) else NONE;
@@ -243,42 +243,36 @@
EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
| ord => ord) <> GREATER;
-in
+fun nicer (Facts.Named (x, _)) (Facts.Named (y, _)) = nicer_name x y
+ | nicer (Facts.Fact _) (Facts.Named _) = true
+ | nicer (Facts.Named _) (Facts.Fact _) = false;
-fun nicer (Fact _) _ = true
- | nicer (PureThy.Name x) (PureThy.Name y) = nicer_name x y
- | nicer (PureThy.Name _) (Fact _) = false
- | nicer (PureThy.Name _) _ = true
- | nicer (NameSelection (x, _)) (NameSelection (y, _)) = nicer_name x y
- | nicer (NameSelection _) _ = false;
+fun rem_cdups xs =
+ let
+ fun rem_c rev_seen [] = rev rev_seen
+ | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
+ | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
+ if Thm.eq_thm_prop (t, t')
+ then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
+ else rem_c (x :: rev_seen) (y :: xs)
+ in rem_c [] xs end;
-end;
+in
fun rem_thm_dups xs =
- let
- fun rem_cdups xs =
- let
- fun rem_c rev_seen [] = rev rev_seen
- | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
- | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
- if Thm.eq_thm_prop (t, t')
- then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
- else rem_c (x :: rev_seen) (y :: xs)
- in rem_c [] xs end;
+ xs ~~ (1 upto length xs)
+ |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
+ |> rem_cdups
+ |> sort (int_ord o pairself #2)
+ |> map #1;
- in
- xs ~~ (1 upto length xs)
- |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
- |> rem_cdups
- |> sort (int_ord o pairself #2)
- |> map #1
- end;
+end;
(* print_theorems *)
fun all_facts_of ctxt =
- maps PureThy.selections
+ maps Facts.selections
(Facts.dest (PureThy.all_facts_of (ProofContext.theory_of ctxt)) @
Facts.dest (ProofContext.facts_of ctxt));
@@ -300,7 +294,7 @@
val thms = Library.drop (len - lim, matches);
fun prt_fact (thmref, thm) =
- ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
+ ProofContext.pretty_fact ctxt (Facts.string_of_ref thmref, [thm]);
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
(if null thms then [Pretty.str "nothing found"]
--- a/src/Pure/Isar/isar_cmd.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Mar 19 22:27:57 2008 +0100
@@ -17,7 +17,7 @@
val oracle: bstring -> string -> string -> theory -> theory
val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
- val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
+ val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
val declaration: string -> local_theory -> local_theory
val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
@@ -91,18 +91,18 @@
val print_antiquotations: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
val thy_deps: Toplevel.transition -> Toplevel.transition
- val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
+ val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
-> Toplevel.transition -> Toplevel.transition
val unused_thms: (string list * string list option) option ->
Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
val print_cases: Toplevel.transition -> Toplevel.transition
- val print_stmts: string list * (thmref * Attrib.src list) list
+ val print_stmts: string list * (Facts.ref * Attrib.src list) list
-> Toplevel.transition -> Toplevel.transition
- val print_thms: string list * (thmref * Attrib.src list) list
+ val print_thms: string list * (Facts.ref * Attrib.src list) list
-> Toplevel.transition -> Toplevel.transition
- val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
+ val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
-> Toplevel.transition -> Toplevel.transition
val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
--- a/src/Pure/Isar/proof.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 19 22:27:57 2008 +0100
@@ -60,18 +60,18 @@
((string * mixfix) * (term * term list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
- val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
+ val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: ((string * Attrib.src list) *
- (thmref * Attrib.src list) list) list -> state -> state
+ (Facts.ref * Attrib.src list) list) list -> state -> state
val note_thmss_i: ((string * attribute list) *
(thm list * attribute list) list) list -> state -> state
- val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
+ val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
- val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
+ val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
- val using: ((thmref * Attrib.src list) list) list -> state -> state
+ val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
val using_i: ((thm list * attribute list) list) list -> state -> state
- val unfolding: ((thmref * Attrib.src list) list) list -> state -> state
+ val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
val unfolding_i: ((thm list * attribute list) list) list -> state -> state
val invoke_case: string * string option list * Attrib.src list -> state -> state
val invoke_case_i: string * string option list * attribute list -> state -> state
--- a/src/Pure/Isar/proof_context.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 19 22:27:57 2008 +0100
@@ -91,8 +91,8 @@
-> Proof.context * (term list list * (Proof.context -> Proof.context))
val fact_tac: thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
- val get_thm: Proof.context -> thmref -> thm
- val get_thms: Proof.context -> thmref -> thm list
+ val get_thm: Proof.context -> Facts.ref -> thm
+ val get_thms: Proof.context -> Facts.ref -> thm list
val valid_thms: Proof.context -> string * thm list -> bool
val add_path: string -> Proof.context -> Proof.context
val no_base_names: Proof.context -> Proof.context
@@ -102,7 +102,7 @@
val reset_naming: Proof.context -> Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
val note_thmss: string ->
- ((bstring * attribute list) * (thmref * attribute list) list) list ->
+ ((bstring * attribute list) * (Facts.ref * attribute list) list) list ->
Proof.context -> (bstring * thm list) list * Proof.context
val note_thmss_i: string ->
((bstring * attribute list) * (thm list * attribute list) list) list ->
@@ -790,7 +790,7 @@
(* get_thm(s) *)
-fun retrieve_thms _ pick ctxt (Fact s) =
+fun retrieve_thms _ pick ctxt (Facts.Fact s) =
let
val prop = Syntax.read_prop (set_mode mode_default ctxt) s
|> singleton (Variable.polymorphic ctxt);
@@ -802,17 +802,17 @@
val thy = theory_of ctxt;
val local_facts = facts_of ctxt;
val space = Facts.space_of local_facts;
- val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
- val name = PureThy.name_of_thmref thmref;
+ val thmref = Facts.map_name_of_ref (NameSpace.intern space) xthmref;
+ val name = Facts.name_of_ref thmref;
val thms =
if name = "" then [Thm.transfer thy Drule.dummy_thm]
else
(case Facts.lookup local_facts name of
- SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
+ SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
| NONE => from_thy thy xthmref);
in pick name thms end;
-val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
+val get_thm = retrieve_thms PureThy.get_thms Facts.the_single;
val get_thms = retrieve_thms PureThy.get_thms (K I);
val get_thms_silent = retrieve_thms PureThy.get_thms_silent (K I);
@@ -820,7 +820,7 @@
(* valid_thms *)
fun valid_thms ctxt (name, ths) =
- (case try (fn () => get_thms_silent ctxt (Name name)) () of
+ (case try (fn () => get_thms_silent ctxt (Facts.Named (name, NONE))) () of
NONE => false
| SOME ths' => Thm.eq_thms (ths, ths'));
--- a/src/Pure/Isar/proof_display.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/proof_display.ML Wed Mar 19 22:27:57 2008 +0100
@@ -111,8 +111,9 @@
if a <> "" then ((a, ths), j)
else if m = n then ((name, ths), j)
else if m = 1 then
- ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
- else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
+ ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
+ else
+ ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
end;
in fst (fold_map name_res res 1) end;
--- a/src/Pure/Isar/spec_parse.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML Wed Mar 19 22:27:57 2008 +0100
@@ -17,10 +17,10 @@
val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
- val xthm: token list -> (thmref * Attrib.src list) * token list
- val xthms1: token list -> (thmref * Attrib.src list) list * token list
+ val xthm: token list -> (Facts.ref * Attrib.src list) * token list
+ val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
val name_facts: token list ->
- ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
+ ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
val locale_mixfix: token list -> mixfix * token list
val locale_fixes: token list -> (string * string option * mixfix) list * token list
val locale_insts: token list ->
@@ -65,13 +65,13 @@
val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
val thm_sel = P.$$$ "(" |-- P.list1
- (P.nat --| P.minus -- P.nat >> PureThy.FromTo ||
- P.nat --| P.minus >> PureThy.From ||
- P.nat >> PureThy.Single) --| P.$$$ ")";
+ (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
+ P.nat --| P.minus >> Facts.From ||
+ P.nat >> Facts.Single) --| P.$$$ ")";
val xthm =
- P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") ||
- (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs;
+ P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
+ (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
val xthms1 = Scan.repeat1 xthm;
--- a/src/Pure/Isar/specification.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/specification.ML Wed Mar 19 22:27:57 2008 +0100
@@ -43,10 +43,11 @@
local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
- val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
- -> local_theory -> (bstring * thm list) list * local_theory
- val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
- -> local_theory -> (bstring * thm list) list * local_theory
+ val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ local_theory -> (bstring * thm list) list * local_theory
+ val theorems_cmd: string ->
+ ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
+ local_theory -> (bstring * thm list) list * local_theory
val theorem: string -> Method.text option ->
(thm list list -> local_theory -> local_theory) ->
string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
--- a/src/Pure/ML/ml_context.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Mar 19 22:27:57 2008 +0100
@@ -264,21 +264,21 @@
(** fact references **)
-fun thm name = ProofContext.get_thm (the_local_context ()) (Name name);
-fun thms name = ProofContext.get_thms (the_local_context ()) (Name name);
+fun thm name = ProofContext.get_thm (the_local_context ()) (Facts.Named (name, NONE));
+fun thms name = ProofContext.get_thms (the_local_context ()) (Facts.Named (name, NONE));
local
-fun print_interval (FromTo arg) =
- "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
- | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i
- | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i;
+fun print_interval (Facts.FromTo arg) =
+ "Facts.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
+ | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
+ | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
fun thm_sel name =
- Args.thm_sel >> (fn is => "PureThy.NameSelection " ^
- ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is))
- || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name);
+ Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
+ ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
fun thm_antiq kind = value_antiq kind
(Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
--- a/src/Pure/Proof/extraction.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Mar 19 22:27:57 2008 +0100
@@ -766,7 +766,7 @@
(Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
(fn xs => Toplevel.theory (fn thy => add_realizers
(map (fn (((a, vs), s1), s2) =>
- (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy)));
+ (PureThy.get_thm thy (Facts.Named (a, NONE)), (vs, s1, s2))) xs) thy)));
val _ =
OuterSyntax.command "realizability"
@@ -780,8 +780,8 @@
val _ =
OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
- (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory
- (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy)));
+ (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+ extract (map (fn (a, vs) => (PureThy.get_thm thy (Facts.Named (a, NONE)), vs)) xs) thy)));
val etype_of = etype_of o add_syntax;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Mar 19 22:27:57 2008 +0100
@@ -712,7 +712,7 @@
What we want is mapping onto simple PGIP name/context model. *)
val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
val thy = Context.theory_of_proof ctx
- val ths = [PureThy.get_thm thy (PureThy.Name thmname)]
+ val ths = [PureThy.get_thm thy (Facts.Named (thmname, NONE))]
val deps = filter_out (equal "")
(Symtab.keys (fold Proofterm.thms_of_proof
(map Thm.proof_of ths) Symtab.empty))
@@ -764,7 +764,7 @@
[] (* asms *)
th))
- fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
+ fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Facts.Named (name, NONE)))
val string_of_thy = Output.output o
Pretty.string_of o (ProofDisplay.pretty_full_theory false)
--- a/src/Pure/facts.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/facts.ML Wed Mar 19 22:27:57 2008 +0100
@@ -7,6 +7,16 @@
signature FACTS =
sig
+ val the_single: string -> thm list -> thm
+ datatype interval = FromTo of int * int | From of int | Single of int
+ datatype ref =
+ Named of string * interval list option |
+ Fact of string
+ val string_of_ref: ref -> string
+ val name_of_ref: ref -> string
+ val map_name_of_ref: (string -> string) -> ref -> ref
+ val select: ref -> thm list -> thm list
+ val selections: string * thm list -> (ref * thm) list
type T
val space_of: T -> NameSpace.T
val lookup: T -> string -> thm list option
@@ -24,7 +34,76 @@
structure Facts: FACTS =
struct
-(* datatype *)
+(** fact references **)
+
+fun the_single _ [th] : thm = th
+ | the_single name _ = error ("Single theorem expected " ^ quote name);
+
+
+(* datatype interval *)
+
+datatype interval =
+ FromTo of int * int |
+ From of int |
+ Single of int;
+
+fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
+ | string_of_interval (From i) = string_of_int i ^ "-"
+ | string_of_interval (Single i) = string_of_int i;
+
+fun interval n iv =
+ let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
+ (case iv of
+ FromTo (i, j) => if i <= j then i upto j else err ()
+ | From i => if i <= n then i upto n else err ()
+ | Single i => [i])
+ end;
+
+
+(* datatype ref *)
+
+datatype ref =
+ Named of string * interval list option |
+ Fact of string;
+
+fun name_of_ref (Named (name, _)) = name
+ | name_of_ref (Fact _) = error "Illegal literal fact";
+
+fun map_name_of_ref f (Named (name, is)) = Named (f name, is)
+ | map_name_of_ref _ r = r;
+
+fun string_of_ref (Named (name, NONE)) = name
+ | string_of_ref (Named (name, SOME is)) =
+ name ^ enclose "(" ")" (commas (map string_of_interval is))
+ | string_of_ref (Fact _) = error "Illegal literal fact";
+
+
+(* select *)
+
+fun select (Fact _) ths = ths
+ | select (Named (_, NONE)) ths = ths
+ | select (Named (name, SOME ivs)) ths =
+ let
+ val n = length ths;
+ fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
+ fun sel i =
+ if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
+ else nth ths (i - 1);
+ val is = maps (interval n) ivs handle Fail msg => err msg;
+ in map sel is end;
+
+
+(* selections *)
+
+fun selections (name, [th]) = [(Named (name, NONE), th)]
+ | selections (name, ths) =
+ map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths;
+
+
+
+(** fact environment **)
+
+(* datatype T *)
datatype T = Facts of
{facts: thm list NameSpace.table,
--- a/src/Pure/pure_thy.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/pure_thy.ML Wed Mar 19 22:27:57 2008 +0100
@@ -7,14 +7,8 @@
signature BASIC_PURE_THY =
sig
- datatype interval = FromTo of int * int | From of int | Single of int
- datatype thmref =
- Name of string |
- NameSelection of string * interval list |
- Fact of string
- val get_thm: theory -> thmref -> thm
- val get_thms: theory -> thmref -> thm list
- val get_thmss: theory -> thmref list -> thm list
+ val get_thm: theory -> Facts.ref -> thm
+ val get_thms: theory -> Facts.ref -> thm list
structure ProtoPure:
sig
val thy: theory
@@ -44,13 +38,7 @@
val kind_internal: attribute
val has_internal: Markup.property list -> bool
val is_internal: thm -> bool
- val string_of_thmref: thmref -> string
- val single_thm: string -> thm list -> thm
- val name_of_thmref: thmref -> string
- val map_name_of_thmref: (string -> string) -> thmref -> thmref
- val select_thm: thmref -> thm list -> thm list
- val selections: string * thm list -> (thmref * thm) list
- val get_thms_silent: theory -> thmref -> thm list
+ val get_thms_silent: theory -> Facts.ref -> thm list
val theorems_of: theory -> thm list NameSpace.table
val all_facts_of: theory -> Facts.T
val thms_of: theory -> (string * thm) list
@@ -73,7 +61,7 @@
val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
val note: string -> string * thm -> theory -> thm * theory
val note_thmss: string -> ((bstring * attribute list) *
- (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+ (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
val note_thmss_i: string -> ((bstring * attribute list) *
(thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
@@ -182,75 +170,6 @@
fun the_thms _ (SOME thms) = thms
| the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
-fun single_thm _ [thm] = thm
- | single_thm name _ = error ("Single theorem expected " ^ quote name);
-
-
-(* datatype interval *)
-
-datatype interval =
- FromTo of int * int |
- From of int |
- Single of int;
-
-fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
- | string_of_interval (From i) = string_of_int i ^ "-"
- | string_of_interval (Single i) = string_of_int i;
-
-fun interval n iv =
- let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
- (case iv of
- FromTo (i, j) => if i <= j then i upto j else err ()
- | From i => if i <= n then i upto n else err ()
- | Single i => [i])
- end;
-
-
-(* datatype thmref *)
-
-datatype thmref =
- Name of string |
- NameSelection of string * interval list |
- Fact of string;
-
-fun name_of_thmref (Name name) = name
- | name_of_thmref (NameSelection (name, _)) = name
- | name_of_thmref (Fact _) = error "Illegal literal fact";
-
-fun map_name_of_thmref f (Name name) = Name (f name)
- | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
- | map_name_of_thmref _ thmref = thmref;
-
-fun string_of_thmref (Name name) = name
- | string_of_thmref (NameSelection (name, is)) =
- name ^ enclose "(" ")" (commas (map string_of_interval is))
- | string_of_thmref (Fact _) = error "Illegal literal fact";
-
-
-(* select_thm *)
-
-fun select_thm (Name _) thms = thms
- | select_thm (Fact _) thms = thms
- | select_thm (NameSelection (name, ivs)) thms =
- let
- val n = length thms;
- fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
- fun select i =
- if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
- else nth thms (i - 1);
- val is = maps (interval n) ivs handle Fail msg => err msg;
- in map select is end;
-
-
-(* selections *)
-
-fun selections (name, [thm]) = [(Name name, thm)]
- | selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
- (NameSelection (name, [Single i]), thm));
-
-
-(* lookup/get thms *)
-
local
fun lookup_thms thy xname =
@@ -270,7 +189,7 @@
fun get_fact silent theory thmref =
let
- val name = name_of_thmref thmref;
+ val name = Facts.name_of_ref thmref;
val new_res = lookup_fact theory name;
val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
val is_same =
@@ -283,14 +202,13 @@
else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
show_result new_res ^ " vs " ^ show_result old_res ^
Position.str_of (Position.thread_data ()));
- in Option.map #2 old_res |> the_thms name |> select_thm thmref |> map (Thm.transfer theory) end;
+ in Option.map #2 old_res |> the_thms name |> Facts.select thmref |> map (Thm.transfer theory) end;
in
val get_thms_silent = get_fact true;
val get_thms = get_fact false;
-fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
-fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
+fun get_thm thy thmref = Facts.the_single (Facts.name_of_ref thmref) (get_thms thy thmref);
end;
--- a/src/Tools/Compute_Oracle/linker.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML Wed Mar 19 22:27:57 2008 +0100
@@ -192,10 +192,10 @@
fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
local
- fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname)
+ fun get_thm thmname = PureThy.get_thm (theory "Main") (Facts.Named (thmname, NONE))
val eq_th = get_thm "HOL.eq_reflection"
in
- fun eq_to_meta th = (eq_th OF [th] handle _ => th)
+ fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
end
--- a/src/Tools/code/code_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Tools/code/code_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -187,7 +187,7 @@
val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
val tfree_vars = map Logic.mk_type tfrees';
- val c = PureThy.string_of_thmref thmref
+ val c = Facts.string_of_ref thmref
|> NameSpace.explode
|> (fn [x] => [x] | (x::xs) => xs)
|> space_implode "_"
@@ -195,7 +195,7 @@
in if c = "" then NONE else SOME (thmref, propdef) end;
in
Facts.dest (PureThy.all_facts_of thy)
- |> maps PureThy.selections
+ |> maps Facts.selections
|> map_filter select
|> map_filter mk_codeprop
end;
@@ -206,7 +206,7 @@
fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
let
- val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref)
+ val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref)
^ " as code property " ^ quote raw_c);
val ([raw_c'], names') = Name.variants [raw_c] names;
val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
--- a/src/ZF/Tools/datatype_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -33,8 +33,8 @@
val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
val add_datatype: string * string list -> (string * string list * mixfix) list list ->
- (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
- (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
+ (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
+ (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
end;
functor Add_datatype_def_Fun
--- a/src/ZF/Tools/induct_tacs.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Wed Mar 19 22:27:57 2008 +0100
@@ -13,8 +13,8 @@
val induct_tac: string -> int -> tactic
val exhaust_tac: string -> int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
- val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
- (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
+ val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
+ (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
val setup: theory -> theory
end;
@@ -167,8 +167,8 @@
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
let
val ctxt = ProofContext.init thy;
- val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
- val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
+ val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
+ val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
--- a/src/ZF/Tools/inductive_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -33,8 +33,8 @@
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
((bstring * string) * Attrib.src list) list ->
- (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
- (thmref * Attrib.src list) list * (thmref * Attrib.src list) list ->
+ (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
+ (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
theory -> theory * inductive_result
end;