1.1 --- a/src/HOL/IsaMakefile Wed Jun 30 16:28:13 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Jun 30 16:28:14 2010 +0200
1.3 @@ -397,8 +397,8 @@
1.4 $(LOG)/HOL-Library.gz: $(OUT)/HOL $(SRC)/HOL/Tools/float_arith.ML \
1.5 $(SRC)/Tools/float.ML Library/Abstract_Rat.thy Library/AssocList.thy \
1.6 Library/BigO.thy Library/Binomial.thy Library/Bit.thy \
1.7 - Library/Boolean_Algebra.thy Library/Char_nat.thy \
1.8 - Library/Code_Char.thy Library/Code_Char_chr.thy \
1.9 + Library/Boolean_Algebra.thy Library/Cardinality.thy \
1.10 + Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy
1.11 Library/Code_Integer.thy Library/ContNotDenum.thy \
1.12 Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
1.13 Library/Diagonalize.thy Library/Dlist.thy Library/Efficient_Nat.thy \
1.14 @@ -1191,9 +1191,9 @@
1.15 HOL-Word: HOL $(OUT)/HOL-Word
1.16
1.17 $(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \
1.18 - Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \
1.19 - Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \
1.20 - Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy \
1.21 + Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \
1.22 + Word/Type_Length.thy Word/BinGeneral.thy Word/BinOperations.thy \
1.23 + Word/BinBoolList.thy Word/Bit_Operations.thy Word/WordDefinition.thy \
1.24 Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy \
1.25 Word/WordGenLib.thy Word/Word.thy Word/document/root.tex \
1.26 Word/document/root.bib Tools/SMT/smt_word.ML
2.1 --- a/src/HOL/Word/BitSyntax.thy Wed Jun 30 16:28:13 2010 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,94 +0,0 @@
2.4 -(*
2.5 - Author: Brian Huffman, PSU and Gerwin Klein, NICTA
2.6 -
2.7 - Syntactic class for bitwise operations.
2.8 -*)
2.9 -
2.10 -
2.11 -header {* Syntactic classes for bitwise operations *}
2.12 -
2.13 -theory BitSyntax
2.14 -imports BinGeneral
2.15 -begin
2.16 -
2.17 -class bit =
2.18 - fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
2.19 - and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
2.20 - and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
2.21 - and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
2.22 -
2.23 -text {*
2.24 - We want the bitwise operations to bind slightly weaker
2.25 - than @{text "+"} and @{text "-"}, but @{text "~~"} to
2.26 - bind slightly stronger than @{text "*"}.
2.27 -*}
2.28 -
2.29 -text {*
2.30 - Testing and shifting operations.
2.31 -*}
2.32 -
2.33 -class bits = bit +
2.34 - fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
2.35 - and lsb :: "'a \<Rightarrow> bool"
2.36 - and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
2.37 - and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
2.38 - and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
2.39 - and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
2.40 -
2.41 -class bitss = bits +
2.42 - fixes msb :: "'a \<Rightarrow> bool"
2.43 -
2.44 -
2.45 -subsection {* Bitwise operations on @{typ bit} *}
2.46 -
2.47 -instantiation bit :: bit
2.48 -begin
2.49 -
2.50 -primrec bitNOT_bit where
2.51 - "NOT bit.B0 = bit.B1"
2.52 - | "NOT bit.B1 = bit.B0"
2.53 -
2.54 -primrec bitAND_bit where
2.55 - "bit.B0 AND y = bit.B0"
2.56 - | "bit.B1 AND y = y"
2.57 -
2.58 -primrec bitOR_bit where
2.59 - "bit.B0 OR y = y"
2.60 - | "bit.B1 OR y = bit.B1"
2.61 -
2.62 -primrec bitXOR_bit where
2.63 - "bit.B0 XOR y = y"
2.64 - | "bit.B1 XOR y = NOT y"
2.65 -
2.66 -instance ..
2.67 -
2.68 -end
2.69 -
2.70 -lemmas bit_simps =
2.71 - bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
2.72 -
2.73 -lemma bit_extra_simps [simp]:
2.74 - "x AND bit.B0 = bit.B0"
2.75 - "x AND bit.B1 = x"
2.76 - "x OR bit.B1 = bit.B1"
2.77 - "x OR bit.B0 = x"
2.78 - "x XOR bit.B1 = NOT x"
2.79 - "x XOR bit.B0 = x"
2.80 - by (cases x, auto)+
2.81 -
2.82 -lemma bit_ops_comm:
2.83 - "(x::bit) AND y = y AND x"
2.84 - "(x::bit) OR y = y OR x"
2.85 - "(x::bit) XOR y = y XOR x"
2.86 - by (cases y, auto)+
2.87 -
2.88 -lemma bit_ops_same [simp]:
2.89 - "(x::bit) AND x = x"
2.90 - "(x::bit) OR x = x"
2.91 - "(x::bit) XOR x = bit.B0"
2.92 - by (cases x, auto)+
2.93 -
2.94 -lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
2.95 - by (cases x) auto
2.96 -
2.97 -end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Word/Bit_Operations.thy Wed Jun 30 16:28:14 2010 +0200
3.3 @@ -0,0 +1,91 @@
3.4 +(* Title: HOL/Word/Bit_Operations.thy
3.5 + Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
3.6 +*)
3.7 +
3.8 +header {* Syntactic classes for bitwise operations *}
3.9 +
3.10 +theory Bit_Operations
3.11 +imports Bit
3.12 +begin
3.13 +
3.14 +class bit =
3.15 + fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
3.16 + and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
3.17 + and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
3.18 + and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
3.19 +
3.20 +text {*
3.21 + We want the bitwise operations to bind slightly weaker
3.22 + than @{text "+"} and @{text "-"}, but @{text "~~"} to
3.23 + bind slightly stronger than @{text "*"}.
3.24 +*}
3.25 +
3.26 +text {*
3.27 + Testing and shifting operations.
3.28 +*}
3.29 +
3.30 +class bits = bit +
3.31 + fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
3.32 + and lsb :: "'a \<Rightarrow> bool"
3.33 + and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
3.34 + and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
3.35 + and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
3.36 + and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
3.37 +
3.38 +class bitss = bits +
3.39 + fixes msb :: "'a \<Rightarrow> bool"
3.40 +
3.41 +
3.42 +subsection {* Bitwise operations on @{typ bit} *}
3.43 +
3.44 +instantiation bit :: bit
3.45 +begin
3.46 +
3.47 +primrec bitNOT_bit where
3.48 + "NOT 0 = (1::bit)"
3.49 + | "NOT 1 = (0::bit)"
3.50 +
3.51 +primrec bitAND_bit where
3.52 + "0 AND y = (0::bit)"
3.53 + | "1 AND y = (y::bit)"
3.54 +
3.55 +primrec bitOR_bit where
3.56 + "0 OR y = (y::bit)"
3.57 + | "1 OR y = (1::bit)"
3.58 +
3.59 +primrec bitXOR_bit where
3.60 + "0 XOR y = (y::bit)"
3.61 + | "1 XOR y = (NOT y :: bit)"
3.62 +
3.63 +instance ..
3.64 +
3.65 +end
3.66 +
3.67 +lemmas bit_simps =
3.68 + bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
3.69 +
3.70 +lemma bit_extra_simps [simp]:
3.71 + "x AND 0 = (0::bit)"
3.72 + "x AND 1 = (x::bit)"
3.73 + "x OR 1 = (1::bit)"
3.74 + "x OR 0 = (x::bit)"
3.75 + "x XOR 1 = NOT (x::bit)"
3.76 + "x XOR 0 = (x::bit)"
3.77 + by (cases x, auto)+
3.78 +
3.79 +lemma bit_ops_comm:
3.80 + "(x::bit) AND y = y AND x"
3.81 + "(x::bit) OR y = y OR x"
3.82 + "(x::bit) XOR y = y XOR x"
3.83 + by (cases y, auto)+
3.84 +
3.85 +lemma bit_ops_same [simp]:
3.86 + "(x::bit) AND x = x"
3.87 + "(x::bit) OR x = x"
3.88 + "(x::bit) XOR x = 0"
3.89 + by (cases x, auto)+
3.90 +
3.91 +lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
3.92 + by (cases x) auto
3.93 +
3.94 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Word/Misc_Numeric.thy Wed Jun 30 16:28:14 2010 +0200
4.3 @@ -0,0 +1,450 @@
4.4 +(*
4.5 + Author: Jeremy Dawson, NICTA
4.6 +*)
4.7 +
4.8 +header {* Useful Numerical Lemmas *}
4.9 +
4.10 +theory Misc_Numeric
4.11 +imports Main Parity
4.12 +begin
4.13 +
4.14 +lemma contentsI: "y = {x} ==> contents y = x"
4.15 + unfolding contents_def by auto -- {* FIXME move *}
4.16 +
4.17 +lemmas split_split = prod.split
4.18 +lemmas split_split_asm = prod.split_asm
4.19 +lemmas split_splits = split_split split_split_asm
4.20 +
4.21 +lemmas funpow_0 = funpow.simps(1)
4.22 +lemmas funpow_Suc = funpow.simps(2)
4.23 +
4.24 +lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
4.25 +
4.26 +lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith
4.27 +
4.28 +declare iszero_0 [iff]
4.29 +
4.30 +lemmas xtr1 = xtrans(1)
4.31 +lemmas xtr2 = xtrans(2)
4.32 +lemmas xtr3 = xtrans(3)
4.33 +lemmas xtr4 = xtrans(4)
4.34 +lemmas xtr5 = xtrans(5)
4.35 +lemmas xtr6 = xtrans(6)
4.36 +lemmas xtr7 = xtrans(7)
4.37 +lemmas xtr8 = xtrans(8)
4.38 +
4.39 +lemmas nat_simps = diff_add_inverse2 diff_add_inverse
4.40 +lemmas nat_iffs = le_add1 le_add2
4.41 +
4.42 +lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith
4.43 +
4.44 +lemma nobm1:
4.45 + "0 < (number_of w :: nat) ==>
4.46 + number_of w - (1 :: nat) = number_of (Int.pred w)"
4.47 + apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
4.48 + apply (simp add: number_of_eq nat_diff_distrib [symmetric])
4.49 + done
4.50 +
4.51 +lemma zless2: "0 < (2 :: int)" by arith
4.52 +
4.53 +lemmas zless2p [simp] = zless2 [THEN zero_less_power]
4.54 +lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]
4.55 +
4.56 +lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
4.57 +lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
4.58 +
4.59 +-- "the inverse(s) of @{text number_of}"
4.60 +lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith
4.61 +
4.62 +lemma emep1:
4.63 + "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
4.64 + apply (simp add: add_commute)
4.65 + apply (safe dest!: even_equiv_def [THEN iffD1])
4.66 + apply (subst pos_zmod_mult_2)
4.67 + apply arith
4.68 + apply (simp add: mod_mult_mult1)
4.69 + done
4.70 +
4.71 +lemmas eme1p = emep1 [simplified add_commute]
4.72 +
4.73 +lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))" by arith
4.74 +
4.75 +lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith
4.76 +
4.77 +lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))" by arith
4.78 +
4.79 +lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith
4.80 +
4.81 +lemmas m1mod2k = zless2p [THEN zmod_minus1]
4.82 +lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
4.83 +lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2]
4.84 +lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
4.85 +lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
4.86 +
4.87 +lemma p1mod22k:
4.88 + "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)"
4.89 + by (simp add: p1mod22k' add_commute)
4.90 +
4.91 +lemma z1pmod2:
4.92 + "(2 * b + 1) mod 2 = (1::int)" by arith
4.93 +
4.94 +lemma z1pdiv2:
4.95 + "(2 * b + 1) div 2 = (b::int)" by arith
4.96 +
4.97 +lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
4.98 + simplified int_one_le_iff_zero_less, simplified, standard]
4.99 +
4.100 +lemma axxbyy:
4.101 + "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>
4.102 + a = b & m = (n :: int)" by arith
4.103 +
4.104 +lemma axxmod2:
4.105 + "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith
4.106 +
4.107 +lemma axxdiv2:
4.108 + "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)" by arith
4.109 +
4.110 +lemmas iszero_minus = trans [THEN trans,
4.111 + OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard]
4.112 +
4.113 +lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute,
4.114 + standard]
4.115 +
4.116 +lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard]
4.117 +
4.118 +lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b"
4.119 + by (simp add : zmod_zminus1_eq_if)
4.120 +
4.121 +lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
4.122 + apply (unfold diff_int_def)
4.123 + apply (rule trans [OF _ mod_add_eq [symmetric]])
4.124 + apply (simp add: zmod_uminus mod_add_eq [symmetric])
4.125 + done
4.126 +
4.127 +lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
4.128 + apply (unfold diff_int_def)
4.129 + apply (rule trans [OF _ mod_add_right_eq [symmetric]])
4.130 + apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
4.131 + done
4.132 +
4.133 +lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
4.134 + by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
4.135 +
4.136 +lemma zmod_zsub_self [simp]:
4.137 + "((b :: int) - a) mod a = b mod a"
4.138 + by (simp add: zmod_zsub_right_eq)
4.139 +
4.140 +lemma zmod_zmult1_eq_rev:
4.141 + "b * a mod c = b mod c * a mod (c::int)"
4.142 + apply (simp add: mult_commute)
4.143 + apply (subst zmod_zmult1_eq)
4.144 + apply simp
4.145 + done
4.146 +
4.147 +lemmas rdmods [symmetric] = zmod_uminus [symmetric]
4.148 + zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
4.149 + mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
4.150 +
4.151 +lemma mod_plus_right:
4.152 + "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
4.153 + apply (induct x)
4.154 + apply (simp_all add: mod_Suc)
4.155 + apply arith
4.156 + done
4.157 +
4.158 +lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)"
4.159 + by (induct n) (simp_all add : mod_Suc)
4.160 +
4.161 +lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
4.162 + THEN mod_plus_right [THEN iffD2], standard, simplified]
4.163 +
4.164 +lemmas push_mods' = mod_add_eq [standard]
4.165 + mod_mult_eq [standard] zmod_zsub_distrib [standard]
4.166 + zmod_uminus [symmetric, standard]
4.167 +
4.168 +lemmas push_mods = push_mods' [THEN eq_reflection, standard]
4.169 +lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
4.170 +lemmas mod_simps =
4.171 + mod_mult_self2_is_0 [THEN eq_reflection]
4.172 + mod_mult_self1_is_0 [THEN eq_reflection]
4.173 + mod_mod_trivial [THEN eq_reflection]
4.174 +
4.175 +lemma nat_mod_eq:
4.176 + "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"
4.177 + by (induct a) auto
4.178 +
4.179 +lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
4.180 +
4.181 +lemma nat_mod_lem:
4.182 + "(0 :: nat) < n ==> b < n = (b mod n = b)"
4.183 + apply safe
4.184 + apply (erule nat_mod_eq')
4.185 + apply (erule subst)
4.186 + apply (erule mod_less_divisor)
4.187 + done
4.188 +
4.189 +lemma mod_nat_add:
4.190 + "(x :: nat) < z ==> y < z ==>
4.191 + (x + y) mod z = (if x + y < z then x + y else x + y - z)"
4.192 + apply (rule nat_mod_eq)
4.193 + apply auto
4.194 + apply (rule trans)
4.195 + apply (rule le_mod_geq)
4.196 + apply simp
4.197 + apply (rule nat_mod_eq')
4.198 + apply arith
4.199 + done
4.200 +
4.201 +lemma mod_nat_sub:
4.202 + "(x :: nat) < z ==> (x - y) mod z = x - y"
4.203 + by (rule nat_mod_eq') arith
4.204 +
4.205 +lemma int_mod_lem:
4.206 + "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
4.207 + apply safe
4.208 + apply (erule (1) mod_pos_pos_trivial)
4.209 + apply (erule_tac [!] subst)
4.210 + apply auto
4.211 + done
4.212 +
4.213 +lemma int_mod_eq:
4.214 + "(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
4.215 + by clarsimp (rule mod_pos_pos_trivial)
4.216 +
4.217 +lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
4.218 +
4.219 +lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
4.220 + apply (cases "a < n")
4.221 + apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a])
4.222 + done
4.223 +
4.224 +lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
4.225 + by (rule int_mod_le [where a = "b - n" and n = n, simplified])
4.226 +
4.227 +lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
4.228 + apply (cases "0 <= a")
4.229 + apply (drule (1) mod_pos_pos_trivial)
4.230 + apply simp
4.231 + apply (rule order_trans [OF _ pos_mod_sign])
4.232 + apply simp
4.233 + apply assumption
4.234 + done
4.235 +
4.236 +lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n"
4.237 + by (rule int_mod_ge [where a = "b + n" and n = n, simplified])
4.238 +
4.239 +lemma mod_add_if_z:
4.240 + "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
4.241 + (x + y) mod z = (if x + y < z then x + y else x + y - z)"
4.242 + by (auto intro: int_mod_eq)
4.243 +
4.244 +lemma mod_sub_if_z:
4.245 + "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
4.246 + (x - y) mod z = (if y <= x then x - y else x - y + z)"
4.247 + by (auto intro: int_mod_eq)
4.248 +
4.249 +lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric]
4.250 +lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
4.251 +
4.252 +(* already have this for naturals, div_mult_self1/2, but not for ints *)
4.253 +lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n"
4.254 + apply (rule mcl)
4.255 + prefer 2
4.256 + apply (erule asm_rl)
4.257 + apply (simp add: zmde ring_distribs)
4.258 + done
4.259 +
4.260 +(** Rep_Integ **)
4.261 +lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
4.262 + unfolding equiv_def refl_on_def quotient_def Image_def by auto
4.263 +
4.264 +lemmas Rep_Integ_ne = Integ.Rep_Integ
4.265 + [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
4.266 +
4.267 +lemmas riq = Integ.Rep_Integ [simplified Integ_def]
4.268 +lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard]
4.269 +lemmas Rep_Integ_equiv = quotient_eq_iff
4.270 + [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard]
4.271 +lemmas Rep_Integ_same =
4.272 + Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard]
4.273 +
4.274 +lemma RI_int: "(a, 0) : Rep_Integ (int a)"
4.275 + unfolding int_def by auto
4.276 +
4.277 +lemmas RI_intrel [simp] = UNIV_I [THEN quotientI,
4.278 + THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard]
4.279 +
4.280 +lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)"
4.281 + apply (rule_tac z=x in eq_Abs_Integ)
4.282 + apply (clarsimp simp: minus)
4.283 + done
4.284 +
4.285 +lemma RI_add:
4.286 + "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==>
4.287 + (a + c, b + d) : Rep_Integ (x + y)"
4.288 + apply (rule_tac z=x in eq_Abs_Integ)
4.289 + apply (rule_tac z=y in eq_Abs_Integ)
4.290 + apply (clarsimp simp: add)
4.291 + done
4.292 +
4.293 +lemma mem_same: "a : S ==> a = b ==> b : S"
4.294 + by fast
4.295 +
4.296 +(* two alternative proofs of this *)
4.297 +lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
4.298 + apply (unfold diff_def)
4.299 + apply (rule mem_same)
4.300 + apply (rule RI_minus RI_add RI_int)+
4.301 + apply simp
4.302 + done
4.303 +
4.304 +lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)"
4.305 + apply safe
4.306 + apply (rule Rep_Integ_same)
4.307 + prefer 2
4.308 + apply (erule asm_rl)
4.309 + apply (rule RI_eq_diff')+
4.310 + done
4.311 +
4.312 +lemma mod_power_lem:
4.313 + "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
4.314 + apply clarsimp
4.315 + apply safe
4.316 + apply (simp add: dvd_eq_mod_eq_0 [symmetric])
4.317 + apply (drule le_iff_add [THEN iffD1])
4.318 + apply (force simp: zpower_zadd_distrib)
4.319 + apply (rule mod_pos_pos_trivial)
4.320 + apply (simp)
4.321 + apply (rule power_strict_increasing)
4.322 + apply auto
4.323 + done
4.324 +
4.325 +lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
4.326 +
4.327 +lemmas min_pm1 [simp] = trans [OF add_commute min_pm]
4.328 +
4.329 +lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith
4.330 +
4.331 +lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm]
4.332 +
4.333 +lemma pl_pl_rels:
4.334 + "a + b = c + d ==>
4.335 + a >= c & b <= d | a <= c & b >= (d :: nat)" by arith
4.336 +
4.337 +lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels]
4.338 +
4.339 +lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))" by arith
4.340 +
4.341 +lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b" by arith
4.342 +
4.343 +lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm]
4.344 +
4.345 +lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
4.346 +
4.347 +lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
4.348 +
4.349 +lemma nat_no_eq_iff:
4.350 + "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==>
4.351 + (number_of b = (number_of c :: nat)) = (b = c)"
4.352 + apply (unfold nat_number_of_def)
4.353 + apply safe
4.354 + apply (drule (2) eq_nat_nat_iff [THEN iffD1])
4.355 + apply (simp add: number_of_eq)
4.356 + done
4.357 +
4.358 +lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]
4.359 +lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
4.360 +lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
4.361 +
4.362 +lemma td_gal:
4.363 + "0 < c ==> (a >= b * c) = (a div c >= (b :: nat))"
4.364 + apply safe
4.365 + apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])
4.366 + apply (erule th2)
4.367 + done
4.368 +
4.369 +lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
4.370 +
4.371 +lemma div_mult_le: "(a :: nat) div b * b <= a"
4.372 + apply (cases b)
4.373 + prefer 2
4.374 + apply (rule order_refl [THEN th2])
4.375 + apply auto
4.376 + done
4.377 +
4.378 +lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
4.379 +
4.380 +lemma given_quot: "f > (0 :: nat) ==> (f * l + (f - 1)) div f = l"
4.381 + by (rule sdl, assumption) (simp (no_asm))
4.382 +
4.383 +lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f - Suc 0) div f = l"
4.384 + apply (frule given_quot)
4.385 + apply (rule trans)
4.386 + prefer 2
4.387 + apply (erule asm_rl)
4.388 + apply (rule_tac f="%n. n div f" in arg_cong)
4.389 + apply (simp add : mult_ac)
4.390 + done
4.391 +
4.392 +lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
4.393 + apply (unfold dvd_def)
4.394 + apply clarify
4.395 + apply (case_tac k)
4.396 + apply clarsimp
4.397 + apply clarify
4.398 + apply (cases "b > 0")
4.399 + apply (drule mult_commute [THEN xtr1])
4.400 + apply (frule (1) td_gal_lt [THEN iffD1])
4.401 + apply (clarsimp simp: le_simps)
4.402 + apply (rule mult_div_cancel [THEN [2] xtr4])
4.403 + apply (rule mult_mono)
4.404 + apply auto
4.405 + done
4.406 +
4.407 +lemma less_le_mult':
4.408 + "w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)"
4.409 + apply (rule mult_right_mono)
4.410 + apply (rule zless_imp_add1_zle)
4.411 + apply (erule (1) mult_right_less_imp_less)
4.412 + apply assumption
4.413 + done
4.414 +
4.415 +lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]
4.416 +
4.417 +lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
4.418 + simplified left_diff_distrib, standard]
4.419 +
4.420 +lemma lrlem':
4.421 + assumes d: "(i::nat) \<le> j \<or> m < j'"
4.422 + assumes R1: "i * k \<le> j * k \<Longrightarrow> R"
4.423 + assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
4.424 + shows "R" using d
4.425 + apply safe
4.426 + apply (rule R1, erule mult_le_mono1)
4.427 + apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
4.428 + done
4.429 +
4.430 +lemma lrlem: "(0::nat) < sc ==>
4.431 + (sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)"
4.432 + apply safe
4.433 + apply arith
4.434 + apply (case_tac "sc >= n")
4.435 + apply arith
4.436 + apply (insert linorder_le_less_linear [of m lb])
4.437 + apply (erule_tac k=n and k'=n in lrlem')
4.438 + apply arith
4.439 + apply simp
4.440 + done
4.441 +
4.442 +lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))"
4.443 + by auto
4.444 +
4.445 +lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i" by arith
4.446 +
4.447 +lemma nonneg_mod_div:
4.448 + "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b"
4.449 + apply (cases "b = 0", clarsimp)
4.450 + apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
4.451 + done
4.452 +
4.453 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Word/Misc_Typedef.thy Wed Jun 30 16:28:14 2010 +0200
5.3 @@ -0,0 +1,228 @@
5.4 +(*
5.5 + Author: Jeremy Dawson and Gerwin Klein, NICTA
5.6 +
5.7 + consequences of type definition theorems,
5.8 + and of extended type definition theorems
5.9 +*)
5.10 +
5.11 +header {* Type Definition Theorems *}
5.12 +
5.13 +theory Misc_Typedef
5.14 +imports Main
5.15 +begin
5.16 +
5.17 +section "More lemmas about normal type definitions"
5.18 +
5.19 +lemma
5.20 + tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and
5.21 + tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and
5.22 + tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
5.23 + by (auto simp: type_definition_def)
5.24 +
5.25 +lemma td_nat_int:
5.26 + "type_definition int nat (Collect (op <= 0))"
5.27 + unfolding type_definition_def by auto
5.28 +
5.29 +context type_definition
5.30 +begin
5.31 +
5.32 +lemmas Rep' [iff] = Rep [simplified] (* if A is given as Collect .. *)
5.33 +
5.34 +declare Rep_inverse [simp] Rep_inject [simp]
5.35 +
5.36 +lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
5.37 + by (simp add: Abs_inject)
5.38 +
5.39 +lemma Abs_inverse':
5.40 + "r : A ==> Abs r = a ==> Rep a = r"
5.41 + by (safe elim!: Abs_inverse)
5.42 +
5.43 +lemma Rep_comp_inverse:
5.44 + "Rep o f = g ==> Abs o g = f"
5.45 + using Rep_inverse by (auto intro: ext)
5.46 +
5.47 +lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
5.48 + by simp
5.49 +
5.50 +lemma Rep_inverse': "Rep a = r ==> Abs r = a"
5.51 + by (safe intro!: Rep_inverse)
5.52 +
5.53 +lemma comp_Abs_inverse:
5.54 + "f o Abs = g ==> g o Rep = f"
5.55 + using Rep_inverse by (auto intro: ext)
5.56 +
5.57 +lemma set_Rep:
5.58 + "A = range Rep"
5.59 +proof (rule set_ext)
5.60 + fix x
5.61 + show "(x \<in> A) = (x \<in> range Rep)"
5.62 + by (auto dest: Abs_inverse [of x, symmetric])
5.63 +qed
5.64 +
5.65 +lemma set_Rep_Abs: "A = range (Rep o Abs)"
5.66 +proof (rule set_ext)
5.67 + fix x
5.68 + show "(x \<in> A) = (x \<in> range (Rep o Abs))"
5.69 + by (auto dest: Abs_inverse [of x, symmetric])
5.70 +qed
5.71 +
5.72 +lemma Abs_inj_on: "inj_on Abs A"
5.73 + unfolding inj_on_def
5.74 + by (auto dest: Abs_inject [THEN iffD1])
5.75 +
5.76 +lemma image: "Abs ` A = UNIV"
5.77 + by (auto intro!: image_eqI)
5.78 +
5.79 +lemmas td_thm = type_definition_axioms
5.80 +
5.81 +lemma fns1:
5.82 + "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
5.83 + by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)
5.84 +
5.85 +lemmas fns1a = disjI1 [THEN fns1]
5.86 +lemmas fns1b = disjI2 [THEN fns1]
5.87 +
5.88 +lemma fns4:
5.89 + "Rep o fa o Abs = fr ==>
5.90 + Rep o fa = fr o Rep & fa o Abs = Abs o fr"
5.91 + by (auto intro!: ext)
5.92 +
5.93 +end
5.94 +
5.95 +interpretation nat_int: type_definition int nat "Collect (op <= 0)"
5.96 + by (rule td_nat_int)
5.97 +
5.98 +declare
5.99 + nat_int.Rep_cases [cases del]
5.100 + nat_int.Abs_cases [cases del]
5.101 + nat_int.Rep_induct [induct del]
5.102 + nat_int.Abs_induct [induct del]
5.103 +
5.104 +
5.105 +subsection "Extended form of type definition predicate"
5.106 +
5.107 +lemma td_conds:
5.108 + "norm o norm = norm ==> (fr o norm = norm o fr) =
5.109 + (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
5.110 + apply safe
5.111 + apply (simp_all add: o_assoc [symmetric])
5.112 + apply (simp_all add: o_assoc)
5.113 + done
5.114 +
5.115 +lemma fn_comm_power:
5.116 + "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n"
5.117 + apply (rule ext)
5.118 + apply (induct n)
5.119 + apply (auto dest: fun_cong)
5.120 + done
5.121 +
5.122 +lemmas fn_comm_power' =
5.123 + ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def, standard]
5.124 +
5.125 +
5.126 +locale td_ext = type_definition +
5.127 + fixes norm
5.128 + assumes eq_norm: "\<And>x. Rep (Abs x) = norm x"
5.129 +begin
5.130 +
5.131 +lemma Abs_norm [simp]:
5.132 + "Abs (norm x) = Abs x"
5.133 + using eq_norm [of x] by (auto elim: Rep_inverse')
5.134 +
5.135 +lemma td_th:
5.136 + "g o Abs = f ==> f (Rep x) = g x"
5.137 + by (drule comp_Abs_inverse [symmetric]) simp
5.138 +
5.139 +lemma eq_norm': "Rep o Abs = norm"
5.140 + by (auto simp: eq_norm intro!: ext)
5.141 +
5.142 +lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
5.143 + by (auto simp: eq_norm' intro: td_th)
5.144 +
5.145 +lemmas td = td_thm
5.146 +
5.147 +lemma set_iff_norm: "w : A <-> w = norm w"
5.148 + by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
5.149 +
5.150 +lemma inverse_norm:
5.151 + "(Abs n = w) = (Rep w = norm n)"
5.152 + apply (rule iffI)
5.153 + apply (clarsimp simp add: eq_norm)
5.154 + apply (simp add: eq_norm' [symmetric])
5.155 + done
5.156 +
5.157 +lemma norm_eq_iff:
5.158 + "(norm x = norm y) = (Abs x = Abs y)"
5.159 + by (simp add: eq_norm' [symmetric])
5.160 +
5.161 +lemma norm_comps:
5.162 + "Abs o norm = Abs"
5.163 + "norm o Rep = Rep"
5.164 + "norm o norm = norm"
5.165 + by (auto simp: eq_norm' [symmetric] o_def)
5.166 +
5.167 +lemmas norm_norm [simp] = norm_comps
5.168 +
5.169 +lemma fns5:
5.170 + "Rep o fa o Abs = fr ==>
5.171 + fr o norm = fr & norm o fr = fr"
5.172 + by (fold eq_norm') (auto intro!: ext)
5.173 +
5.174 +(* following give conditions for converses to td_fns1
5.175 + the condition (norm o fr o norm = fr o norm) says that
5.176 + fr takes normalised arguments to normalised results,
5.177 + (norm o fr o norm = norm o fr) says that fr
5.178 + takes norm-equivalent arguments to norm-equivalent results,
5.179 + (fr o norm = fr) says that fr
5.180 + takes norm-equivalent arguments to the same result, and
5.181 + (norm o fr = fr) says that fr takes any argument to a normalised result
5.182 + *)
5.183 +lemma fns2:
5.184 + "Abs o fr o Rep = fa ==>
5.185 + (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)"
5.186 + apply (fold eq_norm')
5.187 + apply safe
5.188 + prefer 2
5.189 + apply (simp add: o_assoc)
5.190 + apply (rule ext)
5.191 + apply (drule_tac x="Rep x" in fun_cong)
5.192 + apply auto
5.193 + done
5.194 +
5.195 +lemma fns3:
5.196 + "Abs o fr o Rep = fa ==>
5.197 + (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)"
5.198 + apply (fold eq_norm')
5.199 + apply safe
5.200 + prefer 2
5.201 + apply (simp add: o_assoc [symmetric])
5.202 + apply (rule ext)
5.203 + apply (drule fun_cong)
5.204 + apply simp
5.205 + done
5.206 +
5.207 +lemma fns:
5.208 + "fr o norm = norm o fr ==>
5.209 + (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)"
5.210 + apply safe
5.211 + apply (frule fns1b)
5.212 + prefer 2
5.213 + apply (frule fns1a)
5.214 + apply (rule fns3 [THEN iffD1])
5.215 + prefer 3
5.216 + apply (rule fns2 [THEN iffD1])
5.217 + apply (simp_all add: o_assoc [symmetric])
5.218 + apply (simp_all add: o_assoc)
5.219 + done
5.220 +
5.221 +lemma range_norm:
5.222 + "range (Rep o Abs) = A"
5.223 + by (simp add: set_Rep_Abs)
5.224 +
5.225 +end
5.226 +
5.227 +lemmas td_ext_def' =
5.228 + td_ext_def [unfolded type_definition_def td_ext_axioms_def]
5.229 +
5.230 +end
5.231 +
6.1 --- a/src/HOL/Word/Num_Lemmas.thy Wed Jun 30 16:28:13 2010 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,450 +0,0 @@
6.4 -(*
6.5 - Author: Jeremy Dawson, NICTA
6.6 -*)
6.7 -
6.8 -header {* Useful Numerical Lemmas *}
6.9 -
6.10 -theory Num_Lemmas
6.11 -imports Main Parity
6.12 -begin
6.13 -
6.14 -lemma contentsI: "y = {x} ==> contents y = x"
6.15 - unfolding contents_def by auto -- {* FIXME move *}
6.16 -
6.17 -lemmas split_split = prod.split
6.18 -lemmas split_split_asm = prod.split_asm
6.19 -lemmas split_splits = split_split split_split_asm
6.20 -
6.21 -lemmas funpow_0 = funpow.simps(1)
6.22 -lemmas funpow_Suc = funpow.simps(2)
6.23 -
6.24 -lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
6.25 -
6.26 -lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith
6.27 -
6.28 -declare iszero_0 [iff]
6.29 -
6.30 -lemmas xtr1 = xtrans(1)
6.31 -lemmas xtr2 = xtrans(2)
6.32 -lemmas xtr3 = xtrans(3)
6.33 -lemmas xtr4 = xtrans(4)
6.34 -lemmas xtr5 = xtrans(5)
6.35 -lemmas xtr6 = xtrans(6)
6.36 -lemmas xtr7 = xtrans(7)
6.37 -lemmas xtr8 = xtrans(8)
6.38 -
6.39 -lemmas nat_simps = diff_add_inverse2 diff_add_inverse
6.40 -lemmas nat_iffs = le_add1 le_add2
6.41 -
6.42 -lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith
6.43 -
6.44 -lemma nobm1:
6.45 - "0 < (number_of w :: nat) ==>
6.46 - number_of w - (1 :: nat) = number_of (Int.pred w)"
6.47 - apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
6.48 - apply (simp add: number_of_eq nat_diff_distrib [symmetric])
6.49 - done
6.50 -
6.51 -lemma zless2: "0 < (2 :: int)" by arith
6.52 -
6.53 -lemmas zless2p [simp] = zless2 [THEN zero_less_power]
6.54 -lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]
6.55 -
6.56 -lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
6.57 -lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
6.58 -
6.59 --- "the inverse(s) of @{text number_of}"
6.60 -lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith
6.61 -
6.62 -lemma emep1:
6.63 - "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
6.64 - apply (simp add: add_commute)
6.65 - apply (safe dest!: even_equiv_def [THEN iffD1])
6.66 - apply (subst pos_zmod_mult_2)
6.67 - apply arith
6.68 - apply (simp add: mod_mult_mult1)
6.69 - done
6.70 -
6.71 -lemmas eme1p = emep1 [simplified add_commute]
6.72 -
6.73 -lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))" by arith
6.74 -
6.75 -lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith
6.76 -
6.77 -lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))" by arith
6.78 -
6.79 -lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith
6.80 -
6.81 -lemmas m1mod2k = zless2p [THEN zmod_minus1]
6.82 -lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
6.83 -lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2]
6.84 -lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
6.85 -lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
6.86 -
6.87 -lemma p1mod22k:
6.88 - "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)"
6.89 - by (simp add: p1mod22k' add_commute)
6.90 -
6.91 -lemma z1pmod2:
6.92 - "(2 * b + 1) mod 2 = (1::int)" by arith
6.93 -
6.94 -lemma z1pdiv2:
6.95 - "(2 * b + 1) div 2 = (b::int)" by arith
6.96 -
6.97 -lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
6.98 - simplified int_one_le_iff_zero_less, simplified, standard]
6.99 -
6.100 -lemma axxbyy:
6.101 - "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>
6.102 - a = b & m = (n :: int)" by arith
6.103 -
6.104 -lemma axxmod2:
6.105 - "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith
6.106 -
6.107 -lemma axxdiv2:
6.108 - "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)" by arith
6.109 -
6.110 -lemmas iszero_minus = trans [THEN trans,
6.111 - OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard]
6.112 -
6.113 -lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute,
6.114 - standard]
6.115 -
6.116 -lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard]
6.117 -
6.118 -lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b"
6.119 - by (simp add : zmod_zminus1_eq_if)
6.120 -
6.121 -lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
6.122 - apply (unfold diff_int_def)
6.123 - apply (rule trans [OF _ mod_add_eq [symmetric]])
6.124 - apply (simp add: zmod_uminus mod_add_eq [symmetric])
6.125 - done
6.126 -
6.127 -lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
6.128 - apply (unfold diff_int_def)
6.129 - apply (rule trans [OF _ mod_add_right_eq [symmetric]])
6.130 - apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
6.131 - done
6.132 -
6.133 -lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
6.134 - by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
6.135 -
6.136 -lemma zmod_zsub_self [simp]:
6.137 - "((b :: int) - a) mod a = b mod a"
6.138 - by (simp add: zmod_zsub_right_eq)
6.139 -
6.140 -lemma zmod_zmult1_eq_rev:
6.141 - "b * a mod c = b mod c * a mod (c::int)"
6.142 - apply (simp add: mult_commute)
6.143 - apply (subst zmod_zmult1_eq)
6.144 - apply simp
6.145 - done
6.146 -
6.147 -lemmas rdmods [symmetric] = zmod_uminus [symmetric]
6.148 - zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
6.149 - mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
6.150 -
6.151 -lemma mod_plus_right:
6.152 - "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
6.153 - apply (induct x)
6.154 - apply (simp_all add: mod_Suc)
6.155 - apply arith
6.156 - done
6.157 -
6.158 -lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)"
6.159 - by (induct n) (simp_all add : mod_Suc)
6.160 -
6.161 -lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
6.162 - THEN mod_plus_right [THEN iffD2], standard, simplified]
6.163 -
6.164 -lemmas push_mods' = mod_add_eq [standard]
6.165 - mod_mult_eq [standard] zmod_zsub_distrib [standard]
6.166 - zmod_uminus [symmetric, standard]
6.167 -
6.168 -lemmas push_mods = push_mods' [THEN eq_reflection, standard]
6.169 -lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
6.170 -lemmas mod_simps =
6.171 - mod_mult_self2_is_0 [THEN eq_reflection]
6.172 - mod_mult_self1_is_0 [THEN eq_reflection]
6.173 - mod_mod_trivial [THEN eq_reflection]
6.174 -
6.175 -lemma nat_mod_eq:
6.176 - "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"
6.177 - by (induct a) auto
6.178 -
6.179 -lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
6.180 -
6.181 -lemma nat_mod_lem:
6.182 - "(0 :: nat) < n ==> b < n = (b mod n = b)"
6.183 - apply safe
6.184 - apply (erule nat_mod_eq')
6.185 - apply (erule subst)
6.186 - apply (erule mod_less_divisor)
6.187 - done
6.188 -
6.189 -lemma mod_nat_add:
6.190 - "(x :: nat) < z ==> y < z ==>
6.191 - (x + y) mod z = (if x + y < z then x + y else x + y - z)"
6.192 - apply (rule nat_mod_eq)
6.193 - apply auto
6.194 - apply (rule trans)
6.195 - apply (rule le_mod_geq)
6.196 - apply simp
6.197 - apply (rule nat_mod_eq')
6.198 - apply arith
6.199 - done
6.200 -
6.201 -lemma mod_nat_sub:
6.202 - "(x :: nat) < z ==> (x - y) mod z = x - y"
6.203 - by (rule nat_mod_eq') arith
6.204 -
6.205 -lemma int_mod_lem:
6.206 - "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
6.207 - apply safe
6.208 - apply (erule (1) mod_pos_pos_trivial)
6.209 - apply (erule_tac [!] subst)
6.210 - apply auto
6.211 - done
6.212 -
6.213 -lemma int_mod_eq:
6.214 - "(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
6.215 - by clarsimp (rule mod_pos_pos_trivial)
6.216 -
6.217 -lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
6.218 -
6.219 -lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
6.220 - apply (cases "a < n")
6.221 - apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a])
6.222 - done
6.223 -
6.224 -lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
6.225 - by (rule int_mod_le [where a = "b - n" and n = n, simplified])
6.226 -
6.227 -lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
6.228 - apply (cases "0 <= a")
6.229 - apply (drule (1) mod_pos_pos_trivial)
6.230 - apply simp
6.231 - apply (rule order_trans [OF _ pos_mod_sign])
6.232 - apply simp
6.233 - apply assumption
6.234 - done
6.235 -
6.236 -lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n"
6.237 - by (rule int_mod_ge [where a = "b + n" and n = n, simplified])
6.238 -
6.239 -lemma mod_add_if_z:
6.240 - "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
6.241 - (x + y) mod z = (if x + y < z then x + y else x + y - z)"
6.242 - by (auto intro: int_mod_eq)
6.243 -
6.244 -lemma mod_sub_if_z:
6.245 - "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
6.246 - (x - y) mod z = (if y <= x then x - y else x - y + z)"
6.247 - by (auto intro: int_mod_eq)
6.248 -
6.249 -lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric]
6.250 -lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
6.251 -
6.252 -(* already have this for naturals, div_mult_self1/2, but not for ints *)
6.253 -lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n"
6.254 - apply (rule mcl)
6.255 - prefer 2
6.256 - apply (erule asm_rl)
6.257 - apply (simp add: zmde ring_distribs)
6.258 - done
6.259 -
6.260 -(** Rep_Integ **)
6.261 -lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
6.262 - unfolding equiv_def refl_on_def quotient_def Image_def by auto
6.263 -
6.264 -lemmas Rep_Integ_ne = Integ.Rep_Integ
6.265 - [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
6.266 -
6.267 -lemmas riq = Integ.Rep_Integ [simplified Integ_def]
6.268 -lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard]
6.269 -lemmas Rep_Integ_equiv = quotient_eq_iff
6.270 - [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard]
6.271 -lemmas Rep_Integ_same =
6.272 - Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard]
6.273 -
6.274 -lemma RI_int: "(a, 0) : Rep_Integ (int a)"
6.275 - unfolding int_def by auto
6.276 -
6.277 -lemmas RI_intrel [simp] = UNIV_I [THEN quotientI,
6.278 - THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard]
6.279 -
6.280 -lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)"
6.281 - apply (rule_tac z=x in eq_Abs_Integ)
6.282 - apply (clarsimp simp: minus)
6.283 - done
6.284 -
6.285 -lemma RI_add:
6.286 - "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==>
6.287 - (a + c, b + d) : Rep_Integ (x + y)"
6.288 - apply (rule_tac z=x in eq_Abs_Integ)
6.289 - apply (rule_tac z=y in eq_Abs_Integ)
6.290 - apply (clarsimp simp: add)
6.291 - done
6.292 -
6.293 -lemma mem_same: "a : S ==> a = b ==> b : S"
6.294 - by fast
6.295 -
6.296 -(* two alternative proofs of this *)
6.297 -lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
6.298 - apply (unfold diff_def)
6.299 - apply (rule mem_same)
6.300 - apply (rule RI_minus RI_add RI_int)+
6.301 - apply simp
6.302 - done
6.303 -
6.304 -lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)"
6.305 - apply safe
6.306 - apply (rule Rep_Integ_same)
6.307 - prefer 2
6.308 - apply (erule asm_rl)
6.309 - apply (rule RI_eq_diff')+
6.310 - done
6.311 -
6.312 -lemma mod_power_lem:
6.313 - "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
6.314 - apply clarsimp
6.315 - apply safe
6.316 - apply (simp add: dvd_eq_mod_eq_0 [symmetric])
6.317 - apply (drule le_iff_add [THEN iffD1])
6.318 - apply (force simp: zpower_zadd_distrib)
6.319 - apply (rule mod_pos_pos_trivial)
6.320 - apply (simp)
6.321 - apply (rule power_strict_increasing)
6.322 - apply auto
6.323 - done
6.324 -
6.325 -lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
6.326 -
6.327 -lemmas min_pm1 [simp] = trans [OF add_commute min_pm]
6.328 -
6.329 -lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith
6.330 -
6.331 -lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm]
6.332 -
6.333 -lemma pl_pl_rels:
6.334 - "a + b = c + d ==>
6.335 - a >= c & b <= d | a <= c & b >= (d :: nat)" by arith
6.336 -
6.337 -lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels]
6.338 -
6.339 -lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))" by arith
6.340 -
6.341 -lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b" by arith
6.342 -
6.343 -lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm]
6.344 -
6.345 -lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
6.346 -
6.347 -lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
6.348 -
6.349 -lemma nat_no_eq_iff:
6.350 - "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==>
6.351 - (number_of b = (number_of c :: nat)) = (b = c)"
6.352 - apply (unfold nat_number_of_def)
6.353 - apply safe
6.354 - apply (drule (2) eq_nat_nat_iff [THEN iffD1])
6.355 - apply (simp add: number_of_eq)
6.356 - done
6.357 -
6.358 -lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]
6.359 -lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
6.360 -lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
6.361 -
6.362 -lemma td_gal:
6.363 - "0 < c ==> (a >= b * c) = (a div c >= (b :: nat))"
6.364 - apply safe
6.365 - apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])
6.366 - apply (erule th2)
6.367 - done
6.368 -
6.369 -lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
6.370 -
6.371 -lemma div_mult_le: "(a :: nat) div b * b <= a"
6.372 - apply (cases b)
6.373 - prefer 2
6.374 - apply (rule order_refl [THEN th2])
6.375 - apply auto
6.376 - done
6.377 -
6.378 -lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
6.379 -
6.380 -lemma given_quot: "f > (0 :: nat) ==> (f * l + (f - 1)) div f = l"
6.381 - by (rule sdl, assumption) (simp (no_asm))
6.382 -
6.383 -lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f - Suc 0) div f = l"
6.384 - apply (frule given_quot)
6.385 - apply (rule trans)
6.386 - prefer 2
6.387 - apply (erule asm_rl)
6.388 - apply (rule_tac f="%n. n div f" in arg_cong)
6.389 - apply (simp add : mult_ac)
6.390 - done
6.391 -
6.392 -lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
6.393 - apply (unfold dvd_def)
6.394 - apply clarify
6.395 - apply (case_tac k)
6.396 - apply clarsimp
6.397 - apply clarify
6.398 - apply (cases "b > 0")
6.399 - apply (drule mult_commute [THEN xtr1])
6.400 - apply (frule (1) td_gal_lt [THEN iffD1])
6.401 - apply (clarsimp simp: le_simps)
6.402 - apply (rule mult_div_cancel [THEN [2] xtr4])
6.403 - apply (rule mult_mono)
6.404 - apply auto
6.405 - done
6.406 -
6.407 -lemma less_le_mult':
6.408 - "w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)"
6.409 - apply (rule mult_right_mono)
6.410 - apply (rule zless_imp_add1_zle)
6.411 - apply (erule (1) mult_right_less_imp_less)
6.412 - apply assumption
6.413 - done
6.414 -
6.415 -lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]
6.416 -
6.417 -lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
6.418 - simplified left_diff_distrib, standard]
6.419 -
6.420 -lemma lrlem':
6.421 - assumes d: "(i::nat) \<le> j \<or> m < j'"
6.422 - assumes R1: "i * k \<le> j * k \<Longrightarrow> R"
6.423 - assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
6.424 - shows "R" using d
6.425 - apply safe
6.426 - apply (rule R1, erule mult_le_mono1)
6.427 - apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
6.428 - done
6.429 -
6.430 -lemma lrlem: "(0::nat) < sc ==>
6.431 - (sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)"
6.432 - apply safe
6.433 - apply arith
6.434 - apply (case_tac "sc >= n")
6.435 - apply arith
6.436 - apply (insert linorder_le_less_linear [of m lb])
6.437 - apply (erule_tac k=n and k'=n in lrlem')
6.438 - apply arith
6.439 - apply simp
6.440 - done
6.441 -
6.442 -lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))"
6.443 - by auto
6.444 -
6.445 -lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i" by arith
6.446 -
6.447 -lemma nonneg_mod_div:
6.448 - "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b"
6.449 - apply (cases "b = 0", clarsimp)
6.450 - apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
6.451 - done
6.452 -
6.453 -end
7.1 --- a/src/HOL/Word/Size.thy Wed Jun 30 16:28:13 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,71 +0,0 @@
7.4 -(*
7.5 - Author: John Matthews, Galois Connections, Inc., copyright 2006
7.6 -
7.7 - A typeclass for parameterizing types by size.
7.8 - Used primarily to parameterize machine word sizes.
7.9 -*)
7.10 -
7.11 -header "The len classes"
7.12 -
7.13 -theory Size
7.14 -imports Numeral_Type
7.15 -begin
7.16 -
7.17 -text {*
7.18 - The aim of this is to allow any type as index type, but to provide a
7.19 - default instantiation for numeral types. This independence requires
7.20 - some duplication with the definitions in @{text "Numeral_Type"}.
7.21 -*}
7.22 -
7.23 -class len0 =
7.24 - fixes len_of :: "'a itself \<Rightarrow> nat"
7.25 -
7.26 -text {*
7.27 - Some theorems are only true on words with length greater 0.
7.28 -*}
7.29 -
7.30 -class len = len0 +
7.31 - assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
7.32 -
7.33 -instantiation num0 and num1 :: len0
7.34 -begin
7.35 -
7.36 -definition
7.37 - len_num0: "len_of (x::num0 itself) = 0"
7.38 -
7.39 -definition
7.40 - len_num1: "len_of (x::num1 itself) = 1"
7.41 -
7.42 -instance ..
7.43 -
7.44 -end
7.45 -
7.46 -instantiation bit0 and bit1 :: (len0) len0
7.47 -begin
7.48 -
7.49 -definition
7.50 - len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
7.51 -
7.52 -definition
7.53 - len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
7.54 -
7.55 -instance ..
7.56 -
7.57 -end
7.58 -
7.59 -lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
7.60 -
7.61 -instance num1 :: len by (intro_classes) simp
7.62 -instance bit0 :: (len) len by (intro_classes) simp
7.63 -instance bit1 :: (len0) len by (intro_classes) simp
7.64 -
7.65 --- "Examples:"
7.66 -lemma "len_of TYPE(17) = 17" by simp
7.67 -lemma "len_of TYPE(0) = 0" by simp
7.68 -
7.69 --- "not simplified:"
7.70 -lemma "len_of TYPE('a::len0) = x"
7.71 - oops
7.72 -
7.73 -end
7.74 -
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Word/Type_Length.thy Wed Jun 30 16:28:14 2010 +0200
8.3 @@ -0,0 +1,60 @@
8.4 +(* Title: HOL/Word/Type_Length.thy
8.5 + Author: John Matthews, Galois Connections, Inc., copyright 2006
8.6 +*)
8.7 +
8.8 +header {* Assigning lengths to types by typeclasses *}
8.9 +
8.10 +theory Type_Length
8.11 +imports Numeral_Type
8.12 +begin
8.13 +
8.14 +text {*
8.15 + The aim of this is to allow any type as index type, but to provide a
8.16 + default instantiation for numeral types. This independence requires
8.17 + some duplication with the definitions in @{text "Numeral_Type"}.
8.18 +*}
8.19 +
8.20 +class len0 =
8.21 + fixes len_of :: "'a itself \<Rightarrow> nat"
8.22 +
8.23 +text {*
8.24 + Some theorems are only true on words with length greater 0.
8.25 +*}
8.26 +
8.27 +class len = len0 +
8.28 + assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
8.29 +
8.30 +instantiation num0 and num1 :: len0
8.31 +begin
8.32 +
8.33 +definition
8.34 + len_num0: "len_of (x::num0 itself) = 0"
8.35 +
8.36 +definition
8.37 + len_num1: "len_of (x::num1 itself) = 1"
8.38 +
8.39 +instance ..
8.40 +
8.41 +end
8.42 +
8.43 +instantiation bit0 and bit1 :: (len0) len0
8.44 +begin
8.45 +
8.46 +definition
8.47 + len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
8.48 +
8.49 +definition
8.50 + len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
8.51 +
8.52 +instance ..
8.53 +
8.54 +end
8.55 +
8.56 +lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
8.57 +
8.58 +instance num1 :: len proof qed simp
8.59 +instance bit0 :: (len) len proof qed simp
8.60 +instance bit1 :: (len0) len proof qed simp
8.61 +
8.62 +end
8.63 +