wenzelm@7674: (* Title: Pure/Isar/obtain.ML wenzelm@7674: ID: $Id$ wenzelm@7674: Author: Markus Wenzel, TU Muenchen wenzelm@7674: wenzelm@8543: The 'obtain' language element -- generalized existence at the level of wenzelm@8543: proof texts. wenzelm@7674: wenzelm@9468: wenzelm@9468: obtain x where "P x" == wenzelm@7674: wenzelm@12970: have "!!thesis. (!!x. P x ==> thesis) ==> thesis" wenzelm@12970: proof succeed wenzelm@9468: fix thesis wenzelm@12970: assume that [intro?]: "!!x. P x ==> thesis" wenzelm@12970: show thesis wenzelm@12970: qed wenzelm@10379: fix x assm (obtained) "P x" wenzelm@8094: *) wenzelm@7674: wenzelm@7674: signature OBTAIN = wenzelm@7674: sig wenzelm@11890: val obtain: (string list * string option) list -> wenzelm@17111: ((string * Attrib.src list) * (string * (string list * string list)) list) list wenzelm@17357: -> bool -> Proof.state -> Proof.state wenzelm@11890: val obtain_i: (string list * typ option) list -> wenzelm@11890: ((string * Proof.context attribute list) * (term * (term list * term list)) list) list wenzelm@17357: -> bool -> Proof.state -> Proof.state wenzelm@7674: end; wenzelm@7674: wenzelm@10379: structure Obtain: OBTAIN = wenzelm@7674: struct wenzelm@7674: wenzelm@8094: wenzelm@11816: (** export_obtain **) wenzelm@9468: wenzelm@11816: fun export_obtain state parms rule _ cprops thm = wenzelm@9468: let wenzelm@17111: val {thy, prop, maxidx, ...} = Thm.rep_thm thm; wenzelm@17111: val cparms = map (Thm.cterm_of thy) parms; wenzelm@9468: wenzelm@9468: val thm' = thm wenzelm@11816: |> Drule.implies_intr_goals cprops wenzelm@9468: |> Drule.forall_intr_list cparms wenzelm@9468: |> Drule.forall_elim_vars (maxidx + 1); wenzelm@11816: val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal); 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@12055: space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state) wenzelm@17111: else if not (ObjectLogic.is_judgment thy (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@17357: fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state = wenzelm@7674: let wenzelm@9468: val _ = Proof.assert_forward_or_chain state; wenzelm@17357: val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; wenzelm@10464: val thy = Proof.theory_of state; wenzelm@7674: wenzelm@8543: (*obtain vars*) wenzelm@11890: val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars); skalberg@15570: val xs = List.concat (map fst vars); wenzelm@10582: val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars; wenzelm@7674: wenzelm@8543: (*obtain asms*) wenzelm@11890: val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); skalberg@15570: val asm_props = List.concat (map (map fst) proppss); wenzelm@17111: val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; wenzelm@10464: wenzelm@10582: val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt; wenzelm@7674: wenzelm@12970: (*obtain statements*) wenzelm@16606: val thesisN = Term.variant xs AutoBind.thesisN; wenzelm@12970: val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN]; wenzelm@17111: val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment thy thesisN); wenzelm@12970: val bound_thesis_raw as (bound_thesis_name, _) = wenzelm@12970: Term.dest_Free (bind_thesis (Free (thesisN, propT))); wenzelm@12970: val bound_thesis_var = haftmann@16787: fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v) haftmann@16787: | _ => I) bound_thesis bound_thesis_raw; 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; skalberg@15570: val parms = List.mapPartial I raw_parms; wenzelm@10582: val parm_names = skalberg@15570: List.mapPartial (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@12970: val obtain_prop = wenzelm@12970: Logic.list_rename_params ([AutoBind.thesisN], wenzelm@12970: Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis))); wenzelm@7674: wenzelm@17357: fun after_qed _ _ = wenzelm@17357: Proof.local_qed (NONE, false) wenzelm@17357: #> Seq.map (`Proof.the_fact #-> (fn this => wenzelm@17357: Proof.fix_i vars wenzelm@17357: #> Proof.assm_i (export_obtain state parms this) asms)); wenzelm@7674: in wenzelm@8094: state wenzelm@9468: |> Proof.enter_forward wenzelm@17357: |> Proof.have_i (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int wenzelm@17111: |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd skalberg@15531: |> Proof.fix_i [([thesisN], NONE)] skalberg@15531: |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])] wenzelm@16842: |> `Proof.the_facts wenzelm@17357: ||> Proof.chain_facts chain_facts wenzelm@17357: ||> Proof.show_i after_qed [(("", []), [(bound_thesis, ([], []))])] false wenzelm@17357: |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd wenzelm@7674: end; wenzelm@7674: wenzelm@17111: val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp; wenzelm@17111: val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp; wenzelm@8094: wenzelm@8094: end;