# HG changeset patch # User wenzelm # Date 1163459737 -3600 # Node ID 09c3af731e273db2d8c80ba781ac881740ff75ab # Parent 74c1da5d44be58986c127fc69fe1b4c32d15004b removed theorem(_i); incorporated into IsarCmd; diff -r 74c1da5d44be -r 09c3af731e27 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Mon Nov 13 22:31:23 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,141 +0,0 @@ -(* Title: Pure/Isar/isar_thy.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Derived theory and proof operations. -*) - -signature ISAR_THY = -sig - val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory - val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory - val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory - val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory - val have: ((string * Attrib.src list) * (string * string list) list) list -> - bool -> Proof.state -> Proof.state - val hence: ((string * Attrib.src list) * (string * string list) list) list -> - bool -> Proof.state -> Proof.state - val show: ((string * Attrib.src list) * (string * string list) list) list -> - bool -> Proof.state -> Proof.state - val thus: ((string * Attrib.src list) * (string * string list) list) list -> - bool -> Proof.state -> Proof.state - val theorem: string -> string * Attrib.src list -> string * string list -> theory -> Proof.state - val theorem_i: string -> string * attribute list -> term * term list -> theory -> Proof.state - val qed: Method.text option -> Toplevel.transition -> Toplevel.transition - val terminal_proof: Method.text * Method.text option -> - Toplevel.transition -> Toplevel.transition - val default_proof: Toplevel.transition -> Toplevel.transition - val immediate_proof: Toplevel.transition -> Toplevel.transition - val done_proof: Toplevel.transition -> Toplevel.transition - val skip_proof: Toplevel.transition -> Toplevel.transition - val begin_theory: string -> string list -> (string * bool) list -> bool -> theory - val end_theory: theory -> theory - val kill_theory: string -> unit - val theory: string * string list * (string * bool) list - -> Toplevel.transition -> Toplevel.transition - val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition -end; - -structure IsarThy: ISAR_THY = -struct - -(* axioms *) - -fun add_axms f args thy = - f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy; - -val add_axioms = add_axms (snd oo PureThy.add_axioms); - -fun add_defs ((unchecked, overloaded), args) = - add_axms - (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args; - - -(* facts *) - -fun apply_theorems args thy = - let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)] - in apfst (maps snd) (PureThy.note_thmss "" facts thy) end; - -fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)]; - - -(* goals *) - -local - -fun local_goal opt_chain goal stmt int = - opt_chain #> goal NONE (K Seq.single) stmt int; - -fun global_goal goal kind a propp thy = - goal kind NONE (K I) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); - -in - -val have = local_goal I Proof.have; -val hence = local_goal Proof.chain Proof.have; -val show = local_goal I Proof.show; -val thus = local_goal Proof.chain Proof.show; -val theorem = global_goal Proof.theorem; -val theorem_i = global_goal Proof.theorem_i; - -end; - - -(* local endings *) - -fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true)); -val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof; -val local_default_proof = Toplevel.proofs Proof.local_default_proof; -val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; -val local_done_proof = Toplevel.proofs Proof.local_done_proof; -val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof; - -val skip_local_qed = - Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF)); - - -(* global endings *) - -fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true))); -val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof; -val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof); -val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof); -val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; -val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof); - -val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1); - - -(* common endings *) - -fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed; -fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; -val default_proof = local_default_proof o global_default_proof; -val immediate_proof = local_immediate_proof o global_immediate_proof; -val done_proof = local_done_proof o global_done_proof; -val skip_proof = local_skip_proof o global_skip_proof; - - -(* theory init and exit *) - -fun begin_theory name imports uses = - ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); - -val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory; - -val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; - -fun theory (name, imports, uses) = - Toplevel.init_theory (begin_theory name imports uses) - (fn thy => (end_theory thy; ())) - (kill_theory o Context.theory_name); - -fun init_context f x = Toplevel.init_theory - (fn _ => - (case Context.pass NONE f x of - ((), NONE) => raise Toplevel.UNDEF - | ((), SOME thy) => thy)) - (K ()) (K ()); - -end;