1.1 --- a/src/Pure/Isar/obtain.ML	Tue Mar 21 00:17:56 2000 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Mar 21 00:18:54 2000 +0100
     1.3 @@ -2,8 +2,8 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -The 'obtain' language element -- eliminated existential quantification
     1.8 -at the level of proof texts.
     1.9 +The 'obtain' language element -- generalized existence at the level of
    1.10 +proof texts.
    1.11  
    1.12  The common case:
    1.13  
    1.14 @@ -31,18 +31,13 @@
    1.15      have/show !!x. G x ==> C x
    1.16      proof succeed
    1.17        fix x
    1.18 -      assume antecedent: G x
    1.19 +      assume hyps: G x
    1.20        def thesis == C x
    1.21        presume that: !!a. P a ==> thesis
    1.22        from goal_facts show thesis <proof>
    1.23      next
    1.24        fix a
    1.25        assume P a
    1.26 -
    1.27 -TODO:
    1.28 -  - bind terms for goal as well (done?);
    1.29 -  - improve block structure (admit subsequent occurences of 'next') (no?);
    1.30 -  - handle general case (easy??);
    1.31  *)
    1.32  
    1.33  signature OBTAIN_DATA =
    1.34 @@ -67,25 +62,18 @@
    1.35  (** obtain(_i) **)
    1.36  
    1.37  val thatN = "that";
    1.38 +val hypsN = "hyps";
    1.39  
    1.40  fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    1.41    let
    1.42 -    (*thesis*)
    1.43 -    val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
    1.44 +    val _ = Proof.assert_backward state;
    1.45  
    1.46 -    val parms = Logic.strip_params prop;        (* FIXME unused *)
    1.47 -    val _ =
    1.48 -      if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
    1.49 -    val hyps = Logic.strip_assums_hyp prop;     (* FIXME unused *)
    1.50 -    val concl = Logic.strip_assums_concl prop;
    1.51 -    val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    1.52 -
    1.53 -    (*vars*)
    1.54 +    (*obtain vars*)
    1.55      val (vars_ctxt, vars) =
    1.56        foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    1.57      val xs = flat (map fst vars);
    1.58  
    1.59 -    (*asms*)
    1.60 +    (*obtain asms*)
    1.61      fun prep_asm (ctxt, (name, src, raw_propps)) =
    1.62        let
    1.63          val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    1.64 @@ -96,6 +84,21 @@
    1.65      val asm_props = flat (map (map fst o #3) asms);
    1.66      val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    1.67  
    1.68 +    (*thesis*)
    1.69 +    val (prop, (goal_facts, goal)) = Proof.get_goal state;
    1.70 +
    1.71 +    val parms = Logic.strip_params prop;
    1.72 +    val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs));
    1.73 +    val parm_types = map #2 parms;
    1.74 +    val parm_vars = map Library.single parm_names ~~ map Some parm_types;
    1.75 +
    1.76 +    val frees = map2 Free (parm_names, parm_types);
    1.77 +    val rev_frees = rev frees;
    1.78 +
    1.79 +    val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop);
    1.80 +    val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop);
    1.81 +    val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    1.82 +
    1.83      (*that_prop*)
    1.84      fun find_free x t =
    1.85        (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
    1.86 @@ -113,6 +116,8 @@
    1.87      state
    1.88      |> Method.proof (Some (Method.Basic (K Method.succeed)))
    1.89      |> Seq.map (fn st => st
    1.90 +      |> Proof.fix_i parm_vars
    1.91 +      |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)]
    1.92        |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
    1.93        |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
    1.94        |> Proof.from_facts goal_facts
    1.95 @@ -133,7 +138,7 @@
    1.96  local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.97  
    1.98  val obtainP =
    1.99 -  OuterSyntax.command "obtain" "proof text-level existential quantifier"
   1.100 +  OuterSyntax.command "obtain" "generalized existence"
   1.101      K.prf_asm_goal
   1.102      (Scan.optional
   1.103        (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)