# HG changeset patch
# User wenzelm
# Date 1420980265 -3600
# Node ID 3bde948f439cdc5d4181f3cfdc5d33005c8a3705
# Parent  8a6788917b323fa09a428086f32d925e489cb159
tuned -- more Sidekick-friendly layout;

diff -r 8a6788917b32 -r 3bde948f439c src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Sun Jan 11 13:12:47 2015 +0100
+++ b/src/HOL/Library/Discrete.thy	Sun Jan 11 13:44:25 2015 +0100
@@ -1,4 +1,4 @@
-(* Author: Florian Haftmann, TU Muenchen *)  
+(* Author: Florian Haftmann, TU Muenchen *)
 
 section {* Common discrete functions *}
 
@@ -8,45 +8,38 @@
 
 subsection {* Discrete logarithm *}
 
-fun log :: "nat \<Rightarrow> nat" where
-  [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
+fun log :: "nat \<Rightarrow> nat"
+  where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
 
-lemma log_zero [simp]:
-  "log 0 = 0"
+lemma log_zero [simp]: "log 0 = 0"
   by (simp add: log.simps)
 
-lemma log_one [simp]:
-  "log 1 = 0"
+lemma log_one [simp]: "log 1 = 0"
   by (simp add: log.simps)
 
-lemma log_Suc_zero [simp]:
-  "log (Suc 0) = 0"
+lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
   using log_one by simp
 
-lemma log_rec:
-  "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
+lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
   by (simp add: log.simps)
 
-lemma log_twice [simp]:
-  "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
+lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
   by (simp add: log_rec)
 
-lemma log_half [simp]:
-  "log (n div 2) = log n - 1"
+lemma log_half [simp]: "log (n div 2) = log n - 1"
 proof (cases "n < 2")
   case True
   then have "n = 0 \<or> n = 1" by arith
   then show ?thesis by (auto simp del: One_nat_def)
 next
-  case False then show ?thesis by (simp add: log_rec)
+  case False
+  then show ?thesis by (simp add: log_rec)
 qed
 
-lemma log_exp [simp]:
-  "log (2 ^ n) = n"
+lemma log_exp [simp]: "log (2 ^ n) = n"
   by (induct n) simp_all
 
-lemma log_mono:
-  "mono log"
+lemma log_mono: "mono log"
 proof
   fix m n :: nat
   assume "m \<le> n"
@@ -75,8 +68,7 @@
 subsection {* Discrete square root *}
 
 definition sqrt :: "nat \<Rightarrow> nat"
-where
-  "sqrt n = Max {m. m\<^sup>2 \<le> n}"
+  where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
 
 lemma sqrt_aux:
   fixes n :: nat
@@ -93,15 +85,13 @@
   then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
 qed
 
-lemma [code]:
-  "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
+lemma [code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
 proof -
   from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
   then show ?thesis by (simp add: sqrt_def Set.filter_def)
 qed
 
-lemma sqrt_inverse_power2 [simp]:
-  "sqrt (n\<^sup>2) = n"
+lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n"
 proof -
   have "{m. m \<le> n} \<noteq> {}" by auto
   then have "Max {m. m \<le> n} \<le> n" by auto
@@ -109,16 +99,13 @@
     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
 qed
 
-lemma sqrt_zero [simp]:
-  "sqrt 0 = 0"
+lemma sqrt_zero [simp]: "sqrt 0 = 0"
   using sqrt_inverse_power2 [of 0] by simp
 
-lemma sqrt_one [simp]:
-  "sqrt 1 = 1"
+lemma sqrt_one [simp]: "sqrt 1 = 1"
   using sqrt_inverse_power2 [of 1] by simp
 
-lemma mono_sqrt:
-  "mono sqrt"
+lemma mono_sqrt: "mono sqrt"
 proof
   fix m n :: nat
   have *: "0 * 0 \<le> m" by simp
@@ -127,8 +114,7 @@
     by (auto intro!: Max_mono `0 * 0 \<le> m` finite_less_ub simp add: power2_eq_square sqrt_def)
 qed
 
-lemma sqrt_greater_zero_iff [simp]:
-  "sqrt n > 0 \<longleftrightarrow> n > 0"
+lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
 proof -
   have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
     by (rule Max_gr_iff) (fact sqrt_aux)+
@@ -146,8 +132,7 @@
   qed
 qed
 
-lemma sqrt_power2_le [simp]: (* FIXME tune proof *)
-  "(sqrt n)\<^sup>2 \<le> n"
+lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
 proof (cases "n > 0")
   case False then show ?thesis by simp
 next
@@ -172,19 +157,20 @@
         then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
           using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
         then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
-        then show ?thesis apply simp
+        then show ?thesis
+          apply simp
           apply (subst Max_le_iff)
           apply auto
           apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
           apply (metis `q * q \<le> n`)
-          using `q * q \<le> n` by (metis le_cases mult_le_mono1 mult_le_mono2 order_trans)
+          apply (metis `q * q \<le> n` le_cases mult_le_mono1 mult_le_mono2 order_trans)
+          done
       qed
     qed
   with * show ?thesis by (simp add: sqrt_def power2_eq_square)
 qed
 
-lemma sqrt_le:
-  "sqrt n \<le> n"
+lemma sqrt_le: "sqrt n \<le> n"
   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
 
 hide_const (open) log sqrt