src/Pure/Isar/obtain.ML
changeset 7674 99305245f6bd
child 7677 de2e468a42c8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/obtain.ML	Fri Oct 01 20:36:53 1999 +0200
     1.3 @@ -0,0 +1,124 @@
     1.4 +(*  Title:      Pure/Isar/obtain.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +The 'obtain' language element -- achieves (eliminated) existential
     1.9 +quantification proof command level.
    1.10 +
    1.11 +The common case:
    1.12 +
    1.13 +    <goal_facts>
    1.14 +    have/show C
    1.15 +      obtain a in P[a] <proof>          ==
    1.16 +
    1.17 +    <goal_facts>
    1.18 +    have/show C
    1.19 +    proof succeed
    1.20 +      def thesis == C
    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 +The general case:
    1.28 +
    1.29 +    <goal_facts>
    1.30 +    have/show !!x. G x ==> C x
    1.31 +      obtain a in P[a] <proof>          ==
    1.32 +
    1.33 +    <goal_facts>
    1.34 +    have/show !!x. G x ==> C x
    1.35 +    proof succeed
    1.36 +      fix x
    1.37 +      assume antecedent: G x
    1.38 +      def thesis == ?thesis_prop x
    1.39 +      presume that: !!a. P a ==> thesis
    1.40 +      from goal_facts show thesis <proof>
    1.41 +    next
    1.42 +      fix a
    1.43 +      assume P a
    1.44 +
    1.45 +
    1.46 +TODO:
    1.47 +  - handle general case;
    1.48 +*)
    1.49 +
    1.50 +signature OBTAIN =
    1.51 +sig
    1.52 +  val obtain: (string list * string option) list
    1.53 +    -> (string * Proof.context attribute list * (string * (string list * string list)) list) list
    1.54 +    -> Proof.state -> Proof.state Seq.seq
    1.55 +  val obtain_i: (string list * typ option) list
    1.56 +    -> (string * Proof.context attribute list * (term * (term list * term list)) list) list
    1.57 +    -> Proof.state -> Proof.state Seq.seq
    1.58 +end;
    1.59 +
    1.60 +structure Obtain: OBTAIN =
    1.61 +struct
    1.62 +
    1.63 +val thatN = "that";
    1.64 +
    1.65 +fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state =
    1.66 +  let
    1.67 +    val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
    1.68 +
    1.69 +    val parms = Logic.strip_params prop;
    1.70 +    val hyps = Logic.strip_assums_hyp prop;
    1.71 +    val concl = Logic.strip_assums_concl prop;
    1.72 +    val _ =
    1.73 +      if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
    1.74 +
    1.75 +    val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    1.76 +
    1.77 +
    1.78 +    fun fix_vars (ctxt, (xs, raw_T)) =
    1.79 +      let
    1.80 +        val T = apsome (prep_typ ctxt) raw_T;
    1.81 +        val ctxt' = ProofContext.fix_i [(xs, T)] ctxt;
    1.82 +      in (ctxt', map (ProofContext.cert_skolem ctxt') xs) end;
    1.83 +
    1.84 +    fun prep_asm (ctxt, (_, _, raw_propps)) =
    1.85 +      let val ts = map (prep_prop ctxt) (map fst raw_propps);
    1.86 +      in (ctxt |> ProofContext.declare_terms ts, ts) end;
    1.87 +
    1.88 +    val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
    1.89 +    val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
    1.90 +
    1.91 +    fun find_free x t =
    1.92 +      (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
    1.93 +    fun find_skolem x = Library.get_first (find_free x) asms;
    1.94 +    val skolemTs = mapfilter find_skolem skolems;
    1.95 +
    1.96 +    val that_prop =
    1.97 +      Logic.list_rename_params (map (Syntax.dest_skolem o #1) skolemTs,
    1.98 +        Term.list_all_free (skolemTs, Logic.list_implies (asms, atomic_thesis)));
    1.99 +
   1.100 +    val presume_stateq =
   1.101 +      state
   1.102 +      |> Method.proof (Some (Method.Basic (K Method.succeed)))
   1.103 +      |> Seq.map (fn st => st
   1.104 +        |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
   1.105 +        |> Proof.presume_i [(thatN, [], [(that_prop, ([], []))])]);
   1.106 +
   1.107 +    fun after_qed st =
   1.108 +      st
   1.109 +      |> Proof.next_block
   1.110 +      |> fix raw_vars           (*prepared twice!*)
   1.111 +      |> assume raw_asms        (*prepared twice!*)
   1.112 +      |> Seq.single;
   1.113 +  in
   1.114 +    presume_stateq
   1.115 +    |> Seq.map (fn st => st
   1.116 +      |> Proof.from_facts goal_facts
   1.117 +      |> Proof.show_i after_qed "" [] (atomic_thesis, ([], []))
   1.118 +      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts st)))))
   1.119 +    |> Seq.flat
   1.120 +  end;
   1.121 +
   1.122 +
   1.123 +val obtain = gen_obtain ProofContext.read_typ ProofContext.read_prop Proof.fix Proof.assume;
   1.124 +val obtain_i = gen_obtain ProofContext.cert_typ ProofContext.cert_prop Proof.fix_i Proof.assume_i;
   1.125 +
   1.126 +
   1.127 +end;