src/Pure/Isar/proof.ML
changeset 6932 77c14313af51
parent 6896 4bdc3600ddae
child 6950 ab6d35b7283f
--- a/src/Pure/Isar/proof.ML	Thu Jul 08 18:32:43 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 08 18:34:59 1999 +0200
@@ -28,6 +28,7 @@
   type method
   val method: (thm list -> tactic) -> method
   val refine: (context -> method) -> state -> state Seq.seq
+  val export_thm: context -> thm -> thm
   val bind: (indexname * string) list -> state -> state
   val bind_i: (indexname * term) list -> state -> state
   val match_bind: (string list * string) list -> state -> state
@@ -35,29 +36,46 @@
   val have_thmss: thm list -> string -> context attribute list ->
     (thm list * context attribute list) list -> state -> state
   val simple_have_thms: string -> thm 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
-  val theorem_i: bstring -> theory attribute list -> term * term list -> theory -> state
-  val lemma: bstring -> theory attribute list -> string * string list -> theory -> state
-  val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> state
+  val assm: (int -> tactic) * (int -> tactic) -> string -> context attribute list
+    -> (string * (string list * string list)) list -> state -> state
+  val assm_i: (int -> tactic) * (int -> tactic) -> string -> context attribute list
+    -> (term * (term list * term list)) list -> state -> state
+  val assume: string -> context attribute list -> (string * (string list * string list)) list
+    -> state -> state
+  val assume_i: string -> context attribute list -> (term * (term list * term list)) list
+    -> state -> state
+  val presume: string -> context attribute list -> (string * (string list * string list)) list
+    -> state -> state
+  val presume_i: string -> context attribute list -> (term * (term list * term list)) list
+    -> state -> state
+  val theorem: bstring -> theory attribute list -> string * (string list * string list)
+    -> theory -> state
+  val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
+    -> theory -> state
+  val lemma: bstring -> theory attribute list -> string * (string list * string list)
+    -> theory -> state
+  val lemma_i: bstring -> theory attribute list -> term * (term list * term list)
+    -> theory -> state
   val chain: state -> state
+  val export_chain: state -> state Seq.seq
   val from_facts: thm list -> state -> state
-  val show: string -> context attribute list -> string * string list -> state -> state
-  val show_i: string -> context attribute list -> term * term list -> state -> state
-  val have: string -> context attribute list -> string * string list -> state -> state
-  val have_i: string -> context attribute list -> term * term list -> state -> state
+  val show: string -> context attribute list -> string * (string list * string list)
+    -> state -> state
+  val show_i: string -> context attribute list -> term * (term list * term list)
+    -> state -> state
+  val have: string -> context attribute list -> string * (string list * string list)
+    -> state -> state
+  val have_i: string -> context attribute list -> term * (term list * term list)
+    -> state -> state
   val at_bottom: state -> bool
   val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
     -> state -> state Seq.seq
   val global_qed: (state -> state Seq.seq) -> bstring option -> theory attribute list option
     -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
   val begin_block: state -> state
-  val end_block: state -> state
+  val end_block: state -> state Seq.seq
   val next_block: state -> state
 end;
 
@@ -88,13 +106,11 @@
   fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
 
 type goal =
- (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*)
+ (kind *        (*result kind*)
+  string *      (*result name*)
+  term) *       (*result statement*)
+ (thm list *    (*use facts*)
+  thm);         (*goal: subgoals ==> statement*)
 
 
 (* type mode *)
@@ -166,6 +182,7 @@
 val auto_bind_facts = map_context oo ProofContext.auto_bind_facts;
 val put_thms = map_context o ProofContext.put_thms;
 val put_thmss = map_context o ProofContext.put_thmss;
+val assumptions = ProofContext.assumptions o context_of;
 
 
 (* facts *)
@@ -179,6 +196,7 @@
   | _ => raise STATE ("Single fact expected", state));
 
 fun assert_facts state = (the_facts state; state);
+fun get_facts (State ({facts, ...}, _)) = facts;
 
 fun put_facts facts state =
   state
@@ -193,12 +211,11 @@
   |> put_thms (name, facts);
 
 fun these_facts (state, ths) = have_facts ths state;
-fun fetch_facts (State ({facts, ...}, _)) = put_facts facts;
 
 
 (* goal *)
 
-fun find_goal i (State ({goal = Some goal, ...}, _)) = (i, goal)
+fun find_goal i (state as State ({goal = Some goal, ...}, _)) = (context_of state, (i, goal))
   | find_goal i (State ({goal = None, ...}, node :: nodes)) =
       find_goal (i + 1) (State (node, nodes))
   | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state;
@@ -267,16 +284,17 @@
 
 fun print_facts _ None = ()
   | print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:")
-      (map (setmp Display.show_hyps false Display.pretty_thm) ths));
+      (map Display.pretty_thm_no_hyps ths));
 
 fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   let
     val ref (_, _, begin_goal) = Goals.current_goals_markers;
 
     fun levels_up 0 = ""
