--- a/src/HOL/Archimedean_Field.thy Fri Aug 05 14:00:02 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy Fri Aug 05 17:36:38 2016 +0200
@@ -342,17 +342,17 @@
text \<open>Addition and subtraction of integers.\<close>
-lemma floor_add_of_int [simp]: "\<lfloor>x + of_int z\<rfloor> = \<lfloor>x\<rfloor> + z"
- using floor_correct [of x] by (simp add: floor_unique)
+lemma floor_add_int: "\<lfloor>x\<rfloor> + z = \<lfloor>x + of_int z\<rfloor>"
+ using floor_correct [of x] by (simp add: floor_unique[symmetric])
-lemma floor_add_numeral [simp]: "\<lfloor>x + numeral v\<rfloor> = \<lfloor>x\<rfloor> + numeral v"
- using floor_add_of_int [of x "numeral v"] by simp
+lemma int_add_floor: "z + \<lfloor>x\<rfloor> = \<lfloor>of_int z + x\<rfloor>"
+ using floor_correct [of x] by (simp add: floor_unique[symmetric])
-lemma floor_add_one [simp]: "\<lfloor>x + 1\<rfloor> = \<lfloor>x\<rfloor> + 1"
- using floor_add_of_int [of x 1] by simp
+lemma one_add_floor: "\<lfloor>x\<rfloor> + 1 = \<lfloor>x + 1\<rfloor>"
+ using floor_add_int [of x 1] by simp
lemma floor_diff_of_int [simp]: "\<lfloor>x - of_int z\<rfloor> = \<lfloor>x\<rfloor> - z"
- using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
+ using floor_add_int [of x "- z"] by (simp add: algebra_simps)
lemma floor_uminus_of_int [simp]: "\<lfloor>- (of_int z)\<rfloor> = - z"
by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
@@ -414,7 +414,7 @@
then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
by (simp add: ac_simps)
then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + k div l"
- by simp
+ by (simp add: floor_add_int)
with * show ?thesis
by simp
qed
@@ -444,7 +444,7 @@
by simp
ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> =
\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
- by (simp only: floor_add_of_int)
+ by (simp only: floor_add_int)
with * show ?thesis
by simp
qed
@@ -629,19 +629,20 @@
lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
proof -
- have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>" if "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
- using that by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
+ have "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
+ by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
moreover
- have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)" if "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
- using that
+ 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 (auto simp add: algebra_simps)
apply linarith
done
- ultimately show ?thesis
- by (auto simp add: frac_def algebra_simps)
+ ultimately show ?thesis by (auto simp add: frac_def algebra_simps)
qed
+lemma floor_add2[simp]: "frac x = 0 \<or> frac y = 0 \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
+by (metis add.commute add.left_neutral frac_lt_1 floor_add)
+
lemma frac_add:
"frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)"
by (simp add: frac_def floor_add)
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 05 14:00:02 2016 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 05 17:36:38 2016 +0200
@@ -1526,7 +1526,7 @@
also have "\<dots> = real_of_int \<lfloor>real_of_int ?nt * real_of_int x + ?I x ?at\<rfloor>" by simp
also have "\<dots> = real_of_int \<lfloor>?I x ?at + real_of_int (?nt * x)\<rfloor>" by (simp add: ac_simps)
also have "\<dots> = real_of_int (\<lfloor>?I x ?at\<rfloor> + (?nt * x))"
- using floor_add_of_int[of "?I x ?at" "?nt * x"] by simp
+ by (simp add: of_int_mult[symmetric] del: of_int_mult)
also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int \<lfloor>?I x ?at\<rfloor>" by (simp add: ac_simps)
finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
with na show ?case by simp
--- a/src/HOL/Library/Float.thy Fri Aug 05 14:00:02 2016 +0200
+++ b/src/HOL/Library/Float.thy Fri Aug 05 17:36:38 2016 +0200
@@ -881,19 +881,8 @@
definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where "floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
-lemma floorlog_nonneg: "0 \<le> floorlog b x"
-proof -
- have "-1 < log b (-x)" if "0 > x" "b > 1"
- proof -
- have "-1 = log b (inverse b)" using that
- by (subst log_inverse) simp_all
- also have "\<dots> < log b (-x)"
- using \<open>0 > x\<close> by auto
- finally show ?thesis .
- qed
- then show ?thesis
- unfolding floorlog_def by (auto intro!: add_nonneg_nonneg)
-qed
+lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y"
+by(auto simp: floorlog_def floor_mono nat_mono)
lemma floorlog_bounds:
assumes "x > 0" "b > 1"
@@ -944,11 +933,9 @@
by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
qed
-lemma
- floor_log_add_eqI:
+lemma floor_log_add_eqI:
fixes a::nat and b::nat and r::real
- assumes "b > 1"
- assumes "a \<ge> 1" "0 \<le> r" "r < 1"
+ assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>"
proof (rule floor_eq2)
have "log (real b) (real a) \<le> log (real b) (real a + r)"
@@ -977,37 +964,56 @@
finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" .
qed
-lemma
- divide_nat_diff_div_nat_less_one:
+lemma divide_nat_diff_div_nat_less_one:
fixes x b::nat shows "x / b - x div b < 1"
- by (metis One_nat_def add_diff_cancel_left' divide_1 divide_self_if floor_divide_of_nat_eq
- less_eq_real_def mod_div_trivial nat.simps(3) of_nat_eq_0_iff real_of_nat_div3 real_of_nat_div_aux)
-
-context
-begin
-
-qualified lemma compute_floorlog[code]:
- "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
proof -
- {
- assume prems: "x > 0" "b > 1" "0 < x div b"
- have "\<lfloor>log (real b) (real x)\<rfloor> = \<lfloor>log (real b) (x / b * b)\<rfloor>"
- using prems by simp
- also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
- using prems
- by (subst log_mult) auto
- also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using prems by simp
- also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>"
- by simp
- also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
- using prems real_of_nat_div4 divide_nat_diff_div_nat_less_one
- by (intro floor_log_add_eqI) auto
- finally have ?thesis using prems by (simp add: floorlog_def nat_add_distrib)
- } then show ?thesis
- by (auto simp: floorlog_def div_eq_0_iff intro!: floor_eq2)
+ have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp
+ thus ?thesis
+ by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
+ mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
qed
-end
+lemma floor_log_div:
+ fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
+ shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1"
+proof-
+ have "\<lfloor>log (real b) (real x)\<rfloor> = \<lfloor>log (real b) (x / b * b)\<rfloor>"
+ using assms by simp
+ also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
+ using assms by (subst log_mult) auto
+ also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp
+ also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>"
+ by simp
+ also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
+ using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
+ by (intro floor_log_add_eqI) auto
+ finally show ?thesis .
+qed
+
+lemma compute_floorlog[code]:
+ "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
+by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
+ intro!: floor_eq2)
+
+lemma floor_log_eq_if:
+ fixes b x y :: nat
+ assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
+ shows "floor(log b x) = floor(log b y)"
+proof -
+ have "y > 0" using assms by(auto intro: ccontr)
+ thus ?thesis using assms by (simp add: floor_log_div)
+qed
+
+lemma floorlog_eq_if:
+ fixes b x y :: nat
+ assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
+ shows "floorlog b x = floorlog b y"
+proof -
+ have "y > 0" using assms by(auto intro: ccontr)
+ thus ?thesis using assms
+ by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
+qed
+
definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
@@ -1015,7 +1021,7 @@
by (simp add: bitlen_def floorlog_def)
lemma bitlen_nonneg: "0 \<le> bitlen x"
- using floorlog_nonneg by (simp add: bitlen_def)
+by (simp add: bitlen_def)
lemma bitlen_bounds:
assumes "x > 0"
@@ -1419,8 +1425,8 @@
by (simp add: log_mult)
then have "bitlen (int x) < bitlen (int y)"
using assms
- by (simp add: bitlen_alt_def del: floor_add_one)
- (auto intro!: floor_mono simp add: floor_add_one[symmetric] simp del: floor_add floor_add_one)
+ by (simp add: bitlen_alt_def)
+ (auto intro!: floor_mono simp add: one_add_floor)
then show ?thesis
using assms
by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
@@ -1806,9 +1812,9 @@
have "\<dots> = \<lfloor>log 2 (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k)\<rfloor>"
by (subst floor_eq) (auto simp: sgn_if)
also have "k + \<dots> = \<lfloor>log 2 (2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k))\<rfloor>"
- unfolding floor_add2[symmetric]
+ unfolding int_add_floor
using pos[OF less'] \<open>\<bar>b\<bar> \<le> _\<close>
- by (simp add: field_simps add_log_eq_powr)
+ by (simp add: field_simps add_log_eq_powr del: floor_add2)
also have "2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k) =
2 powr k + r + sgn (sgn ai * b) / 2"
by (simp add: sgn_if field_simps)
@@ -1893,8 +1899,8 @@
by (auto simp: field_simps powr_minus[symmetric] powr_divide2[symmetric] powr_mult_base)
then have "\<lfloor>log 2 \<bar>?m1 + ?m2'\<bar>\<rfloor> + ?e = \<lfloor>log 2 \<bar>real_of_float (Float (?m1 * 2 + sgn m2) (?e - 1))\<bar>\<rfloor>"
using \<open>?m1 + ?m2' \<noteq> 0\<close>
- unfolding floor_add_of_int[symmetric]
- by (simp add: log_add_eq_powr abs_mult_pos)
+ unfolding floor_add_int
+ by (simp add: log_add_eq_powr abs_mult_pos del: floor_add2)
finally
have "\<lfloor>log 2 \<bar>?sum\<bar>\<rfloor> = \<lfloor>log 2 \<bar>real_of_float (Float (?m1*2 + sgn m2) (?e - 1))\<bar>\<rfloor>" .
then have "plus_down p (Float m1 e1) (Float m2 e2) =
@@ -1913,7 +1919,7 @@
next
have "e1 + \<lfloor>log 2 \<bar>real_of_int m1\<bar>\<rfloor> - 1 = \<lfloor>log 2 \<bar>?a\<bar>\<rfloor> - 1"
using \<open>m1 \<noteq> 0\<close>
- by (simp add: floor_add2[symmetric] algebra_simps log_mult abs_mult del: floor_add2)
+ by (simp add: int_add_floor algebra_simps log_mult abs_mult del: floor_add2)
also have "\<dots> \<le> \<lfloor>log 2 \<bar>?a + ?b\<bar>\<rfloor>"
using a_half_less_sum \<open>m1 \<noteq> 0\<close> \<open>?sum \<noteq> 0\<close>
unfolding floor_diff_of_int[symmetric]
--- a/src/HOL/Library/Tree.thy Fri Aug 05 14:00:02 2016 +0200
+++ b/src/HOL/Library/Tree.thy Fri Aug 05 17:36:38 2016 +0200
@@ -83,12 +83,38 @@
qed simp
+fun min_height :: "'a tree \<Rightarrow> nat" where
+"min_height Leaf = 0" |
+"min_height (Node l _ r) = min (min_height l) (min_height r) + 1"
+
+lemma min_hight_le_height: "min_height t \<le> height t"
+by(induction t) auto
+
+lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t"
+by (induction t) auto
+
+lemma min_height_le_size1: "2 ^ min_height t \<le> size t + 1"
+proof(induction t)
+ case (Node l a r)
+ have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r"
+ by (simp add: min_def)
+ also have "\<dots> \<le> size(Node l a r) + 1" using Node.IH by simp
+ finally show ?case .
+qed simp
+
+
subsection "Balanced"
fun balanced :: "'a tree \<Rightarrow> bool" where
"balanced Leaf = True" |
"balanced (Node l x r) = (balanced l \<and> balanced r \<and> height l = height r)"
+lemma balanced_iff_min_height: "balanced t \<longleftrightarrow> (min_height t = height t)"
+apply(induction t)
+ apply simp
+apply (simp add: min_def max_def)
+by (metis le_antisym le_trans min_hight_le_height)
+
lemma balanced_size1: "balanced t \<Longrightarrow> size1 t = 2 ^ height t"
by (induction t) auto
--- a/src/HOL/Real.thy Fri Aug 05 14:00:02 2016 +0200
+++ b/src/HOL/Real.thy Fri Aug 05 17:36:38 2016 +0200
@@ -1503,9 +1503,6 @@
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_add2[simp]: "\<lfloor>of_int a + x\<rfloor> = a + \<lfloor>x\<rfloor>"
- by (simp add: add.commute)
-
lemma floor_divide_real_eq_div:
assumes "0 \<le> b"
shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
@@ -1526,27 +1523,34 @@
proof -
have "real_of_int (j * b) < real_of_int i + 1"
using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force
- then show "j * b < 1 + i"
- by linarith
+ then show "j * b < 1 + i" by linarith
qed
ultimately have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b"
by (auto simp: field_simps)
then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b"
using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i]
by linarith+
- then show ?thesis
- using b unfolding mult_less_cancel_right by auto
+ then show ?thesis using b unfolding mult_less_cancel_right by auto
qed
- with b show ?thesis
- by (auto split: floor_split simp: field_simps)
+ with b show ?thesis by (auto split: floor_split simp: field_simps)
qed
-lemma floor_divide_eq_div_numeral [simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
- by (metis floor_divide_of_int_eq of_int_numeral)
+lemma floor_one_divide_eq_div_numeral [simp]:
+ "\<lfloor>1 / numeral b::real\<rfloor> = 1 div numeral b"
+by (metis floor_divide_of_int_eq of_int_1 of_int_numeral)
+
+lemma floor_minus_one_divide_eq_div_numeral [simp]:
+ "\<lfloor>- (1 / numeral b)::real\<rfloor> = - 1 div numeral b"
+by (metis (mono_tags, hide_lams) div_minus_right minus_divide_right
+ floor_divide_of_int_eq of_int_neg_numeral of_int_1)
+
+lemma floor_divide_eq_div_numeral [simp]:
+ "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
+by (metis floor_divide_of_int_eq of_int_numeral)
lemma floor_minus_divide_eq_div_numeral [simp]:
"\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
- by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
+by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
lemma of_int_ceiling_cancel [simp]: "of_int \<lceil>x\<rceil> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
using ceiling_of_int by metis