# HG changeset patch # User wenzelm # Date 1162924790 -3600 # Node ID 9c96c1ec235f56a1dd0d01199201d19f32f81b85 # Parent 54faccb5d6f6371f60ce089c813dd5b36f1a130e moved statement to specification.ML; diff -r 54faccb5d6f6 -r 9c96c1ec235f src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Tue Nov 07 19:39:48 2006 +0100 +++ b/src/Pure/Isar/obtain.ML Tue Nov 07 19:39:50 2006 +0100 @@ -39,6 +39,7 @@ signature OBTAIN = sig + val thatN: string val obtain: string -> (string * string option * mixfix) list -> ((string * Attrib.src list) * (string * string list) list) list -> bool -> Proof.state -> Proof.state @@ -49,11 +50,6 @@ (cterm list * thm list) * Proof.context val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state - val statement: (string * ((string * 'typ option) list * 'term list)) list -> - (('typ, 'term, 'fact) Element.ctxt list * - ((string * Attrib.src list) * ('term * 'term list) list) list) * - (((string * Attrib.src list) * (term * term list) list) list -> Proof.context -> - (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context) end; structure Obtain: OBTAIN = @@ -318,45 +314,4 @@ end; - - -(** statements with several cases **) - -fun statement cases = - let - val names = - cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); - val elems = cases |> map (fn (_, (vars, _)) => - Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))); - val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props)); - - fun mk_stmt stmt ctxt = - let - val thesis = - ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; - val atts = map Attrib.internal - [RuleCases.consumes (~ (length cases)), RuleCases.case_names names]; - - fun assume_case ((name, (vars, _)), (_, propp)) ctxt' = - let - val xs = map fst vars; - val props = map fst propp; - val (parms, _) = ctxt' - |> fold Variable.declare_term props - |> fold_map ProofContext.inferred_param xs; - val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); - in - ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); - ctxt' |> Variable.fix_frees asm - |> ProofContext.add_assms_i Assumption.assume_export - [((name, [ContextRules.intro_query NONE]), [(asm, [])])] - |>> (fn [(_, [th])] => th) - end; - val (ths, ctxt') = ctxt - |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) - |> fold_map assume_case (cases ~~ stmt) - |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths); - in (([(("", atts), [(thesis, [])])], ths), ctxt') end; - in ((elems, concl), mk_stmt) end; - end;