# HG changeset patch # User wenzelm # Date 1129911300 -7200 # Node ID 788836292b1a684e6b1d10ce8dbbc0f1c5a9716b # Parent 09485bdd4b6f2fd93f91b877790bd47d3859db61 Internal goals. diff -r 09485bdd4b6f -r 788836292b1a src/Pure/goal.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/goal.ML Fri Oct 21 18:15:00 2005 +0200 @@ -0,0 +1,164 @@ +(* Title: Pure/goal.ML + ID: $Id$ + Author: Makarius and Lawrence C Paulson + +Internal goals. NB: by attaching the Goal constant the conclusion of +a goal state is guaranteed to be atomic. +*) + +signature BASIC_GOAL = +sig + val SELECT_GOAL: tactic -> int -> tactic +end; + +signature GOAL = +sig + include BASIC_GOAL + val init: cterm -> thm + val conclude: thm -> thm + val finish: thm -> thm + val prove_raw: theory -> term -> tactic -> thm + val norm_hhf_rule: thm -> thm + val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm + val prove_multi: theory -> string list -> term list -> term list -> + (thm list -> tactic) -> thm list + + (* FIXME remove *) + val norm_hhf_plain: thm -> thm + val prove_multi_plain: theory -> string list -> term list -> term list -> + (thm list -> tactic) -> thm list + val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm +end; + +structure Goal: GOAL = +struct + +(* managing goal states *) + +(* + ----------------- (init) + Goal C ==> Goal C +*) +fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI; + +(* + A ==> ... ==> Goal C + -------------------- (conclude) + A ==> ... ==> C +*) +fun conclude th = + (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1) + (Drule.incr_indexes_wrt [] [] [] [th] Drule.goalD) of + SOME th' => th' + | NONE => raise THM ("Failed to conclude goal", 0, [th])); + +(* + Goal C + ------ (finish) + C +*) +fun finish th = + (case Thm.nprems_of th of + 0 => conclude th + | n => raise THM ("Proof failed.\n" ^ + Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^ + ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); + + +(* prove_raw -- minimal checks, no normalization *) + +fun prove_raw thy goal tac = + (case SINGLE tac (init (Thm.cterm_of thy goal)) of + SOME th => finish th + | NONE => raise ERROR_MESSAGE "Tactic failed."); + + +(* tactical proving *) + +val norm_hhf_plain = (* FIXME remove *) + (not o Drule.is_norm_hhf o Thm.prop_of) ? + MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq]; + +val norm_hhf_rule = + norm_hhf_plain + #> Thm.adjust_maxidx_thm + #> Drule.gen_all; + +local + +fun gen_prove finish_thm thy xs asms props tac = + let + val prop = Logic.mk_conjunction_list props; + val statement = Logic.list_implies (asms, prop); + val frees = map Term.dest_Free (Term.term_frees statement); + val fixed_frees = filter_out (member (op =) xs o #1) frees; + val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees); + val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs; + + fun err msg = raise ERROR_MESSAGE + (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ + Sign.string_of_term thy (Term.list_all_free (params, statement))); + + fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t) + handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; + + val _ = cert_safe statement; + val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg; + + val cparams = map (cert_safe o Free) params; + val casms = map cert_safe asms; + val prems = map (norm_hhf_rule o Thm.assume) casms; + + val goal = init (cert_safe prop); + val goal' = (case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed."); + val raw_result = finish goal' handle THM (msg, _, _) => err msg; + + val prop' = Thm.prop_of raw_result; + val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () => + err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')); + in + Drule.conj_elim_precise (length props) raw_result + |> map + (Drule.implies_intr_list casms + #> Drule.forall_intr_list cparams + #> finish_thm fixed_tfrees) + end; + +in + +fun prove_multi thy xs asms prop tac = + gen_prove (fn fixed_tfrees => Drule.zero_var_indexes o + (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule) + thy xs asms prop tac; + +fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac); + +fun prove_multi_plain thy xs asms prop tac = gen_prove (K norm_hhf_plain) thy xs asms prop tac; +fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac); + +end; + + +(* SELECT_GOAL *) + +(*Tactical for restricting the effect of a tactic to subgoal i. Works + by making a new state from subgoal i, applying tac to it, and + composing the resulting thm with the original state.*) + +fun SELECT tac i st = + init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1))) + |> tac + |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st); + +fun SELECT_GOAL tac i st = + let val n = Thm.nprems_of st in + if 1 <= i andalso i <= n then + if n = 1 then tac st else SELECT tac i st + else Seq.empty + end; + + +end; + +structure BasicGoal: BASIC_GOAL = Goal; +open BasicGoal;