src/Pure/Isar/isar_thy.ML
changeset 5915 66f4bde4c6e7
parent 5882 c8096461f5c8
child 5925 669d0bc621e1
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Nov 17 14:13:32 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Nov 17 14:14:38 1998 +0100
     1.3 @@ -5,19 +5,22 @@
     1.4  Derived theory operations.
     1.5  
     1.6  TODO:
     1.7 -  - add_defs: handle empty name (pure_thy.ML (!?));
     1.8    - add_constdefs (atomic!);
     1.9 -  - have_theorems, have_lemmas;
    1.10    - load theory;
    1.11    - 'methods' section (proof macros, ML method defs) (!?);
    1.12    - next_block: ProofHistory open / close (!?);
    1.13 -  - from_facts: attribs, args (!?) (beware of termination!!);
    1.14  *)
    1.15  
    1.16  signature ISAR_THY =
    1.17  sig
    1.18    val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    1.19    val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    1.20 +  val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
    1.21 +    -> theory -> theory
    1.22 +  val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list
    1.23 +    -> theory -> theory
    1.24 +  val have_facts: (string * Args.src list) * (string * Args.src list) list
    1.25 +    -> ProofHistory.T -> ProofHistory.T
    1.26    val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
    1.27    val match_bind: (string * string) list -> ProofHistory.T -> ProofHistory.T
    1.28    val theorem: string -> Args.src list -> string -> theory -> ProofHistory.T
    1.29 @@ -26,7 +29,7 @@
    1.30    val show: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    1.31    val have: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    1.32    val chain: ProofHistory.T -> ProofHistory.T
    1.33 -  val from_facts: string list -> ProofHistory.T -> ProofHistory.T
    1.34 +  val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
    1.35    val begin_block: ProofHistory.T -> ProofHistory.T
    1.36    val next_block: ProofHistory.T -> ProofHistory.T
    1.37    val end_block: ProofHistory.T -> ProofHistory.T
    1.38 @@ -62,10 +65,34 @@
    1.39  
    1.40  (* axioms and defs *)
    1.41  
    1.42 -fun attributize thy (x, srcs) = (x, map (Attrib.global_attribute thy) srcs);
    1.43 +fun add_axms f args thy =
    1.44 +  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
    1.45 +
    1.46 +val add_axioms = add_axms PureThy.add_axioms;
    1.47 +val add_defs = add_axms PureThy.add_defs;
    1.48 +
    1.49 +
    1.50 +(* theorems *)
    1.51 +
    1.52 +fun gen_have_thmss get attrib f ((name, more_srcs), th_srcs) x =
    1.53 +  f name (map (attrib x) more_srcs)
    1.54 +    (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x;
    1.55 +
    1.56  
    1.57 -fun add_axioms axms thy = PureThy.add_axioms (map (attributize thy) axms) thy;
    1.58 -fun add_defs defs thy = PureThy.add_defs (map (attributize thy) defs) thy;
    1.59 +val have_theorems =
    1.60 +  #1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute PureThy.have_tthmss;
    1.61 +
    1.62 +val have_lemmas =
    1.63 +  #1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute
    1.64 +    (fn name => fn more_atts => PureThy.have_tthmss name (more_atts @ [Attribute.tag_lemma]));
    1.65 +
    1.66 +
    1.67 +val have_thmss =
    1.68 +  gen_have_thmss (ProofContext.get_tthms o Proof.context_of)
    1.69 +    (Attrib.local_attribute o Proof.theory_of) Proof.have_tthmss;
    1.70 +
    1.71 +val have_facts = ProofHistory.apply o have_thmss;
    1.72 +val from_facts = ProofHistory.apply o (Proof.chain oo curry have_thmss ("", []));
    1.73  
    1.74  
    1.75  (* context *)
    1.76 @@ -94,10 +121,6 @@
    1.77  
    1.78  val chain = ProofHistory.apply Proof.chain;
    1.79  
    1.80 -fun from_facts names = ProofHistory.apply (fn state =>
    1.81 -  state
    1.82 -  |> Proof.from_facts (ProofContext.get_tthmss (Proof.context_of state) names));
    1.83 -
    1.84  
    1.85  (* end proof *)
    1.86  
    1.87 @@ -161,7 +184,7 @@
    1.88    use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    1.89  
    1.90  val use_setup =
    1.91 -  use_let "setup: (theory -> theory) list" "Theory.apply setup";
    1.92 +  use_let "setup: (theory -> theory) list" "Library.apply setup";
    1.93  
    1.94  
    1.95  (* translation functions *)