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@9468:   <chain_facts>
wenzelm@9468:   obtain x where "P x" <proof> ==
wenzelm@7674: 
wenzelm@9468:   {
wenzelm@9468:     fix thesis
wenzelm@11021:     assume that [intro]: "!!x. P x ==> thesis"
wenzelm@10379:     <chain_facts> have thesis <proof (insert that)>
wenzelm@9468:   }
wenzelm@10379:   fix x assm (obtained) "P x"
wenzelm@7674: 
wenzelm@8094: *)
wenzelm@7674: 
wenzelm@7674: signature OBTAIN =
wenzelm@7674: sig
wenzelm@8094:   val obtain: ((string list * string option) * Comment.text) list
wenzelm@10464:     * (((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@10464:     * (((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@10379: structure Obtain: OBTAIN =
wenzelm@7674: struct
wenzelm@7674: 
wenzelm@8094: 
wenzelm@9481: (** disch_obtained **)
wenzelm@9468: 
wenzelm@9468: fun disch_obtained state parms rule cprops thm =
wenzelm@9468:   let
wenzelm@9468:     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
wenzelm@9468:     val cparms = map (Thm.cterm_of sign) parms;
wenzelm@9468: 
wenzelm@9468:     val thm' = thm
wenzelm@9468:       |> Drule.implies_intr_list cprops
wenzelm@9468:       |> Drule.forall_intr_list cparms
wenzelm@9468:       |> Drule.forall_elim_vars (maxidx + 1);
wenzelm@9468:     val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
wenzelm@9468: 
wenzelm@9468:     val concl = Logic.strip_assums_concl prop;
wenzelm@9468:     val bads = parms inter (Term.term_frees concl);
wenzelm@9468:   in
wenzelm@9468:     if not (null bads) then
wenzelm@9481:       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
wenzelm@9468:         space_implode " " (map (Sign.string_of_term sign) bads), state)
wenzelm@9468:     else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
wenzelm@10379:       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
wenzelm@9468:     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
wenzelm@9468:   end;
wenzelm@9468: 
wenzelm@9468: 
wenzelm@9468: 
wenzelm@8094: (** obtain(_i) **)
wenzelm@8094: 
wenzelm@7674: val thatN = "that";
wenzelm@7674: 
wenzelm@8094: fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
wenzelm@7674:   let
wenzelm@9468:     val _ = Proof.assert_forward_or_chain state;
wenzelm@9468:     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
wenzelm@10464:     val thy = Proof.theory_of 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@10582:     val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
wenzelm@7674: 
wenzelm@8543:     (*obtain asms*)
wenzelm@10582:     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map (snd o Comment.ignore) raw_asms);
wenzelm@10464:     val asm_props = flat (map (map fst) proppss);
wenzelm@7674: 
wenzelm@10582:     fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), propps);
wenzelm@10464:     val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
wenzelm@10464: 
wenzelm@10582:     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
wenzelm@7674: 
wenzelm@8094:     (*that_prop*)
wenzelm@10582:     val thesisN = Term.variant xs AutoBind.thesisN;
wenzelm@10582:     val bound_thesis =
wenzelm@10582:       ProofContext.bind_skolem fix_ctxt [thesisN] (AutoBind.atomic_judgment thy thesisN);
wenzelm@9468: 
wenzelm@10582:     fun occs_var x = Library.get_first (fn t =>
wenzelm@10582:       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
wenzelm@10582:     val raw_parms = map occs_var xs;
wenzelm@10582:     val parms = mapfilter I raw_parms;
wenzelm@10582:     val parm_names =
wenzelm@10582:       mapfilter (fn (Some (Free a), x) => Some (a, x) | _ => None) (raw_parms ~~ xs);
wenzelm@10582: 
wenzelm@10582:     val that_prop =
wenzelm@10582:       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
wenzelm@10582:       |> Library.curry Logic.list_rename_params (map #2 parm_names);
wenzelm@7674: 
wenzelm@9481:     fun export_obtained rule =
wenzelm@9481:       (disch_obtained state parms rule, fn _ => fn _ => []);
wenzelm@9481: 
wenzelm@9468:     fun after_qed st = st
wenzelm@9468:       |> Proof.end_block
wenzelm@9468:       |> Seq.map (fn st' => st'
wenzelm@9468:         |> Proof.fix_i vars
wenzelm@9481:         |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
wenzelm@7674:   in
wenzelm@8094:     state
wenzelm@9468:     |> Proof.enter_forward
wenzelm@9468:     |> Proof.begin_block
wenzelm@9468:     |> Proof.fix_i [([thesisN], None)]
wenzelm@10464:     |> Proof.assume_i [((thatN, [Method.intro_local]), [(that_prop, ([], []))])]
wenzelm@10379:     |> (fn state' =>
wenzelm@10379:       state'
wenzelm@10379:       |> Proof.from_facts chain_facts
wenzelm@10379:       |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
wenzelm@10379:       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
wenzelm@7674:   end;
wenzelm@7674: 
wenzelm@7674: 
wenzelm@10379: val obtain = ProofHistory.applys o
wenzelm@8094:   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
wenzelm@8094: 
wenzelm@10379: 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@10464:       P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- 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: end;