--- 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