src/Pure/Isar/proof.ML
changeset 6848 3d82756e1af5
parent 6798 f6bc583a5776
child 6853 80f88b762816
--- a/src/Pure/Isar/proof.ML	Mon Jun 28 21:44:19 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jun 28 21:46:33 1999 +0200
@@ -24,8 +24,7 @@
   val print_state: state -> unit
   val level: state -> int
   type method
-  val method: (thm list -> thm ->
-    (thm * (indexname * term) list * (string * thm list) list) Seq.seq) -> method
+  val method: (thm list -> tactic) -> method
   val refine: (context -> method) -> state -> state Seq.seq
   val bind: (indexname * string) list -> state -> state
   val bind_i: (indexname * term) list -> state -> state
@@ -33,8 +32,10 @@
   val match_bind_i: (term list * term) list -> state -> state
   val have_thmss: string -> context attribute list ->
     (thm list * context attribute list) list -> state -> state
-  val assume: string -> context attribute list -> (string * string list) list -> state -> state
-  val assume_i: string -> context attribute list -> (term * term list) list -> state -> state
+  val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
+    -> state -> state
+  val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
+    -> state -> state
   val fix: (string * string option) list -> state -> state
   val fix_i: (string * typ) list -> state -> state
   val theorem: bstring -> theory attribute list -> string * string list -> theory -> state
@@ -84,12 +85,13 @@
   fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
 
 type goal =
- (kind *                (*result kind*)
-  string *              (*result name*)
-  cterm list *          (*result assumptions*)
-  term) *               (*result statement*)
- (thm list *            (*use facts*)
-  thm);                 (*goal: subgoals ==> statement*)
+ (kind *               		(*result kind*)
+  string *                      (*result name*)
+  cterm list *			(*result assumptions*)
+  (int -> tactic) list *      	(*tactics to solve result assumptions*)
+  term) *                       (*result statement*)
+ (thm list *                    (*use facts*)
+  thm);                         (*goal: subgoals ==> statement*)
 
 
 (* type mode *)
@@ -168,6 +170,8 @@
     [fact] => fact
   | _ => raise STATE ("Single fact expected", state));
 
+fun assert_facts state = (the_facts state; state);
+
 fun put_facts facts state =
   state
   |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
@@ -262,18 +266,19 @@
     fun levels_up 0 = ""
       | levels_up i = " (" ^ string_of_int i ^ " levels up)";
 
-    fun print_goal (i, ((kind, name, _, _), (goal_facts, thm))) =
+    fun print_goal (i, ((kind, name, _, _, _), (goal_facts, thm))) =
       (print_facts "Using" (if null goal_facts then None else Some goal_facts);
         writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
         Locale.print_goals_marker begin_goal (! goals_limit) thm);
+
+    val ctxt_strings = ProofContext.strings_of_context context;
   in
     writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
     writeln "";
     writeln (mode_name mode ^ " mode");
     writeln "";
     if ! verbose orelse mode = Forward then
-      (ProofContext.print_context context;
-        writeln "";
+      (if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
         print_facts "Current" facts;
         print_goal (find_goal 0 state))
     else if mode = ForwardChain then print_facts "Picking" facts
@@ -286,14 +291,7 @@
 
 (* datatype method *)
 
-datatype method = Method of
-  thm list ->                           (*use facts*)
-  thm                                   (*goal: subgoals ==> statement*)
-    -> (thm *                           (*refined goal*)
-       (indexname * term) list *        (*new bindings*)
-       (string * thm list) list)        (*new thms*)
-         Seq.seq;
-
+datatype method = Method of thm list -> tactic;
 val method = Method;
 
 
@@ -304,17 +302,15 @@
   else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
 
 fun refine meth_fun (state as State ({context, ...}, _)) =
-      let
-        val Method meth = meth_fun context;
-        val (_, (result, (facts, thm))) = find_goal 0 state;
+  let
+    val Method meth = meth_fun context;
+    val (_, (result, (facts, thm))) = find_goal 0 state;
 
-        fun refn (thm', new_binds, new_thms) =
-          state
-          |> check_sign (sign_of_thm thm')
-          |> map_goal (K (result, (facts, thm')))
-          |> add_binds new_binds
-          |> put_thmss new_thms;
-      in Seq.map refn (meth facts thm) end;
+    fun refn thm' =
+      state
+      |> check_sign (Thm.sign_of_thm thm')
+      |> map_goal (K (result, (facts, thm')));
+  in Seq.map refn (meth facts thm) end;
 
 
 (* prepare result *)
@@ -344,6 +340,7 @@
 fun implies_elim_hyps thm =
   foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));
 
+
 fun prep_result state asms t raw_thm =
   let
     val ctxt = context_of state;
@@ -401,10 +398,16 @@
 
 (* solve goal *)
 
-fun solve_goal rule state =
+fun REV_RANGE _ [] = all_tac
+  | REV_RANGE k (tac :: tacs) = tac k THEN REV_RANGE (k - 1) tacs;
+
+fun solve_goal rule tacs state =
   let
+    val rev_tacs = rev tacs;
+    val n = length rev_tacs - 1;
+
     val (_, (result, (facts, thm))) = find_goal 0 state;
-    val thms' = FIRSTGOAL (rtac rule THEN_ALL_NEW (TRY o assume_tac)) thm;
+    val thms' = FIRSTGOAL (rtac rule THEN' (fn i => REV_RANGE (i + n) rev_tacs)) thm;
   in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
 
 
@@ -451,10 +454,10 @@
 
 (* assume *)
 
-fun gen_assume f name atts props state =
+fun gen_assume f tac name atts props state =
   state
   |> assert_forward
-  |> map_context_result (f (PureThy.default_name name) atts props)
+  |> map_context_result (f tac (PureThy.default_name name) atts props)
   |> (fn (st, (facts, prems)) =>
     (st, facts)
     |> these_facts
@@ -472,6 +475,7 @@
 fun chain state =
   state
   |> assert_forward
+  |> assert_facts
   |> enter_forward_chain;
 
 fun from_facts facts state =
@@ -492,14 +496,17 @@
       |> map_context_result (fn c => prepp (c, raw_propp));
     val cterm_of = Thm.cterm_of (sign_of state);
 
-    val casms = ProofContext.assumptions (context_of state');
+    val (casms, asm_tacs) = Library.split_list (ProofContext.assumptions (context_of state'));
     val cprems = map cterm_of (Logic.strip_imp_prems concl);
+    val prem_tacs = replicate (length cprems) (K all_tac);
+
     val prop = Logic.list_implies (map Thm.term_of casms, concl);
     val cprop = cterm_of prop;
     val thm = Drule.mk_triv_goal cprop;
   in
     state'
-    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, prop), ([], thm)))
+    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems,
+        asm_tacs @ prem_tacs, prop), ([], thm)))
     |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block
@@ -604,11 +611,11 @@
 
 fun finish_local print_result state =
   let
-    val ((kind, name, asms, t), (_, raw_thm)) = current_goal state;
+    val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
     val (result, result_prop) = prep_result state asms t raw_thm;
     val (atts, opt_solve) =
       (case kind of
-        Goal atts => (atts, solve_goal result)
+        Goal atts => (atts, solve_goal result tacs)
       | Aux atts => (atts, Seq.single)
       | _ => raise STATE ("No local goal!", state));
   in
@@ -630,7 +637,7 @@
 
 fun finish_global alt_name alt_atts state =
   let
-    val ((kind, def_name, asms, t), (_, raw_thm)) = current_goal state;
+    val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
     val result = final_result state (#1 (prep_result state asms t raw_thm));
 
     val name = if_none alt_name def_name;