src/Pure/Isar/obtain.ML
changeset 18897 b31293969d4f
parent 18870 020e242c02a0
child 18907 f984f22f1cb4
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Feb 02 12:52:21 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Feb 02 12:52:24 2006 +0100
     1.3 @@ -39,14 +39,20 @@
     1.4  
     1.5  signature OBTAIN =
     1.6  sig
     1.7 -  val obtain: (string * string option) list ->
     1.8 +  val obtain: string -> (string * string option) list ->
     1.9      ((string * Attrib.src list) * (string * (string list * string list)) list) list
    1.10      -> bool -> Proof.state -> Proof.state
    1.11 -  val obtain_i: (string * typ option) list ->
    1.12 +  val obtain_i: string -> (string * typ option) list ->
    1.13      ((string * attribute list) * (term * (term list * term list)) list) list
    1.14      -> bool -> Proof.state -> Proof.state
    1.15    val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
    1.16    val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
    1.17 +  val statement: (string * ((string * 'typ option) list * 'term list)) list ->
    1.18 +    (('typ, 'term, 'fact) Element.ctxt list *
    1.19 +      ((string * 'a list) * ('term * ('term list * 'term list)) list) list) *
    1.20 +    (((string * 'b list) * (term * (term list * term list)) list) list -> Proof.context ->
    1.21 +      (((string * 'c list) * (term * (term list * term list)) list) list * thm list) *
    1.22 +        Proof.context)
    1.23  end;
    1.24  
    1.25  structure Obtain: OBTAIN =
    1.26 @@ -56,12 +62,11 @@
    1.27  (** obtain_export **)
    1.28  
    1.29  (*
    1.30 -    [x]
    1.31 -    [A x]
    1.32 -      :
    1.33 -      B
    1.34 -    -----
    1.35 -      B
    1.36 +  [x, A x]
    1.37 +     :
    1.38 +     B
    1.39 +  --------
    1.40 +     B
    1.41  *)
    1.42  fun obtain_export ctxt parms rule cprops thm =
    1.43    let
    1.44 @@ -95,11 +100,12 @@
    1.45      val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
    1.46    in (v, t) end;
    1.47  
    1.48 +val thatN = "that";
    1.49 +
    1.50  local
    1.51  
    1.52 -val thatN = "that";
    1.53 -
    1.54 -fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state =
    1.55 +fun gen_obtain prep_att prep_vars prep_propp
    1.56 +    name raw_vars raw_asms int state =
    1.57    let
    1.58      val _ = Proof.assert_forward_or_chain state;
    1.59      val ctxt = Proof.context_of state;
    1.60 @@ -129,6 +135,7 @@
    1.61      val parm_names =
    1.62        List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
    1.63  
    1.64 +    val that_name = if name = "" then thatN else name;
    1.65      val that_prop =
    1.66        Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis))
    1.67        |> Library.curry Logic.list_rename_params (map #2 parm_names);
    1.68 @@ -147,7 +154,7 @@
    1.69      |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
    1.70      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.71      |> Proof.fix_i [(thesisN, NONE)]
    1.72 -    |> Proof.assume_i [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
    1.73 +    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
    1.74      |> `Proof.the_facts
    1.75      ||> Proof.chain_facts chain_facts
    1.76      ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
    1.77 @@ -268,4 +275,40 @@
    1.78  
    1.79  end;
    1.80  
    1.81 +
    1.82 +
    1.83 +(** statements with several cases **)
    1.84 +
    1.85 +fun statement cases =
    1.86 +  let
    1.87 +    val elems = cases |> map (fn (_, (vars, _)) =>
    1.88 +      Element.Constrains (vars |> List.mapPartial (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
    1.89 +    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
    1.90 +
    1.91 +    fun mk_stmt stmt ctxt =
    1.92 +      let
    1.93 +        val thesis =
    1.94 +          ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
    1.95 +        fun assume_case ((name, (vars, _)), (_, propp)) ctxt' =
    1.96 +          let
    1.97 +            val xs = map fst vars;
    1.98 +            val props = map fst propp;
    1.99 +            val (parms, ctxt'') =
   1.100 +              ctxt'
   1.101 +              |> fold ProofContext.declare_term props
   1.102 +              |> fold_map ProofContext.inferred_param xs;
   1.103 +            val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
   1.104 +          in
   1.105 +            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
   1.106 +            ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
   1.107 +              [((name, [ContextRules.intro_query NONE]), [(asm, ([], []))])]
   1.108 +            |>> (fn [(_, [th])] => th)
   1.109 +          end;
   1.110 +        val (ths, ctxt') = ctxt
   1.111 +          |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
   1.112 +          |> fold_map assume_case (cases ~~ stmt)
   1.113 +          |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
   1.114 +      in (([(("", []), [(thesis, ([], []))])], ths), ctxt') end;
   1.115 +  in ((elems, concl), mk_stmt) end;
   1.116 +
   1.117  end;