--- a/src/HOL/Analysis/Polytope.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Analysis/Polytope.thy Sat Aug 26 16:47:25 2017 +0200
@@ -2803,7 +2803,7 @@
case 1
let ?n = "of_int (floor (x/a)) + 1"
have x: "x < ?n * a"
- by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
+ by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
have "?n * a \<le> a + x"
apply (simp add: algebra_simps)
by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
@@ -2816,7 +2816,7 @@
case 2
let ?n = "of_int (floor (y/a)) + 1"
have y: "y < ?n * a"
- by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
+ by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
have "?n * a \<le> a + y"
apply (simp add: algebra_simps)
by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
--- a/src/HOL/Archimedean_Field.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Archimedean_Field.thy Sat Aug 26 16:47:25 2017 +0200
@@ -224,9 +224,8 @@
lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
using floor_correct [of x] floor_exists1 [of x] by auto
-lemma floor_unique_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
- for x :: "'a::floor_ceiling"
- using floor_correct floor_unique by auto
+lemma floor_eq_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
+using floor_correct floor_unique by auto
lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
using floor_correct ..
@@ -467,6 +466,9 @@
lemma ceiling_unique: "of_int z - 1 < x \<Longrightarrow> x \<le> of_int z \<Longrightarrow> \<lceil>x\<rceil> = z"
unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
+lemma ceiling_eq_iff: "\<lceil>x\<rceil> = a \<longleftrightarrow> of_int a - 1 < x \<and> x \<le> of_int a"
+using ceiling_correct ceiling_unique by auto
+
lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
using ceiling_correct ..
@@ -673,7 +675,7 @@
by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
moreover
have "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
- apply (simp add: floor_unique_iff)
+ apply (simp add: floor_eq_iff)
apply (auto simp add: algebra_simps)
apply linarith
done
@@ -727,7 +729,7 @@
qed
lemma round_of_int [simp]: "round (of_int n) = n"
- unfolding round_def by (subst floor_unique_iff) force
+ unfolding round_def by (subst floor_eq_iff) force
lemma round_0 [simp]: "round 0 = 0"
using round_of_int[of 0] by simp
--- a/src/HOL/Data_Structures/Balance.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Data_Structures/Balance.thy Sat Aug 26 16:47:25 2017 +0200
@@ -7,146 +7,7 @@
"HOL-Library.Tree_Real"
begin
-(* mv *)
-
-text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized
-from 2 to \<open>n\<close> and should be made executable. In the end they should be moved
-to theory \<open>Log_Nat\<close> and \<open>floorlog\<close> should be replaced.\<close>
-
-lemma floor_log_nat_ivl: fixes b n k :: nat
-assumes "b \<ge> 2" "b^n \<le> k" "k < b^(n+1)"
-shows "floor (log b (real k)) = int(n)"
-proof -
- have "k \<ge> 1"
- using assms(1,2) one_le_power[of b n] by linarith
- show ?thesis
- proof(rule floor_eq2)
- show "int n \<le> log b k"
- using assms(1,2) \<open>k \<ge> 1\<close>
- by(simp add: powr_realpow le_log_iff of_nat_power[symmetric] del: of_nat_power)
- next
- have "real k < b powr (real(n + 1))" using assms(1,3)
- by (simp only: powr_realpow) (metis of_nat_less_iff of_nat_power)
- thus "log b k < real_of_int (int n) + 1"
- using assms(1) \<open>k \<ge> 1\<close> by(simp add: log_less_iff add_ac)
- qed
-qed
-
-lemma ceil_log_nat_ivl: fixes b n k :: nat
-assumes "b \<ge> 2" "b^n < k" "k \<le> b^(n+1)"
-shows "ceiling (log b (real k)) = int(n)+1"
-proof(rule ceiling_eq)
- show "int n < log b k"
- using assms(1,2)
- by(simp add: powr_realpow less_log_iff of_nat_power[symmetric] del: of_nat_power)
-next
- have "real k \<le> b powr (real(n + 1))"
- using assms(1,3)
- by (simp only: powr_realpow) (metis of_nat_le_iff of_nat_power)
- thus "log b k \<le> real_of_int (int n) + 1"
- using assms(1,2) by(simp add: log_le_iff add_ac)
-qed
-
-lemma ceil_log2_div2: assumes "n \<ge> 2"
-shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
-proof cases
- assume "n=2"
- thus ?thesis by simp
-next
- let ?m = "(n-1) div 2 + 1"
- assume "n\<noteq>2"
- hence "2 \<le> ?m"
- using assms by arith
- then obtain i where i: "2 ^ i < ?m" "?m \<le> 2 ^ (i + 1)"
- using ex_power_ivl2[of 2 ?m] by auto
- have "n \<le> 2*?m"
- by arith
- also have "2*?m \<le> 2 ^ ((i+1)+1)"
- using i(2) by simp
- finally have *: "n \<le> \<dots>" .
- have "2^(i+1) < n"
- using i(1) by (auto simp add: less_Suc_eq_0_disj)
- from ceil_log_nat_ivl[OF _ this *] ceil_log_nat_ivl[OF _ i]
- show ?thesis by simp
-qed
-
-lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
-shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
-proof cases
- assume "n=2"
- thus ?thesis by simp
-next
- let ?m = "n div 2"
- assume "n\<noteq>2"
- hence "1 \<le> ?m"
- using assms by arith
- then obtain i where i: "2 ^ i \<le> ?m" "?m < 2 ^ (i + 1)"
- using ex_power_ivl1[of 2 ?m] by auto
- have "2^(i+1) \<le> 2*?m"
- using i(1) by simp
- also have "2*?m \<le> n"
- by arith
- finally have *: "2^(i+1) \<le> \<dots>" .
- have "n < 2^(i+1+1)"
- using i(2) by simp
- from floor_log_nat_ivl[OF _ * this] floor_log_nat_ivl[OF _ i]
- show ?thesis by simp
-qed
-
-lemma balanced_Node_if_wbal1:
-assumes "balanced l" "balanced r" "size l = size r + 1"
-shows "balanced \<langle>l, x, r\<rangle>"
-proof -
- from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def)
- have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
- by(rule nat_mono[OF ceiling_mono]) simp
- hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
- using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
- by (simp del: nat_ceiling_le_eq add: max_def)
- have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
- by(rule nat_mono[OF floor_mono]) simp
- hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
- using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
- by (simp)
- have "size1 r \<ge> 1" by(simp add: size1_def)
- then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
- using ex_power_ivl1[of 2 "size1 r"] by auto
- hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
- from 1 2 floor_log_nat_ivl[OF _ i] ceil_log_nat_ivl[OF _ i1]
- show ?thesis by(simp add:balanced_def)
-qed
-
-lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
-by(auto simp: balanced_def)
-
-lemma balanced_Node_if_wbal2:
-assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
-shows "balanced \<langle>l, x, r\<rangle>"
-proof -
- have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
- using assms(3) by linarith
- thus ?thesis
- proof
- assume "?A"
- thus ?thesis using assms(1,2)
- apply(simp add: balanced_def min_def max_def)
- by (metis assms(1,2) balanced_optimal le_antisym le_less)
- next
- assume "?B"
- thus ?thesis
- by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
- qed
-qed
-
-lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
-proof(induction t)
- case Leaf show ?case by (simp add: balanced_def)
-next
- case (Node l x r)
- thus ?case by(simp add: balanced_Node_if_wbal2)
-qed
-
-(* end of mv *)
+(* FIXME rm floor_eq_iff / rename unique \<rightarrow> eq *)
fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where
"bal n xs = (if n=0 then (Leaf,xs) else
@@ -247,7 +108,7 @@
by(simp add: balance_tree_def)
lemma min_height_bal:
- "bal n xs = (t,ys) \<Longrightarrow> min_height t = nat(floor(log 2 (n + 1)))"
+ "bal n xs = (t,ys) \<Longrightarrow> min_height t = nat(\<lfloor>log 2 (n + 1)\<rfloor>)"
proof(induction n xs arbitrary: t ys rule: bal.induct)
case (1 n xs) show ?case
proof cases
@@ -307,7 +168,7 @@
also have "\<dots> = ?log1 + 1" using le by (simp add: max_absorb1)
also have "\<dots> = nat \<lceil>log 2 (n div 2 + 1) + 1\<rceil>" using 0 by linarith
also have "\<dots> = nat \<lceil>log 2 (n + 1)\<rceil>"
- using ceil_log2_div2[of "n+1"] by (simp)
+ using ceiling_log2_div2[of "n+1"] by (simp)
finally show ?thesis .
qed
qed
@@ -327,12 +188,12 @@
by (simp add: balance_list_def height_bal_list)
corollary height_bal_tree:
- "n \<le> length xs \<Longrightarrow> height (bal_tree n t) = nat(ceiling(log 2 (n + 1)))"
+ "n \<le> length xs \<Longrightarrow> height (bal_tree n t) = nat\<lceil>log 2 (n + 1)\<rceil>"
unfolding bal_list_def bal_tree_def
using height_bal prod.exhaust_sel by blast
corollary height_balance_tree:
- "height (balance_tree t) = nat(ceiling(log 2 (size t + 1)))"
+ "height (balance_tree t) = nat\<lceil>log 2 (size t + 1)\<rceil>"
by (simp add: bal_tree_def balance_tree_def height_bal_list)
corollary balanced_bal_list[simp]: "balanced (bal_list n xs)"
--- a/src/HOL/Decision_Procs/MIR.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Sat Aug 26 16:47:25 2017 +0200
@@ -3423,7 +3423,7 @@
(((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
by (simp add: fp_def np algebra_simps)
also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
- using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
+ using floor_eq_iff[where x="?N ?nxs" and a="?l"] by simp
moreover
have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp
ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"
@@ -3449,7 +3449,7 @@
(((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
by (simp add: np fp_def algebra_simps)
also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
- using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
+ using floor_eq_iff[where x="?N ?nxs" and a="?l"] by simp
moreover
have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp
ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"
--- a/src/HOL/Library/Tree_Real.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Library/Tree_Real.thy Sat Aug 26 16:47:25 2017 +0200
@@ -61,4 +61,57 @@
show ?thesis by linarith
qed
+lemma balanced_Node_if_wbal1:
+assumes "balanced l" "balanced r" "size l = size r + 1"
+shows "balanced \<langle>l, x, r\<rangle>"
+proof -
+ from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def)
+ have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
+ by(rule nat_mono[OF ceiling_mono]) simp
+ hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
+ using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
+ by (simp del: nat_ceiling_le_eq add: max_def)
+ have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
+ by(rule nat_mono[OF floor_mono]) simp
+ hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
+ using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
+ by (simp)
+ have "size1 r \<ge> 1" by(simp add: size1_def)
+ then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
+ using ex_power_ivl1[of 2 "size1 r"] by auto
+ hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
+ from 1 2 floor_log_nat_eq_if[OF i] ceiling_log_nat_eq_if[OF i1]
+ show ?thesis by(simp add:balanced_def)
+qed
+
+lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
+by(auto simp: balanced_def)
+
+lemma balanced_Node_if_wbal2:
+assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
+shows "balanced \<langle>l, x, r\<rangle>"
+proof -
+ have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
+ using assms(3) by linarith
+ thus ?thesis
+ proof
+ assume "?A"
+ thus ?thesis using assms(1,2)
+ apply(simp add: balanced_def min_def max_def)
+ by (metis assms(1,2) balanced_optimal le_antisym le_less)
+ next
+ assume "?B"
+ thus ?thesis
+ by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
+ qed
+qed
+
+lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
+proof(induction t)
+ case Leaf show ?case by (simp add: balanced_def)
+next
+ case (Node l x r)
+ thus ?case by(simp add: balanced_Node_if_wbal2)
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Real.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Real.thy Sat Aug 26 16:47:25 2017 +0200
@@ -1495,9 +1495,6 @@
lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \<lfloor>r\<rfloor> + 1"
by linarith
-lemma floor_eq_iff: "\<lfloor>x\<rfloor> = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
- by (simp add: floor_unique_iff)
-
lemma floor_divide_real_eq_div:
assumes "0 \<le> b"
shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
--- a/src/HOL/Transcendental.thy Sat Aug 26 09:10:42 2017 +0200
+++ b/src/HOL/Transcendental.thy Sat Aug 26 16:47:25 2017 +0200
@@ -2694,7 +2694,7 @@
by auto
lemmas powr_le_iff = le_log_iff[symmetric]
- and powr_less_iff = le_log_iff[symmetric]
+ and powr_less_iff = less_log_iff[symmetric]
and less_powr_iff = log_less_iff[symmetric]
and le_powr_iff = log_le_iff[symmetric]
@@ -2739,6 +2739,80 @@
lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
+lemma floor_log_nat_eq_powr_iff: fixes b n k :: nat
+ shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
+ floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
+by (auto simp: floor_log_eq_powr_iff powr_add powr_realpow
+ of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
+ simp del: of_nat_power of_nat_mult)
+
+lemma floor_log_nat_eq_if: fixes b n k :: nat
+ assumes "b^n \<le> k" "k < b^(n+1)" "b \<ge> 2"
+ shows "floor (log b (real k)) = n"
+proof -
+ have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
+ with assms show ?thesis by(simp add: floor_log_nat_eq_powr_iff)
+qed
+
+lemma ceiling_log_eq_powr_iff: "\<lbrakk> x > 0; b > 1 \<rbrakk>
+ \<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
+by (auto simp add: ceiling_eq_iff powr_less_iff le_powr_iff)
+
+lemma ceiling_log_nat_eq_powr_iff: fixes b n k :: nat
+ shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
+ ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
+using ceiling_log_eq_powr_iff
+by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
+ simp del: of_nat_power of_nat_mult)
+
+lemma ceiling_log_nat_eq_if: fixes b n k :: nat
+ assumes "b^n < k" "k \<le> b^(n+1)" "b \<ge> 2"
+ shows "ceiling (log b (real k)) = int n + 1"
+proof -
+ have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
+ with assms show ?thesis by(simp add: ceiling_log_nat_eq_powr_iff)
+qed
+
+(* FIXME: a more appropriate place for these two lemmas
+ is a theory of discrete logarithms
+*)
+
+lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
+shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
+proof cases
+ assume "n=2" thus ?thesis by simp
+next
+ let ?m = "n div 2"
+ assume "n\<noteq>2"
+ hence "1 \<le> ?m" using assms by arith
+ then obtain i where i: "2 ^ i \<le> ?m" "?m < 2 ^ (i + 1)"
+ using ex_power_ivl1[of 2 ?m] by auto
+ have "2^(i+1) \<le> 2*?m" using i(1) by simp
+ also have "2*?m \<le> n" by arith
+ finally have *: "2^(i+1) \<le> \<dots>" .
+ have "n < 2^(i+1+1)" using i(2) by simp
+ from floor_log_nat_eq_if[OF * this] floor_log_nat_eq_if[OF i]
+ show ?thesis by simp
+qed
+
+lemma ceiling_log2_div2: assumes "n \<ge> 2"
+shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
+proof cases
+ assume "n=2" thus ?thesis by simp
+next
+ let ?m = "(n-1) div 2 + 1"
+ assume "n\<noteq>2"
+ hence "2 \<le> ?m" using assms by arith
+ then obtain i where i: "2 ^ i < ?m" "?m \<le> 2 ^ (i + 1)"
+ using ex_power_ivl2[of 2 ?m] by auto
+ have "n \<le> 2*?m" by arith
+ also have "2*?m \<le> 2 ^ ((i+1)+1)" using i(2) by simp
+ finally have *: "n \<le> \<dots>" .
+ have "2^(i+1) < n" using i(1) by (auto simp add: less_Suc_eq_0_disj)
+ from ceiling_log_nat_eq_if[OF this *] ceiling_log_nat_eq_if[OF i]
+ show ?thesis by simp
+qed
+
lemma powr_real_of_int:
"x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]