wenzelm@17980: (*  Title:      Pure/goal.ML
wenzelm@17980:     ID:         $Id$
wenzelm@17980:     Author:     Makarius and Lawrence C Paulson
wenzelm@17980: 
wenzelm@18027: Tactical goal state.
wenzelm@17980: *)
wenzelm@17980: 
wenzelm@17980: signature BASIC_GOAL =
wenzelm@17980: sig
wenzelm@17980:   val SELECT_GOAL: tactic -> int -> tactic
wenzelm@17980: end;
wenzelm@17980: 
wenzelm@17980: signature GOAL =
wenzelm@17980: sig
wenzelm@17980:   include BASIC_GOAL
wenzelm@17980:   val init: cterm -> thm
wenzelm@18027:   val protect: thm -> thm
wenzelm@17980:   val conclude: thm -> thm
wenzelm@17980:   val finish: thm -> thm
wenzelm@18027:   val norm_hhf: thm -> thm
wenzelm@18119:   val compose_hhf: thm -> int -> thm -> thm Seq.seq
wenzelm@18119:   val compose_hhf_tac: thm -> int -> tactic
wenzelm@18027:   val comp_hhf: thm -> thm -> thm
wenzelm@17980:   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
wenzelm@17980:   val prove_multi: theory -> string list -> term list -> term list ->
wenzelm@17980:     (thm list -> tactic) -> thm list
wenzelm@18027:   val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
wenzelm@17980: end;
wenzelm@17980: 
wenzelm@17980: structure Goal: GOAL =
wenzelm@17980: struct
wenzelm@17980: 
wenzelm@18027: (** goals **)
wenzelm@18027: 
wenzelm@18027: (*
wenzelm@18027:   -------- (init)
wenzelm@18027:   C ==> #C
wenzelm@18027: *)
wenzelm@18027: fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI;
wenzelm@17980: 
wenzelm@17980: (*
wenzelm@18119:    C
wenzelm@18119:   --- (protect)
wenzelm@18119:   #C
wenzelm@17980: *)
wenzelm@18027: fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
wenzelm@17980: 
wenzelm@17980: (*
wenzelm@18027:   A ==> ... ==> #C
wenzelm@18027:   ---------------- (conclude)
wenzelm@17980:   A ==> ... ==> C
wenzelm@17980: *)
wenzelm@17980: fun conclude th =
wenzelm@17980:   (case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1)
wenzelm@18027:       (Drule.incr_indexes th Drule.protectD) of
wenzelm@17980:     SOME th' => th'
wenzelm@17980:   | NONE => raise THM ("Failed to conclude goal", 0, [th]));
wenzelm@17980: 
wenzelm@17980: (*
wenzelm@18027:   #C
wenzelm@18027:   --- (finish)
wenzelm@18027:    C
wenzelm@17983: *)
wenzelm@17980: fun finish th =
wenzelm@17980:   (case Thm.nprems_of th of
wenzelm@17980:     0 => conclude th
wenzelm@17980:   | n => raise THM ("Proof failed.\n" ^
wenzelm@17980:       Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
wenzelm@17980:       ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
wenzelm@17980: 
wenzelm@17980: 
wenzelm@18027: 
wenzelm@18027: (** results **)
wenzelm@18027: 
wenzelm@18027: (* HHF normal form *)
wenzelm@17980: 
wenzelm@18119: val norm_hhf =
wenzelm@17980:   (not o Drule.is_norm_hhf o Thm.prop_of) ?
wenzelm@18119:     MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq]
wenzelm@17980:   #> Thm.adjust_maxidx_thm
wenzelm@17980:   #> Drule.gen_all;
wenzelm@17980: 
wenzelm@18027: 
wenzelm@18027: (* composition of normal results *)
wenzelm@18027: 
wenzelm@18027: fun compose_hhf tha i thb =
wenzelm@18027:   Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb;
wenzelm@18027: 
wenzelm@18119: fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
wenzelm@18119: 
wenzelm@18027: fun comp_hhf tha thb =
wenzelm@18119:   (case Seq.chop (2, compose_hhf tha 1 thb) of
wenzelm@18119:     ([th], _) => th
wenzelm@18119:   | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
wenzelm@18119:   | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
wenzelm@17986: 
wenzelm@17986: 
wenzelm@18027: 
wenzelm@18027: (** tactical theorem proving **)
wenzelm@18027: 
wenzelm@18119: (* prove_multi *)
wenzelm@17986: 
wenzelm@18119: fun prove_multi thy xs asms props tac =
wenzelm@17980:   let
wenzelm@17980:     val prop = Logic.mk_conjunction_list props;
wenzelm@17980:     val statement = Logic.list_implies (asms, prop);
wenzelm@17980:     val frees = map Term.dest_Free (Term.term_frees statement);
wenzelm@17980:     val fixed_frees = filter_out (member (op =) xs o #1) frees;
wenzelm@17980:     val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
wenzelm@17980:     val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
wenzelm@17980: 
wenzelm@17980:     fun err msg = raise ERROR_MESSAGE
wenzelm@17980:       (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
wenzelm@17980:         Sign.string_of_term thy (Term.list_all_free (params, statement)));
wenzelm@17980: 
wenzelm@17980:     fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
wenzelm@17980:       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
wenzelm@17980: 
wenzelm@17980:     val _ = cert_safe statement;
wenzelm@17980:     val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
wenzelm@17980: 
wenzelm@17980:     val cparams = map (cert_safe o Free) params;
wenzelm@17980:     val casms = map cert_safe asms;
wenzelm@18027:     val prems = map (norm_hhf o Thm.assume) casms;
wenzelm@17980: 
wenzelm@17980:     val goal = init (cert_safe prop);
wenzelm@18119:     val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
wenzelm@17980:     val raw_result = finish goal' handle THM (msg, _, _) => err msg;
wenzelm@17980: 
wenzelm@17980:     val prop' = Thm.prop_of raw_result;
wenzelm@17986:     val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
wenzelm@17980:       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
wenzelm@17980:   in
wenzelm@17980:     Drule.conj_elim_precise (length props) raw_result
wenzelm@17980:     |> map
wenzelm@17980:       (Drule.implies_intr_list casms
wenzelm@17980:         #> Drule.forall_intr_list cparams
wenzelm@18119:         #> norm_hhf
wenzelm@18119:         #> (#1 o Thm.varifyT' fixed_tfrees)
wenzelm@18119:         #> Drule.zero_var_indexes)
wenzelm@17980:   end;
wenzelm@17980: 
wenzelm@17980: 
wenzelm@18119: (* prove *)
wenzelm@17980: 
wenzelm@17980: fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
wenzelm@17980: 
wenzelm@17980: 
wenzelm@18027: (* prove_raw -- no checks, no normalization of result! *)
wenzelm@18027: 
wenzelm@18027: fun prove_raw casms cprop tac =
wenzelm@18027:   (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
wenzelm@18027:     SOME th => Drule.implies_intr_list casms (finish th)
wenzelm@18027:   | NONE => raise ERROR_MESSAGE "Tactic failed.");
wenzelm@18027: 
wenzelm@18027: 
wenzelm@17980: (* SELECT_GOAL *)
wenzelm@17980: 
wenzelm@17980: (*Tactical for restricting the effect of a tactic to subgoal i.  Works
wenzelm@17980:   by making a new state from subgoal i, applying tac to it, and
wenzelm@17980:   composing the resulting thm with the original state.*)
wenzelm@17980: 
wenzelm@17980: fun SELECT tac i st =
wenzelm@17980:   init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1)))
wenzelm@17980:   |> tac
wenzelm@17980:   |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
wenzelm@17980: 
wenzelm@17980: fun SELECT_GOAL tac i st =
wenzelm@17980:   let val n = Thm.nprems_of st in
wenzelm@17980:     if 1 <= i andalso i <= n then
wenzelm@17980:       if n = 1 then tac st else SELECT tac i st
wenzelm@17980:     else Seq.empty
wenzelm@17980:   end;
wenzelm@17980: 
wenzelm@17980: end;
wenzelm@17980: 
wenzelm@17980: structure BasicGoal: BASIC_GOAL = Goal;
wenzelm@17980: open BasicGoal;