# HG changeset patch
# User wenzelm
# Date 1434199070 -7200
# Node ID 1f2b29f7843983a50eb77a0805eeb7f3a6657ee2
# Parent  b54b913dfa6ac86b853e34576261d443e48a17dc
clarified 'consider', using structured 'have' statement;

diff -r b54b913dfa6a -r 1f2b29f78439 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Jun 13 13:18:37 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Jun 13 14:37:50 2015 +0200
@@ -6,24 +6,19 @@
 fixes/assumes may be introduced into the present context; 'guess' is
 similar, but derives these elements from the course of reasoning!
 
+
   <chain_facts>
-  consider x where "A x" | y where "B x" | ... <proof> ==
+  obtain x where "A x" <proof> ==
 
-  have "!!thesis. (!!x. A x ==> thesis) ==> (!!x. B x ==> thesis) ==> ... ==> thesis"
+  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
   proof succeed
     fix thesis
-    assume that [intro?]: "!!x. A x ==> thesis" "!!x. B x ==> thesis" ...
+    assume that [intro?]: "!!x. A x ==> thesis"
     <chain_facts>
     show thesis
       apply (insert that)
       <proof>
   qed
-
-
-  <chain_facts>
-  obtain x where "A x" <proof> ==
-
-  consider x where "A x" <chain_facts> <proof>
   fix x assm <<obtain_export>> "A x"
 
 
@@ -171,36 +166,36 @@
 
 
 
-(** consider **)
+(** consider: generalized elimination and cases rule **)
+
+(*
+  consider x where (a) "A x" | y (b) where "B x" | ... ==
+
+  have thesis
+    if a [intro?]: "!!x. A x ==> thesis"
+    and b [intro?]: "!!x. B x ==> thesis"
+    and ...
+    for thesis
+    apply (insert that)
+*)
 
 local
 
 fun gen_consider prep_obtains raw_obtains int state =
   let
     val _ = Proof.assert_forward_or_chain state;
+
     val ctxt = Proof.context_of state;
-    val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
-
-    val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
+    val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
     val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
-
-    val obtain_prop =
-      Logic.list_rename_params [Auto_Bind.thesisN]
-        (Logic.all (Free thesis_var)
-          (fold_rev (fn (_, A) => fn B => Logic.mk_implies (A, B)) obtains thesis));
   in
     state
-    |> Proof.enter_forward
-    |> Proof.have NONE (K I) [] []
-      [((Binding.empty, obtains_attributes raw_obtains), [(obtain_prop, [])])] int
-    |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
-    |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
-    |> Proof.assume (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
-    |> `Proof.the_facts
-    ||> Proof.chain_facts chain_facts
-    ||> Proof.show NONE (K (Proof.local_qed (NONE, false)))
-      [] [] [(Thm.empty_binding, [(thesis, [])])] false
-    |-> Proof.refine_insert
+    |> Proof.have NONE (K I)
+      [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+      (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
+      [((Binding.empty, obtains_attributes raw_obtains), [(thesis, [])])] int
+    |> (fn state' => state'
+        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
   end;
 
 in