+      | levels_up 1 = " (1 level up)"
       | 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);
@@ -314,7 +332,7 @@
 fun refine meth_fun (state as State ({context, ...}, _)) =
   let
     val Method meth = meth_fun context;
-    val (_, (result, (facts, thm))) = find_goal 0 state;
+    val (_, (_, (result, (facts, thm)))) = find_goal 0 state;
 
     fun refn thm' =
       state
@@ -323,9 +341,11 @@
   in Seq.map refn (meth facts thm) end;
 
 
-(* prepare result *)
+(* export *)
 
-fun varify_frees names thm =
+local
+
+fun varify_frees fixes thm =
   let
     fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
       | get_free _ (opt, _) = opt;
@@ -333,25 +353,82 @@
     fun find_free t x = foldl_aterms (get_free x) (None, t);
 
     val {sign, prop, ...} = Thm.rep_thm thm;
-    val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names);
+    val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
   in
     thm
     |> Drule.forall_intr_list frees
     |> Drule.forall_elim_vars 0
   end;
 
-fun varify_tfrees thm =
+fun most_general_varify_tfrees thm =
   let
     val {hyps, prop, ...} = Thm.rep_thm thm;
     val frees = foldr Term.add_term_frees (prop :: hyps, []);
     val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
   in thm |> Thm.varifyT' leave_tfrees end;
 
