src/Pure/Isar/proof.ML
changeset 67157 d0657c8b7616
parent 67119 acb0807ddb56
child 67161 b762ed417ed9
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Dec 03 13:22:09 2017 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 07 19:36:48 2017 +0100
     1.3 @@ -106,6 +106,8 @@
     1.4    val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
     1.5      (string * string list) list list -> context -> state
     1.6    val global_qed: Method.text_range option * bool -> state -> context
     1.7 +  val schematic_goal: state -> bool
     1.8 +  val is_relevant: state -> bool
     1.9    val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
    1.10    val local_default_proof: state -> state
    1.11    val local_immediate_proof: state -> state
    1.12 @@ -138,8 +140,6 @@
    1.13      (binding * string option * mixfix) list ->
    1.14      (Attrib.binding * (string * string list) list) list ->
    1.15      (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
    1.16 -  val schematic_goal: state -> bool
    1.17 -  val is_relevant: state -> bool
    1.18    val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
    1.19    val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
    1.20    val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
    1.21 @@ -1125,6 +1125,19 @@
    1.22    global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
    1.23  
    1.24  
    1.25 +(* relevant proof states *)
    1.26 +
    1.27 +fun schematic_goal state =
    1.28 +  let val (_, {statement = (_, _, prop), ...}) = find_goal state
    1.29 +  in Goal.is_schematic prop end;
    1.30 +
    1.31 +fun is_relevant state =
    1.32 +  (case try find_goal state of
    1.33 +    NONE => true
    1.34 +  | SOME (_, {statement = (_, _, prop), goal, ...}) =>
    1.35 +      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
    1.36 +
    1.37 +
    1.38  (* terminal proof steps *)
    1.39  
    1.40  local
    1.41 @@ -1136,11 +1149,15 @@
    1.42      val initial' = apfst check_closure initial;
    1.43      val terminal' = (apfst o Option.map o apfst) check_closure terminal;
    1.44    in
    1.45 -    state
    1.46 -    |> proof (SOME initial')
    1.47 -    |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
    1.48 -    |> Seq.the_result ""
    1.49 -  end;
    1.50 +    if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
    1.51 +      state
    1.52 +      |> proof (SOME (Method.sorry_text false, #2 initial'))
    1.53 +      |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
    1.54 +    else
    1.55 +      state
    1.56 +      |> proof (SOME initial')
    1.57 +      |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
    1.58 +  end |> Seq.the_result "";
    1.59  
    1.60  in
    1.61  
    1.62 @@ -1232,19 +1249,6 @@
    1.63  
    1.64  (** future proofs **)
    1.65  
    1.66 -(* relevant proof states *)
    1.67 -
    1.68 -fun schematic_goal state =
    1.69 -  let val (_, {statement = (_, _, prop), ...}) = find_goal state
    1.70 -  in Goal.is_schematic prop end;
    1.71 -
    1.72 -fun is_relevant state =
    1.73 -  (case try find_goal state of
    1.74 -    NONE => true
    1.75 -  | SOME (_, {statement = (_, _, prop), goal, ...}) =>
    1.76 -      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
    1.77 -
    1.78 -
    1.79  (* full proofs *)
    1.80  
    1.81  local