wenzelm@7674: (*  Title:      Pure/Isar/obtain.ML
wenzelm@7674:     ID:         $Id$
wenzelm@7674:     Author:     Markus Wenzel, TU Muenchen
wenzelm@8807:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@7674: 
wenzelm@8543: The 'obtain' language element -- generalized existence at the level of
wenzelm@8543: proof texts.
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@8543:       assume hyps: G x
wenzelm@8094:       def thesis == C 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@8094: *)
wenzelm@7674: 
wenzelm@8094: signature OBTAIN_DATA =
wenzelm@8094: sig
wenzelm@8094:   val that_atts: Proof.context attribute list
wenzelm@8094: end;
wenzelm@7674: 
wenzelm@7674: signature OBTAIN =
wenzelm@7674: sig
wenzelm@8094:   val obtain: ((string list * string option) * Comment.text) list
wenzelm@8094:     * ((string * Args.src list * (string * (string list * string list)) list)
wenzelm@8094:       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
wenzelm@8094:   val obtain_i: ((string list * typ option) * Comment.text) list
wenzelm@8094:     * ((string * Proof.context attribute list * (term * (term list * term list)) list)
wenzelm@8094:       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
wenzelm@7674: end;
wenzelm@7674: 
wenzelm@8094: functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
wenzelm@7674: struct
wenzelm@7674: 
wenzelm@8094: 
wenzelm@8094: (** obtain(_i) **)
wenzelm@8094: 
wenzelm@7674: val thatN = "that";
wenzelm@8543: val hypsN = "hyps";
wenzelm@7674: 
wenzelm@8094: fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
wenzelm@7674:   let
wenzelm@8543:     val _ = Proof.assert_backward state;
wenzelm@7674: 
wenzelm@8543:     (*obtain vars*)
wenzelm@8094:     val (vars_ctxt, vars) =
wenzelm@8094:       foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
wenzelm@8094:     val xs = flat (map fst vars);
wenzelm@7674: 
wenzelm@8543:     (*obtain asms*)
wenzelm@8094:     fun prep_asm (ctxt, (name, src, raw_propps)) =
wenzelm@8094:       let
wenzelm@8094:         val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
wenzelm@8094:         val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
wenzelm@8094:       in (ctxt', (name, atts, propps)) end;
wenzelm@7674: 
wenzelm@8094:     val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
wenzelm@8094:     val asm_props = flat (map (map fst o #3) asms);
wenzelm@8094:     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
wenzelm@7674: 
wenzelm@8543:     (*thesis*)
wenzelm@8543:     val (prop, (goal_facts, goal)) = Proof.get_goal state;
wenzelm@8543: 
wenzelm@8543:     val parms = Logic.strip_params prop;
wenzelm@8543:     val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs));
wenzelm@8543:     val parm_types = map #2 parms;
wenzelm@8543:     val parm_vars = map Library.single parm_names ~~ map Some parm_types;
wenzelm@8543: 
wenzelm@8543:     val frees = map2 Free (parm_names, parm_types);
wenzelm@8543:     val rev_frees = rev frees;
wenzelm@8543: 
wenzelm@8543:     val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop);
wenzelm@8543:     val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop);
wenzelm@8543:     val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
wenzelm@8543: 
wenzelm@8094:     (*that_prop*)
wenzelm@7674:     fun find_free x t =
wenzelm@8614:       (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
wenzelm@8094:     fun occs_var x = Library.get_first (find_free x) asm_props;
wenzelm@7674:     val that_prop =
wenzelm@8094:       Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));
wenzelm@7674: 
wenzelm@7674:     fun after_qed st =
wenzelm@7674:       st
wenzelm@7674:       |> Proof.next_block
wenzelm@8094:       |> Proof.fix_i vars
wenzelm@8094:       |> Proof.assume_i asms
wenzelm@7674:       |> Seq.single;
wenzelm@7674:   in
wenzelm@8094:     state
wenzelm@8094:     |> Method.proof (Some (Method.Basic (K Method.succeed)))
wenzelm@7674:     |> Seq.map (fn st => st
wenzelm@8543:       |> Proof.fix_i parm_vars
wenzelm@8543:       |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)]
wenzelm@8094:       |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
wenzelm@8094:       |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
wenzelm@7674:       |> Proof.from_facts goal_facts
wenzelm@8094:       |> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])))
wenzelm@7674:   end;
wenzelm@7674: 
wenzelm@7674: 
wenzelm@8094: val obtain = ProofHistory.applys o
wenzelm@8094:   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
wenzelm@8094: 
wenzelm@8094: val obtain_i = ProofHistory.applys o
wenzelm@8094:   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
wenzelm@8094: 
wenzelm@8094: 
wenzelm@8094: 
wenzelm@8094: (** outer syntax **)
wenzelm@8094: 
wenzelm@8094: local structure P = OuterParse and K = OuterSyntax.Keyword in
wenzelm@8094: 
wenzelm@8094: val obtainP =
wenzelm@8543:   OuterSyntax.command "obtain" "generalized existence"
wenzelm@8094:     K.prf_asm_goal
wenzelm@8094:     (Scan.optional
wenzelm@8094:       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
wenzelm@8109:         --| P.$$$ "where") [] --
wenzelm@8094:       P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
wenzelm@8094:     >> (Toplevel.print oo (Toplevel.proof o obtain)));
wenzelm@8094: 
wenzelm@8109: val _ = OuterSyntax.add_keywords ["where"];
wenzelm@8094: val _ = OuterSyntax.add_parsers [obtainP];
wenzelm@8094: 
wenzelm@8094: end;
wenzelm@7674: 
wenzelm@7674: 
wenzelm@7674: end;