--- 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;