added check_result;
authorwenzelm
Thu Jul 01 17:40:48 1999 +0200 (1999-07-01)
changeset 687101866edde713
parent 6870 43d64c520d11
child 6872 b250da153b1e
added check_result;
setmp Display.show_hyps false;
fixed auto_bind_facts;
tuned finish_proof;
fixed backtracking of global_qed;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 01 17:38:44 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 01 17:40:48 1999 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    type context
     1.5    type state
     1.6    exception STATE of string * state
     1.7 +  val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
     1.8    val context_of: state -> context
     1.9    val theory_of: state -> theory
    1.10    val sign_of: state -> Sign.sg
    1.11 @@ -55,7 +56,7 @@
    1.12    val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    1.13      -> state -> state Seq.seq
    1.14    val global_qed: (state -> state Seq.seq) -> bstring option
    1.15 -    -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
    1.16 +    -> theory attribute list option -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    1.17  end;
    1.18  
    1.19  signature PROOF_PRIVATE =
    1.20 @@ -127,6 +128,11 @@
    1.21  fun err_malformed name state =
    1.22    raise STATE (name ^ ": internal error -- malformed proof state", state);
    1.23  
    1.24 +fun check_result msg state sq =
    1.25 +  (case Seq.pull sq of
    1.26 +    None => raise STATE (msg, state)
    1.27 +  | Some s_sq => Seq.cons s_sq);
    1.28 +
    1.29  
    1.30  fun map_current f (State ({context, facts, mode, goal}, nodes)) =
    1.31    State (make_node (f (context, facts, mode, goal)), nodes);
    1.32 @@ -256,8 +262,8 @@
    1.33  val verbose = ProofContext.verbose;
    1.34  
    1.35  fun print_facts _ None = ()
    1.36 -  | print_facts s (Some ths) =
    1.37 -      Pretty.writeln (Pretty.big_list (s ^ " facts:") (map Display.pretty_thm ths));
    1.38 +  | print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:")
    1.39 +      (map (setmp Display.show_hyps false Display.pretty_thm) ths));
    1.40  
    1.41  fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
    1.42    let
    1.43 @@ -370,7 +376,7 @@
    1.44        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
    1.45  (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
    1.46        err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
    1.47 -    else (thm, prop)
    1.48 +    else thm
    1.49    end;
    1.50  
    1.51  
    1.52 @@ -578,19 +584,12 @@
    1.53  
    1.54  (* finish proof *)
    1.55  
    1.56 -fun check_finished state states =
    1.57 -  (case Seq.pull states of
    1.58 -    None => raise STATE ("Failed to finish proof", state)
    1.59 -  | Some s_sq => Seq.cons s_sq);
    1.60 -
    1.61 -fun finish_proof bot finalize state =
    1.62 +fun finish_proof bot state =
    1.63    state
    1.64    |> assert_forward
    1.65    |> close_block
    1.66    |> assert_bottom bot
    1.67 -  |> assert_current_goal true
    1.68 -  |> finalize
    1.69 -  |> check_finished state;
    1.70 +  |> assert_current_goal true;
    1.71  
    1.72  
    1.73  (* end_block *)
    1.74 @@ -609,7 +608,7 @@
    1.75  fun finish_local print_result state =
    1.76    let
    1.77      val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
    1.78 -    val (result, result_prop) = prep_result state asms t raw_thm;
    1.79 +    val result = prep_result state asms t raw_thm;
    1.80      val (atts, opt_solve) =
    1.81        (case kind of
    1.82          Goal atts => (atts, solve_goal result tacs)
    1.83 @@ -619,14 +618,15 @@
    1.84      print_result {kind = kind_name kind, name = name, thm = result};
    1.85      state
    1.86      |> close_block
    1.87 -    |> auto_bind_facts name [result_prop]
    1.88 +    |> auto_bind_facts name [t]
    1.89      |> have_thmss name atts [Thm.no_attributes [result]]
    1.90      |> opt_solve
    1.91    end;
    1.92  
    1.93  fun local_qed finalize print_result state =
    1.94    state
    1.95 -  |> finish_proof false finalize
    1.96 +  |> finish_proof false
    1.97 +  |> finalize
    1.98    |> (Seq.flat o Seq.map (finish_local print_result));
    1.99  
   1.100  
   1.101 @@ -635,7 +635,7 @@
   1.102  fun finish_global alt_name alt_atts state =
   1.103    let
   1.104      val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
   1.105 -    val result = final_result state (#1 (prep_result state asms t raw_thm));
   1.106 +    val result = final_result state (prep_result state asms t raw_thm);
   1.107  
   1.108      val name = if_none alt_name def_name;
   1.109      val atts =
   1.110 @@ -647,11 +647,12 @@
   1.111      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   1.112    in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
   1.113  
   1.114 +(*Note: should inspect first result only, backtracking may destroy theory*)
   1.115  fun global_qed finalize alt_name alt_atts state =
   1.116    state
   1.117 -  |> finish_proof true finalize
   1.118 -  |> Seq.hd
   1.119 -  |> finish_global alt_name alt_atts;
   1.120 +  |> finish_proof true
   1.121 +  |> finalize
   1.122 +  |> Seq.map (finish_global alt_name alt_atts);
   1.123  
   1.124  
   1.125  end;