src/Pure/Isar/proof.ML
changeset 6848 3d82756e1af5
parent 6798 f6bc583a5776
child 6853 80f88b762816
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 28 21:44:19 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Jun 28 21:46:33 1999 +0200
     1.3 @@ -24,8 +24,7 @@
     1.4    val print_state: state -> unit
     1.5    val level: state -> int
     1.6    type method
     1.7 -  val method: (thm list -> thm ->
     1.8 -    (thm * (indexname * term) list * (string * thm list) list) Seq.seq) -> method
     1.9 +  val method: (thm list -> tactic) -> method
    1.10    val refine: (context -> method) -> state -> state Seq.seq
    1.11    val bind: (indexname * string) list -> state -> state
    1.12    val bind_i: (indexname * term) list -> state -> state
    1.13 @@ -33,8 +32,10 @@
    1.14    val match_bind_i: (term list * term) list -> state -> state
    1.15    val have_thmss: string -> context attribute list ->
    1.16      (thm list * context attribute list) list -> state -> state
    1.17 -  val assume: string -> context attribute list -> (string * string list) list -> state -> state
    1.18 -  val assume_i: string -> context attribute list -> (term * term list) list -> state -> state
    1.19 +  val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    1.20 +    -> state -> state
    1.21 +  val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
    1.22 +    -> state -> state
    1.23    val fix: (string * string option) list -> state -> state
    1.24    val fix_i: (string * typ) list -> state -> state
    1.25    val theorem: bstring -> theory attribute list -> string * string list -> theory -> state
    1.26 @@ -84,12 +85,13 @@
    1.27    fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
    1.28  
    1.29  type goal =
    1.30 - (kind *                (*result kind*)
    1.31 -  string *              (*result name*)
    1.32 -  cterm list *          (*result assumptions*)
    1.33 -  term) *               (*result statement*)
    1.34 - (thm list *            (*use facts*)
    1.35 -  thm);                 (*goal: subgoals ==> statement*)
    1.36 + (kind *               		(*result kind*)
    1.37 +  string *                      (*result name*)
    1.38 +  cterm list *			(*result assumptions*)
    1.39 +  (int -> tactic) list *      	(*tactics to solve result assumptions*)
    1.40 +  term) *                       (*result statement*)
    1.41 + (thm list *                    (*use facts*)
    1.42 +  thm);                         (*goal: subgoals ==> statement*)
    1.43  
    1.44  
    1.45  (* type mode *)
    1.46 @@ -168,6 +170,8 @@
    1.47      [fact] => fact
    1.48    | _ => raise STATE ("Single fact expected", state));
    1.49  
    1.50 +fun assert_facts state = (the_facts state; state);
    1.51 +
    1.52  fun put_facts facts state =
    1.53    state
    1.54    |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
    1.55 @@ -262,18 +266,19 @@
    1.56      fun levels_up 0 = ""
    1.57        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
    1.58  
    1.59 -    fun print_goal (i, ((kind, name, _, _), (goal_facts, thm))) =
    1.60 +    fun print_goal (i, ((kind, name, _, _, _), (goal_facts, thm))) =
    1.61        (print_facts "Using" (if null goal_facts then None else Some goal_facts);
    1.62          writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
    1.63          Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.64 +
    1.65 +    val ctxt_strings = ProofContext.strings_of_context context;
    1.66    in
    1.67      writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
    1.68      writeln "";
    1.69      writeln (mode_name mode ^ " mode");
    1.70      writeln "";
    1.71      if ! verbose orelse mode = Forward then
    1.72 -      (ProofContext.print_context context;
    1.73 -        writeln "";
    1.74 +      (if null ctxt_strings then () else (seq writeln ctxt_strings; writeln "");
    1.75          print_facts "Current" facts;
    1.76          print_goal (find_goal 0 state))
    1.77      else if mode = ForwardChain then print_facts "Picking" facts
    1.78 @@ -286,14 +291,7 @@
    1.79  
    1.80  (* datatype method *)
    1.81  
    1.82 -datatype method = Method of
    1.83 -  thm list ->                           (*use facts*)
    1.84 -  thm                                   (*goal: subgoals ==> statement*)
    1.85 -    -> (thm *                           (*refined goal*)
    1.86 -       (indexname * term) list *        (*new bindings*)
    1.87 -       (string * thm list) list)        (*new thms*)
    1.88 -         Seq.seq;
    1.89 -
    1.90 +datatype method = Method of thm list -> tactic;
    1.91  val method = Method;
    1.92  
    1.93  
    1.94 @@ -304,17 +302,15 @@
    1.95    else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
    1.96  
    1.97  fun refine meth_fun (state as State ({context, ...}, _)) =
    1.98 -      let
    1.99 -        val Method meth = meth_fun context;
   1.100 -        val (_, (result, (facts, thm))) = find_goal 0 state;
   1.101 +  let
   1.102 +    val Method meth = meth_fun context;
   1.103 +    val (_, (result, (facts, thm))) = find_goal 0 state;
   1.104  
   1.105 -        fun refn (thm', new_binds, new_thms) =
   1.106 -          state
   1.107 -          |> check_sign (sign_of_thm thm')
   1.108 -          |> map_goal (K (result, (facts, thm')))
   1.109 -          |> add_binds new_binds
   1.110 -          |> put_thmss new_thms;
   1.111 -      in Seq.map refn (meth facts thm) end;
   1.112 +    fun refn thm' =
   1.113 +      state
   1.114 +      |> check_sign (Thm.sign_of_thm thm')
   1.115 +      |> map_goal (K (result, (facts, thm')));
   1.116 +  in Seq.map refn (meth facts thm) end;
   1.117  
   1.118  
   1.119  (* prepare result *)
   1.120 @@ -344,6 +340,7 @@
   1.121  fun implies_elim_hyps thm =
   1.122    foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));
   1.123  
   1.124 +
   1.125  fun prep_result state asms t raw_thm =
   1.126    let
   1.127      val ctxt = context_of state;
   1.128 @@ -401,10 +398,16 @@
   1.129  
   1.130  (* solve goal *)
   1.131  
   1.132 -fun solve_goal rule state =
   1.133 +fun REV_RANGE _ [] = all_tac
   1.134 +  | REV_RANGE k (tac :: tacs) = tac k THEN REV_RANGE (k - 1) tacs;
   1.135 +
   1.136 +fun solve_goal rule tacs state =
   1.137    let
   1.138 +    val rev_tacs = rev tacs;
   1.139 +    val n = length rev_tacs - 1;
   1.140 +
   1.141      val (_, (result, (facts, thm))) = find_goal 0 state;
   1.142 -    val thms' = FIRSTGOAL (rtac rule THEN_ALL_NEW (TRY o assume_tac)) thm;
   1.143 +    val thms' = FIRSTGOAL (rtac rule THEN' (fn i => REV_RANGE (i + n) rev_tacs)) thm;
   1.144    in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
   1.145  
   1.146  
   1.147 @@ -451,10 +454,10 @@
   1.148  
   1.149  (* assume *)
   1.150  
   1.151 -fun gen_assume f name atts props state =
   1.152 +fun gen_assume f tac name atts props state =
   1.153    state
   1.154    |> assert_forward
   1.155 -  |> map_context_result (f (PureThy.default_name name) atts props)
   1.156 +  |> map_context_result (f tac (PureThy.default_name name) atts props)
   1.157    |> (fn (st, (facts, prems)) =>
   1.158      (st, facts)
   1.159      |> these_facts
   1.160 @@ -472,6 +475,7 @@
   1.161  fun chain state =
   1.162    state
   1.163    |> assert_forward
   1.164 +  |> assert_facts
   1.165    |> enter_forward_chain;
   1.166  
   1.167  fun from_facts facts state =
   1.168 @@ -492,14 +496,17 @@
   1.169        |> map_context_result (fn c => prepp (c, raw_propp));
   1.170      val cterm_of = Thm.cterm_of (sign_of state);
   1.171  
   1.172 -    val casms = ProofContext.assumptions (context_of state');
   1.173 +    val (casms, asm_tacs) = Library.split_list (ProofContext.assumptions (context_of state'));
   1.174      val cprems = map cterm_of (Logic.strip_imp_prems concl);
   1.175 +    val prem_tacs = replicate (length cprems) (K all_tac);
   1.176 +
   1.177      val prop = Logic.list_implies (map Thm.term_of casms, concl);
   1.178      val cprop = cterm_of prop;
   1.179      val thm = Drule.mk_triv_goal cprop;
   1.180    in
   1.181      state'
   1.182 -    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, prop), ([], thm)))
   1.183 +    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems,
   1.184 +        asm_tacs @ prem_tacs, prop), ([], thm)))
   1.185      |> auto_bind_goal prop
   1.186      |> (if is_chain state then use_facts else reset_facts)
   1.187      |> new_block
   1.188 @@ -604,11 +611,11 @@
   1.189  
   1.190  fun finish_local print_result state =
   1.191    let
   1.192 -    val ((kind, name, asms, t), (_, raw_thm)) = current_goal state;
   1.193 +    val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
   1.194      val (result, result_prop) = prep_result state asms t raw_thm;
   1.195      val (atts, opt_solve) =
   1.196        (case kind of
   1.197 -        Goal atts => (atts, solve_goal result)
   1.198 +        Goal atts => (atts, solve_goal result tacs)
   1.199        | Aux atts => (atts, Seq.single)
   1.200        | _ => raise STATE ("No local goal!", state));
   1.201    in
   1.202 @@ -630,7 +637,7 @@
   1.203  
   1.204  fun finish_global alt_name alt_atts state =
   1.205    let
   1.206 -    val ((kind, def_name, asms, t), (_, raw_thm)) = current_goal state;
   1.207 +    val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
   1.208      val result = final_result state (#1 (prep_result state asms t raw_thm));
   1.209  
   1.210      val name = if_none alt_name def_name;