# HG changeset patch # User wenzelm # Date 1002997958 -7200 # Node ID 44034a6474e55aefcbec41d9812cf30b44966b26 # Parent 470e608d7a74e54d7d0de2d3cbf80e2c55a5ff59 generic theorem kinds; diff -r 470e608d7a74 -r 44034a6474e5 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Oct 13 20:32:07 2001 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat Oct 13 20:32:38 2001 +0200 @@ -191,11 +191,11 @@ val theoremsP = OuterSyntax.command "theorems" "define theorems" K.thy_decl - (name_facts >> (Toplevel.theory o IsarThy.have_theorems)); + (name_facts >> (Toplevel.theory o IsarThy.have_theorems Drule.theoremK)); val lemmasP = OuterSyntax.command "lemmas" "define lemmas" K.thy_decl - (name_facts >> (Toplevel.theory o IsarThy.have_lemmas)); + (name_facts >> (Toplevel.theory o IsarThy.have_theorems Drule.lemmaK)); val declareP = OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script @@ -288,11 +288,15 @@ val theoremP = OuterSyntax.command "theorem" "state theorem" K.thy_goal - (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f)); + (statement (IsarThy.theorem Drule.theoremK) >> (Toplevel.print oo Toplevel.theory_to_proof)); val lemmaP = OuterSyntax.command "lemma" "state lemma" K.thy_goal - (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f)); + (statement (IsarThy.theorem Drule.lemmaK) >> (Toplevel.print oo Toplevel.theory_to_proof)); + +val corollaryP = + OuterSyntax.command "corollary" "state corollary" K.thy_goal + (statement (IsarThy.theorem Drule.corollaryK) >> (Toplevel.print oo Toplevel.theory_to_proof)); val showP = OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal @@ -699,12 +703,13 @@ typed_print_translationP, print_ast_translationP, token_translationP, oracleP, (*proof commands*) - theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP, - defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP, - nextP, qedP, terminal_proofP, default_proofP, immediate_proofP, - done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP, - apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP, - cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP, + theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, assumeP, + presumeP, defP, fixP, letP, caseP, thenP, fromP, withP, noteP, + beginP, endP, nextP, qedP, terminal_proofP, default_proofP, + immediate_proofP, done_proofP, skip_proofP, forget_proofP, deferP, + preferP, applyP, apply_endP, proofP, alsoP, finallyP, moreoverP, + ultimatelyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP, + undoP, killP, (*diagnostic commands*) pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, print_syntaxP, print_theoremsP, print_attributesP, diff -r 470e608d7a74 -r 44034a6474e5 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Sat Oct 13 20:32:07 2001 +0200 +++ b/src/Pure/Isar/isar_thy.ML Sat Oct 13 20:32:38 2001 +0200 @@ -63,15 +63,11 @@ 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: + val have_theorems: string -> (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list -> theory -> theory - val have_theorems_i: (((bstring * theory attribute list) * (thm * theory attribute list) list) - * Comment.text) list -> theory -> theory - val have_lemmas: - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list - -> theory -> theory - val have_lemmas_i: (((bstring * theory attribute list) * (thm * theory attribute list) list) + val have_theorems_i: string -> + (((bstring * theory attribute list) * (thm * theory attribute list) list) * Comment.text) list -> theory -> theory val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list -> ProofHistory.T -> ProofHistory.T @@ -94,13 +90,9 @@ val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T val invoke_case_i: (string * Proof.context attribute list) * Comment.text -> ProofHistory.T -> ProofHistory.T - val theorem: ((bstring * Args.src list) * (string * (string list * string list))) - * Comment.text -> bool -> theory -> ProofHistory.T - val theorem_i: ((bstring * theory attribute list) * (term * (term list * term list))) + val theorem: string -> ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text -> bool -> theory -> ProofHistory.T - val lemma: ((bstring * Args.src list) * (string * (string list * string list))) - * Comment.text -> bool -> theory -> ProofHistory.T - val lemma_i: ((bstring * theory attribute list) * (term * (term list * term list))) + val theorem_i: string -> ((bstring * theory attribute list) * (term * (term list * term list))) * Comment.text -> bool -> theory -> ProofHistory.T val assume: (((string * Args.src list) * (string * (string list * string list)) list) * Comment.text) list -> ProofHistory.T -> ProofHistory.T @@ -292,14 +284,15 @@ ((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 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 args' thy; - fun present (name, thms) = Present.results kind name thms; + val (thy', named_thmss) = f (cond_kind kind) args' thy; + fun present (name, thms) = Present.results (kind ^ "s") name thms; in - if kind = "" then () + if kind = "" orelse kind = Drule.internalK then () else Context.setmp (Some thy') (fn () => seq present named_thmss) (); (thy', named_thmss) end; @@ -314,22 +307,17 @@ ((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)]; + 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)]; val declare_theorems = #1 oo (apply_theorems o Comment.ignore); val declare_theorems_i = #1 oo (apply_theorems_i o Comment.ignore); -val have_theorems = - #1 oo (global_have_thmss "theorems" (PureThy.have_thmss []) o map Comment.ignore); -val have_theorems_i = - #1 oo (gen_have_thmss_i (PureThy.have_thmss []) o map Comment.ignore); - -val have_lemmas = - #1 oo (global_have_thmss "lemmas" (PureThy.have_thmss [Drule.tag_lemma]) o map Comment.ignore); -val have_lemmas_i = - #1 oo (gen_have_thmss_i (PureThy.have_thmss [Drule.tag_lemma]) o map Comment.ignore); +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; @@ -405,13 +393,6 @@ local -fun global_statement f ((name, src), s) int thy = - ProofHistory.init (Toplevel.undo_limit int) - (f name (map (Attrib.global_attribute thy) src) s thy); - -fun global_statement_i f ((name, atts), t) int thy = - ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy); - fun local_statement' f g ((name, src), s) int = ProofHistory.apply (fn state => f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s int (g state)); @@ -431,10 +412,13 @@ in -val theorem = global_statement Proof.theorem o Comment.ignore; -val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore; -val lemma = global_statement Proof.lemma o Comment.ignore; -val lemma_i = global_statement_i Proof.lemma_i o Comment.ignore; +fun theorem k (((name, src), s), comment_ignore) int thy = + ProofHistory.init (Toplevel.undo_limit int) + (Proof.theorem k name (map (Attrib.global_attribute thy) src) s thy); + +fun theorem_i k (((name, atts), t), comment_ignore) int thy = + ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k name atts t thy); + val assume = multi_statement Proof.assume o map Comment.ignore; val assume_i = multi_statement_i Proof.assume_i o map Comment.ignore; val presume = multi_statement Proof.presume o map Comment.ignore; @@ -503,7 +487,11 @@ val state = ProofHistory.current prf; val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF; val (thy, res as {kind, name, thm}) = finish state; - in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end); + in + if kind = "" orelse kind = Drule.internalK then () + else (print_result res; Context.setmp (Some thy) (Present.result kind name) thm); + thy + end); val global_qed = global_result o Method.global_qed true o apsome Comment.ignore_interest; val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests; diff -r 470e608d7a74 -r 44034a6474e5 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Oct 13 20:32:07 2001 +0200 +++ b/src/Pure/Isar/proof.ML Sat Oct 13 20:32:38 2001 +0200 @@ -81,13 +81,9 @@ val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list -> state -> state val invoke_case: string * context attribute list -> state -> state - val theorem: bstring -> theory attribute list -> string * (string list * string list) - -> theory -> state - val theorem_i: bstring -> theory attribute list -> term * (term list * term list) + val theorem: string -> bstring -> theory attribute list -> string * (string list * string list) -> theory -> state - val lemma: bstring -> theory attribute list -> string * (string list * string list) - -> theory -> state - val lemma_i: bstring -> theory attribute list -> term * (term list * term list) + val theorem_i: string -> bstring -> theory attribute list -> term * (term list * term list) -> theory -> state val chain: state -> state val from_facts: thm list -> state -> state @@ -127,13 +123,11 @@ (* type goal *) datatype kind = - Theorem of theory attribute list | (*top-level theorem*) - Lemma of theory attribute list | (*top-level lemma*) - Show of context attribute list | (*intermediate result, solving subgoal*) - Have of context attribute list ; (*intermediate result*) + Theorem of string * theory attribute list | (*top-level theorem*) + Show of context attribute list | (*intermediate result, solving subgoal*) + Have of context attribute list ; (*intermediate result*) -val kind_name = - fn Theorem _ => "theorem" | Lemma _ => "lemma" | Show _ => "show" | Have _ => "have"; +val kind_name = fn Theorem (s, _) => s | Show _ => "show" | Have _ => "have"; type goal = (kind * (*result kind*) @@ -619,12 +613,10 @@ (*global goals*) fun global_goal prepp kind name atts x thy = - setup_goal I prepp kind Seq.single name atts x (init_state thy); + setup_goal I prepp (curry Theorem kind) Seq.single name atts x (init_state thy); -val theorem = global_goal ProofContext.bind_propp_schematic Theorem; -val theorem_i = global_goal ProofContext.bind_propp_schematic_i Theorem; -val lemma = global_goal ProofContext.bind_propp_schematic Lemma; -val lemma_i = global_goal ProofContext.bind_propp_schematic_i Lemma; +val theorem = global_goal ProofContext.bind_propp_schematic; +val theorem_i = global_goal ProofContext.bind_propp_schematic_i; (*local goals*) @@ -720,9 +712,7 @@ |> curry Thm.name_thm full_name; val atts = - (case kind of - Theorem atts => atts - | Lemma atts => atts @ [Drule.tag_lemma] + (case kind of Theorem (s, atts) => atts @ [Drule.kind s] | _ => err_malformed "finish_global" state); val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);