improved messages;
authorwenzelm
Wed Feb 27 21:53:33 2002 +0100 (2002-02-27)
changeset 12970c9b1838a2cc0
parent 12969 d860fa102386
child 12971 92195e8c6208
improved messages;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Feb 27 21:53:12 2002 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Feb 27 21:53:33 2002 +0100
     1.3 @@ -9,23 +9,25 @@
     1.4    <chain_facts>
     1.5    obtain x where "P x" <proof> ==
     1.6  
     1.7 -  {
     1.8 +  have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
     1.9 +  proof succeed
    1.10      fix thesis
    1.11 -    assume that [intro]: "!!x. P x ==> thesis"
    1.12 -    <chain_facts> have thesis <proof (insert that)>
    1.13 -  }
    1.14 +    assume that [intro?]: "!!x. P x ==> thesis"
    1.15 +    <chain_facts> show thesis <proof (insert that)>
    1.16 +  qed
    1.17    fix x assm (obtained) "P x"
    1.18 -
    1.19  *)
    1.20  
    1.21  signature OBTAIN =
    1.22  sig
    1.23    val obtain: (string list * string option) list ->
    1.24      ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
    1.25 -    -> Proof.state -> Proof.state Seq.seq
    1.26 +    -> (Proof.context -> string * (string * thm list) list -> unit) *
    1.27 +      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.28    val obtain_i: (string list * typ option) list ->
    1.29      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    1.30 -    -> Proof.state -> Proof.state Seq.seq
    1.31 +    -> (Proof.context -> string * (string * thm list) list -> unit) *
    1.32 +      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.33  end;
    1.34  
    1.35  structure Obtain: OBTAIN =
    1.36 @@ -62,7 +64,7 @@
    1.37  
    1.38  val thatN = "that";
    1.39  
    1.40 -fun gen_obtain prep_vars prep_propp raw_vars raw_asms state =
    1.41 +fun gen_obtain prep_vars prep_propp raw_vars raw_asms print state =
    1.42    let
    1.43      val _ = Proof.assert_forward_or_chain state;
    1.44      val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    1.45 @@ -81,10 +83,15 @@
    1.46  
    1.47      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    1.48  
    1.49 -    (*that_prop*)
    1.50 +    (*obtain statements*)
    1.51      val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
    1.52 -    val bound_thesis =
    1.53 -      ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);
    1.54 +    val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
    1.55 +    val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment sign thesisN);
    1.56 +    val bound_thesis_raw as (bound_thesis_name, _) =
    1.57 +      Term.dest_Free (bind_thesis (Free (thesisN, propT)));
    1.58 +    val bound_thesis_var =
    1.59 +      foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
    1.60 +        | (v, t) => v) (bound_thesis_raw, bound_thesis);
    1.61  
    1.62      fun occs_var x = Library.get_first (fn t =>
    1.63        ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.64 @@ -96,27 +103,30 @@
    1.65      val that_prop =
    1.66        Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
    1.67        |> Library.curry Logic.list_rename_params (map #2 parm_names);
    1.68 +    val obtain_prop =
    1.69 +      Logic.list_rename_params ([AutoBind.thesisN],
    1.70 +        Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
    1.71  
    1.72      fun after_qed st = st
    1.73 -      |> Proof.end_block
    1.74 +      |> Method.local_qed false None print
    1.75        |> Seq.map (fn st' => st'
    1.76          |> Proof.fix_i vars
    1.77          |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
    1.78    in
    1.79      state
    1.80      |> Proof.enter_forward
    1.81 -    |> Proof.begin_block
    1.82 +    |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
    1.83 +    |> Method.proof (Some (Method.Basic (K Method.succeed))) |> Seq.hd
    1.84      |> Proof.fix_i [([thesisN], None)]
    1.85      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
    1.86      |> (fn state' =>
    1.87 -      state'
    1.88 -      |> Proof.from_facts chain_facts
    1.89 -      |> Proof.have_i after_qed [(("", []), [(bound_thesis, ([], []))])]
    1.90 -      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
    1.91 +        state'
    1.92 +        |> Proof.from_facts chain_facts
    1.93 +        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    1.94 +        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
    1.95    end;
    1.96  
    1.97  val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
    1.98  val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
    1.99  
   1.100 -
   1.101  end;