--- a/src/Pure/drule.ML Thu Aug 13 17:29:18 1998 +0200
+++ b/src/Pure/drule.ML Thu Aug 13 17:43:00 1998 +0200
@@ -73,9 +73,10 @@
val triv_forall_equality: thm
val swap_prems_rl : thm
val equal_intr_rule : thm
- val triv_goal: thm
- val rev_triv_goal: thm
- val instantiate': ctyp option list -> cterm option list -> thm -> thm
+ val triv_goal : thm
+ val rev_triv_goal : thm
+ val mk_triv_goal : cterm -> thm
+ val instantiate' : ctyp option list -> cterm option list -> thm -> thm
end;
structure Drule : DRULE =
@@ -630,6 +631,9 @@
end;
+(*Make an initial proof state, "PROP A ==> (PROP A)" *)
+fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
+
end;
open Drule;
--- a/src/Pure/goals.ML Thu Aug 13 17:29:18 1998 +0200
+++ b/src/Pure/goals.ML Thu Aug 13 17:43:00 1998 +0200
@@ -61,6 +61,7 @@
val prove_goal : theory -> string -> (thm list -> tactic list) -> thm
val prove_goalw : theory->thm list->string->(thm list->tactic list)->thm
val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
+ val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm
val push_proof : unit -> unit
val read : string -> term
val ren : string -> int -> unit
@@ -159,7 +160,7 @@
val cAs = map (cterm_of sign) As;
val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs;
val cB = cterm_of sign B;
- val st0 = let val st = Drule.instantiate' [] [Some cB] Drule.triv_goal
+ val st0 = let val st = Drule.mk_triv_goal cB
in rewrite_goals_rule rths st end
(*discharges assumptions from state in the order they appear in goal;
checks (if requested) that resulting theorem is equivalent to goal. *)
@@ -225,18 +226,22 @@
Syntax is similar to "goal" command for easy keyboard use. **)
(*Version taking the goal as a cterm*)
-fun prove_goalw_cterm rths chorn tacsf =
+fun prove_goalw_cterm_general check rths chorn tacsf =
let val (prems, st0, mkresult) = prepare_proof false rths chorn
val tac = EVERY (tacsf prems)
fun statef() =
(case Seq.pull (tac st0) of
Some(st,_) => st
| _ => error ("prove_goal: tactic failed"))
- in mkresult (true, cond_timeit (!proof_timing) statef) end
+ in mkresult (check, cond_timeit (!proof_timing) statef) end
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
error ("The exception above was raised for\n" ^
string_of_cterm chorn));
+(*Two variants: one checking the result, one not*)
+val prove_goalw_cterm = prove_goalw_cterm_general true
+and prove_goalw_cterm_nocheck = prove_goalw_cterm_general false;
+
(*Version taking the goal as a string*)
fun prove_goalw thy rths agoal tacsf =