# HG changeset patch
# User wenzelm
# Date 1333121134 -7200
# Node ID 3ff8c79a9e2f15033d78e242aea1e554bc4f0849
# Parent  ba37aaead15556d7f4424ec3bff09b22d5e96e45# Parent  6584098d5378c4acadb740fde74b4db641fb6728
merged

diff -r ba37aaead155 -r 3ff8c79a9e2f src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Fri Mar 30 17:21:36 2012 +0200
+++ b/src/HOL/Enum.thy	Fri Mar 30 17:25:34 2012 +0200
@@ -152,7 +152,8 @@
     from length map_of_zip_enum_is_Some obtain y1 y2
       where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
         and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
-    moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
+    moreover from map_of
+      have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
       by (auto dest: fun_cong)
     ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
       by simp
@@ -832,7 +833,7 @@
       by (rule finite_imageD)
     then show False by simp
   qed
-  then guess n .. note n = this
+  then obtain n where n: "f n = f (Suc n)" ..
   def N \<equiv> "LEAST n. f n = f (Suc n)"
   have N: "f N = f (Suc N)"
     unfolding N_def using n by (rule LeastI)
@@ -921,13 +922,13 @@
 proof
   fix x
   assume "x : acc r"
-  from this have "\<exists> n. x : bacc r n"
-  proof (induct x arbitrary: n rule: acc.induct)
+  then have "\<exists> n. x : bacc r n"
+  proof (induct x arbitrary: rule: acc.induct)
     case (accI x)
-    from accI have "\<forall> y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
-    from choice[OF this] guess n .. note n = this
-    have "\<exists> n. \<forall>y. (y, x) : r --> y : bacc r n"
-    proof (safe intro!: exI[of _ "Max ((%(y,x). n y)`r)"])
+    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
+    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
+    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
+    proof
       fix y assume y: "(y, x) : r"
       with n have "y : bacc r (n y)" by auto
       moreover have "n y <= Max ((%(y, x). n y) ` r)"
@@ -935,11 +936,10 @@
       note bacc_mono[OF this, of r]
       ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
     qed
-    from this guess n ..
-    from this show ?case
+    then show ?case
       by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
   qed
-  thus "x : (UN n. bacc r n)" by auto
+  then show "x : (UN n. bacc r n)" by auto
 qed
 
 lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
diff -r ba37aaead155 -r 3ff8c79a9e2f src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Mar 30 17:21:36 2012 +0200
+++ b/src/HOL/Library/Float.thy	Fri Mar 30 17:25:34 2012 +0200
@@ -165,9 +165,8 @@
 
   {
     assume bcmp: "b > b'"
-    then have "\<exists>c::nat. b - b' = int c + 1"
-      by arith
-    then guess c ..
+    then obtain c :: nat where "b - b' = int c + 1"
+      by atomize_elim arith
     with a' have "real a' = real (a * 2^c * 2)"
       by (simp add: pow2_def nat_add_distrib)
     with odd have False
diff -r ba37aaead155 -r 3ff8c79a9e2f src/HOL/Quickcheck_Examples/Completeness.thy
--- a/src/HOL/Quickcheck_Examples/Completeness.thy	Fri Mar 30 17:21:36 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Fri Mar 30 17:25:34 2012 +0200
@@ -173,7 +173,7 @@
     show ?case
     proof
       assume "\<exists>v. Completeness.size_class.size v \<le> Suc n \<and> is_some (f v)"
-      from this guess v .. note v = this
+      then obtain v where v: "size v \<le> Suc n" "is_some (f v)" by blast
       show "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))"
       proof (cases "v")
       case Nil
@@ -196,20 +196,23 @@
       show "\<exists>v. size v \<le> Suc n \<and> is_some (f v)"
       proof (cases "f []")
         case Some
-        from this show ?thesis
+        then show ?thesis
         by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1))
       next
         case None
-        from this is_some have
+        with is_some have
           "is_some (exhaustive_class.exhaustive (\<lambda>x. exhaustive_class.exhaustive (\<lambda>xs. f (x # xs)) (Code_Numeral.of_nat n)) (Code_Numeral.of_nat n))"
           unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def
           by simp
-        from complete_imp2[OF this] guess v' . note v = this
-        from Suc[of "%xs. f (v' # xs)"] this(2) obtain vs' where "size vs' \<le> n" "is_some (f (v' # vs'))"
+        then obtain v' where
+            v: "size v' \<le> n"
+              "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (Code_Numeral.of_nat n))"
+          by (rule complete_imp2)
+        with Suc[of "%xs. f (v' # xs)"]
+        obtain vs' where vs': "size vs' \<le> n" "is_some (f (v' # vs'))"
           by metis
-        note vs' = this
-        from this v have "size (v' # vs') \<le> Suc n" by auto
-        from this vs' v show ?thesis by metis
+        with v have "size (v' # vs') \<le> Suc n" by auto
+        with vs' v show ?thesis by metis
       qed
     qed
   qed