moved definition of power on ints to theory Int
authorhaftmann
Fri Jan 25 14:53:52 2008 +0100 (2008-01-25)
changeset 25961ec39d7e40554
parent 25960 1f9956e0bd89
child 25962 13b6c0b31005
moved definition of power on ints to theory Int
NEWS
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/Library/Word.thy
     1.1 --- a/NEWS	Thu Jan 24 23:51:22 2008 +0100
     1.2 +++ b/NEWS	Fri Jan 25 14:53:52 2008 +0100
     1.3 @@ -25,6 +25,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theorems "power.simps" renamed to "power_int.simps".
     1.8 +
     1.9  * New class semiring_div provides basic abstract properties of semirings
    1.10  with division and modulo operations.  Subsumes former class dvd_mod.
    1.11  
     2.1 --- a/src/HOL/Int.thy	Thu Jan 24 23:51:22 2008 +0100
     2.2 +++ b/src/HOL/Int.thy	Fri Jan 25 14:53:52 2008 +0100
     2.3 @@ -221,6 +221,7 @@
     2.4      by (cases i, cases j, cases k) (simp add: le add)
     2.5  qed
     2.6  
     2.7 +
     2.8  text{*Strict Monotonicity of Multiplication*}
     2.9  
    2.10  text{*strict, in 1st argument; proof is by induction on k>0*}
    2.11 @@ -261,6 +262,13 @@
    2.12      by (simp only: zsgn_def)
    2.13  qed
    2.14  
    2.15 +instance int :: lordered_ring
    2.16 +proof  
    2.17 +  fix k :: int
    2.18 +  show "abs k = sup k (- k)"
    2.19 +    by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
    2.20 +qed
    2.21 +
    2.22  lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
    2.23  apply (cases w, cases z) 
    2.24  apply (simp add: less le add One_int_def)
    2.25 @@ -1729,6 +1737,46 @@
    2.26  qed
    2.27  
    2.28  
    2.29 +subsection{*Integer Powers*} 
    2.30 +
    2.31 +instantiation int :: recpower
    2.32 +begin
    2.33 +
    2.34 +primrec power_int where
    2.35 +  "p ^ 0 = (1\<Colon>int)"
    2.36 +  | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
    2.37 +
    2.38 +instance proof
    2.39 +  fix z :: int
    2.40 +  fix n :: nat
    2.41 +  show "z ^ 0 = 1" by simp
    2.42 +  show "z ^ Suc n = z * (z ^ n)" by simp
    2.43 +qed
    2.44 +
    2.45 +end
    2.46 +
    2.47 +lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
    2.48 +  by (rule Power.power_add)
    2.49 +
    2.50 +lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
    2.51 +  by (rule Power.power_mult [symmetric])
    2.52 +
    2.53 +lemma zero_less_zpower_abs_iff [simp]:
    2.54 +  "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
    2.55 +  by (induct n) (auto simp add: zero_less_mult_iff)
    2.56 +
    2.57 +lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
    2.58 +  by (induct n) (auto simp add: zero_le_mult_iff)
    2.59 +
    2.60 +lemma of_int_power:
    2.61 +  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
    2.62 +  by (induct n) (simp_all add: power_Suc)
    2.63 +
    2.64 +lemma int_power: "int (m^n) = (int m) ^ n"
    2.65 +  by (rule of_nat_power)
    2.66 +
    2.67 +lemmas zpower_int = int_power [symmetric]
    2.68 +
    2.69  subsection {* Configuration of the code generator *}
    2.70  
    2.71  instance int :: eq ..
    2.72 @@ -1765,7 +1813,7 @@
    2.73  
    2.74  lemma one_is_num_one [code func, code inline, symmetric, code post]:
    2.75    "(1\<Colon>int) = Numeral1" 
    2.76 -  by simp 
    2.77 +  by simp
    2.78  
    2.79  code_modulename SML
    2.80    Int Integer
     3.1 --- a/src/HOL/IntDiv.thy	Thu Jan 24 23:51:22 2008 +0100
     3.2 +++ b/src/HOL/IntDiv.thy	Fri Jan 25 14:53:52 2008 +0100
     3.3 @@ -1418,28 +1418,6 @@
     3.4    apply (auto simp add: dvd_imp_le)
     3.5    done
     3.6  
     3.7 -
     3.8 -subsection{*Integer Powers*} 
     3.9 -
    3.10 -instance int :: power ..
    3.11 -
    3.12 -primrec
    3.13 -  "p ^ 0 = 1"
    3.14 -  "p ^ (Suc n) = (p::int) * (p ^ n)"
    3.15 -
    3.16 -
    3.17 -instance int :: recpower
    3.18 -proof
    3.19 -  fix z :: int
    3.20 -  fix n :: nat
    3.21 -  show "z^0 = 1" by simp
    3.22 -  show "z^(Suc n) = z * (z^n)" by simp
    3.23 -qed
    3.24 -
    3.25 -lemma of_int_power:
    3.26 -  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
    3.27 -  by (induct n) (simp_all add: power_Suc)
    3.28 -
    3.29  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
    3.30  apply (induct "y", auto)
    3.31  apply (rule zmod_zmult1_eq [THEN trans])
    3.32 @@ -1447,29 +1425,6 @@
    3.33  apply (rule zmod_zmult_distrib [symmetric])
    3.34  done
    3.35  
    3.36 -lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
    3.37 -  by (rule Power.power_add)
    3.38 -
    3.39 -lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
    3.40 -  by (rule Power.power_mult [symmetric])
    3.41 -
    3.42 -lemma zero_less_zpower_abs_iff [simp]:
    3.43 -     "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
    3.44 -apply (induct "n")
    3.45 -apply (auto simp add: zero_less_mult_iff)
    3.46 -done
    3.47 -
    3.48 -lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
    3.49 -apply (induct "n")
    3.50 -apply (auto simp add: zero_le_mult_iff)
    3.51 -done
    3.52 -
    3.53 -lemma int_power: "int (m^n) = (int m) ^ n"
    3.54 -  by (rule of_nat_power)
    3.55 -
    3.56 -text{*Compatibility binding*}
    3.57 -lemmas zpower_int = int_power [symmetric]
    3.58 -
    3.59  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
    3.60  apply (subst split_div, auto)
    3.61  apply (subst split_zdiv, auto)
     4.1 --- a/src/HOL/Library/Word.thy	Thu Jan 24 23:51:22 2008 +0100
     4.2 +++ b/src/HOL/Library/Word.thy	Fri Jan 25 14:53:52 2008 +0100
     4.3 @@ -40,11 +40,11 @@
     4.4      Zero ("\<zero>")
     4.5    | One ("\<one>")
     4.6  
     4.7 -consts
     4.8 +primrec
     4.9    bitval :: "bit => nat"
    4.10 -primrec
    4.11 +where
    4.12    "bitval \<zero> = 0"
    4.13 -  "bitval \<one> = 1"
    4.14 +  | "bitval \<one> = 1"
    4.15  
    4.16  consts
    4.17    bitnot :: "bit => bit"
    4.18 @@ -1531,7 +1531,7 @@
    4.19      show ?thesis
    4.20        apply simp
    4.21        apply (subst power_Suc [symmetric])
    4.22 -      apply (simp del: power.simps)
    4.23 +      apply (simp del: power_int.simps)
    4.24        done
    4.25    qed
    4.26    finally show ?thesis .