(*  Title:      Pure/Isar/obtain.ML

     ID:         $Id$

     Author:     Markus Wenzel, TU Muenchen

 The 'obtain' language element -- generalized existence at the level of

 proof texts.

   <chain_facts>

   obtain x where "P x" <proof> ==

   have "!!thesis. (!!x. P x ==> thesis) ==> thesis"

   proof succeed

     fix thesis

     assume that [intro?]: "!!x. P x ==> thesis"

     <chain_facts> show thesis <proof (insert that)>

   qed

   fix x assm (obtained) "P x"

 *)

 signature OBTAIN =

 sig

   val obtain: (string list * string option) list ->

     ((string * Attrib.src list) * (string * (string list * string list)) list) list

     -> (Proof.context -> string * (string * thm list) list -> unit) *

       (Proof.context -> thm -> unit) -> 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.context -> string * (string * thm list) list -> unit) *

       (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq

 end;

 structure Obtain: OBTAIN =

 struct

 (** export_obtain **)

 fun export_obtain state parms rule _ cprops thm =

   let

     val {thy, prop, maxidx, ...} = Thm.rep_thm thm;

     val cparms = map (Thm.cterm_of thy) parms;

     val thm' = thm

       |> Drule.implies_intr_goals cprops

       |> Drule.forall_intr_list cparms

       |> Drule.forall_elim_vars (maxidx + 1);

     val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);

     val concl = Logic.strip_assums_concl prop;

     val bads = parms inter (Term.term_frees concl);

   in

     if not (null bads) then

       raise Proof.STATE ("Conclusion contains obtained parameters: " ^

         space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)

     else if not (ObjectLogic.is_judgment thy (Logic.strip_assums_concl prop)) then

       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)

     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule

   end;

 (** obtain(_i) **)

 val thatN = "that";

 fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms print state =

   let

     val _ = Proof.assert_forward_or_chain state;

     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];

     val thy = Proof.theory_of state;

     (*obtain vars*)

     val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);

     val xs = List.concat (map fst vars);

     val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;

     (*obtain asms*)

     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);

     val asm_props = List.concat (map (map fst) proppss);

     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;

     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;

     (*obtain statements*)

     val thesisN = Term.variant xs AutoBind.thesisN;

     val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];

     val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment thy thesisN);

     val bound_thesis_raw as (bound_thesis_name, _) =

       Term.dest_Free (bind_thesis (Free (thesisN, propT)));

     val bound_thesis_var =

       fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v)

         | _ => I) bound_thesis bound_thesis_raw;

     fun occs_var x = Library.get_first (fn t =>

       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;

     val raw_parms = map occs_var xs;

     val parms = List.mapPartial I raw_parms;

     val parm_names =

       List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);

     val that_prop =

       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))

       |> Library.curry Logic.list_rename_params (map #2 parm_names);

     val obtain_prop =

       Logic.list_rename_params ([AutoBind.thesisN],

         Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));

     fun after_qed _ =

       Proof.local_qed false NONE print

       #> Seq.map (fn st => st

         |> Proof.fix_i vars

         |> Proof.assm_i (export_obtain state parms (Proof.the_fact st)) asms);

   in

     state

     |> Proof.enter_forward

     |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]

     |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd

     |> Proof.fix_i [([thesisN], NONE)]

     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]

     |> `Proof.the_facts

     ||> Proof.from_facts chain_facts

     ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false

     |-> (fn facts => Proof.refine (Method.Basic (K (Method.insert facts))))

   end;

 val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;

 val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;

 end;