--- 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;