qed/after_qed: singleton result;
authorwenzelm
Wed Jan 07 16:22:10 2009 +0100 (2009-01-07)
changeset 29383223f18cfbb32
parent 29382 9f6e2658a868
child 29384 a3c7e9ae9b71
qed/after_qed: singleton result;
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/old_locale.ML
src/Pure/Isar/proof.ML
src/Pure/Tools/invoke.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Jan 07 12:10:22 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Jan 07 16:22:10 2009 +0100
     1.3 @@ -887,7 +887,7 @@
     1.4        end;
     1.5  
     1.6      fun after_qed results =
     1.7 -      Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
     1.8 +      Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
     1.9    in
    1.10      state |> Proof.map_context (K goal_ctxt) |>
    1.11        Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 07 12:10:22 2009 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 07 16:22:10 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      Pure/Isar/isar_cmd.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Markus Wenzel, TU Muenchen
     2.7  
     2.8  Derived Isar commands.
     2.9 @@ -219,7 +218,7 @@
    2.10  (* goals *)
    2.11  
    2.12  fun goal opt_chain goal stmt int =
    2.13 -  opt_chain #> goal NONE (K Seq.single) stmt int;
    2.14 +  opt_chain #> goal NONE (K I) stmt int;
    2.15  
    2.16  val have = goal I Proof.have;
    2.17  val hence = goal Proof.chain Proof.have;
    2.18 @@ -229,12 +228,12 @@
    2.19  
    2.20  (* local endings *)
    2.21  
    2.22 -fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
    2.23 -val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
    2.24 -val local_default_proof = Toplevel.proofs Proof.local_default_proof;
    2.25 -val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
    2.26 -val local_done_proof = Toplevel.proofs Proof.local_done_proof;
    2.27 -val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
    2.28 +fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
    2.29 +val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
    2.30 +val local_default_proof = Toplevel.proof Proof.local_default_proof;
    2.31 +val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
    2.32 +val local_done_proof = Toplevel.proof Proof.local_done_proof;
    2.33 +val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
    2.34  
    2.35  val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
    2.36  
     3.1 --- a/src/Pure/Isar/obtain.ML	Wed Jan 07 12:10:22 2009 +0100
     3.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jan 07 16:22:10 2009 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      Pure/Isar/obtain.ML
     3.5 -    ID:         $Id$
     3.6      Author:     Markus Wenzel, TU Muenchen
     3.7  
     3.8  The 'obtain' and 'guess' language elements -- generalized existence at
     3.9 @@ -150,13 +149,13 @@
    3.10  
    3.11      fun after_qed _ =
    3.12        Proof.local_qed (NONE, false)
    3.13 -      #> Seq.map (`Proof.the_fact #-> (fn rule =>
    3.14 +      #> `Proof.the_fact #-> (fn rule =>
    3.15          Proof.fix_i vars
    3.16 -        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
    3.17 +        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
    3.18    in
    3.19      state
    3.20      |> Proof.enter_forward
    3.21 -    |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
    3.22 +    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
    3.23      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    3.24      |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
    3.25      |> Proof.assume_i
    3.26 @@ -306,7 +305,7 @@
    3.27      val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
    3.28          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
    3.29      fun after_qed [[_, res]] =
    3.30 -      Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
    3.31 +      Proof.end_block #> guess_context (check_result ctxt thesis res);
    3.32    in
    3.33      state
    3.34      |> Proof.enter_forward
     4.1 --- a/src/Pure/Isar/old_locale.ML	Wed Jan 07 12:10:22 2009 +0100
     4.2 +++ b/src/Pure/Isar/old_locale.ML	Wed Jan 07 16:22:10 2009 +0100
     4.3 @@ -116,7 +116,7 @@
     4.4      theory -> Proof.state
     4.5    val interpretation_in_locale: (Proof.context -> Proof.context) ->
     4.6      xstring * expr -> theory -> Proof.state
     4.7 -  val interpret: (Proof.state -> Proof.state Seq.seq) ->
     4.8 +  val interpret: (Proof.state -> Proof.state) ->
     4.9      (Binding.T -> Binding.T) -> expr ->
    4.10      term option list * (Attrib.binding * term) list ->
    4.11      bool -> Proof.state ->
    4.12 @@ -2478,7 +2478,7 @@
    4.13  
    4.14  val interpret = gen_interpret prep_local_registration;
    4.15  fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
    4.16 -  Seq.single (standard_name_morph interp_prfx);
    4.17 +  I (standard_name_morph interp_prfx);
    4.18  
    4.19  end;
    4.20  
     5.1 --- a/src/Pure/Isar/proof.ML	Wed Jan 07 12:10:22 2009 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Wed Jan 07 16:22:10 2009 +0100
     5.3 @@ -87,31 +87,31 @@
     5.4    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     5.5      (theory -> 'a -> attribute) ->
     5.6      (context * 'b list -> context * (term list list * (context -> context))) ->
     5.7 -    string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
     5.8 +    string -> Method.text option -> (thm list list -> state -> state) ->
     5.9      ((Binding.T * 'a list) * 'b) list -> state -> state
    5.10 -  val local_qed: Method.text option * bool -> state -> state Seq.seq
    5.11 +  val local_qed: Method.text option * bool -> state -> state
    5.12    val theorem: Method.text option -> (thm list list -> context -> context) ->
    5.13      (string * string list) list list -> context -> state
    5.14    val theorem_i: Method.text option -> (thm list list -> context -> context) ->
    5.15      (term * term list) list list -> context -> state
    5.16    val global_qed: Method.text option * bool -> state -> context
    5.17 -  val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
    5.18 -  val local_default_proof: state -> state Seq.seq
    5.19 -  val local_immediate_proof: state -> state Seq.seq
    5.20 -  val local_done_proof: state -> state Seq.seq
    5.21 -  val local_skip_proof: bool -> state -> state Seq.seq
    5.22 +  val local_terminal_proof: Method.text * Method.text option -> state -> state
    5.23 +  val local_default_proof: state -> state
    5.24 +  val local_immediate_proof: state -> state
    5.25 +  val local_skip_proof: bool -> state -> state
    5.26 +  val local_done_proof: state -> state
    5.27    val global_terminal_proof: Method.text * Method.text option -> state -> context
    5.28    val global_default_proof: state -> context
    5.29    val global_immediate_proof: state -> context
    5.30 +  val global_skip_proof: bool -> state -> context
    5.31    val global_done_proof: state -> context
    5.32 -  val global_skip_proof: bool -> state -> context
    5.33 -  val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    5.34 +  val have: Method.text option -> (thm list list -> state -> state) ->
    5.35      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
    5.36 -  val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    5.37 +  val have_i: Method.text option -> (thm list list -> state -> state) ->
    5.38      ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
    5.39 -  val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    5.40 +  val show: Method.text option -> (thm list list -> state -> state) ->
    5.41      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
    5.42 -  val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
    5.43 +  val show_i: Method.text option -> (thm list list -> state -> state) ->
    5.44      ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
    5.45    val is_relevant: state -> bool
    5.46    val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
    5.47 @@ -148,7 +148,7 @@
    5.48      goal: thm,                            (*subgoals ==> statement*)
    5.49      before_qed: Method.text option,
    5.50      after_qed:
    5.51 -      (thm list list -> state -> state Seq.seq) *
    5.52 +      (thm list list -> state -> state) *
    5.53        (thm list list -> context -> context)};
    5.54  
    5.55  fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
    5.56 @@ -347,8 +347,7 @@
    5.57        (case filter_out (fn s => s = "") strs of [] => ""
    5.58        | strs' => enclose " (" ")" (commas strs'));
    5.59  
    5.60 -    fun prt_goal (SOME (ctxt, (i,
    5.61 -            {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
    5.62 +    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) =
    5.63            pretty_facts "using " ctxt
    5.64              (if mode <> Backward orelse null using then NONE else SOME using) @
    5.65            [Pretty.str ("goal" ^
    5.66 @@ -751,6 +750,13 @@
    5.67    |> `before_qed |-> (refine o the_default Method.succeed_text)
    5.68    |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
    5.69  
    5.70 +fun check_result msg sq =
    5.71 +  (case Seq.pull sq of
    5.72 +    NONE => error msg
    5.73 +  | SOME (s, _) => s);
    5.74 +
    5.75 +fun check_finish sq = check_result "Failed to finish proof" sq;
    5.76 +
    5.77  
    5.78  (* unstructured refinement *)
    5.79  
    5.80 @@ -842,7 +848,7 @@
    5.81        |> burrow (ProofContext.export goal_ctxt outer_ctxt);
    5.82  
    5.83      val (after_local, after_global) = after_qed;
    5.84 -    fun after_local' x y = Position.setmp_thread_data_seq pos (fn () => after_local x y) ();
    5.85 +    fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
    5.86      fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
    5.87    in
    5.88      outer_state
    5.89 @@ -871,61 +877,47 @@
    5.90      |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
    5.91    end;
    5.92  
    5.93 -fun local_qed txt =
    5.94 -  end_proof false txt #>
    5.95 -  Seq.maps (generic_qed ProofContext.auto_bind_facts #->
    5.96 +fun local_qeds txt =
    5.97 +  end_proof false txt
    5.98 +  #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
    5.99      (fn ((after_qed, _), results) => after_qed results));
   5.100  
   5.101 +fun local_qed txt = local_qeds txt #> check_finish;
   5.102 +
   5.103  
   5.104  (* global goals *)
   5.105  
   5.106  fun global_goal prepp before_qed after_qed propp ctxt =
   5.107    init ctxt
   5.108 -  |> generic_goal (prepp #> ProofContext.auto_fixes) ""
   5.109 -    before_qed (K Seq.single, after_qed) propp;
   5.110 +  |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
   5.111  
   5.112  val theorem = global_goal ProofContext.bind_propp_schematic;
   5.113  val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
   5.114  
   5.115 -fun check_result msg sq =
   5.116 -  (case Seq.pull sq of
   5.117 -    NONE => error msg
   5.118 -  | SOME (s', sq') => Seq.cons s' sq');
   5.119 -
   5.120  fun global_qeds txt =
   5.121    end_proof true txt
   5.122    #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
   5.123 -    after_qed results (context_of state)))
   5.124 -  |> Seq.DETERM;   (*backtracking may destroy theory!*)
   5.125 +    after_qed results (context_of state)));
   5.126  
   5.127 -fun global_qed txt =
   5.128 -  global_qeds txt
   5.129 -  #> check_result "Failed to finish proof"
   5.130 -  #> Seq.hd;
   5.131 +fun global_qed txt = global_qeds txt #> check_finish;
   5.132  
   5.133  
   5.134  (* concluding steps *)
   5.135  
   5.136 -fun local_terminal_proof (text, opt_text) =
   5.137 -  proof (SOME text) #> Seq.maps (local_qed (opt_text, true));
   5.138 +fun terminal_proof qed initial terminal =
   5.139 +  proof (SOME initial) #> Seq.maps (qed terminal) #> check_finish;
   5.140  
   5.141 +fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
   5.142  val local_default_proof = local_terminal_proof (Method.default_text, NONE);
   5.143  val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
   5.144 -val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
   5.145  fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
   5.146 +val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
   5.147  
   5.148 -fun global_term_proof immed (text, opt_text) =
   5.149 -  proof (SOME text)
   5.150 -  #> check_result "Terminal proof method failed"
   5.151 -  #> Seq.maps (global_qeds (opt_text, immed))
   5.152 -  #> check_result "Failed to finish proof (after successful terminal method)"
   5.153 -  #> Seq.hd;
   5.154 -
   5.155 -val global_terminal_proof = global_term_proof true;
   5.156 +fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
   5.157  val global_default_proof = global_terminal_proof (Method.default_text, NONE);
   5.158  val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
   5.159 -val global_done_proof = global_term_proof false (Method.done_text, NONE);
   5.160  fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
   5.161 +val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
   5.162  
   5.163  
   5.164  (* common goal statements *)
   5.165 @@ -940,7 +932,7 @@
   5.166      val testing = ref false;
   5.167      val rule = ref (NONE: thm option);
   5.168      fun fail_msg ctxt =
   5.169 -      "Local statement will fail to solve any pending goal" ::
   5.170 +      "Local statement will fail to refine any pending goal" ::
   5.171        (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
   5.172        |> cat_lines;
   5.173  
   5.174 @@ -951,13 +943,14 @@
   5.175        else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
   5.176        else ();
   5.177      val test_proof =
   5.178 -      (Seq.pull oo local_skip_proof) true
   5.179 +      try (local_skip_proof true)
   5.180        |> setmp_noncritical testing true
   5.181        |> Exn.capture;
   5.182  
   5.183      fun after_qed' results =
   5.184        refine_goals print_rule (context_of state) (flat results)
   5.185 -      #> Seq.maps (after_qed results);
   5.186 +      #> check_result "Failed to refine any pending goal"
   5.187 +      #> after_qed results;
   5.188    in
   5.189      state
   5.190      |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
   5.191 @@ -998,12 +991,12 @@
   5.192  
   5.193  fun future_proof fork_proof state =
   5.194    let
   5.195 -    val _ = is_relevant state andalso error "Cannot fork relevant proof";
   5.196 -
   5.197      val _ = assert_backward state;
   5.198      val (goal_ctxt, (_, goal)) = find_goal state;
   5.199      val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
   5.200  
   5.201 +    val _ = is_relevant state andalso error "Cannot fork relevant proof";
   5.202 +
   5.203      val prop' = Logic.protect prop;
   5.204      val statement' = (kind, [[], [prop']], prop');
   5.205      val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
     6.1 --- a/src/Pure/Tools/invoke.ML	Wed Jan 07 12:10:22 2009 +0100
     6.2 +++ b/src/Pure/Tools/invoke.ML	Wed Jan 07 16:22:10 2009 +0100
     6.3 @@ -88,7 +88,7 @@
     6.4            |> (snd o ProofContext.note_thmss_i "" notes)
     6.5            |> ProofContext.restore_naming ctxt
     6.6          end) #>
     6.7 -      Proof.put_facts NONE #> Seq.single;
     6.8 +      Proof.put_facts NONE;
     6.9    in
    6.10      state'
    6.11      |> Proof.chain_facts chain_facts