# HG changeset patch # User haftmann # Date 1376832590 -7200 # Node ID 3af1a60200145cf61b9abf5f27ce5e3fb5a8c9e2 # Parent 417cb0f713e0c556e67809c7727fef0fe6bee95e some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Bit_Int.thy --- a/src/HOL/Word/Bit_Int.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Bit_Int.thy Sun Aug 18 15:29:50 2013 +0200 @@ -365,7 +365,7 @@ done lemmas int_and_le = - xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] + xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] lemma add_BIT_simps [simp]: (* FIXME: move *) "x BIT 0 + y BIT 0 = (x + y) BIT 0" @@ -553,7 +553,7 @@ (ALL k. bin_nth b k = (k < n & bin_nth c k))" apply (induct n arbitrary: b c) apply clarsimp - apply (clarsimp simp: Let_def split: ls_splits) + apply (clarsimp simp: Let_def split: prod.split_asm) apply (case_tac k) apply auto done @@ -589,11 +589,11 @@ lemma split_bintrunc: "bin_split n c = (a, b) ==> b = bintrunc n c" - by (induct n arbitrary: b c) (auto simp: Let_def split: ls_splits) + by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm) lemma bin_cat_split: "bin_split n w = (u, v) ==> w = bin_cat u n v" - by (induct n arbitrary: v w) (auto simp: Let_def split: ls_splits) + by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm) lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)" @@ -610,18 +610,18 @@ "bin_split (min m n) c = (a, b) ==> bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" apply (induct n arbitrary: m b c, clarsimp) - apply (simp add: bin_rest_trunc Let_def split: ls_splits) + apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) apply (case_tac m) - apply (auto simp: Let_def split: ls_splits) + apply (auto simp: Let_def split: prod.split_asm) done lemma bin_split_trunc1: "bin_split n c = (a, b) ==> bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" apply (induct n arbitrary: m b c, clarsimp) - apply (simp add: bin_rest_trunc Let_def split: ls_splits) + apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) apply (case_tac m) - apply (auto simp: Let_def split: ls_splits) + apply (auto simp: Let_def split: prod.split_asm) done lemma bin_cat_num: @@ -658,3 +658,4 @@ by auto end + diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Bit_Operations.thy --- a/src/HOL/Word/Bit_Operations.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Bit_Operations.thy Sun Aug 18 15:29:50 2013 +0200 @@ -8,6 +8,8 @@ imports "~~/src/HOL/Library/Bit" begin +subsection {* Abstract syntactic bit operations *} + class bit = fixes bitNOT :: "'a \ 'a" ("NOT _" [70] 71) and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) @@ -35,7 +37,7 @@ class bitss = bits + fixes msb :: "'a \ bool" - + subsection {* Bitwise operations on @{typ bit} *} instantiation bit :: bit diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Bit_Representation.thy Sun Aug 18 15:29:50 2013 +0200 @@ -1,16 +1,14 @@ (* Author: Jeremy Dawson, NICTA - - Basic definitions to do with integers, expressed using Pls, Min, BIT. *) -header {* Basic Definitions for Binary Integers *} +header {* Integers as implict bit strings *} theory Bit_Representation -imports Misc_Numeric "~~/src/HOL/Library/Bit" +imports "~~/src/HOL/Library/Bit" Misc_Numeric begin -subsection {* Further properties of numerals *} +subsection {* Constructors and destructors for binary integers *} definition bitval :: "bit \ 'a\zero_neq_one" where "bitval = bit_case 0 1" @@ -23,6 +21,20 @@ definition Bit :: "int \ bit \ int" (infixl "BIT" 90) where "k BIT b = bitval b + k + k" +lemma Bit_B0: + "k BIT (0::bit) = k + k" + by (unfold Bit_def) simp + +lemma Bit_B1: + "k BIT (1::bit) = k + k + 1" + by (unfold Bit_def) simp + +lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" + by (rule trans, rule Bit_B0) simp + +lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" + by (rule trans, rule Bit_B1) simp + definition bin_last :: "int \ bit" where "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))" @@ -99,19 +111,28 @@ "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" unfolding Bit_def by (auto simp add: bitval_def split: bit.split) -lemma Bit_B0: - "k BIT (0::bit) = k + k" - by (unfold Bit_def) simp +lemma pred_BIT_simps [simp]: + "x BIT 0 - 1 = (x - 1) BIT 1" + "x BIT 1 - 1 = x BIT 0" + by (simp_all add: Bit_B0_2t Bit_B1_2t) + +lemma succ_BIT_simps [simp]: + "x BIT 0 + 1 = x BIT 1" + "x BIT 1 + 1 = (x + 1) BIT 0" + by (simp_all add: Bit_B0_2t Bit_B1_2t) -lemma Bit_B1: - "k BIT (1::bit) = k + k + 1" - by (unfold Bit_def) simp - -lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" - by (rule trans, rule Bit_B0) simp +lemma add_BIT_simps [simp]: + "x BIT 0 + y BIT 0 = (x + y) BIT 0" + "x BIT 0 + y BIT 1 = (x + y) BIT 1" + "x BIT 1 + y BIT 0 = (x + y) BIT 1" + "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0" + by (simp_all add: Bit_B0_2t Bit_B1_2t) -lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" - by (rule trans, rule Bit_B1) simp +lemma mult_BIT_simps [simp]: + "x BIT 0 * y = (x * y) BIT 0" + "x * y BIT 0 = (x * y) BIT 0" + "x BIT 1 * y = (x * y) BIT 0 + y" + by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps) lemma B_mod_2': "X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0" @@ -140,9 +161,6 @@ apply force done - -subsection {* Destructors for binary integers *} - primrec bin_nth where Z: "bin_nth w 0 = (bin_last w = (1::bit))" | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" @@ -575,7 +593,7 @@ "sbintrunc (numeral k) 1 = 1" by (simp_all add: sbintrunc_numeral) -lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)" +lemma no_bintr_alt1: "bintrunc n = (\w. w mod 2 ^ n :: int)" by (rule ext) (rule bintrunc_mod2p) lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}" @@ -674,7 +692,7 @@ "(bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)" by (induct n arbitrary: bin) auto -lemma bin_rest_power_trunc [rule_format] : +lemma bin_rest_power_trunc: "(bin_rest ^^ k) (bintrunc n bin) = bintrunc (n - k) ((bin_rest ^^ k) bin)" by (induct k) (auto simp: bin_rest_trunc) @@ -720,17 +738,12 @@ apply simp done -lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" - apply (rule ext) - apply (induct n) - apply (simp_all add: o_def) - done - lemmas rco_bintr = bintrunc_rest' [THEN rco_lem [THEN fun_cong], unfolded o_def] lemmas rco_sbintr = sbintrunc_rest' [THEN rco_lem [THEN fun_cong], unfolded o_def] + subsection {* Splitting and concatenation *} primrec bin_split :: "nat \ int \ int \ int" where @@ -747,59 +760,5 @@ Z: "bin_cat w 0 v = w" | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v" -subsection {* Miscellaneous lemmas *} - -lemma funpow_minus_simp: - "0 < n \ f ^^ n = f \ f ^^ (n - 1)" - by (cases n) simp_all - -lemma funpow_numeral [simp]: - "f ^^ numeral k = f \ f ^^ (pred_numeral k)" - by (simp add: numeral_eq_Suc) - -lemma replicate_numeral [simp]: (* TODO: move to List.thy *) - "replicate (numeral k) x = x # replicate (pred_numeral k) x" - by (simp add: numeral_eq_Suc) - -lemmas power_minus_simp = - trans [OF gen_minus [where f = "power f"] power_Suc] for f - -lemma list_exhaust_size_gt0: - assumes y: "\a list. y = a # list \ P" - shows "0 < length y \ P" - apply (cases y, simp) - apply (rule y) - apply fastforce - done +end -lemma list_exhaust_size_eq0: - assumes y: "y = [] \ P" - shows "length y = 0 \ P" - apply (cases y) - apply (rule y, simp) - apply simp - done - -lemma size_Cons_lem_eq: - "y = xa # list ==> size y = Suc k ==> size list = k" - by auto - -lemmas ls_splits = prod.split prod.split_asm split_if_asm - -lemma not_B1_is_B0: "y \ (1::bit) \ y = (0::bit)" - by (cases y) auto - -lemma B1_ass_B0: - assumes y: "y = (0::bit) \ y = (1::bit)" - shows "y = (1::bit)" - apply (rule classical) - apply (drule not_B1_is_B0) - apply (erule y) - done - --- "simplifications for specific word lengths" -lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' - -lemmas s2n_ths = n2s_ths [symmetric] - -end diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Bool_List_Representation.thy Sun Aug 18 15:29:50 2013 +0200 @@ -12,6 +12,23 @@ imports Bit_Int begin +definition map2 :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" +where + "map2 f as bs = map (split f) (zip as bs)" + +lemma map2_Nil [simp, code]: + "map2 f [] ys = []" + unfolding map2_def by auto + +lemma map2_Nil2 [simp, code]: + "map2 f xs [] = []" + unfolding map2_def by auto + +lemma map2_Cons [simp, code]: + "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" + unfolding map2_def by auto + + subsection {* Operations on lists of booleans *} primrec bl_to_bin_aux :: "bool list \ int \ int" where @@ -40,19 +57,6 @@ case xs of [] => fill # takefill fill n xs | y # ys => y # takefill fill n ys)" -definition map2 :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" where - "map2 f as bs = map (split f) (zip as bs)" - -lemma map2_Nil [simp]: "map2 f [] ys = []" - unfolding map2_def by auto - -lemma map2_Nil2 [simp]: "map2 f xs [] = []" - unfolding map2_def by auto - -lemma map2_Cons [simp]: - "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" - unfolding map2_def by auto - subsection "Arithmetic in terms of bool lists" @@ -314,12 +318,12 @@ apply clarsimp apply clarsimp apply safe - apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+ + apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+ done lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)" apply (unfold bl_to_bin_def) - apply (rule xtr1) + apply (rule xtrans(1)) prefer 2 apply (rule bl_to_bin_lt2p_aux) apply simp @@ -337,7 +341,7 @@ lemma bl_to_bin_ge0: "bl_to_bin bs >= 0" apply (unfold bl_to_bin_def) - apply (rule xtr4) + apply (rule xtrans(4)) apply (rule bl_to_bin_ge2p_aux) apply simp done @@ -534,7 +538,7 @@ bin_to_bl m a = take m (bin_to_bl (m + n) c)" apply (induct n arbitrary: b c) apply clarsimp - apply (clarsimp simp: Let_def split: ls_splits) + apply (clarsimp simp: Let_def split: prod.split_asm) apply (simp add: bin_to_bl_def) apply (simp add: take_bin2bl_lem) done @@ -748,11 +752,6 @@ lemmas rbl_Nils = rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil -lemma pred_BIT_simps [simp]: - "x BIT 0 - 1 = (x - 1) BIT 1" - "x BIT 1 - 1 = x BIT 0" - by (simp_all add: Bit_B0_2t Bit_B1_2t) - lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))" apply (induct n arbitrary: bin, simp) @@ -763,11 +762,6 @@ apply (clarsimp simp: bin_to_bl_aux_alt)+ done -lemma succ_BIT_simps [simp]: - "x BIT 0 + 1 = x BIT 1" - "x BIT 1 + 1 = (x + 1) BIT 0" - by (simp_all add: Bit_B0_2t Bit_B1_2t) - lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" apply (induct n arbitrary: bin, simp) @@ -778,13 +772,6 @@ apply (clarsimp simp: bin_to_bl_aux_alt)+ done -lemma add_BIT_simps [simp]: (* FIXME: move *) - "x BIT 0 + y BIT 0 = (x + y) BIT 0" - "x BIT 0 + y BIT 1 = (x + y) BIT 1" - "x BIT 1 + y BIT 0 = (x + y) BIT 1" - "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0" - by (simp_all add: Bit_B0_2t Bit_B1_2t) - lemma rbl_add: "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina + binb))" @@ -870,12 +857,6 @@ apply (simp add: bin_to_bl_aux_alt) done -lemma mult_BIT_simps [simp]: - "x BIT 0 * y = (x * y) BIT 0" - "x * y BIT 0 = (x * y) BIT 0" - "x BIT 1 * y = (x * y) BIT 0 + y" - by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps) - lemma rbl_mult: "!!bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb))" @@ -907,56 +888,6 @@ (y --> P (rbl_add ws xs)) & (~ y --> P ws))" by (clarsimp simp add : Let_def) -lemma and_len: "xs = ys ==> xs = ys & length xs = length ys" - by auto - -lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)" - by auto - -lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)" - by auto - -lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)" - by auto - -lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))" - by auto - -lemma if_x_Not: "(if p then x else ~ x) = (p = x)" - by auto - -lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)" - by auto - -lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))" - by auto - -lemma if_same_eq_not: - "(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))" - by auto - -(* note - if_Cons can cause blowup in the size, if p is complex, - so make a simproc *) -lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" - by auto - -lemma if_single: - "(if xc then [xab] else [an]) = [if xc then xab else an]" - by auto - -lemma if_bool_simps: - "If p True y = (p | y) & If p False y = (~p & y) & - If p y True = (p --> y) & If p y False = (p & y)" - by auto - -lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps - -lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *) - -(* TODO: move name bindings to List.thy *) -lemmas tl_Nil = tl.simps (1) -lemmas tl_Cons = tl.simps (2) - subsection "Repeated splitting or concatenation" @@ -1008,7 +939,7 @@ apply (induct n m c bs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (subst bin_rsplit_aux.simps) - apply (clarsimp split: ls_splits) + apply (clarsimp split: prod.split) apply auto done @@ -1017,7 +948,7 @@ apply (induct n m c bs rule: bin_rsplitl_aux.induct) apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplitl_aux.simps) - apply (clarsimp split: ls_splits) + apply (clarsimp split: prod.split) apply auto done @@ -1065,7 +996,7 @@ apply clarsimp apply clarsimp apply (drule bthrs) - apply (simp (no_asm_use) add: Let_def split: ls_splits) + apply (simp (no_asm_use) add: Let_def split: prod.split_asm split_if_asm) apply clarify apply (drule split_bintrunc) apply simp @@ -1081,7 +1012,7 @@ apply clarsimp apply clarsimp apply (drule bthrs) - apply (simp (no_asm_use) add: Let_def split: ls_splits) + apply (simp (no_asm_use) add: Let_def split: prod.split_asm split_if_asm) apply clarify apply (erule allE, erule impE, erule exI) apply (case_tac k) @@ -1097,7 +1028,7 @@ lemma bin_rsplit_all: "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]" unfolding bin_rsplit_def - by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: ls_splits) + by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: prod.split) lemma bin_rsplit_l [rule_format] : "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)" @@ -1106,7 +1037,7 @@ apply (rule allI) apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplit_aux.simps) - apply (clarsimp simp: Let_def split: ls_splits) + apply (clarsimp simp: Let_def split: prod.split) apply (drule bin_split_trunc) apply (drule sym [THEN trans], assumption) apply (subst rsplit_aux_alts(1)) @@ -1132,7 +1063,7 @@ length ws \ m \ nw + length bs * n \ m * n" apply (induct n nw w bs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) - apply (simp add: lrlem Let_def split: ls_splits) + apply (simp add: lrlem Let_def split: prod.split) done lemma bin_rsplit_len_le: @@ -1144,7 +1075,7 @@ (nw + n - 1) div n + length cs" apply (induct n nw w cs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) - apply (clarsimp simp: Let_def split: ls_splits) + apply (clarsimp simp: Let_def split: prod.split) apply (erule thin_rl) apply (case_tac m) apply simp @@ -1172,7 +1103,7 @@ by auto show ?thesis using `length bs = length cs` `n \ 0` by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len - split: ls_splits) + split: prod.split) qed qed diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Misc_Numeric.thy --- a/src/HOL/Word/Misc_Numeric.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Misc_Numeric.thy Sun Aug 18 15:29:50 2013 +0200 @@ -8,38 +8,26 @@ imports Main Parity begin -lemma the_elemI: "y = {x} ==> the_elem y = x" - by simp - -lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto - -lemma gt_or_eq_0: "0 < y \ 0 = (y::nat)" by arith +lemma zmod_zsub_self [simp]: (* FIXME move to Divides.thy *) + "((b :: int) - a) mod a = b mod a" + by (simp add: mod_diff_right_eq) 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) +lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith + +lemmas min_pm1 [simp] = trans [OF add_commute min_pm] -lemmas nat_simps = diff_add_inverse2 diff_add_inverse -lemmas nat_iffs = le_add1 le_add2 +lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith -lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith - -lemma zless2: "0 < (2 :: int)" by arith +lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm] -lemmas zless2p = zless2 [THEN zero_less_power] -lemmas zle2p = zless2p [THEN order_less_imp_le] +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] -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"]] - -lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith +lemma z1pmod2: + "(2 * b + 1) mod 2 = (1::int)" by arith lemma emep1: "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1" @@ -50,114 +38,6 @@ 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] - -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]] - -lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute] - -lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2]] - -lemma zmod_zsub_self [simp]: - "((b :: int) - a) mod a = b mod a" - by (simp add: mod_diff_right_eq) - -lemmas rdmods [symmetric] = mod_minus_eq - mod_diff_left_eq mod_diff_right_eq mod_add_left_eq - mod_add_right_eq mod_mult_right_eq mod_mult_left_eq - -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], simplified] - -lemmas push_mods' = mod_add_eq - mod_mult_eq mod_diff_eq - mod_minus_eq - -lemmas push_mods = push_mods' [THEN eq_reflection] -lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection] -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 @@ -166,18 +46,6 @@ 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::int) <= a ==> a mod n <= a" - by (fact zmod_le_nonneg_dividend) (* FIXME: delete *) - -lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n" - using zmod_le_nonneg_dividend [of "b - n" "n"] by simp - lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n" apply (cases "0 <= a") apply (drule (1) mod_pos_pos_trivial) @@ -190,121 +58,36 @@ 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 +lemma zless2: + "0 < (2 :: int)" + by arith -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: power_add) - 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 zless2p: + "0 < (2 ^ n :: int)" + by arith -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 zle2p: + "0 \ (2 ^ n :: int)" + by arith -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 int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n" + using zmod_le_nonneg_dividend [of "b - n" "n"] by simp -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 diff_le_eq': "(a - b \ c) = (a \ b + (c::int))" by arith -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" - by (fact dtle) - -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 m1mod2k: + "-1 mod 2 ^ n = (2 ^ n - 1 :: int)" + using zless2p by (rule zmod_minus1) -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 p1mod22k': + fixes b :: int + shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)" + using zle2p by (rule pos_zmod_mult_2) -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 distrib_right, simplified] - -lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, - simplified left_diff_distrib] +lemma p1mod22k: + fixes b :: int + shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1" + by (simp add: p1mod22k' add_commute) lemma lrlem': assumes d: "(i::nat) \ j \ m < j'" @@ -328,15 +111,5 @@ 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 +end -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 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Misc_Typedef.thy --- a/src/HOL/Word/Misc_Typedef.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Misc_Typedef.thy Sun Aug 18 15:29:50 2013 +0200 @@ -1,7 +1,7 @@ (* Author: Jeremy Dawson and Gerwin Klein, NICTA - Consequences of type definition theorems, and of extended type definition. theorems + Consequences of type definition theorems, and of extended type definition. *) header {* Type Definition Theorems *} diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sun Aug 18 13:58:33 2013 +0200 +++ b/src/HOL/Word/Word.thy Sun Aug 18 15:29:50 2013 +0200 @@ -7,9 +7,10 @@ theory Word imports Type_Length - Misc_Typedef "~~/src/HOL/Library/Boolean_Algebra" Bool_List_Representation + Misc_Typedef + Word_Miscellaneous begin text {* see @{text "Examples/WordExamples.thy"} for examples *} diff -r 417cb0f713e0 -r 3af1a6020014 src/HOL/Word/Word_Miscellaneous.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Word/Word_Miscellaneous.thy Sun Aug 18 15:29:50 2013 +0200 @@ -0,0 +1,389 @@ +(* Title: HOL/Word/Word_Miscellaneous.thy + Author: Miscellaneous +*) + +header {* Miscellaneous lemmas, of at least doubtful value *} + +theory Word_Miscellaneous +imports Main Parity "~~/src/HOL/Library/Bit" Misc_Numeric +begin + +lemma power_minus_simp: + "0 < n \ a ^ n = a * a ^ (n - 1)" + by (auto dest: gr0_implies_Suc) + +lemma funpow_minus_simp: + "0 < n \ f ^^ n = f \ f ^^ (n - 1)" + by (auto dest: gr0_implies_Suc) + +lemma power_numeral: + "a ^ numeral k = a * a ^ (pred_numeral k)" + by (simp add: numeral_eq_Suc) + +lemma funpow_numeral [simp]: + "f ^^ numeral k = f \ f ^^ (pred_numeral k)" + by (simp add: numeral_eq_Suc) + +lemma replicate_numeral [simp]: + "replicate (numeral k) x = x # replicate (pred_numeral k) x" + by (simp add: numeral_eq_Suc) + +lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" + apply (rule ext) + apply (induct n) + apply (simp_all add: o_def) + done + +lemma list_exhaust_size_gt0: + assumes y: "\a list. y = a # list \ P" + shows "0 < length y \ P" + apply (cases y, simp) + apply (rule y) + apply fastforce + done + +lemma list_exhaust_size_eq0: + assumes y: "y = [] \ P" + shows "length y = 0 \ P" + apply (cases y) + apply (rule y, simp) + apply simp + done + +lemma size_Cons_lem_eq: + "y = xa # list ==> size y = Suc k ==> size list = k" + by auto + +lemmas ls_splits = prod.split prod.split_asm split_if_asm + +lemma not_B1_is_B0: "y \ (1::bit) \ y = (0::bit)" + by (cases y) auto + +lemma B1_ass_B0: + assumes y: "y = (0::bit) \ y = (1::bit)" + shows "y = (1::bit)" + apply (rule classical) + apply (drule not_B1_is_B0) + apply (erule y) + done + +-- "simplifications for specific word lengths" +lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' + +lemmas s2n_ths = n2s_ths [symmetric] + +lemma and_len: "xs = ys ==> xs = ys & length xs = length ys" + by auto + +lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)" + by auto + +lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)" + by auto + +lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)" + by auto + +lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))" + by auto + +lemma if_x_Not: "(if p then x else ~ x) = (p = x)" + by auto + +lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)" + by auto + +lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))" + by auto + +lemma if_same_eq_not: + "(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))" + by auto + +(* note - if_Cons can cause blowup in the size, if p is complex, + so make a simproc *) +lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" + by auto + +lemma if_single: + "(if xc then [xab] else [an]) = [if xc then xab else an]" + by auto + +lemma if_bool_simps: + "If p True y = (p | y) & If p False y = (~p & y) & + If p y True = (p --> y) & If p y False = (p & y)" + by auto + +lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps + +lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *) + +(* TODO: move name bindings to List.thy *) +lemmas tl_Nil = tl.simps (1) +lemmas tl_Cons = tl.simps (2) + +lemma the_elemI: "y = {x} ==> the_elem y = x" + by simp + +lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto + +lemma gt_or_eq_0: "0 < y \ 0 = (y::nat)" by arith + +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 + +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"]] + +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_less_eq': "(a - b < c) = (a < b + (c::int))" by arith + +lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1] +lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified] +lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified] + +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] + +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]] + +lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute] + +lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2]] + +lemmas rdmods [symmetric] = mod_minus_eq + mod_diff_left_eq mod_diff_right_eq mod_add_left_eq + mod_add_right_eq mod_mult_right_eq mod_mult_left_eq + +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], simplified] + +lemmas push_mods' = mod_add_eq + mod_mult_eq mod_diff_eq + mod_minus_eq + +lemmas push_mods = push_mods' [THEN eq_reflection] +lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection] +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::int) <= a ==> a mod n <= a" + by (fact zmod_le_nonneg_dividend) (* FIXME: delete *) + +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 + +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: power_add) + apply (rule mod_pos_pos_trivial) + apply (simp) + apply (rule power_strict_increasing) + apply auto + done + +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] + +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" + by (fact dtle) + +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 distrib_right, simplified] + +lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, + simplified left_diff_distrib] + +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 +