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
--- a/doc-src/TutorialI/Documents/Documents.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Mon Jan 12 16:51:45 2004 +0100
@@ -763,13 +763,13 @@
*}
lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
- by (auto(*<*)simp add: int_less_le(*>*))
+ by (auto(*<*)simp add: zero_less_mult_iff(*>*))
text {*
\noindent Here the real source of the proof has been as follows:
\begin{verbatim}
- by (auto(*<*)simp add: int_less_le(*>*))
+ by (auto(*<*)simp add: zero_less_mult_iff(*>*))
\end{verbatim}
%(*
--- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 12 16:51:45 2004 +0100
@@ -799,7 +799,7 @@
\noindent Here the real source of the proof has been as follows:
\begin{verbatim}
- by (auto(*<*)simp add: int_less_le(*>*))
+ by (auto(*<*)simp add: zero_less_mult_iff(*>*))
\end{verbatim}
%(*
--- a/doc-src/TutorialI/Types/Numbers.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Mon Jan 12 16:51:45 2004 +0100
@@ -197,14 +197,11 @@
text {*REALS
-@{thm[display] realpow_abs[no_vars]}
-\rulename{realpow_abs}
-
@{thm[display] dense[no_vars]}
\rulename{dense}
-@{thm[display] realpow_abs[no_vars]}
-\rulename{realpow_abs}
+@{thm[display] power_abs[no_vars]}
+\rulename{power_abs}
@{thm[display] times_divide_eq_right[no_vars]}
\rulename{times_divide_eq_right}
--- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Jan 12 16:51:45 2004 +0100
@@ -320,19 +320,14 @@
REALS
\begin{isabelle}%
-{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
-\end{isabelle}
-\rulename{realpow_abs}
-
-\begin{isabelle}%
a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
\end{isabelle}
\rulename{dense}
\begin{isabelle}%
-{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
+{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
\end{isabelle}
-\rulename{realpow_abs}
+\rulename{power_abs}
\begin{isabelle}%
a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
--- a/doc-src/TutorialI/Types/document/Records.tex Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex Mon Jan 12 16:51:45 2004 +0100
@@ -379,9 +379,9 @@
be the same as \isa{point{\isachardot}make}.
\begin{isabelle}%
-point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isanewline
+point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isasep\isanewline%
point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
-{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline
+{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
\end{isabelle}
@@ -389,10 +389,10 @@
\begin{isabelle}%
cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
-{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isanewline
-cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isanewline
+{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
+cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
-{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline
+{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
\end{isabelle}
--- a/doc-src/TutorialI/Types/numerics.tex Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Mon Jan 12 16:51:45 2004 +0100
@@ -439,9 +439,9 @@
defined for the reals, along with many theorems such as this one about
exponentiation:
\begin{isabelle}
-\isasymbar r\ \isacharcircum \ n\isasymbar\ =\
-\isasymbar r\isasymbar \ \isacharcircum \ n
-\rulename{realpow_abs}
+\isasymbar a\ \isacharcircum \ n\isasymbar\ =\
+\isasymbar a\isasymbar \ \isacharcircum \ n
+\rulename{power_abs}
\end{isabelle}
Numeric literals\index{numeric literals!for type \protect\isa{real}}
--- a/doc-src/TutorialI/isabelle.sty Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/isabelle.sty Mon Jan 12 16:51:45 2004 +0100
@@ -52,6 +52,7 @@
\newcommand{\isaindent}[1]{\hphantom{#1}}
\newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
\newcommand{\isadigit}[1]{#1}
\chardef\isacharbang=`\!
--- a/src/HOL/Complex/Complex.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Complex/Complex.thy Mon Jan 12 16:51:45 2004 +0100
@@ -527,7 +527,7 @@
lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1"
apply (rule_tac z = z in eq_Abs_complex)
apply (auto simp add: complex_mult complex_inverse complex_one_def
- complex_zero_def add_divide_distrib [symmetric] real_power_two mult_ac)
+ complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
apply (drule_tac y = y in real_sum_squares_not_zero)
apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
done
@@ -615,7 +615,7 @@
"complex_of_real(inverse x) = inverse(complex_of_real x)"
apply (case_tac "x=0", simp)
apply (simp add: complex_inverse complex_of_real_def real_divide_def
- inverse_mult_distrib real_power_two)
+ inverse_mult_distrib power2_eq_square)
done
lemma complex_of_real_add:
@@ -658,10 +658,10 @@
declare complex_mod_zero [simp]
lemma complex_mod_one [simp]: "cmod(1) = 1"
-by (simp add: cmod_def real_power_two)
+by (simp add: cmod_def power2_eq_square)
lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
-apply (simp add: complex_of_real_def real_power_two complex_mod)
+apply (simp add: complex_of_real_def power2_eq_square complex_mod)
done
declare complex_mod_complex_of_real [simp]
@@ -702,7 +702,7 @@
lemma complex_mod_cnj: "cmod (cnj z) = cmod z"
apply (rule_tac z = z in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_cnj complex_mod real_power_two)
+apply (simp (no_asm_simp) add: complex_cnj complex_mod power2_eq_square)
done
declare complex_mod_cnj [simp]
@@ -713,7 +713,7 @@
lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"
apply (rule_tac z = z in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_cnj complex_inverse real_power_two)
+apply (simp (no_asm_simp) add: complex_cnj complex_inverse power2_eq_square)
done
lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"
@@ -771,7 +771,7 @@
lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
apply (rule_tac z = z in eq_Abs_complex)
-apply (auto simp add: complex_cnj complex_mult complex_of_real_def real_power_two)
+apply (auto simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
done
@@ -802,7 +802,7 @@
lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
apply (rule_tac z = x in eq_Abs_complex)
-apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def real_power_two)
+apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square)
done
declare complex_mod_eq_zero_cancel [simp]
@@ -813,14 +813,14 @@
lemma complex_mod_minus: "cmod (-x) = cmod(x)"
apply (rule_tac z = x in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_mod complex_minus real_power_two)
+apply (simp (no_asm_simp) add: complex_mod complex_minus power2_eq_square)
done
declare complex_mod_minus [simp]
lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
apply (rule_tac z = z in eq_Abs_complex)
apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult);
-apply (simp (no_asm) add: real_power_two real_abs_def)
+apply (simp (no_asm) add: power2_eq_square real_abs_def)
done
lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"
@@ -841,15 +841,15 @@
apply (rule_tac z = y in eq_Abs_complex)
apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
apply (rule_tac n = 1 in power_inject_base)
-apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc)
-apply (auto simp add: real_diff_def real_power_two right_distrib left_distrib add_ac mult_ac)
+apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
+apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac)
done
lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
apply (rule_tac z = x in eq_Abs_complex)
apply (rule_tac z = y in eq_Abs_complex)
apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
-apply (auto simp add: right_distrib left_distrib real_power_two mult_ac add_ac)
+apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
done
lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) <= cmod(x * cnj y)"
@@ -866,7 +866,7 @@
declare complex_Re_mult_cnj_le_cmod2 [simp]
lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
-apply (simp (no_asm) add: left_distrib right_distrib real_power_two)
+apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)
done
lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 <= (cmod(x) + cmod(y)) ^ 2"
@@ -883,7 +883,7 @@
lemma complex_mod_triangle_ineq: "cmod (x + y) <= cmod(x) + cmod(y)"
apply (rule_tac n = 1 in realpow_increasing)
apply (auto intro: order_trans [OF _ complex_mod_ge_zero]
- simp add: real_power_two [symmetric])
+ simp add: power2_eq_square [symmetric])
done
declare complex_mod_triangle_ineq [simp]
@@ -897,7 +897,7 @@
lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"
apply (rule_tac z = x in eq_Abs_complex)
apply (rule_tac z = y in eq_Abs_complex)
-apply (auto simp add: complex_diff complex_mod right_diff_distrib real_power_two left_diff_distrib add_ac mult_ac)
+apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)
done
lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"
@@ -943,7 +943,7 @@
lemma complex_inverse_minus: "inverse (-x) = - inverse (x::complex)"
apply (rule_tac z = x in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_inverse complex_minus real_power_two)
+apply (simp (no_asm_simp) add: complex_inverse complex_minus power2_eq_square)
done
lemma complex_divide_one: "x / (1::complex) = x"
@@ -1201,7 +1201,7 @@
lemma complex_mod_mult_i:
"cmod (ii * complex_of_real y) = abs y"
apply (unfold i_def complex_of_real_def)
-apply (auto simp add: complex_mult complex_mod real_power_two)
+apply (auto simp add: complex_mult complex_mod power2_eq_square)
done
declare complex_mod_mult_i [simp]
@@ -1427,7 +1427,7 @@
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
apply (case_tac "r=0")
apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
-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)
+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)
apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def)
done
--- a/src/HOL/Complex/NSCA.ML Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Complex/NSCA.ML Mon Jan 12 16:51:45 2004 +0100
@@ -823,26 +823,28 @@
by (dtac (approx_minus_iff RS iffD1) 1);
by (dtac (approx_minus_iff RS iffD1) 1);
by (rtac (capprox_minus_iff RS iffD2) 1);
-by (auto_tac (claset(),simpset() addsimps [mem_cinfmal_iff RS sym,
- mem_infmal_iff RS sym,hypreal_minus,hypreal_add,hcomplex_minus,
- hcomplex_add,CInfinitesimal_hcmod_iff,hcmod,Infinitesimal_FreeUltrafilterNat_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [mem_cinfmal_iff RS sym,
+ mem_infmal_iff RS sym,hypreal_minus,hypreal_add,hcomplex_minus,
+ hcomplex_add,CInfinitesimal_hcmod_iff,hcmod,
+ Infinitesimal_FreeUltrafilterNat_iff]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by Auto_tac;
by (dres_inst_tac [("x","u/2")] spec 1);
by (dres_inst_tac [("x","u/2")] spec 1);
-by (Step_tac 1);
+by Safe_tac;
by (TRYALL(Force_tac));
by (ultra_tac (claset(),HOL_ss) 1);
-by (dtac sym 1 THEN dtac sym 1);
+by (dtac sym 1 THEN dtac sym 1);
by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
-by (auto_tac (claset(),HOL_ss addsimps [complex_minus,complex_add,
+by (auto_tac (claset(),
+ HOL_ss addsimps [complex_minus,complex_add,
complex_mod, snd_conv, fst_conv,numeral_2_eq_2]));
-by (rtac (realpow_two_abs RS subst) 1);
-by (res_inst_tac [("x1","xa + - xb")] (realpow_two_abs RS subst) 1);
-by (simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym]) 1);
-by (rtac lemma_sqrt_hcomplex_capprox 1);
+by (subgoal_tac "sqrt (abs(xa + - xb) ^ 2 + abs(y + - ya) ^ 2) < u" 1);
+by (rtac lemma_sqrt_hcomplex_capprox 2);
by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1);
qed "hcomplex_capproxI";
Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) =\
@@ -902,11 +904,10 @@
by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
-by (rtac (realpow_two_abs RS subst) 1);
-by (res_inst_tac [("x1","Y x")] (realpow_two_abs RS subst) 1);
-by (simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym]) 1);
-by (rtac lemma_sqrt_hcomplex_capprox 1);
+by (subgoal_tac "sqrt (abs(Y x) ^ 2 + abs(Z x) ^ 2) < 2*u + 2*v" 1);
+by (rtac lemma_sqrt_hcomplex_capprox 2);
by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1);
qed "HFinite_Re_Im_CFinite";
Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite) = \
--- a/src/HOL/Complex/NSComplexBin.ML Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Complex/NSComplexBin.ML Mon Jan 12 16:51:45 2004 +0100
@@ -328,8 +328,7 @@
val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
[add_zero_left, add_zero_right,
- mult_left_zero, mult_right_zero, mult_1,
- mult_1_right];
+ mult_zero_left, mult_zero_right, mult_1, mult_1_right];
val prep_simproc = Complex_Numeral_Simprocs.prep_simproc;
--- a/src/HOL/Complex/ex/Sqrt.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Complex/ex/Sqrt.thy Mon Jan 12 16:51:45 2004 +0100
@@ -84,7 +84,7 @@
proof -
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
- by (auto simp add: power_two real_power_two)
+ by (auto simp add: power2_eq_square)
also have "(sqrt (real p))\<twosuperior> = real p" by simp
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
finally show ?thesis ..
@@ -94,8 +94,8 @@
from eq have "p dvd m\<twosuperior>" ..
with p_prime show "p dvd m" by (rule prime_dvd_power_two)
then obtain k where "m = p * k" ..
- with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
- with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
+ with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
+ with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
with p_prime show "p dvd n" by (rule prime_dvd_power_two)
qed
@@ -127,15 +127,15 @@
and gcd: "gcd (m, n) = 1" ..
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
- by (auto simp add: power_two real_power_two)
+ by (auto simp add: power2_eq_square)
also have "(sqrt (real p))\<twosuperior> = real p" by simp
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
then have "p dvd m\<twosuperior>" ..
with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
then obtain k where "m = p * k" ..
- with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
- with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
+ with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
+ with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
with p_prime have "p dvd n" by (rule prime_dvd_power_two)
with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
--- a/src/HOL/Hoare/Arith2.ML Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Hoare/Arith2.ML Mon Jan 12 16:51:45 2004 +0100
@@ -64,7 +64,7 @@
(*** pow ***)
Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
-by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
- mult_div_cancel]) 1);
+by (asm_simp_tac (simpset() addsimps [power2_eq_square RS sym,
+ power_mult RS sym, mult_div_cancel]) 1);
qed "sq_pow_div2";
Addsimps [sq_pow_div2];
--- a/src/HOL/Integ/Int.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/Int.thy Mon Jan 12 16:51:45 2004 +0100
@@ -229,6 +229,8 @@
by (simp add: zabs_def)
text{*This version is proved for all ordered rings, not just integers!
+ It is proved here because attribute @{text arith_split} is not available
+ in theory @{text Ring_and_Field}.
But is it really better than just rewriting with @{text abs_if}?*}
lemma abs_split [arith_split]:
"P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
@@ -371,6 +373,7 @@
val negative_eq_positive = thm "negative_eq_positive";
val zle_iff_zadd = thm "zle_iff_zadd";
val abs_int_eq = thm "abs_int_eq";
+val abs_split = thm"abs_split";
val nat_int = thm "nat_int";
val nat_zminus_int = thm "nat_zminus_int";
val nat_zero = thm "nat_zero";
--- a/src/HOL/Integ/IntArith.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/IntArith.thy Mon Jan 12 16:51:45 2004 +0100
@@ -8,6 +8,7 @@
theory IntArith = Bin
files ("int_arith1.ML"):
+
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
@@ -24,6 +25,7 @@
use "int_arith1.ML"
setup int_arith_setup
+
subsection{*More inequality reasoning*}
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
@@ -41,7 +43,8 @@
lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
by arith
-subsection{*Results about @{term nat}*}
+
+subsection{*The Functions @{term nat} and @{term int}*}
lemma nonneg_eq_int: "[| 0 \<le> z; !!m. z = int m ==> P |] ==> P"
by (blast dest: nat_0_le sym)
@@ -62,7 +65,8 @@
by (auto simp add: nat_eq_iff2)
-(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
+text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
+ @{term "w + - z"}*}
declare Zero_int_def [symmetric, simp]
declare One_int_def [symmetric, simp]
@@ -87,28 +91,11 @@
lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
-subsection{*@{term abs}: Absolute Value, as an Integer*}
-
-(* Simpler: use zabs_def as rewrite rule
- but arith_tac is not parameterized by such simp rules
-*)
-
-lemma zabs_split [arith_split]:
- "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
-by (simp add: zabs_def)
-
-lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)"
-by (simp add: zabs_def)
-
text{*This simplifies expressions of the form @{term "int n = z"} where
z is an integer literal.*}
declare int_eq_iff [of _ "number_of v", standard, simp]
-lemma zabs_eq_iff:
- "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
- by (auto simp add: zabs_def)
-
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
by simp
@@ -202,21 +189,6 @@
apply (rule step, simp+)
done
-subsection{*Simple Equations*}
-
-lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)"
-by simp
-
-lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)"
-by arith
-
-lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
-by arith
-
-lemma triangle_ineq: "abs(x+y) \<le> abs(x) + abs(y::int)"
-by arith
-
-
subsection{*Intermediate value theorems*}
lemma int_val_lemma:
@@ -249,39 +221,6 @@
done
-subsection{*Some convenient biconditionals for products of signs*}
-
-lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
- by (rule Ring_and_Field.mult_pos)
-
-lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
- by (rule Ring_and_Field.mult_neg)
-
-lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
- by (rule Ring_and_Field.mult_pos_neg)
-
-lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
- by (rule Ring_and_Field.zero_less_mult_iff)
-
-lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
- by (rule Ring_and_Field.zero_le_mult_iff)
-
-lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
- by (rule Ring_and_Field.mult_less_0_iff)
-
-lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
- by (rule Ring_and_Field.mult_le_0_iff)
-
-lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
- by (rule Ring_and_Field.abs_eq_0)
-
-lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
- by (rule Ring_and_Field.zero_less_abs_iff)
-
-lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
- by (rule Ring_and_Field.zero_le_square)
-
-
subsection{*Products and 1, by T. M. Rasmussen*}
lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
@@ -307,7 +246,7 @@
apply (rule zless_1_zmult, arith)
apply (subgoal_tac "0<n", arith)
apply (subgoal_tac "0<m*n")
-apply (drule int_0_less_mult_iff [THEN iffD1], auto)
+apply (drule zero_less_mult_iff [THEN iffD1], auto)
done
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
@@ -341,8 +280,8 @@
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
apply (case_tac "0 \<le> z'")
apply (rule inj_int [THEN injD])
-apply (simp add: zmult_int [symmetric] int_0_le_mult_iff)
-apply (simp add: zmult_le_0_iff)
+apply (simp add: zmult_int [symmetric] zero_le_mult_iff)
+apply (simp add: mult_le_0_iff)
done
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
@@ -353,9 +292,10 @@
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
apply (case_tac "z=0 | w=0")
apply (auto simp add: zabs_def nat_mult_distrib [symmetric]
- nat_mult_distrib_neg [symmetric] zmult_less_0_iff)
+ nat_mult_distrib_neg [symmetric] mult_less_0_iff)
done
+
ML
{*
val zle_diff1_eq = thm "zle_diff1_eq";
@@ -370,25 +310,8 @@
val nat_2 = thm "nat_2";
val nat_less_eq_zless = thm "nat_less_eq_zless";
val nat_le_eq_zle = thm "nat_le_eq_zle";
-val zabs_split = thm "zabs_split";
-val zero_le_zabs = thm "zero_le_zabs";
-val int_diff_minus_eq = thm "int_diff_minus_eq";
-val abs_abs = thm "abs_abs";
-val abs_minus = thm "abs_minus";
-val triangle_ineq = thm "triangle_ineq";
val nat_intermed_int_val = thm "nat_intermed_int_val";
-val zmult_pos = thm "zmult_pos";
-val zmult_neg = thm "zmult_neg";
-val zmult_pos_neg = thm "zmult_pos_neg";
-val int_0_less_mult_iff = thm "int_0_less_mult_iff";
-val int_0_le_mult_iff = thm "int_0_le_mult_iff";
-val zmult_less_0_iff = thm "zmult_less_0_iff";
-val zmult_le_0_iff = thm "zmult_le_0_iff";
-val abs_mult = thm "abs_mult";
-val abs_eq_0 = thm "abs_eq_0";
-val zero_less_abs_iff = thm "zero_less_abs_iff";
-val square_nonzero = thm "square_nonzero";
val zmult_eq_self_iff = thm "zmult_eq_self_iff";
val zless_1_zmult = thm "zless_1_zmult";
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
--- a/src/HOL/Integ/IntDiv.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/IntDiv.thy Mon Jan 12 16:51:45 2004 +0100
@@ -357,12 +357,12 @@
lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
apply (subgoal_tac "0 < a*q")
- apply (simp add: int_0_less_mult_iff, arith)
+ apply (simp add: zero_less_mult_iff, arith)
done
lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
apply (subgoal_tac "0 \<le> a* (1-q) ")
- apply (simp add: int_0_le_mult_iff)
+ apply (simp add: zero_le_mult_iff)
apply (simp add: zdiff_zmult_distrib2)
done
@@ -516,7 +516,7 @@
lemma q_pos_lemma:
"[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)"
apply (subgoal_tac "0 < b'* (q' + 1) ")
- apply (simp add: int_0_less_mult_iff)
+ apply (simp add: zero_less_mult_iff)
apply (simp add: zadd_zmult_distrib2)
done
@@ -549,7 +549,7 @@
lemma q_neg_lemma:
"[| b'*q' + r' < 0; 0 \<le> r'; 0 < b' |] ==> q' \<le> (0::int)"
apply (subgoal_tac "b'*q' < 0")
- apply (simp add: zmult_less_0_iff, arith)
+ apply (simp add: mult_less_0_iff, arith)
done
lemma zdiv_mono2_neg_lemma:
@@ -711,13 +711,13 @@
lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
apply (subgoal_tac "b * (q mod c) \<le> 0")
apply arith
-apply (simp add: zmult_le_0_iff)
+apply (simp add: mult_le_0_iff)
done
lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \<le> r; r < b |] ==> 0 \<le> b * (q mod c) + r"
apply (subgoal_tac "0 \<le> b * (q mod c) ")
apply arith
-apply (simp add: int_0_le_mult_iff)
+apply (simp add: zero_le_mult_iff)
done
lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
@@ -733,7 +733,7 @@
lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b ~= 0; 0 < c |]
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
by (auto simp add: mult_ac quorem_def linorder_neq_iff
- int_0_less_mult_iff zadd_zmult_distrib2 [symmetric]
+ zero_less_mult_iff zadd_zmult_distrib2 [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
@@ -1033,7 +1033,7 @@
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
apply (unfold dvd_def, auto)
- apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff)
+ apply (simp add: zmult_assoc zmult_eq_self_iff zero_less_mult_iff zmult_eq_1_iff)
done
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
@@ -1112,15 +1112,15 @@
apply (subgoal_tac "0 < n")
prefer 2
apply (blast intro: zless_trans)
- apply (simp add: int_0_less_mult_iff)
+ apply (simp add: zero_less_mult_iff)
apply (subgoal_tac "n * k < n * 1")
apply (drule zmult_zless_cancel1 [THEN iffD1], auto)
done
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
apply (auto simp add: dvd_def nat_abs_mult_distrib)
- apply (auto simp add: nat_eq_iff zabs_eq_iff)
- apply (rule_tac [2] x = "-(int k)" in exI)
+ apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
+ apply (rule_tac x = "-(int k)" in exI)
apply (auto simp add: zmult_int [symmetric])
done
@@ -1131,7 +1131,7 @@
apply (rule_tac x = "nat (-k)" in exI)
apply (cut_tac [3] k = m in int_less_0_conv)
apply (cut_tac k = m in int_less_0_conv)
- apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
+ apply (auto simp add: zero_le_mult_iff mult_less_0_iff
nat_mult_distrib [symmetric] nat_eq_iff2)
done
@@ -1139,7 +1139,7 @@
apply (auto simp add: dvd_def zmult_int [symmetric])
apply (rule_tac x = "nat k" in exI)
apply (cut_tac k = m in int_less_0_conv)
- apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff
+ apply (auto simp add: zero_le_mult_iff mult_less_0_iff
nat_mult_distrib [symmetric] nat_eq_iff2)
done
@@ -1162,6 +1162,49 @@
done
+subsection{*Integer Powers*}
+
+instance int :: power ..
+
+primrec
+ "p ^ 0 = 1"
+ "p ^ (Suc n) = (p::int) * (p ^ n)"
+
+
+instance int :: ringpower
+proof
+ fix z :: int
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
+
+
+lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
+apply (induct_tac "y", auto)
+apply (rule zmod_zmult1_eq [THEN trans])
+apply (simp (no_asm_simp))
+apply (rule zmod_zmult_distrib [symmetric])
+done
+
+lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
+ by (rule Power.power_add)
+
+lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
+ by (rule Power.power_mult [symmetric])
+
+lemma zero_less_zpower_abs_iff [simp]:
+ "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
+apply (induct_tac "n")
+apply (auto simp add: zero_less_mult_iff)
+done
+
+lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
+apply (induct_tac "n")
+apply (auto simp add: zero_le_mult_iff)
+done
+
+
ML
{*
val quorem_def = thm "quorem_def";
@@ -1264,6 +1307,12 @@
val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff";
val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff";
val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff";
+
+val zpower_zmod = thm "zpower_zmod";
+val zpower_zadd_distrib = thm "zpower_zadd_distrib";
+val zpower_zpower = thm "zpower_zpower";
+val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
+val zero_le_zpower_abs = thm "zero_le_zpower_abs";
*}
end
--- a/src/HOL/Integ/IntPower.thy Mon Jan 12 16:45:35 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* Title: IntPower.thy
- ID: $Id$
- Author: Thomas M. Rasmussen
- Copyright 2000 University of Cambridge
-
-Integer powers
-*)
-
-theory IntPower = IntDiv:
-
-instance int :: power ..
-
-primrec
- power_0: "p ^ 0 = 1"
- power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)"
-
-
-instance int :: ringpower
-proof
- fix z :: int
- fix n :: nat
- show "z^0 = 1" by simp
- show "z^(Suc n) = z * (z^n)" by simp
-qed
-
-
-lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
-apply (induct_tac "y", auto)
-apply (rule zmod_zmult1_eq [THEN trans])
-apply (simp (no_asm_simp))
-apply (rule zmod_zmult_distrib [symmetric])
-done
-
-lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
- by (rule Power.power_add)
-
-lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
- by (rule Power.power_mult [symmetric])
-
-lemma zero_less_zpower_abs_iff [simp]:
- "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
-apply (induct_tac "n")
-apply (auto simp add: int_0_less_mult_iff)
-done
-
-lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
-apply (induct_tac "n")
-apply (auto simp add: int_0_le_mult_iff)
-done
-
-ML
-{*
-val zpower_zmod = thm "zpower_zmod";
-val zpower_zadd_distrib = thm "zpower_zadd_distrib";
-val zpower_zpower = thm "zpower_zpower";
-val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
-val zero_le_zpower_abs = thm "zero_le_zpower_abs";
-*}
-
-end
-
--- a/src/HOL/Integ/NatBin.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy Mon Jan 12 16:51:45 2004 +0100
@@ -6,7 +6,7 @@
header {* Binary arithmetic for the natural numbers *}
-theory NatBin = IntPower:
+theory NatBin = IntDiv:
text {*
Arithmetic for naturals is reduced to that for the non-negative integers.
@@ -19,7 +19,7 @@
"(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
-(** nat (coercion from int to nat) **)
+subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
declare nat_0 [simp] nat_1 [simp]
@@ -75,7 +75,7 @@
done
-(** int (coercion from nat to int) **)
+subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
(*"neg" is used in rewrite rules for binary comparisons*)
lemma int_nat_number_of:
@@ -284,6 +284,89 @@
lemmas numerals = numeral_0_eq_0 numeral_1_eq_1 numeral_2_eq_2
+subsection{*General Theorems About Powers Involving Binary Numerals*}
+
+text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
+We cannot prove general results about the numeral @{term "-1"}, so we have to
+use @{term "- 1"} instead.*}
+
+lemma power2_eq_square: "(a::'a::{semiring,ringpower})\<twosuperior> = a * a"
+ by (simp add: numeral_2_eq_2 Power.power_Suc)
+
+lemma [simp]: "(0::'a::{semiring,ringpower})\<twosuperior> = 0"
+ by (simp add: power2_eq_square)
+
+lemma [simp]: "(1::'a::{semiring,ringpower})\<twosuperior> = 1"
+ by (simp add: power2_eq_square)
+
+text{*Squares of literal numerals will be evaluated.*}
+declare power2_eq_square [of "number_of w", standard, simp]
+
+lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_ring,ringpower})"
+ by (simp add: power2_eq_square zero_le_square)
+
+lemma zero_less_power2 [simp]:
+ "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_ring,ringpower}))"
+ by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
+
+lemma zero_eq_power2 [simp]:
+ "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_ring,ringpower}))"
+ by (force simp add: power2_eq_square mult_eq_0_iff)
+
+lemma abs_power2 [simp]:
+ "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_ring,ringpower})"
+ by (simp add: power2_eq_square abs_mult abs_mult_self)
+
+lemma power2_abs [simp]:
+ "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_ring,ringpower})"
+ by (simp add: power2_eq_square abs_mult_self)
+
+lemma power2_minus [simp]:
+ "(- a)\<twosuperior> = (a\<twosuperior>::'a::{ring,ringpower})"
+ by (simp add: power2_eq_square)
+
+lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{ring,ringpower})"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc power_add)
+done
+
+lemma power_minus_even [simp]:
+ "(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)"
+by (simp add: power_minus1_even power_minus [of a])
+
+lemma zero_le_even_power:
+ "0 \<le> (a::'a::{ordered_ring,ringpower}) ^ (2*n)"
+proof (induct "n")
+ case 0
+ show ?case by (simp add: zero_le_one)
+next
+ case (Suc n)
+ have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
+ by (simp add: mult_ac power_add power2_eq_square)
+ thus ?case
+ by (simp add: prems zero_le_square zero_le_mult_iff)
+qed
+
+lemma odd_power_less_zero:
+ "(a::'a::{ordered_ring,ringpower}) < 0 ==> a ^ Suc(2*n) < 0"
+proof (induct "n")
+ case 0
+ show ?case by (simp add: Power.power_Suc)
+next
+ case (Suc n)
+ have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
+ by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
+ thus ?case
+ by (simp add: prems mult_less_0_iff mult_neg)
+qed
+
+lemma odd_0_le_power_imp_0_le:
+ "0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_ring,ringpower})"
+apply (insert odd_power_less_zero [of a n])
+apply (force simp add: linorder_not_less [symmetric])
+done
+
+
(** Nat **)
lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
@@ -320,11 +403,6 @@
declare diff_less' [of "number_of v", standard, simp]
-(** Power **)
-
-lemma power_two: "(p::nat) ^ 2 = p*p"
-by (simp add: numerals)
-
(*** Comparisons involving (0::nat) ***)
@@ -477,9 +555,6 @@
lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
by (simp add: zpower_zpower mult_commute)
-lemma zpower_two: "(p::int) ^ 2 = p*p"
-by (simp add: numerals)
-
lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
by (simp add: zpower_even zpower_zadd_distrib)
@@ -490,7 +565,7 @@
apply (simp only: number_of_add)
apply (rule_tac x = "number_of w" in spec, clarify)
apply (case_tac " (0::int) <= x")
-apply (auto simp add: nat_mult_distrib zpower_even zpower_two)
+apply (auto simp add: nat_mult_distrib zpower_even power2_eq_square)
done
lemma zpower_number_of_odd:
@@ -501,7 +576,7 @@
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def)
apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0)
apply (rule_tac x = "number_of w" in spec, clarify)
-apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat)
+apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even power2_eq_square neg_nat)
done
declare zpower_number_of_even [of "number_of v", standard, simp]
@@ -569,52 +644,6 @@
by (simp add: Let_def)
-subsection {*More ML Bindings*}
-
-ML
-{*
-val eq_nat_nat_iff = thm"eq_nat_nat_iff";
-val eq_nat_number_of = thm"eq_nat_number_of";
-val less_nat_number_of = thm"less_nat_number_of";
-val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less";
-val Suc_pred' = thm"Suc_pred'";
-val expand_Suc = thm"expand_Suc";
-val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
-val add_eq_if = thm"add_eq_if";
-val mult_eq_if = thm"mult_eq_if";
-val power_eq_if = thm"power_eq_if";
-val diff_less' = thm"diff_less'";
-val power_two = thm"power_two";
-val eq_number_of_0 = thm"eq_number_of_0";
-val eq_0_number_of = thm"eq_0_number_of";
-val less_0_number_of = thm"less_0_number_of";
-val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
-val eq_number_of_Suc = thm"eq_number_of_Suc";
-val Suc_eq_number_of = thm"Suc_eq_number_of";
-val less_number_of_Suc = thm"less_number_of_Suc";
-val less_Suc_number_of = thm"less_Suc_number_of";
-val le_number_of_Suc = thm"le_number_of_Suc";
-val le_Suc_number_of = thm"le_Suc_number_of";
-val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
-val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
-val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
-val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
-val nat_power_eq = thm"nat_power_eq";
-val power_nat_number_of = thm"power_nat_number_of";
-val zpower_even = thm"zpower_even";
-val zpower_two = thm"zpower_two";
-val zpower_odd = thm"zpower_odd";
-val zpower_number_of_even = thm"zpower_number_of_even";
-val zpower_number_of_odd = thm"zpower_number_of_odd";
-val nat_number_of_Pls = thm"nat_number_of_Pls";
-val nat_number_of_Min = thm"nat_number_of_Min";
-val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
-val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
-val Let_Suc = thm"Let_Suc";
-
-val nat_number = thms"nat_number";
-*}
-
subsection {*Lemmas for the Combination and Cancellation Simprocs*}
lemma nat_number_of_add_left:
@@ -697,8 +726,61 @@
"(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
by (simp add: nat_mult_div_cancel1)
+
ML
{*
+val eq_nat_nat_iff = thm"eq_nat_nat_iff";
+val eq_nat_number_of = thm"eq_nat_number_of";
+val less_nat_number_of = thm"less_nat_number_of";
+val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less";
+val power2_eq_square = thm "power2_eq_square";
+val zero_le_power2 = thm "zero_le_power2";
+val zero_less_power2 = thm "zero_less_power2";
+val zero_eq_power2 = thm "zero_eq_power2";
+val abs_power2 = thm "abs_power2";
+val power2_abs = thm "power2_abs";
+val power2_minus = thm "power2_minus";
+val power_minus1_even = thm "power_minus1_even";
+val power_minus_even = thm "power_minus_even";
+val zero_le_even_power = thm "zero_le_even_power";
+val odd_power_less_zero = thm "odd_power_less_zero";
+val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le";
+
+val Suc_pred' = thm"Suc_pred'";
+val expand_Suc = thm"expand_Suc";
+val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
+val add_eq_if = thm"add_eq_if";
+val mult_eq_if = thm"mult_eq_if";
+val power_eq_if = thm"power_eq_if";
+val diff_less' = thm"diff_less'";
+val eq_number_of_0 = thm"eq_number_of_0";
+val eq_0_number_of = thm"eq_0_number_of";
+val less_0_number_of = thm"less_0_number_of";
+val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
+val eq_number_of_Suc = thm"eq_number_of_Suc";
+val Suc_eq_number_of = thm"Suc_eq_number_of";
+val less_number_of_Suc = thm"less_number_of_Suc";
+val less_Suc_number_of = thm"less_Suc_number_of";
+val le_number_of_Suc = thm"le_number_of_Suc";
+val le_Suc_number_of = thm"le_Suc_number_of";
+val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
+val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
+val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
+val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
+val nat_power_eq = thm"nat_power_eq";
+val power_nat_number_of = thm"power_nat_number_of";
+val zpower_even = thm"zpower_even";
+val zpower_odd = thm"zpower_odd";
+val zpower_number_of_even = thm"zpower_number_of_even";
+val zpower_number_of_odd = thm"zpower_number_of_odd";
+val nat_number_of_Pls = thm"nat_number_of_Pls";
+val nat_number_of_Min = thm"nat_number_of_Min";
+val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
+val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
+val Let_Suc = thm"Let_Suc";
+
+val nat_number = thms"nat_number";
+
val nat_number_of_add_left = thm"nat_number_of_add_left";
val left_add_mult_distrib = thm"left_add_mult_distrib";
val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
@@ -717,6 +799,10 @@
val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj";
val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj";
val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
+
+val power_minus1_even = thm"power_minus1_even";
+val power_minus_even = thm"power_minus_even";
+val zero_le_even_power = thm"zero_le_even_power";
*}
--- a/src/HOL/Integ/NatSimprocs.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy Mon Jan 12 16:51:45 2004 +0100
@@ -152,7 +152,8 @@
declare zero_le_divide_iff [of "number_of w", standard, simp]
declare divide_le_0_iff [of "number_of w", standard, simp]
-(*Replaces "inverse #nn" by 1/#nn *)
+(*Replaces "inverse #nn" by 1/#nn. It looks strange, but then other simprocs
+simplify the quotient.*)
declare inverse_eq_divide [of "number_of w", standard, simp]
text{*These laws simplify inequalities, moving unary minus from a term
--- a/src/HOL/Integ/Presburger.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/Presburger.thy Mon Jan 12 16:51:45 2004 +0100
@@ -883,7 +883,7 @@
next
assume ?Q
hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
- with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
+ with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
thus ?P by(simp)
qed
--- a/src/HOL/Integ/presburger.ML Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/presburger.ML Mon Jan 12 16:51:45 2004 +0100
@@ -184,7 +184,7 @@
addcongs [conj_le_cong, imp_le_cong]
(* simp rules for elimination of abs *)
- val simpset3 = HOL_basic_ss addsplits [zabs_split]
+ val simpset3 = HOL_basic_ss addsplits [abs_split]
val ct = cterm_of sg (HOLogic.mk_Trueprop t)
--- a/src/HOL/IsaMakefile Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/IsaMakefile Mon Jan 12 16:51:45 2004 +0100
@@ -87,8 +87,7 @@
HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
- Integ/IntDiv.thy Integ/IntPower.thy \
- Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
+ Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/int_arith1.ML \
Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
@@ -144,7 +143,6 @@
Real/PRat.ML Real/PRat.thy \
Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
Real/ROOT.ML Real/Real.thy \
- Real/RealArith0.thy Real/real_arith0.ML \
Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
Real/RealBin.thy Real/RealDef.thy \
Real/RealInt.thy Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
@@ -152,8 +150,7 @@
Hyperreal/Fact.ML Hyperreal/Fact.thy\
Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
- Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
- Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
+ Hyperreal/HyperArith.thy Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.ML Hyperreal/Log.thy\
@@ -164,7 +161,6 @@
Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
- Hyperreal/hypreal_arith0.ML\
Complex/Complex_Main.thy\
Complex/CLim.ML Complex/CLim.thy\
Complex/CSeries.ML Complex/CSeries.thy\
--- a/src/HOL/Library/Primes.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Library/Primes.thy Mon Jan 12 16:51:45 2004 +0100
@@ -200,7 +200,7 @@
by (auto dest: prime_dvd_mult)
lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
- by (rule prime_dvd_square) (simp_all add: power_two)
+ by (rule prime_dvd_square) (simp_all add: power2_eq_square)
text {* \medskip Addition laws *}
--- a/src/HOL/Library/Rational_Numbers.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy Mon Jan 12 16:51:45 2004 +0100
@@ -1,7 +1,7 @@
-(* Title: HOL/Library/Rational_Numbers.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
- License: GPL (GNU GENERAL PUBLIC LICENSE)
+(* Title: HOL/Library/Rational_Numbers.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {*
@@ -85,7 +85,7 @@
next
assume a': "a' \<noteq> 0"
from eq1 eq2 have "(a * b') * (a' * b'') = (a' * b) * (a'' * b')" by simp
- hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: zmult_ac)
+ hence "(a * b'') * (a' * b') = (a'' * b) * (a' * b')" by (simp only: mult_ac)
with a' b' show ?thesis by simp
qed
thus "fract a b \<sim> fract a'' b''" ..
@@ -152,11 +152,11 @@
(is "?lhs = ?rhs")
proof -
have "?lhs = (a * b') * (d * d') + (c * d') * (b * b')"
- by (simp add: int_distrib zmult_ac)
+ by (simp add: int_distrib mult_ac)
also have "... = (a' * b) * (d * d') + (c' * d) * (b * b')"
by (simp only: eq1 eq2)
also have "... = ?rhs"
- by (simp add: int_distrib zmult_ac)
+ by (simp add: int_distrib mult_ac)
finally show "?lhs = ?rhs" .
qed
from neq show "b * d \<noteq> 0" by simp
@@ -188,7 +188,7 @@
have "\<lfloor>fract (a * c) (b * d)\<rfloor> = \<lfloor>fract (a' * c') (b' * d')\<rfloor>"
proof
from eq1 eq2 have "(a * b') * (c * d') = (a' * b) * (c' * d)" by simp
- thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: zmult_ac)
+ thus "(a * c) * (b' * d') = (a' * c') * (b * d)" by (simp add: mult_ac)
from neq show "b * d \<noteq> 0" by simp
from neq show "b' * d' \<noteq> 0" by simp
qed
@@ -206,7 +206,7 @@
with neq obtain "a \<noteq> 0" and "a' \<noteq> 0" by (simp add: is_zero_fraction_iff)
assume "\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor>"
hence "a * b' = a' * b" ..
- hence "b * a' = b' * a" by (simp only: zmult_ac)
+ hence "b * a' = b' * a" by (simp only: mult_ac)
hence "\<lfloor>fract b a\<rfloor> = \<lfloor>fract b' a'\<rfloor>" ..
with neq show ?thesis by (simp add: inverse_fraction_def)
qed
@@ -225,12 +225,12 @@
fix a b c d x :: int assume x: "x \<noteq> 0"
have "?le a b c d = ?le (a * x) (b * x) c d"
proof -
- from x have "0 < x * x" by (auto simp add: int_less_le)
+ from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
hence "?le a b c d =
((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
- by (simp add: zmult_zle_cancel2)
+ by (simp add: mult_le_cancel_right)
also have "... = ?le (a * x) (b * x) c d"
- by (simp add: zmult_ac)
+ by (simp add: mult_ac)
finally show ?thesis .
qed
} note le_factor = this
@@ -241,11 +241,11 @@
hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
by (rule le_factor)
also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
- by (simp add: zmult_ac)
+ by (simp add: mult_ac)
also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
by (simp only: eq1 eq2)
also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
- by (simp add: zmult_ac)
+ by (simp add: mult_ac)
also from D have "... = ?le a' b' c' d'"
by (rule le_factor [symmetric])
finally have "?le a b c d = ?le a' b' c' d'" .
@@ -470,14 +470,15 @@
theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
- (auto simp add: zmult_less_0_iff int_0_less_mult_iff int_le_less split: zabs_split)
+ (auto simp add: mult_less_0_iff zero_less_mult_iff int_le_less
+ split: abs_split)
subsubsection {* The ordered field of rational numbers *}
lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
by (induct q, induct r, induct s)
- (simp add: add_rat zadd_ac zmult_ac int_distrib)
+ (simp add: add_rat add_ac mult_ac int_distrib)
lemma rat_add_0: "0 + q = (q::rat)"
by (induct q) (simp add: zero_rat add_rat)
@@ -492,7 +493,7 @@
show "(q + r) + s = q + (r + s)"
by (rule rat_add_assoc)
show "q + r = r + q"
- by (induct q, induct r) (simp add: add_rat zadd_ac zmult_ac)
+ by (induct q, induct r) (simp add: add_rat add_ac mult_ac)
show "0 + q = q"
by (induct q) (simp add: zero_rat add_rat)
show "(-q) + q = 0"
@@ -500,9 +501,9 @@
show "q - r = q + (-r)"
by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
show "(q * r) * s = q * (r * s)"
- by (induct q, induct r, induct s) (simp add: mult_rat zmult_ac)
+ by (induct q, induct r, induct s) (simp add: mult_rat mult_ac)
show "q * r = r * q"
- by (induct q, induct r) (simp add: mult_rat zmult_ac)
+ by (induct q, induct r) (simp add: mult_rat mult_ac)
show "1 * q = q"
by (induct q) (simp add: one_rat mult_rat)
show "(q + r) * s = q * s + r * s"
@@ -533,25 +534,25 @@
show "Fract a b \<le> Fract e f"
proof -
from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f"
- by (auto simp add: int_less_le)
+ by (auto simp add: zero_less_mult_iff linorder_neq_iff)
have "(a * d) * (b * d) * (f * f) \<le> (c * b) * (b * d) * (f * f)"
proof -
from neq 1 have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
by (simp add: le_rat)
- with ff show ?thesis by (simp add: zmult_zle_cancel2)
+ with ff show ?thesis by (simp add: mult_le_cancel_right)
qed
also have "... = (c * f) * (d * f) * (b * b)"
- by (simp only: zmult_ac)
+ by (simp only: mult_ac)
also have "... \<le> (e * d) * (d * f) * (b * b)"
proof -
from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
by (simp add: le_rat)
- with bb show ?thesis by (simp add: zmult_zle_cancel2)
+ with bb show ?thesis by (simp add: mult_le_cancel_right)
qed
finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
- by (simp only: zmult_ac)
+ by (simp only: mult_ac)
with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
- by (simp add: zmult_zle_cancel2)
+ by (simp add: mult_le_cancel_right)
with neq show ?thesis by (simp add: le_rat)
qed
qed
@@ -570,7 +571,7 @@
proof -
from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
by (simp add: le_rat)
- thus ?thesis by (simp only: zmult_ac)
+ thus ?thesis by (simp only: mult_ac)
qed
finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
moreover from neq have "b * d \<noteq> 0" by simp
@@ -584,7 +585,7 @@
show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
by (simp only: less_rat_def)
show "q \<le> r \<or> r \<le> q"
- by (induct q, induct r) (simp add: le_rat zmult_ac, arith)
+ by (induct q, induct r) (simp add: le_rat mult_ac, arith)
}
qed
@@ -601,12 +602,12 @@
show "Fract e f + Fract a b \<le> Fract e f + Fract c d"
proof -
let ?F = "f * f" from neq have F: "0 < ?F"
- by (auto simp add: int_less_le)
+ by (auto simp add: zero_less_mult_iff)
from neq le have "(a * d) * (b * d) \<le> (c * b) * (b * d)"
by (simp add: le_rat)
with F have "(a * d) * (b * d) * ?F * ?F \<le> (c * b) * (b * d) * ?F * ?F"
- by (simp add: zmult_zle_cancel2)
- with neq show ?thesis by (simp add: add_rat le_rat zmult_ac int_distrib)
+ by (simp add: mult_le_cancel_right)
+ with neq show ?thesis by (simp add: add_rat le_rat mult_ac int_distrib)
qed
qed
show "q < r ==> 0 < s ==> s * q < s * r"
@@ -621,13 +622,13 @@
from neq gt have "0 < ?E"
by (auto simp add: zero_rat less_rat le_rat int_less_le eq_rat)
moreover from neq have "0 < ?F"
- by (auto simp add: int_less_le)
+ by (auto simp add: zero_less_mult_iff)
moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
by (simp add: less_rat)
ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
- by (simp add: zmult_zless_cancel2)
+ by (simp add: mult_less_cancel_right)
with neq show ?thesis
- by (simp add: less_rat mult_rat zmult_ac)
+ by (simp add: less_rat mult_rat mult_ac)
qed
qed
show "\<bar>q\<bar> = (if q < 0 then -q else q)"
--- a/src/HOL/NumberTheory/Chinese.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/NumberTheory/Chinese.thy Mon Jan 12 16:51:45 2004 +0100
@@ -75,7 +75,7 @@
lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
apply (induct n)
apply auto
- apply (simp add: int_0_less_mult_iff)
+ apply (simp add: zero_less_mult_iff)
done
lemma funprod_zgcd [rule_format (no_asm)]:
--- a/src/HOL/NumberTheory/Gauss.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Mon Jan 12 16:51:45 2004 +0100
@@ -180,7 +180,7 @@
lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
apply (insert a_nonzero)
-by (auto simp add: B_def zmult_pos A_greater_zero)
+by (auto simp add: B_def mult_pos A_greater_zero)
lemma (in GAUSS) C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)";
apply (auto simp add: C_def)
--- a/src/HOL/NumberTheory/IntPrimes.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Mon Jan 12 16:51:45 2004 +0100
@@ -126,7 +126,7 @@
lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
by (simp del: zmult_zminus_right
add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def
- zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
+ mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
by (simp add: zabs_def zgcd_zmult_distrib2)
@@ -144,7 +144,7 @@
"zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
apply (subgoal_tac "m = zgcd (m * n, m * k)")
apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
- apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
+ apply (simp_all add: zgcd_zmult_distrib2 [symmetric] zero_le_mult_iff)
done
lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
@@ -363,7 +363,7 @@
"0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
apply (unfold zcong_def dvd_def, auto)
apply (subgoal_tac "0 < m")
- apply (simp add: int_0_le_mult_iff)
+ apply (simp add: zero_le_mult_iff)
apply (subgoal_tac "m * k < m * 1")
apply (drule zmult_zless_cancel1 [THEN iffD1])
apply (auto simp add: linorder_neq_iff)
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Mon Jan 12 16:51:45 2004 +0100
@@ -130,7 +130,7 @@
then have "0 \<le> x";
by (auto simp add: A_def)
with a_nonzero have "0 \<le> x * a";
- by (auto simp add: int_0_le_mult_iff)
+ by (auto simp add: zero_le_mult_iff)
with p_g_2 show "0 \<le> x * a div p";
by (auto simp add: pos_imp_zdiv_nonneg_iff)
qed;
--- a/src/HOL/Power.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Power.thy Mon Jan 12 16:51:45 2004 +0100
@@ -153,6 +153,12 @@
lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
by force
+lemma nonzero_power_inverse:
+ "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
+done
+
text{*Perhaps these should be simprules.*}
lemma power_inverse:
"inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
@@ -160,11 +166,38 @@
apply (auto simp add: power_Suc inverse_mult_distrib)
done
+lemma nonzero_power_divide:
+ "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
+by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+
+lemma power_divide:
+ "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
+apply (case_tac "b=0", simp add: power_0_left)
+apply (rule nonzero_power_divide)
+apply assumption
+done
+
lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
apply (induct_tac "n")
apply (auto simp add: power_Suc abs_mult)
done
+lemma zero_less_power_abs_iff [simp]:
+ "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
+proof (induct "n")
+ case 0
+ show ?case by (simp add: zero_less_one)
+next
+ case (Suc n)
+ show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
+qed
+
+lemma zero_le_power_abs [simp]:
+ "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n"
+apply (induct_tac "n")
+apply (auto simp add: zero_le_one zero_le_power)
+done
+
lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
proof -
have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric])
@@ -413,7 +446,11 @@
val field_power_eq_0_iff = thm"field_power_eq_0_iff";
val field_power_not_zero = thm"field_power_not_zero";
val power_inverse = thm"power_inverse";
+val nonzero_power_divide = thm"nonzero_power_divide";
+val power_divide = thm"power_divide";
val power_abs = thm"power_abs";
+val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
+val zero_le_power_abs = thm "zero_le_power_abs";
val power_minus = thm"power_minus";
val power_Suc_less = thm"power_Suc_less";
val power_strict_decreasing = thm"power_strict_decreasing";
--- a/src/HOL/Presburger.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Presburger.thy Mon Jan 12 16:51:45 2004 +0100
@@ -883,7 +883,7 @@
next
assume ?Q
hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac)
- with gr0 have "0 < (c*n + t - m)" by(simp add:int_0_less_mult_iff)
+ with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff)
thus ?P by(simp)
qed
--- a/src/HOL/Ring_and_Field.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Jan 12 16:51:45 2004 +0100
@@ -7,13 +7,11 @@
header {*
\title{Ring and field structures}
- \author{Gertrud Bauer and Markus Wenzel}
+ \author{Gertrud Bauer, L. C. Paulson and Markus Wenzel}
*}
theory Ring_and_Field = Inductive:
-text{*Lemmas and extension to semirings by L. C. Paulson*}
-
subsection {* Abstract algebraic structures *}
axclass semiring \<subseteq> zero, one, plus, times
@@ -167,14 +165,14 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
-lemma mult_left_zero [simp]: "0 * a = (0::'a::semiring)"
+lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring)"
proof -
have "0*a + 0*a = 0*a + 0"
by (simp add: left_distrib [symmetric])
thus ?thesis by (simp only: add_left_cancel)
qed
-lemma mult_right_zero [simp]: "a * 0 = (0::'a::semiring)"
+lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring)"
by (simp add: mult_commute)
@@ -1333,6 +1331,39 @@
apply (simp add: divide_inverse_zero field_mult_cancel_left)
done
+subsection {* Division and the Number One *}
+
+text{*Simplify expressions equated with 1*}
+lemma divide_eq_1_iff [simp]:
+ "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+apply (case_tac "b=0", simp)
+apply (simp add: right_inverse_eq)
+done
+
+
+lemma one_eq_divide_iff [simp]:
+ "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+by (simp add: eq_commute [of 1])
+
+lemma zero_eq_1_divide_iff [simp]:
+ "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
+apply (case_tac "a=0", simp)
+apply (auto simp add: nonzero_eq_divide_eq)
+done
+
+lemma one_divide_eq_0_iff [simp]:
+ "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
+apply (case_tac "a=0", simp)
+apply (insert zero_neq_one [THEN not_sym])
+apply (auto simp add: nonzero_divide_eq_eq)
+done
+
+text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
+declare zero_less_divide_iff [of "1", simp]
+declare divide_less_0_iff [of "1", simp]
+declare zero_le_divide_iff [of "1", simp]
+declare divide_le_0_iff [of "1", simp]
+
subsection {* Ordering Rules for Division *}
@@ -1413,7 +1444,6 @@
minus_mult_left [symmetric] minus_mult_right [symmetric])
done
-
lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
by (simp add: abs_if)
@@ -1571,8 +1601,8 @@
val mult_1 = thm"mult_1";
val mult_1_right = thm"mult_1_right";
val mult_left_commute = thm"mult_left_commute";
-val mult_left_zero = thm"mult_left_zero";
-val mult_right_zero = thm"mult_right_zero";
+val mult_zero_left = thm"mult_zero_left";
+val mult_zero_right = thm"mult_zero_right";
val left_distrib = thm "left_distrib";
val right_distrib = thm"right_distrib";
val combine_common_factor = thm"combine_common_factor";
--- a/src/HOL/Tools/Presburger/presburger.ML Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Mon Jan 12 16:51:45 2004 +0100
@@ -184,7 +184,7 @@
addcongs [conj_le_cong, imp_le_cong]
(* simp rules for elimination of abs *)
- val simpset3 = HOL_basic_ss addsplits [zabs_split]
+ val simpset3 = HOL_basic_ss addsplits [abs_split]
val ct = cterm_of sg (HOLogic.mk_Trueprop t)
--- a/src/HOL/ex/PresburgerEx.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/ex/PresburgerEx.thy Mon Jan 12 16:51:45 2004 +0100
@@ -8,79 +8,86 @@
theory PresburgerEx = Main:
-theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x"
+theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
by presburger
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
- (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)"
+ (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)"
by presburger
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==>
- 2 dvd (y::int) ==> (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)"
+ 2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)"
by presburger
-theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x ";
+theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x ";
by presburger
-theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2";
+text{*Very slow: about 55 seconds on a 1.8GHz machine.*}
+theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2";
by presburger
-theorem "EX (x::int). 0 < x" by presburger
+theorem "\<exists>(x::int). 0 < x" by presburger
-theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
+theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
-theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger
+theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" by presburger
theorem
- "EX (x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by presburger
+ "\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" by presburger
-theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
by presburger
-theorem "ALL (x::int). b < x --> a <= x"
+theorem "\<forall>(x::int). b < x --> a \<le> x"
apply (presburger no_quantify)
oops
-theorem "ALL (x::int). b < x --> a <= x"
+theorem "\<forall>(x::int). b < x --> a \<le> x"
apply (presburger no_quantify)
oops
-theorem "~ (EX (x::int). False)"
+theorem "~ (\<exists>(x::int). False)"
by presburger
-theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x"
+theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
apply (presburger no_quantify)
oops
-theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger
+theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger
-theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger
+theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger
-theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger
+theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" by presburger
-theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger
+theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger
+
+theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger
-theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger
-
-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))))"
+theorem "~ (\<forall>(x::int).
+ ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
+ (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
+ --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
by presburger
theorem
- "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+ "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
by presburger
theorem
- "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger
+ "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
+ by presburger
theorem
- "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" by presburger
+ "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
+ by presburger
theorem
- "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+ "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
by presburger
-theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
+text{*Very slow: about 80 seconds on a 1.8GHz machine.*}
+theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
-theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
+theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
end
\ No newline at end of file
--- a/src/HOL/ex/set.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/ex/set.thy Mon Jan 12 16:51:45 2004 +0100
@@ -156,8 +156,9 @@
lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
\<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
- -- {* Example 8. *}
- by force -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
+ -- {* Example 8 now needs a small hint. *}
+ by (simp add: abs_if, force)
+ -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
text {* Example 9 omitted (requires the reals). *}