src/Pure/Isar/obtain.ML

tuned;

(*  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 * Proof.context attribute 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 {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    val cparms = map (Thm.cterm_of sign) 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 sign (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_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;
    val sign = Theory.sign_of thy;

    (*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 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 sign thesisN);
    val bound_thesis_raw as (bound_thesis_name, _) =
      Term.dest_Free (bind_thesis (Free (thesisN, propT)));
    val bound_thesis_var =
      foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
        | (v, t) => v) (bound_thesis_raw, bound_thesis);

    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 st = st
      |> Method.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 Seq.single true [(("", []), [(obtain_prop, ([], []))])]
    |> Method.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, ([], []))])]
    |> (fn state' =>
        state'
        |> Proof.from_facts chain_facts
        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
  end;

val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;

end;