incorporated IsarThy into IsarCmd;
authorwenzelm
Tue Nov 14 00:15:38 2006 +0100 (2006-11-14)
changeset 213506e58289b6685
parent 21349 09c3af731e27
child 21351 1fb804b96d7c
incorporated IsarThy into IsarCmd;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/old_inductive_package.ML
src/Pure/Isar/ROOT.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/proof_general.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Nov 14 00:15:37 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Nov 14 00:15:38 2006 +0100
     1.3 @@ -921,8 +921,8 @@
     1.4        simps = simps}, thy11)
     1.5    end;
     1.6  
     1.7 -val rep_datatype = gen_rep_datatype IsarThy.apply_theorems;
     1.8 -val rep_datatype_i = gen_rep_datatype IsarThy.apply_theorems_i;
     1.9 +val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems;
    1.10 +val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i;
    1.11  
    1.12  
    1.13  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Nov 14 00:15:37 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Nov 14 00:15:38 2006 +0100
     2.3 @@ -766,7 +766,7 @@
     2.4        (s, SOME (ProofContext.infer_type ctxt' s))) pnames_syn;
     2.5      val cnames_syn' = map (fn (s, _, mx) =>
     2.6        (s, SOME (ProofContext.infer_type ctxt' s), mx)) cnames_syn;
     2.7 -    val (monos, ctxt'') = LocalTheory.theory_result (IsarThy.apply_theorems raw_monos) ctxt;
     2.8 +    val (monos, ctxt'') = LocalTheory.theory_result (IsarCmd.apply_theorems raw_monos) ctxt;
     2.9    in
    2.10      add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt''
    2.11    end;
     3.1 --- a/src/HOL/Tools/old_inductive_package.ML	Tue Nov 14 00:15:37 2006 +0100
     3.2 +++ b/src/HOL/Tools/old_inductive_package.ML	Tue Nov 14 00:15:38 2006 +0100
     3.3 @@ -858,7 +858,7 @@
     3.4      val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs;
     3.5      val (cs', intr_ts') = unify_consts thy cs intr_ts;
     3.6  
     3.7 -    val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
     3.8 +    val (monos, thy') = thy |> IsarCmd.apply_theorems raw_monos;
     3.9    in
    3.10      add_inductive_i verbose false "" coind false false cs'
    3.11        ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
     4.1 --- a/src/Pure/Isar/ROOT.ML	Tue Nov 14 00:15:37 2006 +0100
     4.2 +++ b/src/Pure/Isar/ROOT.ML	Tue Nov 14 00:15:38 2006 +0100
     4.3 @@ -65,6 +65,5 @@
     4.4  use "rule_insts.ML";
     4.5  use "../simplifier.ML";
     4.6  use "find_theorems.ML";
     4.7 -use "isar_thy.ML";
     4.8  use "isar_cmd.ML";
     4.9  use "isar_syn.ML";
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 14 00:15:37 2006 +0100
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 14 00:15:38 2006 +0100
     5.3 @@ -2,11 +2,36 @@
     5.4      ID:         $Id$
     5.5      Author:     Markus Wenzel, TU Muenchen
     5.6  
     5.7 -Non-logical toplevel commands.
     5.8 +Derived Isar commands.
     5.9  *)
    5.10  
    5.11  signature ISAR_CMD =
    5.12  sig
    5.13 +  val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    5.14 +  val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    5.15 +  val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    5.16 +  val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    5.17 +  val have: ((string * Attrib.src list) * (string * string list) list) list ->
    5.18 +    bool -> Proof.state -> Proof.state
    5.19 +  val hence: ((string * Attrib.src list) * (string * string list) list) list ->
    5.20 +    bool -> Proof.state -> Proof.state
    5.21 +  val show: ((string * Attrib.src list) * (string * string list) list) list ->
    5.22 +    bool -> Proof.state -> Proof.state
    5.23 +  val thus: ((string * Attrib.src list) * (string * string list) list) list ->
    5.24 +    bool -> Proof.state -> Proof.state
    5.25 +  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    5.26 +  val terminal_proof: Method.text * Method.text option ->
    5.27 +    Toplevel.transition -> Toplevel.transition
    5.28 +  val default_proof: Toplevel.transition -> Toplevel.transition
    5.29 +  val immediate_proof: Toplevel.transition -> Toplevel.transition
    5.30 +  val done_proof: Toplevel.transition -> Toplevel.transition
    5.31 +  val skip_proof: Toplevel.transition -> Toplevel.transition
    5.32 +  val begin_theory: string -> string list -> (string * bool) list -> bool -> theory
    5.33 +  val end_theory: theory -> theory
    5.34 +  val kill_theory: string -> unit
    5.35 +  val theory: string * string list * (string * bool) list
    5.36 +    -> Toplevel.transition -> Toplevel.transition
    5.37 +  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
    5.38    val welcome: Toplevel.transition -> Toplevel.transition
    5.39    val init_toplevel: Toplevel.transition -> Toplevel.transition
    5.40    val exit: Toplevel.transition -> Toplevel.transition
    5.41 @@ -96,9 +121,96 @@
    5.42  struct
    5.43  
    5.44  
    5.45 -(* variations on init / exit *)
    5.46 +(* axioms *)
    5.47 +
    5.48 +fun add_axms f args thy =
    5.49 +  f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
    5.50 +
    5.51 +val add_axioms = add_axms (snd oo PureThy.add_axioms);
    5.52 +
    5.53 +fun add_defs ((unchecked, overloaded), args) =
    5.54 +  add_axms
    5.55 +    (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args;
    5.56 +
    5.57 +
    5.58 +(* facts *)
    5.59 +
    5.60 +fun apply_theorems args thy =
    5.61 +  let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)]
    5.62 +  in apfst (maps snd) (PureThy.note_thmss "" facts thy) end;
    5.63 +
    5.64 +fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)];
    5.65 +
    5.66 +
    5.67 +(* goals *)
    5.68 +
    5.69 +fun goal opt_chain goal stmt int =
    5.70 +  opt_chain #> goal NONE (K Seq.single) stmt int;
    5.71 +
    5.72 +val have = goal I Proof.have;
    5.73 +val hence = goal Proof.chain Proof.have;
    5.74 +val show = goal I Proof.show;
    5.75 +val thus = goal Proof.chain Proof.show;
    5.76 +
    5.77 +
    5.78 +(* local endings *)
    5.79 +
    5.80 +fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
    5.81 +val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
    5.82 +val local_default_proof = Toplevel.proofs Proof.local_default_proof;
    5.83 +val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
    5.84 +val local_done_proof = Toplevel.proofs Proof.local_done_proof;
    5.85 +val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
    5.86 +
    5.87 +val skip_local_qed =
    5.88 +  Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));
    5.89 +
    5.90 +
    5.91 +(* global endings *)
    5.92 +
    5.93 +fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
    5.94 +val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
    5.95 +val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
    5.96 +val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
    5.97 +val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
    5.98 +val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
    5.99 +
   5.100 +val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1);
   5.101 +
   5.102 +
   5.103 +(* common endings *)
   5.104 +
   5.105 +fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
   5.106 +fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
   5.107 +val default_proof = local_default_proof o global_default_proof;
   5.108 +val immediate_proof = local_immediate_proof o global_immediate_proof;
   5.109 +val done_proof = local_done_proof o global_done_proof;
   5.110 +val skip_proof = local_skip_proof o global_skip_proof;
   5.111 +
   5.112 +
   5.113 +(* init and exit *)
   5.114 +
   5.115 +fun begin_theory name imports uses =
   5.116 +  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
   5.117 +
   5.118 +val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory;
   5.119 +
   5.120 +val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
   5.121 +
   5.122 +fun theory (name, imports, uses) =
   5.123 +  Toplevel.init_theory (begin_theory name imports uses)
   5.124 +    (fn thy => (end_theory thy; ()))
   5.125 +    (kill_theory o Context.theory_name);
   5.126 +
   5.127 +fun init_context f x = Toplevel.init_theory
   5.128 +  (fn _ =>
   5.129 +    (case Context.pass NONE f x of
   5.130 +      ((), NONE) => raise Toplevel.UNDEF
   5.131 +    | ((), SOME thy) => thy))
   5.132 +  (K ()) (K ());
   5.133  
   5.134  val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
   5.135 +
   5.136  val welcome = Toplevel.imperative (writeln o Session.welcome);
   5.137  
   5.138  val exit = Toplevel.keep (fn state =>
   5.139 @@ -115,7 +227,7 @@
   5.140  val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
   5.141  fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
   5.142  fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
   5.143 -fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
   5.144 +fun kill_thy name = Toplevel.imperative (fn () => kill_theory name);
   5.145  
   5.146  
   5.147  (* print state *)
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 14 00:15:37 2006 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 14 00:15:38 2006 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4  
     6.5  val theoryP =
     6.6    OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
     6.7 -    (ThyHeader.args >> (Toplevel.print oo IsarThy.theory));
     6.8 +    (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory));
     6.9  
    6.10  val endP =
    6.11    OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    6.12 @@ -174,7 +174,7 @@
    6.13  
    6.14  val axiomsP =
    6.15    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
    6.16 -    (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
    6.17 +    (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
    6.18  
    6.19  val opt_unchecked_overloaded =
    6.20    Scan.optional (P.$$$ "(" |-- P.!!!
    6.21 @@ -184,7 +184,7 @@
    6.22  val defsP =
    6.23    OuterSyntax.command "defs" "define constants" K.thy_decl
    6.24      (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name
    6.25 -      >> (Toplevel.theory o IsarThy.add_defs));
    6.26 +      >> (Toplevel.theory o IsarCmd.add_defs));
    6.27  
    6.28  
    6.29  (* constant definitions and abbreviations *)
    6.30 @@ -399,22 +399,22 @@
    6.31  val haveP =
    6.32    OuterSyntax.command "have" "state local goal"
    6.33      (K.tag_proof K.prf_goal)
    6.34 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.have));
    6.35 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
    6.36  
    6.37  val henceP =
    6.38    OuterSyntax.command "hence" "abbreviates \"then have\""
    6.39      (K.tag_proof K.prf_goal)
    6.40 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.hence));
    6.41 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
    6.42  
    6.43  val showP =
    6.44    OuterSyntax.command "show" "state local goal, solving current obligation"
    6.45      (K.tag_proof K.prf_goal)
    6.46 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show));
    6.47 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
    6.48  
    6.49  val thusP =
    6.50    OuterSyntax.command "thus" "abbreviates \"then show\""
    6.51      (K.tag_proof K.prf_goal)
    6.52 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus));
    6.53 +    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
    6.54  
    6.55  
    6.56  (* facts *)
    6.57 @@ -527,32 +527,32 @@
    6.58  val qedP =
    6.59    OuterSyntax.command "qed" "conclude (sub-)proof"
    6.60      (K.tag_proof K.qed_block)
    6.61 -    (Scan.option P.method >> (Toplevel.print3 oo IsarThy.qed));
    6.62 +    (Scan.option P.method >> (Toplevel.print3 oo IsarCmd.qed));
    6.63  
    6.64  val terminal_proofP =
    6.65    OuterSyntax.command "by" "terminal backward proof"
    6.66      (K.tag_proof K.qed)
    6.67 -    (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarThy.terminal_proof));
    6.68 +    (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarCmd.terminal_proof));
    6.69  
    6.70  val default_proofP =
    6.71    OuterSyntax.command ".." "default proof"
    6.72      (K.tag_proof K.qed)
    6.73 -    (Scan.succeed (Toplevel.print3 o IsarThy.default_proof));
    6.74 +    (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
    6.75  
    6.76  val immediate_proofP =
    6.77    OuterSyntax.command "." "immediate proof"
    6.78      (K.tag_proof K.qed)
    6.79 -    (Scan.succeed (Toplevel.print3 o IsarThy.immediate_proof));
    6.80 +    (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
    6.81  
    6.82  val done_proofP =
    6.83    OuterSyntax.command "done" "done proof"
    6.84      (K.tag_proof K.qed)
    6.85 -    (Scan.succeed (Toplevel.print3 o IsarThy.done_proof));
    6.86 +    (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
    6.87  
    6.88  val skip_proofP =
    6.89    OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
    6.90      (K.tag_proof K.qed)
    6.91 -    (Scan.succeed (Toplevel.print3 o IsarThy.skip_proof));
    6.92 +    (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
    6.93  
    6.94  val forget_proofP =
    6.95    OuterSyntax.command "oops" "forget proof"
     7.1 --- a/src/Pure/proof_general.ML	Tue Nov 14 00:15:37 2006 +0100
     7.2 +++ b/src/Pure/proof_general.ML	Tue Nov 14 00:15:38 2006 +0100
     7.3 @@ -1377,12 +1377,12 @@
     7.4  
     7.5  val context_thy_onlyP =
     7.6    OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
     7.7 -    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
     7.8 +    (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
     7.9  
    7.10  val try_context_thy_onlyP =
    7.11    OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
    7.12      (P.name >> (Toplevel.no_timing oo
    7.13 -      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
    7.14 +      (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
    7.15  
    7.16  val restartP =
    7.17    OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
     8.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Nov 14 00:15:37 2006 +0100
     8.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Nov 14 00:15:38 2006 +0100
     8.3 @@ -396,9 +396,9 @@
     8.4        else read_i sdom;
     8.5    in
     8.6      thy
     8.7 -    |> IsarThy.apply_theorems raw_monos
     8.8 -    ||>> IsarThy.apply_theorems raw_type_intrs
     8.9 -    ||>> IsarThy.apply_theorems raw_type_elims
    8.10 +    |> IsarCmd.apply_theorems raw_monos
    8.11 +    ||>> IsarCmd.apply_theorems raw_type_intrs
    8.12 +    ||>> IsarCmd.apply_theorems raw_type_elims
    8.13      |-> (fn ((monos, type_intrs), type_elims) =>
    8.14            add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
    8.15    end;
     9.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Nov 14 00:15:37 2006 +0100
     9.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Nov 14 00:15:38 2006 +0100
     9.3 @@ -173,10 +173,10 @@
     9.4  
     9.5  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
     9.6    thy
     9.7 -  |> IsarThy.apply_theorems [raw_elim]
     9.8 -  ||>> IsarThy.apply_theorems [raw_induct]
     9.9 -  ||>> IsarThy.apply_theorems raw_case_eqns
    9.10 -  ||>> IsarThy.apply_theorems raw_recursor_eqns
    9.11 +  |> IsarCmd.apply_theorems [raw_elim]
    9.12 +  ||>> IsarCmd.apply_theorems [raw_induct]
    9.13 +  ||>> IsarCmd.apply_theorems raw_case_eqns
    9.14 +  ||>> IsarCmd.apply_theorems raw_recursor_eqns
    9.15    |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
    9.16            rep_datatype_i (PureThy.single_thm "elimination" elims)
    9.17              (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
    10.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Nov 14 00:15:37 2006 +0100
    10.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Nov 14 00:15:38 2006 +0100
    10.3 @@ -567,10 +567,10 @@
    10.4      val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
    10.5    in
    10.6      thy
    10.7 -    |> IsarThy.apply_theorems raw_monos
    10.8 -    ||>> IsarThy.apply_theorems raw_con_defs
    10.9 -    ||>> IsarThy.apply_theorems raw_type_intrs
   10.10 -    ||>> IsarThy.apply_theorems raw_type_elims
   10.11 +    |> IsarCmd.apply_theorems raw_monos
   10.12 +    ||>> IsarCmd.apply_theorems raw_con_defs
   10.13 +    ||>> IsarCmd.apply_theorems raw_type_intrs
   10.14 +    ||>> IsarCmd.apply_theorems raw_type_elims
   10.15      |-> (fn (((monos, con_defs), type_intrs), type_elims) =>
   10.16            add_inductive_i true (rec_tms, dom_sum) intr_specs
   10.17              (monos, con_defs, type_intrs, type_elims))