--- a/src/HOL/Enum.thy Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Enum.thy Fri Mar 30 17:22:17 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))"
--- a/src/HOL/Library/Float.thy Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Library/Float.thy Fri Mar 30 17:22:17 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
--- a/src/HOL/Quickcheck_Examples/Completeness.thy Fri Mar 30 15:25:47 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy Fri Mar 30 17:22:17 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