tuned proofs, less guesswork;
authorwenzelm
Fri Mar 30 17:22:17 2012 +0200 (2012-03-30)
changeset 472306584098d5378
parent 47215 ca516aa5b6ce
child 47231 3ff8c79a9e2f
tuned proofs, less guesswork;
src/HOL/Enum.thy
src/HOL/Library/Float.thy
src/HOL/Quickcheck_Examples/Completeness.thy
     1.1 --- a/src/HOL/Enum.thy	Fri Mar 30 15:25:47 2012 +0200
     1.2 +++ b/src/HOL/Enum.thy	Fri Mar 30 17:22:17 2012 +0200
     1.3 @@ -152,7 +152,8 @@
     1.4      from length map_of_zip_enum_is_Some obtain y1 y2
     1.5        where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
     1.6          and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
     1.7 -    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)"
     1.8 +    moreover from map_of
     1.9 +      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)"
    1.10        by (auto dest: fun_cong)
    1.11      ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
    1.12        by simp
    1.13 @@ -832,7 +833,7 @@
    1.14        by (rule finite_imageD)
    1.15      then show False by simp
    1.16    qed
    1.17 -  then guess n .. note n = this
    1.18 +  then obtain n where n: "f n = f (Suc n)" ..
    1.19    def N \<equiv> "LEAST n. f n = f (Suc n)"
    1.20    have N: "f N = f (Suc N)"
    1.21      unfolding N_def using n by (rule LeastI)
    1.22 @@ -921,13 +922,13 @@
    1.23  proof
    1.24    fix x
    1.25    assume "x : acc r"
    1.26 -  from this have "\<exists> n. x : bacc r n"
    1.27 -  proof (induct x arbitrary: n rule: acc.induct)
    1.28 +  then have "\<exists> n. x : bacc r n"
    1.29 +  proof (induct x arbitrary: rule: acc.induct)
    1.30      case (accI x)
    1.31 -    from accI have "\<forall> y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
    1.32 -    from choice[OF this] guess n .. note n = this
    1.33 -    have "\<exists> n. \<forall>y. (y, x) : r --> y : bacc r n"
    1.34 -    proof (safe intro!: exI[of _ "Max ((%(y,x). n y)`r)"])
    1.35 +    then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
    1.36 +    from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
    1.37 +    obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
    1.38 +    proof
    1.39        fix y assume y: "(y, x) : r"
    1.40        with n have "y : bacc r (n y)" by auto
    1.41        moreover have "n y <= Max ((%(y, x). n y) ` r)"
    1.42 @@ -935,11 +936,10 @@
    1.43        note bacc_mono[OF this, of r]
    1.44        ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
    1.45      qed
    1.46 -    from this guess n ..
    1.47 -    from this show ?case
    1.48 +    then show ?case
    1.49        by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
    1.50    qed
    1.51 -  thus "x : (UN n. bacc r n)" by auto
    1.52 +  then show "x : (UN n. bacc r n)" by auto
    1.53  qed
    1.54  
    1.55  lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
     2.1 --- a/src/HOL/Library/Float.thy	Fri Mar 30 15:25:47 2012 +0200
     2.2 +++ b/src/HOL/Library/Float.thy	Fri Mar 30 17:22:17 2012 +0200
     2.3 @@ -165,9 +165,8 @@
     2.4  
     2.5    {
     2.6      assume bcmp: "b > b'"
     2.7 -    then have "\<exists>c::nat. b - b' = int c + 1"
     2.8 -      by arith
     2.9 -    then guess c ..
    2.10 +    then obtain c :: nat where "b - b' = int c + 1"
    2.11 +      by atomize_elim arith
    2.12      with a' have "real a' = real (a * 2^c * 2)"
    2.13        by (simp add: pow2_def nat_add_distrib)
    2.14      with odd have False
     3.1 --- a/src/HOL/Quickcheck_Examples/Completeness.thy	Fri Mar 30 15:25:47 2012 +0200
     3.2 +++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Fri Mar 30 17:22:17 2012 +0200
     3.3 @@ -173,7 +173,7 @@
     3.4      show ?case
     3.5      proof
     3.6        assume "\<exists>v. Completeness.size_class.size v \<le> Suc n \<and> is_some (f v)"
     3.7 -      from this guess v .. note v = this
     3.8 +      then obtain v where v: "size v \<le> Suc n" "is_some (f v)" by blast
     3.9        show "is_some (exhaustive_class.exhaustive f (Code_Numeral.of_nat (Suc n)))"
    3.10        proof (cases "v")
    3.11        case Nil
    3.12 @@ -196,20 +196,23 @@
    3.13        show "\<exists>v. size v \<le> Suc n \<and> is_some (f v)"
    3.14        proof (cases "f []")
    3.15          case Some
    3.16 -        from this show ?thesis
    3.17 +        then show ?thesis
    3.18          by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1))
    3.19        next
    3.20          case None
    3.21 -        from this is_some have
    3.22 +        with is_some have
    3.23            "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))"
    3.24            unfolding list.exhaustive_list.simps[of _ "Code_Numeral.of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def
    3.25            by simp
    3.26 -        from complete_imp2[OF this] guess v' . note v = this
    3.27 -        from Suc[of "%xs. f (v' # xs)"] this(2) obtain vs' where "size vs' \<le> n" "is_some (f (v' # vs'))"
    3.28 +        then obtain v' where
    3.29 +            v: "size v' \<le> n"
    3.30 +              "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (Code_Numeral.of_nat n))"
    3.31 +          by (rule complete_imp2)
    3.32 +        with Suc[of "%xs. f (v' # xs)"]
    3.33 +        obtain vs' where vs': "size vs' \<le> n" "is_some (f (v' # vs'))"
    3.34            by metis
    3.35 -        note vs' = this
    3.36 -        from this v have "size (v' # vs') \<le> Suc n" by auto
    3.37 -        from this vs' v show ?thesis by metis
    3.38 +        with v have "size (v' # vs') \<le> Suc n" by auto
    3.39 +        with vs' v show ?thesis by metis
    3.40        qed
    3.41      qed
    3.42    qed