# HG changeset patch # User wenzelm # Date 938803013 -7200 # Node ID 99305245f6bd04ccf726256ee1db34414143aac2 # Parent b8e7fa177d62849eef9843fb1ca166c8775df887 The 'obtain' language element -- achieves (eliminated) existential quantification proof command level. diff -r b8e7fa177d62 -r 99305245f6bd src/Pure/Isar/obtain.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/obtain.ML Fri Oct 01 20:36:53 1999 +0200 @@ -0,0 +1,124 @@ +(* Title: Pure/Isar/obtain.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +The 'obtain' language element -- achieves (eliminated) existential +quantification proof command level. + +The common case: + + + have/show C + obtain a in P[a] == + + + have/show C + proof succeed + def thesis == C + presume that: !!a. P a ==> thesis + from goal_facts show thesis + next + fix a + assume P a + +The general case: + + + have/show !!x. G x ==> C x + obtain a in P[a] == + + + have/show !!x. G x ==> C x + proof succeed + fix x + assume antecedent: G x + def thesis == ?thesis_prop x + presume that: !!a. P a ==> thesis + from goal_facts show thesis + next + fix a + assume P a + + +TODO: + - handle general case; +*) + +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 +end; + +structure Obtain: OBTAIN = +struct + +val thatN = "that"; + +fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state = + let + 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 _ = + if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state); + + 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; + + 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; + + 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)); + + 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; + + 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, ([], []))])]); + + fun after_qed st = + st + |> Proof.next_block + |> fix raw_vars (*prepared twice!*) + |> assume raw_asms (*prepared twice!*) + |> Seq.single; + in + presume_stateq + |> Seq.map (fn st => st + |> 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 + 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; + + +end;