src/HOL/Hyperreal/NthRoot.thy
changeset 23257 9117e228a8e3
parent 23122 3d853d6f2f7d
child 23441 ee218296d635
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue Jun 05 16:32:16 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Tue Jun 05 17:16:41 2007 +0200
     1.3 @@ -179,6 +179,66 @@
     1.4  lemmas real_root_le_0_iff [simp] = real_root_le_iff [where y=0, simplified]
     1.5  lemmas real_root_eq_0_iff [simp] = real_root_eq_iff [where y=0, simplified]
     1.6  
     1.7 +lemma real_root_gt_1_iff [simp]: "0 < n \<Longrightarrow> (1 < root n y) = (1 < y)"
     1.8 +by (insert real_root_less_iff [where x=1], simp)
     1.9 +
    1.10 +lemma real_root_lt_1_iff [simp]: "0 < n \<Longrightarrow> (root n x < 1) = (x < 1)"
    1.11 +by (insert real_root_less_iff [where y=1], simp)
    1.12 +
    1.13 +lemma real_root_ge_1_iff [simp]: "0 < n \<Longrightarrow> (1 \<le> root n y) = (1 \<le> y)"
    1.14 +by (insert real_root_le_iff [where x=1], simp)
    1.15 +
    1.16 +lemma real_root_le_1_iff [simp]: "0 < n \<Longrightarrow> (root n x \<le> 1) = (x \<le> 1)"
    1.17 +by (insert real_root_le_iff [where y=1], simp)
    1.18 +
    1.19 +lemma real_root_eq_1_iff [simp]: "0 < n \<Longrightarrow> (root n x = 1) = (x = 1)"
    1.20 +by (insert real_root_eq_iff [where y=1], simp)
    1.21 +
    1.22 +text {* Roots of roots *}
    1.23 +
    1.24 +lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x"
    1.25 +by (simp add: odd_real_root_unique)
    1.26 +
    1.27 +lemma real_root_pos_mult_exp:
    1.28 +  "\<lbrakk>0 < m; 0 < n; 0 < x\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
    1.29 +by (rule real_root_pos_unique, simp_all add: power_mult)
    1.30 +
    1.31 +lemma real_root_mult_exp:
    1.32 +  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
    1.33 +apply (rule linorder_cases [where x=x and y=0])
    1.34 +apply (subgoal_tac "root (m * n) (- x) = root m (root n (- x))")
    1.35 +apply (simp add: real_root_minus)
    1.36 +apply (simp_all add: real_root_pos_mult_exp)
    1.37 +done
    1.38 +
    1.39 +lemma real_root_commute:
    1.40 +  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root m (root n x) = root n (root m x)"
    1.41 +by (simp add: real_root_mult_exp [symmetric] mult_commute)
    1.42 +
    1.43 +text {* Monotonicity in first argument *}
    1.44 +
    1.45 +lemma real_root_strict_decreasing:
    1.46 +  "\<lbrakk>0 < n; n < N; 1 < x\<rbrakk> \<Longrightarrow> root N x < root n x"
    1.47 +apply (subgoal_tac "root n (root N x) ^ n < root N (root n x) ^ N", simp)
    1.48 +apply (simp add: real_root_commute power_strict_increasing
    1.49 +            del: real_root_pow_pos2)
    1.50 +done
    1.51 +
    1.52 +lemma real_root_strict_increasing:
    1.53 +  "\<lbrakk>0 < n; n < N; 0 < x; x < 1\<rbrakk> \<Longrightarrow> root n x < root N x"
    1.54 +apply (subgoal_tac "root N (root n x) ^ N < root n (root N x) ^ n", simp)
    1.55 +apply (simp add: real_root_commute power_strict_decreasing
    1.56 +            del: real_root_pow_pos2)
    1.57 +done
    1.58 +
    1.59 +lemma real_root_decreasing:
    1.60 +  "\<lbrakk>0 < n; n < N; 1 \<le> x\<rbrakk> \<Longrightarrow> root N x \<le> root n x"
    1.61 +by (auto simp add: order_le_less real_root_strict_decreasing)
    1.62 +
    1.63 +lemma real_root_increasing:
    1.64 +  "\<lbrakk>0 < n; n < N; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> root n x \<le> root N x"
    1.65 +by (auto simp add: order_le_less real_root_strict_increasing)
    1.66 +
    1.67  text {* Roots of multiplication and division *}
    1.68  
    1.69  lemma real_root_mult_lemma: