src/Pure/Isar/proof.ML
author haftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 23086 12320f6e2523
parent 21727 5acd4f35d26f
child 23360 9e3c0c1ad0ad
permissions -rw-r--r--
tuned Pure/General/name_space.ML
     1 (*  Title:      Pure/Isar/proof.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The Isar/VM proof language interpreter: maintains a structured flow of
     6 context elements, goals, refinements, and facts.
     7 *)
     8 
     9 signature PROOF =
    10 sig
    11   type context (*= Context.proof*)
    12   type method (*= Method.method*)
    13   type state
    14   val init: context -> state
    15   val level: state -> int
    16   val assert_bottom: bool -> state -> state
    17   val context_of: state -> context
    18   val theory_of: state -> theory
    19   val map_context: (context -> context) -> state -> state
    20   val add_binds_i: (indexname * term option) list -> state -> state
    21   val put_thms: string * thm list option -> state -> state
    22   val the_facts: state -> thm list
    23   val the_fact: state -> thm
    24   val put_facts: thm list option -> state -> state
    25   val assert_forward: state -> state
    26   val assert_chain: state -> state
    27   val assert_forward_or_chain: state -> state
    28   val assert_backward: state -> state
    29   val assert_no_chain: state -> state
    30   val enter_forward: state -> state
    31   val get_goal: state -> context * (thm list * thm)
    32   val schematic_goal: state -> bool
    33   val show_main_goal: bool ref
    34   val verbose: bool ref
    35   val pretty_state: int -> state -> Pretty.T list
    36   val pretty_goals: bool -> state -> Pretty.T list
    37   val refine: Method.text -> state -> state Seq.seq
    38   val refine_end: Method.text -> state -> state Seq.seq
    39   val refine_insert: thm list -> state -> state
    40   val goal_tac: thm -> int -> tactic
    41   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
    42   val match_bind: (string list * string) list -> state -> state
    43   val match_bind_i: (term list * term) list -> state -> state
    44   val let_bind: (string list * string) list -> state -> state
    45   val let_bind_i: (term list * term) list -> state -> state
    46   val fix: (string * string option * mixfix) list -> state -> state
    47   val fix_i: (string * typ option * mixfix) list -> state -> state
    48   val assm: Assumption.export ->
    49     ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    50   val assm_i: Assumption.export ->
    51     ((string * attribute list) * (term * term list) list) list -> state -> state
    52   val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    53   val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
    54   val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    55   val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
    56   val def: ((string * Attrib.src list) *
    57     ((string * mixfix) * (string * string list))) list -> state -> state
    58   val def_i: ((string * attribute list) *
    59     ((string * mixfix) * (term * term list))) list -> state -> state
    60   val chain: state -> state
    61   val chain_facts: thm list -> state -> state
    62   val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
    63   val note_thmss: ((string * Attrib.src list) *
    64     (thmref * Attrib.src list) list) list -> state -> state
    65   val note_thmss_i: ((string * attribute list) *
    66     (thm list * attribute list) list) list -> state -> state
    67   val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
    68   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
    69   val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
    70   val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
    71   val using: ((thmref * Attrib.src list) list) list -> state -> state
    72   val using_i: ((thm list * attribute list) list) list -> state -> state
    73   val unfolding: ((thmref * Attrib.src list) list) list -> state -> state
    74   val unfolding_i: ((thm list * attribute list) list) list -> state -> state
    75   val invoke_case: string * string option list * Attrib.src list -> state -> state
    76   val invoke_case_i: string * string option list * attribute list -> state -> state
    77   val begin_block: state -> state
    78   val next_block: state -> state
    79   val end_block: state -> state
    80   val proof: Method.text option -> state -> state Seq.seq
    81   val defer: int option -> state -> state Seq.seq
    82   val prefer: int -> state -> state Seq.seq
    83   val apply: Method.text -> state -> state Seq.seq
    84   val apply_end: Method.text -> state -> state Seq.seq
    85   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
    86     (theory -> 'a -> attribute) ->
    87     (context * 'b list -> context * (term list list * (context -> context))) ->
    88     string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
    89     ((string * 'a list) * 'b) list -> state -> state
    90   val local_qed: Method.text option * bool -> state -> state Seq.seq
    91   val theorem: Method.text option -> (thm list list -> context -> context) ->
    92     (string * string list) list list -> context -> state
    93   val theorem_i: Method.text option -> (thm list list -> context -> context) ->
    94     (term * term list) list list -> context -> state
    95   val global_qed: Method.text option * bool -> state -> context
    96   val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
    97   val local_default_proof: state -> state Seq.seq
    98   val local_immediate_proof: state -> state Seq.seq
    99   val local_done_proof: state -> state Seq.seq
   100   val local_skip_proof: bool -> state -> state Seq.seq
   101   val global_terminal_proof: Method.text * Method.text option -> state -> context
   102   val global_default_proof: state -> context
   103   val global_immediate_proof: state -> context
   104   val global_done_proof: state -> context
   105   val global_skip_proof: bool -> state -> context
   106   val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   107     ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   108   val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   109     ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   110   val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   111     ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   112   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   113     ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   114 end;
   115 
   116 structure Proof: PROOF =
   117 struct
   118 
   119 type context = Context.proof;
   120 type method = Method.method;
   121 
   122 
   123 (** proof state **)
   124 
   125 (* datatype state *)
   126 
   127 datatype mode = Forward | Chain | Backward;
   128 
   129 datatype state =
   130   State of node Stack.T
   131 and node =
   132   Node of
   133    {context: context,
   134     facts: thm list option,
   135     mode: mode,
   136     goal: goal option}
   137 and goal =
   138   Goal of
   139    {statement: string * term list list,     (*goal kind and statement, starting with vars*)
   140     using: thm list,                        (*goal facts*)
   141     goal: thm,                              (*subgoals ==> statement*)
   142     before_qed: Method.text option,
   143     after_qed:
   144       (thm list list -> state -> state Seq.seq) *
   145       (thm list list -> context -> context)};
   146 
   147 fun make_goal (statement, using, goal, before_qed, after_qed) =
   148   Goal {statement = statement, using = using, goal = goal,
   149     before_qed = before_qed, after_qed = after_qed};
   150 
   151 fun make_node (context, facts, mode, goal) =
   152   Node {context = context, facts = facts, mode = mode, goal = goal};
   153 
   154 fun map_node f (Node {context, facts, mode, goal}) =
   155   make_node (f (context, facts, mode, goal));
   156 
   157 val init_context =
   158   ProofContext.set_stmt true #> ProofContext.reset_naming;
   159 
   160 fun init ctxt =
   161   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
   162 
   163 fun current (State st) = Stack.top st |> (fn Node node => node);
   164 fun map_current f (State st) = State (Stack.map_top (map_node f) st);
   165 
   166 
   167 
   168 (** basic proof state operations **)
   169 
   170 (* block structure *)
   171 
   172 fun open_block (State st) = State (Stack.push st);
   173 
   174 fun close_block (State st) = State (Stack.pop st)
   175   handle Empty => error "Unbalanced block parentheses";
   176 
   177 fun level (State st) = Stack.level st;
   178 
   179 fun assert_bottom b state =
   180   let val b' = (level state <= 2) in
   181     if b andalso not b' then error "Not at bottom of proof!"
   182     else if not b andalso b' then error "Already at bottom of proof!"
   183     else state
   184   end;
   185 
   186 
   187 (* context *)
   188 
   189 val context_of = #context o current;
   190 val theory_of = ProofContext.theory_of o context_of;
   191 
   192 fun map_context f =
   193   map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   194 
   195 fun map_context_result f state =
   196   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
   197 
   198 val add_binds_i = map_context o ProofContext.add_binds_i;
   199 val put_thms = map_context o ProofContext.put_thms;
   200 
   201 
   202 (* facts *)
   203 
   204 val get_facts = #facts o current;
   205 
   206 fun the_facts state =
   207   (case get_facts state of SOME facts => facts
   208   | NONE => error "No current facts available");
   209 
   210 fun the_fact state =
   211   (case the_facts state of [thm] => thm
   212   | _ => error "Single theorem expected");
   213 
   214 fun put_facts facts =
   215   map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   216   put_thms (AutoBind.thisN, facts);
   217 
   218 fun these_factss more_facts (named_factss, state) =
   219   (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
   220 
   221 fun export_facts inner outer =
   222   (case get_facts inner of
   223     NONE => put_facts NONE outer
   224   | SOME thms =>
   225       thms
   226       |> ProofContext.export (context_of inner) (context_of outer)
   227       |> (fn ths => put_facts (SOME ths) outer));
   228 
   229 
   230 (* mode *)
   231 
   232 val get_mode = #mode o current;
   233 fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
   234 
   235 val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
   236 
   237 fun assert_mode pred state =
   238   let val mode = get_mode state in
   239     if pred mode then state
   240     else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
   241   end;
   242 
   243 val assert_forward = assert_mode (fn mode => mode = Forward);
   244 val assert_chain = assert_mode (fn mode => mode = Chain);
   245 val assert_forward_or_chain = assert_mode (fn mode => mode = Forward orelse mode = Chain);
   246 val assert_backward = assert_mode (fn mode => mode = Backward);
   247 val assert_no_chain = assert_mode (fn mode => mode <> Chain);
   248 
   249 val enter_forward = put_mode Forward;
   250 val enter_chain = put_mode Chain;
   251 val enter_backward = put_mode Backward;
   252 
   253 
   254 (* current goal *)
   255 
   256 fun current_goal state =
   257   (case current state of
   258     {context, goal = SOME (Goal goal), ...} => (context, goal)
   259   | _ => error "No current goal!");
   260 
   261 fun assert_current_goal g state =
   262   let val g' = can current_goal state in
   263     if g andalso not g' then error "No goal in this block!"
   264     else if not g andalso g' then error "Goal present in this block!"
   265     else state
   266   end;
   267 
   268 fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
   269 
   270 val before_qed = #before_qed o #2 o current_goal;
   271 
   272 
   273 (* nested goal *)
   274 
   275 fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) =
   276       let
   277         val Goal {statement, using, goal, before_qed, after_qed} = goal;
   278         val goal' = make_goal (g (statement, using, goal, before_qed, after_qed));
   279       in State (make_node (f context, facts, mode, SOME goal'), nodes) end
   280   | map_goal f g (State (nd, node :: nodes)) =
   281       let val State (node', nodes') = map_goal f g (State (node, nodes))
   282       in map_context f (State (nd, node' :: nodes')) end
   283   | map_goal _ _ state = state;
   284 
   285 fun set_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
   286   (statement, using, goal, before_qed, after_qed));
   287 
   288 fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
   289   (statement, using, goal, before_qed, after_qed));
   290 
   291 local
   292   fun find i state =
   293     (case try current_goal state of
   294       SOME (ctxt, goal) => (ctxt, (i, goal))
   295     | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
   296 in val find_goal = find 0 end;
   297 
   298 fun get_goal state =
   299   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   300   in (ctxt, (using, goal)) end;
   301 
   302 fun schematic_goal state =
   303   let val (_, (_, {statement = (_, propss), ...})) = find_goal state in
   304     exists (exists (Term.exists_subterm Term.is_Var)) propss orelse
   305     exists (exists (Term.exists_type (Term.exists_subtype Term.is_TVar))) propss
   306   end;
   307 
   308 
   309 
   310 (** pretty_state **)
   311 
   312 val show_main_goal = ref false;
   313 val verbose = ProofContext.verbose;
   314 
   315 val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp;
   316 
   317 fun pretty_facts _ _ NONE = []
   318   | pretty_facts s ctxt (SOME ths) =
   319       [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
   320 
   321 fun pretty_state nr state =
   322   let
   323     val {context, facts, mode, goal = _} = current state;
   324     val ref (_, _, bg) = Display.current_goals_markers;
   325 
   326     fun levels_up 0 = ""
   327       | levels_up 1 = "1 level up"
   328       | levels_up i = string_of_int i ^ " levels up";
   329 
   330     fun subgoals 0 = ""
   331       | subgoals 1 = "1 subgoal"
   332       | subgoals n = string_of_int n ^ " subgoals";
   333 
   334     fun description strs =
   335       (case filter_out (equal "") strs of [] => ""
   336       | strs' => enclose " (" ")" (commas strs'));
   337 
   338     fun prt_goal (SOME (ctxt, (i, {statement = _, using, goal, before_qed, after_qed}))) =
   339           pretty_facts "using " ctxt
   340             (if mode <> Backward orelse null using then NONE else SOME using) @
   341           [Pretty.str ("goal" ^
   342             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
   343           pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal
   344       | prt_goal NONE = [];
   345 
   346     val prt_ctxt =
   347       if ! verbose orelse mode = Forward then ProofContext.pretty_context context
   348       else if mode = Backward then ProofContext.pretty_ctxt context
   349       else [];
   350   in
   351     [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
   352       (if ! verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
   353       Pretty.str ""] @
   354     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
   355     (if ! verbose orelse mode = Forward then
   356        pretty_facts "" context facts @ prt_goal (try find_goal state)
   357      else if mode = Chain then pretty_facts "picking " context facts
   358      else prt_goal (try find_goal state))
   359   end;
   360 
   361 fun pretty_goals main state =
   362   let val (ctxt, (_, goal)) = get_goal state
   363   in pretty_goals_local ctxt "" (false, main) (! Display.goals_limit) goal end;
   364 
   365 
   366 
   367 (** proof steps **)
   368 
   369 (* refine via method *)
   370 
   371 local
   372 
   373 fun goalN i = "goal" ^ string_of_int i;
   374 fun goals st = map goalN (1 upto Thm.nprems_of st);
   375 
   376 fun no_goal_cases st = map (rpair NONE) (goals st);
   377 
   378 fun goal_cases st =
   379   RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
   380 
   381 fun apply_method current_context meth_fun state =
   382   let
   383     val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state;
   384     val meth = meth_fun (if current_context then context_of state else goal_ctxt);
   385   in
   386     Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>
   387       state
   388       |> map_goal
   389           (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
   390            ProofContext.add_cases true meth_cases)
   391           (K (statement, using, goal', before_qed, after_qed)))
   392   end;
   393 
   394 fun select_goals n meth state =
   395   state
   396   |> (#2 o #2 o get_goal)
   397   |> ALLGOALS Goal.conjunction_tac
   398   |> Seq.maps (fn goal =>
   399     state
   400     |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
   401     |> Seq.maps meth
   402     |> Seq.maps (fn state' => state'
   403       |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
   404     |> Seq.maps (apply_method true (K Method.succeed)));
   405 
   406 fun apply_text cc text state =
   407   let
   408     val thy = theory_of state;
   409 
   410     fun eval (Method.Basic m) = apply_method cc m
   411       | eval (Method.Source src) = apply_method cc (Method.method thy src)
   412       | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
   413       | eval (Method.Then txts) = Seq.EVERY (map eval txts)
   414       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
   415       | eval (Method.Try txt) = Seq.TRY (eval txt)
   416       | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
   417       | eval (Method.SelectGoals (n, txt)) = select_goals n (eval txt);
   418   in eval text state end;
   419 
   420 in
   421 
   422 val refine = apply_text true;
   423 val refine_end = apply_text false;
   424 
   425 fun refine_insert [] = I
   426   | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
   427 
   428 end;
   429 
   430 
   431 (* refine via sub-proof *)
   432 
   433 fun goal_tac rule =
   434   Goal.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
   435     (Goal.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
   436       if can Logic.unprotect (Logic.strip_assums_concl goal) then
   437         Tactic.etac Drule.protectI i
   438       else all_tac)));
   439 
   440 fun refine_goals print_rule inner raw_rules state =
   441   let
   442     val (outer, (_, goal)) = get_goal state;
   443     fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
   444   in
   445     raw_rules
   446     |> ProofContext.goal_export inner outer
   447     |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
   448   end;
   449 
   450 
   451 (* conclude_goal *)
   452 
   453 fun conclude_goal state goal propss =
   454   let
   455     val thy = theory_of state;
   456     val ctxt = context_of state;
   457     val string_of_term = ProofContext.string_of_term ctxt;
   458     val string_of_thm = ProofContext.string_of_thm ctxt;
   459 
   460     val ngoals = Thm.nprems_of goal;
   461     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
   462         (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
   463           [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
   464 
   465     val extra_hyps = Assumption.extra_hyps ctxt goal;
   466     val _ = null extra_hyps orelse
   467       error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
   468 
   469     val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
   470       handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
   471     val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse
   472       error ("Proved a different theorem:\n" ^ string_of_thm th);
   473   in results end;
   474 
   475 
   476 
   477 (*** structured proof commands ***)
   478 
   479 (** context elements **)
   480 
   481 (* bindings *)
   482 
   483 local
   484 
   485 fun gen_bind bind args state =
   486   state
   487   |> assert_forward
   488   |> map_context (bind args #> snd)
   489   |> put_facts NONE;
   490 
   491 in
   492 
   493 val match_bind = gen_bind (ProofContext.match_bind false);
   494 val match_bind_i = gen_bind (ProofContext.match_bind_i false);
   495 val let_bind = gen_bind (ProofContext.match_bind true);
   496 val let_bind_i = gen_bind (ProofContext.match_bind_i true);
   497 
   498 end;
   499 
   500 
   501 (* fix *)
   502 
   503 local
   504 
   505 fun gen_fix add_fixes args =
   506   assert_forward
   507   #> map_context (snd o add_fixes args)
   508   #> put_facts NONE;
   509 
   510 in
   511 
   512 val fix = gen_fix ProofContext.add_fixes;
   513 val fix_i = gen_fix ProofContext.add_fixes_i;
   514 
   515 end;
   516 
   517 
   518 (* assume etc. *)
   519 
   520 local
   521 
   522 fun gen_assume asm prep_att exp args state =
   523   state
   524   |> assert_forward
   525   |> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args))
   526   |> these_factss [] |> #2;
   527 
   528 in
   529 
   530 val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
   531 val assm_i    = gen_assume ProofContext.add_assms_i (K I);
   532 val assume    = assm Assumption.assume_export;
   533 val assume_i  = assm_i Assumption.assume_export;
   534 val presume   = assm Assumption.presume_export;
   535 val presume_i = assm_i Assumption.presume_export;
   536 
   537 end;
   538 
   539 
   540 (* def *)
   541 
   542 local
   543 
   544 fun gen_def prep_att prep_vars prep_binds args state =
   545   let
   546     val _ = assert_forward state;
   547     val thy = theory_of state;
   548     val ctxt = context_of state;
   549 
   550     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
   551     val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
   552   in
   553     state
   554     |> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
   555     |>> map (fn (x, _, mx) => (x, mx))
   556     |-> (fn vars =>
   557       map_context_result (prep_binds false (map swap raw_rhss))
   558       #-> (fn rhss => map_context_result (LocalDefs.add_defs (vars ~~ (name_atts ~~ rhss)))))
   559     |-> (put_facts o SOME o map (#2 o #2))
   560   end;
   561 
   562 in
   563 
   564 val def = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
   565 val def_i = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
   566 
   567 end;
   568 
   569 
   570 
   571 (** facts **)
   572 
   573 (* chain *)
   574 
   575 val chain =
   576   assert_forward
   577   #> tap the_facts
   578   #> enter_chain;
   579 
   580 fun chain_facts facts =
   581   put_facts (SOME facts)
   582   #> chain;
   583 
   584 
   585 (* note etc. *)
   586 
   587 fun no_binding args = map (pair ("", [])) args;
   588 
   589 local
   590 
   591 fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state =
   592   state
   593   |> assert_forward
   594   |> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args))
   595   |> these_factss (more_facts state)
   596   ||> opt_chain
   597   |> opt_result;
   598 
   599 in
   600 
   601 val note_thmss = gen_thmss (ProofContext.note_thmss "") (K []) I #2 Attrib.attribute;
   602 val note_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) I #2 (K I);
   603 
   604 val from_thmss =
   605   gen_thmss (ProofContext.note_thmss "") (K []) chain #2 Attrib.attribute o no_binding;
   606 val from_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) chain #2 (K I) o no_binding;
   607 
   608 val with_thmss =
   609   gen_thmss (ProofContext.note_thmss "") the_facts chain #2 Attrib.attribute o no_binding;
   610 val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding;
   611 
   612 val local_results =
   613   gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
   614 
   615 fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
   616 
   617 end;
   618 
   619 
   620 (* using/unfolding *)
   621 
   622 local
   623 
   624 fun gen_using f g note prep_atts args state =
   625   state
   626   |> assert_backward
   627   |> map_context_result
   628     (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
   629   |> (fn (named_facts, state') =>
   630     state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
   631       let
   632         val ctxt = context_of state';
   633         val ths = maps snd named_facts;
   634       in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
   635 
   636 fun append_using _ ths using = using @ ths;
   637 fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
   638 val unfold_goals = LocalDefs.unfold_goals;
   639 
   640 in
   641 
   642 val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute;
   643 val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I);
   644 val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute;
   645 val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I);
   646 
   647 end;
   648 
   649 
   650 (* case *)
   651 
   652 local
   653 
   654 fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   655   let
   656     val atts = map (prep_att (theory_of state)) raw_atts;
   657     val (asms, state') = state |> map_context_result (fn ctxt =>
   658       ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
   659     val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
   660   in
   661     state'
   662     |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
   663     |> assume_i assumptions
   664     |> add_binds_i AutoBind.no_facts
   665     |> map_context (ProofContext.restore_naming (context_of state))
   666     |> `the_facts |-> (fn thms => note_thmss_i [((name, []), [(thms, [])])])
   667   end;
   668 
   669 in
   670 
   671 val invoke_case = gen_invoke_case Attrib.attribute;
   672 val invoke_case_i = gen_invoke_case (K I);
   673 
   674 end;
   675 
   676 
   677 
   678 (** proof structure **)
   679 
   680 (* blocks *)
   681 
   682 val begin_block =
   683   assert_forward
   684   #> open_block
   685   #> put_goal NONE
   686   #> open_block;
   687 
   688 val next_block =
   689   assert_forward
   690   #> close_block
   691   #> open_block
   692   #> put_goal NONE
   693   #> put_facts NONE;
   694 
   695 fun end_block state =
   696   state
   697   |> assert_forward
   698   |> close_block
   699   |> assert_current_goal false
   700   |> close_block
   701   |> export_facts state;
   702 
   703 
   704 (* sub-proofs *)
   705 
   706 fun proof opt_text =
   707   assert_backward
   708   #> refine (the_default Method.default_text opt_text)
   709   #> Seq.map (using_facts [] #> enter_forward);
   710 
   711 fun end_proof bot txt =
   712   assert_forward
   713   #> assert_bottom bot
   714   #> close_block
   715   #> assert_current_goal true
   716   #> using_facts []
   717   #> `before_qed #-> (refine o the_default Method.succeed_text)
   718   #> Seq.maps (refine (Method.finish_text txt));
   719 
   720 
   721 (* unstructured refinement *)
   722 
   723 fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
   724 fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
   725 
   726 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
   727 fun apply_end text = assert_forward #> refine_end text;
   728 
   729 
   730 
   731 (** goals **)
   732 
   733 (* generic goals *)
   734 
   735 local
   736 
   737 fun implicit_vars dest add props =
   738   let
   739     val (explicit_vars, props') = take_prefix (can dest) props |>> map dest;
   740     val vars = rev (subtract (op =) explicit_vars (fold add props []));
   741     val _ =
   742       if null vars then ()
   743       else warning ("Goal statement contains unbound schematic variable(s): " ^
   744         commas_quote (map (Term.string_of_vname o fst) vars));
   745   in (rev vars, props') end;
   746 
   747 fun refine_terms n =
   748   refine (Method.Basic (K (Method.RAW_METHOD
   749     (K (HEADGOAL (PRECISE_CONJUNCTS n
   750       (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
   751   #> Seq.hd;
   752 
   753 in
   754 
   755 fun generic_goal prepp kind before_qed after_qed raw_propp state =
   756   let
   757     val thy = theory_of state;
   758     val chaining = can assert_chain state;
   759 
   760     val ((propss, after_ctxt), goal_state) =
   761       state
   762       |> assert_forward_or_chain
   763       |> enter_forward
   764       |> open_block
   765       |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
   766     val props = flat propss;
   767 
   768     val (_, props') =
   769       implicit_vars (dest_TVar o Logic.dest_type o Logic.dest_term) Term.add_tvars props;
   770     val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
   771 
   772     val propss' = map (Logic.mk_term o Var) vars :: propss;
   773     val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
   774     val after_qed' = after_qed |>> (fn after_local =>
   775       fn results => map_context after_ctxt #> after_local results);
   776   in
   777     goal_state
   778     |> map_context (init_context #> Variable.set_body true)
   779     |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
   780     |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
   781     |> map_context (ProofContext.auto_bind_goal props)
   782     |> chaining ? (`the_facts #-> using_facts)
   783     |> put_facts NONE
   784     |> open_block
   785     |> put_goal NONE
   786     |> enter_backward
   787     |> not (null vars) ? refine_terms (length propss')
   788     |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   789   end;
   790 
   791 fun generic_qed state =
   792   let
   793     val (goal_ctxt, {statement = (_, stmt), using = _, goal, before_qed = _, after_qed}) =
   794       current_goal state;
   795     val outer_state = state |> close_block;
   796     val outer_ctxt = context_of outer_state;
   797 
   798     val props =
   799       flat (tl stmt)
   800       |> Variable.exportT_terms goal_ctxt outer_ctxt;
   801     val results =
   802       tl (conclude_goal state goal stmt)
   803       |> burrow (ProofContext.export goal_ctxt outer_ctxt);
   804   in
   805     outer_state
   806     |> map_context (ProofContext.auto_bind_facts props)
   807     |> pair (after_qed, results)
   808   end;
   809 
   810 end;
   811 
   812 
   813 (* local goals *)
   814 
   815 fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
   816   let
   817     val thy = theory_of state;
   818     val ((names, attss), propp) =
   819       Attrib.map_specs (prep_att thy) stmt |> split_list |>> split_list;
   820 
   821     fun after_qed' results =
   822       local_results ((names ~~ attss) ~~ results)
   823       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
   824       #> after_qed results;
   825   in
   826     state
   827     |> generic_goal prepp kind before_qed (after_qed', K I) propp
   828     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   829   end;
   830 
   831 fun local_qed txt =
   832   end_proof false txt #>
   833   Seq.maps (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
   834 
   835 
   836 (* global goals *)
   837 
   838 fun global_goal prepp before_qed after_qed propp ctxt =
   839   init ctxt
   840   |> generic_goal (prepp #> ProofContext.auto_fixes) ""
   841     before_qed (K Seq.single, after_qed) propp;
   842 
   843 val theorem = global_goal ProofContext.bind_propp_schematic;
   844 val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
   845 
   846 fun check_result msg sq =
   847   (case Seq.pull sq of
   848     NONE => error msg
   849   | SOME (s', sq') => Seq.cons s' sq');
   850 
   851 fun global_qeds txt =
   852   end_proof true txt
   853   #> Seq.map (generic_qed #> (fn (((_, after_qed), results), state) =>
   854     after_qed results (context_of state)))
   855   |> Seq.DETERM;   (*backtracking may destroy theory!*)
   856 
   857 fun global_qed txt =
   858   global_qeds txt
   859   #> check_result "Failed to finish proof"
   860   #> Seq.hd;
   861 
   862 
   863 (* concluding steps *)
   864 
   865 fun local_terminal_proof (text, opt_text) =
   866   proof (SOME text) #> Seq.maps (local_qed (opt_text, true));
   867 
   868 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
   869 val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
   870 val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
   871 fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
   872 
   873 fun global_term_proof immed (text, opt_text) =
   874   proof (SOME text)
   875   #> check_result "Terminal proof method failed"
   876   #> Seq.maps (global_qeds (opt_text, immed))
   877   #> check_result "Failed to finish proof (after successful terminal method)"
   878   #> Seq.hd;
   879 
   880 val global_terminal_proof = global_term_proof true;
   881 val global_default_proof = global_terminal_proof (Method.default_text, NONE);
   882 val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
   883 val global_done_proof = global_term_proof false (Method.done_text, NONE);
   884 fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
   885 
   886 
   887 (* common goal statements *)
   888 
   889 local
   890 
   891 fun gen_have prep_att prepp before_qed after_qed stmt int =
   892   local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt;
   893 
   894 fun gen_show prep_att prepp before_qed after_qed stmt int state =
   895   let
   896     val testing = ref false;
   897     val rule = ref (NONE: thm option);
   898     fun fail_msg ctxt =
   899       "Local statement will fail to solve any pending goal" ::
   900       (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
   901       |> cat_lines;
   902 
   903     fun print_results ctxt res =
   904       if ! testing then () else ProofDisplay.print_results int ctxt res;
   905     fun print_rule ctxt th =
   906       if ! testing then rule := SOME th
   907       else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
   908       else ();
   909     val test_proof =
   910       (Seq.pull oo local_skip_proof) true
   911       |> setmp testing true
   912       |> setmp proofs 0
   913       |> capture;
   914 
   915     fun after_qed' results =
   916       refine_goals print_rule (context_of state) (flat results)
   917       #> Seq.maps (after_qed results);
   918   in
   919     state
   920     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
   921     |> int ? (fn goal_state =>
   922       (case test_proof goal_state of
   923         Result (SOME _) => goal_state
   924       | Result NONE => error (fail_msg (context_of goal_state))
   925       | Exn Interrupt => raise Interrupt
   926       | Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state))))
   927   end;
   928 
   929 in
   930 
   931 val have = gen_have Attrib.attribute ProofContext.bind_propp;
   932 val have_i = gen_have (K I) ProofContext.bind_propp_i;
   933 val show = gen_show Attrib.attribute ProofContext.bind_propp;
   934 val show_i = gen_show (K I) ProofContext.bind_propp_i;
   935 
   936 end;
   937 
   938 end;