src/Pure/Isar/proof.ML
author wenzelm
Wed Mar 30 23:32:50 2016 +0200 (2016-03-30)
changeset 62773 e6443edaebff
parent 62771 dd2914250ca7
child 62819 d3ff367a16a0
permissions -rw-r--r--
more explicit support for object-logic constraint;
     1 (*  Title:      Pure/Isar/proof.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 The Isar/VM proof language interpreter: maintains a structured flow of
     5 context elements, goals, refinements, and facts.
     6 *)
     7 
     8 signature PROOF =
     9 sig
    10   type context = Proof.context
    11   type method = Method.method
    12   type state
    13   val init: context -> state
    14   val level: state -> int
    15   val assert_bottom: bool -> state -> state
    16   val context_of: state -> context
    17   val theory_of: state -> theory
    18   val map_context: (context -> context) -> state -> state
    19   val map_context_result : (context -> 'a * context) -> state -> 'a * state
    20   val map_contexts: (context -> context) -> state -> state
    21   val propagate_ml_env: state -> state
    22   val put_thms: bool -> string * thm list option -> state -> state
    23   val the_facts: state -> thm list
    24   val the_fact: state -> thm
    25   val set_facts: thm list -> state -> state
    26   val reset_facts: state -> state
    27   val assert_forward: state -> state
    28   val assert_chain: state -> state
    29   val assert_forward_or_chain: state -> state
    30   val assert_backward: state -> state
    31   val assert_no_chain: state -> state
    32   val enter_forward: state -> state
    33   val enter_chain: state -> state
    34   val enter_backward: state -> state
    35   val has_bottom_goal: state -> bool
    36   val using_facts: thm list -> state -> state
    37   val pretty_state: state -> Pretty.T list
    38   val refine: Method.text -> state -> state Seq.result Seq.seq
    39   val refine_end: Method.text -> state -> state Seq.result Seq.seq
    40   val refine_singleton: Method.text -> state -> state
    41   val refine_insert: thm list -> state -> state
    42   val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
    43   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
    44   val goal: state -> {context: context, facts: thm list, goal: thm}
    45   val simple_goal: state -> {context: context, goal: thm}
    46   val status_markup: state -> Markup.T
    47   val let_bind: (term list * term) list -> state -> state
    48   val let_bind_cmd: (string list * string) list -> state -> state
    49   val write: Syntax.mode -> (term * mixfix) list -> state -> state
    50   val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
    51   val fix: (binding * typ option * mixfix) list -> state -> state
    52   val fix_cmd: (binding * string option * mixfix) list -> state -> state
    53   val assm: Assumption.export -> (binding * typ option * mixfix) list ->
    54     (term * term list) list list -> (Thm.binding * (term * term list) list) list ->
    55     state -> state
    56   val assm_cmd: Assumption.export -> (binding * string option * mixfix) list ->
    57     (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
    58     state -> state
    59   val assume: (binding * typ option * mixfix) list ->
    60     (term * term list) list list -> (Thm.binding * (term * term list) list) list ->
    61     state -> state
    62   val assume_cmd: (binding * string option * mixfix) list ->
    63     (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
    64     state -> state
    65   val presume: (binding * typ option * mixfix) list ->
    66     (term * term list) list list -> (Thm.binding * (term * term list) list) list ->
    67     state -> state
    68   val presume_cmd: (binding * string option * mixfix) list ->
    69     (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
    70     state -> state
    71   val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
    72   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
    73   val chain: state -> state
    74   val chain_facts: thm list -> state -> state
    75   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    76   val note_thmss_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
    77   val from_thmss: ((thm list * attribute list) list) list -> state -> state
    78   val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    79   val with_thmss: ((thm list * attribute list) list) list -> state -> state
    80   val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    81   val supply: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    82   val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
    83   val using: ((thm list * attribute list) list) list -> state -> state
    84   val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    85   val unfolding: ((thm list * attribute list) list) list -> state -> state
    86   val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    87   val case_: Thm.binding * ((string * Position.T) * binding option list) -> state -> state
    88   val case_cmd: Attrib.binding * ((string * Position.T) * binding option list) -> state -> state
    89   val begin_block: state -> state
    90   val next_block: state -> state
    91   val end_block: state -> state
    92   val begin_notepad: context -> state
    93   val end_notepad: state -> context
    94   val proof: Method.text_range option -> state -> state Seq.result Seq.seq
    95   val defer: int -> state -> state
    96   val prefer: int -> state -> state
    97   val apply: Method.text_range -> state -> state Seq.result Seq.seq
    98   val apply_end: Method.text_range -> state -> state Seq.result Seq.seq
    99   val local_qed: Method.text_range option * bool -> state -> state
   100   val theorem: Method.text option -> (thm list list -> context -> context) ->
   101     (term * term list) list list -> context -> state
   102   val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
   103     (string * string list) list list -> context -> state
   104   val global_qed: Method.text_range option * bool -> state -> context
   105   val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
   106   val local_default_proof: state -> state
   107   val local_immediate_proof: state -> state
   108   val local_skip_proof: bool -> state -> state
   109   val local_done_proof: state -> state
   110   val global_terminal_proof: Method.text_range * Method.text_range option -> state -> context
   111   val global_default_proof: state -> context
   112   val global_immediate_proof: state -> context
   113   val global_skip_proof: bool -> state -> context
   114   val global_done_proof: state -> context
   115   val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
   116     Proof_Context.mode -> bool -> string -> Method.text option ->
   117     (context * thm list list -> state -> state) ->
   118     (binding * typ option * mixfix) list ->
   119     (Thm.binding * (term * term list) list) list ->
   120     (Thm.binding * (term * term list) list) list -> state -> thm list * state
   121   val have: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   122     (binding * typ option * mixfix) list ->
   123     (Thm.binding * (term * term list) list) list ->
   124     (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
   125   val have_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   126     (binding * string option * mixfix) list ->
   127     (Attrib.binding * (string * string list) list) list ->
   128     (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
   129   val show: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   130     (binding * typ option * mixfix) list ->
   131     (Thm.binding * (term * term list) list) list ->
   132     (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
   133   val show_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   134     (binding * string option * mixfix) list ->
   135     (Attrib.binding * (string * string list) list) list ->
   136     (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
   137   val schematic_goal: state -> bool
   138   val is_relevant: state -> bool
   139   val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
   140   val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
   141   val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
   142 end;
   143 
   144 structure Proof: PROOF =
   145 struct
   146 
   147 type context = Proof.context;
   148 type method = Method.method;
   149 
   150 
   151 (** proof state **)
   152 
   153 (* datatype state *)
   154 
   155 datatype mode = Forward | Chain | Backward;
   156 
   157 datatype state =
   158   State of node Stack.T
   159 and node =
   160   Node of
   161    {context: context,
   162     facts: thm list option,
   163     mode: mode,
   164     goal: goal option}
   165 and goal =
   166   Goal of
   167    {statement: (string * Position.T) * term list list * term,
   168       (*goal kind and statement (starting with vars), initial proposition*)
   169     using: thm list,                      (*goal facts*)
   170     goal: thm,                            (*subgoals ==> statement*)
   171     before_qed: Method.text option,
   172     after_qed:
   173       (context * thm list list -> state -> state) *
   174       (context * thm list list -> context -> context)};
   175 
   176 val _ =
   177   PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
   178     Pretty.to_polyml (Pretty.str "<Proof.state>"));
   179 
   180 fun make_goal (statement, using, goal, before_qed, after_qed) =
   181   Goal {statement = statement, using = using, goal = goal,
   182     before_qed = before_qed, after_qed = after_qed};
   183 
   184 fun make_node (context, facts, mode, goal) =
   185   Node {context = context, facts = facts, mode = mode, goal = goal};
   186 
   187 fun map_node f (Node {context, facts, mode, goal}) =
   188   make_node (f (context, facts, mode, goal));
   189 
   190 val init_context =
   191   Proof_Context.set_stmt true #>
   192   Proof_Context.map_naming (K Name_Space.local_naming);
   193 
   194 fun init ctxt =
   195   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
   196 
   197 fun top (State stack) = Stack.top stack |> (fn Node node => node);
   198 fun map_top f (State stack) = State (Stack.map_top (map_node f) stack);
   199 fun map_all f (State stack) = State (Stack.map_all (map_node f) stack);
   200 
   201 
   202 
   203 (** basic proof state operations **)
   204 
   205 (* block structure *)
   206 
   207 fun open_block (State stack) = State (Stack.push stack);
   208 
   209 fun close_block (State stack) = State (Stack.pop stack)
   210   handle List.Empty => error "Unbalanced block parentheses";
   211 
   212 fun level (State stack) = Stack.level stack;
   213 
   214 fun assert_bottom b state =
   215   let val b' = level state <= 2 in
   216     if b andalso not b' then error "Not at bottom of proof"
   217     else if not b andalso b' then error "Already at bottom of proof"
   218     else state
   219   end;
   220 
   221 
   222 (* context *)
   223 
   224 val context_of = #context o top;
   225 val theory_of = Proof_Context.theory_of o context_of;
   226 
   227 fun map_context f =
   228   map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   229 
   230 fun map_context_result f state =
   231   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
   232 
   233 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   234 
   235 fun propagate_ml_env state = map_contexts
   236   (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
   237 
   238 val put_thms = map_context oo Proof_Context.put_thms;
   239 
   240 
   241 (* facts *)
   242 
   243 val get_facts = #facts o top;
   244 
   245 fun the_facts state =
   246   (case get_facts state of
   247     SOME facts => facts
   248   | NONE => error "No current facts available");
   249 
   250 fun the_fact state =
   251   (case the_facts state of
   252     [thm] => thm
   253   | _ => error "Single theorem expected");
   254 
   255 fun put_facts facts =
   256   map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   257   put_thms true (Auto_Bind.thisN, facts);
   258 
   259 val set_facts = put_facts o SOME;
   260 val reset_facts = put_facts NONE;
   261 
   262 fun these_factss more_facts (named_factss, state) =
   263   (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
   264 
   265 fun export_facts inner outer =
   266   (case get_facts inner of
   267     NONE => reset_facts outer
   268   | SOME thms =>
   269       thms
   270       |> Proof_Context.export (context_of inner) (context_of outer)
   271       |> (fn ths => set_facts ths outer));
   272 
   273 
   274 (* mode *)
   275 
   276 val get_mode = #mode o top;
   277 fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
   278 
   279 val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
   280 
   281 fun assert_mode pred state =
   282   let val mode = get_mode state in
   283     if pred mode then state
   284     else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
   285   end;
   286 
   287 val assert_forward = assert_mode (fn mode => mode = Forward);
   288 val assert_chain = assert_mode (fn mode => mode = Chain);
   289 val assert_forward_or_chain = assert_mode (fn mode => mode = Forward orelse mode = Chain);
   290 val assert_backward = assert_mode (fn mode => mode = Backward);
   291 val assert_no_chain = assert_mode (fn mode => mode <> Chain);
   292 
   293 val enter_forward = put_mode Forward;
   294 val enter_chain = put_mode Chain;
   295 val enter_backward = put_mode Backward;
   296 
   297 
   298 (* current goal *)
   299 
   300 fun current_goal state =
   301   (case top state of
   302     {context = ctxt, goal = SOME (Goal goal), ...} => (ctxt, goal)
   303   | _ => error "No current goal");
   304 
   305 fun assert_current_goal g state =
   306   let val g' = can current_goal state in
   307     if g andalso not g' then error "No goal in this block"
   308     else if not g andalso g' then error "Goal present in this block"
   309     else state
   310   end;
   311 
   312 fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
   313 
   314 val set_goal = put_goal o SOME;
   315 val reset_goal = put_goal NONE;
   316 
   317 val before_qed = #before_qed o #2 o current_goal;
   318 
   319 
   320 (* bottom goal *)
   321 
   322 fun has_bottom_goal (State stack) =
   323   let
   324     fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
   325       | bottom [Node {goal, ...}] = is_some goal
   326       | bottom [] = false
   327       | bottom (_ :: rest) = bottom rest;
   328   in bottom (op :: (Stack.dest stack)) end;
   329 
   330 
   331 (* nested goal *)
   332 
   333 fun map_goal f (State stack) =
   334   (case Stack.dest stack of
   335     (Node {context = ctxt, facts, mode, goal = SOME goal}, node :: nodes) =>
   336       let
   337         val Goal {statement, using, goal, before_qed, after_qed} = goal;
   338         val (ctxt', statement', using', goal', before_qed', after_qed') =
   339           f (ctxt, statement, using, goal, before_qed, after_qed);
   340         val goal' = make_goal (statement', using', goal', before_qed', after_qed');
   341       in State (Stack.make (make_node (ctxt', facts, mode, SOME goal')) (node :: nodes)) end
   342   | (top_node, node :: nodes) =>
   343       let
   344         val State stack' = map_goal f (State (Stack.make node nodes));
   345         val (node', nodes') = Stack.dest stack';
   346       in State (Stack.make top_node (node' :: nodes')) end
   347   | _ => State stack);
   348 
   349 fun provide_goal goal =
   350   map_goal (fn (ctxt, statement, using, _, before_qed, after_qed) =>
   351     (ctxt, statement, using, goal, before_qed, after_qed));
   352 
   353 fun using_facts using =
   354   map_goal (fn (ctxt, statement, _, goal, before_qed, after_qed) =>
   355     (ctxt, statement, using, goal, before_qed, after_qed));
   356 
   357 fun find_goal state =
   358   (case try current_goal state of
   359     SOME ctxt_goal => ctxt_goal
   360   | NONE => find_goal (close_block state handle ERROR _ => error "No proof goal"));
   361 
   362 fun get_goal state =
   363   let val (ctxt, {using, goal, ...}) = find_goal state
   364   in (ctxt, (using, goal)) end;
   365 
   366 
   367 
   368 (** pretty_state **)
   369 
   370 local
   371 
   372 fun pretty_facts _ _ NONE = []
   373   | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths];
   374 
   375 fun pretty_sep prts [] = prts
   376   | pretty_sep [] prts = prts
   377   | pretty_sep prts1 prts2 = prts1 @ [Pretty.str ""] @ prts2;
   378 
   379 in
   380 
   381 fun pretty_state state =
   382   let
   383     val {context = ctxt, facts, mode, goal = _} = top state;
   384     val verbose = Config.get ctxt Proof_Context.verbose;
   385 
   386     fun prt_goal (SOME (_, {statement = _, using, goal, before_qed = _, after_qed = _})) =
   387           pretty_sep
   388             (pretty_facts ctxt "using"
   389               (if mode <> Backward orelse null using then NONE else SOME using))
   390             ([Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal)
   391       | prt_goal NONE = [];
   392 
   393     val prt_ctxt =
   394       if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
   395       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
   396       else [];
   397 
   398     val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   399   in
   400     [Pretty.block
   401       [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
   402     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
   403     (if verbose orelse mode = Forward then
   404        pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state))
   405      else if mode = Chain then pretty_facts ctxt "picking" facts
   406      else prt_goal (try find_goal state))
   407   end;
   408 
   409 end;
   410 
   411 
   412 
   413 (** proof steps **)
   414 
   415 (* refine via method *)
   416 
   417 local
   418 
   419 fun goalN i = "goal" ^ string_of_int i;
   420 fun goals st = map goalN (1 upto Thm.nprems_of st);
   421 
   422 fun no_goal_cases st = map (rpair NONE) (goals st);
   423 
   424 fun goal_cases ctxt st =
   425   Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
   426 
   427 fun apply_method text ctxt state =
   428   find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
   429     Method.evaluate text ctxt using (goal_ctxt, goal)
   430     |> Seq.map_result (fn (goal_ctxt', goal') =>
   431       let
   432         val goal_ctxt'' = goal_ctxt'
   433           |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
   434         val state' = state
   435           |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
   436       in state' end));
   437 
   438 in
   439 
   440 fun refine text state = apply_method text (context_of state) state;
   441 fun refine_end text state = apply_method text (#1 (find_goal state)) state;
   442 
   443 fun refine_singleton text = refine text #> Seq.the_result "";
   444 
   445 fun refine_insert ths =
   446   refine_singleton (Method.Basic (K (Method.insert ths)));
   447 
   448 fun refine_primitive r =
   449   refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
   450 
   451 end;
   452 
   453 
   454 (* refine via sub-proof *)
   455 
   456 local
   457 
   458 fun finish_tac _ 0 = K all_tac
   459   | finish_tac ctxt n =
   460       Goal.norm_hhf_tac ctxt THEN'
   461       SUBGOAL (fn (goal, i) =>
   462         if can Logic.unprotect (Logic.strip_assums_concl goal) then
   463           eresolve_tac ctxt [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
   464         else finish_tac ctxt (n - 1) (i + 1));
   465 
   466 fun goal_tac ctxt rule =
   467   Goal.norm_hhf_tac ctxt THEN'
   468   resolve_tac ctxt [rule] THEN'
   469   finish_tac ctxt (Thm.nprems_of rule);
   470 
   471 fun FINDGOAL tac st =
   472   let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
   473   in find 1 (Thm.nprems_of st) st end;
   474 
   475 fun protect_prem i th =
   476   Thm.bicompose NONE {flatten = false, match = false, incremented = true}
   477     (false, Drule.incr_indexes th Drule.protectD, 1) i th
   478   |> Seq.hd;
   479 
   480 fun protect_prems th =
   481   fold_rev protect_prem (1 upto Thm.nprems_of th) th;
   482 
   483 in
   484 
   485 fun refine_goals print_rule result_ctxt result state =
   486   let
   487     val (goal_ctxt, (_, goal)) = get_goal state;
   488     fun refine rule st =
   489       (print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
   490   in
   491     result
   492     |> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
   493     |> Proof_Context.goal_export result_ctxt goal_ctxt
   494     |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
   495   end;
   496 
   497 end;
   498 
   499 
   500 (* conclude goal *)
   501 
   502 fun conclude_goal ctxt goal propss =
   503   let
   504     val thy = Proof_Context.theory_of ctxt;
   505 
   506     val _ =
   507       Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse
   508         error "Bad background theory of goal state";
   509     val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
   510 
   511     fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
   512 
   513     val th =
   514       (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
   515         handle THM _ => err_lost ())
   516       |> Drule.flexflex_unique (SOME ctxt)
   517       |> Thm.check_shyps ctxt
   518       |> Thm.check_hyps (Context.Proof ctxt);
   519 
   520     val goal_propss = filter_out null propss;
   521     val results =
   522       Conjunction.elim_balanced (length goal_propss) th
   523       |> map2 Conjunction.elim_balanced (map length goal_propss)
   524       handle THM _ => err_lost ();
   525     val _ =
   526       Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
   527         orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
   528 
   529     fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
   530       | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
   531       | recover_result [] [] = []
   532       | recover_result _ _ = err_lost ();
   533   in recover_result propss results end;
   534 
   535 val finished_goal_error = "Failed to finish proof";
   536 
   537 fun finished_goal pos state =
   538   let val (ctxt, (_, goal)) = get_goal state in
   539     if Thm.no_prems goal then Seq.Result state
   540     else
   541       Seq.Error (fn () =>
   542         finished_goal_error ^ Position.here pos ^ ":\n" ^
   543           Proof_Display.string_of_goal ctxt goal)
   544   end;
   545 
   546 
   547 (* goal views -- corresponding to methods *)
   548 
   549 fun raw_goal state =
   550   let val (ctxt, (facts, goal)) = get_goal state
   551   in {context = ctxt, facts = facts, goal = goal} end;
   552 
   553 val goal = raw_goal o refine_insert [];
   554 
   555 fun simple_goal state =
   556   let
   557     val (_, (facts, _)) = get_goal state;
   558     val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
   559   in {context = ctxt, goal = goal} end;
   560 
   561 fun status_markup state =
   562   (case try goal state of
   563     SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
   564   | NONE => Markup.empty);
   565 
   566 fun method_error kind pos state =
   567   Seq.single (Proof_Display.method_error kind pos (raw_goal state));
   568 
   569 
   570 
   571 (*** structured proof commands ***)
   572 
   573 (** context elements **)
   574 
   575 (* let bindings *)
   576 
   577 local
   578 
   579 fun gen_bind bind args state =
   580   state
   581   |> assert_forward
   582   |> map_context (bind true args #> snd)
   583   |> reset_facts;
   584 
   585 in
   586 
   587 val let_bind = gen_bind Proof_Context.match_bind;
   588 val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd;
   589 
   590 end;
   591 
   592 
   593 (* concrete syntax *)
   594 
   595 local
   596 
   597 fun read_arg (c, mx) ctxt =
   598   (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
   599     Free (x, _) =>
   600       let
   601         val ctxt' =
   602           ctxt |> is_none (Variable.default_type ctxt x) ?
   603             Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
   604         val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
   605       in ((t, mx), ctxt') end
   606   | t => ((t, mx), ctxt));
   607 
   608 fun gen_write prep_arg mode args =
   609   assert_forward
   610   #> map_context (fold_map prep_arg args #-> Proof_Context.notation true mode)
   611   #> reset_facts;
   612 
   613 in
   614 
   615 val write = gen_write pair;
   616 val write_cmd = gen_write read_arg;
   617 
   618 end;
   619 
   620 
   621 (* fix *)
   622 
   623 local
   624 
   625 fun gen_fix add_fixes raw_fixes =
   626   assert_forward
   627   #> map_context (snd o add_fixes raw_fixes)
   628   #> reset_facts;
   629 
   630 in
   631 
   632 val fix = gen_fix Proof_Context.add_fixes;
   633 val fix_cmd = gen_fix Proof_Context.add_fixes_cmd;
   634 
   635 end;
   636 
   637 
   638 (* structured clause *)
   639 
   640 fun export_binds ctxt' ctxt binds =
   641   let
   642     val rhss =
   643       map (the_list o snd) binds
   644       |> burrow (Variable.export_terms ctxt' ctxt)
   645       |> map (try the_single);
   646   in map fst binds ~~ rhss end;
   647 
   648 fun prep_clause prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
   649   let
   650     (*fixed variables*)
   651     val ((xs', vars), fix_ctxt) = ctxt
   652       |> fold_map prep_var raw_fixes
   653       |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
   654 
   655     (*propositions with term bindings*)
   656     val (all_propss, binds) = prep_propp fix_ctxt (raw_assumes @ raw_shows);
   657     val (assumes_propss, shows_propss) = chop (length raw_assumes) all_propss;
   658 
   659     (*params*)
   660     val (ps, params_ctxt) = fix_ctxt
   661       |> (fold o fold) Variable.declare_term all_propss
   662       |> fold Variable.bind_term binds
   663       |> fold_map Proof_Context.inferred_param xs';
   664     val xs = map (Variable.check_name o #1) vars;
   665     val params = xs ~~ map Free ps;
   666 
   667     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
   668 
   669     (*result term bindings*)
   670     val shows_props = flat shows_propss;
   671     val binds' =
   672       (case try List.last shows_props of
   673         NONE => []
   674       | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
   675     val result_binds =
   676       (Auto_Bind.facts params_ctxt shows_props @ binds')
   677       |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
   678       |> export_binds params_ctxt ctxt;
   679   in ((params, assumes_propss, shows_propss, result_binds), params_ctxt) end;
   680 
   681 
   682 (* assume *)
   683 
   684 local
   685 
   686 fun gen_assume prep_var prep_propp prep_att export raw_fixes raw_prems raw_concls state =
   687   let
   688     val ctxt = context_of state;
   689 
   690     val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
   691     val (params, prems_propss, concl_propss, result_binds) =
   692       #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
   693 
   694     fun close prop =
   695       fold_rev Logic.dependent_all_name params
   696         (Logic.list_implies (flat prems_propss, prop));
   697     val propss = (map o map) close concl_propss;
   698   in
   699     state
   700     |> assert_forward
   701     |> map_context_result (fn ctxt =>
   702       ctxt
   703       |> (fold o fold) Variable.declare_term propss
   704       |> fold Variable.maybe_bind_term result_binds
   705       |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss
   706       |-> (fn premss =>
   707         Proof_Context.note_thmss "" (bindings ~~ (map o map) (fn th => ([th], [])) premss)))
   708     |> these_factss [] |> #2
   709   end;
   710 
   711 in
   712 
   713 val assm = gen_assume Proof_Context.cert_var Proof_Context.cert_propp (K I);
   714 val assm_cmd = gen_assume Proof_Context.read_var Proof_Context.read_propp Attrib.attribute_cmd;
   715 
   716 val assume = assm Assumption.assume_export;
   717 val assume_cmd = assm_cmd Assumption.assume_export;
   718 
   719 val presume = assm Assumption.presume_export;
   720 val presume_cmd = assm_cmd Assumption.presume_export;
   721 
   722 end;
   723 
   724 
   725 (* def *)
   726 
   727 local
   728 
   729 fun gen_def prep_att prep_var prep_binds args state =
   730   let
   731     val _ = assert_forward state;
   732     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
   733     val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
   734   in
   735     state
   736     |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
   737     |>> map (fn (x, _, mx) => (x, mx))
   738     |-> (fn vars =>
   739       map_context_result (prep_binds false (map swap raw_rhss))
   740       #-> (fn rhss =>
   741         let
   742           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
   743             ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
   744         in map_context_result (Local_Defs.add_defs defs) end))
   745     |-> (set_facts o map (#2 o #2))
   746   end;
   747 
   748 in
   749 
   750 val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
   751 val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
   752 
   753 end;
   754 
   755 
   756 
   757 (** facts **)
   758 
   759 (* chain *)
   760 
   761 fun clean_facts ctxt =
   762   set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
   763 
   764 val chain =
   765   assert_forward
   766   #> clean_facts
   767   #> enter_chain;
   768 
   769 fun chain_facts facts =
   770   set_facts facts
   771   #> chain;
   772 
   773 
   774 (* note etc. *)
   775 
   776 fun no_binding args = map (pair (Binding.empty, [])) args;
   777 
   778 local
   779 
   780 fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   781   state
   782   |> assert_forward
   783   |> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   784     (Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
   785   |> these_factss (more_facts state)
   786   ||> opt_chain
   787   |> opt_result;
   788 
   789 in
   790 
   791 val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
   792 val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
   793 
   794 val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
   795 val from_thmss_cmd =
   796   gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
   797 
   798 val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
   799 val with_thmss_cmd =
   800   gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
   801 
   802 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
   803 
   804 end;
   805 
   806 
   807 (* facts during goal refinement *)
   808 
   809 local
   810 
   811 fun gen_supply prep_att prep_fact args state =
   812   state
   813   |> assert_backward
   814   |> map_context (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   815        (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) |> snd);
   816 
   817 in
   818 
   819 val supply = gen_supply (K I) (K I);
   820 val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact;
   821 
   822 end;
   823 
   824 
   825 (* using/unfolding *)
   826 
   827 local
   828 
   829 fun gen_using f g prep_att prep_fact args state =
   830   state
   831   |> assert_backward
   832   |> map_context_result
   833     (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   834       (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   835   |> (fn (named_facts, state') =>
   836     state' |> map_goal (fn (goal_ctxt, statement, using, goal, before_qed, after_qed) =>
   837       let
   838         val ctxt = context_of state';
   839         val ths = maps snd named_facts;
   840       in (goal_ctxt, statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
   841 
   842 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
   843 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
   844 val unfold_goals = Local_Defs.unfold_goals;
   845 
   846 in
   847 
   848 val using = gen_using append_using (K (K I)) (K I) (K I);
   849 val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
   850 val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
   851 val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
   852 
   853 end;
   854 
   855 
   856 (* case *)
   857 
   858 local
   859 
   860 fun gen_case internal prep_att ((raw_binding, raw_atts), ((name, pos), xs)) state =
   861   let
   862     val ctxt = context_of state;
   863 
   864     val binding = if Binding.is_empty raw_binding then Binding.make (name, pos) else raw_binding;
   865     val atts = map (prep_att ctxt) raw_atts;
   866 
   867     val (asms, state') = state |> map_context_result (fn ctxt =>
   868       ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs));
   869     val assumptions =
   870       asms |> map (fn (a, ts) => ((Binding.qualified true a binding, []), map (rpair []) ts));
   871   in
   872     state'
   873     |> assume [] [] assumptions
   874     |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
   875     |> `the_facts |-> (fn thms => note_thmss [((binding, atts), [(thms, [])])])
   876   end;
   877 
   878 in
   879 
   880 val case_ = gen_case true (K I);
   881 val case_cmd = gen_case false Attrib.attribute_cmd;
   882 
   883 end;
   884 
   885 
   886 
   887 (** proof structure **)
   888 
   889 (* blocks *)
   890 
   891 val begin_block =
   892   assert_forward
   893   #> open_block
   894   #> reset_goal
   895   #> open_block;
   896 
   897 val next_block =
   898   assert_forward
   899   #> close_block
   900   #> open_block
   901   #> reset_goal
   902   #> reset_facts;
   903 
   904 fun end_block state =
   905   state
   906   |> assert_forward
   907   |> assert_bottom false
   908   |> close_block
   909   |> assert_current_goal false
   910   |> close_block
   911   |> export_facts state;
   912 
   913 
   914 (* global notepad *)
   915 
   916 val begin_notepad =
   917   init
   918   #> open_block
   919   #> map_context (Variable.set_body true)
   920   #> open_block;
   921 
   922 val end_notepad =
   923   assert_forward
   924   #> assert_bottom true
   925   #> close_block
   926   #> assert_current_goal false
   927   #> close_block
   928   #> context_of;
   929 
   930 
   931 (* sub-proofs *)
   932 
   933 fun proof opt_text =
   934   Seq.APPEND
   935     (assert_backward
   936       #> refine (the_default Method.standard_text (Method.text opt_text))
   937       #> Seq.map_result
   938         (using_facts []
   939           #> enter_forward
   940           #> open_block
   941           #> reset_goal),
   942      method_error "initial" (Method.position opt_text));
   943 
   944 fun end_proof bot (prev_pos, (opt_text, immed)) =
   945   let
   946     val (finish_text, terminal_pos, finished_pos) =
   947       (case opt_text of
   948         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
   949       | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
   950   in
   951     Seq.APPEND (fn state =>
   952       state
   953       |> assert_forward
   954       |> assert_bottom bot
   955       |> close_block
   956       |> assert_current_goal true
   957       |> using_facts []
   958       |> `before_qed |-> (refine o the_default Method.succeed_text)
   959       |> Seq.maps_results (refine finish_text),
   960       method_error "terminal" terminal_pos)
   961     #> Seq.maps_results (Seq.single o finished_goal finished_pos)
   962   end;
   963 
   964 fun check_result msg sq =
   965   (case Seq.pull sq of
   966     NONE => error msg
   967   | SOME (s, _) => s);
   968 
   969 
   970 (* unstructured refinement *)
   971 
   972 fun defer i =
   973   assert_no_chain #>
   974   refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i)));
   975 
   976 fun prefer i =
   977   assert_no_chain #>
   978   refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i)));
   979 
   980 fun apply (text, (pos, _)) =
   981   Seq.APPEND (assert_backward #> refine text #> Seq.map_result (using_facts []),
   982     method_error "" pos);
   983 
   984 fun apply_end (text, (pos, _)) =
   985   Seq.APPEND (assert_forward #> refine_end text, method_error "" pos);
   986 
   987 
   988 
   989 (** goals **)
   990 
   991 (* generic goals *)
   992 
   993 local
   994 
   995 val is_var =
   996   can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
   997   can (dest_Var o Logic.dest_term);
   998 
   999 fun implicit_vars props =
  1000   let
  1001     val (var_props, _) = take_prefix is_var props;
  1002     val explicit_vars = fold Term.add_vars var_props [];
  1003     val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
  1004   in map (Logic.mk_term o Var) vars end;
  1005 
  1006 fun refine_terms n =
  1007   refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
  1008     K (HEADGOAL (PRECISE_CONJUNCTS n
  1009       (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
  1010 
  1011 in
  1012 
  1013 fun generic_goal kind before_qed after_qed goal_ctxt goal_propss result_binds state =
  1014   let
  1015     val chaining = can assert_chain state;
  1016     val pos = Position.thread_data ();
  1017 
  1018     val goal_props = flat goal_propss;
  1019     val vars = implicit_vars goal_props;
  1020     val propss' = vars :: goal_propss;
  1021     val goal_propss = filter_out null propss';
  1022 
  1023     val goal =
  1024       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
  1025       |> Thm.cterm_of goal_ctxt
  1026       |> Thm.weaken_sorts' goal_ctxt;
  1027     val statement = ((kind, pos), propss', Thm.term_of goal);
  1028 
  1029     val after_qed' = after_qed |>> (fn after_local => fn results =>
  1030       map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
  1031   in
  1032     state
  1033     |> assert_forward_or_chain
  1034     |> enter_forward
  1035     |> open_block
  1036     |> enter_backward
  1037     |> map_context
  1038       (K goal_ctxt
  1039         #> init_context
  1040         #> Variable.set_body true
  1041         #> Proof_Context.auto_bind_goal goal_props)
  1042     |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
  1043     |> chaining ? (`the_facts #-> using_facts)
  1044     |> reset_facts
  1045     |> not (null vars) ? refine_terms (length goal_propss)
  1046     |> null goal_props ? refine_singleton (Method.Basic Method.assumption)
  1047   end;
  1048 
  1049 fun generic_qed state =
  1050   let
  1051     val (goal_ctxt, {statement = (_, propss, _), goal, after_qed, ...}) =
  1052       current_goal state;
  1053     val results = tl (conclude_goal goal_ctxt goal propss);
  1054   in state |> close_block |> pair (after_qed, (goal_ctxt, results)) end;
  1055 
  1056 end;
  1057 
  1058 
  1059 (* local goals *)
  1060 
  1061 fun local_goal print_results prep_att prep_propp prep_var strict_asm
  1062     kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
  1063   let
  1064     val ctxt = context_of state;
  1065 
  1066     val add_assumes =
  1067       Assumption.add_assms
  1068         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
  1069 
  1070     (*params*)
  1071     val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
  1072       |> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows);
  1073 
  1074     (*prems*)
  1075     val (assumes_bindings, shows_bindings) =
  1076       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
  1077     val (that_fact, goal_ctxt) = params_ctxt
  1078       |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
  1079       |> (fn (premss, ctxt') =>
  1080           let
  1081             val prems = Assumption.local_prems_of ctxt' ctxt;
  1082             val ctxt'' =
  1083               ctxt'
  1084               |> not (null assumes_propss) ?
  1085                 (snd o Proof_Context.note_thmss ""
  1086                   [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
  1087               |> (snd o Proof_Context.note_thmss ""
  1088                   (assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
  1089           in (prems, ctxt'') end);
  1090 
  1091     (*result*)
  1092     fun after_qed' (result_ctxt, results) state' =
  1093       let
  1094         val ctxt' = context_of state';
  1095         val export0 =
  1096           Assumption.export false result_ctxt ctxt' #>
  1097           fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
  1098           Raw_Simplifier.norm_hhf_protect ctxt';
  1099         val export = map export0 #> Variable.export result_ctxt ctxt';
  1100       in
  1101         state'
  1102         |> local_results (shows_bindings ~~ burrow export results)
  1103         |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
  1104         |> after_qed (result_ctxt, results)
  1105       end;
  1106   in
  1107     state
  1108     |> generic_goal kind before_qed (after_qed', K I) goal_ctxt shows_propss result_binds
  1109     |> pair that_fact
  1110   end;
  1111 
  1112 fun local_qeds arg =
  1113   end_proof false arg
  1114   #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
  1115 
  1116 fun local_qed arg =
  1117   local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
  1118 
  1119 
  1120 (* global goals *)
  1121 
  1122 fun global_goal prep_propp before_qed after_qed propp ctxt =
  1123   let
  1124     val (propss, binds) =
  1125       prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
  1126     val goal_ctxt = ctxt
  1127       |> (fold o fold) Variable.auto_fixes propss
  1128       |> fold Variable.bind_term binds;
  1129     fun after_qed' (result_ctxt, results) ctxt' = ctxt'
  1130       |> Proof_Context.restore_naming ctxt
  1131       |> after_qed (burrow (Proof_Context.export result_ctxt ctxt') results);
  1132   in
  1133     ctxt
  1134     |> init
  1135     |> generic_goal "" before_qed (K I, after_qed') goal_ctxt propss []
  1136   end;
  1137 
  1138 val theorem = global_goal Proof_Context.cert_propp;
  1139 val theorem_cmd = global_goal Proof_Context.read_propp;
  1140 
  1141 fun global_qeds arg =
  1142   end_proof true arg
  1143   #> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) =>
  1144     after_qed results (context_of state)));
  1145 
  1146 fun global_qed arg =
  1147   global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
  1148 
  1149 
  1150 (* terminal proof steps *)
  1151 
  1152 local
  1153 
  1154 fun terminal_proof qeds initial terminal =
  1155   proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
  1156   #> Seq.the_result "";
  1157 
  1158 in
  1159 
  1160 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
  1161 val local_default_proof = local_terminal_proof ((Method.standard_text, Position.no_range), NONE);
  1162 val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
  1163 val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
  1164 
  1165 fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
  1166 val global_default_proof = global_terminal_proof ((Method.standard_text, Position.no_range), NONE);
  1167 val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
  1168 val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
  1169 
  1170 end;
  1171 
  1172 
  1173 (* skip proofs *)
  1174 
  1175 fun local_skip_proof int state =
  1176   local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
  1177   Skip_Proof.report (context_of state);
  1178 
  1179 fun global_skip_proof int state =
  1180   global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
  1181   Skip_Proof.report (context_of state);
  1182 
  1183 
  1184 (* common goal statements *)
  1185 
  1186 fun internal_goal print_results mode =
  1187   local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
  1188     Proof_Context.cert_var;
  1189 
  1190 local
  1191 
  1192 fun gen_have prep_att prep_propp prep_var
  1193     strict_asm before_qed after_qed fixes assumes shows int =
  1194   local_goal (Proof_Display.print_results int (Position.thread_data ()))
  1195     prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
  1196 
  1197 fun gen_show prep_att prep_propp prep_var
  1198     strict_asm before_qed after_qed fixes assumes shows int state =
  1199   let
  1200     val testing = Unsynchronized.ref false;
  1201     val rule = Unsynchronized.ref (NONE: thm option);
  1202     fun fail_msg ctxt =
  1203       "Local statement fails to refine any pending goal" ::
  1204       (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
  1205       |> cat_lines;
  1206 
  1207     val pos = Position.thread_data ();
  1208     fun print_results ctxt res =
  1209       if ! testing then ()
  1210       else Proof_Display.print_results int pos ctxt res;
  1211     fun print_rule ctxt th =
  1212       if ! testing then rule := SOME th
  1213       else if int then
  1214         Proof_Display.string_of_rule ctxt "Successful" th
  1215         |> Markup.markup Markup.text_fold
  1216         |> Output.state
  1217       else ();
  1218     val test_proof =
  1219       local_skip_proof true
  1220       |> Unsynchronized.setmp testing true
  1221       |> Exn.interruptible_capture;
  1222 
  1223     fun after_qed' (result_ctxt, results) state' = state'
  1224       |> refine_goals print_rule result_ctxt (flat results)
  1225       |> check_result "Failed to refine any pending goal"
  1226       |> after_qed (result_ctxt, results);
  1227   in
  1228     state
  1229     |> local_goal print_results prep_att prep_propp prep_var strict_asm
  1230       "show" before_qed after_qed' fixes assumes shows
  1231     ||> int ? (fn goal_state =>
  1232       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
  1233         Exn.Res _ => goal_state
  1234       | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
  1235   end;
  1236 
  1237 in
  1238 
  1239 val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
  1240 val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
  1241 val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
  1242 val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
  1243 
  1244 end;
  1245 
  1246 
  1247 
  1248 (** future proofs **)
  1249 
  1250 (* relevant proof states *)
  1251 
  1252 fun schematic_goal state =
  1253   let val (_, {statement = (_, _, prop), ...}) = find_goal state
  1254   in Goal.is_schematic prop end;
  1255 
  1256 fun is_relevant state =
  1257   (case try find_goal state of
  1258     NONE => true
  1259   | SOME (_, {statement = (_, _, prop), goal, ...}) =>
  1260       Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
  1261 
  1262 
  1263 (* full proofs *)
  1264 
  1265 local
  1266 
  1267 structure Result = Proof_Data
  1268 (
  1269   type T = thm option;
  1270   fun init _ = NONE;
  1271 );
  1272 
  1273 fun the_result ctxt =
  1274   (case Result.get ctxt of
  1275     NONE => error "No result of forked proof"
  1276   | SOME th => th);
  1277 
  1278 val set_result = Result.put o SOME;
  1279 val reset_result = Result.put NONE;
  1280 
  1281 in
  1282 
  1283 fun future_proof fork_proof state =
  1284   let
  1285     val _ = assert_backward state;
  1286     val (goal_ctxt, goal_info) = find_goal state;
  1287     val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal_info;
  1288 
  1289     val _ = is_relevant state andalso error "Cannot fork relevant proof";
  1290 
  1291     val after_qed' =
  1292       (fn (_, [[th]]) => map_context (set_result th),
  1293        fn (_, [[th]]) => set_result th);
  1294     val result_ctxt =
  1295       state
  1296       |> map_context reset_result
  1297       |> map_goal (K (goal_ctxt, (kind, [[], [prop]], prop), using, goal, before_qed, after_qed'))
  1298       |> fork_proof;
  1299 
  1300     val future_thm = Future.map (the_result o snd) result_ctxt;
  1301     val finished_goal = Goal.protect 0 (Goal.future_result goal_ctxt future_thm prop);
  1302     val state' =
  1303       state
  1304       |> map_goal (K (goal_ctxt, statement, using, finished_goal, NONE, after_qed));
  1305   in (Future.map fst result_ctxt, state') end;
  1306 
  1307 end;
  1308 
  1309 
  1310 (* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
  1311 
  1312 local
  1313 
  1314 fun future_terminal_proof proof1 proof2 done state =
  1315   if Goal.future_enabled 3 andalso not (is_relevant state) then
  1316     state |> future_proof (fn state' =>
  1317       let
  1318         val pos = Position.thread_data ();
  1319         val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
  1320       in
  1321         Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
  1322           (fn () => ((), Timing.protocol props proof2 state'))
  1323       end) |> snd |> done
  1324   else proof1 state;
  1325 
  1326 in
  1327 
  1328 fun local_future_terminal_proof meths =
  1329   future_terminal_proof
  1330     (local_terminal_proof meths)
  1331     (local_terminal_proof meths #> context_of) local_done_proof;
  1332 
  1333 fun global_future_terminal_proof meths =
  1334   future_terminal_proof
  1335     (global_terminal_proof meths)
  1336     (global_terminal_proof meths) global_done_proof;
  1337 
  1338 end;
  1339 
  1340 end;