src/HOL/NthRoot.thy
changeset 62393 a620a8756b7c
parent 62381 a6479cb85944
parent 62390 842917225d56
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/NthRoot.thy	Tue Feb 23 16:50:10 2016 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Tue Feb 23 18:04:31 2016 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4    have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
     1.5    fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
     1.6      using power_less_imp_less_base[of a n b]  power_less_imp_less_base[of "-b" n "-a"]
     1.7 -    by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
     1.8 +    by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: if_split_asm)
     1.9  qed
    1.10  
    1.11  lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
    1.12 @@ -122,13 +122,13 @@
    1.13    by (auto split: split_root simp: sgn_real_def)
    1.14  
    1.15  lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
    1.16 -  using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
    1.17 +  using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: if_split_asm)
    1.18  
    1.19  lemma real_root_power_cancel: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (x ^ n) = x"
    1.20    using root_sgn_power[of n x] by (auto simp add: le_less power_0_left)
    1.21  
    1.22  lemma odd_real_root_power_cancel: "odd n \<Longrightarrow> root n (x ^ n) = x"
    1.23 -  using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: split_if_asm)
    1.24 +  using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: if_split_asm)
    1.25  
    1.26  lemma real_root_pos_unique: "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
    1.27    using root_sgn_power[of n y] by (auto simp add: le_less power_0_left)