src/Pure/Isar/proof.ML
changeset 6932 77c14313af51
parent 6896 4bdc3600ddae
child 6950 ab6d35b7283f
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 08 18:32:43 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 08 18:34:59 1999 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    type method
     1.5    val method: (thm list -> tactic) -> method
     1.6    val refine: (context -> method) -> state -> state Seq.seq
     1.7 +  val export_thm: context -> thm -> thm
     1.8    val bind: (indexname * string) list -> state -> state
     1.9    val bind_i: (indexname * term) list -> state -> state
    1.10    val match_bind: (string list * string) list -> state -> state
    1.11 @@ -35,29 +36,46 @@
    1.12    val have_thmss: thm list -> string -> context attribute list ->
    1.13      (thm list * context attribute list) list -> state -> state
    1.14    val simple_have_thms: string -> thm list -> state -> state
    1.15 -  val assume: (int -> tactic) -> string -> context attribute list -> (string * string list) list
    1.16 -    -> state -> state
    1.17 -  val assume_i: (int -> tactic) -> string -> context attribute list -> (term * term list) list
    1.18 -    -> state -> state
    1.19    val fix: (string * string option) list -> state -> state
    1.20    val fix_i: (string * typ) list -> state -> state
    1.21 -  val theorem: bstring -> theory attribute list -> string * string list -> theory -> state
    1.22 -  val theorem_i: bstring -> theory attribute list -> term * term list -> theory -> state
    1.23 -  val lemma: bstring -> theory attribute list -> string * string list -> theory -> state
    1.24 -  val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> state
    1.25 +  val assm: (int -> tactic) * (int -> tactic) -> string -> context attribute list
    1.26 +    -> (string * (string list * string list)) list -> state -> state
    1.27 +  val assm_i: (int -> tactic) * (int -> tactic) -> string -> context attribute list
    1.28 +    -> (term * (term list * term list)) list -> state -> state
    1.29 +  val assume: string -> context attribute list -> (string * (string list * string list)) list
    1.30 +    -> state -> state
    1.31 +  val assume_i: string -> context attribute list -> (term * (term list * term list)) list
    1.32 +    -> state -> state
    1.33 +  val presume: string -> context attribute list -> (string * (string list * string list)) list
    1.34 +    -> state -> state
    1.35 +  val presume_i: string -> context attribute list -> (term * (term list * term list)) list
    1.36 +    -> state -> state
    1.37 +  val theorem: bstring -> theory attribute list -> string * (string list * string list)
    1.38 +    -> theory -> state
    1.39 +  val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
    1.40 +    -> theory -> state
    1.41 +  val lemma: bstring -> theory attribute list -> string * (string list * string list)
    1.42 +    -> theory -> state
    1.43 +  val lemma_i: bstring -> theory attribute list -> term * (term list * term list)
    1.44 +    -> theory -> state
    1.45    val chain: state -> state
    1.46 +  val export_chain: state -> state Seq.seq
    1.47    val from_facts: thm list -> state -> state
    1.48 -  val show: string -> context attribute list -> string * string list -> state -> state
    1.49 -  val show_i: string -> context attribute list -> term * term list -> state -> state
    1.50 -  val have: string -> context attribute list -> string * string list -> state -> state
    1.51 -  val have_i: string -> context attribute list -> term * term list -> state -> state
    1.52 +  val show: string -> context attribute list -> string * (string list * string list)
    1.53 +    -> state -> state
    1.54 +  val show_i: string -> context attribute list -> term * (term list * term list)
    1.55 +    -> state -> state
    1.56 +  val have: string -> context attribute list -> string * (string list * string list)
    1.57 +    -> state -> state
    1.58 +  val have_i: string -> context attribute list -> term * (term list * term list)
    1.59 +    -> state -> state
    1.60    val at_bottom: state -> bool
    1.61    val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
    1.62      -> state -> state Seq.seq
    1.63    val global_qed: (state -> state Seq.seq) -> bstring option -> theory attribute list option
    1.64      -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    1.65    val begin_block: state -> state
    1.66 -  val end_block: state -> state
    1.67 +  val end_block: state -> state Seq.seq
    1.68    val next_block: state -> state
    1.69  end;
    1.70  
    1.71 @@ -88,13 +106,11 @@
    1.72    fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
    1.73  
    1.74  type goal =
    1.75 - (kind *               		(*result kind*)
    1.76 -  string *                      (*result name*)
    1.77 -  cterm list *			(*result assumptions*)
    1.78 -  (int -> tactic) list *      	(*tactics to solve result assumptions*)
    1.79 -  term) *                       (*result statement*)
    1.80 - (thm list *                    (*use facts*)
    1.81 -  thm);                         (*goal: subgoals ==> statement*)
    1.82 + (kind *        (*result kind*)
    1.83 +  string *      (*result name*)
    1.84 +  term) *       (*result statement*)
    1.85 + (thm list *    (*use facts*)
    1.86 +  thm);         (*goal: subgoals ==> statement*)
    1.87  
    1.88  
    1.89  (* type mode *)
    1.90 @@ -166,6 +182,7 @@
    1.91  val auto_bind_facts = map_context oo ProofContext.auto_bind_facts;
    1.92  val put_thms = map_context o ProofContext.put_thms;
    1.93  val put_thmss = map_context o ProofContext.put_thmss;
    1.94 +val assumptions = ProofContext.assumptions o context_of;
    1.95  
    1.96  
    1.97  (* facts *)
    1.98 @@ -179,6 +196,7 @@
    1.99    | _ => raise STATE ("Single fact expected", state));
   1.100  
   1.101  fun assert_facts state = (the_facts state; state);
   1.102 +fun get_facts (State ({facts, ...}, _)) = facts;
   1.103  
   1.104  fun put_facts facts state =
   1.105    state
   1.106 @@ -193,12 +211,11 @@
   1.107    |> put_thms (name, facts);
   1.108  
   1.109  fun these_facts (state, ths) = have_facts ths state;
   1.110 -fun fetch_facts (State ({facts, ...}, _)) = put_facts facts;
   1.111  
   1.112  
   1.113  (* goal *)
   1.114  
   1.115 -fun find_goal i (State ({goal = Some goal, ...}, _)) = (i, goal)
   1.116 +fun find_goal i (state as State ({goal = Some goal, ...}, _)) = (context_of state, (i, goal))
   1.117    | find_goal i (State ({goal = None, ...}, node :: nodes)) =
   1.118        find_goal (i + 1) (State (node, nodes))
   1.119    | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state;
   1.120 @@ -267,16 +284,17 @@
   1.121  
   1.122  fun print_facts _ None = ()
   1.123    | print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:")
   1.124 -      (map (setmp Display.show_hyps false Display.pretty_thm) ths));
   1.125 +      (map Display.pretty_thm_no_hyps ths));
   1.126  
   1.127  fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   1.128    let
   1.129      val ref (_, _, begin_goal) = Goals.current_goals_markers;
   1.130  
   1.131      fun levels_up 0 = ""
   1.132 +      | levels_up 1 = " (1 level up)"
   1.133        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
   1.134  
   1.135 -    fun print_goal (i, ((kind, name, _, _, _), (goal_facts, thm))) =
   1.136 +    fun print_goal (_, (i, ((kind, name, _), (goal_facts, thm)))) =
   1.137        (print_facts "Using" (if null goal_facts then None else Some goal_facts);
   1.138          writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
   1.139          Locale.print_goals_marker begin_goal (! goals_limit) thm);
   1.140 @@ -314,7 +332,7 @@
   1.141  fun refine meth_fun (state as State ({context, ...}, _)) =
   1.142    let
   1.143      val Method meth = meth_fun context;
   1.144 -    val (_, (result, (facts, thm))) = find_goal 0 state;
   1.145 +    val (_, (_, (result, (facts, thm)))) = find_goal 0 state;
   1.146  
   1.147      fun refn thm' =
   1.148        state
   1.149 @@ -323,9 +341,11 @@
   1.150    in Seq.map refn (meth facts thm) end;
   1.151  
   1.152  
   1.153 -(* prepare result *)
   1.154 +(* export *)
   1.155  
   1.156 -fun varify_frees names thm =
   1.157 +local
   1.158 +
   1.159 +fun varify_frees fixes thm =
   1.160    let
   1.161      fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
   1.162        | get_free _ (opt, _) = opt;
   1.163 @@ -333,25 +353,82 @@
   1.164      fun find_free t x = foldl_aterms (get_free x) (None, t);
   1.165  
   1.166      val {sign, prop, ...} = Thm.rep_thm thm;
   1.167 -    val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names);
   1.168 +    val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
   1.169    in
   1.170      thm
   1.171      |> Drule.forall_intr_list frees
   1.172      |> Drule.forall_elim_vars 0
   1.173    end;
   1.174  
   1.175 -fun varify_tfrees thm =
   1.176 +fun most_general_varify_tfrees thm =
   1.177    let
   1.178      val {hyps, prop, ...} = Thm.rep_thm thm;
   1.179      val frees = foldr Term.add_term_frees (prop :: hyps, []);
   1.180      val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
   1.181    in thm |> Thm.varifyT' leave_tfrees end;
   1.182  
   1.183 -fun implies_elim_hyps thm =
   1.184 -  foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));
   1.185 +fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
   1.186 +  | diff_context inner (Some outer) =
   1.187 +      (ProofContext.fixed_names inner \\ ProofContext.fixed_names outer,
   1.188 +        Library.drop (length (ProofContext.assumptions outer), ProofContext.assumptions inner));
   1.189 +
   1.190 +in
   1.191 +
   1.192 +fun export fixes casms thm =
   1.193 +  thm
   1.194 +  |> Drule.implies_intr_list casms
   1.195 +  |> varify_frees fixes
   1.196 +  |> most_general_varify_tfrees;
   1.197 +
   1.198 +fun export_wrt inner opt_outer =
   1.199 +  let
   1.200 +    val (fixes, asms) = diff_context inner opt_outer;
   1.201 +    val casms = map #1 asms;
   1.202 +    val tacs = map #2 asms;
   1.203 +  in (export fixes casms, tacs) end;
   1.204 +
   1.205 +end;
   1.206  
   1.207  
   1.208 -fun prep_result state asms t raw_thm =
   1.209 +(* export results *)
   1.210 +
   1.211 +fun RANGE [] _ = all_tac
   1.212 +  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
   1.213 +
   1.214 +fun export_goal raw_rule inner_state state =
   1.215 +  let
   1.216 +    val (outer, (_, (result, (facts, thm)))) = find_goal 0 state;
   1.217 +    val (exp, tacs) = export_wrt (context_of inner_state) (Some outer);
   1.218 +    val rule = exp raw_rule;
   1.219 +    val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
   1.220 +  in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end;
   1.221 +
   1.222 +
   1.223 +fun export_thm inner thm =
   1.224 +  let val (exp, tacs) = export_wrt inner None in
   1.225 +    (case Seq.chop (2, RANGE (map #2 tacs) 1 (exp thm)) of
   1.226 +      ([thm'], _) => thm'
   1.227 +    | ([], _) => raise THM ("export: failed", 0, [thm])
   1.228 +    | _ => raise THM ("export: more than one result", 0, [thm]))
   1.229 +  end;
   1.230 +
   1.231 +
   1.232 +fun export_facts inner_state opt_outer_state state =
   1.233 +  let
   1.234 +    val thms = the_facts inner_state;
   1.235 +    val (exp, tacs) = export_wrt (context_of inner_state) (apsome context_of opt_outer_state);
   1.236 +    val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms;
   1.237 +  in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end;
   1.238 +
   1.239 +fun transfer_facts inner_state state =
   1.240 +  (case get_facts inner_state of
   1.241 +    None => Seq.single (reset_facts state)
   1.242 +  | Some ths => export_facts inner_state (Some state) state);
   1.243 +
   1.244 +
   1.245 +(* prepare result *)
   1.246 +
   1.247 +fun prep_result state t raw_thm =
   1.248    let
   1.249      val ctxt = context_of state;
   1.250      fun err msg = raise STATE (msg, state);
   1.251 @@ -361,26 +438,18 @@
   1.252        if ngoals = 0 then ()
   1.253        else (Locale.print_goals ngoals raw_thm; err (string_of_int ngoals ^ " unsolved goal(s)!"));
   1.254  
   1.255 -    val thm =
   1.256 -      raw_thm RS Drule.rev_triv_goal
   1.257 -      |> implies_elim_hyps
   1.258 -      |> Drule.implies_intr_list asms
   1.259 -      |> varify_frees (ProofContext.fixed_names ctxt)
   1.260 -      |> varify_tfrees;
   1.261 -
   1.262 -    val {hyps, prop, sign, ...} = Thm.rep_thm thm;
   1.263 +    val thm = raw_thm RS Drule.rev_triv_goal;
   1.264 +    val {hyps, prop, sign, maxidx, ...} = Thm.rep_thm thm;
   1.265      val tsig = Sign.tsig_of sign;
   1.266 +
   1.267 +    val casms = map #1 (assumptions state);
   1.268 +    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
   1.269    in
   1.270 -(* FIXME
   1.271 -    if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
   1.272 -      warning ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
   1.273 -    else ();
   1.274 -*)
   1.275 -    if not (null hyps) then
   1.276 -      err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
   1.277 +    if not (null bad_hyps) then
   1.278 +      err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
   1.279  (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
   1.280        err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
   1.281 -    else thm
   1.282 +    else Drule.forall_elim_vars (maxidx + 1) thm
   1.283    end;
   1.284  
   1.285  
   1.286 @@ -406,18 +475,6 @@
   1.287    end;
   1.288  
   1.289  
   1.290 -(* solve goal *)
   1.291 -
   1.292 -fun RANGE [] _ = all_tac
   1.293 -  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
   1.294 -
   1.295 -fun solve_goal rule tacs state =
   1.296 -  let
   1.297 -    val (_, (result, (facts, thm))) = find_goal 0 state;
   1.298 -    val thms' = FIRSTGOAL (rtac rule THEN' RANGE tacs) thm;
   1.299 -  in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
   1.300 -
   1.301 -
   1.302  
   1.303  (*** structured proof commands ***)
   1.304  
   1.305 @@ -463,17 +520,22 @@
   1.306  
   1.307  (* assume *)
   1.308  
   1.309 -fun gen_assume f tac name atts props state =
   1.310 +fun gen_assume f tacs name atts props state =
   1.311    state
   1.312    |> assert_forward
   1.313 -  |> map_context_result (f tac (PureThy.default_name name) atts props)
   1.314 +  |> map_context_result (f tacs (PureThy.default_name name) atts props)
   1.315    |> (fn (st, (facts, prems)) =>
   1.316      (st, facts)
   1.317      |> these_facts
   1.318      |> put_thms ("prems", prems));
   1.319  
   1.320 -val assume = gen_assume ProofContext.assume;
   1.321 -val assume_i = gen_assume ProofContext.assume_i;
   1.322 +val assm = gen_assume ProofContext.assume;
   1.323 +val assm_i = gen_assume ProofContext.assume_i;
   1.324 +
   1.325 +val assume = assm (assume_tac, K all_tac);
   1.326 +val assume_i = assm_i (assume_tac, K all_tac);
   1.327 +val presume = assm (K all_tac, K all_tac);
   1.328 +val presume_i = assm_i (K all_tac, K all_tac);
   1.329  
   1.330  
   1.331  
   1.332 @@ -487,6 +549,12 @@
   1.333    |> assert_facts
   1.334    |> enter_forward_chain;
   1.335  
   1.336 +fun export_chain state =
   1.337 +  state
   1.338 +  |> assert_forward
   1.339 +  |> export_facts state None
   1.340 +  |> Seq.map chain;
   1.341 +
   1.342  fun from_facts facts state =
   1.343    state
   1.344    |> put_facts (Some facts)
   1.345 @@ -497,25 +565,21 @@
   1.346  
   1.347  fun setup_goal opt_block prepp kind name atts raw_propp state =
   1.348    let
   1.349 -    val (state', concl) =
   1.350 +    val (state', prop) =
   1.351        state
   1.352        |> assert_forward_or_chain
   1.353        |> enter_forward
   1.354        |> opt_block
   1.355        |> map_context_result (fn c => prepp (c, raw_propp));
   1.356 -    val cterm_of = Thm.cterm_of (sign_of state);
   1.357 +    val cprop = Thm.cterm_of (sign_of state') prop;
   1.358 +    val casms = map #1 (assumptions state');
   1.359  
   1.360 -    val (casms, asm_tacs) = Library.split_list (ProofContext.assumptions (context_of state'));
   1.361 -    val cprems = map cterm_of (Logic.strip_imp_prems concl);
   1.362 -    val prem_tacs = replicate (length cprems) (K all_tac);
   1.363 -
   1.364 -    val prop = Logic.list_implies (map Thm.term_of casms, concl);
   1.365 -    val cprop = cterm_of prop;
   1.366 -    val thm = Drule.mk_triv_goal cprop;
   1.367 +    val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
   1.368 +    fun cut_asm (casm, thm) = (Thm.assume casm COMP revcut_rl) RS thm;
   1.369 +    val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
   1.370    in
   1.371      state'
   1.372 -    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems,
   1.373 -        asm_tacs @ prem_tacs, prop), ([], thm)))
   1.374 +    |> put_goal (Some ((kind atts, (PureThy.default_name name), prop), ([], goal)))
   1.375      |> auto_bind_goal prop
   1.376      |> (if is_chain state then use_facts else reset_facts)
   1.377      |> new_block
   1.378 @@ -565,10 +629,7 @@
   1.379  
   1.380  val at_bottom = can (assert_bottom true o close_block);
   1.381  
   1.382 -
   1.383 -(* finish proof *)
   1.384 -
   1.385 -fun finish_proof bot state =
   1.386 +fun end_proof bot state =
   1.387    state
   1.388    |> assert_forward
   1.389    |> close_block
   1.390 @@ -580,13 +641,13 @@
   1.391  
   1.392  fun finish_local print_result state =
   1.393    let
   1.394 -    val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
   1.395 -    val result = prep_result state asms t raw_thm;
   1.396 +    val ((kind, name, t), (_, raw_thm)) = current_goal state;
   1.397 +    val result = prep_result state t raw_thm;
   1.398      val (atts, opt_solve) =
   1.399        (case kind of
   1.400 -        Goal atts => (atts, solve_goal result tacs)
   1.401 +        Goal atts => (atts, export_goal result state)
   1.402        | Aux atts => (atts, Seq.single)
   1.403 -      | _ => raise STATE ("No local goal!", state));
   1.404 +      | _ => err_malformed "finish_local" state);
   1.405    in
   1.406      print_result {kind = kind_name kind, name = name, thm = result};
   1.407      state
   1.408 @@ -598,7 +659,7 @@
   1.409  
   1.410  fun local_qed finalize print_result state =
   1.411    state
   1.412 -  |> finish_proof false
   1.413 +  |> end_proof false
   1.414    |> finalize
   1.415    |> (Seq.flat o Seq.map (finish_local print_result));
   1.416  
   1.417 @@ -607,15 +668,15 @@
   1.418  
   1.419  fun finish_global alt_name alt_atts state =
   1.420    let
   1.421 -    val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
   1.422 -    val result = final_result state (prep_result state asms t raw_thm);
   1.423 +    val ((kind, def_name, t), (_, raw_thm)) = current_goal state;
   1.424 +    val result = final_result state (prep_result state t raw_thm);
   1.425  
   1.426      val name = if_none alt_name def_name;
   1.427      val atts =
   1.428        (case kind of
   1.429          Theorem atts => if_none alt_atts atts
   1.430        | Lemma atts => (if_none alt_atts atts) @ [Drule.tag_lemma]
   1.431 -      | _ => raise STATE ("No global goal!", state));
   1.432 +      | _ => err_malformed "finish_global" state);
   1.433  
   1.434      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   1.435    in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
   1.436 @@ -623,7 +684,7 @@
   1.437  (*Note: should inspect first result only, backtracking may destroy theory*)
   1.438  fun global_qed finalize alt_name alt_atts state =
   1.439    state
   1.440 -  |> finish_proof true
   1.441 +  |> end_proof true
   1.442    |> finalize
   1.443    |> Seq.map (finish_global alt_name alt_atts);
   1.444  
   1.445 @@ -648,7 +709,7 @@
   1.446    |> close_block
   1.447    |> assert_current_goal false
   1.448    |> close_block
   1.449 -  |> fetch_facts state;          (* FIXME proper check / export (!?) *)
   1.450 +  |> transfer_facts state;
   1.451  
   1.452  
   1.453  (* next_block *)
   1.454 @@ -657,6 +718,7 @@
   1.455    state
   1.456    |> assert_forward
   1.457    |> close_block
   1.458 +  |> assert_current_goal true
   1.459    |> new_block;
   1.460  
   1.461