summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 30 Mar 2012 17:22:17 +0200 | |

changeset 47230 | 6584098d5378 |

parent 47215 | ca516aa5b6ce |

child 47231 | 3ff8c79a9e2f |

tuned proofs, less guesswork;

--- 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