wenzelm@7674: (*  Title:      Pure/Isar/obtain.ML
wenzelm@7674:     ID:         $Id$
wenzelm@7674:     Author:     Markus Wenzel, TU Muenchen
wenzelm@7674: 
wenzelm@7674: The 'obtain' language element -- achieves (eliminated) existential
wenzelm@7677: quantification at proof command level.
wenzelm@7674: 
wenzelm@7674: The common case:
wenzelm@7674: 
wenzelm@7674:     <goal_facts>
wenzelm@7674:     have/show C
wenzelm@7674:       obtain a in P[a] <proof>          ==
wenzelm@7674: 
wenzelm@7674:     <goal_facts>
wenzelm@7674:     have/show C
wenzelm@7674:     proof succeed
wenzelm@7674:       def thesis == C
wenzelm@7674:       presume that: !!a. P a ==> thesis
wenzelm@7674:       from goal_facts show thesis <proof>
wenzelm@7674:     next
wenzelm@7674:       fix a
wenzelm@7674:       assume P a
wenzelm@7674: 
wenzelm@7674: The general case:
wenzelm@7674: 
wenzelm@7674:     <goal_facts>
wenzelm@7674:     have/show !!x. G x ==> C x
wenzelm@7674:       obtain a in P[a] <proof>          ==
wenzelm@7674: 
wenzelm@7674:     <goal_facts>
wenzelm@7674:     have/show !!x. G x ==> C x
wenzelm@7674:     proof succeed
wenzelm@7674:       fix x
wenzelm@7674:       assume antecedent: G x
wenzelm@7674:       def thesis == ?thesis_prop x
wenzelm@7674:       presume that: !!a. P a ==> thesis
wenzelm@7674:       from goal_facts show thesis <proof>
wenzelm@7674:     next
wenzelm@7674:       fix a
wenzelm@7674:       assume P a
wenzelm@7674: 
wenzelm@7674: 
wenzelm@7674: TODO:
wenzelm@7674:   - handle general case;
wenzelm@7674: *)
wenzelm@7674: 
wenzelm@7674: signature OBTAIN =
wenzelm@7674: sig
wenzelm@7674:   val obtain: (string list * string option) list
wenzelm@7674:     -> (string * Proof.context attribute list * (string * (string list * string list)) list) list
wenzelm@7674:     -> Proof.state -> Proof.state Seq.seq
wenzelm@7674:   val obtain_i: (string list * typ option) list
wenzelm@7674:     -> (string * Proof.context attribute list * (term * (term list * term list)) list) list
wenzelm@7674:     -> Proof.state -> Proof.state Seq.seq
wenzelm@7674: end;
wenzelm@7674: 
wenzelm@7674: structure Obtain: OBTAIN =
wenzelm@7674: struct
wenzelm@7674: 
wenzelm@7674: val thatN = "that";
wenzelm@7674: 
wenzelm@7674: fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state =
wenzelm@7674:   let
wenzelm@7674:     val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
wenzelm@7674: 
wenzelm@7674:     val parms = Logic.strip_params prop;
wenzelm@7674:     val hyps = Logic.strip_assums_hyp prop;
wenzelm@7674:     val concl = Logic.strip_assums_concl prop;
wenzelm@7674:     val _ =
wenzelm@7674:       if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
wenzelm@7674: 
wenzelm@7674:     val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
wenzelm@7674: 
wenzelm@7674: 
wenzelm@7674:     fun fix_vars (ctxt, (xs, raw_T)) =
wenzelm@7674:       let
wenzelm@7674:         val T = apsome (prep_typ ctxt) raw_T;
wenzelm@7674:         val ctxt' = ProofContext.fix_i [(xs, T)] ctxt;
wenzelm@7674:       in (ctxt', map (ProofContext.cert_skolem ctxt') xs) end;
wenzelm@7674: 
wenzelm@7674:     fun prep_asm (ctxt, (_, _, raw_propps)) =
wenzelm@7674:       let val ts = map (prep_prop ctxt) (map fst raw_propps);
wenzelm@7674:       in (ctxt |> ProofContext.declare_terms ts, ts) end;
wenzelm@7674: 
wenzelm@7674:     val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
wenzelm@7674:     val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
wenzelm@7674: 
wenzelm@7674:     fun find_free x t =
wenzelm@7674:       (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
wenzelm@7674:     fun find_skolem x = Library.get_first (find_free x) asms;
wenzelm@7674:     val skolemTs = mapfilter find_skolem skolems;
wenzelm@7674: 
wenzelm@7674:     val that_prop =
wenzelm@7674:       Logic.list_rename_params (map (Syntax.dest_skolem o #1) skolemTs,
wenzelm@7674:         Term.list_all_free (skolemTs, Logic.list_implies (asms, atomic_thesis)));
wenzelm@7674: 
wenzelm@7674:     val presume_stateq =
wenzelm@7674:       state
wenzelm@7674:       |> Method.proof (Some (Method.Basic (K Method.succeed)))
wenzelm@7674:       |> Seq.map (fn st => st
wenzelm@7674:         |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
wenzelm@7674:         |> Proof.presume_i [(thatN, [], [(that_prop, ([], []))])]);
wenzelm@7674: 
wenzelm@7674:     fun after_qed st =
wenzelm@7674:       st
wenzelm@7674:       |> Proof.next_block
wenzelm@7674:       |> fix raw_vars           (*prepared twice!*)
wenzelm@7674:       |> assume raw_asms        (*prepared twice!*)
wenzelm@7674:       |> Seq.single;
wenzelm@7674:   in
wenzelm@7674:     presume_stateq
wenzelm@7674:     |> Seq.map (fn st => st
wenzelm@7674:       |> Proof.from_facts goal_facts
wenzelm@7674:       |> Proof.show_i after_qed "" [] (atomic_thesis, ([], []))
wenzelm@7674:       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts st)))))
wenzelm@7674:     |> Seq.flat
wenzelm@7674:   end;
wenzelm@7674: 
wenzelm@7674: 
wenzelm@7674: val obtain = gen_obtain ProofContext.read_typ ProofContext.read_prop Proof.fix Proof.assume;
wenzelm@7674: val obtain_i = gen_obtain ProofContext.cert_typ ProofContext.cert_prop Proof.fix_i Proof.assume_i;
wenzelm@7674: 
wenzelm@7674: 
wenzelm@7674: end;