--- 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;
--- 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;
--- 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'
--- 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";
--- 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 *)
--- 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"
--- 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
--- 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;
--- 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);
--- 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))