# HG changeset patch # User paulson # Date 1073922705 -3600 # Node ID 79f9fbef910679f43851d514d6146d6de0b15cd2 # Parent a8b1a44d82642dc7e5755253a68c86cf53bb6fb8 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 diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Documents/Documents.thy --- 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 \ (0::int) \ 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} %(* diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Documents/document/Documents.tex --- 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} %(* diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Types/Numbers.thy --- 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} diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Types/document/Numbers.tex --- 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% diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Types/document/Records.tex --- 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} diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Types/numerics.tex --- 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}} diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/isabelle.sty --- 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=`\! diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Complex/Complex.thy --- 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 diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Complex/NSCA.ML --- 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) = \ diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Complex/NSComplexBin.ML --- 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; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Complex/ex/Sqrt.thy --- 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 = \sqrt (real p)\ * real n" by simp then have "real (m\) = (sqrt (real p))\ * real (n\)" - by (auto simp add: power_two real_power_two) + by (auto simp add: power2_eq_square) also have "(sqrt (real p))\ = real p" by simp also have "\ * real (n\) = real (p * n\)" by simp finally show ?thesis .. @@ -94,8 +94,8 @@ from eq have "p dvd m\" .. 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\ = p\ * k\" by (auto simp add: power_two mult_ac) - with p have "n\ = p * k\" by (simp add: power_two) + with eq have "p * n\ = p\ * k\" by (auto simp add: power2_eq_square mult_ac) + with p have "n\ = p * k\" by (simp add: power2_eq_square) then have "p dvd n\" .. 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 = \sqrt (real p)\ * real n" by simp then have "real (m\) = (sqrt (real p))\ * real (n\)" - by (auto simp add: power_two real_power_two) + by (auto simp add: power2_eq_square) also have "(sqrt (real p))\ = real p" by simp also have "\ * real (n\) = real (p * n\)" by simp finally have eq: "m\ = p * n\" .. then have "p dvd m\" .. 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\ = p\ * k\" by (auto simp add: power_two mult_ac) - with p have "n\ = p * k\" by (simp add: power_two) + with eq have "p * n\ = p\ * k\" by (auto simp add: power2_eq_square mult_ac) + with p have "n\ = p * k\" by (simp add: power2_eq_square) then have "p dvd n\" .. 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) diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Hoare/Arith2.ML --- 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]; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/Int.thy --- 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 \ 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"; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/IntArith.thy --- 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 w + (1::int) \ 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; !!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 \ z ==> (nat w \ nat z) = (w\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 \ i --> P i) & (i < 0 --> P(-i)))" -by (simp add: zabs_def) - -lemma zero_le_zabs [iff]: "0 \ 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 \ 0 \ z \ z = -w \ z < 0)" - by (auto simp add: zabs_def) - lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ 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) \ 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) \ x*y) = (0 \ x & 0 \ y | x \ 0 & y \ 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 \ (0::int)) = (0 \ x & y \ 0 | x \ 0 & 0 \ 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 \ 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 z ==> nat (z*z') = nat z * nat z'" apply (case_tac "0 \ 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 \ (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"; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/IntDiv.thy --- 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 \ 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 \ r |] ==> q \ 1" apply (subgoal_tac "0 \ 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 \ b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \ (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 \ r'; 0 < b' |] ==> q' \ (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 \ 0 |] ==> b * (q mod c) + r \ 0" apply (subgoal_tac "b * (q mod c) \ 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 \ r; r < b |] ==> 0 \ b * (q mod c) + r" apply (subgoal_tac "0 \ 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 \ 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 \ (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 diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/IntPower.thy --- 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 \ (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 - diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/NatBin.thy --- 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})\ = a * a" + by (simp add: numeral_2_eq_2 Power.power_Suc) + +lemma [simp]: "(0::'a::{semiring,ringpower})\ = 0" + by (simp add: power2_eq_square) + +lemma [simp]: "(1::'a::{semiring,ringpower})\ = 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 \ (a\::'a::{ordered_ring,ringpower})" + by (simp add: power2_eq_square zero_le_square) + +lemma zero_less_power2 [simp]: + "(0 < a\) = (a \ (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\ = 0) = (a = (0::'a::{ordered_ring,ringpower}))" + by (force simp add: power2_eq_square mult_eq_0_iff) + +lemma abs_power2 [simp]: + "abs(a\) = (a\::'a::{ordered_ring,ringpower})" + by (simp add: power2_eq_square abs_mult abs_mult_self) + +lemma power2_abs [simp]: + "(abs a)\ = (a\::'a::{ordered_ring,ringpower})" + by (simp add: power2_eq_square abs_mult_self) + +lemma power2_minus [simp]: + "(- a)\ = (a\::'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 \ (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 \ a ^ Suc(2*n) ==> 0 \ (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"; *} diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/NatSimprocs.thy --- 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 diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/Presburger.thy --- 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 diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Integ/presburger.ML --- 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) diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/IsaMakefile --- 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\ diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Library/Primes.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 \ prime ==> p dvd m\ ==> 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 *} diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Library/Rational_Numbers.thy --- 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' \ 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 \ 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 \ 0" by simp @@ -188,7 +188,7 @@ have "\fract (a * c) (b * d)\ = \fract (a' * c') (b' * d')\" 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 \ 0" by simp from neq show "b' * d' \ 0" by simp qed @@ -206,7 +206,7 @@ with neq obtain "a \ 0" and "a' \ 0" by (simp add: is_zero_fraction_iff) assume "\fract a b\ = \fract a' b'\" 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 "\fract b a\ = \fract b' a'\" .. 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 \ 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) \ (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' \ (c * d') * ?D * ?D' * b * b')" - by (simp add: zmult_ac) + by (simp add: mult_ac) also have "... = ((a' * b) * ?D * ?D' * d * d' \ (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 \ 0 ==> \Fract a b\ = Fract \a\ \b\" 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 \ 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) \ (c * b) * (b * d) * (f * f)" proof - from neq 1 have "(a * d) * (b * d) \ (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 "... \ (e * d) * (d * f) * (b * b)" proof - from neq 2 have "(c * f) * (d * f) \ (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) \ e * b * (b * f) * (d * d)" - by (simp only: zmult_ac) + by (simp only: mult_ac) with dd have "(a * f) * (b * f) \ (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) \ (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 \ 0" by simp @@ -584,7 +585,7 @@ show "(q < r) = (q \ r \ q \ r)" by (simp only: less_rat_def) show "q \ r \ r \ 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 \ 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) \ (c * b) * (b * d)" by (simp add: le_rat) with F have "(a * d) * (b * d) * ?F * ?F \ (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 "\q\ = (if q < 0 then -q else q)" diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/NumberTheory/Chinese.thy --- 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: "(\i. i \ 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)]: diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/NumberTheory/Gauss.thy --- 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 \ 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 \ C ==> ~[x = 0](mod p)"; apply (auto simp add: C_def) diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/NumberTheory/IntPrimes.thy --- 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 \ 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 \ 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 \ 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) diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/NumberTheory/Quadratic_Reciprocity.thy --- 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 \ x"; by (auto simp add: A_def) with a_nonzero have "0 \ 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 \ x * a div p"; by (auto simp add: pos_imp_zdiv_nonneg_iff) qed; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Power.thy --- 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 \ (0::'a::{field,ringpower}) ==> a^n \ 0" by force +lemma nonzero_power_inverse: + "a \ 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 \ 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 \ (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}) \ (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"; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Presburger.thy --- 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 diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Ring_and_Field.thy --- 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 \ 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 \ 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 \ 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"; diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Tools/Presburger/presburger.ML --- 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) diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/ex/PresburgerEx.thy --- 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 "(\(y::int). 3 dvd y) ==> \(x::int). b < x --> a \ 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)" + (\(x::int). 2*x = y) & (\(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) ==> (\(x::int). 2*x = y) & (\(k::int). 3*k = z)" by presburger -theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x "; +theorem "\(x::nat). \(y::nat). (0::nat) \ 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 "\(x::nat). \(y::nat). y = 5 + x | x div 6 + 1= 2"; by presburger -theorem "EX (x::int). 0 < x" by presburger +theorem "\(x::int). 0 < x" by presburger -theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger +theorem "\(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 "\(x::int) y. 2 * x + 1 \ 2 * y" by presburger theorem - "EX (x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by presburger + "\(x::int) y. 0 < x & 0 \ y & 3 * x - 5 * y = 1" by presburger -theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" +theorem "~ (\(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by presburger -theorem "ALL (x::int). b < x --> a <= x" +theorem "\(x::int). b < x --> a \ x" apply (presburger no_quantify) oops -theorem "ALL (x::int). b < x --> a <= x" +theorem "\(x::int). b < x --> a \ x" apply (presburger no_quantify) oops -theorem "~ (EX (x::int). False)" +theorem "~ (\(x::int). False)" by presburger -theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x" +theorem "\(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 "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" by presburger -theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger +theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" by presburger -theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger +theorem "\(x::int). (2 dvd x) = (\(y::int). x = 2*y)" by presburger -theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger +theorem "\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y + 1))" by presburger + +theorem "\(x::int). ((2 dvd x) = (\(y::int). x \ 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 "~ (\(x::int). + ((2 dvd x) = (\(y::int). x \ 2*y+1) | + (\(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))" + "~ (\(i::int). 4 \ i --> (\x y. 0 \ x & 0 \ 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 + "\(i::int). 8 \ i --> (\x y. 0 \ x & 0 \ 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 + "\(j::int). \i. j \ i --> (\x y. 0 \ x & 0 \ 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))" + "~ (\j (i::int). j \ i --> (\x y. 0 \ x & 0 \ 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 "(\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 "(\m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger end \ No newline at end of file diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/ex/set.thy --- 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 "(\u v. u < (0::int) \ u \ abs v) \ (\A::int set. (\y. abs y \ A) \ -2 \ 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). *}