# HG changeset patch
# User wenzelm
# Date 947069101 -3600
# Node ID 62b45a2e6ecb41da8346dfe92d1475a9b88b7c3f
# Parent  d5eb246c94ec05f67b621296ba5975a37fab776b
ObtainFun;
prepare vars / asms / pats only once;

diff -r d5eb246c94ec -r 62b45a2e6ecb src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jan 05 11:43:37 2000 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Jan 05 11:45:01 2000 +0100
@@ -2,8 +2,8 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-The 'obtain' language element -- achieves (eliminated) existential
-quantification at proof command level.
+The 'obtain' language element -- eliminated existential quantification
+at the level of proof texts.
 
 The common case:
 
@@ -32,94 +32,118 @@
     proof succeed
       fix x
       assume antecedent: G x
-      def thesis == ?thesis_prop x
+      def thesis == C x
       presume that: !!a. P a ==> thesis
       from goal_facts show thesis <proof>
     next
       fix a
       assume P a
 
+TODO:
+  - bind terms for goal as well (done?);
+  - improve block structure (admit subsequent occurences of 'next') (no?);
+  - handle general case (easy??);
+*)
 
-TODO:
-  - handle general case;
-*)
+signature OBTAIN_DATA =
+sig
+  val that_atts: Proof.context attribute list
+end;
 
 signature OBTAIN =
 sig
-  val obtain: (string list * string option) list
-    -> (string * Proof.context attribute list * (string * (string list * string list)) list) list
-    -> Proof.state -> Proof.state Seq.seq
-  val obtain_i: (string list * typ option) list
-    -> (string * Proof.context attribute list * (term * (term list * term list)) list) list
-    -> Proof.state -> Proof.state Seq.seq
+  val obtain: ((string list * string option) * Comment.text) list
+    * ((string * Args.src list * (string * (string list * string list)) list)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val obtain_i: ((string list * typ option) * Comment.text) list
+    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
+      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
 end;
 
-structure Obtain: OBTAIN =
+functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
 struct
 
+
+(** obtain(_i) **)
+
 val thatN = "that";
 
-fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state =
+fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
   let
+    (*thesis*)
     val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
 
-    val parms = Logic.strip_params prop;
-    val hyps = Logic.strip_assums_hyp prop;
-    val concl = Logic.strip_assums_concl prop;
+    val parms = Logic.strip_params prop;        (* FIXME unused *)
     val _ =
       if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
-
+    val hyps = Logic.strip_assums_hyp prop;     (* FIXME unused *)
+    val concl = Logic.strip_assums_concl prop;
     val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
 
-
-    fun fix_vars (ctxt, (xs, raw_T)) =
-      let
-        val T = apsome (prep_typ ctxt) raw_T;
-        val ctxt' = ProofContext.fix_i [(xs, T)] ctxt;
-      in (ctxt', map (ProofContext.cert_skolem ctxt') xs) end;
+    (*vars*)
+    val (vars_ctxt, vars) =
+      foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
+    val xs = flat (map fst vars);
 
-    fun prep_asm (ctxt, (_, _, raw_propps)) =
-      let val ts = map (prep_prop ctxt) (map fst raw_propps);
-      in (ctxt |> ProofContext.declare_terms ts, ts) end;
+    (*asms*)
+    fun prep_asm (ctxt, (name, src, raw_propps)) =
+      let
+        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
+        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
+      in (ctxt', (name, atts, propps)) end;
 
-    val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
-    val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
-    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
+    val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
+    val asm_props = flat (map (map fst o #3) asms);
+    val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
 
+    (*that_prop*)
     fun find_free x t =
       (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
-    fun find_skolem x = Library.get_first (find_free x) asms;
-    val skolemTs = mapfilter find_skolem skolems;
-
+    fun occs_var x = Library.get_first (find_free x) asm_props;
     val that_prop =
-      Logic.list_rename_params (map (Syntax.dest_skolem o #1) skolemTs,
-        Term.list_all_free (skolemTs, Logic.list_implies (asms, atomic_thesis)));
-
-    val presume_stateq =
-      state
-      |> Method.proof (Some (Method.Basic (K Method.succeed)))
-      |> Seq.map (fn st => st
-        |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
-        |> Proof.presume_i [(thatN, [], [(that_prop, ([], []))])]);
+      Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));
 
     fun after_qed st =
       st
       |> Proof.next_block
-      |> fix raw_vars           (*prepared twice!*)
-      |> assume raw_asms        (*prepared twice!*)
+      |> Proof.fix_i vars
+      |> Proof.assume_i asms
       |> Seq.single;
   in
-    presume_stateq
+    state
+    |> Method.proof (Some (Method.Basic (K Method.succeed)))
     |> Seq.map (fn st => st
+      |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
+      |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
       |> Proof.from_facts goal_facts
-      |> Proof.show_i after_qed "" [] (atomic_thesis, ([], []))
-      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts st)))))
-    |> Seq.flat
+      |> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])))
   end;
 
 
-val obtain = gen_obtain ProofContext.read_typ ProofContext.read_prop Proof.fix Proof.assume;
-val obtain_i = gen_obtain ProofContext.cert_typ ProofContext.cert_prop Proof.fix_i Proof.assume_i;
+val obtain = ProofHistory.applys o
+  (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
+
+val obtain_i = ProofHistory.applys o
+  (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
+
+
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+val obtainP =
+  OuterSyntax.command "obtain" "proof text-level existential quantifier"
+    K.prf_asm_goal
+    (Scan.optional
+      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
+        --| P.$$$ "in") [] --
+      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
+    >> (Toplevel.print oo (Toplevel.proof o obtain)));
+
+val _ = OuterSyntax.add_parsers [obtainP];
+
+end;
 
 
 end;