src/Pure/Isar/proof.ML
changeset 29381 45d77aeb1608
parent 29364 cea7b4034461
child 29383 223f18cfbb32
equal deleted inserted replaced
29380:a9ee3475abf4 29381:45d77aeb1608
   113     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   113     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   114   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   114   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   115     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   115     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   116   val is_relevant: state -> bool
   116   val is_relevant: state -> bool
   117   val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
   117   val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
   118   val future_terminal_proof: Method.text * Method.text option -> state -> context
   118   val future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
   119 end;
   119 end;
   120 
   120 
   121 structure Proof: PROOF =
   121 structure Proof: PROOF =
   122 struct
   122 struct
   123 
   123 
   991 
   991 
   992 in
   992 in
   993 
   993 
   994 fun is_relevant state =
   994 fun is_relevant state =
   995   can (assert_bottom false) state orelse
   995   can (assert_bottom false) state orelse
   996   can assert_forward state orelse
       
   997   not (is_original state) orelse
   996   not (is_original state) orelse
   998   schematic_goal state;
   997   schematic_goal state;
   999 
   998 
  1000 fun future_proof fork_proof state =
   999 fun future_proof fork_proof state =
  1001   let
  1000   let
  1002     val _ = is_relevant state andalso error "Cannot fork relevant proof";
  1001     val _ = is_relevant state andalso error "Cannot fork relevant proof";
  1003 
  1002 
       
  1003     val _ = assert_backward state;
  1004     val (goal_ctxt, (_, goal)) = find_goal state;
  1004     val (goal_ctxt, (_, goal)) = find_goal state;
  1005     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
  1005     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
  1006 
  1006 
  1007     val prop' = Logic.protect prop;
  1007     val prop' = Logic.protect prop;
  1008     val statement' = (kind, [[], [prop']], prop');
  1008     val statement' = (kind, [[], [prop']], prop');
  1026       |> global_done_proof;
  1026       |> global_done_proof;
  1027   in (Future.map #1 result_ctxt, state') end;
  1027   in (Future.map #1 result_ctxt, state') end;
  1028 
  1028 
  1029 end;
  1029 end;
  1030 
  1030 
  1031 fun future_terminal_proof meths state =
  1031 fun future_terminal_proof meths int state =
  1032   if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
  1032   if int orelse is_relevant state orelse not (Future.enabled ())
       
  1033   then global_terminal_proof meths state
  1033   else #2 (state |> future_proof (fn state' =>
  1034   else #2 (state |> future_proof (fn state' =>
  1034     Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
  1035     Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
  1035 
  1036 
  1036 end;
  1037 end;
  1037 
  1038