src/Pure/tactic.ML
changeset 11961 e5911a25d094
parent 11929 a77ad6c86564
child 11970 e7eedbd2c8ca
     1.1 --- a/src/Pure/tactic.ML	Sat Oct 27 00:06:46 2001 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Oct 27 00:07:19 2001 +0200
     1.3 @@ -112,6 +112,7 @@
     1.4    val rewrite: bool -> thm list -> cterm -> thm
     1.5    val rewrite_cterm: bool -> thm list -> cterm -> cterm
     1.6    val simplify: bool -> thm list -> thm -> thm
     1.7 +  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.8  end;
     1.9  
    1.10  structure Tactic: TACTIC =
    1.11 @@ -607,6 +608,48 @@
    1.12         end)
    1.13    end;
    1.14  
    1.15 +
    1.16 +(** primitive goal interface for internal use -- avoids "standard" operation *)
    1.17 +
    1.18 +fun prove thy xs asms prop tac =
    1.19 +  let
    1.20 +    val sg = Theory.sign_of thy;
    1.21 +    val statement = Logic.list_implies (asms, prop);
    1.22 +    val frees = map Term.dest_Free (Term.term_frees statement);
    1.23 +    val params = mapfilter (fn x => apsome (pair x) (assoc_string (frees, x))) xs;
    1.24 +
    1.25 +    fun err msg = error (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
    1.26 +      Sign.string_of_term sg (Term.list_all_free (params, statement)));
    1.27 +
    1.28 +    fun cert_safe t = Thm.cterm_of sg t
    1.29 +      handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.30 +
    1.31 +    val _ = cert_safe statement;
    1.32 +    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => error msg;
    1.33 +
    1.34 +    val casms = map cert_safe asms;
    1.35 +    val prems = map (norm_hhf o Thm.assume) casms;
    1.36 +    val goal = Drule.mk_triv_goal (cert_safe prop);
    1.37 +
    1.38 +    val goal' =
    1.39 +      (case Seq.pull (tac prems goal) of Some (goal', _) => goal' | _ => err "Tactic failed.");
    1.40 +    val ngoals = Thm.nprems_of goal';
    1.41 +    val raw_result = goal' RS Drule.rev_triv_goal;
    1.42 +    val prop' = #prop (Thm.rep_thm raw_result);
    1.43 +  in
    1.44 +    if ngoals <> 0 then
    1.45 +      err ("Proof failed.\n" ^ Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal'))
    1.46 +        ^ ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!"))
    1.47 +    else if not (Pattern.matches (Sign.tsig_of sg) (prop, prop')) then
    1.48 +      err ("Proved a different theorem: " ^ Sign.string_of_term sg prop')
    1.49 +    else
    1.50 +      raw_result
    1.51 +      |> Drule.implies_intr_list casms
    1.52 +      |> Drule.forall_intr_list (map (cert_safe o Free) params)
    1.53 +      |> norm_hhf
    1.54 +      |> Thm.varifyT    (* FIXME proper scope for polymorphisms!? *)
    1.55 +  end;
    1.56 +
    1.57  end;
    1.58  
    1.59  structure BasicTactic: BASIC_TACTIC = Tactic;