# HG changeset patch # User wenzelm # Date 931451699 -7200 # Node ID 77c14313af5195e080d044d7df950fa6942b56d8 # Parent bd8aa6ae6bcdfdd3b5e4fe98b7d60d16249af0fc propp: 'concl' patterns; assumptions: tactics for non-goal export; use Display.pretty_thm_no_hyps; assm vs. assume vs. presume; tuned type goal; tuned print_goal; relative exports, absolute export_thm rule; transfer_facts; tuned; diff -r bd8aa6ae6bcd -r 77c14313af51 src/Pure/Isar/proof.ML --- 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;