added 'obtain' command;
authorwenzelm
Fri Oct 01 20:38:50 1999 +0200 (1999-10-01 ago)
changeset 7678027b6ec2f084
parent 7677 de2e468a42c8
child 7679 99912beb8fa0
added 'obtain' command;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Oct 01 20:38:16 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 01 20:38:50 1999 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4      (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
     1.5  
     1.6  val thenceP =
     1.7 -  OuterSyntax.command "thence" "forward chaining, including full export" K.prf_chain
     1.8 +  OuterSyntax.command "thence" "forward chaining, including full export (EXPERIMENTAL!)" K.prf_chain
     1.9      (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.export_chain)));
    1.10  
    1.11  val fromP =
    1.12 @@ -399,6 +399,18 @@
    1.13      (calc_args -- P.marg_comment >> IsarThy.finally);
    1.14  
    1.15  
    1.16 +(* obtain *)
    1.17 +
    1.18 +val obtainP =
    1.19 +  OuterSyntax.command "obtain" "document-level existential quantifier (EXPERIMENTAL!)"
    1.20 +    K.prf_asm_goal
    1.21 +    (Scan.optional
    1.22 +      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
    1.23 +        --| P.$$$ "in") [] --
    1.24 +      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
    1.25 +    >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
    1.26 +
    1.27 +
    1.28  (* proof navigation *)
    1.29  
    1.30  val backP =
    1.31 @@ -581,8 +593,8 @@
    1.32  val keywords =
    1.33   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
    1.34    "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
    1.35 -  "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
    1.36 -  "}"];
    1.37 +  "concl", "files", "in", "infixl", "infixr", "is", "output", "{",
    1.38 +  "|", "}"];
    1.39  
    1.40  val parsers = [
    1.41    (*theory structure*)
    1.42 @@ -601,8 +613,8 @@
    1.43    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.44    defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
    1.45    nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    1.46 -  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
    1.47 -  cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    1.48 +  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, obtainP,
    1.49 +  backP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    1.50    (*diagnostic commands*)
    1.51    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.52    print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:16 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Oct 01 20:38:50 1999 +0200
     2.3 @@ -135,6 +135,12 @@
     2.4      -> Toplevel.transition -> Toplevel.transition
     2.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     2.6      -> Toplevel.transition -> Toplevel.transition
     2.7 +  val obtain: ((string list * string option) * Comment.text) list
     2.8 +    * ((string * Args.src list * (string * (string list * string list)) list)
     2.9 +      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    2.10 +  val obtain_i: ((string list * typ option) * Comment.text) list
    2.11 +    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    2.12 +      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    2.13    val use_mltext: string -> bool -> theory option -> unit
    2.14    val use_mltext_theory: string -> bool -> theory -> theory
    2.15    val use_setup: string -> theory -> theory
    2.16 @@ -281,6 +287,9 @@
    2.17  
    2.18  (* statements *)
    2.19  
    2.20 +fun multi_local_attribute state (name, src, s) =
    2.21 +  (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s);
    2.22 +
    2.23  local
    2.24  
    2.25  fun global_statement f (name, src, s) int thy =
    2.26 @@ -296,8 +305,7 @@
    2.27  fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
    2.28  
    2.29  fun multi_statement f args = ProofHistory.apply (fn state =>
    2.30 -  f (map (fn (name, src, s) =>
    2.31 -      (name, map (Attrib.local_attribute (Proof.theory_of state)) src, s)) args) state);
    2.32 +  f (map (multi_local_attribute state) args) state);
    2.33  
    2.34  fun multi_statement_i f args = ProofHistory.apply (f args);
    2.35  
    2.36 @@ -433,6 +441,17 @@
    2.37  end;
    2.38  
    2.39  
    2.40 +(* obtain *)
    2.41 +
    2.42 +fun obtain (xs, asms) = ProofHistory.applys (fn state =>
    2.43 +  Obtain.obtain (map Comment.ignore xs)
    2.44 +    (map (multi_local_attribute state o Comment.ignore) asms) state);
    2.45 +
    2.46 +fun obtain_i (xs, asms) = ProofHistory.applys
    2.47 +  (Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
    2.48 +
    2.49 +
    2.50 +
    2.51  (* use ML text *)
    2.52  
    2.53  fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;