# HG changeset patch
# User nipkow
# Date 1470411398 -7200
# Node ID 7725bba95adafbbbcd5852f4559babd73a16d878
# Parent  aca2659ebba79c21a255f0336878120247d81d2a# Parent  ae810a755cd2793cb4f70c69ff863daa5aa13b37
merged

diff -r aca2659ebba7 -r 7725bba95ada src/HOL/Archimedean_Field.thy
--- 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)
diff -r aca2659ebba7 -r 7725bba95ada src/HOL/Decision_Procs/MIR.thy
--- 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
diff -r aca2659ebba7 -r 7725bba95ada src/HOL/Library/Float.thy
--- 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]
diff -r aca2659ebba7 -r 7725bba95ada src/HOL/Library/Tree.thy
--- 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
 
diff -r aca2659ebba7 -r 7725bba95ada src/HOL/Real.thy
--- 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