# HG changeset patch
# User nipkow
# Date 898073318 -7200
# Node ID a1d0a6d555cd62a823367cf53cdf8a1b19f6cde4
# Parent  78abd4c4802ae305ca2fa067fbe6570ab521ba30
Goals may now contain assumptions, which are not returned.
This is controlled by an argument `atomic' to the goal commands.

diff -r 78abd4c4802a -r a1d0a6d555cd src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Jun 16 18:37:34 1998 +0200
+++ b/src/Pure/goals.ML	Wed Jun 17 10:48:38 1998 +0200
@@ -13,6 +13,8 @@
 signature GOALS =
   sig
   type proof
+  val atomic_goal	: theory -> string -> thm list
+  val atomic_goalw	: theory -> thm list -> string -> thm list
   val ba		: int -> unit
   val back		: unit -> unit
   val bd		: thm -> int -> unit
@@ -127,20 +129,29 @@
 val result_error_fn = ref result_error_default;
 
 (*Common treatment of "goal" and "prove_goal":
-  Return assumptions, initial proof state, and function to make result. *)
-fun prepare_proof rths chorn =
+  Return assumptions, initial proof state, and function to make result.
+  "atomic" indicates if the goal should be wrapped up in the function
+  "Goal::prop=>prop" to avoid assumptions being returned separately.
+*)
+fun prepare_proof atomic rths chorn =
   let val {sign, t=horn,...} = rep_cterm chorn;
       val (_,As,B) = Logic.strip_horn(horn);
+      val atoms = atomic andalso
+            forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
+      val (As,B) = if atoms then ([],horn) else (As,B);
       val cAs = map (cterm_of sign) As;
-      val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs
-      and st0 = (rewrite_goals_rule rths o trivial) (cterm_of sign B)
+      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
+                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. *)
       fun mkresult (check,state) =
         let val state = Seq.hd (flexflex_rule state)
 	    		handle THM _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
-            val th = strip_shyps (implies_intr_list cAs state)
+            val ath = strip_shyps (implies_intr_list cAs state)
+            val th = ath RS Drule.rev_triv_goal
             val {hyps,prop,sign=sign',...} = rep_thm th
             val xshyps = extra_shyps th;
         in  if not check then th
@@ -157,7 +168,7 @@
                  commas (map (Sign.str_of_sort sign) xshyps))
 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
 			            (term_of chorn, prop)
-		 then  standard th 
+		 then  standard th
 	    else  !result_error_fn state "proved a different theorem"
         end
   in
@@ -196,7 +207,7 @@
 
 (*Version taking the goal as a cterm*)
 fun prove_goalw_cterm rths chorn tacsf =
-  let val (prems, st0, mkresult) = prepare_proof rths chorn
+  let val (prems, st0, mkresult) = prepare_proof false rths chorn
       val tac = EVERY (tacsf prems)
       fun statef() = 
 	  (case Seq.pull (tac st0) of 
@@ -304,8 +315,8 @@
 
 (*Version taking the goal as a cterm; if you have a term t and theory thy, use
     goalw_cterm rths (cterm_of (sign_of thy) t);      *)
-fun goalw_cterm rths chorn = 
-  let val (prems, st0, mkresult) = prepare_proof rths chorn
+fun agoalw_cterm atomic rths chorn = 
+  let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
   in  undo_list := [];
       setstate [ (st0, Seq.empty) ];  
       curr_prems := prems;
@@ -313,14 +324,25 @@
       prems
   end;
 
+val goalw_cterm = agoalw_cterm false;
+
 (*Version taking the goal as a string*)
-fun goalw thy rths agoal = 
-  goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
+fun agoalw atomic thy rths agoal = 
+  agoalw_cterm atomic rths (read_cterm(sign_of thy)(agoal,propT))
   handle ERROR => error (*from type_assign, etc via prepare_proof*)
 	    ("The error(s) above occurred for " ^ quote agoal);
 
+val goalw = agoalw false;
+
 (*String version with no meta-rewrite-rules*)
-fun goal thy = goalw thy [];
+fun agoal atomic thy = agoalw atomic thy [];
+val goal = agoal false;
+
+(*now the versions that wrap the goal up in `Goal' to make it atomic*)
+
+val atomic_goalw = agoalw true;
+val atomic_goal = agoal true;
+
 
 (*Proof step "by" the given tactic -- apply tactic to the proof state*)
 fun by_com tac ((th,ths), pairs) : gstack =
diff -r 78abd4c4802a -r a1d0a6d555cd src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jun 16 18:37:34 1998 +0200
+++ b/src/Pure/logic.ML	Wed Jun 17 10:48:38 1998 +0200
@@ -21,7 +21,9 @@
   val dest_type		: term -> typ
   val flatten_params	: int -> term -> term
   val incr_indexes	: typ list * int -> term -> term
+  val is_all            : term -> bool
   val is_equals         : term -> bool
+  val is_implies        : term -> bool
   val lift_fns		: term * int -> (term -> term) * (term -> term)
   val list_flexpairs	: (term*term)list * term -> term
   val list_implies	: term list * term -> term
@@ -55,6 +57,12 @@
 
 (*** Abstract syntax operations on the meta-connectives ***)
 
+(** all **)
+
+fun is_all (Const ("all", _) $ _) = true
+  | is_all _ = false;
+
+
 (** equality **)
 
 (*Make an equality.  DOES NOT CHECK TYPE OF u*)
@@ -74,6 +82,9 @@
 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
   | dest_implies A = raise TERM("dest_implies", [A]);
 
+fun is_implies (Const ("==>", _) $ _ $ _) = true
+  | is_implies _ = false;
+
 
 (** nested implications **)
 
diff -r 78abd4c4802a -r a1d0a6d555cd src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Jun 16 18:37:34 1998 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jun 17 10:48:38 1998 +0200
@@ -406,6 +406,8 @@
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
     ("TYPE", "'a itself", NoSyn)]
+  |> Theory.add_modesyntax ("", false)
+    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   |> local_path
   |> (add_defs o map Attribute.none)
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),