moved statement to specification.ML;
authorwenzelm
Tue Nov 07 19:39:50 2006 +0100 (2006-11-07)
changeset 212299c96c1ec235f
parent 21228 54faccb5d6f6
child 21230 abfdce60b371
moved statement to specification.ML;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Nov 07 19:39:48 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Nov 07 19:39:50 2006 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4  
     1.5  signature OBTAIN =
     1.6  sig
     1.7 +  val thatN: string
     1.8    val obtain: string -> (string * string option * mixfix) list ->
     1.9      ((string * Attrib.src list) * (string * string list) list) list ->
    1.10      bool -> Proof.state -> Proof.state
    1.11 @@ -49,11 +50,6 @@
    1.12      (cterm list * thm list) * Proof.context
    1.13    val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.14    val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.15 -  val statement: (string * ((string * 'typ option) list * 'term list)) list ->
    1.16 -    (('typ, 'term, 'fact) Element.ctxt list *
    1.17 -      ((string * Attrib.src list) * ('term * 'term list) list) list) *
    1.18 -    (((string * Attrib.src list) * (term * term list) list) list -> Proof.context ->
    1.19 -      (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context)
    1.20  end;
    1.21  
    1.22  structure Obtain: OBTAIN =
    1.23 @@ -318,45 +314,4 @@
    1.24  
    1.25  end;
    1.26  
    1.27 -
    1.28 -
    1.29 -(** statements with several cases **)
    1.30 -
    1.31 -fun statement cases =
    1.32 -  let
    1.33 -    val names =
    1.34 -      cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
    1.35 -    val elems = cases |> map (fn (_, (vars, _)) =>
    1.36 -      Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
    1.37 -    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props));
    1.38 -
    1.39 -    fun mk_stmt stmt ctxt =
    1.40 -      let
    1.41 -        val thesis =
    1.42 -          ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
    1.43 -        val atts = map Attrib.internal
    1.44 -          [RuleCases.consumes (~ (length cases)), RuleCases.case_names names];
    1.45 -
    1.46 -        fun assume_case ((name, (vars, _)), (_, propp)) ctxt' =
    1.47 -          let
    1.48 -            val xs = map fst vars;
    1.49 -            val props = map fst propp;
    1.50 -            val (parms, _) = ctxt'
    1.51 -              |> fold Variable.declare_term props
    1.52 -              |> fold_map ProofContext.inferred_param xs;
    1.53 -            val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    1.54 -          in
    1.55 -            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
    1.56 -            ctxt' |> Variable.fix_frees asm
    1.57 -            |> ProofContext.add_assms_i Assumption.assume_export
    1.58 -              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    1.59 -            |>> (fn [(_, [th])] => th)
    1.60 -          end;
    1.61 -        val (ths, ctxt') = ctxt
    1.62 -          |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
    1.63 -          |> fold_map assume_case (cases ~~ stmt)
    1.64 -          |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
    1.65 -      in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
    1.66 -  in ((elems, concl), mk_stmt) end;
    1.67 -
    1.68  end;