--- a/src/Pure/Isar/isar_thy.ML Fri Jan 11 00:30:28 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML Fri Jan 11 00:32:17 2002 +0100
@@ -59,16 +59,27 @@
-> theory -> theory
val add_constdefs_i: (((bstring * typ * mixfix) * Comment.text) * (term * Comment.text)) list
-> theory -> theory
+ val theorems: string ->
+ (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+ -> theory -> theory * (string * thm list) list
+ val theorems_i: string ->
+ (((bstring * theory attribute list)
+ * (thm list * theory attribute list) list) * Comment.text) list
+ -> theory -> theory * (string * thm list) list
+ val locale_theorems: string -> xstring ->
+ (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+ -> theory -> theory * (bstring * thm list) list
+ val locale_theorems_i: string -> string ->
+ (((bstring * Proof.context attribute list)
+ * (thm list * Proof.context attribute list) list) * Comment.text) list
+ -> theory -> theory * (string * thm list) list
+ val smart_theorems: string -> xstring option ->
+ (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
+ -> theory -> theory * (string * thm list) list
+ val declare_theorems: xstring option -> (xstring * Args.src list) list * Comment.text
+ -> theory -> theory
val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
- val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list
- val declare_theorems: (xstring * Args.src list) list * Comment.text -> theory -> theory
- val declare_theorems_i: (thm * theory attribute list) list * Comment.text -> theory -> theory
- val have_theorems: string ->
- (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list
- -> theory -> theory
- val have_theorems_i: string ->
- (((bstring * theory attribute list) * (thm * theory attribute list) list)
- * Comment.text) list -> theory -> theory
+ val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list
-> ProofHistory.T -> ProofHistory.T
val have_facts_i: (((string * Proof.context attribute list) *
@@ -316,66 +327,76 @@
fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args;
+(* attributes *)
+
+local
+
+fun prep_attribs f = map (fn ((name, more_srcs), th_srcs) =>
+ ((name, map f more_srcs), map (apsnd (map f)) th_srcs));
+
+in
+
+fun global_attribs thy = prep_attribs (Attrib.global_attribute thy);
+fun local_attribs thy = prep_attribs (Attrib.local_attribute thy);
+
+end;
+
+
(* theorems *)
local
-fun prep_thmss get attrib = map (fn ((name, more_srcs), th_srcs) =>
- ((name, map attrib more_srcs), map (fn (s, srcs) => (get s, map attrib srcs)) th_srcs));
-
-fun flat_unnamed (x, ys) = (x, flat (map snd ys));
-fun cond_kind k = if k = "" then [] else [Drule.kind k];
+fun present_thmss kind (thy, named_thmss) =
+ let fun present (name, thms) = Present.results (kind ^ "s") name thms in
+ if kind = "" orelse kind = Drule.internalK then ()
+ else Context.setmp (Some thy) (fn () => seq present named_thmss) ();
+ (thy, named_thmss)
+ end;
in
-fun global_have_thmss kind f args thy =
- let
- val args' = prep_thmss (PureThy.get_thms thy) (Attrib.global_attribute thy) args
- val (thy', named_thmss) = f (cond_kind kind) args' thy;
- fun present (name, thms) = Present.results (kind ^ "s") name thms;
- in
- if kind = "" orelse kind = Drule.internalK then ()
- else Context.setmp (Some thy') (fn () => seq present named_thmss) ();
- (thy', named_thmss)
- end;
+fun theorems_i k = (present_thmss k oo PureThy.have_thmss_i (Drule.kind k)) o map Comment.ignore;
+fun locale_theorems_i k loc = (present_thmss k oo Locale.have_thmss_i k loc) o map Comment.ignore;
-fun local_have_thmss f args state =
- let
- val args' = prep_thmss (ProofContext.get_thms (Proof.context_of state))
- (Attrib.local_attribute (Proof.theory_of state)) args;
- in f args' state end;
+fun theorems k args thy = thy
+ |> PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args))
+ |> present_thmss k;
+
+fun locale_theorems k loc args thy = thy
+ |> Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args))
+ |> present_thmss k;
-fun gen_have_thmss_i f args = f (map (fn ((name, more_atts), th_atts) =>
- ((name, more_atts), map (apfst single) th_atts)) args);
-
-fun apply_theorems th_srcs =
- flat_unnamed o global_have_thmss "" PureThy.have_thmss [(("", []), th_srcs)];
-fun apply_theorems_i th_srcs =
- flat_unnamed o gen_have_thmss_i (PureThy.have_thmss []) [(("", []), th_srcs)];
+fun smart_theorems k opt_loc args thy = thy
+ |> (case opt_loc of
+ None => PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args))
+ | Some loc => Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args)))
+ |> present_thmss k;
-val declare_theorems = #1 oo (apply_theorems o Comment.ignore);
-val declare_theorems_i = #1 oo (apply_theorems_i o Comment.ignore);
+fun declare_theorems opt_loc (args, comment) =
+ #1 o smart_theorems "" opt_loc [((("", []), args), comment)];
-fun have_theorems kind =
- #1 oo (global_have_thmss kind PureThy.have_thmss o map Comment.ignore);
-fun have_theorems_i kind =
- #1 oo (gen_have_thmss_i (PureThy.have_thmss (cond_kind kind)) o map Comment.ignore);
-
-val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss o map Comment.ignore;
-val have_facts_i = ProofHistory.apply o gen_have_thmss_i Proof.have_thmss o map Comment.ignore;
+fun apply_theorems args =
+ apsnd (flat o map snd) o theorems "" [((("", []), args), Comment.none)];
+fun apply_theorems_i args =
+ apsnd (flat o map snd) o theorems_i "" [((("", []), args), Comment.none)];
end;
-(* forward chaining *)
+(* facts and forward chaining *)
-fun gen_from_facts f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
+fun local_thmss f args state = f (local_attribs (Proof.theory_of state) args) state;
+fun local_thmss_i f args = f (map (fn ((name, more_atts), th_atts) =>
+ ((name, more_atts), map (apfst single) th_atts)) args);
-val from_facts = gen_from_facts (local_have_thmss Proof.have_thmss) o map Comment.ignore;
-val from_facts_i = gen_from_facts (gen_have_thmss_i Proof.have_thmss) o map Comment.ignore;
-val with_facts = gen_from_facts (local_have_thmss Proof.with_thmss) o map Comment.ignore;
-val with_facts_i = gen_from_facts (gen_have_thmss_i Proof.with_thmss) o map Comment.ignore;
+fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
+val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss o map Comment.ignore;
+val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i o map Comment.ignore;
+val from_facts = chain_thmss (local_thmss Proof.have_thmss) o map Comment.ignore;
+val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i) o map Comment.ignore;
+val with_facts = chain_thmss (local_thmss Proof.with_thmss) o map Comment.ignore;
+val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i) o map Comment.ignore;
fun chain comment_ignore = ProofHistory.apply Proof.chain;
@@ -612,7 +633,7 @@
in
-fun get_thmss srcs = Proof.the_facts o local_have_thmss Proof.have_thmss [(("", []), srcs)];
+fun get_thmss srcs = Proof.the_facts o local_thmss Proof.have_thmss [(("", []), srcs)];
fun get_thmss_i thms _ = thms;
fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x);