# HG changeset patch # User haftmann # Date 1277908094 -7200 # Node ID f4d616d41a595e4d730ed357d701406b20410afa # Parent 8e33b9d04a82ddeabe12aa026e4364a8d2692dc0 more speaking theory names diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/IsaMakefile Wed Jun 30 16:28:14 2010 +0200 @@ -397,8 +397,8 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL $(SRC)/HOL/Tools/float_arith.ML \ $(SRC)/Tools/float.ML Library/Abstract_Rat.thy Library/AssocList.thy \ Library/BigO.thy Library/Binomial.thy Library/Bit.thy \ - Library/Boolean_Algebra.thy Library/Char_nat.thy \ - Library/Code_Char.thy Library/Code_Char_chr.thy \ + Library/Boolean_Algebra.thy Library/Cardinality.thy \ + Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy Library/Code_Integer.thy Library/ContNotDenum.thy \ Library/Continuity.thy Library/Convex.thy Library/Countable.thy \ Library/Diagonalize.thy Library/Dlist.thy Library/Efficient_Nat.thy \ @@ -1191,9 +1191,9 @@ HOL-Word: HOL $(OUT)/HOL-Word $(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \ - Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \ - Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \ - Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy \ + Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \ + Word/Type_Length.thy Word/BinGeneral.thy Word/BinOperations.thy \ + Word/BinBoolList.thy Word/Bit_Operations.thy Word/WordDefinition.thy \ Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy \ Word/WordGenLib.thy Word/Word.thy Word/document/root.tex \ Word/document/root.bib Tools/SMT/smt_word.ML diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/BitSyntax.thy --- a/src/HOL/Word/BitSyntax.thy Wed Jun 30 16:28:13 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ -(* - Author: Brian Huffman, PSU and Gerwin Klein, NICTA - - Syntactic class for bitwise operations. -*) - - -header {* Syntactic classes for bitwise operations *} - -theory BitSyntax -imports BinGeneral -begin - -class bit = - fixes bitNOT :: "'a \ 'a" ("NOT _" [70] 71) - and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) - and bitOR :: "'a \ 'a \ 'a" (infixr "OR" 59) - and bitXOR :: "'a \ 'a \ 'a" (infixr "XOR" 59) - -text {* - We want the bitwise operations to bind slightly weaker - than @{text "+"} and @{text "-"}, but @{text "~~"} to - bind slightly stronger than @{text "*"}. -*} - -text {* - Testing and shifting operations. -*} - -class bits = bit + - fixes test_bit :: "'a \ nat \ bool" (infixl "!!" 100) - and lsb :: "'a \ bool" - and set_bit :: "'a \ nat \ bool \ 'a" - and set_bits :: "(nat \ bool) \ 'a" (binder "BITS " 10) - and shiftl :: "'a \ nat \ 'a" (infixl "<<" 55) - and shiftr :: "'a \ nat \ 'a" (infixl ">>" 55) - -class bitss = bits + - fixes msb :: "'a \ bool" - - -subsection {* Bitwise operations on @{typ bit} *} - -instantiation bit :: bit -begin - -primrec bitNOT_bit where - "NOT bit.B0 = bit.B1" - | "NOT bit.B1 = bit.B0" - -primrec bitAND_bit where - "bit.B0 AND y = bit.B0" - | "bit.B1 AND y = y" - -primrec bitOR_bit where - "bit.B0 OR y = y" - | "bit.B1 OR y = bit.B1" - -primrec bitXOR_bit where - "bit.B0 XOR y = y" - | "bit.B1 XOR y = NOT y" - -instance .. - -end - -lemmas bit_simps = - bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps - -lemma bit_extra_simps [simp]: - "x AND bit.B0 = bit.B0" - "x AND bit.B1 = x" - "x OR bit.B1 = bit.B1" - "x OR bit.B0 = x" - "x XOR bit.B1 = NOT x" - "x XOR bit.B0 = x" - by (cases x, auto)+ - -lemma bit_ops_comm: - "(x::bit) AND y = y AND x" - "(x::bit) OR y = y OR x" - "(x::bit) XOR y = y XOR x" - by (cases y, auto)+ - -lemma bit_ops_same [simp]: - "(x::bit) AND x = x" - "(x::bit) OR x = x" - "(x::bit) XOR x = bit.B0" - by (cases x, auto)+ - -lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x" - by (cases x) auto - -end diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/Bit_Operations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Word/Bit_Operations.thy Wed Jun 30 16:28:14 2010 +0200 @@ -0,0 +1,91 @@ +(* Title: HOL/Word/Bit_Operations.thy + Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA +*) + +header {* Syntactic classes for bitwise operations *} + +theory Bit_Operations +imports Bit +begin + +class bit = + fixes bitNOT :: "'a \ 'a" ("NOT _" [70] 71) + and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) + and bitOR :: "'a \ 'a \ 'a" (infixr "OR" 59) + and bitXOR :: "'a \ 'a \ 'a" (infixr "XOR" 59) + +text {* + We want the bitwise operations to bind slightly weaker + than @{text "+"} and @{text "-"}, but @{text "~~"} to + bind slightly stronger than @{text "*"}. +*} + +text {* + Testing and shifting operations. +*} + +class bits = bit + + fixes test_bit :: "'a \ nat \ bool" (infixl "!!" 100) + and lsb :: "'a \ bool" + and set_bit :: "'a \ nat \ bool \ 'a" + and set_bits :: "(nat \ bool) \ 'a" (binder "BITS " 10) + and shiftl :: "'a \ nat \ 'a" (infixl "<<" 55) + and shiftr :: "'a \ nat \ 'a" (infixl ">>" 55) + +class bitss = bits + + fixes msb :: "'a \ bool" + + +subsection {* Bitwise operations on @{typ bit} *} + +instantiation bit :: bit +begin + +primrec bitNOT_bit where + "NOT 0 = (1::bit)" + | "NOT 1 = (0::bit)" + +primrec bitAND_bit where + "0 AND y = (0::bit)" + | "1 AND y = (y::bit)" + +primrec bitOR_bit where + "0 OR y = (y::bit)" + | "1 OR y = (1::bit)" + +primrec bitXOR_bit where + "0 XOR y = (y::bit)" + | "1 XOR y = (NOT y :: bit)" + +instance .. + +end + +lemmas bit_simps = + bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps + +lemma bit_extra_simps [simp]: + "x AND 0 = (0::bit)" + "x AND 1 = (x::bit)" + "x OR 1 = (1::bit)" + "x OR 0 = (x::bit)" + "x XOR 1 = NOT (x::bit)" + "x XOR 0 = (x::bit)" + by (cases x, auto)+ + +lemma bit_ops_comm: + "(x::bit) AND y = y AND x" + "(x::bit) OR y = y OR x" + "(x::bit) XOR y = y XOR x" + by (cases y, auto)+ + +lemma bit_ops_same [simp]: + "(x::bit) AND x = x" + "(x::bit) OR x = x" + "(x::bit) XOR x = 0" + by (cases x, auto)+ + +lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x" + by (cases x) auto + +end diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/Misc_Numeric.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Word/Misc_Numeric.thy Wed Jun 30 16:28:14 2010 +0200 @@ -0,0 +1,450 @@ +(* + Author: Jeremy Dawson, NICTA +*) + +header {* Useful Numerical Lemmas *} + +theory Misc_Numeric +imports Main Parity +begin + +lemma contentsI: "y = {x} ==> contents y = x" + unfolding contents_def by auto -- {* FIXME move *} + +lemmas split_split = prod.split +lemmas split_split_asm = prod.split_asm +lemmas split_splits = split_split split_split_asm + +lemmas funpow_0 = funpow.simps(1) +lemmas funpow_Suc = funpow.simps(2) + +lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto + +lemma gt_or_eq_0: "0 < y \ 0 = (y::nat)" by arith + +declare iszero_0 [iff] + +lemmas xtr1 = xtrans(1) +lemmas xtr2 = xtrans(2) +lemmas xtr3 = xtrans(3) +lemmas xtr4 = xtrans(4) +lemmas xtr5 = xtrans(5) +lemmas xtr6 = xtrans(6) +lemmas xtr7 = xtrans(7) +lemmas xtr8 = xtrans(8) + +lemmas nat_simps = diff_add_inverse2 diff_add_inverse +lemmas nat_iffs = le_add1 le_add2 + +lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith + +lemma nobm1: + "0 < (number_of w :: nat) ==> + number_of w - (1 :: nat) = number_of (Int.pred w)" + apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def) + apply (simp add: number_of_eq nat_diff_distrib [symmetric]) + done + +lemma zless2: "0 < (2 :: int)" by arith + +lemmas zless2p [simp] = zless2 [THEN zero_less_power] +lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] + +lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] +lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] + +-- "the inverse(s) of @{text number_of}" +lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith + +lemma emep1: + "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" + apply (simp add: add_commute) + apply (safe dest!: even_equiv_def [THEN iffD1]) + apply (subst pos_zmod_mult_2) + apply arith + apply (simp add: mod_mult_mult1) + done + +lemmas eme1p = emep1 [simplified add_commute] + +lemma le_diff_eq': "(a \ c - b) = (b + a \ (c::int))" by arith + +lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith + +lemma diff_le_eq': "(a - b \ c) = (a \ b + (c::int))" by arith + +lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith + +lemmas m1mod2k = zless2p [THEN zmod_minus1] +lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] +lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2] +lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified] +lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified] + +lemma p1mod22k: + "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)" + by (simp add: p1mod22k' add_commute) + +lemma z1pmod2: + "(2 * b + 1) mod 2 = (1::int)" by arith + +lemma z1pdiv2: + "(2 * b + 1) div 2 = (b::int)" by arith + +lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, + simplified int_one_le_iff_zero_less, simplified, standard] + +lemma axxbyy: + "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==> + a = b & m = (n :: int)" by arith + +lemma axxmod2: + "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith + +lemma axxdiv2: + "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)" by arith + +lemmas iszero_minus = trans [THEN trans, + OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard] + +lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute, + standard] + +lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard] + +lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b" + by (simp add : zmod_zminus1_eq_if) + +lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c" + apply (unfold diff_int_def) + apply (rule trans [OF _ mod_add_eq [symmetric]]) + apply (simp add: zmod_uminus mod_add_eq [symmetric]) + done + +lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c" + apply (unfold diff_int_def) + apply (rule trans [OF _ mod_add_right_eq [symmetric]]) + apply (simp add : zmod_uminus mod_add_right_eq [symmetric]) + done + +lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c" + by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]]) + +lemma zmod_zsub_self [simp]: + "((b :: int) - a) mod a = b mod a" + by (simp add: zmod_zsub_right_eq) + +lemma zmod_zmult1_eq_rev: + "b * a mod c = b mod c * a mod (c::int)" + apply (simp add: mult_commute) + apply (subst zmod_zmult1_eq) + apply simp + done + +lemmas rdmods [symmetric] = zmod_uminus [symmetric] + zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq + mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev + +lemma mod_plus_right: + "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))" + apply (induct x) + apply (simp_all add: mod_Suc) + apply arith + done + +lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)" + by (induct n) (simp_all add : mod_Suc) + +lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric], + THEN mod_plus_right [THEN iffD2], standard, simplified] + +lemmas push_mods' = mod_add_eq [standard] + mod_mult_eq [standard] zmod_zsub_distrib [standard] + zmod_uminus [symmetric, standard] + +lemmas push_mods = push_mods' [THEN eq_reflection, standard] +lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard] +lemmas mod_simps = + mod_mult_self2_is_0 [THEN eq_reflection] + mod_mult_self1_is_0 [THEN eq_reflection] + mod_mod_trivial [THEN eq_reflection] + +lemma nat_mod_eq: + "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)" + by (induct a) auto + +lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq] + +lemma nat_mod_lem: + "(0 :: nat) < n ==> b < n = (b mod n = b)" + apply safe + apply (erule nat_mod_eq') + apply (erule subst) + apply (erule mod_less_divisor) + done + +lemma mod_nat_add: + "(x :: nat) < z ==> y < z ==> + (x + y) mod z = (if x + y < z then x + y else x + y - z)" + apply (rule nat_mod_eq) + apply auto + apply (rule trans) + apply (rule le_mod_geq) + apply simp + apply (rule nat_mod_eq') + apply arith + done + +lemma mod_nat_sub: + "(x :: nat) < z ==> (x - y) mod z = x - y" + by (rule nat_mod_eq') arith + +lemma int_mod_lem: + "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)" + apply safe + apply (erule (1) mod_pos_pos_trivial) + apply (erule_tac [!] subst) + apply auto + done + +lemma int_mod_eq: + "(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b" + by clarsimp (rule mod_pos_pos_trivial) + +lemmas int_mod_eq' = refl [THEN [3] int_mod_eq] + +lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a" + apply (cases "a < n") + apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a]) + done + +lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n" + by (rule int_mod_le [where a = "b - n" and n = n, simplified]) + +lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n" + apply (cases "0 <= a") + apply (drule (1) mod_pos_pos_trivial) + apply simp + apply (rule order_trans [OF _ pos_mod_sign]) + apply simp + apply assumption + done + +lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n" + by (rule int_mod_ge [where a = "b + n" and n = n, simplified]) + +lemma mod_add_if_z: + "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> + (x + y) mod z = (if x + y < z then x + y else x + y - z)" + by (auto intro: int_mod_eq) + +lemma mod_sub_if_z: + "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> + (x - y) mod z = (if y <= x then x - y else x - y + z)" + by (auto intro: int_mod_eq) + +lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric] +lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule] + +(* already have this for naturals, div_mult_self1/2, but not for ints *) +lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n" + apply (rule mcl) + prefer 2 + apply (erule asm_rl) + apply (simp add: zmde ring_distribs) + done + +(** Rep_Integ **) +lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}" + unfolding equiv_def refl_on_def quotient_def Image_def by auto + +lemmas Rep_Integ_ne = Integ.Rep_Integ + [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard] + +lemmas riq = Integ.Rep_Integ [simplified Integ_def] +lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard] +lemmas Rep_Integ_equiv = quotient_eq_iff + [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard] +lemmas Rep_Integ_same = + Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard] + +lemma RI_int: "(a, 0) : Rep_Integ (int a)" + unfolding int_def by auto + +lemmas RI_intrel [simp] = UNIV_I [THEN quotientI, + THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard] + +lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)" + apply (rule_tac z=x in eq_Abs_Integ) + apply (clarsimp simp: minus) + done + +lemma RI_add: + "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==> + (a + c, b + d) : Rep_Integ (x + y)" + apply (rule_tac z=x in eq_Abs_Integ) + apply (rule_tac z=y in eq_Abs_Integ) + apply (clarsimp simp: add) + done + +lemma mem_same: "a : S ==> a = b ==> b : S" + by fast + +(* two alternative proofs of this *) +lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)" + apply (unfold diff_def) + apply (rule mem_same) + apply (rule RI_minus RI_add RI_int)+ + apply simp + done + +lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)" + apply safe + apply (rule Rep_Integ_same) + prefer 2 + apply (erule asm_rl) + apply (rule RI_eq_diff')+ + done + +lemma mod_power_lem: + "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)" + apply clarsimp + apply safe + apply (simp add: dvd_eq_mod_eq_0 [symmetric]) + apply (drule le_iff_add [THEN iffD1]) + apply (force simp: zpower_zadd_distrib) + apply (rule mod_pos_pos_trivial) + apply (simp) + apply (rule power_strict_increasing) + apply auto + done + +lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith + +lemmas min_pm1 [simp] = trans [OF add_commute min_pm] + +lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith + +lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] + +lemma pl_pl_rels: + "a + b = c + d ==> + a >= c & b <= d | a <= c & b >= (d :: nat)" by arith + +lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels] + +lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))" by arith + +lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b" by arith + +lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm] + +lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith + +lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus] + +lemma nat_no_eq_iff: + "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==> + (number_of b = (number_of c :: nat)) = (b = c)" + apply (unfold nat_number_of_def) + apply safe + apply (drule (2) eq_nat_nat_iff [THEN iffD1]) + apply (simp add: number_of_eq) + done + +lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right] +lemmas dtle = xtr3 [OF dme [symmetric] le_add1] +lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle] + +lemma td_gal: + "0 < c ==> (a >= b * c) = (a div c >= (b :: nat))" + apply safe + apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m]) + apply (erule th2) + done + +lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified] + +lemma div_mult_le: "(a :: nat) div b * b <= a" + apply (cases b) + prefer 2 + apply (rule order_refl [THEN th2]) + apply auto + done + +lemmas sdl = split_div_lemma [THEN iffD1, symmetric] + +lemma given_quot: "f > (0 :: nat) ==> (f * l + (f - 1)) div f = l" + by (rule sdl, assumption) (simp (no_asm)) + +lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f - Suc 0) div f = l" + apply (frule given_quot) + apply (rule trans) + prefer 2 + apply (erule asm_rl) + apply (rule_tac f="%n. n div f" in arg_cong) + apply (simp add : mult_ac) + done + +lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b" + apply (unfold dvd_def) + apply clarify + apply (case_tac k) + apply clarsimp + apply clarify + apply (cases "b > 0") + apply (drule mult_commute [THEN xtr1]) + apply (frule (1) td_gal_lt [THEN iffD1]) + apply (clarsimp simp: le_simps) + apply (rule mult_div_cancel [THEN [2] xtr4]) + apply (rule mult_mono) + apply auto + done + +lemma less_le_mult': + "w * c < b * c ==> 0 \ c ==> (w + 1) * c \ b * (c::int)" + apply (rule mult_right_mono) + apply (rule zless_imp_add1_zle) + apply (erule (1) mult_right_less_imp_less) + apply assumption + done + +lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified] + +lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, + simplified left_diff_distrib, standard] + +lemma lrlem': + assumes d: "(i::nat) \ j \ m < j'" + assumes R1: "i * k \ j * k \ R" + assumes R2: "Suc m * k' \ j' * k' \ R" + shows "R" using d + apply safe + apply (rule R1, erule mult_le_mono1) + apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) + done + +lemma lrlem: "(0::nat) < sc ==> + (sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)" + apply safe + apply arith + apply (case_tac "sc >= n") + apply arith + apply (insert linorder_le_less_linear [of m lb]) + apply (erule_tac k=n and k'=n in lrlem') + apply arith + apply simp + done + +lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))" + by auto + +lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i" by arith + +lemma nonneg_mod_div: + "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b" + apply (cases "b = 0", clarsimp) + apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2]) + done + +end diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/Misc_Typedef.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Word/Misc_Typedef.thy Wed Jun 30 16:28:14 2010 +0200 @@ -0,0 +1,228 @@ +(* + Author: Jeremy Dawson and Gerwin Klein, NICTA + + consequences of type definition theorems, + and of extended type definition theorems +*) + +header {* Type Definition Theorems *} + +theory Misc_Typedef +imports Main +begin + +section "More lemmas about normal type definitions" + +lemma + tdD1: "type_definition Rep Abs A \ \x. Rep x \ A" and + tdD2: "type_definition Rep Abs A \ \x. Abs (Rep x) = x" and + tdD3: "type_definition Rep Abs A \ \y. y \ A \ Rep (Abs y) = y" + by (auto simp: type_definition_def) + +lemma td_nat_int: + "type_definition int nat (Collect (op <= 0))" + unfolding type_definition_def by auto + +context type_definition +begin + +lemmas Rep' [iff] = Rep [simplified] (* if A is given as Collect .. *) + +declare Rep_inverse [simp] Rep_inject [simp] + +lemma Abs_eqD: "Abs x = Abs y ==> x \ A ==> y \ A ==> x = y" + by (simp add: Abs_inject) + +lemma Abs_inverse': + "r : A ==> Abs r = a ==> Rep a = r" + by (safe elim!: Abs_inverse) + +lemma Rep_comp_inverse: + "Rep o f = g ==> Abs o g = f" + using Rep_inverse by (auto intro: ext) + +lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y" + by simp + +lemma Rep_inverse': "Rep a = r ==> Abs r = a" + by (safe intro!: Rep_inverse) + +lemma comp_Abs_inverse: + "f o Abs = g ==> g o Rep = f" + using Rep_inverse by (auto intro: ext) + +lemma set_Rep: + "A = range Rep" +proof (rule set_ext) + fix x + show "(x \ A) = (x \ range Rep)" + by (auto dest: Abs_inverse [of x, symmetric]) +qed + +lemma set_Rep_Abs: "A = range (Rep o Abs)" +proof (rule set_ext) + fix x + show "(x \ A) = (x \ range (Rep o Abs))" + by (auto dest: Abs_inverse [of x, symmetric]) +qed + +lemma Abs_inj_on: "inj_on Abs A" + unfolding inj_on_def + by (auto dest: Abs_inject [THEN iffD1]) + +lemma image: "Abs ` A = UNIV" + by (auto intro!: image_eqI) + +lemmas td_thm = type_definition_axioms + +lemma fns1: + "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa" + by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) + +lemmas fns1a = disjI1 [THEN fns1] +lemmas fns1b = disjI2 [THEN fns1] + +lemma fns4: + "Rep o fa o Abs = fr ==> + Rep o fa = fr o Rep & fa o Abs = Abs o fr" + by (auto intro!: ext) + +end + +interpretation nat_int: type_definition int nat "Collect (op <= 0)" + by (rule td_nat_int) + +declare + nat_int.Rep_cases [cases del] + nat_int.Abs_cases [cases del] + nat_int.Rep_induct [induct del] + nat_int.Abs_induct [induct del] + + +subsection "Extended form of type definition predicate" + +lemma td_conds: + "norm o norm = norm ==> (fr o norm = norm o fr) = + (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)" + apply safe + apply (simp_all add: o_assoc [symmetric]) + apply (simp_all add: o_assoc) + done + +lemma fn_comm_power: + "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n" + apply (rule ext) + apply (induct n) + apply (auto dest: fun_cong) + done + +lemmas fn_comm_power' = + ext [THEN fn_comm_power, THEN fun_cong, unfolded o_def, standard] + + +locale td_ext = type_definition + + fixes norm + assumes eq_norm: "\x. Rep (Abs x) = norm x" +begin + +lemma Abs_norm [simp]: + "Abs (norm x) = Abs x" + using eq_norm [of x] by (auto elim: Rep_inverse') + +lemma td_th: + "g o Abs = f ==> f (Rep x) = g x" + by (drule comp_Abs_inverse [symmetric]) simp + +lemma eq_norm': "Rep o Abs = norm" + by (auto simp: eq_norm intro!: ext) + +lemma norm_Rep [simp]: "norm (Rep x) = Rep x" + by (auto simp: eq_norm' intro: td_th) + +lemmas td = td_thm + +lemma set_iff_norm: "w : A <-> w = norm w" + by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric]) + +lemma inverse_norm: + "(Abs n = w) = (Rep w = norm n)" + apply (rule iffI) + apply (clarsimp simp add: eq_norm) + apply (simp add: eq_norm' [symmetric]) + done + +lemma norm_eq_iff: + "(norm x = norm y) = (Abs x = Abs y)" + by (simp add: eq_norm' [symmetric]) + +lemma norm_comps: + "Abs o norm = Abs" + "norm o Rep = Rep" + "norm o norm = norm" + by (auto simp: eq_norm' [symmetric] o_def) + +lemmas norm_norm [simp] = norm_comps + +lemma fns5: + "Rep o fa o Abs = fr ==> + fr o norm = fr & norm o fr = fr" + by (fold eq_norm') (auto intro!: ext) + +(* following give conditions for converses to td_fns1 + the condition (norm o fr o norm = fr o norm) says that + fr takes normalised arguments to normalised results, + (norm o fr o norm = norm o fr) says that fr + takes norm-equivalent arguments to norm-equivalent results, + (fr o norm = fr) says that fr + takes norm-equivalent arguments to the same result, and + (norm o fr = fr) says that fr takes any argument to a normalised result + *) +lemma fns2: + "Abs o fr o Rep = fa ==> + (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)" + apply (fold eq_norm') + apply safe + prefer 2 + apply (simp add: o_assoc) + apply (rule ext) + apply (drule_tac x="Rep x" in fun_cong) + apply auto + done + +lemma fns3: + "Abs o fr o Rep = fa ==> + (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)" + apply (fold eq_norm') + apply safe + prefer 2 + apply (simp add: o_assoc [symmetric]) + apply (rule ext) + apply (drule fun_cong) + apply simp + done + +lemma fns: + "fr o norm = norm o fr ==> + (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)" + apply safe + apply (frule fns1b) + prefer 2 + apply (frule fns1a) + apply (rule fns3 [THEN iffD1]) + prefer 3 + apply (rule fns2 [THEN iffD1]) + apply (simp_all add: o_assoc [symmetric]) + apply (simp_all add: o_assoc) + done + +lemma range_norm: + "range (Rep o Abs) = A" + by (simp add: set_Rep_Abs) + +end + +lemmas td_ext_def' = + td_ext_def [unfolded type_definition_def td_ext_axioms_def] + +end + diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Wed Jun 30 16:28:13 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,450 +0,0 @@ -(* - Author: Jeremy Dawson, NICTA -*) - -header {* Useful Numerical Lemmas *} - -theory Num_Lemmas -imports Main Parity -begin - -lemma contentsI: "y = {x} ==> contents y = x" - unfolding contents_def by auto -- {* FIXME move *} - -lemmas split_split = prod.split -lemmas split_split_asm = prod.split_asm -lemmas split_splits = split_split split_split_asm - -lemmas funpow_0 = funpow.simps(1) -lemmas funpow_Suc = funpow.simps(2) - -lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto - -lemma gt_or_eq_0: "0 < y \ 0 = (y::nat)" by arith - -declare iszero_0 [iff] - -lemmas xtr1 = xtrans(1) -lemmas xtr2 = xtrans(2) -lemmas xtr3 = xtrans(3) -lemmas xtr4 = xtrans(4) -lemmas xtr5 = xtrans(5) -lemmas xtr6 = xtrans(6) -lemmas xtr7 = xtrans(7) -lemmas xtr8 = xtrans(8) - -lemmas nat_simps = diff_add_inverse2 diff_add_inverse -lemmas nat_iffs = le_add1 le_add2 - -lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith - -lemma nobm1: - "0 < (number_of w :: nat) ==> - number_of w - (1 :: nat) = number_of (Int.pred w)" - apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def) - apply (simp add: number_of_eq nat_diff_distrib [symmetric]) - done - -lemma zless2: "0 < (2 :: int)" by arith - -lemmas zless2p [simp] = zless2 [THEN zero_less_power] -lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] - -lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]] -lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]] - --- "the inverse(s) of @{text number_of}" -lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith - -lemma emep1: - "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" - apply (simp add: add_commute) - apply (safe dest!: even_equiv_def [THEN iffD1]) - apply (subst pos_zmod_mult_2) - apply arith - apply (simp add: mod_mult_mult1) - done - -lemmas eme1p = emep1 [simplified add_commute] - -lemma le_diff_eq': "(a \ c - b) = (b + a \ (c::int))" by arith - -lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith - -lemma diff_le_eq': "(a - b \ c) = (a \ b + (c::int))" by arith - -lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith - -lemmas m1mod2k = zless2p [THEN zmod_minus1] -lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] -lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2] -lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified] -lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified] - -lemma p1mod22k: - "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)" - by (simp add: p1mod22k' add_commute) - -lemma z1pmod2: - "(2 * b + 1) mod 2 = (1::int)" by arith - -lemma z1pdiv2: - "(2 * b + 1) div 2 = (b::int)" by arith - -lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, - simplified int_one_le_iff_zero_less, simplified, standard] - -lemma axxbyy: - "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==> - a = b & m = (n :: int)" by arith - -lemma axxmod2: - "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith - -lemma axxdiv2: - "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)" by arith - -lemmas iszero_minus = trans [THEN trans, - OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard] - -lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute, - standard] - -lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard] - -lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b" - by (simp add : zmod_zminus1_eq_if) - -lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c" - apply (unfold diff_int_def) - apply (rule trans [OF _ mod_add_eq [symmetric]]) - apply (simp add: zmod_uminus mod_add_eq [symmetric]) - done - -lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c" - apply (unfold diff_int_def) - apply (rule trans [OF _ mod_add_right_eq [symmetric]]) - apply (simp add : zmod_uminus mod_add_right_eq [symmetric]) - done - -lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c" - by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]]) - -lemma zmod_zsub_self [simp]: - "((b :: int) - a) mod a = b mod a" - by (simp add: zmod_zsub_right_eq) - -lemma zmod_zmult1_eq_rev: - "b * a mod c = b mod c * a mod (c::int)" - apply (simp add: mult_commute) - apply (subst zmod_zmult1_eq) - apply simp - done - -lemmas rdmods [symmetric] = zmod_uminus [symmetric] - zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq - mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev - -lemma mod_plus_right: - "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))" - apply (induct x) - apply (simp_all add: mod_Suc) - apply arith - done - -lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)" - by (induct n) (simp_all add : mod_Suc) - -lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric], - THEN mod_plus_right [THEN iffD2], standard, simplified] - -lemmas push_mods' = mod_add_eq [standard] - mod_mult_eq [standard] zmod_zsub_distrib [standard] - zmod_uminus [symmetric, standard] - -lemmas push_mods = push_mods' [THEN eq_reflection, standard] -lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard] -lemmas mod_simps = - mod_mult_self2_is_0 [THEN eq_reflection] - mod_mult_self1_is_0 [THEN eq_reflection] - mod_mod_trivial [THEN eq_reflection] - -lemma nat_mod_eq: - "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)" - by (induct a) auto - -lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq] - -lemma nat_mod_lem: - "(0 :: nat) < n ==> b < n = (b mod n = b)" - apply safe - apply (erule nat_mod_eq') - apply (erule subst) - apply (erule mod_less_divisor) - done - -lemma mod_nat_add: - "(x :: nat) < z ==> y < z ==> - (x + y) mod z = (if x + y < z then x + y else x + y - z)" - apply (rule nat_mod_eq) - apply auto - apply (rule trans) - apply (rule le_mod_geq) - apply simp - apply (rule nat_mod_eq') - apply arith - done - -lemma mod_nat_sub: - "(x :: nat) < z ==> (x - y) mod z = x - y" - by (rule nat_mod_eq') arith - -lemma int_mod_lem: - "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)" - apply safe - apply (erule (1) mod_pos_pos_trivial) - apply (erule_tac [!] subst) - apply auto - done - -lemma int_mod_eq: - "(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b" - by clarsimp (rule mod_pos_pos_trivial) - -lemmas int_mod_eq' = refl [THEN [3] int_mod_eq] - -lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a" - apply (cases "a < n") - apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a]) - done - -lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n" - by (rule int_mod_le [where a = "b - n" and n = n, simplified]) - -lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n" - apply (cases "0 <= a") - apply (drule (1) mod_pos_pos_trivial) - apply simp - apply (rule order_trans [OF _ pos_mod_sign]) - apply simp - apply assumption - done - -lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n" - by (rule int_mod_ge [where a = "b + n" and n = n, simplified]) - -lemma mod_add_if_z: - "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> - (x + y) mod z = (if x + y < z then x + y else x + y - z)" - by (auto intro: int_mod_eq) - -lemma mod_sub_if_z: - "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> - (x - y) mod z = (if y <= x then x - y else x - y + z)" - by (auto intro: int_mod_eq) - -lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric] -lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule] - -(* already have this for naturals, div_mult_self1/2, but not for ints *) -lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n" - apply (rule mcl) - prefer 2 - apply (erule asm_rl) - apply (simp add: zmde ring_distribs) - done - -(** Rep_Integ **) -lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}" - unfolding equiv_def refl_on_def quotient_def Image_def by auto - -lemmas Rep_Integ_ne = Integ.Rep_Integ - [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard] - -lemmas riq = Integ.Rep_Integ [simplified Integ_def] -lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard] -lemmas Rep_Integ_equiv = quotient_eq_iff - [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard] -lemmas Rep_Integ_same = - Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard] - -lemma RI_int: "(a, 0) : Rep_Integ (int a)" - unfolding int_def by auto - -lemmas RI_intrel [simp] = UNIV_I [THEN quotientI, - THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard] - -lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)" - apply (rule_tac z=x in eq_Abs_Integ) - apply (clarsimp simp: minus) - done - -lemma RI_add: - "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==> - (a + c, b + d) : Rep_Integ (x + y)" - apply (rule_tac z=x in eq_Abs_Integ) - apply (rule_tac z=y in eq_Abs_Integ) - apply (clarsimp simp: add) - done - -lemma mem_same: "a : S ==> a = b ==> b : S" - by fast - -(* two alternative proofs of this *) -lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)" - apply (unfold diff_def) - apply (rule mem_same) - apply (rule RI_minus RI_add RI_int)+ - apply simp - done - -lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)" - apply safe - apply (rule Rep_Integ_same) - prefer 2 - apply (erule asm_rl) - apply (rule RI_eq_diff')+ - done - -lemma mod_power_lem: - "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)" - apply clarsimp - apply safe - apply (simp add: dvd_eq_mod_eq_0 [symmetric]) - apply (drule le_iff_add [THEN iffD1]) - apply (force simp: zpower_zadd_distrib) - apply (rule mod_pos_pos_trivial) - apply (simp) - apply (rule power_strict_increasing) - apply auto - done - -lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith - -lemmas min_pm1 [simp] = trans [OF add_commute min_pm] - -lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith - -lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] - -lemma pl_pl_rels: - "a + b = c + d ==> - a >= c & b <= d | a <= c & b >= (d :: nat)" by arith - -lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels] - -lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))" by arith - -lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b" by arith - -lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm] - -lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith - -lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus] - -lemma nat_no_eq_iff: - "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==> - (number_of b = (number_of c :: nat)) = (b = c)" - apply (unfold nat_number_of_def) - apply safe - apply (drule (2) eq_nat_nat_iff [THEN iffD1]) - apply (simp add: number_of_eq) - done - -lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right] -lemmas dtle = xtr3 [OF dme [symmetric] le_add1] -lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle] - -lemma td_gal: - "0 < c ==> (a >= b * c) = (a div c >= (b :: nat))" - apply safe - apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m]) - apply (erule th2) - done - -lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified] - -lemma div_mult_le: "(a :: nat) div b * b <= a" - apply (cases b) - prefer 2 - apply (rule order_refl [THEN th2]) - apply auto - done - -lemmas sdl = split_div_lemma [THEN iffD1, symmetric] - -lemma given_quot: "f > (0 :: nat) ==> (f * l + (f - 1)) div f = l" - by (rule sdl, assumption) (simp (no_asm)) - -lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f - Suc 0) div f = l" - apply (frule given_quot) - apply (rule trans) - prefer 2 - apply (erule asm_rl) - apply (rule_tac f="%n. n div f" in arg_cong) - apply (simp add : mult_ac) - done - -lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b" - apply (unfold dvd_def) - apply clarify - apply (case_tac k) - apply clarsimp - apply clarify - apply (cases "b > 0") - apply (drule mult_commute [THEN xtr1]) - apply (frule (1) td_gal_lt [THEN iffD1]) - apply (clarsimp simp: le_simps) - apply (rule mult_div_cancel [THEN [2] xtr4]) - apply (rule mult_mono) - apply auto - done - -lemma less_le_mult': - "w * c < b * c ==> 0 \ c ==> (w + 1) * c \ b * (c::int)" - apply (rule mult_right_mono) - apply (rule zless_imp_add1_zle) - apply (erule (1) mult_right_less_imp_less) - apply assumption - done - -lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified] - -lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, - simplified left_diff_distrib, standard] - -lemma lrlem': - assumes d: "(i::nat) \ j \ m < j'" - assumes R1: "i * k \ j * k \ R" - assumes R2: "Suc m * k' \ j' * k' \ R" - shows "R" using d - apply safe - apply (rule R1, erule mult_le_mono1) - apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) - done - -lemma lrlem: "(0::nat) < sc ==> - (sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)" - apply safe - apply arith - apply (case_tac "sc >= n") - apply arith - apply (insert linorder_le_less_linear [of m lb]) - apply (erule_tac k=n and k'=n in lrlem') - apply arith - apply simp - done - -lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))" - by auto - -lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i" by arith - -lemma nonneg_mod_div: - "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b" - apply (cases "b = 0", clarsimp) - apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2]) - done - -end diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/Size.thy --- a/src/HOL/Word/Size.thy Wed Jun 30 16:28:13 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,71 +0,0 @@ -(* - Author: John Matthews, Galois Connections, Inc., copyright 2006 - - A typeclass for parameterizing types by size. - Used primarily to parameterize machine word sizes. -*) - -header "The len classes" - -theory Size -imports Numeral_Type -begin - -text {* - The aim of this is to allow any type as index type, but to provide a - default instantiation for numeral types. This independence requires - some duplication with the definitions in @{text "Numeral_Type"}. -*} - -class len0 = - fixes len_of :: "'a itself \ nat" - -text {* - Some theorems are only true on words with length greater 0. -*} - -class len = len0 + - assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)" - -instantiation num0 and num1 :: len0 -begin - -definition - len_num0: "len_of (x::num0 itself) = 0" - -definition - len_num1: "len_of (x::num1 itself) = 1" - -instance .. - -end - -instantiation bit0 and bit1 :: (len0) len0 -begin - -definition - len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)" - -definition - len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1" - -instance .. - -end - -lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 - -instance num1 :: len by (intro_classes) simp -instance bit0 :: (len) len by (intro_classes) simp -instance bit1 :: (len0) len by (intro_classes) simp - --- "Examples:" -lemma "len_of TYPE(17) = 17" by simp -lemma "len_of TYPE(0) = 0" by simp - --- "not simplified:" -lemma "len_of TYPE('a::len0) = x" - oops - -end - diff -r 8e33b9d04a82 -r f4d616d41a59 src/HOL/Word/Type_Length.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Word/Type_Length.thy Wed Jun 30 16:28:14 2010 +0200 @@ -0,0 +1,60 @@ +(* Title: HOL/Word/Type_Length.thy + Author: John Matthews, Galois Connections, Inc., copyright 2006 +*) + +header {* Assigning lengths to types by typeclasses *} + +theory Type_Length +imports Numeral_Type +begin + +text {* + The aim of this is to allow any type as index type, but to provide a + default instantiation for numeral types. This independence requires + some duplication with the definitions in @{text "Numeral_Type"}. +*} + +class len0 = + fixes len_of :: "'a itself \ nat" + +text {* + Some theorems are only true on words with length greater 0. +*} + +class len = len0 + + assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)" + +instantiation num0 and num1 :: len0 +begin + +definition + len_num0: "len_of (x::num0 itself) = 0" + +definition + len_num1: "len_of (x::num1 itself) = 1" + +instance .. + +end + +instantiation bit0 and bit1 :: (len0) len0 +begin + +definition + len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)" + +definition + len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1" + +instance .. + +end + +lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 + +instance num1 :: len proof qed simp +instance bit0 :: (len) len proof qed simp +instance bit1 :: (len0) len proof qed simp + +end +