src/HOL/Parity.thy
changeset 60758 d8d85a8172b5
parent 60562 24af00b010cf
child 60867 86e7560e07d0
     1.1 --- a/src/HOL/Parity.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Parity.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Author:     Jacques D. Fleuriot
     1.5  *)
     1.6  
     1.7 -section {* Parity in rings and semirings *}
     1.8 +section \<open>Parity in rings and semirings\<close>
     1.9  
    1.10  theory Parity
    1.11  imports Nat_Transfer
    1.12  begin
    1.13  
    1.14 -subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
    1.15 +subsection \<open>Ring structures with parity and @{text even}/@{text odd} predicates\<close>
    1.16  
    1.17  class semiring_parity = comm_semiring_1_cancel + numeral +
    1.18    assumes odd_one [simp]: "\<not> 2 dvd 1"
    1.19 @@ -115,7 +115,7 @@
    1.20  end
    1.21  
    1.22  
    1.23 -subsection {* Instances for @{typ nat} and @{typ int} *}
    1.24 +subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
    1.25  
    1.26  lemma even_Suc_Suc_iff [simp]:
    1.27    "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
    1.28 @@ -227,7 +227,7 @@
    1.29    by (simp add: even_int_iff [symmetric])
    1.30  
    1.31  
    1.32 -subsection {* Parity and powers *}
    1.33 +subsection \<open>Parity and powers\<close>
    1.34  
    1.35  context comm_ring_1
    1.36  begin
    1.37 @@ -291,34 +291,34 @@
    1.38    shows "a ^ n \<le> b ^ n"
    1.39  proof -
    1.40    have "0 \<le> \<bar>a\<bar>" by auto
    1.41 -  with `\<bar>a\<bar> \<le> \<bar>b\<bar>`
    1.42 +  with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close>
    1.43    have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" by (rule power_mono)
    1.44 -  with `even n` show ?thesis by (simp add: power_even_abs)  
    1.45 +  with \<open>even n\<close> show ?thesis by (simp add: power_even_abs)  
    1.46  qed
    1.47  
    1.48  lemma power_mono_odd:
    1.49    assumes "odd n" and "a \<le> b"
    1.50    shows "a ^ n \<le> b ^ n"
    1.51  proof (cases "b < 0")
    1.52 -  case True with `a \<le> b` have "- b \<le> - a" and "0 \<le> - b" by auto
    1.53 +  case True with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
    1.54    hence "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
    1.55 -  with `odd n` show ?thesis by simp
    1.56 +  with \<open>odd n\<close> show ?thesis by simp
    1.57  next
    1.58    case False then have "0 \<le> b" by auto
    1.59    show ?thesis
    1.60    proof (cases "a < 0")
    1.61 -    case True then have "n \<noteq> 0" and "a \<le> 0" using `odd n` [THEN odd_pos] by auto
    1.62 -    then have "a ^ n \<le> 0" unfolding power_le_zero_eq using `odd n` by auto
    1.63 +    case True then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
    1.64 +    then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
    1.65      moreover
    1.66 -    from `0 \<le> b` have "0 \<le> b ^ n" by auto
    1.67 +    from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
    1.68      ultimately show ?thesis by auto
    1.69    next
    1.70      case False then have "0 \<le> a" by auto
    1.71 -    with `a \<le> b` show ?thesis using power_mono by auto
    1.72 +    with \<open>a \<le> b\<close> show ?thesis using power_mono by auto
    1.73    qed
    1.74  qed
    1.75   
    1.76 -text {* Simplify, when the exponent is a numeral *}
    1.77 +text \<open>Simplify, when the exponent is a numeral\<close>
    1.78  
    1.79  lemma zero_le_power_eq_numeral [simp]:
    1.80    "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
    1.81 @@ -345,7 +345,7 @@
    1.82  end
    1.83  
    1.84  
    1.85 -subsubsection {* Tools setup *}
    1.86 +subsubsection \<open>Tools setup\<close>
    1.87  
    1.88  declare transfer_morphism_int_nat [transfer add return:
    1.89    even_int_iff