1.1 --- a/src/HOL/Library/Formal_Power_Series.thy Tue Nov 05 09:45:00 2013 +0100
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -451,7 +451,7 @@
1.4
1.5 definition
1.6 dist_fps_def: "dist (a::'a fps) b =
1.7 - (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
1.8 + (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
1.9
1.10 lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
1.11 by (simp add: dist_fps_def)
1.12 @@ -467,34 +467,6 @@
1.13
1.14 end
1.15
1.16 -lemma fps_nonzero_least_unique:
1.17 - assumes a0: "a \<noteq> 0"
1.18 - shows "\<exists>!n. leastP (\<lambda>n. a$n \<noteq> 0) n"
1.19 -proof -
1.20 - from fps_nonzero_nth_minimal [of a] a0
1.21 - obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast
1.22 - then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n"
1.23 - by (auto simp add: leastP_def setge_def not_le [symmetric])
1.24 - moreover
1.25 - {
1.26 - fix m
1.27 - assume "leastP (\<lambda>n. a $ n \<noteq> 0) m"
1.28 - then have "m = n" using ln
1.29 - apply (auto simp add: leastP_def setge_def)
1.30 - apply (erule allE[where x=n])
1.31 - apply (erule allE[where x=m])
1.32 - apply simp
1.33 - done
1.34 - }
1.35 - ultimately show ?thesis by blast
1.36 -qed
1.37 -
1.38 -lemma fps_eq_least_unique:
1.39 - assumes "(a::('a::ab_group_add) fps) \<noteq> b"
1.40 - shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
1.41 - using fps_nonzero_least_unique[of "a - b"] assms
1.42 - by auto
1.43 -
1.44 instantiation fps :: (comm_ring_1) metric_space
1.45 begin
1.46
1.47 @@ -540,31 +512,15 @@
1.48 moreover
1.49 {
1.50 assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
1.51 - let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
1.52 - from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac]
1.53 - fps_eq_least_unique[OF bc]
1.54 - obtain nab nac nbc where nab: "leastP (?P a b) nab"
1.55 - and nac: "leastP (?P a c) nac"
1.56 - and nbc: "leastP (?P b c) nbc" by blast
1.57 - from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab"
1.58 - by (auto simp add: leastP_def setge_def)
1.59 - from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac"
1.60 - by (auto simp add: leastP_def setge_def)
1.61 - from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc"
1.62 - by (auto simp add: leastP_def setge_def)
1.63 -
1.64 - have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
1.65 - by (simp add: fps_eq_iff)
1.66 - from ab ac bc nab nac nbc
1.67 - have dab: "dist a b = inverse (2 ^ nab)"
1.68 - and dac: "dist a c = inverse (2 ^ nac)"
1.69 - and dbc: "dist b c = inverse (2 ^ nbc)"
1.70 - unfolding th0
1.71 - apply (simp_all add: dist_fps_def)
1.72 - apply (erule the1_equality[OF fps_eq_least_unique[OF ab]])
1.73 - apply (erule the1_equality[OF fps_eq_least_unique[OF ac]])
1.74 - apply (erule the1_equality[OF fps_eq_least_unique[OF bc]])
1.75 - done
1.76 + def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n"
1.77 + then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m"
1.78 + by (auto dest: not_less_Least)
1.79 +
1.80 + from ab ac bc
1.81 + have dab: "dist a b = inverse (2 ^ n a b)"
1.82 + and dac: "dist a c = inverse (2 ^ n a c)"
1.83 + and dbc: "dist b c = inverse (2 ^ n b c)"
1.84 + by (simp_all add: dist_fps_def n_def fps_eq_iff)
1.85 from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
1.86 unfolding th by simp_all
1.87 from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0"
1.88 @@ -575,11 +531,13 @@
1.89 assume h: "dist a b > dist a c + dist b c"
1.90 then have gt: "dist a b > dist a c" "dist a b > dist b c"
1.91 using pos by auto
1.92 - from gt have gtn: "nab < nbc" "nab < nac"
1.93 + from gt have gtn: "n a b < n b c" "n a b < n a c"
1.94 unfolding dab dbc dac by (auto simp add: th1)
1.95 - from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)]
1.96 - have "a $ nab = b $ nab" by simp
1.97 - with nab'(2) have False by simp
1.98 + from n'[OF gtn(2)] n'(1)[OF gtn(1)]
1.99 + have "a $ n a b = b $ n a b" by simp
1.100 + moreover have "a $ n a b \<noteq> b $ n a b"
1.101 + unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff)
1.102 + ultimately have False by contradiction
1.103 }
1.104 then have "dist a b \<le> dist a c + dist b c"
1.105 by (auto simp add: not_le[symmetric])
1.106 @@ -649,17 +607,12 @@
1.107 moreover
1.108 {
1.109 assume neq: "?s n \<noteq> a"
1.110 - from fps_eq_least_unique[OF neq]
1.111 - obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast
1.112 - have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
1.113 - by (simp add: fps_eq_iff)
1.114 + def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i"
1.115 from neq have dth: "dist (?s n) a = (1/2)^k"
1.116 - unfolding th0 dist_fps_def
1.117 - unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k]
1.118 - by (auto simp add: inverse_eq_divide power_divide)
1.119 -
1.120 - from k have kn: "k > n"
1.121 - by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
1.122 + by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
1.123 +
1.124 + from neq have kn: "k > n"
1.125 + by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
1.126 then have "dist (?s n) a < (1/2)^n" unfolding dth
1.127 by (auto intro: power_strict_decreasing)
1.128 also have "\<dots> <= (1/2)^n0" using nn0
1.129 @@ -3797,20 +3750,14 @@
1.130 assumes "dist f g < inverse (2 ^ i)"
1.131 and"j \<le> i"
1.132 shows "f $ j = g $ j"
1.133 -proof (cases "f = g")
1.134 - case False
1.135 - hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
1.136 - with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
1.137 +proof (rule ccontr)
1.138 + assume "f $ j \<noteq> g $ j"
1.139 + then have "\<exists>n. f $ n \<noteq> g $ n" by auto
1.140 + with assms have "i < (LEAST n. f $ n \<noteq> g $ n)"
1.141 by (simp add: split_if_asm dist_fps_def)
1.142 - moreover
1.143 - from fps_eq_least_unique[OF `f \<noteq> g`]
1.144 - obtain n where n: "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
1.145 - moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
1.146 - by (auto simp add: leastP_def setge_def)
1.147 - ultimately show ?thesis using `j \<le> i` by simp
1.148 -next
1.149 - case True
1.150 - then show ?thesis by simp
1.151 + also have "\<dots> \<le> j"
1.152 + using `f $ j \<noteq> g $ j` by (auto intro: Least_le)
1.153 + finally show False using `j \<le> i` by simp
1.154 qed
1.155
1.156 lemma nth_equal_imp_dist_less:
1.157 @@ -3819,18 +3766,13 @@
1.158 proof (cases "f = g")
1.159 case False
1.160 hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
1.161 - with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
1.162 + with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))"
1.163 by (simp add: split_if_asm dist_fps_def)
1.164 moreover
1.165 - from fps_eq_least_unique[OF `f \<noteq> g`]
1.166 - obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
1.167 - with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
1.168 - by (metis (full_types) leastPD1 not_le)
1.169 + from assms `\<exists>n. f $ n \<noteq> g $ n` have "i < (LEAST n. f $ n \<noteq> g $ n)"
1.170 + by (metis (mono_tags) LeastI not_less)
1.171 ultimately show ?thesis by simp
1.172 -next
1.173 - case True
1.174 - then show ?thesis by simp
1.175 -qed
1.176 +qed simp
1.177
1.178 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
1.179 using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast