src/Pure/Isar/proof.ML
changeset 6404 2daaf2943c79
parent 6262 0ebfcf181d84
child 6529 0f4c2ebc5018
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 18 16:44:53 1999 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 19 11:24:00 1999 +0100
     1.3 @@ -55,9 +55,11 @@
     1.4    val have_i: string -> context attribute list -> term * term list -> state -> state
     1.5    val begin_block: state -> state
     1.6    val next_block: state -> state
     1.7 -  val end_block: (context -> method) -> state -> state Seq.seq
     1.8 -  val qed: (context -> method) -> bstring option -> theory attribute list option -> state
     1.9 -    -> theory * (string * string * thm)
    1.10 +  val end_block: state -> state
    1.11 +  val at_bottom: state -> bool
    1.12 +  val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
    1.13 +  val global_qed: (state -> state Seq.seq) -> bstring option
    1.14 +    -> theory attribute list option -> state -> theory * (string * string * thm)
    1.15  end;
    1.16  
    1.17  signature PROOF_PRIVATE =
    1.18 @@ -555,7 +557,11 @@
    1.19  fun current_goal (State ({goal = Some goal, ...}, _)) = goal
    1.20    | current_goal state = raise STATE ("No current goal!", state);
    1.21  
    1.22 -fun assert_current_goal state = (current_goal state; state);
    1.23 +fun assert_current_goal true (state as State ({goal = None, ...}, _)) =
    1.24 +      raise STATE ("No goal in this block!", state)
    1.25 +  | assert_current_goal false (state as State ({goal = Some _, ...}, _)) =
    1.26 +      raise STATE ("Goal present in this block!", state)
    1.27 +  | assert_current_goal _ state = state;
    1.28  
    1.29  fun assert_bottom true (state as State (_, _ :: _)) =
    1.30        raise STATE ("Not at bottom of proof!", state)
    1.31 @@ -563,6 +569,8 @@
    1.32        raise STATE ("Already at bottom of proof!", state)
    1.33    | assert_bottom _ state = state;
    1.34  
    1.35 +val at_bottom = can (assert_bottom true o close_block);
    1.36 +
    1.37  
    1.38  (* finish proof *)
    1.39  
    1.40 @@ -571,17 +579,28 @@
    1.41      None => raise STATE ("Failed to finish proof", state)
    1.42    | Some s_sq => Seq.cons s_sq);
    1.43  
    1.44 -fun finish_proof bot meth_fun state =
    1.45 +fun finish_proof bot finalize state =
    1.46    state
    1.47    |> assert_forward
    1.48    |> close_block
    1.49    |> assert_bottom bot
    1.50 -  |> assert_current_goal
    1.51 -  |> refine meth_fun
    1.52 +  |> assert_current_goal true
    1.53 +  |> finalize
    1.54    |> check_finished state;
    1.55  
    1.56  
    1.57 -(* conclude local proof *)
    1.58 +(* end_block *)
    1.59 +
    1.60 +fun end_block state =
    1.61 +  state
    1.62 +  |> assert_forward
    1.63 +  |> close_block
    1.64 +  |> assert_current_goal false
    1.65 +  |> close_block
    1.66 +  |> fetch_facts state;
    1.67 +
    1.68 +
    1.69 +(* local_qed *)
    1.70  
    1.71  fun finish_local state =
    1.72    let
    1.73 @@ -599,21 +618,13 @@
    1.74      |> opt_solve
    1.75    end;
    1.76  
    1.77 -fun end_block meth_fun state =
    1.78 -  if can assert_current_goal (close_block state) then
    1.79 -    state
    1.80 -    |> finish_proof false meth_fun
    1.81 -    |> (Seq.flat o Seq.map finish_local)
    1.82 -  else
    1.83 -    state
    1.84 -    |> assert_forward
    1.85 -    |> close_block
    1.86 -    |> close_block
    1.87 -    |> fetch_facts state
    1.88 -    |> Seq.single;
    1.89 +fun local_qed finalize state =
    1.90 +  state
    1.91 +  |> finish_proof false finalize
    1.92 +  |> (Seq.flat o Seq.map finish_local);
    1.93  
    1.94  
    1.95 -(* conclude global proof *)
    1.96 +(* global_qed *)
    1.97  
    1.98  fun finish_global alt_name alt_atts state =
    1.99    let
   1.100 @@ -630,9 +641,9 @@
   1.101      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   1.102    in (thy', (kind_name kind, name, result')) end;
   1.103  
   1.104 -fun qed meth_fun alt_name alt_atts state =
   1.105 +fun global_qed finalize alt_name alt_atts state =
   1.106    state
   1.107 -  |> finish_proof true meth_fun
   1.108 +  |> finish_proof true finalize
   1.109    |> Seq.hd
   1.110    |> finish_global alt_name alt_atts;
   1.111