(* 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
-> bool -> Proof.state -> Proof.state
val obtain_i: (string list * typ option) list ->
((string * Proof.context attribute list) * (term * (term list * term list)) list) list
-> bool -> Proof.state -> Proof.state
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 int state =
let
val _ = Proof.assert_forward_or_chain state;
val chain_facts = if can Proof.assert_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 (NONE, false)
#> Seq.map (`Proof.the_fact #-> (fn this =>
Proof.fix_i vars
#> Proof.assm_i (export_obtain state parms this) asms));
in
state
|> Proof.enter_forward
|> Proof.have_i (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
|> 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.chain_facts chain_facts
||> Proof.show_i after_qed [(("", []), [(bound_thesis, ([], []))])] false
|-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
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;