# HG changeset patch # User wenzelm # Date 964954447 -7200 # Node ID 9adbcf6375c165d784fa2aad876301085975b1ea # Parent 52fb37876254bdde8b6aa6a51cd73fc7a192d96f turned into plain context element; exporter setup; diff -r 52fb37876254 -r 9adbcf6375c1 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Sun Jul 30 12:53:22 2000 +0200 +++ b/src/Pure/Isar/obtain.ML Sun Jul 30 12:54:07 2000 +0200 @@ -6,43 +6,21 @@ The 'obtain' language element -- generalized existence at the level of proof texts. -The common case: - - - have/show C - obtain a in P[a] == - - - have/show C - proof succeed - def thesis == C - presume that: !!a. P a ==> thesis - from goal_facts show thesis - next - fix a - assume P a + + obtain x where "P x" == -The general case: - - - have/show !!x. G x ==> C x - obtain a in P[a] == + { + fix thesis + assume that: "!!x. P x ==> thesis" + have thesis + } + fix x assm(obtained) "P x" - - have/show !!x. G x ==> C x - proof succeed - fix x - assume hyps: G x - def thesis == C x - presume that: !!a. P a ==> thesis - from goal_facts show thesis - next - fix a - assume P a *) signature OBTAIN_DATA = sig + val atomic_thesis: string -> term val that_atts: Proof.context attribute list end; @@ -60,22 +38,51 @@ struct +(** export_obtained **) + +fun disch_obtained 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_list cprops + |> Drule.forall_intr_list cparms + |> Drule.forall_elim_vars (maxidx + 1); + val elim_tacs = replicate (length cprops) Proof.hard_asm_tac; + + val concl = Logic.strip_assums_concl prop; + val bads = parms inter (Term.term_frees concl); + in + if not (null bads) then + raise Proof.STATE ("Result contains illegal parameters: " ^ + space_implode " " (map (Sign.string_of_term sign) bads), state) + else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then + raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state) + else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule + end; + +fun export_obtained state parms rule = + (disch_obtained state parms rule, fn _ => fn _ => []); + + + (** obtain(_i) **) val thatN = "that"; -val hypsN = "hyps"; fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state = let - val _ = Proof.assert_backward state; + val _ = Proof.assert_forward_or_chain state; + val chain_facts = if Proof.is_chain state then Proof.the_facts state else []; (*obtain vars*) val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars); val xs = flat (map fst vars); - val xs_thesis = xs @ [AutoBind.thesisN]; + val thesisN = Term.variant xs AutoBind.thesisN; - val bind_skolem = ProofContext.bind_skolem vars_ctxt xs_thesis; + val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]); fun bind_propp (prop, (pats1, pats2)) = (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2)); @@ -91,52 +98,36 @@ val asm_props = flat asm_propss; val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt; - (*thesis*) - val (prop, (goal_facts, _)) = Proof.get_goal state; - - val parms = Logic.strip_params prop; - val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs_thesis)); - val parm_types = map #2 parms; - val parm_vars = map Library.single parm_names ~~ map Some parm_types; - - val frees = map2 Free (parm_names, parm_types); - val rev_frees = rev frees; - - val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop); - val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop); - val (thesis_term, atomic_thesis) = AutoBind.atomic_thesis concl; - val bound_thesis = bind_skolem atomic_thesis; - (*that_prop*) fun find_free x t = (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None); fun occs_var x = Library.get_first (find_free x) asm_props; - val that_prop = - Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, bound_thesis)); + val xs' = mapfilter occs_var xs; + val parms = map (bind_skolem o Free) xs'; + + val bound_thesis = bind_skolem (Data.atomic_thesis thesisN); + val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis)); - fun after_qed st = - st - |> Proof.next_block - |> Proof.fix_i vars - |> Proof.assume_i asms - |> Seq.single; + fun after_qed st = st + |> Proof.end_block + |> Seq.map (fn st' => st' + |> Proof.fix_i vars + |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms); in state - |> Method.proof (Some (Method.Basic (K Method.succeed))) - |> Seq.map (fn st => st - |> Proof.fix_i parm_vars - |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)] - |> LocalDefs.def_i "" [] ((AutoBind.thesisN, None), (thesis_term, [])) - |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])] - |> Proof.from_facts goal_facts - |> Proof.show_i after_qed "" [] (bound_thesis, ([], []))) + |> Proof.enter_forward + |> Proof.begin_block + |> Proof.fix_i [([thesisN], None)] + |> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])] + |> Proof.from_facts chain_facts + |> Proof.have_i after_qed "" [] (bound_thesis, ([], [])) end; -val obtain = ProofHistory.applys o +val obtain = ProofHistory.apply o (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute); -val obtain_i = ProofHistory.applys o +val obtain_i = ProofHistory.apply o (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I)); @@ -159,5 +150,4 @@ end; - end;