author wenzelm Tue Jan 31 18:19:25 2006 +0100 (2006-01-31) changeset 18870 020e242c02a0 parent 18869 00741f7280f7 child 18871 ca48320f6619
 src/Pure/Isar/obtain.ML file | annotate | diff | revisions src/Pure/ROOT.ML file | annotate | diff | revisions
```     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Jan 31 17:48:28 2006 +0100
1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jan 31 18:19:25 2006 +0100
1.3 @@ -8,15 +8,18 @@
1.4  similar, but derives these elements from the course of reasoning!
1.5
1.6    <chain_facts>
1.7 -  obtain x where "P x" <proof> ==
1.8 +  obtain x where "A x" <proof> ==
1.9
1.10 -  have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
1.11 +  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
1.12    proof succeed
1.13      fix thesis
1.14 -    assume that [intro?]: "!!x. P x ==> thesis"
1.15 -    <chain_facts> show thesis <proof (insert that)>
1.16 +    assume that [intro?]: "!!x. A x ==> thesis"
1.17 +    <chain_facts>
1.18 +    show thesis
1.19 +      apply (insert that)
1.20 +      <proof>
1.21    qed
1.22 -  fix x assm (obtained) "P x"
1.23 +  fix x assm <<obtain_export>> "A x"
1.24
1.25
1.26    <chain_facts>
1.27 @@ -25,13 +28,13 @@
1.28    {
1.29      fix thesis
1.30      <chain_facts> have "PROP ?guess"
1.31 -      apply magic      -- {* turns goal into "thesis ==> Goal thesis" *}
1.32 +      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
1.33        <proof body>
1.34 -      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> Goal thesis" into
1.35 -        "Goal ((!!x. P x ==> thesis) ==> thesis)" which is a finished goal state *}
1.36 +      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
1.37 +        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
1.38        <proof end>
1.39    }
1.40 -  fix x assm (obtained) "P x"
1.41 +  fix x assm <<obtain_export>> "A x"
1.42  *)
1.43
1.44  signature OBTAIN =
1.45 @@ -52,6 +55,14 @@
1.46
1.47  (** obtain_export **)
1.48
1.49 +(*
1.50 +    [x]
1.51 +    [A x]
1.52 +      :
1.53 +      B
1.54 +    -----
1.55 +      B
1.56 +*)
1.57  fun obtain_export ctxt parms rule cprops thm =
1.58    let
1.59      val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
1.60 @@ -136,8 +147,7 @@
1.61      |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
1.62      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
1.63      |> Proof.fix_i [(thesisN, NONE)]
1.64 -    |> Proof.assume_i
1.65 -      [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
1.66 +    |> Proof.assume_i [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
1.67      |> `Proof.the_facts
1.68      ||> Proof.chain_facts chain_facts
1.69      ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
```
```     2.1 --- a/src/Pure/ROOT.ML	Tue Jan 31 17:48:28 2006 +0100
2.2 +++ b/src/Pure/ROOT.ML	Tue Jan 31 18:19:25 2006 +0100
2.3 @@ -63,7 +63,7 @@