# HG changeset patch # User wenzelm # Date 1163459738 -3600 # Node ID 6e58289b66853902e04c9bbc7ba73f5512dd1002 # Parent 09c3af731e273db2d8c80ba781ac881740ff75ab incorporated IsarThy into IsarCmd; diff -r 09c3af731e27 -r 6e58289b6685 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/HOL/Tools/datatype_package.ML Tue Nov 14 00:15:38 2006 +0100 @@ -921,8 +921,8 @@ simps = simps}, thy11) end; -val rep_datatype = gen_rep_datatype IsarThy.apply_theorems; -val rep_datatype_i = gen_rep_datatype IsarThy.apply_theorems_i; +val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems; +val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i; diff -r 09c3af731e27 -r 6e58289b6685 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/HOL/Tools/inductive_package.ML Tue Nov 14 00:15:38 2006 +0100 @@ -766,7 +766,7 @@ (s, SOME (ProofContext.infer_type ctxt' s))) pnames_syn; val cnames_syn' = map (fn (s, _, mx) => (s, SOME (ProofContext.infer_type ctxt' s), mx)) cnames_syn; - val (monos, ctxt'') = LocalTheory.theory_result (IsarThy.apply_theorems raw_monos) ctxt; + val (monos, ctxt'') = LocalTheory.theory_result (IsarCmd.apply_theorems raw_monos) ctxt; in add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt'' end; diff -r 09c3af731e27 -r 6e58289b6685 src/HOL/Tools/old_inductive_package.ML --- a/src/HOL/Tools/old_inductive_package.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/HOL/Tools/old_inductive_package.ML Tue Nov 14 00:15:38 2006 +0100 @@ -858,7 +858,7 @@ val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs; val (cs', intr_ts') = unify_consts thy cs intr_ts; - val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos; + val (monos, thy') = thy |> IsarCmd.apply_theorems raw_monos; in add_inductive_i verbose false "" coind false false cs' ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' diff -r 09c3af731e27 -r 6e58289b6685 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/Pure/Isar/ROOT.ML Tue Nov 14 00:15:38 2006 +0100 @@ -65,6 +65,5 @@ use "rule_insts.ML"; use "../simplifier.ML"; use "find_theorems.ML"; -use "isar_thy.ML"; use "isar_cmd.ML"; use "isar_syn.ML"; diff -r 09c3af731e27 -r 6e58289b6685 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Nov 14 00:15:38 2006 +0100 @@ -2,11 +2,36 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Non-logical toplevel commands. +Derived Isar commands. *) signature ISAR_CMD = 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 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 val welcome: Toplevel.transition -> Toplevel.transition val init_toplevel: Toplevel.transition -> Toplevel.transition val exit: Toplevel.transition -> Toplevel.transition @@ -96,9 +121,96 @@ struct -(* variations on init / exit *) +(* 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 *) + +fun goal opt_chain goal stmt int = + opt_chain #> goal NONE (K Seq.single) stmt int; + +val have = goal I Proof.have; +val hence = goal Proof.chain Proof.have; +val show = goal I Proof.show; +val thus = goal Proof.chain Proof.show; + + +(* 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; + + +(* 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 ()); val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART); + val welcome = Toplevel.imperative (writeln o Session.welcome); val exit = Toplevel.keep (fn state => @@ -115,7 +227,7 @@ val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys; fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name); fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name); -fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name); +fun kill_thy name = Toplevel.imperative (fn () => kill_theory name); (* print state *) diff -r 09c3af731e27 -r 6e58289b6685 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Nov 14 00:15:38 2006 +0100 @@ -15,7 +15,7 @@ val theoryP = OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) - (ThyHeader.args >> (Toplevel.print oo IsarThy.theory)); + (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory)); val endP = OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end) @@ -174,7 +174,7 @@ val axiomsP = OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl - (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms)); + (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarCmd.add_axioms)); val opt_unchecked_overloaded = Scan.optional (P.$$$ "(" |-- P.!!! @@ -184,7 +184,7 @@ val defsP = OuterSyntax.command "defs" "define constants" K.thy_decl (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name - >> (Toplevel.theory o IsarThy.add_defs)); + >> (Toplevel.theory o IsarCmd.add_defs)); (* constant definitions and abbreviations *) @@ -399,22 +399,22 @@ val haveP = OuterSyntax.command "have" "state local goal" (K.tag_proof K.prf_goal) - (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.have)); + (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); val henceP = OuterSyntax.command "hence" "abbreviates \"then have\"" (K.tag_proof K.prf_goal) - (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.hence)); + (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); val showP = OuterSyntax.command "show" "state local goal, solving current obligation" (K.tag_proof K.prf_goal) - (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show)); + (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); val thusP = OuterSyntax.command "thus" "abbreviates \"then show\"" (K.tag_proof K.prf_goal) - (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus)); + (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); (* facts *) @@ -527,32 +527,32 @@ val qedP = OuterSyntax.command "qed" "conclude (sub-)proof" (K.tag_proof K.qed_block) - (Scan.option P.method >> (Toplevel.print3 oo IsarThy.qed)); + (Scan.option P.method >> (Toplevel.print3 oo IsarCmd.qed)); val terminal_proofP = OuterSyntax.command "by" "terminal backward proof" (K.tag_proof K.qed) - (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarThy.terminal_proof)); + (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarCmd.terminal_proof)); val default_proofP = OuterSyntax.command ".." "default proof" (K.tag_proof K.qed) - (Scan.succeed (Toplevel.print3 o IsarThy.default_proof)); + (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof)); val immediate_proofP = OuterSyntax.command "." "immediate proof" (K.tag_proof K.qed) - (Scan.succeed (Toplevel.print3 o IsarThy.immediate_proof)); + (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof)); val done_proofP = OuterSyntax.command "done" "done proof" (K.tag_proof K.qed) - (Scan.succeed (Toplevel.print3 o IsarThy.done_proof)); + (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof)); val skip_proofP = OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" (K.tag_proof K.qed) - (Scan.succeed (Toplevel.print3 o IsarThy.skip_proof)); + (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof)); val forget_proofP = OuterSyntax.command "oops" "forget proof" diff -r 09c3af731e27 -r 6e58289b6685 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/Pure/proof_general.ML Tue Nov 14 00:15:38 2006 +0100 @@ -1377,12 +1377,12 @@ val context_thy_onlyP = OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control - (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); + (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only)); val try_context_thy_onlyP = OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control (P.name >> (Toplevel.no_timing oo - (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); + (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only))); val restartP = OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control diff -r 09c3af731e27 -r 6e58289b6685 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Nov 14 00:15:38 2006 +0100 @@ -396,9 +396,9 @@ else read_i sdom; in thy - |> IsarThy.apply_theorems raw_monos - ||>> IsarThy.apply_theorems raw_type_intrs - ||>> IsarThy.apply_theorems raw_type_elims + |> IsarCmd.apply_theorems raw_monos + ||>> IsarCmd.apply_theorems raw_type_intrs + ||>> IsarCmd.apply_theorems raw_type_elims |-> (fn ((monos, type_intrs), type_elims) => add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims)) end; diff -r 09c3af731e27 -r 6e58289b6685 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Tue Nov 14 00:15:38 2006 +0100 @@ -173,10 +173,10 @@ fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = thy - |> IsarThy.apply_theorems [raw_elim] - ||>> IsarThy.apply_theorems [raw_induct] - ||>> IsarThy.apply_theorems raw_case_eqns - ||>> IsarThy.apply_theorems raw_recursor_eqns + |> IsarCmd.apply_theorems [raw_elim] + ||>> IsarCmd.apply_theorems [raw_induct] + ||>> IsarCmd.apply_theorems raw_case_eqns + ||>> IsarCmd.apply_theorems raw_recursor_eqns |-> (fn (((elims, inducts), case_eqns), recursor_eqns) => rep_datatype_i (PureThy.single_thm "elimination" elims) (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns); diff -r 09c3af731e27 -r 6e58289b6685 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Nov 14 00:15:37 2006 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Nov 14 00:15:38 2006 +0100 @@ -567,10 +567,10 @@ val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs; in thy - |> IsarThy.apply_theorems raw_monos - ||>> IsarThy.apply_theorems raw_con_defs - ||>> IsarThy.apply_theorems raw_type_intrs - ||>> IsarThy.apply_theorems raw_type_elims + |> IsarCmd.apply_theorems raw_monos + ||>> IsarCmd.apply_theorems raw_con_defs + ||>> IsarCmd.apply_theorems raw_type_intrs + ||>> IsarCmd.apply_theorems raw_type_elims |-> (fn (((monos, con_defs), type_intrs), type_elims) => add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims))