# HG changeset patch
# User noschinl
# Date 1324302068 -3600
# Node ID 2a882ef2cd73ffe6920d629e1c22f8e849b2f4eb
# Parent  758671e966a0ebbc9c5592ae33702607ebc49434
add lemmas

diff -r 758671e966a0 -r 2a882ef2cd73 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Mon Dec 19 13:58:54 2011 +0100
+++ b/src/HOL/Fact.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -285,6 +285,12 @@
     (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
 by (cases m) auto
 
+lemma fact_le_power: "fact n \<le> n^n"
+proof (induct n)
+  case (Suc n)
+  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
+  then show ?case by (simp add: add_le_mono)
+qed simp
 
 subsection {* @{term fact} and @{term of_nat} *}
 
diff -r 758671e966a0 -r 2a882ef2cd73 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Mon Dec 19 13:58:54 2011 +0100
+++ b/src/HOL/Log.thy	Mon Dec 19 14:41:08 2011 +0100
@@ -60,6 +60,10 @@
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
 by (simp add: powr_def exp_add [symmetric] left_distrib)
 
+lemma powr_mult_base:
+  "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
+using assms by (auto simp: powr_add)
+
 lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
 by (simp add: powr_def)
 
@@ -178,6 +182,10 @@
   apply (rule powr_realpow [THEN sym], simp)
 done
 
+lemma root_powr_inverse:
+  "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
+by (auto simp: root_def powr_realpow[symmetric] powr_powr)
+
 lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
 by (unfold powr_def, simp)