Added lemmas to Ring_and_Field with slightly modified simplification rules
authorpaulson
Mon Jan 12 16:51:45 2004 +0100 (2004-01-12)
changeset 1435379f9fbef9106
parent 14352 a8b1a44d8264
child 14354 988aa4648597
Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers
doc-src/TutorialI/Documents/Documents.thy
doc-src/TutorialI/Documents/document/Documents.tex
doc-src/TutorialI/Types/Numbers.thy
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/document/Records.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/isabelle.sty
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSCA.ML
src/HOL/Complex/NSComplexBin.ML
src/HOL/Complex/ex/Sqrt.thy
src/HOL/Hoare/Arith2.ML
src/HOL/Integ/Int.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/IntPower.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/Presburger.thy
src/HOL/Integ/presburger.ML
src/HOL/IsaMakefile
src/HOL/Library/Primes.thy
src/HOL/Library/Rational_Numbers.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/Power.thy
src/HOL/Presburger.thy
src/HOL/Ring_and_Field.thy
src/HOL/Tools/Presburger/presburger.ML
src/HOL/ex/PresburgerEx.thy
src/HOL/ex/set.thy
     1.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Mon Jan 12 16:45:35 2004 +0100
     1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Jan 12 16:51:45 2004 +0100
     1.3 @@ -763,13 +763,13 @@
     1.4  *}
     1.5  
     1.6  lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
     1.7 -  by (auto(*<*)simp add: int_less_le(*>*))
     1.8 +  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
     1.9  
    1.10  text {*
    1.11    \noindent Here the real source of the proof has been as follows:
    1.12  
    1.13  \begin{verbatim}
    1.14 -  by (auto(*<*)simp add: int_less_le(*>*))
    1.15 +  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
    1.16  \end{verbatim}
    1.17  %(*
    1.18  
     2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 12 16:45:35 2004 +0100
     2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 12 16:51:45 2004 +0100
     2.3 @@ -799,7 +799,7 @@
     2.4  \noindent Here the real source of the proof has been as follows:
     2.5  
     2.6  \begin{verbatim}
     2.7 -  by (auto(*<*)simp add: int_less_le(*>*))
     2.8 +  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
     2.9  \end{verbatim}
    2.10  %(*
    2.11  
     3.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Mon Jan 12 16:45:35 2004 +0100
     3.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Jan 12 16:51:45 2004 +0100
     3.3 @@ -197,14 +197,11 @@
     3.4  
     3.5  text {*REALS
     3.6  
     3.7 -@{thm[display] realpow_abs[no_vars]}
     3.8 -\rulename{realpow_abs}
     3.9 -
    3.10  @{thm[display] dense[no_vars]}
    3.11  \rulename{dense}
    3.12  
    3.13 -@{thm[display] realpow_abs[no_vars]}
    3.14 -\rulename{realpow_abs}
    3.15 +@{thm[display] power_abs[no_vars]}
    3.16 +\rulename{power_abs}
    3.17  
    3.18  @{thm[display] times_divide_eq_right[no_vars]}
    3.19  \rulename{times_divide_eq_right}
     4.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Jan 12 16:45:35 2004 +0100
     4.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Jan 12 16:51:45 2004 +0100
     4.3 @@ -320,19 +320,14 @@
     4.4  REALS
     4.5  
     4.6  \begin{isabelle}%
     4.7 -{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
     4.8 -\end{isabelle}
     4.9 -\rulename{realpow_abs}
    4.10 -
    4.11 -\begin{isabelle}%
    4.12  a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
    4.13  \end{isabelle}
    4.14  \rulename{dense}
    4.15  
    4.16  \begin{isabelle}%
    4.17 -{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
    4.18 +{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
    4.19  \end{isabelle}
    4.20 -\rulename{realpow_abs}
    4.21 +\rulename{power_abs}
    4.22  
    4.23  \begin{isabelle}%
    4.24  a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
     5.1 --- a/doc-src/TutorialI/Types/document/Records.tex	Mon Jan 12 16:45:35 2004 +0100
     5.2 +++ b/doc-src/TutorialI/Types/document/Records.tex	Mon Jan 12 16:51:45 2004 +0100
     5.3 @@ -379,9 +379,9 @@
     5.4    be the same as \isa{point{\isachardot}make}.
     5.5  
     5.6    \begin{isabelle}%
     5.7 -point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isanewline
     5.8 +point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isasep\isanewline%
     5.9  point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
    5.10 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline
    5.11 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
    5.12  point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
    5.13  \end{isabelle}
    5.14  
    5.15 @@ -389,10 +389,10 @@
    5.16  
    5.17    \begin{isabelle}%
    5.18  cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
    5.19 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isanewline
    5.20 -cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isanewline
    5.21 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
    5.22 +cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
    5.23  cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
    5.24 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline
    5.25 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
    5.26  cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
    5.27  {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
    5.28  \end{isabelle}
     6.1 --- a/doc-src/TutorialI/Types/numerics.tex	Mon Jan 12 16:45:35 2004 +0100
     6.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Mon Jan 12 16:51:45 2004 +0100
     6.3 @@ -439,9 +439,9 @@
     6.4  defined for the reals, along with many theorems such as this one about
     6.5  exponentiation:
     6.6  \begin{isabelle}
     6.7 -\isasymbar r\ \isacharcircum \ n\isasymbar\ =\ 
     6.8 -\isasymbar r\isasymbar \ \isacharcircum \ n
     6.9 -\rulename{realpow_abs}
    6.10 +\isasymbar a\ \isacharcircum \ n\isasymbar\ =\ 
    6.11 +\isasymbar a\isasymbar \ \isacharcircum \ n
    6.12 +\rulename{power_abs}
    6.13  \end{isabelle}
    6.14  
    6.15  Numeric literals\index{numeric literals!for type \protect\isa{real}}
     7.1 --- a/doc-src/TutorialI/isabelle.sty	Mon Jan 12 16:45:35 2004 +0100
     7.2 +++ b/doc-src/TutorialI/isabelle.sty	Mon Jan 12 16:51:45 2004 +0100
     7.3 @@ -52,6 +52,7 @@
     7.4  
     7.5  \newcommand{\isaindent}[1]{\hphantom{#1}}
     7.6  \newcommand{\isanewline}{\mbox{}\par\mbox{}}
     7.7 +\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
     7.8  \newcommand{\isadigit}[1]{#1}
     7.9  
    7.10  \chardef\isacharbang=`\!
     8.1 --- a/src/HOL/Complex/Complex.thy	Mon Jan 12 16:45:35 2004 +0100
     8.2 +++ b/src/HOL/Complex/Complex.thy	Mon Jan 12 16:51:45 2004 +0100
     8.3 @@ -527,7 +527,7 @@
     8.4  lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1"
     8.5  apply (rule_tac z = z in eq_Abs_complex)
     8.6  apply (auto simp add: complex_mult complex_inverse complex_one_def 
     8.7 -       complex_zero_def add_divide_distrib [symmetric] real_power_two mult_ac)
     8.8 +       complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
     8.9  apply (drule_tac y = y in real_sum_squares_not_zero)
    8.10  apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
    8.11  done
    8.12 @@ -615,7 +615,7 @@
    8.13   "complex_of_real(inverse x) = inverse(complex_of_real x)"
    8.14  apply (case_tac "x=0", simp)
    8.15  apply (simp add: complex_inverse complex_of_real_def real_divide_def 
    8.16 -                 inverse_mult_distrib real_power_two)
    8.17 +                 inverse_mult_distrib power2_eq_square)
    8.18  done
    8.19  
    8.20  lemma complex_of_real_add:
    8.21 @@ -658,10 +658,10 @@
    8.22  declare complex_mod_zero [simp]
    8.23  
    8.24  lemma complex_mod_one [simp]: "cmod(1) = 1"
    8.25 -by (simp add: cmod_def real_power_two)
    8.26 +by (simp add: cmod_def power2_eq_square)
    8.27  
    8.28  lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
    8.29 -apply (simp add: complex_of_real_def real_power_two complex_mod)
    8.30 +apply (simp add: complex_of_real_def power2_eq_square complex_mod)
    8.31  done
    8.32  declare complex_mod_complex_of_real [simp]
    8.33  
    8.34 @@ -702,7 +702,7 @@
    8.35  
    8.36  lemma complex_mod_cnj: "cmod (cnj z) = cmod z"
    8.37  apply (rule_tac z = z in eq_Abs_complex)
    8.38 -apply (simp (no_asm_simp) add: complex_cnj complex_mod real_power_two)
    8.39 +apply (simp (no_asm_simp) add: complex_cnj complex_mod power2_eq_square)
    8.40  done
    8.41  declare complex_mod_cnj [simp]
    8.42  
    8.43 @@ -713,7 +713,7 @@
    8.44  
    8.45  lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"
    8.46  apply (rule_tac z = z in eq_Abs_complex)
    8.47 -apply (simp (no_asm_simp) add: complex_cnj complex_inverse real_power_two)
    8.48 +apply (simp (no_asm_simp) add: complex_cnj complex_inverse power2_eq_square)
    8.49  done
    8.50  
    8.51  lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"
    8.52 @@ -771,7 +771,7 @@
    8.53  
    8.54  lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
    8.55  apply (rule_tac z = z in eq_Abs_complex)
    8.56 -apply (auto simp add: complex_cnj complex_mult complex_of_real_def real_power_two)
    8.57 +apply (auto simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
    8.58  done
    8.59  
    8.60  
    8.61 @@ -802,7 +802,7 @@
    8.62  
    8.63  lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
    8.64  apply (rule_tac z = x in eq_Abs_complex)
    8.65 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def real_power_two)
    8.66 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square)
    8.67  done
    8.68  declare complex_mod_eq_zero_cancel [simp]
    8.69  
    8.70 @@ -813,14 +813,14 @@
    8.71  
    8.72  lemma complex_mod_minus: "cmod (-x) = cmod(x)"
    8.73  apply (rule_tac z = x in eq_Abs_complex)
    8.74 -apply (simp (no_asm_simp) add: complex_mod complex_minus real_power_two)
    8.75 +apply (simp (no_asm_simp) add: complex_mod complex_minus power2_eq_square)
    8.76  done
    8.77  declare complex_mod_minus [simp]
    8.78  
    8.79  lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
    8.80  apply (rule_tac z = z in eq_Abs_complex)
    8.81  apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult);
    8.82 -apply (simp (no_asm) add: real_power_two real_abs_def)
    8.83 +apply (simp (no_asm) add: power2_eq_square real_abs_def)
    8.84  done
    8.85  
    8.86  lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"
    8.87 @@ -841,15 +841,15 @@
    8.88  apply (rule_tac z = y in eq_Abs_complex)
    8.89  apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
    8.90  apply (rule_tac n = 1 in power_inject_base)
    8.91 -apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc)
    8.92 -apply (auto simp add: real_diff_def real_power_two right_distrib left_distrib add_ac mult_ac)
    8.93 +apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
    8.94 +apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac)
    8.95  done
    8.96  
    8.97  lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
    8.98  apply (rule_tac z = x in eq_Abs_complex)
    8.99  apply (rule_tac z = y in eq_Abs_complex)
   8.100  apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   8.101 -apply (auto simp add: right_distrib left_distrib real_power_two mult_ac add_ac)
   8.102 +apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
   8.103  done
   8.104  
   8.105  lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) <= cmod(x * cnj y)"
   8.106 @@ -866,7 +866,7 @@
   8.107  declare complex_Re_mult_cnj_le_cmod2 [simp]
   8.108  
   8.109  lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
   8.110 -apply (simp (no_asm) add: left_distrib right_distrib real_power_two)
   8.111 +apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)
   8.112  done
   8.113  
   8.114  lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 <= (cmod(x) + cmod(y)) ^ 2"
   8.115 @@ -883,7 +883,7 @@
   8.116  lemma complex_mod_triangle_ineq: "cmod (x + y) <= cmod(x) + cmod(y)"
   8.117  apply (rule_tac n = 1 in realpow_increasing)
   8.118  apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
   8.119 -            simp add: real_power_two [symmetric])
   8.120 +            simp add: power2_eq_square [symmetric])
   8.121  done
   8.122  declare complex_mod_triangle_ineq [simp]
   8.123  
   8.124 @@ -897,7 +897,7 @@
   8.125  lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"
   8.126  apply (rule_tac z = x in eq_Abs_complex)
   8.127  apply (rule_tac z = y in eq_Abs_complex)
   8.128 -apply (auto simp add: complex_diff complex_mod right_diff_distrib real_power_two left_diff_distrib add_ac mult_ac)
   8.129 +apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)
   8.130  done
   8.131  
   8.132  lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"
   8.133 @@ -943,7 +943,7 @@
   8.134  
   8.135  lemma complex_inverse_minus: "inverse (-x) = - inverse (x::complex)"
   8.136  apply (rule_tac z = x in eq_Abs_complex)
   8.137 -apply (simp (no_asm_simp) add: complex_inverse complex_minus real_power_two)
   8.138 +apply (simp (no_asm_simp) add: complex_inverse complex_minus power2_eq_square)
   8.139  done
   8.140  
   8.141  lemma complex_divide_one: "x / (1::complex) = x"
   8.142 @@ -1201,7 +1201,7 @@
   8.143  lemma complex_mod_mult_i:
   8.144      "cmod (ii * complex_of_real y) = abs y"
   8.145  apply (unfold i_def complex_of_real_def)
   8.146 -apply (auto simp add: complex_mult complex_mod real_power_two)
   8.147 +apply (auto simp add: complex_mult complex_mod power2_eq_square)
   8.148  done
   8.149  declare complex_mod_mult_i [simp]
   8.150  
   8.151 @@ -1427,7 +1427,7 @@
   8.152  lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
   8.153  apply (case_tac "r=0")
   8.154  apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
   8.155 -apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def real_power_two complex_mult_ac mult_ac)
   8.156 +apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def power2_eq_square complex_mult_ac mult_ac)
   8.157  apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def)
   8.158  done
   8.159  
     9.1 --- a/src/HOL/Complex/NSCA.ML	Mon Jan 12 16:45:35 2004 +0100
     9.2 +++ b/src/HOL/Complex/NSCA.ML	Mon Jan 12 16:51:45 2004 +0100
     9.3 @@ -823,26 +823,28 @@
     9.4  by (dtac (approx_minus_iff RS iffD1) 1);
     9.5  by (dtac (approx_minus_iff RS iffD1) 1);
     9.6  by (rtac (capprox_minus_iff RS iffD2) 1);
     9.7 -by (auto_tac (claset(),simpset() addsimps [mem_cinfmal_iff RS sym,
     9.8 -    mem_infmal_iff RS sym,hypreal_minus,hypreal_add,hcomplex_minus,
     9.9 -    hcomplex_add,CInfinitesimal_hcmod_iff,hcmod,Infinitesimal_FreeUltrafilterNat_iff]));
    9.10 +by (auto_tac (claset(),
    9.11 +     simpset() addsimps [mem_cinfmal_iff RS sym,
    9.12 +	    mem_infmal_iff RS sym,hypreal_minus,hypreal_add,hcomplex_minus,
    9.13 +	    hcomplex_add,CInfinitesimal_hcmod_iff,hcmod,
    9.14 +	    Infinitesimal_FreeUltrafilterNat_iff]));
    9.15  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    9.16  by Auto_tac;
    9.17  by (dres_inst_tac [("x","u/2")] spec 1);
    9.18  by (dres_inst_tac [("x","u/2")] spec 1);
    9.19 -by (Step_tac 1);
    9.20 +by Safe_tac;
    9.21  by (TRYALL(Force_tac));
    9.22  by (ultra_tac (claset(),HOL_ss) 1);
    9.23 -by (dtac sym 1 THEN dtac sym 1);
    9.24 +by (dtac sym 1 THEN dtac sym 1); 
    9.25  by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    9.26  by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    9.27 -by (auto_tac (claset(),HOL_ss addsimps [complex_minus,complex_add,
    9.28 +by (auto_tac (claset(),
    9.29 +    HOL_ss addsimps [complex_minus,complex_add,
    9.30      complex_mod, snd_conv, fst_conv,numeral_2_eq_2]));
    9.31 -by (rtac (realpow_two_abs RS subst) 1);
    9.32 -by (res_inst_tac [("x1","xa + - xb")] (realpow_two_abs RS subst) 1);
    9.33 -by (simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym]) 1);
    9.34 -by (rtac lemma_sqrt_hcomplex_capprox 1);
    9.35 +by (subgoal_tac "sqrt (abs(xa + - xb) ^ 2 + abs(y + - ya) ^ 2) < u" 1);
    9.36 +by (rtac lemma_sqrt_hcomplex_capprox 2);
    9.37  by Auto_tac;
    9.38 +by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1); 
    9.39  qed "hcomplex_capproxI";
    9.40  
    9.41  Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) =\
    9.42 @@ -902,11 +904,10 @@
    9.43  by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
    9.44  by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
    9.45  by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
    9.46 -by (rtac (realpow_two_abs RS subst) 1);
    9.47 -by (res_inst_tac [("x1","Y x")] (realpow_two_abs RS subst) 1);
    9.48 -by (simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym]) 1);
    9.49 -by (rtac lemma_sqrt_hcomplex_capprox 1);
    9.50 +by (subgoal_tac "sqrt (abs(Y x) ^ 2 + abs(Z x) ^ 2) < 2*u + 2*v" 1);
    9.51 +by (rtac lemma_sqrt_hcomplex_capprox 2);
    9.52  by Auto_tac;
    9.53 +by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1); 
    9.54  qed "HFinite_Re_Im_CFinite";
    9.55  
    9.56  Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite) = \
    10.1 --- a/src/HOL/Complex/NSComplexBin.ML	Mon Jan 12 16:45:35 2004 +0100
    10.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Mon Jan 12 16:51:45 2004 +0100
    10.3 @@ -328,8 +328,7 @@
    10.4  val simplify_meta_eq = 
    10.5      Int_Numeral_Simprocs.simplify_meta_eq
    10.6           [add_zero_left, add_zero_right,
    10.7 - 	  mult_left_zero, mult_right_zero, mult_1, 
    10.8 -          mult_1_right];
    10.9 + 	  mult_zero_left, mult_zero_right, mult_1, mult_1_right];
   10.10  
   10.11  val prep_simproc = Complex_Numeral_Simprocs.prep_simproc;
   10.12  
    11.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Mon Jan 12 16:45:35 2004 +0100
    11.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Mon Jan 12 16:51:45 2004 +0100
    11.3 @@ -84,7 +84,7 @@
    11.4    proof -
    11.5      from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    11.6      then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
    11.7 -      by (auto simp add: power_two real_power_two)
    11.8 +      by (auto simp add: power2_eq_square)
    11.9      also have "(sqrt (real p))\<twosuperior> = real p" by simp
   11.10      also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
   11.11      finally show ?thesis ..
   11.12 @@ -94,8 +94,8 @@
   11.13      from eq have "p dvd m\<twosuperior>" ..
   11.14      with p_prime show "p dvd m" by (rule prime_dvd_power_two)
   11.15      then obtain k where "m = p * k" ..
   11.16 -    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
   11.17 -    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
   11.18 +    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
   11.19 +    with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
   11.20      then have "p dvd n\<twosuperior>" ..
   11.21      with p_prime show "p dvd n" by (rule prime_dvd_power_two)
   11.22    qed
   11.23 @@ -127,15 +127,15 @@
   11.24      and gcd: "gcd (m, n) = 1" ..
   11.25    from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
   11.26    then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
   11.27 -    by (auto simp add: power_two real_power_two)
   11.28 +    by (auto simp add: power2_eq_square)
   11.29    also have "(sqrt (real p))\<twosuperior> = real p" by simp
   11.30    also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
   11.31    finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
   11.32    then have "p dvd m\<twosuperior>" ..
   11.33    with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
   11.34    then obtain k where "m = p * k" ..
   11.35 -  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
   11.36 -  with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
   11.37 +  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
   11.38 +  with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
   11.39    then have "p dvd n\<twosuperior>" ..
   11.40    with p_prime have "p dvd n" by (rule prime_dvd_power_two)
   11.41    with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
    12.1 --- a/src/HOL/Hoare/Arith2.ML	Mon Jan 12 16:45:35 2004 +0100
    12.2 +++ b/src/HOL/Hoare/Arith2.ML	Mon Jan 12 16:51:45 2004 +0100
    12.3 @@ -64,7 +64,7 @@
    12.4  (*** pow ***)
    12.5  
    12.6  Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
    12.7 -by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
    12.8 -				      mult_div_cancel]) 1);
    12.9 +by (asm_simp_tac (simpset() addsimps [power2_eq_square RS sym, 
   12.10 +                   power_mult RS sym, mult_div_cancel]) 1);
   12.11  qed "sq_pow_div2";
   12.12  Addsimps [sq_pow_div2];
    13.1 --- a/src/HOL/Integ/Int.thy	Mon Jan 12 16:45:35 2004 +0100
    13.2 +++ b/src/HOL/Integ/Int.thy	Mon Jan 12 16:51:45 2004 +0100
    13.3 @@ -229,6 +229,8 @@
    13.4  by (simp add: zabs_def)
    13.5  
    13.6  text{*This version is proved for all ordered rings, not just integers!
    13.7 +      It is proved here because attribute @{text arith_split} is not available
    13.8 +      in theory @{text Ring_and_Field}.
    13.9        But is it really better than just rewriting with @{text abs_if}?*}
   13.10  lemma abs_split [arith_split]:
   13.11       "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   13.12 @@ -371,6 +373,7 @@
   13.13  val negative_eq_positive = thm "negative_eq_positive";
   13.14  val zle_iff_zadd = thm "zle_iff_zadd";
   13.15  val abs_int_eq = thm "abs_int_eq";
   13.16 +val abs_split = thm"abs_split";
   13.17  val nat_int = thm "nat_int";
   13.18  val nat_zminus_int = thm "nat_zminus_int";
   13.19  val nat_zero = thm "nat_zero";
    14.1 --- a/src/HOL/Integ/IntArith.thy	Mon Jan 12 16:45:35 2004 +0100
    14.2 +++ b/src/HOL/Integ/IntArith.thy	Mon Jan 12 16:51:45 2004 +0100
    14.3 @@ -8,6 +8,7 @@
    14.4  theory IntArith = Bin
    14.5  files ("int_arith1.ML"):
    14.6  
    14.7 +
    14.8  subsection{*Inequality Reasoning for the Arithmetic Simproc*}
    14.9  
   14.10  lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
   14.11 @@ -24,6 +25,7 @@
   14.12  use "int_arith1.ML"
   14.13  setup int_arith_setup
   14.14  
   14.15 +
   14.16  subsection{*More inequality reasoning*}
   14.17  
   14.18  lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
   14.19 @@ -41,7 +43,8 @@
   14.20  lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
   14.21  by arith
   14.22  
   14.23 -subsection{*Results about @{term nat}*}
   14.24 +
   14.25 +subsection{*The Functions @{term nat} and @{term int}*}
   14.26  
   14.27  lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
   14.28  by (blast dest: nat_0_le sym)
   14.29 @@ -62,7 +65,8 @@
   14.30  by (auto simp add: nat_eq_iff2)
   14.31  
   14.32  
   14.33 -(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
   14.34 +text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
   14.35 +  @{term "w + - z"}*}
   14.36  declare Zero_int_def [symmetric, simp]
   14.37  declare One_int_def [symmetric, simp]
   14.38  
   14.39 @@ -87,28 +91,11 @@
   14.40  lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   14.41  by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
   14.42  
   14.43 -subsection{*@{term abs}: Absolute Value, as an Integer*}
   14.44 -
   14.45 -(* Simpler: use zabs_def as rewrite rule
   14.46 -   but arith_tac is not parameterized by such simp rules
   14.47 -*)
   14.48 -
   14.49 -lemma zabs_split [arith_split]:
   14.50 -     "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
   14.51 -by (simp add: zabs_def)
   14.52 -
   14.53 -lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)"
   14.54 -by (simp add: zabs_def)
   14.55 -
   14.56  
   14.57  text{*This simplifies expressions of the form @{term "int n = z"} where
   14.58        z is an integer literal.*}
   14.59  declare int_eq_iff [of _ "number_of v", standard, simp]
   14.60  
   14.61 -lemma zabs_eq_iff:
   14.62 -    "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
   14.63 -  by (auto simp add: zabs_def)
   14.64 -
   14.65  lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   14.66    by simp
   14.67  
   14.68 @@ -202,21 +189,6 @@
   14.69  apply (rule step, simp+)
   14.70  done
   14.71  
   14.72 -subsection{*Simple Equations*}
   14.73 -
   14.74 -lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)"
   14.75 -by simp
   14.76 -
   14.77 -lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)"
   14.78 -by arith
   14.79 -
   14.80 -lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
   14.81 -by arith
   14.82 -
   14.83 -lemma triangle_ineq: "abs(x+y) \<le> abs(x) + abs(y::int)"
   14.84 -by arith
   14.85 -
   14.86 -
   14.87  subsection{*Intermediate value theorems*}
   14.88  
   14.89  lemma int_val_lemma:
   14.90 @@ -249,39 +221,6 @@
   14.91  done
   14.92  
   14.93  
   14.94 -subsection{*Some convenient biconditionals for products of signs*}
   14.95 -
   14.96 -lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
   14.97 -  by (rule Ring_and_Field.mult_pos)
   14.98 -
   14.99 -lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
  14.100 -  by (rule Ring_and_Field.mult_neg)
  14.101 -
  14.102 -lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
  14.103 -  by (rule Ring_and_Field.mult_pos_neg)
  14.104 -
  14.105 -lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
  14.106 -  by (rule Ring_and_Field.zero_less_mult_iff)
  14.107 -
  14.108 -lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
  14.109 -  by (rule Ring_and_Field.zero_le_mult_iff)
  14.110 -
  14.111 -lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
  14.112 -  by (rule Ring_and_Field.mult_less_0_iff)
  14.113 -
  14.114 -lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
  14.115 -  by (rule Ring_and_Field.mult_le_0_iff)
  14.116 -
  14.117 -lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
  14.118 -  by (rule Ring_and_Field.abs_eq_0)
  14.119 -
  14.120 -lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
  14.121 -  by (rule Ring_and_Field.zero_less_abs_iff)
  14.122 -
  14.123 -lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
  14.124 -  by (rule Ring_and_Field.zero_le_square)
  14.125 -
  14.126 -
  14.127  subsection{*Products and 1, by T. M. Rasmussen*}
  14.128  
  14.129  lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
  14.130 @@ -307,7 +246,7 @@
  14.131  apply (rule zless_1_zmult, arith)
  14.132  apply (subgoal_tac "0<n", arith)
  14.133  apply (subgoal_tac "0<m*n")
  14.134 -apply (drule int_0_less_mult_iff [THEN iffD1], auto)
  14.135 +apply (drule zero_less_mult_iff [THEN iffD1], auto)
  14.136  done
  14.137  
  14.138  lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  14.139 @@ -341,8 +280,8 @@
  14.140  lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
  14.141  apply (case_tac "0 \<le> z'")
  14.142  apply (rule inj_int [THEN injD])
  14.143 -apply (simp add: zmult_int [symmetric] int_0_le_mult_iff)
  14.144 -apply (simp add: zmult_le_0_iff)
  14.145 +apply (simp add: zmult_int [symmetric] zero_le_mult_iff)
  14.146 +apply (simp add: mult_le_0_iff)
  14.147  done
  14.148  
  14.149  lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
  14.150 @@ -353,9 +292,10 @@
  14.151  lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
  14.152  apply (case_tac "z=0 | w=0")
  14.153  apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 
  14.154 -                      nat_mult_distrib_neg [symmetric] zmult_less_0_iff)
  14.155 +                      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
  14.156  done
  14.157  
  14.158 +
  14.159  ML
  14.160  {*
  14.161  val zle_diff1_eq = thm "zle_diff1_eq";
  14.162 @@ -370,25 +310,8 @@
  14.163  val nat_2 = thm "nat_2";
  14.164  val nat_less_eq_zless = thm "nat_less_eq_zless";
  14.165  val nat_le_eq_zle = thm "nat_le_eq_zle";
  14.166 -val zabs_split = thm "zabs_split";
  14.167 -val zero_le_zabs = thm "zero_le_zabs";
  14.168  
  14.169 -val int_diff_minus_eq = thm "int_diff_minus_eq";
  14.170 -val abs_abs = thm "abs_abs";
  14.171 -val abs_minus = thm "abs_minus";
  14.172 -val triangle_ineq = thm "triangle_ineq";
  14.173  val nat_intermed_int_val = thm "nat_intermed_int_val";
  14.174 -val zmult_pos = thm "zmult_pos";
  14.175 -val zmult_neg = thm "zmult_neg";
  14.176 -val zmult_pos_neg = thm "zmult_pos_neg";
  14.177 -val int_0_less_mult_iff = thm "int_0_less_mult_iff";
  14.178 -val int_0_le_mult_iff = thm "int_0_le_mult_iff";
  14.179 -val zmult_less_0_iff = thm "zmult_less_0_iff";
  14.180 -val zmult_le_0_iff = thm "zmult_le_0_iff";
  14.181 -val abs_mult = thm "abs_mult";
  14.182 -val abs_eq_0 = thm "abs_eq_0";
  14.183 -val zero_less_abs_iff = thm "zero_less_abs_iff";
  14.184 -val square_nonzero = thm "square_nonzero";
  14.185  val zmult_eq_self_iff = thm "zmult_eq_self_iff";
  14.186  val zless_1_zmult = thm "zless_1_zmult";
  14.187  val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
    15.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Jan 12 16:45:35 2004 +0100
    15.2 +++ b/src/HOL/Integ/IntDiv.thy	Mon Jan 12 16:51:45 2004 +0100
    15.3 @@ -357,12 +357,12 @@
    15.4  
    15.5  lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
    15.6  apply (subgoal_tac "0 < a*q")
    15.7 - apply (simp add: int_0_less_mult_iff, arith)
    15.8 + apply (simp add: zero_less_mult_iff, arith)
    15.9  done
   15.10  
   15.11  lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
   15.12  apply (subgoal_tac "0 \<le> a* (1-q) ")
   15.13 - apply (simp add: int_0_le_mult_iff)
   15.14 + apply (simp add: zero_le_mult_iff)
   15.15  apply (simp add: zdiff_zmult_distrib2)
   15.16  done
   15.17  
   15.18 @@ -516,7 +516,7 @@
   15.19  lemma q_pos_lemma:
   15.20       "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
   15.21  apply (subgoal_tac "0 < b'* (q' + 1) ")
   15.22 - apply (simp add: int_0_less_mult_iff)
   15.23 + apply (simp add: zero_less_mult_iff)
   15.24  apply (simp add: zadd_zmult_distrib2)
   15.25  done
   15.26  
   15.27 @@ -549,7 +549,7 @@
   15.28  lemma q_neg_lemma:
   15.29       "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
   15.30  apply (subgoal_tac "b'*q' < 0")
   15.31 - apply (simp add: zmult_less_0_iff, arith)
   15.32 + apply (simp add: mult_less_0_iff, arith)
   15.33  done
   15.34  
   15.35  lemma zdiv_mono2_neg_lemma:
   15.36 @@ -711,13 +711,13 @@
   15.37  lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
   15.38  apply (subgoal_tac "b * (q mod c) \<le> 0")
   15.39   apply arith
   15.40 -apply (simp add: zmult_le_0_iff)
   15.41 +apply (simp add: mult_le_0_iff)
   15.42  done
   15.43  
   15.44  lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
   15.45  apply (subgoal_tac "0 \<le> b * (q mod c) ")
   15.46  apply arith
   15.47 -apply (simp add: int_0_le_mult_iff)
   15.48 +apply (simp add: zero_le_mult_iff)
   15.49  done
   15.50  
   15.51  lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
   15.52 @@ -733,7 +733,7 @@
   15.53  lemma zmult2_lemma: "[| quorem ((a,b), (q,r));  b ~= 0;  0 < c |]  
   15.54        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
   15.55  by (auto simp add: mult_ac quorem_def linorder_neq_iff
   15.56 -                   int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
   15.57 +                   zero_less_mult_iff zadd_zmult_distrib2 [symmetric] 
   15.58                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
   15.59  
   15.60  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
   15.61 @@ -1033,7 +1033,7 @@
   15.62  lemma zdvd_anti_sym:
   15.63      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   15.64    apply (unfold dvd_def, auto)
   15.65 -  apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
   15.66 +  apply (simp add: zmult_assoc zmult_eq_self_iff zero_less_mult_iff zmult_eq_1_iff)
   15.67    done
   15.68  
   15.69  lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
   15.70 @@ -1112,15 +1112,15 @@
   15.71    apply (subgoal_tac "0 < n")
   15.72     prefer 2
   15.73     apply (blast intro: zless_trans)
   15.74 -  apply (simp add: int_0_less_mult_iff)
   15.75 +  apply (simp add: zero_less_mult_iff)
   15.76    apply (subgoal_tac "n * k < n * 1")
   15.77     apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
   15.78    done
   15.79  
   15.80  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   15.81    apply (auto simp add: dvd_def nat_abs_mult_distrib)
   15.82 -  apply (auto simp add: nat_eq_iff zabs_eq_iff)
   15.83 -   apply (rule_tac [2] x = "-(int k)" in exI)
   15.84 +  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
   15.85 +   apply (rule_tac x = "-(int k)" in exI)
   15.86    apply (auto simp add: zmult_int [symmetric])
   15.87    done
   15.88  
   15.89 @@ -1131,7 +1131,7 @@
   15.90      apply (rule_tac x = "nat (-k)" in exI)
   15.91      apply (cut_tac [3] k = m in int_less_0_conv)
   15.92      apply (cut_tac k = m in int_less_0_conv)
   15.93 -    apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
   15.94 +    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
   15.95        nat_mult_distrib [symmetric] nat_eq_iff2)
   15.96    done
   15.97  
   15.98 @@ -1139,7 +1139,7 @@
   15.99    apply (auto simp add: dvd_def zmult_int [symmetric])
  15.100    apply (rule_tac x = "nat k" in exI)
  15.101    apply (cut_tac k = m in int_less_0_conv)
  15.102 -  apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
  15.103 +  apply (auto simp add: zero_le_mult_iff mult_less_0_iff
  15.104      nat_mult_distrib [symmetric] nat_eq_iff2)
  15.105    done
  15.106  
  15.107 @@ -1162,6 +1162,49 @@
  15.108    done
  15.109  
  15.110  
  15.111 +subsection{*Integer Powers*} 
  15.112 +
  15.113 +instance int :: power ..
  15.114 +
  15.115 +primrec
  15.116 +  "p ^ 0 = 1"
  15.117 +  "p ^ (Suc n) = (p::int) * (p ^ n)"
  15.118 +
  15.119 +
  15.120 +instance int :: ringpower
  15.121 +proof
  15.122 +  fix z :: int
  15.123 +  fix n :: nat
  15.124 +  show "z^0 = 1" by simp
  15.125 +  show "z^(Suc n) = z * (z^n)" by simp
  15.126 +qed
  15.127 +
  15.128 +
  15.129 +lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
  15.130 +apply (induct_tac "y", auto)
  15.131 +apply (rule zmod_zmult1_eq [THEN trans])
  15.132 +apply (simp (no_asm_simp))
  15.133 +apply (rule zmod_zmult_distrib [symmetric])
  15.134 +done
  15.135 +
  15.136 +lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
  15.137 +  by (rule Power.power_add)
  15.138 +
  15.139 +lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
  15.140 +  by (rule Power.power_mult [symmetric])
  15.141 +
  15.142 +lemma zero_less_zpower_abs_iff [simp]:
  15.143 +     "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
  15.144 +apply (induct_tac "n")
  15.145 +apply (auto simp add: zero_less_mult_iff)
  15.146 +done
  15.147 +
  15.148 +lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
  15.149 +apply (induct_tac "n")
  15.150 +apply (auto simp add: zero_le_mult_iff)
  15.151 +done
  15.152 +
  15.153 +
  15.154  ML
  15.155  {*
  15.156  val quorem_def = thm "quorem_def";
  15.157 @@ -1264,6 +1307,12 @@
  15.158  val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff";
  15.159  val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff";
  15.160  val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff";
  15.161 +
  15.162 +val zpower_zmod = thm "zpower_zmod";
  15.163 +val zpower_zadd_distrib = thm "zpower_zadd_distrib";
  15.164 +val zpower_zpower = thm "zpower_zpower";
  15.165 +val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
  15.166 +val zero_le_zpower_abs = thm "zero_le_zpower_abs";
  15.167  *}
  15.168  
  15.169  end
    16.1 --- a/src/HOL/Integ/IntPower.thy	Mon Jan 12 16:45:35 2004 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,61 +0,0 @@
    16.4 -(*  Title:	IntPower.thy
    16.5 -    ID:         $Id$
    16.6 -    Author:	Thomas M. Rasmussen
    16.7 -    Copyright	2000  University of Cambridge
    16.8 -
    16.9 -Integer powers 
   16.10 -*)
   16.11 -
   16.12 -theory IntPower = IntDiv:
   16.13 -
   16.14 -instance int :: power ..
   16.15 -
   16.16 -primrec
   16.17 -  power_0:   "p ^ 0 = 1"
   16.18 -  power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)"
   16.19 -
   16.20 -
   16.21 -instance int :: ringpower
   16.22 -proof
   16.23 -  fix z :: int
   16.24 -  fix n :: nat
   16.25 -  show "z^0 = 1" by simp
   16.26 -  show "z^(Suc n) = z * (z^n)" by simp
   16.27 -qed
   16.28 -
   16.29 -
   16.30 -lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
   16.31 -apply (induct_tac "y", auto)
   16.32 -apply (rule zmod_zmult1_eq [THEN trans])
   16.33 -apply (simp (no_asm_simp))
   16.34 -apply (rule zmod_zmult_distrib [symmetric])
   16.35 -done
   16.36 -
   16.37 -lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
   16.38 -  by (rule Power.power_add)
   16.39 -
   16.40 -lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
   16.41 -  by (rule Power.power_mult [symmetric])
   16.42 -
   16.43 -lemma zero_less_zpower_abs_iff [simp]:
   16.44 -     "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
   16.45 -apply (induct_tac "n")
   16.46 -apply (auto simp add: int_0_less_mult_iff)
   16.47 -done
   16.48 -
   16.49 -lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
   16.50 -apply (induct_tac "n")
   16.51 -apply (auto simp add: int_0_le_mult_iff)
   16.52 -done
   16.53 -
   16.54 -ML
   16.55 -{*
   16.56 -val zpower_zmod = thm "zpower_zmod";
   16.57 -val zpower_zadd_distrib = thm "zpower_zadd_distrib";
   16.58 -val zpower_zpower = thm "zpower_zpower";
   16.59 -val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
   16.60 -val zero_le_zpower_abs = thm "zero_le_zpower_abs";
   16.61 -*}
   16.62 -
   16.63 -end
   16.64 -
    17.1 --- a/src/HOL/Integ/NatBin.thy	Mon Jan 12 16:45:35 2004 +0100
    17.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Jan 12 16:51:45 2004 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4  
    17.5  header {* Binary arithmetic for the natural numbers *}
    17.6  
    17.7 -theory NatBin = IntPower:
    17.8 +theory NatBin = IntDiv:
    17.9  
   17.10  text {*
   17.11    Arithmetic for naturals is reduced to that for the non-negative integers.
   17.12 @@ -19,7 +19,7 @@
   17.13       "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
   17.14  
   17.15  
   17.16 -(** nat (coercion from int to nat) **)
   17.17 +subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
   17.18  
   17.19  declare nat_0 [simp] nat_1 [simp]
   17.20  
   17.21 @@ -75,7 +75,7 @@
   17.22  done
   17.23  
   17.24  
   17.25 -(** int (coercion from nat to int) **)
   17.26 +subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   17.27  
   17.28  (*"neg" is used in rewrite rules for binary comparisons*)
   17.29  lemma int_nat_number_of:
   17.30 @@ -284,6 +284,89 @@
   17.31  lemmas numerals = numeral_0_eq_0 numeral_1_eq_1 numeral_2_eq_2
   17.32  
   17.33  
   17.34 +subsection{*General Theorems About Powers Involving Binary Numerals*}
   17.35 +
   17.36 +text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
   17.37 +We cannot prove general results about the numeral @{term "-1"}, so we have to
   17.38 +use @{term "- 1"} instead.*}
   17.39 +
   17.40 +lemma power2_eq_square: "(a::'a::{semiring,ringpower})\<twosuperior> = a * a"
   17.41 +  by (simp add: numeral_2_eq_2 Power.power_Suc)
   17.42 +
   17.43 +lemma [simp]: "(0::'a::{semiring,ringpower})\<twosuperior> = 0"
   17.44 +  by (simp add: power2_eq_square)
   17.45 +
   17.46 +lemma [simp]: "(1::'a::{semiring,ringpower})\<twosuperior> = 1"
   17.47 +  by (simp add: power2_eq_square)
   17.48 +
   17.49 +text{*Squares of literal numerals will be evaluated.*}
   17.50 +declare power2_eq_square [of "number_of w", standard, simp]
   17.51 +
   17.52 +lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_ring,ringpower})"
   17.53 +  by (simp add: power2_eq_square zero_le_square)
   17.54 +
   17.55 +lemma zero_less_power2 [simp]:
   17.56 +     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_ring,ringpower}))"
   17.57 +  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   17.58 +
   17.59 +lemma zero_eq_power2 [simp]:
   17.60 +     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_ring,ringpower}))"
   17.61 +  by (force simp add: power2_eq_square mult_eq_0_iff)
   17.62 +
   17.63 +lemma abs_power2 [simp]:
   17.64 +     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_ring,ringpower})"
   17.65 +  by (simp add: power2_eq_square abs_mult abs_mult_self)
   17.66 +
   17.67 +lemma power2_abs [simp]:
   17.68 +     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_ring,ringpower})"
   17.69 +  by (simp add: power2_eq_square abs_mult_self)
   17.70 +
   17.71 +lemma power2_minus [simp]:
   17.72 +     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{ring,ringpower})"
   17.73 +  by (simp add: power2_eq_square)
   17.74 +
   17.75 +lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{ring,ringpower})"
   17.76 +apply (induct_tac "n")
   17.77 +apply (auto simp add: power_Suc power_add)
   17.78 +done
   17.79 +
   17.80 +lemma power_minus_even [simp]:
   17.81 +     "(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)"
   17.82 +by (simp add: power_minus1_even power_minus [of a]) 
   17.83 +
   17.84 +lemma zero_le_even_power:
   17.85 +     "0 \<le> (a::'a::{ordered_ring,ringpower}) ^ (2*n)"
   17.86 +proof (induct "n")
   17.87 +  case 0
   17.88 +    show ?case by (simp add: zero_le_one)
   17.89 +next
   17.90 +  case (Suc n)
   17.91 +    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   17.92 +      by (simp add: mult_ac power_add power2_eq_square)
   17.93 +    thus ?case
   17.94 +      by (simp add: prems zero_le_square zero_le_mult_iff)
   17.95 +qed
   17.96 +
   17.97 +lemma odd_power_less_zero:
   17.98 +     "(a::'a::{ordered_ring,ringpower}) < 0 ==> a ^ Suc(2*n) < 0"
   17.99 +proof (induct "n")
  17.100 +  case 0
  17.101 +    show ?case by (simp add: Power.power_Suc)
  17.102 +next
  17.103 +  case (Suc n)
  17.104 +    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
  17.105 +      by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
  17.106 +    thus ?case
  17.107 +      by (simp add: prems mult_less_0_iff mult_neg)
  17.108 +qed
  17.109 +
  17.110 +lemma odd_0_le_power_imp_0_le:
  17.111 +     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_ring,ringpower})"
  17.112 +apply (insert odd_power_less_zero [of a n]) 
  17.113 +apply (force simp add: linorder_not_less [symmetric]) 
  17.114 +done
  17.115 +
  17.116 +
  17.117  (** Nat **)
  17.118  
  17.119  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
  17.120 @@ -320,11 +403,6 @@
  17.121  
  17.122  declare diff_less' [of "number_of v", standard, simp]
  17.123  
  17.124 -(** Power **)
  17.125 -
  17.126 -lemma power_two: "(p::nat) ^ 2 = p*p"
  17.127 -by (simp add: numerals)
  17.128 -
  17.129  
  17.130  (*** Comparisons involving (0::nat) ***)
  17.131  
  17.132 @@ -477,9 +555,6 @@
  17.133  lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
  17.134  by (simp add: zpower_zpower mult_commute)
  17.135  
  17.136 -lemma zpower_two: "(p::int) ^ 2 = p*p"
  17.137 -by (simp add: numerals)
  17.138 -
  17.139  lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
  17.140  by (simp add: zpower_even zpower_zadd_distrib)
  17.141  
  17.142 @@ -490,7 +565,7 @@
  17.143  apply (simp only: number_of_add) 
  17.144  apply (rule_tac x = "number_of w" in spec, clarify)
  17.145  apply (case_tac " (0::int) <= x")
  17.146 -apply (auto simp add: nat_mult_distrib zpower_even zpower_two)
  17.147 +apply (auto simp add: nat_mult_distrib zpower_even power2_eq_square)
  17.148  done
  17.149  
  17.150  lemma zpower_number_of_odd:
  17.151 @@ -501,7 +576,7 @@
  17.152  apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
  17.153  apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
  17.154  apply (rule_tac x = "number_of w" in spec, clarify)
  17.155 -apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat)
  17.156 +apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even power2_eq_square neg_nat)
  17.157  done
  17.158  
  17.159  declare zpower_number_of_even [of "number_of v", standard, simp]
  17.160 @@ -569,52 +644,6 @@
  17.161    by (simp add: Let_def)
  17.162  
  17.163  
  17.164 -subsection {*More ML Bindings*}
  17.165 -
  17.166 -ML
  17.167 -{*
  17.168 -val eq_nat_nat_iff = thm"eq_nat_nat_iff";
  17.169 -val eq_nat_number_of = thm"eq_nat_number_of";
  17.170 -val less_nat_number_of = thm"less_nat_number_of";
  17.171 -val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less";
  17.172 -val Suc_pred' = thm"Suc_pred'";
  17.173 -val expand_Suc = thm"expand_Suc";
  17.174 -val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
  17.175 -val add_eq_if = thm"add_eq_if";
  17.176 -val mult_eq_if = thm"mult_eq_if";
  17.177 -val power_eq_if = thm"power_eq_if";
  17.178 -val diff_less' = thm"diff_less'";
  17.179 -val power_two = thm"power_two";
  17.180 -val eq_number_of_0 = thm"eq_number_of_0";
  17.181 -val eq_0_number_of = thm"eq_0_number_of";
  17.182 -val less_0_number_of = thm"less_0_number_of";
  17.183 -val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
  17.184 -val eq_number_of_Suc = thm"eq_number_of_Suc";
  17.185 -val Suc_eq_number_of = thm"Suc_eq_number_of";
  17.186 -val less_number_of_Suc = thm"less_number_of_Suc";
  17.187 -val less_Suc_number_of = thm"less_Suc_number_of";
  17.188 -val le_number_of_Suc = thm"le_number_of_Suc";
  17.189 -val le_Suc_number_of = thm"le_Suc_number_of";
  17.190 -val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
  17.191 -val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
  17.192 -val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
  17.193 -val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
  17.194 -val nat_power_eq = thm"nat_power_eq";
  17.195 -val power_nat_number_of = thm"power_nat_number_of";
  17.196 -val zpower_even = thm"zpower_even";
  17.197 -val zpower_two = thm"zpower_two";
  17.198 -val zpower_odd = thm"zpower_odd";
  17.199 -val zpower_number_of_even = thm"zpower_number_of_even";
  17.200 -val zpower_number_of_odd = thm"zpower_number_of_odd";
  17.201 -val nat_number_of_Pls = thm"nat_number_of_Pls";
  17.202 -val nat_number_of_Min = thm"nat_number_of_Min";
  17.203 -val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
  17.204 -val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
  17.205 -val Let_Suc = thm"Let_Suc";
  17.206 -
  17.207 -val nat_number = thms"nat_number";
  17.208 -*}
  17.209 -
  17.210  subsection {*Lemmas for the Combination and Cancellation Simprocs*}
  17.211  
  17.212  lemma nat_number_of_add_left:
  17.213 @@ -697,8 +726,61 @@
  17.214       "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
  17.215  by (simp add: nat_mult_div_cancel1)
  17.216  
  17.217 +
  17.218  ML
  17.219  {*
  17.220 +val eq_nat_nat_iff = thm"eq_nat_nat_iff";
  17.221 +val eq_nat_number_of = thm"eq_nat_number_of";
  17.222 +val less_nat_number_of = thm"less_nat_number_of";
  17.223 +val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less";
  17.224 +val power2_eq_square = thm "power2_eq_square";
  17.225 +val zero_le_power2 = thm "zero_le_power2";
  17.226 +val zero_less_power2 = thm "zero_less_power2";
  17.227 +val zero_eq_power2 = thm "zero_eq_power2";
  17.228 +val abs_power2 = thm "abs_power2";
  17.229 +val power2_abs = thm "power2_abs";
  17.230 +val power2_minus = thm "power2_minus";
  17.231 +val power_minus1_even = thm "power_minus1_even";
  17.232 +val power_minus_even = thm "power_minus_even";
  17.233 +val zero_le_even_power = thm "zero_le_even_power";
  17.234 +val odd_power_less_zero = thm "odd_power_less_zero";
  17.235 +val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le";
  17.236 +
  17.237 +val Suc_pred' = thm"Suc_pred'";
  17.238 +val expand_Suc = thm"expand_Suc";
  17.239 +val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
  17.240 +val add_eq_if = thm"add_eq_if";
  17.241 +val mult_eq_if = thm"mult_eq_if";
  17.242 +val power_eq_if = thm"power_eq_if";
  17.243 +val diff_less' = thm"diff_less'";
  17.244 +val eq_number_of_0 = thm"eq_number_of_0";
  17.245 +val eq_0_number_of = thm"eq_0_number_of";
  17.246 +val less_0_number_of = thm"less_0_number_of";
  17.247 +val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
  17.248 +val eq_number_of_Suc = thm"eq_number_of_Suc";
  17.249 +val Suc_eq_number_of = thm"Suc_eq_number_of";
  17.250 +val less_number_of_Suc = thm"less_number_of_Suc";
  17.251 +val less_Suc_number_of = thm"less_Suc_number_of";
  17.252 +val le_number_of_Suc = thm"le_number_of_Suc";
  17.253 +val le_Suc_number_of = thm"le_Suc_number_of";
  17.254 +val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
  17.255 +val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
  17.256 +val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
  17.257 +val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
  17.258 +val nat_power_eq = thm"nat_power_eq";
  17.259 +val power_nat_number_of = thm"power_nat_number_of";
  17.260 +val zpower_even = thm"zpower_even";
  17.261 +val zpower_odd = thm"zpower_odd";
  17.262 +val zpower_number_of_even = thm"zpower_number_of_even";
  17.263 +val zpower_number_of_odd = thm"zpower_number_of_odd";
  17.264 +val nat_number_of_Pls = thm"nat_number_of_Pls";
  17.265 +val nat_number_of_Min = thm"nat_number_of_Min";
  17.266 +val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
  17.267 +val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
  17.268 +val Let_Suc = thm"Let_Suc";
  17.269 +
  17.270 +val nat_number = thms"nat_number";
  17.271 +
  17.272  val nat_number_of_add_left = thm"nat_number_of_add_left";
  17.273  val left_add_mult_distrib = thm"left_add_mult_distrib";
  17.274  val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
  17.275 @@ -717,6 +799,10 @@
  17.276  val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj";
  17.277  val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
  17.278  val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
  17.279 +
  17.280 +val power_minus1_even = thm"power_minus1_even";
  17.281 +val power_minus_even = thm"power_minus_even";
  17.282 +val zero_le_even_power = thm"zero_le_even_power";
  17.283  *}
  17.284  
  17.285  
    18.1 --- a/src/HOL/Integ/NatSimprocs.thy	Mon Jan 12 16:45:35 2004 +0100
    18.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Mon Jan 12 16:51:45 2004 +0100
    18.3 @@ -152,7 +152,8 @@
    18.4  declare zero_le_divide_iff [of "number_of w", standard, simp]
    18.5  declare divide_le_0_iff [of "number_of w", standard, simp]
    18.6  
    18.7 -(*Replaces "inverse #nn" by 1/#nn *)
    18.8 +(*Replaces "inverse #nn" by 1/#nn.  It looks strange, but then other simprocs
    18.9 +simplify the quotient.*)
   18.10  declare inverse_eq_divide [of "number_of w", standard, simp]
   18.11  
   18.12  text{*These laws simplify inequalities, moving unary minus from a term
    19.1 --- a/src/HOL/Integ/Presburger.thy	Mon Jan 12 16:45:35 2004 +0100
    19.2 +++ b/src/HOL/Integ/Presburger.thy	Mon Jan 12 16:51:45 2004 +0100
    19.3 @@ -883,7 +883,7 @@
    19.4  next
    19.5    assume ?Q
    19.6    hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
    19.7 -  with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
    19.8 +  with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
    19.9    thus ?P by(simp)
   19.10  qed
   19.11  
    20.1 --- a/src/HOL/Integ/presburger.ML	Mon Jan 12 16:45:35 2004 +0100
    20.2 +++ b/src/HOL/Integ/presburger.ML	Mon Jan 12 16:51:45 2004 +0100
    20.3 @@ -184,7 +184,7 @@
    20.4        addcongs [conj_le_cong, imp_le_cong]
    20.5      (* simp rules for elimination of abs *)
    20.6  
    20.7 -    val simpset3 = HOL_basic_ss addsplits [zabs_split]
    20.8 +    val simpset3 = HOL_basic_ss addsplits [abs_split]
    20.9  	      
   20.10      val ct = cterm_of sg (HOLogic.mk_Trueprop t)
   20.11  
    21.1 --- a/src/HOL/IsaMakefile	Mon Jan 12 16:45:35 2004 +0100
    21.2 +++ b/src/HOL/IsaMakefile	Mon Jan 12 16:51:45 2004 +0100
    21.3 @@ -87,8 +87,7 @@
    21.4    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
    21.5    Integ/cooper_dec.ML Integ/cooper_proof.ML \
    21.6    Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
    21.7 -  Integ/IntDiv.thy Integ/IntPower.thy \
    21.8 -  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
    21.9 +  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
   21.10    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   21.11    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   21.12    Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
   21.13 @@ -144,7 +143,6 @@
   21.14    Real/PRat.ML Real/PRat.thy \
   21.15    Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
   21.16    Real/ROOT.ML Real/Real.thy \
   21.17 -  Real/RealArith0.thy Real/real_arith0.ML \
   21.18    Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
   21.19    Real/RealBin.thy Real/RealDef.thy \
   21.20    Real/RealInt.thy Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
   21.21 @@ -152,8 +150,7 @@
   21.22    Hyperreal/Fact.ML Hyperreal/Fact.thy\
   21.23    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
   21.24    Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
   21.25 -  Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
   21.26 -  Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
   21.27 +  Hyperreal/HyperArith.thy Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
   21.28    Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   21.29    Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   21.30    Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
   21.31 @@ -164,7 +161,6 @@
   21.32    Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
   21.33    Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
   21.34    Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
   21.35 -  Hyperreal/hypreal_arith0.ML\
   21.36    Complex/Complex_Main.thy\
   21.37    Complex/CLim.ML Complex/CLim.thy\
   21.38    Complex/CSeries.ML Complex/CSeries.thy\
    22.1 --- a/src/HOL/Library/Primes.thy	Mon Jan 12 16:45:35 2004 +0100
    22.2 +++ b/src/HOL/Library/Primes.thy	Mon Jan 12 16:51:45 2004 +0100
    22.3 @@ -200,7 +200,7 @@
    22.4    by (auto dest: prime_dvd_mult)
    22.5  
    22.6  lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
    22.7 -  by (rule prime_dvd_square) (simp_all add: power_two)
    22.8 +  by (rule prime_dvd_square) (simp_all add: power2_eq_square)
    22.9  
   22.10  
   22.11  text {* \medskip Addition laws *}
    23.1 --- a/src/HOL/Library/Rational_Numbers.thy	Mon Jan 12 16:45:35 2004 +0100
    23.2 +++ b/src/HOL/Library/Rational_Numbers.thy	Mon Jan 12 16:51:45 2004 +0100
    23.3 @@ -1,7 +1,7 @@
    23.4 -(*  Title:      HOL/Library/Rational_Numbers.thy
    23.5 -    ID:         $Id$
    23.6 -    Author:     Markus Wenzel, TU Muenchen
    23.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    23.8 +(*  Title: HOL/Library/Rational_Numbers.thy
    23.9 +    ID:    $Id$
   23.10 +    Author: Markus Wenzel, TU Muenchen
   23.11 +    License: GPL (GNU GENERAL PUBLIC LICENSE)
   23.12  *)
   23.13  
   23.14  header {*
   23.15 @@ -85,7 +85,7 @@
   23.16        next
   23.17          assume a': "a' \<noteq> 0"
   23.18          from eq1 eq2 have "(a * b') * (a' * b'') = (a' * b) * (a'' * b')" by simp
   23.19 -        hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: zmult_ac)
   23.20 +        hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: mult_ac)
   23.21          with a' b' show ?thesis by simp
   23.22        qed
   23.23        thus "fract a b \<sim> fract a'' b''" ..
   23.24 @@ -152,11 +152,11 @@
   23.25        (is "?lhs = ?rhs")
   23.26      proof -
   23.27        have "?lhs = (a * b') * (d * d') + (c * d') * (b * b')"
   23.28 -        by (simp add: int_distrib zmult_ac)
   23.29 +        by (simp add: int_distrib mult_ac)
   23.30        also have "... = (a' * b) * (d * d') + (c' * d) * (b * b')"
   23.31          by (simp only: eq1 eq2)
   23.32        also have "... = ?rhs"
   23.33 -        by (simp add: int_distrib zmult_ac)
   23.34 +        by (simp add: int_distrib mult_ac)
   23.35        finally show "?lhs = ?rhs" .
   23.36      qed
   23.37      from neq show "b * d \<noteq> 0" by simp
   23.38 @@ -188,7 +188,7 @@
   23.39    have "\<lfloor>fract (a * c) (b * d)\<rfloor> = \<lfloor>fract (a' * c') (b' * d')\<rfloor>"
   23.40    proof
   23.41      from eq1 eq2 have "(a * b') * (c * d') = (a' * b) * (c' * d)" by simp
   23.42 -    thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: zmult_ac)
   23.43 +    thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: mult_ac)
   23.44      from neq show "b * d \<noteq> 0" by simp
   23.45      from neq show "b' * d' \<noteq> 0" by simp
   23.46    qed
   23.47 @@ -206,7 +206,7 @@
   23.48    with neq obtain "a \<noteq> 0" and "a' \<noteq> 0" by (simp add: is_zero_fraction_iff)
   23.49    assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>"
   23.50    hence "a * b' = a' * b" ..
   23.51 -  hence "b * a' = b' * a" by (simp only: zmult_ac)
   23.52 +  hence "b * a' = b' * a" by (simp only: mult_ac)
   23.53    hence "\<lfloor>fract b a\<rfloor> = \<lfloor>fract b' a'\<rfloor>" ..
   23.54    with neq show ?thesis by (simp add: inverse_fraction_def)
   23.55  qed
   23.56 @@ -225,12 +225,12 @@
   23.57      fix a b c d x :: int assume x: "x \<noteq> 0"
   23.58      have "?le a b c d = ?le (a * x) (b * x) c d"
   23.59      proof -
   23.60 -      from x have "0 < x * x" by (auto simp add: int_less_le)
   23.61 +      from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
   23.62        hence "?le a b c d =
   23.63            ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   23.64 -        by (simp add: zmult_zle_cancel2)
   23.65 +        by (simp add: mult_le_cancel_right)
   23.66        also have "... = ?le (a * x) (b * x) c d"
   23.67 -        by (simp add: zmult_ac)
   23.68 +        by (simp add: mult_ac)
   23.69        finally show ?thesis .
   23.70      qed
   23.71    } note le_factor = this
   23.72 @@ -241,11 +241,11 @@
   23.73    hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   23.74      by (rule le_factor)
   23.75    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
   23.76 -    by (simp add: zmult_ac)
   23.77 +    by (simp add: mult_ac)
   23.78    also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   23.79      by (simp only: eq1 eq2)
   23.80    also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   23.81 -    by (simp add: zmult_ac)
   23.82 +    by (simp add: mult_ac)
   23.83    also from D have "... = ?le a' b' c' d'"
   23.84      by (rule le_factor [symmetric])
   23.85    finally have "?le a b c d = ?le a' b' c' d'" .
   23.86 @@ -470,14 +470,15 @@
   23.87  
   23.88  theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   23.89    by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
   23.90 -    (auto simp add: zmult_less_0_iff int_0_less_mult_iff int_le_less split: zabs_split)
   23.91 +     (auto simp add: mult_less_0_iff zero_less_mult_iff int_le_less 
   23.92 +                split: abs_split)
   23.93  
   23.94  
   23.95  subsubsection {* The ordered field of rational numbers *}
   23.96  
   23.97  lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
   23.98    by (induct q, induct r, induct s) 
   23.99 -     (simp add: add_rat zadd_ac zmult_ac int_distrib)
  23.100 +     (simp add: add_rat add_ac mult_ac int_distrib)
  23.101  
  23.102  lemma rat_add_0: "0 + q = (q::rat)"
  23.103    by (induct q) (simp add: zero_rat add_rat)
  23.104 @@ -492,7 +493,7 @@
  23.105    show "(q + r) + s = q + (r + s)"
  23.106      by (rule rat_add_assoc)
  23.107    show "q + r = r + q"
  23.108 -    by (induct q, induct r) (simp add: add_rat zadd_ac zmult_ac)
  23.109 +    by (induct q, induct r) (simp add: add_rat add_ac mult_ac)
  23.110    show "0 + q = q"
  23.111      by (induct q) (simp add: zero_rat add_rat)
  23.112    show "(-q) + q = 0"
  23.113 @@ -500,9 +501,9 @@
  23.114    show "q - r = q + (-r)"
  23.115      by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
  23.116    show "(q * r) * s = q * (r * s)"
  23.117 -    by (induct q, induct r, induct s) (simp add: mult_rat zmult_ac)
  23.118 +    by (induct q, induct r, induct s) (simp add: mult_rat mult_ac)
  23.119    show "q * r = r * q"
  23.120 -    by (induct q, induct r) (simp add: mult_rat zmult_ac)
  23.121 +    by (induct q, induct r) (simp add: mult_rat mult_ac)
  23.122    show "1 * q = q"
  23.123      by (induct q) (simp add: one_rat mult_rat)
  23.124    show "(q + r) * s = q * s + r * s"
  23.125 @@ -533,25 +534,25 @@
  23.126        show "Fract a b \<le> Fract e f"
  23.127        proof -
  23.128          from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
  23.129 -          by (auto simp add: int_less_le)
  23.130 +          by (auto simp add: zero_less_mult_iff linorder_neq_iff)
  23.131          have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)"
  23.132          proof -
  23.133            from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
  23.134              by (simp add: le_rat)
  23.135 -          with ff show ?thesis by (simp add: zmult_zle_cancel2)
  23.136 +          with ff show ?thesis by (simp add: mult_le_cancel_right)
  23.137          qed
  23.138          also have "... = (c * f) * (d * f) * (b * b)"
  23.139 -          by (simp only: zmult_ac)
  23.140 +          by (simp only: mult_ac)
  23.141          also have "... \<le> (e * d) * (d * f) * (b * b)"
  23.142          proof -
  23.143            from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
  23.144              by (simp add: le_rat)
  23.145 -          with bb show ?thesis by (simp add: zmult_zle_cancel2)
  23.146 +          with bb show ?thesis by (simp add: mult_le_cancel_right)
  23.147          qed
  23.148          finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
  23.149 -          by (simp only: zmult_ac)
  23.150 +          by (simp only: mult_ac)
  23.151          with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
  23.152 -          by (simp add: zmult_zle_cancel2)
  23.153 +          by (simp add: mult_le_cancel_right)
  23.154          with neq show ?thesis by (simp add: le_rat)
  23.155        qed
  23.156      qed
  23.157 @@ -570,7 +571,7 @@
  23.158          proof -
  23.159            from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
  23.160              by (simp add: le_rat)
  23.161 -          thus ?thesis by (simp only: zmult_ac)
  23.162 +          thus ?thesis by (simp only: mult_ac)
  23.163          qed
  23.164          finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
  23.165          moreover from neq have "b * d \<noteq> 0" by simp
  23.166 @@ -584,7 +585,7 @@
  23.167      show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
  23.168        by (simp only: less_rat_def)
  23.169      show "q \<le> r \<or> r \<le> q"
  23.170 -      by (induct q, induct r) (simp add: le_rat zmult_ac, arith)
  23.171 +      by (induct q, induct r) (simp add: le_rat mult_ac, arith)
  23.172    }
  23.173  qed
  23.174  
  23.175 @@ -601,12 +602,12 @@
  23.176      show "Fract e f + Fract a b \<le> Fract e f + Fract c d"
  23.177      proof -
  23.178        let ?F = "f * f" from neq have F: "0 < ?F"
  23.179 -        by (auto simp add: int_less_le)
  23.180 +        by (auto simp add: zero_less_mult_iff)
  23.181        from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
  23.182          by (simp add: le_rat)
  23.183        with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
  23.184 -        by (simp add: zmult_zle_cancel2)
  23.185 -      with neq show ?thesis by (simp add: add_rat le_rat zmult_ac int_distrib)
  23.186 +        by (simp add: mult_le_cancel_right)
  23.187 +      with neq show ?thesis by (simp add: add_rat le_rat mult_ac int_distrib)
  23.188      qed
  23.189    qed
  23.190    show "q < r ==> 0 < s ==> s * q < s * r"
  23.191 @@ -621,13 +622,13 @@
  23.192        from neq gt have "0 < ?E"
  23.193          by (auto simp add: zero_rat less_rat le_rat int_less_le eq_rat)
  23.194        moreover from neq have "0 < ?F"
  23.195 -        by (auto simp add: int_less_le)
  23.196 +        by (auto simp add: zero_less_mult_iff)
  23.197        moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
  23.198          by (simp add: less_rat)
  23.199        ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
  23.200 -        by (simp add: zmult_zless_cancel2)
  23.201 +        by (simp add: mult_less_cancel_right)
  23.202        with neq show ?thesis
  23.203 -        by (simp add: less_rat mult_rat zmult_ac)
  23.204 +        by (simp add: less_rat mult_rat mult_ac)
  23.205      qed
  23.206    qed
  23.207    show "\<bar>q\<bar> = (if q < 0 then -q else q)"
    24.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Jan 12 16:45:35 2004 +0100
    24.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Mon Jan 12 16:51:45 2004 +0100
    24.3 @@ -75,7 +75,7 @@
    24.4  lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
    24.5    apply (induct n)
    24.6     apply auto
    24.7 -  apply (simp add: int_0_less_mult_iff)
    24.8 +  apply (simp add: zero_less_mult_iff)
    24.9    done
   24.10  
   24.11  lemma funprod_zgcd [rule_format (no_asm)]:
    25.1 --- a/src/HOL/NumberTheory/Gauss.thy	Mon Jan 12 16:45:35 2004 +0100
    25.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Mon Jan 12 16:51:45 2004 +0100
    25.3 @@ -180,7 +180,7 @@
    25.4  
    25.5  lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
    25.6    apply (insert a_nonzero)
    25.7 -by (auto simp add: B_def zmult_pos A_greater_zero)
    25.8 +by (auto simp add: B_def mult_pos A_greater_zero)
    25.9  
   25.10  lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)";
   25.11    apply (auto simp add: C_def)
    26.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 12 16:45:35 2004 +0100
    26.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 12 16:51:45 2004 +0100
    26.3 @@ -126,7 +126,7 @@
    26.4  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
    26.5    by (simp del: zmult_zminus_right
    26.6        add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
    26.7 -          zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
    26.8 +          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
    26.9  
   26.10  lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
   26.11    by (simp add: zabs_def zgcd_zmult_distrib2)
   26.12 @@ -144,7 +144,7 @@
   26.13       "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
   26.14    apply (subgoal_tac "m = zgcd (m * n, m * k)")
   26.15     apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
   26.16 -   apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
   26.17 +   apply (simp_all add: zgcd_zmult_distrib2 [symmetric] zero_le_mult_iff)
   26.18    done
   26.19  
   26.20  lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
   26.21 @@ -363,7 +363,7 @@
   26.22      "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
   26.23    apply (unfold zcong_def dvd_def, auto)
   26.24    apply (subgoal_tac "0 < m")
   26.25 -   apply (simp add: int_0_le_mult_iff)
   26.26 +   apply (simp add: zero_le_mult_iff)
   26.27     apply (subgoal_tac "m * k < m * 1")
   26.28      apply (drule zmult_zless_cancel1 [THEN iffD1])
   26.29      apply (auto simp add: linorder_neq_iff)
    27.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Jan 12 16:45:35 2004 +0100
    27.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Mon Jan 12 16:51:45 2004 +0100
    27.3 @@ -130,7 +130,7 @@
    27.4          then have "0 \<le> x";
    27.5            by (auto simp add: A_def)
    27.6          with a_nonzero have "0 \<le> x * a";
    27.7 -          by (auto simp add: int_0_le_mult_iff)
    27.8 +          by (auto simp add: zero_le_mult_iff)
    27.9          with p_g_2 show "0 \<le> x * a div p"; 
   27.10            by (auto simp add: pos_imp_zdiv_nonneg_iff)
   27.11        qed;
    28.1 --- a/src/HOL/Power.thy	Mon Jan 12 16:45:35 2004 +0100
    28.2 +++ b/src/HOL/Power.thy	Mon Jan 12 16:51:45 2004 +0100
    28.3 @@ -153,6 +153,12 @@
    28.4  lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
    28.5  by force
    28.6  
    28.7 +lemma nonzero_power_inverse:
    28.8 +  "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"
    28.9 +apply (induct_tac "n")
   28.10 +apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
   28.11 +done
   28.12 +
   28.13  text{*Perhaps these should be simprules.*}
   28.14  lemma power_inverse:
   28.15    "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
   28.16 @@ -160,11 +166,38 @@
   28.17  apply (auto simp add: power_Suc inverse_mult_distrib)
   28.18  done
   28.19  
   28.20 +lemma nonzero_power_divide: 
   28.21 +    "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
   28.22 +by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
   28.23 +
   28.24 +lemma power_divide: 
   28.25 +    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
   28.26 +apply (case_tac "b=0", simp add: power_0_left)
   28.27 +apply (rule nonzero_power_divide) 
   28.28 +apply assumption 
   28.29 +done
   28.30 +
   28.31  lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
   28.32  apply (induct_tac "n")
   28.33  apply (auto simp add: power_Suc abs_mult)
   28.34  done
   28.35  
   28.36 +lemma zero_less_power_abs_iff [simp]:
   28.37 +     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" 
   28.38 +proof (induct "n")
   28.39 +  case 0
   28.40 +    show ?case by (simp add: zero_less_one)
   28.41 +next
   28.42 +  case (Suc n)
   28.43 +    show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
   28.44 +qed
   28.45 +
   28.46 +lemma zero_le_power_abs [simp]:
   28.47 +     "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n"
   28.48 +apply (induct_tac "n")
   28.49 +apply (auto simp add: zero_le_one zero_le_power)
   28.50 +done
   28.51 +
   28.52  lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
   28.53  proof -
   28.54    have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
   28.55 @@ -413,7 +446,11 @@
   28.56  val field_power_eq_0_iff = thm"field_power_eq_0_iff";
   28.57  val field_power_not_zero = thm"field_power_not_zero";
   28.58  val power_inverse = thm"power_inverse";
   28.59 +val nonzero_power_divide = thm"nonzero_power_divide";
   28.60 +val power_divide = thm"power_divide";
   28.61  val power_abs = thm"power_abs";
   28.62 +val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
   28.63 +val zero_le_power_abs = thm "zero_le_power_abs";
   28.64  val power_minus = thm"power_minus";
   28.65  val power_Suc_less = thm"power_Suc_less";
   28.66  val power_strict_decreasing = thm"power_strict_decreasing";
    29.1 --- a/src/HOL/Presburger.thy	Mon Jan 12 16:45:35 2004 +0100
    29.2 +++ b/src/HOL/Presburger.thy	Mon Jan 12 16:51:45 2004 +0100
    29.3 @@ -883,7 +883,7 @@
    29.4  next
    29.5    assume ?Q
    29.6    hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
    29.7 -  with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
    29.8 +  with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
    29.9    thus ?P by(simp)
   29.10  qed
   29.11  
    30.1 --- a/src/HOL/Ring_and_Field.thy	Mon Jan 12 16:45:35 2004 +0100
    30.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Jan 12 16:51:45 2004 +0100
    30.3 @@ -7,13 +7,11 @@
    30.4  
    30.5  header {*
    30.6    \title{Ring and field structures}
    30.7 -  \author{Gertrud Bauer and Markus Wenzel}
    30.8 +  \author{Gertrud Bauer, L. C. Paulson and Markus Wenzel}
    30.9  *}
   30.10  
   30.11  theory Ring_and_Field = Inductive:
   30.12  
   30.13 -text{*Lemmas and extension to semirings by L. C. Paulson*}
   30.14 -
   30.15  subsection {* Abstract algebraic structures *}
   30.16  
   30.17  axclass semiring \<subseteq> zero, one, plus, times
   30.18 @@ -167,14 +165,14 @@
   30.19  
   30.20  theorems mult_ac = mult_assoc mult_commute mult_left_commute
   30.21  
   30.22 -lemma mult_left_zero [simp]: "0 * a = (0::'a::semiring)"
   30.23 +lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring)"
   30.24  proof -
   30.25    have "0*a + 0*a = 0*a + 0"
   30.26      by (simp add: left_distrib [symmetric])
   30.27    thus ?thesis by (simp only: add_left_cancel)
   30.28  qed
   30.29  
   30.30 -lemma mult_right_zero [simp]: "a * 0 = (0::'a::semiring)"
   30.31 +lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring)"
   30.32    by (simp add: mult_commute)
   30.33  
   30.34  
   30.35 @@ -1333,6 +1331,39 @@
   30.36  apply (simp add: divide_inverse_zero field_mult_cancel_left) 
   30.37  done
   30.38  
   30.39 +subsection {* Division and the Number One *}
   30.40 +
   30.41 +text{*Simplify expressions equated with 1*}
   30.42 +lemma divide_eq_1_iff [simp]:
   30.43 +     "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   30.44 +apply (case_tac "b=0", simp) 
   30.45 +apply (simp add: right_inverse_eq) 
   30.46 +done
   30.47 +
   30.48 +
   30.49 +lemma one_eq_divide_iff [simp]:
   30.50 +     "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   30.51 +by (simp add: eq_commute [of 1])  
   30.52 +
   30.53 +lemma zero_eq_1_divide_iff [simp]:
   30.54 +     "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
   30.55 +apply (case_tac "a=0", simp) 
   30.56 +apply (auto simp add: nonzero_eq_divide_eq) 
   30.57 +done
   30.58 +
   30.59 +lemma one_divide_eq_0_iff [simp]:
   30.60 +     "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
   30.61 +apply (case_tac "a=0", simp) 
   30.62 +apply (insert zero_neq_one [THEN not_sym]) 
   30.63 +apply (auto simp add: nonzero_divide_eq_eq) 
   30.64 +done
   30.65 +
   30.66 +text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
   30.67 +declare zero_less_divide_iff [of "1", simp]
   30.68 +declare divide_less_0_iff [of "1", simp]
   30.69 +declare zero_le_divide_iff [of "1", simp]
   30.70 +declare divide_le_0_iff [of "1", simp]
   30.71 +
   30.72  
   30.73  subsection {* Ordering Rules for Division *}
   30.74  
   30.75 @@ -1413,7 +1444,6 @@
   30.76                    minus_mult_left [symmetric] minus_mult_right [symmetric])  
   30.77  done
   30.78  
   30.79 -
   30.80  lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
   30.81  by (simp add: abs_if) 
   30.82  
   30.83 @@ -1571,8 +1601,8 @@
   30.84  val mult_1 = thm"mult_1";
   30.85  val mult_1_right = thm"mult_1_right";
   30.86  val mult_left_commute = thm"mult_left_commute";
   30.87 -val mult_left_zero = thm"mult_left_zero";
   30.88 -val mult_right_zero = thm"mult_right_zero";
   30.89 +val mult_zero_left = thm"mult_zero_left";
   30.90 +val mult_zero_right = thm"mult_zero_right";
   30.91  val left_distrib = thm "left_distrib";
   30.92  val right_distrib = thm"right_distrib";
   30.93  val combine_common_factor = thm"combine_common_factor";
    31.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Mon Jan 12 16:45:35 2004 +0100
    31.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Mon Jan 12 16:51:45 2004 +0100
    31.3 @@ -184,7 +184,7 @@
    31.4        addcongs [conj_le_cong, imp_le_cong]
    31.5      (* simp rules for elimination of abs *)
    31.6  
    31.7 -    val simpset3 = HOL_basic_ss addsplits [zabs_split]
    31.8 +    val simpset3 = HOL_basic_ss addsplits [abs_split]
    31.9  	      
   31.10      val ct = cterm_of sg (HOLogic.mk_Trueprop t)
   31.11  
    32.1 --- a/src/HOL/ex/PresburgerEx.thy	Mon Jan 12 16:45:35 2004 +0100
    32.2 +++ b/src/HOL/ex/PresburgerEx.thy	Mon Jan 12 16:51:45 2004 +0100
    32.3 @@ -8,79 +8,86 @@
    32.4  
    32.5  theory PresburgerEx = Main:
    32.6  
    32.7 -theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x"
    32.8 +theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
    32.9    by presburger
   32.10  
   32.11  theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
   32.12 -  (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
   32.13 +  (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
   32.14    by presburger
   32.15  
   32.16  theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
   32.17 -  2 dvd (y::int) ==> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
   32.18 +  2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
   32.19    by presburger
   32.20  
   32.21 -theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x ";
   32.22 +theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x ";
   32.23    by presburger
   32.24  
   32.25 -theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2";
   32.26 +text{*Very slow: about 55 seconds on a 1.8GHz machine.*}
   32.27 +theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2";
   32.28    by presburger
   32.29  
   32.30 -theorem "EX (x::int). 0 < x" by presburger
   32.31 +theorem "\<exists>(x::int). 0 < x" by presburger
   32.32  
   32.33 -theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
   32.34 +theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
   32.35   
   32.36 -theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger
   32.37 +theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" by presburger
   32.38   
   32.39  theorem
   32.40 -   "EX (x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1" by presburger
   32.41 +   "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1" by presburger
   32.42  
   32.43 -theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
   32.44 +theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
   32.45    by presburger
   32.46  
   32.47 -theorem "ALL (x::int). b < x --> a <= x"
   32.48 +theorem "\<forall>(x::int). b < x --> a \<le> x"
   32.49    apply (presburger no_quantify)
   32.50    oops
   32.51  
   32.52 -theorem "ALL (x::int). b < x --> a <= x"
   32.53 +theorem "\<forall>(x::int). b < x --> a \<le> x"
   32.54    apply (presburger no_quantify)
   32.55    oops
   32.56  
   32.57 -theorem "~ (EX (x::int). False)"
   32.58 +theorem "~ (\<exists>(x::int). False)"
   32.59    by presburger
   32.60  
   32.61 -theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x"
   32.62 +theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
   32.63    apply (presburger no_quantify)
   32.64    oops
   32.65  
   32.66 -theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger 
   32.67 +theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger 
   32.68  
   32.69 -theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger 
   32.70 +theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger 
   32.71  
   32.72 -theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger 
   32.73 +theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" by presburger 
   32.74    
   32.75 -theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger 
   32.76 +theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger 
   32.77 +
   32.78 +theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger 
   32.79  
   32.80 -theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger 
   32.81 -
   32.82 -theorem "~ (ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y+1))| (EX (q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
   32.83 +theorem "~ (\<forall>(x::int). 
   32.84 +            ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | 
   32.85 +             (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
   32.86 +             --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
   32.87    by presburger
   32.88   
   32.89  theorem 
   32.90 -   "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
   32.91 +   "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
   32.92    by presburger
   32.93  
   32.94  theorem
   32.95 -    "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger
   32.96 +    "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" 
   32.97 +  by presburger
   32.98     
   32.99  theorem
  32.100 -   "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" by presburger
  32.101 +   "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
  32.102 +  by presburger
  32.103  
  32.104  theorem
  32.105 -   "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
  32.106 +   "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
  32.107    by presburger
  32.108  
  32.109 -theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
  32.110 +text{*Very slow: about 80 seconds on a 1.8GHz machine.*}
  32.111 +theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
  32.112  
  32.113 -theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
  32.114 +theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
  32.115  
  32.116  end
  32.117 \ No newline at end of file
    33.1 --- a/src/HOL/ex/set.thy	Mon Jan 12 16:45:35 2004 +0100
    33.2 +++ b/src/HOL/ex/set.thy	Mon Jan 12 16:51:45 2004 +0100
    33.3 @@ -156,8 +156,9 @@
    33.4  
    33.5  lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
    33.6      \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
    33.7 -  -- {* Example 8. *}
    33.8 -  by force  -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
    33.9 +  -- {* Example 8 now needs a small hint. *}
   33.10 +  by (simp add: abs_if, force)
   33.11 +    -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
   33.12  
   33.13  text {* Example 9 omitted (requires the reals). *}
   33.14