-fun implies_elim_hyps thm =
-  foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));
+fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
+  | diff_context inner (Some outer) =
+      (ProofContext.fixed_names inner \\ ProofContext.fixed_names outer,
+        Library.drop (length (ProofContext.assumptions outer), ProofContext.assumptions inner));
+
+in
+
+fun export fixes casms thm =
+  thm
+  |> Drule.implies_intr_list casms
+  |> varify_frees fixes
+  |> most_general_varify_tfrees;
+
+fun export_wrt inner opt_outer =
+  let
+    val (fixes, asms) = diff_context inner opt_outer;
+    val casms = map #1 asms;
+    val tacs = map #2 asms;
+  in (export fixes casms, tacs) end;
+
+end;
 
 
-fun prep_result state asms t raw_thm =
+(* export results *)
+
+fun RANGE [] _ = all_tac
+  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
+
+fun export_goal raw_rule inner_state state =
+  let
+    val (outer, (_, (result, (facts, thm)))) = find_goal 0 state;
+    val (exp, tacs) = export_wrt (context_of inner_state) (Some outer);
+    val rule = exp raw_rule;
+    val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
+  in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end;
+
+
+fun export_thm inner thm =
+  let val (exp, tacs) = export_wrt inner None in
+    (case Seq.chop (2, RANGE (map #2 tacs) 1 (exp thm)) of
+      ([thm'], _) => thm'
+    | ([], _) => raise THM ("export: failed", 0, [thm])
+    | _ => raise THM ("export: more than one result", 0, [thm]))
+  end;
+
+
+fun export_facts inner_state opt_outer_state state =
+  let
+    val thms = the_facts inner_state;
+    val (exp, tacs) = export_wrt (context_of inner_state) (apsome context_of opt_outer_state);
+    val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms;
+  in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end;
+
+fun transfer_facts inner_state state =
+  (case get_facts inner_state of
+    None => Seq.single (reset_facts state)
+  | Some ths => export_facts inner_state (Some state) state);
+
+
+(* prepare result *)
+
+fun prep_result state t raw_thm =
   let
     val ctxt = context_of state;
     fun err msg = raise STATE (msg, state);
@@ -361,26 +438,18 @@
       if ngoals = 0 then ()
       else (Locale.print_goals ngoals raw_thm; err (string_of_int ngoals ^ " unsolved goal(s)!"));
 
-    val thm =
-      raw_thm RS Drule.rev_triv_goal
-      |> implies_elim_hyps
-      |> Drule.implies_intr_list asms
-      |> varify_frees (ProofContext.fixed_names ctxt)
-      |> varify_tfrees;
-
-    val {hyps, prop, sign, ...} = Thm.rep_thm thm;
+    val thm = raw_thm RS Drule.rev_triv_goal;
+    val {hyps, prop, sign, maxidx, ...} = Thm.rep_thm thm;
     val tsig = Sign.tsig_of sign;
+
+    val casms = map #1 (assumptions state);
+    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
   in
-(* FIXME
-    if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
-      warning ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
-    else ();
-*)
-    if not (null hyps) then
-      err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
+    if not (null bad_hyps) then
+      err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
 (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
       err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
-    else thm
+    else Drule.forall_elim_vars (maxidx + 1) thm
   end;
 
 
@@ -406,18 +475,6 @@
   end;
 
 
-(* solve goal *)
-
-fun RANGE [] _ = all_tac
-  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
-
-fun solve_goal rule tacs state =
-  let
-    val (_, (result, (facts, thm))) = find_goal 0 state;
-    val thms' = FIRSTGOAL (rtac rule THEN' RANGE tacs) thm;
-  in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end;
-
-
 
 (*** structured proof commands ***)
 
@@ -463,17 +520,22 @@
 
 (* assume *)
 
-fun gen_assume f tac name atts props state =
+fun gen_assume f tacs name atts props state =
   state
   |> assert_forward
-  |> map_context_result (f tac (PureThy.default_name name) atts props)
+  |> map_context_result (f tacs (PureThy.default_name name) atts props)
   |> (fn (st, (facts, prems)) =>
     (st, facts)
     |> these_facts
     |> put_thms ("prems", prems));
 
-val assume = gen_assume ProofContext.assume;
-val assume_i = gen_assume ProofContext.assume_i;
+val assm = gen_assume ProofContext.assume;
+val assm_i = gen_assume ProofContext.assume_i;
+
+val assume = assm (assume_tac, K all_tac);
+val assume_i = assm_i (assume_tac, K all_tac);
+val presume = assm (K all_tac, K all_tac);
+val presume_i = assm_i (K all_tac, K all_tac);
 
 
 
@@ -487,6 +549,12 @@
   |> assert_facts
   |> enter_forward_chain;
 
+fun export_chain state =
+  state
+  |> assert_forward
+  |> export_facts state None
+  |> Seq.map chain;
+
 fun from_facts facts state =
   state
   |> put_facts (Some facts)
@@ -497,25 +565,21 @@
 
 fun setup_goal opt_block prepp kind name atts raw_propp state =
   let
-    val (state', concl) =
+    val (state', prop) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> opt_block
       |> map_context_result (fn c => prepp (c, raw_propp));
-    val cterm_of = Thm.cterm_of (sign_of state);
+    val cprop = Thm.cterm_of (sign_of state') prop;
+    val casms = map #1 (assumptions 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;
+    val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
+    fun cut_asm (casm, thm) = (Thm.assume casm COMP revcut_rl) RS thm;
+    val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
   in
     state'
-    |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems,
-        asm_tacs @ prem_tacs, prop), ([], thm)))
+    |> put_goal (Some ((kind atts, (PureThy.default_name name), prop), ([], goal)))
     |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block
@@ -565,10 +629,7 @@
 
 val at_bottom = can (assert_bottom true o close_block);
 
-
-(* finish proof *)
-
-fun finish_proof bot state =
+fun end_proof bot state =
   state
   |> assert_forward
   |> close_block
@@ -580,13 +641,13 @@
 
 fun finish_local print_result state =
   let
-    val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state;
-    val result = prep_result state asms t raw_thm;
+    val ((kind, name, t), (_, raw_thm)) = current_goal state;
+    val result = prep_result state t raw_thm;
     val (atts, opt_solve) =
       (case kind of
-        Goal atts => (atts, solve_goal result tacs)
+        Goal atts => (atts, export_goal result state)
       | Aux atts => (atts, Seq.single)
-      | _ => raise STATE ("No local goal!", state));
+      | _ => err_malformed "finish_local" state);
   in
     print_result {kind = kind_name kind, name = name, thm = result};
     state
@@ -598,7 +659,7 @@
 
 fun local_qed finalize print_result state =
   state
-  |> finish_proof false
+  |> end_proof false
   |> finalize
   |> (Seq.flat o Seq.map (finish_local print_result));
 
@@ -607,15 +668,15 @@
 
 fun finish_global alt_name alt_atts state =
   let
-    val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state;
-    val result = final_result state (prep_result state asms t raw_thm);
+    val ((kind, def_name, t), (_, raw_thm)) = current_goal state;
+    val result = final_result state (prep_result state t raw_thm);
 
     val name = if_none alt_name def_name;
     val atts =
       (case kind of
         Theorem atts => if_none alt_atts atts
       | Lemma atts => (if_none alt_atts atts) @ [Drule.tag_lemma]
-      | _ => raise STATE ("No global goal!", state));
+      | _ => err_malformed "finish_global" state);
 
     val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
@@ -623,7 +684,7 @@
 (*Note: should inspect first result only, backtracking may destroy theory*)
 fun global_qed finalize alt_name alt_atts state =
   state
-  |> finish_proof true
+  |> end_proof true
   |> finalize
   |> Seq.map (finish_global alt_name alt_atts);
 
@@ -648,7 +709,7 @@
   |> close_block
   |> assert_current_goal false
   |> close_block
-  |> fetch_facts state;          (* FIXME proper check / export (!?) *)
+  |> transfer_facts state;
 
 
 (* next_block *)
@@ -657,6 +718,7 @@
   state
   |> assert_forward
   |> close_block
+  |> assert_current_goal true
   |> new_block;