src/Pure/Isar/proof.ML
changeset 6871 01866edde713
parent 6853 80f88b762816
child 6876 4ae9c47f2b6b
equal deleted inserted replaced
6870:43d64c520d11 6871:01866edde713
     8 signature PROOF =
     8 signature PROOF =
     9 sig
     9 sig
    10   type context
    10   type context
    11   type state
    11   type state
    12   exception STATE of string * state
    12   exception STATE of string * state
       
    13   val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
    13   val context_of: state -> context
    14   val context_of: state -> context
    14   val theory_of: state -> theory
    15   val theory_of: state -> theory
    15   val sign_of: state -> Sign.sg
    16   val sign_of: state -> Sign.sg
    16   val the_facts: state -> thm list
    17   val the_facts: state -> thm list
    17   val the_fact: state -> thm
    18   val the_fact: state -> thm
    53   val end_block: state -> state
    54   val end_block: state -> state
    54   val at_bottom: state -> bool
    55   val at_bottom: state -> bool
    55   val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    56   val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    56     -> state -> state Seq.seq
    57     -> state -> state Seq.seq
    57   val global_qed: (state -> state Seq.seq) -> bstring option
    58   val global_qed: (state -> state Seq.seq) -> bstring option
    58     -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
    59     -> theory attribute list option -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    59 end;
    60 end;
    60 
    61 
    61 signature PROOF_PRIVATE =
    62 signature PROOF_PRIVATE =
    62 sig
    63 sig
    63   include PROOF
    64   include PROOF
   125 exception STATE of string * state;
   126 exception STATE of string * state;
   126 
   127 
   127 fun err_malformed name state =
   128 fun err_malformed name state =
   128   raise STATE (name ^ ": internal error -- malformed proof state", state);
   129   raise STATE (name ^ ": internal error -- malformed proof state", state);
   129 
   130 
       
   131 fun check_result msg state sq =
       
   132   (case Seq.pull sq of
       
   133     None => raise STATE (msg, state)
       
   134   | Some s_sq => Seq.cons s_sq);
       
   135 
   130 
   136 
   131 fun map_current f (State ({context, facts, mode, goal}, nodes)) =
   137 fun map_current f (State ({context, facts, mode, goal}, nodes)) =
   132   State (make_node (f (context, facts, mode, goal)), nodes);
   138   State (make_node (f (context, facts, mode, goal)), nodes);
   133 
   139 
   134 fun init_state thy =
   140 fun init_state thy =
   254 (** print_state **)
   260 (** print_state **)
   255 
   261 
   256 val verbose = ProofContext.verbose;
   262 val verbose = ProofContext.verbose;
   257 
   263 
   258 fun print_facts _ None = ()
   264 fun print_facts _ None = ()
   259   | print_facts s (Some ths) =
   265   | print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:")
   260       Pretty.writeln (Pretty.big_list (s ^ " facts:") (map Display.pretty_thm ths));
   266       (map (setmp Display.show_hyps false Display.pretty_thm) ths));
   261 
   267 
   262 fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   268 fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   263   let
   269   let
   264     val ref (_, _, begin_goal) = Goals.current_goals_markers;
   270     val ref (_, _, begin_goal) = Goals.current_goals_markers;
   265 
   271 
   368 *)
   374 *)
   369     if not (null hyps) then
   375     if not (null hyps) then
   370       err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
   376       err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
   371 (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
   377 (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
   372       err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
   378       err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
   373     else (thm, prop)
   379     else thm
   374   end;
   380   end;
   375 
   381 
   376 
   382 
   377 (* prepare final result *)
   383 (* prepare final result *)
   378 
   384 
   576 val at_bottom = can (assert_bottom true o close_block);
   582 val at_bottom = can (assert_bottom true o close_block);
   577 
   583 
   578 
   584 
   579 (* finish proof *)
   585 (* finish proof *)
   580 
   586 
   581 fun check_finished state states =
   587 fun finish_proof bot state =
   582   (case Seq.pull states of
       
   583     None => raise STATE ("Failed to finish proof", state)
       
   584   | Some s_sq => Seq.cons s_sq);
       
   585 
       
   586 fun finish_proof bot finalize state =
       
   587   state
   588   state
   588   |> assert_forward
   589   |> assert_forward
   589   |> close_block
   590   |> close_block
   590   |> assert_bottom bot
   591   |> assert_bottom bot
   591   |> assert_current_goal true
   592   |> assert_current_goal true;
   592   |> finalize
       
   593   |> check_finished state;
       
   594 
   593 
   595 
   594 
   596 (* end_block *)
   595 (* end_block *)
   597 
   596 
   598 fun end_block state =
   597 fun end_block state =
   607 (* local_qed *)
   606 (* local_qed *)
   608 
   607 
   609 fun finish_local print_result state =
   608 fun finish_local print_result state =
   610   let
   609   let
   611     val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
   610     val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
   612     val (result, result_prop) = prep_result state asms t raw_thm;
   611     val result = prep_result state asms t raw_thm;
   613     val (atts, opt_solve) =
   612     val (atts, opt_solve) =
   614       (case kind of
   613       (case kind of
   615         Goal atts => (atts, solve_goal result tacs)
   614         Goal atts => (atts, solve_goal result tacs)
   616       | Aux atts => (atts, Seq.single)
   615       | Aux atts => (atts, Seq.single)
   617       | _ => raise STATE ("No local goal!", state));
   616       | _ => raise STATE ("No local goal!", state));
   618   in
   617   in
   619     print_result {kind = kind_name kind, name = name, thm = result};
   618     print_result {kind = kind_name kind, name = name, thm = result};
   620     state
   619     state
   621     |> close_block
   620     |> close_block
   622     |> auto_bind_facts name [result_prop]
   621     |> auto_bind_facts name [t]
   623     |> have_thmss name atts [Thm.no_attributes [result]]
   622     |> have_thmss name atts [Thm.no_attributes [result]]
   624     |> opt_solve
   623     |> opt_solve
   625   end;
   624   end;
   626 
   625 
   627 fun local_qed finalize print_result state =
   626 fun local_qed finalize print_result state =
   628   state
   627   state
   629   |> finish_proof false finalize
   628   |> finish_proof false
       
   629   |> finalize
   630   |> (Seq.flat o Seq.map (finish_local print_result));
   630   |> (Seq.flat o Seq.map (finish_local print_result));
   631 
   631 
   632 
   632 
   633 (* global_qed *)
   633 (* global_qed *)
   634 
   634 
   635 fun finish_global alt_name alt_atts state =
   635 fun finish_global alt_name alt_atts state =
   636   let
   636   let
   637     val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
   637     val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
   638     val result = final_result state (#1 (prep_result state asms t raw_thm));
   638     val result = final_result state (prep_result state asms t raw_thm);
   639 
   639 
   640     val name = if_none alt_name def_name;
   640     val name = if_none alt_name def_name;
   641     val atts =
   641     val atts =
   642       (case kind of
   642       (case kind of
   643         Theorem atts => if_none alt_atts atts
   643         Theorem atts => if_none alt_atts atts
   645       | _ => raise STATE ("No global goal!", state));
   645       | _ => raise STATE ("No global goal!", state));
   646 
   646 
   647     val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   647     val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   648   in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
   648   in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
   649 
   649 
       
   650 (*Note: should inspect first result only, backtracking may destroy theory*)
   650 fun global_qed finalize alt_name alt_atts state =
   651 fun global_qed finalize alt_name alt_atts state =
   651   state
   652   state
   652   |> finish_proof true finalize
   653   |> finish_proof true
   653   |> Seq.hd
   654   |> finalize
   654   |> finish_global alt_name alt_atts;
   655   |> Seq.map (finish_global alt_name alt_atts);
   655 
   656 
   656 
   657 
   657 end;
   658 end;