src/HOL/Enum.thy
 changeset 47231 3ff8c79a9e2f parent 47221 7205eb4a0a05 parent 47230 6584098d5378 child 48123 104e5fccea12
```     1.1 --- a/src/HOL/Enum.thy	Fri Mar 30 17:21:36 2012 +0200
1.2 +++ b/src/HOL/Enum.thy	Fri Mar 30 17:25:34 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))"
```