renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
--- a/NEWS Mon Sep 20 15:29:53 2010 +0200
+++ b/NEWS Mon Sep 20 16:05:25 2010 +0200
@@ -244,6 +244,10 @@
*** ML ***
+* Renamed structure PureThy to Pure_Thy and moved most of its
+operations to structure Global_Theory, to emphasize that this is
+rarely-used global-only stuff.
+
* Discontinued Output.debug. Minor INCOMPATIBILITY, use plain writeln
instead (or tracing for high-volume output).
--- a/src/CTT/CTT.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/CTT/CTT.thy Mon Sep 20 16:05:25 2010 +0200
@@ -10,7 +10,7 @@
uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
begin
-setup PureThy.old_appl_syntax_setup
+setup Pure_Thy.old_appl_syntax_setup
typedecl i
typedecl t
--- a/src/Cube/Cube.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Cube/Cube.thy Mon Sep 20 16:05:25 2010 +0200
@@ -8,7 +8,7 @@
imports Pure
begin
-setup PureThy.old_appl_syntax_setup
+setup Pure_Thy.old_appl_syntax_setup
typedecl "term"
typedecl "context"
--- a/src/FOL/IFOL.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/FOL/IFOL.thy Mon Sep 20 16:05:25 2010 +0200
@@ -26,7 +26,7 @@
subsection {* Syntax and axiomatic basis *}
-setup PureThy.old_appl_syntax_setup
+setup Pure_Thy.old_appl_syntax_setup
classes "term"
default_sort "term"
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Sep 20 16:05:25 2010 +0200
@@ -442,7 +442,7 @@
interpretation int2?: semi "op +"
by unfold_locales (* subsumed, thm int2.assoc not generated *)
-ML {* (PureThy.get_thms @{theory} "int2.assoc";
+ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
error "thm int2.assoc was generated")
handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
--- a/src/FOLP/IFOLP.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/FOLP/IFOLP.thy Mon Sep 20 16:05:25 2010 +0200
@@ -10,7 +10,7 @@
uses ("hypsubst.ML") ("intprover.ML")
begin
-setup PureThy.old_appl_syntax_setup
+setup Pure_Thy.old_appl_syntax_setup
classes "term"
default_sort "term"
--- a/src/HOL/Import/hol4rews.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Mon Sep 20 16:05:25 2010 +0200
@@ -370,7 +370,7 @@
val thm2 = Drule.export_without_context thm1;
in
thy
- |> PureThy.store_thm (Binding.name bthm, thm2)
+ |> Global_Theory.store_thm (Binding.name bthm, thm2)
|> snd
|> add_hol4_theorem bthy bthm hth
end;
--- a/src/HOL/Import/proof_kernel.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Sep 20 16:05:25 2010 +0200
@@ -1261,10 +1261,10 @@
case get_hol4_mapping thyname thmname thy of
SOME (SOME thmname) =>
let
- val th1 = (SOME (PureThy.get_thm thy thmname)
+ val th1 = (SOME (Global_Theory.get_thm thy thmname)
handle ERROR _ =>
(case split_name thmname of
- SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
+ SOME (listname,idx) => (SOME (List.nth(Global_Theory.get_thms thy listname,idx-1))
handle _ => NONE) (* FIXME avoid handle _ *)
| NONE => NONE))
in
@@ -1922,7 +1922,7 @@
| _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
val eq = mk_defeq constname rhs' thy1
- val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1
+ val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1
val _ = ImportRecorder.add_defs thmname eq
val def_thm = hd thms
val thm' = def_thm RS meta_eq_to_obj_eq_thm
@@ -2144,7 +2144,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 (thmname^"_@intern")) handle ERROR _ => hth)
+ HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
| _ =>
let
val _ = message "TYPE_INTRO:"
--- a/src/HOL/Import/replay.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Import/replay.ML Mon Sep 20 16:05:25 2010 +0200
@@ -339,7 +339,7 @@
| delta (Hol_move (fullname, moved_thmname)) thy =
add_hol4_move fullname moved_thmname thy
| delta (Defs (thmname, eq)) thy =
- snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
+ snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
| delta (Hol_theorem (thyname, thmname, th)) thy =
add_hol4_theorem thyname thmname ([], th_of thy th) thy
| delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy =
--- a/src/HOL/Import/shuffler.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Sep 20 16:05:25 2010 +0200
@@ -623,7 +623,7 @@
val shuffles = ShuffleData.get thy
val ignored = collect_ignored shuffles []
val all_thms =
- map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
+ map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (Global_Theory.facts_of thy)))
in
filter (match_consts ignored t) all_thms
end
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Sep 20 16:05:25 2010 +0200
@@ -183,7 +183,7 @@
fun theorems_in_proof_term thm =
let
- val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
+ val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm)
fun collect (s, _, _) = if s <> "" then insert (op =) s else I
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
fun resolve_thms names = map_filter (member_of names) all_thms
--- a/src/HOL/Mutabelle/Mutabelle.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy Mon Sep 20 16:05:25 2010 +0200
@@ -75,12 +75,12 @@
fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
is_executable thy th)
- (PureThy.all_thms_of thy);
+ (Global_Theory.all_thms_of thy);
fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
is_executable thy th)
- (PureThy.all_thms_of thy);
+ (Global_Theory.all_thms_of thy);
*}
ML {*
--- a/src/HOL/Mutabelle/mutabelle.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Mon Sep 20 16:05:25 2010 +0200
@@ -59,7 +59,7 @@
fun all_unconcealed_thms_of thy =
let
- val facts = PureThy.facts_of thy
+ val facts = Global_Theory.facts_of thy
in
Facts.fold_static
(fn (s, ths) =>
--- a/src/HOL/Nominal/nominal_atoms.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Sep 20 16:05:25 2010 +0200
@@ -88,8 +88,8 @@
let val T = fastype_of x
in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
-fun add_thms_string args = PureThy.add_thms ((map o apfst o apfst) Binding.name args);
-fun add_thmss_string args = PureThy.add_thmss ((map o apfst o apfst) Binding.name args);
+fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
+fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
(* this function sets up all matters related to atom- *)
(* kinds; the user specifies a list of atom-kind names *)
@@ -189,7 +189,7 @@
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
in
thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)]
- |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
+ |> Global_Theory.add_defs_unchecked true [((Binding.name name, def2),[])]
|> snd
|> OldPrimrec.add_primrec_unchecked_i "" [(("", def1),[])]
end) ak_names_types thy1;
@@ -244,7 +244,7 @@
val def = Logic.mk_equals
(cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
in
- PureThy.add_defs_unchecked true [((Binding.name name, def),[])] thy'
+ Global_Theory.add_defs_unchecked true [((Binding.name name, def),[])] thy'
end) ak_names_types thy) ak_names_types thy4;
(* proves that every atom-kind is an instance of at *)
@@ -257,7 +257,7 @@
val i_type = Type(ak_name_qu,[]);
val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
val at_type = Logic.mk_type i_type;
- val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5)
+ val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy5)
["at_def",
ak_name ^ "_prm_" ^ ak_name ^ "_def",
ak_name ^ "_prm_" ^ ak_name ^ ".simps",
@@ -321,7 +321,7 @@
val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val pt_type = Logic.mk_type i_type1;
val at_type = Logic.mk_type i_type2;
- val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7)
+ val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy7)
["pt_def",
"pt_" ^ ak_name ^ "1",
"pt_" ^ ak_name ^ "2",
@@ -369,7 +369,7 @@
(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val fs_type = Logic.mk_type i_type1;
val at_type = Logic.mk_type i_type2;
- val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11)
+ val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy11)
["fs_def",
"fs_" ^ ak_name ^ "1"];
@@ -422,8 +422,8 @@
val at_type = Logic.mk_type i_type1;
val at_type' = Logic.mk_type i_type2;
val cp_type = Logic.mk_type i_type0;
- val simp_s = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"];
- val cp1 = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
+ val simp_s = HOL_basic_ss addsimps maps (Global_Theory.get_thms thy') ["cp_def"];
+ val cp1 = Global_Theory.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
@@ -454,7 +454,7 @@
(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val at_type = Logic.mk_type i_type1;
val at_type' = Logic.mk_type i_type2;
- val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy')
+ val simp_s = HOL_ss addsimps maps (Global_Theory.get_thms thy')
["disjoint_def",
ak_name ^ "_prm_" ^ ak_name' ^ "_def",
ak_name' ^ "_prm_" ^ ak_name ^ "_def"];
@@ -493,7 +493,7 @@
let
val qu_name = Sign.full_bname thy' ak_name';
val cls_name = Sign.full_bname thy' ("pt_"^ak_name);
- val at_inst = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
+ val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
val proof1 = EVERY [Class.intro_classes_tac [],
rtac ((at_inst RS at_pt_inst) RS pt1) 1,
@@ -501,7 +501,7 @@
rtac ((at_inst RS at_pt_inst) RS pt3) 1,
atac 1];
val simp_s = HOL_basic_ss addsimps
- maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];
+ maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];
val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
in
@@ -523,8 +523,8 @@
val thy18 = fold (fn ak_name => fn thy =>
let
val cls_name = Sign.full_bname thy ("pt_"^ak_name);
- val at_thm = PureThy.get_thm thy ("at_"^ak_name^"_inst");
- val pt_inst = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
+ val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst");
+ val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst");
fun pt_proof thm =
EVERY [Class.intro_classes_tac [],
@@ -571,11 +571,11 @@
val proof =
(if ak_name = ak_name'
then
- let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
+ let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst");
in EVERY [Class.intro_classes_tac [],
rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
else
- let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
+ let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
in
@@ -593,7 +593,7 @@
val thy24 = fold (fn ak_name => fn thy =>
let
val cls_name = Sign.full_bname thy ("fs_"^ak_name);
- val fs_inst = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
+ val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst");
fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
val fs_thm_unit = fs_unit_inst;
@@ -637,18 +637,18 @@
val proof =
(if (ak_name'=ak_name'') then
(let
- val pt_inst = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst");
- val at_inst = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst");
+ val pt_inst = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst");
+ val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst");
in
EVERY [Class.intro_classes_tac [],
rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
end)
else
(let
- val dj_inst = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
+ val dj_inst = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
val simp_s = HOL_basic_ss addsimps
((dj_inst RS dj_pp_forget)::
- (maps (PureThy.get_thms thy'')
+ (maps (Global_Theory.get_thms thy'')
[ak_name' ^"_prm_"^ak_name^"_def",
ak_name''^"_prm_"^ak_name^"_def"]));
in
@@ -671,9 +671,9 @@
fold (fn ak_name' => fn thy' =>
let
val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name');
- val cp_inst = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
- val pt_inst = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
- val at_inst = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
+ val cp_inst = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
+ val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst");
+ val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst");
fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
@@ -839,27 +839,27 @@
(* list of all at_inst-theorems *)
- val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names
+ val ats = map (fn ak => Global_Theory.get_thm thy32 ("at_"^ak^"_inst")) ak_names
(* list of all pt_inst-theorems *)
- val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
+ val pts = map (fn ak => Global_Theory.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
(* list of all cp_inst-theorems as a collection of lists*)
val cps =
- let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
+ let fun cps_fun ak1 ak2 = Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end;
(* list of all cp_inst-theorems that have different atom types *)
val cps' =
let fun cps'_fun ak1 ak2 =
- if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
+ if ak1=ak2 then NONE else SOME (Global_Theory.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end;
(* list of all dj_inst-theorems *)
val djs =
let fun djs_fun ak1 ak2 =
- if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1))
+ if ak1=ak2 then NONE else SOME(Global_Theory.get_thm thy32 ("dj_"^ak2^"_"^ak1))
in map_filter I (map_product djs_fun ak_names ak_names) end;
(* list of all fs_inst-theorems *)
- val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
+ val fss = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
(* list of all at_inst-theorems *)
- val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names
+ val fs_axs = map (fn ak => Global_Theory.get_thm thy32 ("fs_"^ak^"1")) ak_names
fun inst_pt thms = maps (fn ti => instR ti pts) thms;
fun inst_at thms = maps (fn ti => instR ti ats) thms;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 20 16:05:25 2010 +0200
@@ -306,7 +306,7 @@
val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
- val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
+ val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
val unfolded_perm_eq_thms =
if length descr = length new_type_names then []
@@ -351,8 +351,8 @@
val _ = warning "perm_append_thms";
(*FIXME: these should be looked up statically*)
- val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
- val pt2 = PureThy.get_thm thy2 "pt2";
+ val at_pt_inst = Global_Theory.get_thm thy2 "at_pt_inst";
+ val pt2 = Global_Theory.get_thm thy2 "pt2";
val perm_append_thms = maps (fn a =>
let
@@ -361,7 +361,7 @@
val pi2 = Free ("pi2", permT);
val pt_inst = pt_inst_of thy2 a;
val pt2' = pt_inst RS pt2;
- val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
+ val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
in List.take (map Drule.export_without_context (split_conj_thm
(Goal.prove_global thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a]
@@ -384,8 +384,8 @@
val _ = warning "perm_eq_thms";
- val pt3 = PureThy.get_thm thy2 "pt3";
- val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
+ val pt3 = Global_Theory.get_thm thy2 "pt3";
+ val pt3_rev = Global_Theory.get_thm thy2 "pt3_rev";
val perm_eq_thms = maps (fn a =>
let
@@ -396,7 +396,7 @@
val pt_inst = pt_inst_of thy2 a;
val pt3' = pt_inst RS pt3;
val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
- val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
+ val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
in List.take (map Drule.export_without_context (split_conj_thm
(Goal.prove_global thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
@@ -418,11 +418,11 @@
(**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
- val cp1 = PureThy.get_thm thy2 "cp1";
- val dj_cp = PureThy.get_thm thy2 "dj_cp";
- val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
- val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
- val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
+ val cp1 = Global_Theory.get_thm thy2 "cp1";
+ val dj_cp = Global_Theory.get_thm thy2 "dj_cp";
+ val pt_perm_compose = Global_Theory.get_thm thy2 "pt_perm_compose";
+ val pt_perm_compose_rev = Global_Theory.get_thm thy2 "pt_perm_compose_rev";
+ val dj_perm_perm_forget = Global_Theory.get_thm thy2 "dj_perm_perm_forget";
fun composition_instance name1 name2 thy =
let
@@ -486,7 +486,7 @@
resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
(full_new_type_names' ~~ tyvars) thy
end) atoms |>
- PureThy.add_thmss
+ Global_Theory.add_thmss
[((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
unfolded_perm_eq_thms), [Simplifier.simp_add]),
((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
@@ -578,7 +578,7 @@
val _ = warning "proving closure under permutation...";
- val abs_perm = PureThy.get_thms thy4 "abs_perm";
+ val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
val perm_indnames' = map_filter
(fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
@@ -626,7 +626,7 @@
val pi = Free ("pi", permT);
val T = Type (Sign.intern_type thy name, map TFree tvs);
in apfst (pair r o hd)
- (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
+ (Global_Theory.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
(Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
(Const ("Nominal.perm", permT --> U --> U) $ pi $
@@ -662,7 +662,7 @@
asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1,
asm_full_simp_tac (global_simpset_of thy addsimps
[Rep RS perm_closed RS Abs_inverse]) 1,
- asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
+ asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
end)
(Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
@@ -801,7 +801,7 @@
val def_name = (Long_Name.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
- (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
+ (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
fun dt_constr_defs ((((((_, (_, _, constrs)),
@@ -935,8 +935,8 @@
(** prove injectivity of constructors **)
val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
- val alpha = PureThy.get_thms thy8 "alpha";
- val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
+ val alpha = Global_Theory.get_thms thy8 "alpha";
+ val abs_fresh = Global_Theory.get_thms thy8 "abs_fresh";
val pt_cp_sort =
map (pt_class_of thy8) dt_atoms @
@@ -1087,8 +1087,8 @@
val indnames = Datatype_Prop.make_tnames recTs;
- val abs_supp = PureThy.get_thms thy8 "abs_supp";
- val supp_atm = PureThy.get_thms thy8 "supp_atm";
+ val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
+ val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
val finite_supp_thms = map (fn atom =>
let val atomT = Type (atom, [])
@@ -1103,7 +1103,7 @@
(fn _ => indtac dt_induct indnames 1 THEN
ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
(abs_supp @ supp_atm @
- PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
+ Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
flat supp_thms))))),
length new_type_names))
end) atoms;
@@ -1117,8 +1117,8 @@
val (_, thy9) = thy8 |>
Sign.add_path big_name |>
- PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
- PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
+ Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
+ Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
Sign.parent_path ||>>
Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
@@ -1235,17 +1235,17 @@
val fin_set_fresh = map (fn s =>
at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
val pt1_atoms = map (fn Type (s, _) =>
- PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
+ Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
val pt2_atoms = map (fn Type (s, _) =>
- PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
- val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
- val fs_atoms = PureThy.get_thms thy9 "fin_supp";
- val abs_supp = PureThy.get_thms thy9 "abs_supp";
- val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
- val calc_atm = PureThy.get_thms thy9 "calc_atm";
- val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
- val fresh_left = PureThy.get_thms thy9 "fresh_left";
- val perm_swap = PureThy.get_thms thy9 "perm_swap";
+ Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
+ val exists_fresh' = Global_Theory.get_thms thy9 "exists_fresh'";
+ val fs_atoms = Global_Theory.get_thms thy9 "fin_supp";
+ val abs_supp = Global_Theory.get_thms thy9 "abs_supp";
+ val perm_fresh_fresh = Global_Theory.get_thms thy9 "perm_fresh_fresh";
+ val calc_atm = Global_Theory.get_thms thy9 "calc_atm";
+ val fresh_atm = Global_Theory.get_thms thy9 "fresh_atm";
+ val fresh_left = Global_Theory.get_thms thy9 "fresh_left";
+ val perm_swap = Global_Theory.get_thms thy9 "perm_swap";
fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
let
@@ -1408,9 +1408,9 @@
val (_, thy10) = thy9 |>
Sign.add_path big_name |>
- PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
- PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
- PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
+ Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
+ Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
+ Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
(**** recursion combinator ****)
@@ -1517,13 +1517,13 @@
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
- ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
+ ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
||> Sign.restore_naming thy10;
(** equivariance **)
- val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
- val perm_bij = PureThy.get_thms thy11 "perm_bij";
+ val fresh_bij = Global_Theory.get_thms thy11 "fresh_bij";
+ val perm_bij = Global_Theory.get_thms thy11 "perm_bij";
val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
let
@@ -1565,7 +1565,7 @@
val rec_fin_supp_thms = map (fn aT =>
let
val name = Long_Name.base_name (fst (dest_Type aT));
- val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
+ val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
val aset = HOLogic.mk_setT aT;
val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
val fins = map (fn (f, T) => HOLogic.mk_Trueprop
@@ -1604,7 +1604,7 @@
val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
let
val name = Long_Name.base_name (fst (dest_Type aT));
- val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
+ val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
val a = Free ("a", aT);
val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
(fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
@@ -2018,7 +2018,7 @@
|> Sign.add_consts_i (map (fn ((name, T), T') =>
(Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
- |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+ |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
@@ -2055,7 +2055,7 @@
(* FIXME: theorems are stored in database for testing only *)
val (_, thy13) = thy12 |>
- PureThy.add_thmss
+ Global_Theory.add_thmss
[((Binding.name "rec_equiv", flat rec_equiv_thms), []),
((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Sep 20 16:05:25 2010 +0200
@@ -37,7 +37,7 @@
res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
fun get_dyn_thm thy name atom_name =
- PureThy.get_thm thy name handle ERROR _ =>
+ Global_Theory.get_thm thy name handle ERROR _ =>
error ("The atom type "^atom_name^" is not defined.");
(* End of function waiting to be in the library :o) *)
@@ -126,8 +126,8 @@
val thy = theory_of_thm thm;
val ctxt = ProofContext.init_global thy;
val ss = global_simpset_of thy;
- val abs_fresh = PureThy.get_thms thy "abs_fresh";
- val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
+ val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
+ val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
val ss' = ss addsimps fresh_prod::abs_fresh;
val ss'' = ss' addsimps fresh_perm_app;
val x = hd (tl (OldTerm.term_vars (prop_of exI)));
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Sep 20 16:05:25 2010 +0200
@@ -271,21 +271,21 @@
(NominalDatatype.fresh_const U T $ u $ t)) bvars)
(ts ~~ binder_types (fastype_of p)))) prems;
- val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
- val pt2_atoms = map (fn aT => PureThy.get_thm thy
+ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
+ val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
- val fresh_bij = PureThy.get_thms thy "fresh_bij";
- val perm_bij = PureThy.get_thms thy "perm_bij";
- val fs_atoms = map (fn aT => PureThy.get_thm thy
+ val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
+ val perm_bij = Global_Theory.get_thms thy "perm_bij";
+ val fs_atoms = map (fn aT => Global_Theory.get_thm thy
("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
- val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
- val fresh_atm = PureThy.get_thms thy "fresh_atm";
- val swap_simps = PureThy.get_thms thy "swap_simps";
- val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh";
+ val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
+ val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
+ val swap_simps = Global_Theory.get_thms thy "swap_simps";
+ val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh";
fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
let
@@ -610,7 +610,7 @@
| xs => error ("No such atoms: " ^ commas xs);
atoms)
end;
- val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
+ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
(NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
[mk_perm_bool_simproc names,
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 20 16:05:25 2010 +0200
@@ -290,14 +290,14 @@
HOLogic.mk_setT U --> HOLogic.boolT) $ u)) sets) |>
split_list) prems |> split_list;
- val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
- val pt2_atoms = map (fn a => PureThy.get_thm thy
+ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
+ val pt2_atoms = map (fn a => Global_Theory.get_thm thy
("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
addsimprocs [mk_perm_bool_simproc ["Fun.id"],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
- val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij";
+ val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
val dj_thms = maps (fn a =>
@@ -319,7 +319,7 @@
val p = foldr1 HOLogic.mk_prod (map protect ts);
val atom = fst (dest_Type T);
val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
- val fs_atom = PureThy.get_thm thy
+ val fs_atom = Global_Theory.get_thm thy
("fs_" ^ Long_Name.base_name atom ^ "1");
val avoid_th = Drule.instantiate'
[SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
--- a/src/HOL/Nominal/nominal_permeq.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Mon Sep 20 16:05:25 2010 +0200
@@ -71,8 +71,8 @@
val supports_fresh_rule = @{thm "supports_fresh"};
(* pulls out dynamically a thm via the proof state *)
-fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) name;
-fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) name;
+fun dynamic_thms st name = Global_Theory.get_thms (theory_of_thm st) name;
+fun dynamic_thm st name = Global_Theory.get_thm (theory_of_thm st) name;
(* needed in the process of fully simplifying permutations *)
@@ -107,8 +107,8 @@
(if (applicable_app f) then
let
val name = Long_Name.base_name n
- val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
- val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
+ val at_inst = Global_Theory.get_thm sg ("at_" ^ name ^ "_inst")
+ val pt_inst = Global_Theory.get_thm sg ("pt_" ^ name ^ "_inst")
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
else NONE)
| _ => NONE
@@ -202,13 +202,13 @@
SOME (Drule.instantiate'
[SOME (ctyp_of sg (fastype_of t))]
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
- (mk_meta_eq ([PureThy.get_thm sg ("pt_"^tname'^"_inst"),
- PureThy.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
+ (mk_meta_eq ([Global_Theory.get_thm sg ("pt_"^tname'^"_inst"),
+ Global_Theory.get_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
else
SOME (Drule.instantiate'
[SOME (ctyp_of sg (fastype_of t))]
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
- (mk_meta_eq (PureThy.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS
+ (mk_meta_eq (Global_Theory.get_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS
cp1_aux)))
else NONE
end
--- a/src/HOL/Nominal/nominal_thmdecls.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Sep 20 16:05:25 2010 +0200
@@ -56,7 +56,7 @@
val mypi = Thm.cterm_of thy pi
val T = fastype_of pi'
val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
- val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"
+ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"
in
EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
@@ -175,7 +175,7 @@
"equivariance theorem declaration" #>
Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
"equivariance theorem declaration (without checking the form of the lemma)" #>
- PureThy.add_thms_dynamic (@{binding eqvts}, Data.get);
+ Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get);
end;
--- a/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 20 16:05:25 2010 +0200
@@ -671,7 +671,7 @@
setup {*
Theory.add_consts_i const_decls
-#> (fn thy => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
+#> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy
in (da := thm; thy') end)
*}
--- a/src/HOL/String.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/String.thy Mon Sep 20 16:05:25 2010 +0200
@@ -53,7 +53,8 @@
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
nibbles nibbles;
in
- PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
+ Global_Theory.note_thmss Thm.definitionK
+ [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
end
*}
--- a/src/HOL/Tools/Datatype/datatype.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Sep 20 16:05:25 2010 +0200
@@ -241,7 +241,7 @@
val ([def_thm], thy') =
thy
|> Sign.add_consts_i [(cname', constrT, mx)]
- |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
+ |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
@@ -352,7 +352,7 @@
Logic.mk_equals (Const (iso_name, T --> Univ_elT),
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') =
- apsnd Theory.checkpoint ((PureThy.add_defs false o map Thm.no_attributes) defs thy);
+ apsnd Theory.checkpoint ((Global_Theory.add_defs false o map Thm.no_attributes) defs thy);
(* prove characteristic equations *)
@@ -628,7 +628,7 @@
val ([dt_induct'], thy7) =
thy6
|> Sign.add_path big_name
- |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
+ |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
||> Sign.parent_path
||> Theory.checkpoint;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Sep 20 16:05:25 2010 +0200
@@ -234,11 +234,13 @@
|> Sign.add_consts_i (map (fn ((name, T), T') =>
(Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
- |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
- (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
- Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
- set $ Free ("x", T) $ Free ("y", T'))))))
- (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
+ |> (Global_Theory.add_defs false o map Thm.no_attributes)
+ (map (fn ((((name, comb), set), T), T') =>
+ (Binding.name (Long_Name.base_name name ^ "_def"),
+ Logic.mk_equals (comb, absfree ("x", T,
+ Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+ set $ Free ("x", T) $ Free ("y", T'))))))
+ (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> Sign.parent_path
||> Theory.checkpoint;
@@ -259,7 +261,7 @@
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
- |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
+ |> Global_Theory.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
||> Sign.parent_path
||> Theory.checkpoint
|-> (fn thms => pair (reccomb_names, flat thms))
@@ -319,7 +321,7 @@
val ([def_thm], thy') =
thy
|> Sign.declare_const decl |> snd
- |> (PureThy.add_defs false o map Thm.no_attributes) [def];
+ |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
in (defs @ [def_thm], thy')
end) (hd descr ~~ newTs ~~ case_names ~~
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 20 16:05:25 2010 +0200
@@ -99,7 +99,7 @@
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
- #> PureThy.add_thmss [((Binding.name label, thms), atts)]
+ #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
#-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
@@ -108,7 +108,7 @@
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
- #> PureThy.add_thms [((Binding.name label, thms), atts)]
+ #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
#-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Sep 20 16:05:25 2010 +0200
@@ -109,7 +109,7 @@
fun add_eq_thms tyco =
Theory.checkpoint
#> `(fn thy => mk_eq_eqns thy tyco)
- #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
+ #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
[((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
#> snd
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Sep 20 16:05:25 2010 +0200
@@ -334,7 +334,7 @@
(drop (length dt_names) inducts);
in
thy9
- |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
+ |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []),
((prfx (Binding.name "inducts"), inducts), []),
((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
@@ -367,7 +367,8 @@
|> store_thmss "inject" new_type_names raw_inject
||>> store_thmss "distinct" new_type_names raw_distinct
||> Sign.add_path (space_implode "_" new_type_names)
- ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
+ ||>> Global_Theory.add_thms
+ [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
||> Sign.restore_naming thy1;
in
thy2
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Sep 20 16:05:25 2010 +0200
@@ -122,7 +122,7 @@
val vs = map (fn i => List.nth (pnames, i)) is;
val (thm', thy') = thy
|> Sign.root_path
- |> PureThy.store_thm
+ |> Global_Theory.store_thm
(Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
@@ -193,7 +193,7 @@
val exh_name = Thm.derivation_name exhaust;
val (thm', thy') = thy
|> Sign.root_path
- |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
+ |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
--- a/src/HOL/Tools/Function/size.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML Mon Sep 20 16:05:25 2010 +0200
@@ -142,7 +142,7 @@
|> Sign.add_consts_i (map (fn (s, T) =>
(Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
(size_names ~~ recTs1))
- |> PureThy.add_defs false
+ |> Global_Theory.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
(map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
||> Class.instantiation
@@ -207,11 +207,12 @@
val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
- val ([size_thms], thy'') = PureThy.add_thmss
- [((Binding.name "size", size_eqns),
- [Simplifier.simp_add, Nitpick_Simps.add,
- Thm.declaration_attribute
- (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
+ val ([size_thms], thy'') =
+ Global_Theory.add_thmss
+ [((Binding.name "size", size_eqns),
+ [Simplifier.simp_add, Nitpick_Simps.add,
+ Thm.declaration_attribute
+ (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy';
in
SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Sep 20 16:05:25 2010 +0200
@@ -1303,7 +1303,7 @@
List.partition (is_typedef_axiom ctxt false) user_nondefs
|>> append built_in_nondefs
val defs =
- (thy |> PureThy.all_thms_of
+ (thy |> Global_Theory.all_thms_of
|> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
|> map (prop_of o snd)
|> filter_out is_trivial_definition
@@ -1867,7 +1867,7 @@
fun ground_theorem_table thy =
fold ((fn @{const Trueprop} $ t1 =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
- | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
+ | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
(* TODO: Move to "Nitpick.thy" *)
val basic_ersatz_table =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Sep 20 16:05:25 2010 +0200
@@ -2158,15 +2158,15 @@
val def = Logic.mk_equals (lhs, predterm)
val ([definition], thy') = thy |>
Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
- PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+ Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
val ctxt' = ProofContext.init_global thy'
val rules as ((intro, elim), _) =
create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
in thy'
|> set_function_name Pred name mode mode_cname
|> add_predfun_data name mode (definition, rules)
- |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
- |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
+ |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
+ |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
|> Theory.checkpoint
end;
in
@@ -2883,7 +2883,7 @@
(fn thm => Context.mapping (Code.add_eqn thm) I))))
val thy''' =
Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
- fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
+ fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
[((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
[attrib thy ])] thy))
result_thms' thy'' |> Theory.checkpoint)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Sep 20 16:05:25 2010 +0200
@@ -108,7 +108,7 @@
val def = Logic.mk_equals (lhs, atom)
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
in
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
@@ -327,7 +327,7 @@
val def = Logic.mk_equals (lhs, abs_arg')
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
in
(list_comb (Logic.varify_global const, vars),
((full_constname, [definition])::new_defs, thy'))
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Sep 20 16:05:25 2010 +0200
@@ -57,7 +57,7 @@
val z3_rules_setup =
Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
- PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
+ Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Sep 20 16:05:25 2010 +0200
@@ -708,7 +708,7 @@
fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
let
val thy = ProofContext.theory_of ctxt
- val global_facts = PureThy.facts_of thy
+ val global_facts = Global_Theory.facts_of thy
val local_facts = ProofContext.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
val assms = Assumption.all_assms_of ctxt
--- a/src/HOL/Tools/TFL/tfl.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Sep 20 16:05:25 2010 +0200
@@ -382,7 +382,7 @@
$ functional
val def_term = const_def thy (fid, Ty, wfrec_R_M)
val ([def], thy') =
- PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
+ Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
in (thy', def) end;
end;
@@ -539,7 +539,7 @@
val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
val ([def0], theory) =
thy
- |> PureThy.add_defs false
+ |> Global_Theory.add_defs false
[Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
val def = Thm.unvarify_global def0;
val dummy =
--- a/src/HOL/Tools/choice_specification.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon Sep 20 16:05:25 2010 +0200
@@ -33,7 +33,7 @@
else thname
val def_eq = Logic.mk_equals (Const(cname_full,ctype),
HOLogic.choice_const ctype $ P)
- val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
+ val (thms, thy') = Global_Theory.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
val thm' = [thm,hd thms] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
@@ -189,7 +189,7 @@
if name = ""
then arg |> Library.swap
else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
- PureThy.store_thm (Binding.name name, thm) thy)
+ Global_Theory.store_thm (Binding.name name, thm) thy)
in
args |> apsnd (remove_alls frees)
|> apsnd undo_imps
--- a/src/HOL/Tools/inductive_realizer.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Sep 20 16:05:25 2010 +0200
@@ -273,7 +273,7 @@
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
let
val qualifier = Long_Name.qualifier (name_of_thm induct);
- val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
+ val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
val ar = length vs + length iTs;
val params = Inductive.params_of raw_induct;
@@ -356,7 +356,7 @@
subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
(rintrs ~~ maps snd rss)) [] ||>
Sign.root_path;
- val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
+ val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
(** realizer for induction rule **)
@@ -395,11 +395,11 @@
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
[K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
- val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
+ val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
(Datatype_Aux.split_conj_thm thm');
- val ([thms'], thy'') = PureThy.add_thmss
+ val ([thms'], thy'') = Global_Theory.add_thmss
[((Binding.qualified_name (space_implode "_"
(Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
["correctness"])), thms), [])] thy';
@@ -454,7 +454,7 @@
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
- val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
+ val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
in
Extraction.add_realizers_i
--- a/src/HOL/Tools/old_primrec.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/old_primrec.ML Mon Sep 20 16:05:25 2010 +0200
@@ -308,11 +308,11 @@
end;
fun thy_note ((name, atts), thms) =
- PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+ Global_Theory.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
fun thy_def false ((name, atts), t) =
- PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
+ Global_Theory.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
| thy_def true ((name, atts), t) =
- PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
+ Global_Theory.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
in
--- a/src/HOL/Tools/recdef.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/recdef.ML Mon Sep 20 16:05:25 2010 +0200
@@ -208,9 +208,9 @@
val ((simps' :: rules', [induct']), thy) =
thy
|> Sign.add_path bname
- |> PureThy.add_thmss
+ |> Global_Theory.add_thmss
(((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
- ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
+ ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
@@ -239,7 +239,7 @@
val ([induct_rules'], thy3) =
thy2
|> Sign.add_path bname
- |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])]
+ |> Global_Theory.add_thms [((Binding.name "induct_rules", induct_rules), [])]
||> Sign.parent_path;
in (thy3, {induct_rules = induct_rules'}) end;
--- a/src/HOL/Tools/record.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon Sep 20 16:05:25 2010 +0200
@@ -153,7 +153,7 @@
val ([isom_def], cdef_thy) =
typ_thy
|> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
- |> PureThy.add_defs false
+ |> Global_Theory.add_defs false
[((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
@@ -1658,7 +1658,7 @@
fun mk_defs () =
typ_thy
|> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
- |> PureThy.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
+ |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
||> Theory.checkpoint
val ([ext_def], defs_thy) =
timeit_msg "record extension constructor def:" mk_defs;
@@ -1749,7 +1749,7 @@
val ([induct', inject', surjective', split_meta'], thm_thy) =
defs_thy
- |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
+ |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
[("ext_induct", induct),
("ext_inject", inject),
("ext_surjective", surject),
@@ -2096,11 +2096,12 @@
(sel_decls ~~ (field_syntax @ [NoSyn]))
|> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
- |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
- sel_specs
- ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
- upd_specs
- ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
+ |> (Global_Theory.add_defs false o
+ map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
+ ||>> (Global_Theory.add_defs false o
+ map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
+ ||>> (Global_Theory.add_defs false o
+ map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
[make_spec, fields_spec, extend_spec, truncate_spec]
||> Theory.checkpoint
val (((sel_defs, upd_defs), derived_defs), defs_thy) =
@@ -2339,7 +2340,7 @@
[surjective', equality']),
[induct_scheme', induct', cases_scheme', cases']), thms_thy) =
defs_thy
- |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
+ |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
[("select_convs", sel_convs_standard),
("update_convs", upd_convs_standard),
("select_defs", sel_defs),
@@ -2348,10 +2349,10 @@
("unfold_congs", unfold_congs),
("splits", [split_meta_standard, split_object, split_ex]),
("defs", derived_defs)]
- ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
+ ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
[("surjective", surjective),
("equality", equality)]
- ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
+ ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
[(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
(("induct", induct), induct_type_global name),
(("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
@@ -2364,7 +2365,7 @@
val ([simps', iffs'], thms_thy') =
thms_thy
- |> PureThy.add_thmss
+ |> Global_Theory.add_thmss
[((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
((Binding.name "iffs", iffs), [iff_add])];
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Mon Sep 20 16:05:25 2010 +0200
@@ -63,7 +63,7 @@
(Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
val defs = map2 mk_def consts specs;
val (def_thms, thy) =
- PureThy.add_defs false (map Thm.no_attributes defs) thy;
+ Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
in
((consts, def_thms), thy)
end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon Sep 20 16:05:25 2010 +0200
@@ -194,7 +194,7 @@
||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
in
theorems_thy
- |> PureThy.add_thmss
+ |> Global_Theory.add_thmss
[((Binding.qualified true "rews" comp_dbind,
flat rewss @ take_rews), [])]
|> snd
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Sep 20 16:05:25 2010 +0200
@@ -169,7 +169,7 @@
(* register constant definitions *)
val (fixdef_thms, thy) =
- (PureThy.add_defs false o map Thm.no_attributes)
+ (Global_Theory.add_defs false o map Thm.no_attributes)
(map (Binding.suffix_name "_def") binds ~~ eqns) thy;
(* prove applied version of definitions *)
@@ -201,7 +201,7 @@
(* register unfold theorems *)
val (unfold_thms, thy) =
- (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
+ (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(mk_unfold_thms unfold_binds tuple_unfold_thm) thy;
in
((proj_thms, unfold_thms), thy)
@@ -242,13 +242,13 @@
val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
val eqn = Logic.mk_equals (const, rhs);
val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
- val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
+ val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy;
in
((const, def_thm), thy)
end;
fun add_qualified_thm name (dbind, thm) =
- yield_singleton PureThy.add_thms
+ yield_singleton Global_Theory.add_thms
((Binding.qualified true name dbind, thm), []);
(******************************************************************************)
@@ -349,7 +349,7 @@
val deflation_map_binds = dbinds |>
map (Binding.prefix_name "deflation_" o Binding.suffix_name "_map");
val (deflation_map_thms, thy) = thy |>
- (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
+ (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(conjuncts deflation_map_binds deflation_map_thm);
(* register map functions in theory data *)
@@ -496,7 +496,7 @@
(* register REP equations *)
val REP_eq_binds = map (Binding.prefix_name "REP_eq_") dbinds;
val (_, thy) = thy |>
- (PureThy.add_thms o map Thm.no_attributes)
+ (Global_Theory.add_thms o map Thm.no_attributes)
(REP_eq_binds ~~ REP_eq_thms);
(* define rep/abs functions *)
@@ -607,7 +607,7 @@
val thmR = thm RS @{thm conjunct2};
in (n, thmL):: conjuncts ns thmR end;
val (isodefl_thms, thy) = thy |>
- (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
+ (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(conjuncts isodefl_binds isodefl_thm);
val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
@@ -631,7 +631,7 @@
map prove_map_ID_thm
(map_consts ~~ dom_eqns ~~ REP_thms ~~ isodefl_thms);
val (_, thy) = thy |>
- (PureThy.add_thms o map Thm.no_attributes)
+ (Global_Theory.add_thms o map Thm.no_attributes)
(map_ID_binds ~~ map_ID_thms);
val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Sep 20 16:05:25 2010 +0200
@@ -204,15 +204,15 @@
(******************************************************************************)
fun add_qualified_def name (dbind, eqn) =
- yield_singleton (PureThy.add_defs false)
+ yield_singleton (Global_Theory.add_defs false)
((Binding.qualified true name dbind, eqn), []);
fun add_qualified_thm name (dbind, thm) =
- yield_singleton PureThy.add_thms
+ yield_singleton Global_Theory.add_thms
((Binding.qualified true name dbind, thm), []);
fun add_qualified_simp_thm name (dbind, thm) =
- yield_singleton PureThy.add_thms
+ yield_singleton Global_Theory.add_thms
((Binding.qualified true name dbind, thm), [Simplifier.simp_add]);
(******************************************************************************)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Sep 20 16:05:25 2010 +0200
@@ -124,7 +124,7 @@
val rep_const = #rep_const iso_info;
local
- fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
+ fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
in
val ax_take_0 = ga "take_0" dname;
val ax_take_strict = ga "take_strict" dname;
@@ -200,7 +200,7 @@
in
thy
- |> PureThy.add_thmss [
+ |> Global_Theory.add_thmss [
((qualified "iso_rews" , iso_rews ), [simp]),
((qualified "nchotomy" , [nchotomy] ), []),
((qualified "exhaust" , [exhaust] ),
@@ -240,8 +240,8 @@
val pg = pg' thy;
local
- fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
- fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
+ fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
+ fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s);
in
val axs_rep_iso = map (ga "rep_iso") dnames;
val axs_abs_iso = map (ga "abs_iso") dnames;
@@ -421,10 +421,10 @@
in
thy
- |> snd o PureThy.add_thmss [
+ |> snd o Global_Theory.add_thmss [
((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []),
((Binding.qualified true "induct" comp_dbind, [ind] ), [])]
- |> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
+ |> (snd o Global_Theory.add_thmss (map ind_rule (dnames ~~ inducts)))
end; (* prove_induction *)
(******************************************************************************)
@@ -444,7 +444,7 @@
val n_eqs = length eqs;
val take_rews =
- maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
+ maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
(* ----- define bisimulation predicate -------------------------------------- *)
@@ -465,7 +465,7 @@
singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
fun legacy_infer_prop thy t = legacy_infer_term thy (Type.constraint propT t);
fun infer_props thy = map (apsnd (legacy_infer_prop thy));
- fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
+ fun add_defs_i x = Global_Theory.add_defs false (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
fun one_con (con, args) =
@@ -568,7 +568,7 @@
in pg [] goal (K tacs) end;
end; (* local *)
-in thy |> snd o PureThy.add_thmss
+in thy |> snd o Global_Theory.add_thmss
[((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
end; (* let *)
@@ -603,7 +603,7 @@
val take_lemmas = #take_lemma_thms take_info;
val take_rews =
- maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
+ maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
(* prove induction rules, unless definition is indirect recursive *)
val thy =
--- a/src/HOLCF/Tools/fixrec.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Mon Sep 20 16:05:25 2010 +0200
@@ -419,7 +419,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 (cname^".unfold");
+ val unfold_thm = Global_Theory.get_thm thy (cname^".unfold");
val simp = Goal.prove_global thy [] [] eq
(fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
in simp end;
@@ -431,7 +431,7 @@
val ts = map (prep_term thy) strings;
val simps = map (fix_pat thy) ts;
in
- (snd o PureThy.add_thmss [((name, simps), atts)]) thy
+ (snd o Global_Theory.add_thmss [((name, simps), atts)]) thy
end;
val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
--- a/src/HOLCF/Tools/pcpodef.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Mon Sep 20 16:05:25 2010 +0200
@@ -100,7 +100,7 @@
val (_, thy) =
thy
|> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
+ |> Global_Theory.add_thms
([((Binding.prefix_name "adm_" name, admissible'), []),
((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
@@ -143,7 +143,7 @@
val (_, thy) =
thy
|> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
+ |> Global_Theory.add_thms
([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []),
((Binding.suffix_name "_strict" Abs_name, Abs_strict), []),
((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
--- a/src/HOLCF/Tools/repdef.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Mon Sep 20 16:05:25 2010 +0200
@@ -139,7 +139,7 @@
[type_definition_thm, #below_def cpo_info, emb_def, prj_def];
val (REP_thm, thy) = thy
|> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thm
+ |> Global_Theory.add_thm
((Binding.prefix_name "REP_" name,
Drule.zero_var_indexes (@{thm typedef_REP} OF typedef_thms')), [])
||> Sign.restore_naming thy;
--- a/src/HOLCF/ex/Pattern_Match.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOLCF/ex/Pattern_Match.thy Mon Sep 20 16:05:25 2010 +0200
@@ -379,7 +379,7 @@
(Binding.suffix_name "_def" b, Logic.mk_equals (c, t));
val defs = map2 mk_def consts specs;
val (def_thms, thy) =
- PureThy.add_defs false (map Thm.no_attributes defs) thy;
+ Global_Theory.add_defs false (map Thm.no_attributes defs) thy;
in
((consts, def_thms), thy)
end;
--- a/src/Pure/IsaMakefile Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/IsaMakefile Mon Sep 20 16:05:25 2010 +0200
@@ -218,6 +218,7 @@
drule.ML \
envir.ML \
facts.ML \
+ global_theory.ML \
goal.ML \
goal_display.ML \
interpretation.ML \
--- a/src/Pure/Isar/attrib.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Sep 20 16:05:25 2010 +0200
@@ -181,7 +181,7 @@
fun gen_thm pick = Scan.depend (fn context =>
let
val thy = Context.theory_of context;
- val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
+ val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context;
val get_fact = get o Facts.Fact;
fun get_named pos name = get (Facts.Named ((name, pos), NONE));
in
--- a/src/Pure/Isar/calculation.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Sep 20 16:05:25 2010 +0200
@@ -98,7 +98,7 @@
"declaration of symmetry rule" #>
Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
"resolution with symmetry rule" #>
- PureThy.add_thms
+ Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
((Binding.empty, symmetric_thm), [sym_add])] #> snd));
--- a/src/Pure/Isar/class.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/class.ML Mon Sep 20 16:05:25 2010 +0200
@@ -329,7 +329,7 @@
|> snd
|> Thm.add_def false false (b_def, def_eq)
|>> apsnd Thm.varifyT_global
- |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
+ |-> (fn (_, def_thm) => Global_Theory.store_thm (b_def, def_thm)
#> snd
#> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
|> Sign.add_const_constraint (c', SOME ty')
--- a/src/Pure/Isar/context_rules.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/context_rules.ML Mon Sep 20 16:05:25 2010 +0200
@@ -196,7 +196,7 @@
val dest_query = rule_add elim_queryK Tactic.make_elim;
val _ = Context.>> (Context.map_theory
- (snd o PureThy.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
+ (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
(* concrete syntax *)
--- a/src/Pure/Isar/element.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/element.ML Mon Sep 20 16:05:25 2010 +0200
@@ -480,7 +480,7 @@
val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
in
context |> Context.mapping_result
- (PureThy.note_thmss kind facts')
+ (Global_Theory.note_thmss kind facts')
(ProofContext.note_thmss kind facts')
end;
--- a/src/Pure/Isar/expression.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/expression.ML Mon Sep 20 16:05:25 2010 +0200
@@ -640,7 +640,7 @@
thy
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
- |> PureThy.add_defs false
+ |> Global_Theory.add_defs false
[((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
@@ -681,7 +681,7 @@
val (_, thy'') =
thy'
|> Sign.qualified_path true abinding
- |> PureThy.note_thmss ""
+ |> Global_Theory.note_thmss ""
[((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
@@ -695,7 +695,7 @@
val (_, thy'''') =
thy'''
|> Sign.qualified_path true binding
- |> PureThy.note_thmss ""
+ |> Global_Theory.note_thmss ""
[((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
((Binding.conceal (Binding.name axiomsN), []),
[(map (Drule.export_without_context o Element.conclude_witness) axioms, [])])]
--- a/src/Pure/Isar/generic_target.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML Mon Sep 20 16:05:25 2010 +0200
@@ -122,7 +122,7 @@
|> Drule.zero_var_indexes_list;
(*thm definition*)
- val result = PureThy.name_thm true true name th'';
+ val result = Global_Theory.name_thm true true name th'';
(*import fixes*)
val (tvars, vars) =
@@ -142,7 +142,7 @@
NONE => raise THM ("Failed to re-import result", 0, [result'])
| SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
|> Goal.norm_result
- |> PureThy.name_thm false false name;
+ |> Global_Theory.name_thm false false name;
in (result'', result) end;
@@ -150,11 +150,11 @@
let
val thy = ProofContext.theory_of lthy;
val facts' = facts
- |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
+ |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
(Local_Theory.full_name lthy (fst a))) bs))
- |> PureThy.map_facts (import_export_proof lthy);
- val local_facts = PureThy.map_facts #1 facts';
- val global_facts = PureThy.map_facts #2 facts';
+ |> Global_Theory.map_facts (import_export_proof lthy);
+ val local_facts = Global_Theory.map_facts #1 facts';
+ val global_facts = Global_Theory.map_facts #2 facts';
in
lthy
|> target_notes kind global_facts local_facts
@@ -214,7 +214,7 @@
val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
in
lthy
- |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
|> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
end;
--- a/src/Pure/Isar/isar_cmd.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Sep 20 16:05:25 2010 +0200
@@ -174,8 +174,9 @@
val add_axioms = fold (snd oo Specification.axiom_cmd);
fun add_defs ((unchecked, overloaded), args) thy =
- thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
- (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
+ thy |>
+ (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
+ overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
|> snd;
@@ -215,7 +216,8 @@
val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
-val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact;
+val hide_fact =
+ hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
(* goals *)
--- a/src/Pure/Isar/locale.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/locale.ML Mon Sep 20 16:05:25 2010 +0200
@@ -506,7 +506,7 @@
let
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
- in PureThy.note_thmss kind args'' #> snd end)
+ in Global_Theory.note_thmss kind args'' #> snd end)
(registrations_of (Context.Theory thy) loc) thy))
in ctxt'' end;
--- a/src/Pure/Isar/named_target.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/named_target.ML Mon Sep 20 16:05:25 2010 +0200
@@ -118,7 +118,7 @@
(Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
in
lthy
- |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
+ |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
|> Local_Theory.target (Locale.add_thmss locale kind local_facts')
end
--- a/src/Pure/Isar/proof_context.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Sep 20 16:05:25 2010 +0200
@@ -297,7 +297,7 @@
fun extern_fact ctxt name =
let
val local_facts = facts_of ctxt;
- val global_facts = PureThy.facts_of (theory_of ctxt);
+ val global_facts = Global_Theory.facts_of (theory_of ctxt);
in
if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
then Facts.extern local_facts name
@@ -790,7 +790,7 @@
extern_const = Consts.extern consts};
in
Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
- (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt)))
+ (Local_Syntax.syn_of syntax) (not (Pure_Thy.old_appl_syntax (theory_of ctxt)))
end;
in
@@ -982,7 +982,7 @@
SOME (_, ths) =>
(Context_Position.report ctxt pos (Markup.local_fact name);
map (Thm.transfer thy) (Facts.select thmref ths))
- | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
+ | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
in pick name thms end;
in
@@ -1012,12 +1012,12 @@
val name = full_name ctxt b;
val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
- val facts = PureThy.name_thmss false name raw_facts;
+ val facts = Global_Theory.name_thmss false name raw_facts;
fun app (th, attrs) x =
swap (Library.foldl_map
(Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
val (res, ctxt') = fold_map app facts ctxt;
- val thms = PureThy.name_thms false false name (flat res);
+ val thms = Global_Theory.name_thms false false name (flat res);
val Mode {stmt, ...} = get_mode ctxt;
in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
--- a/src/Pure/Isar/proof_display.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/proof_display.ML Mon Sep 20 16:05:25 2010 +0200
@@ -49,9 +49,9 @@
fun pretty_theorems_diff verbose prev_thys thy =
let
val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
- val facts = PureThy.facts_of thy;
+ val facts = Global_Theory.facts_of thy;
val thmss =
- Facts.dest_static (map PureThy.facts_of prev_thys) facts
+ Facts.dest_static (map Global_Theory.facts_of prev_thys) facts
|> not verbose ? filter_out (Facts.is_concealed facts o #1);
in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
--- a/src/Pure/Isar/specification.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/specification.ML Mon Sep 20 16:05:25 2010 +0200
@@ -180,7 +180,7 @@
val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
fold_map Thm.add_axiom
(map (apfst (fn a => Binding.map_name (K a) b))
- (PureThy.name_multi (Name.of_binding b) (map subst props)))
+ (Global_Theory.name_multi (Name.of_binding b) (map subst props)))
#>> (fn ths => ((b, atts), [(map #2 ths, [])])));
(*facts*)
--- a/src/Pure/ML/ml_context.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Sep 20 16:05:25 2010 +0200
@@ -75,7 +75,7 @@
fun ml_store get (name, ths) =
let
val ths' = Context.>>> (Context.map_theory_result
- (PureThy.store_thms (Binding.name name, ths)));
+ (Global_Theory.store_thms (Binding.name name, ths)));
val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
val _ =
if name = "" then ()
--- a/src/Pure/Proof/extraction.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Sep 20 16:05:25 2010 +0200
@@ -783,11 +783,11 @@
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
|> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
- |> PureThy.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
+ |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
thy'
- |> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
+ |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
(ProofChecker.thm_of_proof thy'
@@ -815,7 +815,7 @@
Keyword.thy_decl
(Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
(fn xs => Toplevel.theory (fn thy => add_realizers
- (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
+ (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
val _ =
Outer_Syntax.command "realizability"
@@ -830,7 +830,7 @@
val _ =
Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
(Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
- extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
+ extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
val etype_of = etype_of o add_syntax;
--- a/src/Pure/Proof/proof_syntax.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Mon Sep 20 16:05:25 2010 +0200
@@ -88,7 +88,7 @@
fun proof_of_term thy ty =
let
- val thms = PureThy.all_thms_of thy;
+ val thms = Global_Theory.all_thms_of thy;
val axms = Theory.all_axioms_of thy;
fun mk_term t = (if ty then I else map_types (K dummyT))
@@ -188,7 +188,7 @@
fun cterm_of_proof thy prf =
let
- val thm_names = map fst (PureThy.all_thms_of thy);
+ val thm_names = map fst (Global_Theory.all_thms_of thy);
val axm_names = map fst (Theory.all_axioms_of thy);
val thy' = thy
|> add_proof_syntax
@@ -207,7 +207,7 @@
fun read_term thy topsort =
let
- val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy));
+ val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
val axm_names = map fst (Theory.all_axioms_of thy);
val ctxt = thy
|> add_proof_syntax
--- a/src/Pure/Proof/proofchecker.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML Mon Sep 20 16:05:25 2010 +0200
@@ -16,7 +16,7 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
+ let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
in
(fn s => case Symtab.lookup tab s of
NONE => error ("Unknown theorem " ^ quote s)
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 20 16:05:25 2010 +0200
@@ -267,8 +267,8 @@
fun new_thms_deps thy thy' =
let
- val prev_facts = PureThy.facts_of thy;
- val facts = PureThy.facts_of thy';
+ val prev_facts = Global_Theory.facts_of thy;
+ val facts = Global_Theory.facts_of thy';
in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
end;
@@ -519,7 +519,7 @@
fun theory_facts name =
let val thy = Thy_Info.get_theory name
- in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
+ in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end;
fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
@@ -608,7 +608,7 @@
What we want is mapping onto simple PGIP name/context model. *)
val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
val thy = ProofContext.theory_of ctx
- val ths = [PureThy.get_thm thy thmname]
+ val ths = [Global_Theory.get_thm thy thmname]
val deps = #2 (thms_deps ths);
in
if null deps then ()
@@ -649,7 +649,7 @@
text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
fun strings_of_thm (thy, name) =
- map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
+ map (Display.string_of_thm_global thy) (Global_Theory.get_thms thy name)
val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
in
--- a/src/Pure/ROOT.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/ROOT.ML Mon Sep 20 16:05:25 2010 +0200
@@ -134,6 +134,7 @@
use "thm.ML";
use "more_thm.ML";
use "facts.ML";
+use "global_theory.ML";
use "pure_thy.ML";
use "drule.ML";
use "morphism.ML";
--- a/src/Pure/Thy/thm_deps.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML Mon Sep 20 16:05:25 2010 +0200
@@ -49,7 +49,7 @@
fun unused_thms (base_thys, thys) =
let
fun add_fact space (name, ths) =
- if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
+ if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
else
let val {concealed, group, ...} = Name_Space.the_entry space name in
fold_rev (fn th =>
@@ -60,7 +60,7 @@
fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
val new_thms =
- fold (add_facts o PureThy.facts_of) thys []
+ fold (add_facts o Global_Theory.facts_of) thys []
|> sort_distinct (string_ord o pairself #1);
val used =
--- a/src/Pure/Thy/thy_info.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Sep 20 16:05:25 2010 +0200
@@ -194,7 +194,7 @@
tasks |> maps (fn name =>
let
val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
- val _ = PureThy.join_proofs thy;
+ val _ = Global_Theory.join_proofs thy;
val _ = after_load ();
in [] end handle exn => [Exn.Exn exn])
|> rev |> Exn.release_all;
--- a/src/Pure/Tools/find_theorems.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Sep 20 16:05:25 2010 +0200
@@ -350,7 +350,7 @@
fun nicer_shortest ctxt =
let
(* FIXME global name space!? *)
- val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
+ val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
val shorten =
Name_Space.extern_flags
@@ -381,7 +381,7 @@
|> filter_out (Facts.is_concealed facts o #1);
in
maps Facts.selections
- (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @
+ (visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @
visible_facts (ProofContext.facts_of ctxt))
end;
--- a/src/Pure/Tools/named_thms.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Tools/named_thms.ML Mon Sep 20 16:05:25 2010 +0200
@@ -39,6 +39,6 @@
val setup =
Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
- PureThy.add_thms_dynamic (Binding.name name, content);
+ Global_Theory.add_thms_dynamic (Binding.name name, content);
end;
--- a/src/Pure/assumption.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/assumption.ML Mon Sep 20 16:05:25 2010 +0200
@@ -81,7 +81,7 @@
(*named prems -- legacy feature*)
val _ = Context.>>
- (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
+ (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
--- a/src/Pure/axclass.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/axclass.ML Mon Sep 20 16:05:25 2010 +0200
@@ -390,7 +390,7 @@
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> apsnd Thm.varifyT_global
#-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
+ #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), [])
#> #2
#> pair (Const (c, T))))
||> Sign.restore_naming thy
@@ -419,7 +419,7 @@
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
- val (th', thy') = PureThy.store_thm
+ val (th', thy') = Global_Theory.store_thm
(Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
val th'' = th'
|> Thm.unconstrainT
@@ -438,7 +438,7 @@
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val (th', thy') = PureThy.store_thm
+ val (th', thy') = Global_Theory.store_thm
(Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
val args = Name.names Name.context Name.aT Ss;
@@ -560,7 +560,7 @@
val ([def], def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])];
+ |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])];
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
@@ -571,7 +571,7 @@
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
def_thy
|> Sign.qualified_path true bconst
- |> PureThy.note_thmss ""
+ |> Global_Theory.note_thmss ""
[((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
((Binding.name "axioms", []),
@@ -586,7 +586,8 @@
facts_thy
|> fold (#2 oo put_trancl_classrel) (map (pair class) super ~~ classrel)
|> Sign.qualified_path false bconst
- |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> #2
+ |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms))
+ |> #2
|> Sign.restore_naming facts_thy
|> map_axclasses (Symtab.update (class, axclass))
|> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
--- a/src/Pure/drule.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/drule.ML Mon Sep 20 16:05:25 2010 +0200
@@ -433,10 +433,10 @@
val read_prop = certify o Simple_Syntax.read_prop;
fun store_thm name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
+ Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th)));
fun store_thm_open name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
+ Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
fun store_standard_thm name th = store_thm name (export_without_context th);
fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/global_theory.ML Mon Sep 20 16:05:25 2010 +0200
@@ -0,0 +1,224 @@
+(* Title: Pure/global_theory.ML
+ Author: Makarius
+
+Global theory content: stored facts.
+*)
+
+signature GLOBAL_THEORY =
+sig
+ val facts_of: theory -> Facts.T
+ val intern_fact: theory -> xstring -> string
+ val defined_fact: theory -> string -> bool
+ val hide_fact: bool -> string -> theory -> theory
+ val join_proofs: theory -> unit
+ val get_fact: Context.generic -> theory -> Facts.ref -> thm list
+ val get_thms: theory -> xstring -> thm list
+ val get_thm: theory -> xstring -> thm
+ val all_thms_of: theory -> (string * thm) list
+ val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
+ val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
+ val burrow_facts: ('a list -> 'b list) ->
+ ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
+ val name_multi: string -> 'a list -> (string * 'a) list
+ val name_thm: bool -> bool -> string -> thm -> thm
+ val name_thms: bool -> bool -> string -> thm list -> thm list
+ val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
+ val store_thms: binding * thm list -> theory -> thm list * theory
+ val store_thm: binding * thm -> theory -> thm * theory
+ val store_thm_open: binding * thm -> theory -> thm * theory
+ val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
+ val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
+ val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
+ val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
+ val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
+ -> theory -> (string * thm list) list * theory
+ val add_defs: bool -> ((binding * term) * attribute list) list ->
+ theory -> thm list * theory
+ val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
+ theory -> thm list * theory
+ val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
+ theory -> thm list * theory
+ val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
+ theory -> thm list * theory
+end;
+
+structure Global_Theory: GLOBAL_THEORY =
+struct
+
+(** theory data **)
+
+structure Data = Theory_Data
+(
+ type T = Facts.T * thm list;
+ val empty = (Facts.empty, []);
+ fun extend (facts, _) = (facts, []);
+ fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+);
+
+
+(* facts *)
+
+val facts_of = #1 o Data.get;
+
+val intern_fact = Facts.intern o facts_of;
+val defined_fact = Facts.defined o facts_of;
+
+fun hide_fact fully name = Data.map (apfst (Facts.hide fully name));
+
+
+(* proofs *)
+
+fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
+
+fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
+
+
+
+(** retrieve theorems **)
+
+fun get_fact context thy xthmref =
+ let
+ val xname = Facts.name_of_ref xthmref;
+ val pos = Facts.pos_of_ref xthmref;
+
+ val name = intern_fact thy xname;
+ val res = Facts.lookup context (facts_of thy) name;
+ val _ = Theory.check_thy thy;
+ in
+ (case res of
+ NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
+ | SOME (static, ths) =>
+ (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
+ Facts.select xthmref (map (Thm.transfer thy) ths)))
+ end;
+
+fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
+fun get_thm thy name = Facts.the_single name (get_thms thy name);
+
+fun all_thms_of thy =
+ Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
+
+
+
+(** store theorems **)
+
+(* fact specifications *)
+
+fun map_facts f = map (apsnd (map (apfst (map f))));
+fun burrow_fact f = split_list #>> burrow f #> op ~~;
+fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
+
+
+(* naming *)
+
+fun name_multi name [x] = [(name, x)]
+ | name_multi "" xs = map (pair "") xs
+ | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
+
+fun name_thm pre official name thm = thm
+ |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
+ |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
+
+fun name_thms pre official name xs =
+ map (uncurry (name_thm pre official)) (name_multi name xs);
+
+fun name_thmss official name fact =
+ burrow_fact (name_thms true official name) fact;
+
+
+(* enter_thms *)
+
+fun enter_thms pre_name post_name app_att (b, thms) thy =
+ if Binding.is_empty b
+ then swap (register_proofs (app_att (thy, thms)))
+ else
+ let
+ val naming = Sign.naming_of thy;
+ val name = Name_Space.full_name naming b;
+ val (thy', thms') =
+ register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+ val thms'' = map (Thm.transfer thy') thms';
+ val thy'' = thy' |> (Data.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
+ in (thms'', thy'') end;
+
+
+(* store_thm(s) *)
+
+fun store_thms (b, thms) =
+ enter_thms (name_thms true true) (name_thms false true) I (b, thms);
+
+fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
+
+fun store_thm_open (b, th) =
+ enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
+
+
+(* add_thms(s) *)
+
+fun add_thms_atts pre_name ((b, thms), atts) =
+ enter_thms pre_name (name_thms false true)
+ (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
+
+fun gen_add_thmss pre_name =
+ fold_map (add_thms_atts pre_name);
+
+fun gen_add_thms pre_name args =
+ apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
+
+val add_thmss = gen_add_thmss (name_thms true true);
+val add_thms = gen_add_thms (name_thms true true);
+val add_thm = yield_singleton add_thms;
+
+
+(* add_thms_dynamic *)
+
+fun add_thms_dynamic (b, f) thy = thy
+ |> (Data.map o apfst)
+ (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
+
+
+(* note_thmss *)
+
+fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
+ let
+ val pos = Binding.pos_of b;
+ val name = Sign.full_name thy b;
+ val _ = Position.report pos (Markup.fact_decl name);
+
+ fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
+ val (thms, thy') = thy |> enter_thms
+ (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
+ (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
+ in ((name, thms), thy') end);
+
+
+(* store axioms as theorems *)
+
+local
+
+fun no_read _ (_, t) = t;
+
+fun read thy (b, str) =
+ Syntax.read_prop_global thy str handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
+
+fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
+ let
+ val prop = prep thy (b, raw_prop);
+ val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+ val thm = def
+ |> Thm.forall_intr_frees
+ |> Thm.forall_elim_vars 0
+ |> Thm.varifyT_global;
+ in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
+
+in
+
+val add_defs = add no_read false;
+val add_defs_unchecked = add no_read true;
+val add_defs_cmd = add read false;
+val add_defs_unchecked_cmd = add read true;
+
+end;
+
+end;
--- a/src/Pure/pure_thy.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/pure_thy.ML Mon Sep 20 16:05:25 2010 +0200
@@ -1,235 +1,18 @@
(* Title: Pure/pure_thy.ML
Author: Markus Wenzel, TU Muenchen
-Theorem storage. Pure theory syntax and logical content.
+Pure theory syntax and further logical content.
*)
signature PURE_THY =
sig
- val facts_of: theory -> Facts.T
- val intern_fact: theory -> xstring -> string
- val defined_fact: theory -> string -> bool
- val hide_fact: bool -> string -> theory -> theory
- val join_proofs: theory -> unit
- val get_fact: Context.generic -> theory -> Facts.ref -> thm list
- val get_thms: theory -> xstring -> thm list
- val get_thm: theory -> xstring -> thm
- val all_thms_of: theory -> (string * thm) list
- val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
- val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
- val burrow_facts: ('a list -> 'b list) ->
- ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
- val name_multi: string -> 'a list -> (string * 'a) list
- val name_thm: bool -> bool -> string -> thm -> thm
- val name_thms: bool -> bool -> string -> thm list -> thm list
- val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
- val store_thms: binding * thm list -> theory -> thm list * theory
- val store_thm: binding * thm -> theory -> thm * theory
- val store_thm_open: binding * thm -> theory -> thm * theory
- val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
- val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
- val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
- val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
- val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
- -> theory -> (string * thm list) list * theory
- val add_defs: bool -> ((binding * term) * attribute list) list ->
- theory -> thm list * theory
- val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
- theory -> thm list * theory
- val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
- theory -> thm list * theory
- val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
- theory -> thm list * theory
val old_appl_syntax: theory -> bool
val old_appl_syntax_setup: theory -> theory
end;
-structure PureThy: PURE_THY =
+structure Pure_Thy: PURE_THY =
struct
-
-(*** stored facts ***)
-
-(** theory data **)
-
-structure Global_Facts = Theory_Data
-(
- type T = Facts.T * thm list;
- val empty = (Facts.empty, []);
- fun extend (facts, _) = (facts, []);
- fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
-);
-
-
-(* facts *)
-
-val facts_of = #1 o Global_Facts.get;
-
-val intern_fact = Facts.intern o facts_of;
-val defined_fact = Facts.defined o facts_of;
-
-fun hide_fact fully name = Global_Facts.map (apfst (Facts.hide fully name));
-
-
-(* proofs *)
-
-fun register_proofs (thy, thms) = (Global_Facts.map (apsnd (append thms)) thy, thms);
-
-fun join_proofs thy = Thm.join_proofs (rev (#2 (Global_Facts.get thy)));
-
-
-
-(** retrieve theorems **)
-
-fun get_fact context thy xthmref =
- let
- val xname = Facts.name_of_ref xthmref;
- val pos = Facts.pos_of_ref xthmref;
-
- val name = intern_fact thy xname;
- val res = Facts.lookup context (facts_of thy) name;
- val _ = Theory.check_thy thy;
- in
- (case res of
- NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
- | SOME (static, ths) =>
- (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
- Facts.select xthmref (map (Thm.transfer thy) ths)))
- end;
-
-fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
-fun get_thm thy name = Facts.the_single name (get_thms thy name);
-
-fun all_thms_of thy =
- Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
-
-
-
-(** store theorems **)
-
-(* fact specifications *)
-
-fun map_facts f = map (apsnd (map (apfst (map f))));
-fun burrow_fact f = split_list #>> burrow f #> op ~~;
-fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
-
-
-(* naming *)
-
-fun name_multi name [x] = [(name, x)]
- | name_multi "" xs = map (pair "") xs
- | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
-
-fun name_thm pre official name thm = thm
- |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
- |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
-
-fun name_thms pre official name xs =
- map (uncurry (name_thm pre official)) (name_multi name xs);
-
-fun name_thmss official name fact =
- burrow_fact (name_thms true official name) fact;
-
-
-(* enter_thms *)
-
-fun enter_thms pre_name post_name app_att (b, thms) thy =
- if Binding.is_empty b
- then swap (register_proofs (app_att (thy, thms)))
- else
- let
- val naming = Sign.naming_of thy;
- val name = Name_Space.full_name naming b;
- val (thy', thms') =
- register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
- val thms'' = map (Thm.transfer thy') thms';
- val thy'' = thy' |> (Global_Facts.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
- in (thms'', thy'') end;
-
-
-(* store_thm(s) *)
-
-fun store_thms (b, thms) =
- enter_thms (name_thms true true) (name_thms false true) I (b, thms);
-
-fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
-
-fun store_thm_open (b, th) =
- enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
-
-
-(* add_thms(s) *)
-
-fun add_thms_atts pre_name ((b, thms), atts) =
- enter_thms pre_name (name_thms false true)
- (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
-
-fun gen_add_thmss pre_name =
- fold_map (add_thms_atts pre_name);
-
-fun gen_add_thms pre_name args =
- apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
-
-val add_thmss = gen_add_thmss (name_thms true true);
-val add_thms = gen_add_thms (name_thms true true);
-val add_thm = yield_singleton add_thms;
-
-
-(* add_thms_dynamic *)
-
-fun add_thms_dynamic (b, f) thy = thy
- |> (Global_Facts.map o apfst)
- (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
-
-
-(* note_thmss *)
-
-fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
- let
- val pos = Binding.pos_of b;
- val name = Sign.full_name thy b;
- val _ = Position.report pos (Markup.fact_decl name);
-
- fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
- val (thms, thy') = thy |> enter_thms
- (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
- (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
- in ((name, thms), thy') end);
-
-
-(* store axioms as theorems *)
-
-local
-
-fun no_read _ (_, t) = t;
-
-fun read thy (b, str) =
- Syntax.read_prop_global thy str handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
-
-fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
- let
- val prop = prep thy (b, raw_prop);
- val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
- val thm = def
- |> Thm.forall_intr_frees
- |> Thm.forall_elim_vars 0
- |> Thm.varifyT_global;
- in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
-
-in
-
-val add_defs = add no_read false;
-val add_defs_unchecked = add no_read true;
-val add_defs_cmd = add read false;
-val add_defs_unchecked_cmd = add read true;
-
-end;
-
-
-
-(*** Pure theory syntax and logical content ***)
-
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
@@ -366,7 +149,7 @@
[(Binding.name "term", typ "'a => prop", NoSyn),
(Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
(Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
- #> (add_defs false o map Thm.no_attributes)
+ #> (Global_Theory.add_defs false o map Thm.no_attributes)
[(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
(Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
(Binding.name "sort_constraint_def",
@@ -376,7 +159,7 @@
#> Sign.hide_const false "Pure.term"
#> Sign.hide_const false "Pure.sort_constraint"
#> Sign.hide_const false "Pure.conjunction"
- #> add_thmss [((Binding.name "nothing", []), [])] #> snd
+ #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
#> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
end;
--- a/src/Sequents/Sequents.thy Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Sequents/Sequents.thy Mon Sep 20 16:05:25 2010 +0200
@@ -10,7 +10,7 @@
uses ("prover.ML")
begin
-setup PureThy.old_appl_syntax_setup
+setup Pure_Thy.old_appl_syntax_setup
declare [[unify_trace_bound = 20, unify_search_bound = 40]]
--- a/src/ZF/Tools/datatype_package.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon Sep 20 16:05:25 2010 +0200
@@ -242,17 +242,18 @@
val need_recursor = (not coind andalso recursor_typ <> case_typ);
fun add_recursor thy =
- if need_recursor then
- thy |> Sign.add_consts_i
- [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
- |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
- else thy;
+ if need_recursor then
+ thy
+ |> Sign.add_consts_i
+ [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
+ |> (snd o Global_Theory.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
+ else thy;
val (con_defs, thy0) = thy_path
|> Sign.add_consts_i
(map (fn (c, T, mx) => (Binding.name c, T, mx))
((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
- |> PureThy.add_defs false
+ |> Global_Theory.add_defs false
(map (Thm.no_attributes o apfst Binding.name)
(case_def ::
flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
@@ -379,7 +380,7 @@
in
(*Updating theory components: simprules and datatype info*)
(thy1 |> Sign.add_path big_rec_base_name
- |> PureThy.add_thmss
+ |> Global_Theory.add_thmss
[((Binding.name "simps", simps), [Simplifier.simp_add]),
((Binding.empty , intrs), [Classical.safe_intro NONE]),
((Binding.name "con_defs", con_defs), []),
--- a/src/ZF/Tools/ind_cases.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML Mon Sep 20 16:05:25 2010 +0200
@@ -50,7 +50,7 @@
val facts = args |> map (fn ((name, srcs), props) =>
((name, map (Attrib.attribute thy) srcs),
map (Thm.no_attributes o single o smart_cases ctxt) props));
- in thy |> PureThy.note_thmss "" facts |> snd end;
+ in thy |> Global_Theory.note_thmss "" facts |> snd end;
(* ind_cases method *)
--- a/src/ZF/Tools/induct_tacs.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Sep 20 16:05:25 2010 +0200
@@ -158,7 +158,7 @@
in
thy
|> Sign.add_path (Long_Name.base_name big_rec_name)
- |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
+ |> Global_Theory.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Sign.parent_path
--- a/src/ZF/Tools/inductive_package.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Mon Sep 20 16:05:25 2010 +0200
@@ -172,7 +172,7 @@
val (_, thy1) =
thy
|> Sign.add_path big_rec_base_name
- |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
+ |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
val ctxt1 = ProofContext.init_global thy1;
@@ -508,7 +508,7 @@
val ([induct', mutual_induct'], thy') =
thy
- |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
+ |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
[case_names, Induct.induct_pred big_rec_name]),
((Binding.name "mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
@@ -520,7 +520,7 @@
if not coind then induction_rules raw_induct thy1
else
(thy1
- |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
+ |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
|> apfst hd |> Library.swap, @{thm TrueI})
and defs = big_rec_def :: part_rec_defs
@@ -528,16 +528,16 @@
val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) =
thy2
|> IndCases.declare big_rec_name make_cases
- |> PureThy.add_thms
+ |> Global_Theory.add_thms
[((Binding.name "bnd_mono", bnd_mono), []),
((Binding.name "dom_subset", dom_subset), []),
((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
- ||>> (PureThy.add_thmss o map Thm.no_attributes)
+ ||>> (Global_Theory.add_thmss o map Thm.no_attributes)
[(Binding.name "defs", defs),
(Binding.name "intros", intrs)];
val (intrs'', thy4) =
thy3
- |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
+ |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
||> Sign.parent_path;
in
(thy4,
--- a/src/ZF/Tools/primrec_package.ML Mon Sep 20 15:29:53 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Mon Sep 20 16:05:25 2010 +0200
@@ -169,7 +169,7 @@
val ([def_thm], thy1) = thy
|> Sign.add_path (Long_Name.base_name fname)
- |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
+ |> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val eqn_thms =
@@ -179,10 +179,10 @@
val (eqn_thms', thy2) =
thy1
- |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
+ |> Global_Theory.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
- |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
+ |> Global_Theory.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
||> Sign.parent_path;
in (thy3, eqn_thms') end;