--- a/src/HOL/Word/Word.thy Wed Mar 15 17:24:48 2017 +0100
+++ b/src/HOL/Word/Word.thy Wed Mar 15 19:33:34 2017 +0100
@@ -21,44 +21,35 @@
typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
morphisms uint Abs_word by auto
-lemma uint_nonnegative:
- "0 \<le> uint w"
+lemma uint_nonnegative: "0 \<le> uint w"
using word.uint [of w] by simp
-lemma uint_bounded:
- fixes w :: "'a::len0 word"
- shows "uint w < 2 ^ len_of TYPE('a)"
+lemma uint_bounded: "uint w < 2 ^ len_of TYPE('a)"
+ for w :: "'a::len0 word"
using word.uint [of w] by simp
-lemma uint_idem:
- fixes w :: "'a::len0 word"
- shows "uint w mod 2 ^ len_of TYPE('a) = uint w"
+lemma uint_idem: "uint w mod 2 ^ len_of TYPE('a) = uint w"
+ for w :: "'a::len0 word"
using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
-lemma word_uint_eq_iff:
- "a = b \<longleftrightarrow> uint a = uint b"
+lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
by (simp add: uint_inject)
-lemma word_uint_eqI:
- "uint a = uint b \<Longrightarrow> a = b"
+lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
by (simp add: word_uint_eq_iff)
definition word_of_int :: "int \<Rightarrow> 'a::len0 word"
-where
\<comment> \<open>representation of words using unsigned or signed bins,
only difference in these is the type class\<close>
- "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
-
-lemma uint_word_of_int:
- "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ len_of TYPE('a)"
+ where "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
+
+lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ len_of TYPE('a)"
by (auto simp add: word_of_int_def intro: Abs_word_inverse)
-lemma word_of_int_uint:
- "word_of_int (uint w) = w"
+lemma word_of_int_uint: "word_of_int (uint w) = w"
by (simp add: word_of_int_def uint_idem uint_inverse)
-lemma split_word_all:
- "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
+lemma split_word_all: "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
proof
fix x :: "'a word"
assume "\<And>x. PROP P (word_of_int x)"
@@ -70,112 +61,93 @@
subsection \<open>Type conversions and casting\<close>
definition sint :: "'a::len word \<Rightarrow> int"
-where
\<comment> \<open>treats the most-significant-bit as a sign bit\<close>
- sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
+ where sint_uint: "sint w = sbintrunc (len_of TYPE('a) - 1) (uint w)"
definition unat :: "'a::len0 word \<Rightarrow> nat"
-where
- "unat w = nat (uint w)"
+ where "unat w = nat (uint w)"
definition uints :: "nat \<Rightarrow> int set"
-where
\<comment> "the sets of integers representing the words"
- "uints n = range (bintrunc n)"
+ where "uints n = range (bintrunc n)"
definition sints :: "nat \<Rightarrow> int set"
-where
- "sints n = range (sbintrunc (n - 1))"
-
-lemma uints_num:
- "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
+ where "sints n = range (sbintrunc (n - 1))"
+
+lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
by (simp add: uints_def range_bintrunc)
-lemma sints_num:
- "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
+lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
by (simp add: sints_def range_sbintrunc)
definition unats :: "nat \<Rightarrow> nat set"
-where
- "unats n = {i. i < 2 ^ n}"
+ where "unats n = {i. i < 2 ^ n}"
definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int"
-where
- "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
+ where "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
definition scast :: "'a::len word \<Rightarrow> 'b::len word"
-where
\<comment> "cast a word to a different length"
- "scast w = word_of_int (sint w)"
+ where "scast w = word_of_int (sint w)"
definition ucast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
-where
- "ucast w = word_of_int (uint w)"
+ where "ucast w = word_of_int (uint w)"
instantiation word :: (len0) size
begin
-definition
- word_size: "size (w :: 'a word) = len_of TYPE('a)"
+definition word_size: "size (w :: 'a word) = len_of TYPE('a)"
instance ..
end
-lemma word_size_gt_0 [iff]:
- "0 < size (w::'a::len word)"
+lemma word_size_gt_0 [iff]: "0 < size w"
+ for w :: "'a::len word"
by (simp add: word_size)
lemmas lens_gt_0 = word_size_gt_0 len_gt_0
lemma lens_not_0 [iff]:
- shows "size (w::'a::len word) \<noteq> 0"
- and "len_of TYPE('a::len) \<noteq> 0"
+ fixes w :: "'a::len word"
+ shows "size w \<noteq> 0"
+ and "len_of TYPE('a) \<noteq> 0"
by auto
definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
-where
\<comment> "whether a cast (or other) function is to a longer or shorter length"
- [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"
+ where [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"
definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"
-where
- [code del]: "target_size c = size (c undefined)"
+ where [code del]: "target_size c = size (c undefined)"
definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
-where
- "is_up c \<longleftrightarrow> source_size c \<le> target_size c"
-
-definition is_down :: "('a :: len0 word \<Rightarrow> 'b :: len0 word) \<Rightarrow> bool"
-where
- "is_down c \<longleftrightarrow> target_size c \<le> source_size c"
+ where "is_up c \<longleftrightarrow> source_size c \<le> target_size c"
+
+definition is_down :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
+ where "is_down c \<longleftrightarrow> target_size c \<le> source_size c"
definition of_bl :: "bool list \<Rightarrow> 'a::len0 word"
-where
- "of_bl bl = word_of_int (bl_to_bin bl)"
+ where "of_bl bl = word_of_int (bl_to_bin bl)"
definition to_bl :: "'a::len0 word \<Rightarrow> bool list"
-where
- "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
+ where "to_bl w = bin_to_bl (len_of TYPE('a)) (uint w)"
definition word_reverse :: "'a::len0 word \<Rightarrow> 'a word"
-where
- "word_reverse w = of_bl (rev (to_bl w))"
-
-definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b"
-where
- "word_int_case f w = f (uint w)"
+ where "word_reverse w = of_bl (rev (to_bl w))"
+
+definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b"
+ where "word_int_case f w = f (uint w)"
translations
- "case x of XCONST of_int y => b" == "CONST word_int_case (%y. b) x"
- "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
+ "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x"
+ "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x"
subsection \<open>Correspondence relation for theorem transfer\<close>
definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
-where
- "cr_word = (\<lambda>x y. word_of_int x = y)"
+ where "cr_word = (\<lambda>x y. word_of_int x = y)"
lemma Quotient_word:
"Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
@@ -192,8 +164,7 @@
text \<open>TODO: The next lemma could be generated automatically.\<close>
lemma uint_transfer [transfer_rule]:
- "(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a)))
- (uint :: 'a::len0 word \<Rightarrow> int)"
+ "(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a))) (uint :: 'a::len0 word \<Rightarrow> int)"
unfolding rel_fun_def word.pcr_cr_eq cr_word_def
by (simp add: no_bintr_alt1 uint_word_of_int)
@@ -201,11 +172,9 @@
subsection \<open>Basic code generation setup\<close>
definition Word :: "int \<Rightarrow> 'a::len0 word"
-where
- [code_post]: "Word = word_of_int"
-
-lemma [code abstype]:
- "Word (uint w) = w"
+ where [code_post]: "Word = word_of_int"
+
+lemma [code abstype]: "Word (uint w) = w"
by (simp add: Word_def word_of_int_uint)
declare uint_word_of_int [code abstract]
@@ -214,11 +183,10 @@
begin
definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
-where
- "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
-
-instance proof
-qed (simp add: equal equal_word_def word_uint_eq_iff)
+ where "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
+
+instance
+ by standard (simp add: equal equal_word_def word_uint_eq_iff)
end
@@ -247,8 +215,8 @@
lemmas uint_lt = uint_bounded (* FIXME duplicate *)
lemmas uint_mod_same = uint_idem (* FIXME duplicate *)
-lemma td_ext_uint:
- "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))
+lemma td_ext_uint:
+ "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))
(\<lambda>w::int. w mod 2 ^ len_of TYPE('a))"
apply (unfold td_ext_def')
apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
@@ -257,10 +225,11 @@
done
interpretation word_uint:
- td_ext "uint::'a::len0 word \<Rightarrow> int"
- word_of_int
- "uints (len_of TYPE('a::len0))"
- "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
+ td_ext
+ "uint::'a::len0 word \<Rightarrow> int"
+ word_of_int
+ "uints (len_of TYPE('a::len0))"
+ "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
by (fact td_ext_uint)
lemmas td_uint = word_uint.td_thm
@@ -272,10 +241,11 @@
by (unfold no_bintr_alt1) (fact td_ext_uint)
interpretation word_ubin:
- td_ext "uint::'a::len0 word \<Rightarrow> int"
- word_of_int
- "uints (len_of TYPE('a::len0))"
- "bintrunc (len_of TYPE('a::len0))"
+ td_ext
+ "uint::'a::len0 word \<Rightarrow> int"
+ word_of_int
+ "uints (len_of TYPE('a::len0))"
+ "bintrunc (len_of TYPE('a::len0))"
by (fact td_ext_ubin)
@@ -319,27 +289,26 @@
text \<open>Legacy theorems:\<close>
-lemma word_arith_wis [code]: shows
- word_add_def: "a + b = word_of_int (uint a + uint b)" and
- word_sub_wi: "a - b = word_of_int (uint a - uint b)" and
- word_mult_def: "a * b = word_of_int (uint a * uint b)" and
- word_minus_def: "- a = word_of_int (- uint a)" and
- word_succ_alt: "word_succ a = word_of_int (uint a + 1)" and
- word_pred_alt: "word_pred a = word_of_int (uint a - 1)" and
- word_0_wi: "0 = word_of_int 0" and
- word_1_wi: "1 = word_of_int 1"
+lemma word_arith_wis [code]:
+ shows word_add_def: "a + b = word_of_int (uint a + uint b)"
+ and word_sub_wi: "a - b = word_of_int (uint a - uint b)"
+ and word_mult_def: "a * b = word_of_int (uint a * uint b)"
+ and word_minus_def: "- a = word_of_int (- uint a)"
+ and word_succ_alt: "word_succ a = word_of_int (uint a + 1)"
+ and word_pred_alt: "word_pred a = word_of_int (uint a - 1)"
+ and word_0_wi: "0 = word_of_int 0"
+ and word_1_wi: "1 = word_of_int 1"
unfolding plus_word_def minus_word_def times_word_def uminus_word_def
unfolding word_succ_def word_pred_def zero_word_def one_word_def
by simp_all
-lemma wi_homs:
- shows
- wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
- wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" and
- wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
- wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
- wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
- wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
+lemma wi_homs:
+ shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)"
+ and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)"
+ and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)"
+ and wi_hom_neg: "- word_of_int a = word_of_int (- a)"
+ and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)"
+ and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
by (transfer, simp)+
lemmas wi_hom_syms = wi_homs [symmetric]
@@ -350,9 +319,9 @@
instance word :: (len) comm_ring_1
proof
- have "0 < len_of TYPE('a)" by (rule len_gt_0)
- then show "(0::'a word) \<noteq> 1"
- by - (transfer, auto simp add: gr0_conv_Suc)
+ have *: "0 < len_of TYPE('a)" by (rule len_gt_0)
+ show "(0::'a word) \<noteq> 1"
+ by transfer (use * in \<open>auto simp add: gr0_conv_Suc\<close>)
qed
lemma word_of_nat: "of_nat n = word_of_int (int n)"
@@ -364,9 +333,8 @@
apply (simp add: word_of_nat wi_hom_sub)
done
-definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
-where
- "a udvd b = (EX n>=0. uint b = n * uint a)"
+definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50)
+ where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)"
subsection \<open>Ordering\<close>
@@ -374,24 +342,20 @@
instantiation word :: (len0) linorder
begin
-definition
- word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
-
-definition
- word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
+definition word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
+
+definition word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
instance
by standard (auto simp: word_less_def word_le_def)
end
-definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
-where
- "a <=s b = (sint a <= sint b)"
-
-definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
-where
- "(x <s y) = (x <=s y & x ~= y)"
+definition word_sle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <=s _)" [50, 51] 50)
+ where "a <=s b \<longleftrightarrow> sint a \<le> sint b"
+
+definition word_sless :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <s _)" [50, 51] 50)
+ where "x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y"
subsection \<open>Bit-wise operations\<close>
@@ -411,167 +375,130 @@
lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitXOR
by (metis bin_trunc_xor)
-definition
- word_test_bit_def: "test_bit a = bin_nth (uint a)"
-
-definition
- word_set_bit_def: "set_bit a n x =
- word_of_int (bin_sc n x (uint a))"
-
-definition
- word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"
-
-definition
- word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
+definition word_test_bit_def: "test_bit a = bin_nth (uint a)"
+
+definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
+
+definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE('a)) f)"
+
+definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
definition shiftl1 :: "'a word \<Rightarrow> 'a word"
-where
- "shiftl1 w = word_of_int (uint w BIT False)"
+ where "shiftl1 w = word_of_int (uint w BIT False)"
definition shiftr1 :: "'a word \<Rightarrow> 'a word"
where
\<comment> "shift right as unsigned or as signed, ie logical or arithmetic"
"shiftr1 w = word_of_int (bin_rest (uint w))"
-definition
- shiftl_def: "w << n = (shiftl1 ^^ n) w"
-
-definition
- shiftr_def: "w >> n = (shiftr1 ^^ n) w"
+definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
+
+definition shiftr_def: "w >> n = (shiftr1 ^^ n) w"
instance ..
end
-lemma [code]: shows
- word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))" and
- word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and
- word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and
- word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
- unfolding bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def
- by simp_all
+lemma [code]:
+ shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))"
+ and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
+ and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)"
+ and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
+ by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def)
instantiation word :: (len) bitss
begin
-definition
- word_msb_def:
- "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
+definition word_msb_def: "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
instance ..
end
-definition setBit :: "'a :: len0 word => nat => 'a word"
-where
- "setBit w n = set_bit w n True"
-
-definition clearBit :: "'a :: len0 word => nat => 'a word"
-where
- "clearBit w n = set_bit w n False"
+definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
+ where "setBit w n = set_bit w n True"
+
+definition clearBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
+ where "clearBit w n = set_bit w n False"
subsection \<open>Shift operations\<close>
-definition sshiftr1 :: "'a :: len word => 'a word"
-where
- "sshiftr1 w = word_of_int (bin_rest (sint w))"
-
-definition bshiftr1 :: "bool => 'a :: len word => 'a word"
-where
- "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
-
-definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
-where
- "w >>> n = (sshiftr1 ^^ n) w"
-
-definition mask :: "nat => 'a::len word"
-where
- "mask n = (1 << n) - 1"
-
-definition revcast :: "'a :: len0 word => 'b :: len0 word"
-where
- "revcast w = of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
-
-definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
-where
- "slice1 n w = of_bl (takefill False n (to_bl w))"
-
-definition slice :: "nat => 'a :: len0 word => 'b :: len0 word"
-where
- "slice n w = slice1 (size w - n) w"
+definition sshiftr1 :: "'a::len word \<Rightarrow> 'a word"
+ where "sshiftr1 w = word_of_int (bin_rest (sint w))"
+
+definition bshiftr1 :: "bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word"
+ where "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
+
+definition sshiftr :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" (infixl ">>>" 55)
+ where "w >>> n = (sshiftr1 ^^ n) w"
+
+definition mask :: "nat \<Rightarrow> 'a::len word"
+ where "mask n = (1 << n) - 1"
+
+definition revcast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+ where "revcast w = of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
+
+definition slice1 :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"
+ where "slice1 n w = of_bl (takefill False n (to_bl w))"
+
+definition slice :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"
+ where "slice n w = slice1 (size w - n) w"
subsection \<open>Rotation\<close>
-definition rotater1 :: "'a list => 'a list"
-where
- "rotater1 ys =
- (case ys of [] => [] | x # xs => last ys # butlast ys)"
-
-definition rotater :: "nat => 'a list => 'a list"
-where
- "rotater n = rotater1 ^^ n"
-
-definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
-where
- "word_rotr n w = of_bl (rotater n (to_bl w))"
-
-definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"
-where
- "word_rotl n w = of_bl (rotate n (to_bl w))"
-
-definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word"
-where
- "word_roti i w = (if i >= 0 then word_rotr (nat i) w
- else word_rotl (nat (- i)) w)"
+definition rotater1 :: "'a list \<Rightarrow> 'a list"
+ where "rotater1 ys =
+ (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)"
+
+definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ where "rotater n = rotater1 ^^ n"
+
+definition word_rotr :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word"
+ where "word_rotr n w = of_bl (rotater n (to_bl w))"
+
+definition word_rotl :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word"
+ where "word_rotl n w = of_bl (rotate n (to_bl w))"
+
+definition word_roti :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word"
+ where "word_roti i w =
+ (if i \<ge> 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)"
subsection \<open>Split and cat operations\<close>
-definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
-where
- "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
-
-definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"
-where
- "word_split a =
- (case bin_split (len_of TYPE ('c)) (uint a) of
- (u, v) => (word_of_int u, word_of_int v))"
-
-definition word_rcat :: "'a :: len0 word list => 'b :: len0 word"
-where
- "word_rcat ws =
- word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
-
-definition word_rsplit :: "'a :: len0 word => 'b :: len word list"
-where
- "word_rsplit w =
- map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
-
-definition max_word :: "'a::len word" \<comment> "Largest representable machine integer."
-where
- "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
+definition word_cat :: "'a::len0 word \<Rightarrow> 'b::len0 word \<Rightarrow> 'c::len0 word"
+ where "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE('b)) (uint b))"
+
+definition word_split :: "'a::len0 word \<Rightarrow> 'b::len0 word \<times> 'c::len0 word"
+ where "word_split a =
+ (case bin_split (len_of TYPE('c)) (uint a) of
+ (u, v) \<Rightarrow> (word_of_int u, word_of_int v))"
+
+definition word_rcat :: "'a::len0 word list \<Rightarrow> 'b::len0 word"
+ where "word_rcat ws = word_of_int (bin_rcat (len_of TYPE('a)) (map uint ws))"
+
+definition word_rsplit :: "'a::len0 word \<Rightarrow> 'b::len word list"
+ where "word_rsplit w = map word_of_int (bin_rsplit (len_of TYPE('b)) (len_of TYPE('a), uint w))"
+
+definition max_word :: "'a::len word" \<comment> "Largest representable machine integer."
+ where "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
subsection \<open>Theorems about typedefs\<close>
-lemma sint_sbintrunc':
- "sint (word_of_int bin :: 'a word) =
- (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
- unfolding sint_uint
- by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt)
-
-lemma uint_sint:
- "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))"
- unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
-
-lemma bintr_uint:
- fixes w :: "'a::len0 word"
- shows "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
- apply (subst word_ubin.norm_Rep [symmetric])
+lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) bin"
+ by (auto simp: sint_uint word_ubin.eq_norm sbintrunc_bintrunc_lt)
+
+lemma uint_sint: "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a::len word))"
+ by (auto simp: sint_uint bintrunc_sbintrunc_le)
+
+lemma bintr_uint: "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
+ for w :: "'a::len0 word"
+ apply (subst word_ubin.norm_Rep [symmetric])
apply (simp only: bintrunc_bintrunc_min word_size)
apply (simp add: min.absorb2)
done
@@ -579,17 +506,17 @@
lemma wi_bintr:
"len_of TYPE('a::len0) \<le> n \<Longrightarrow>
word_of_int (bintrunc n w) = (word_of_int w :: 'a word)"
- by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min.absorb1)
-
-lemma td_ext_sbin:
- "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len)))
+ by (auto simp: word_ubin.norm_eq_iff [symmetric] min.absorb1)
+
+lemma td_ext_sbin:
+ "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len)))
(sbintrunc (len_of TYPE('a) - 1))"
apply (unfold td_ext_def' sint_uint)
apply (simp add : word_ubin.eq_norm)
apply (cases "len_of TYPE('a)")
apply (auto simp add : sints_def)
apply (rule sym [THEN trans])
- apply (rule word_ubin.Abs_norm)
+ apply (rule word_ubin.Abs_norm)
apply (simp only: bintrunc_sbintrunc)
apply (drule sym)
apply simp
@@ -602,46 +529,45 @@
using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
(* We do sint before sbin, before sint is the user version
- and interpretations do not produce thm duplicates. I.e.
+ and interpretations do not produce thm duplicates. I.e.
we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
because the latter is the same thm as the former *)
interpretation word_sint:
- td_ext "sint ::'a::len word => int"
- word_of_int
- "sints (len_of TYPE('a::len))"
- "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
- 2 ^ (len_of TYPE('a::len) - 1)"
+ td_ext
+ "sint ::'a::len word \<Rightarrow> int"
+ word_of_int
+ "sints (len_of TYPE('a::len))"
+ "\<lambda>w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
+ 2 ^ (len_of TYPE('a::len) - 1)"
by (rule td_ext_sint)
interpretation word_sbin:
- td_ext "sint ::'a::len word => int"
- word_of_int
- "sints (len_of TYPE('a::len))"
- "sbintrunc (len_of TYPE('a::len) - 1)"
+ td_ext
+ "sint ::'a::len word \<Rightarrow> int"
+ word_of_int
+ "sints (len_of TYPE('a::len))"
+ "sbintrunc (len_of TYPE('a::len) - 1)"
by (rule td_ext_sbin)
lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
lemmas td_sint = word_sint.td
-lemma to_bl_def':
- "(to_bl :: 'a :: len0 word => bool list) =
- bin_to_bl (len_of TYPE('a)) o uint"
+lemma to_bl_def': "(to_bl :: 'a::len0 word \<Rightarrow> bool list) = bin_to_bl (len_of TYPE('a)) \<circ> uint"
by (auto simp: to_bl_def)
-lemmas word_reverse_no_def [simp] = word_reverse_def [of "numeral w"] for w
+lemmas word_reverse_no_def [simp] =
+ word_reverse_def [of "numeral w"] for w
lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
by (fact uints_def [unfolded no_bintr_alt1])
-lemma word_numeral_alt:
- "numeral b = word_of_int (numeral b)"
+lemma word_numeral_alt: "numeral b = word_of_int (numeral b)"
by (induct b, simp_all only: numeral.simps word_of_int_homs)
declare word_numeral_alt [symmetric, code_abbrev]
-lemma word_neg_numeral_alt:
- "- numeral b = word_of_int (- numeral b)"
+lemma word_neg_numeral_alt: "- numeral b = word_of_int (- numeral b)"
by (simp only: word_numeral_alt wi_hom_neg)
declare word_neg_numeral_alt [symmetric, code_abbrev]
@@ -650,37 +576,34 @@
"(rel_fun op = pcr_word) numeral numeral"
"(rel_fun op = pcr_word) (- numeral) (- numeral)"
apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
- using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
+ using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by auto
lemma uint_bintrunc [simp]:
- "uint (numeral bin :: 'a word) =
- bintrunc (len_of TYPE ('a :: len0)) (numeral bin)"
+ "uint (numeral bin :: 'a word) =
+ bintrunc (len_of TYPE('a::len0)) (numeral bin)"
unfolding word_numeral_alt by (rule word_ubin.eq_norm)
-lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) =
- bintrunc (len_of TYPE ('a :: len0)) (- numeral bin)"
+lemma uint_bintrunc_neg [simp]:
+ "uint (- numeral bin :: 'a word) = bintrunc (len_of TYPE('a::len0)) (- numeral bin)"
by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
lemma sint_sbintrunc [simp]:
- "sint (numeral bin :: 'a word) =
- sbintrunc (len_of TYPE ('a :: len) - 1) (numeral bin)"
+ "sint (numeral bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) (numeral bin)"
by (simp only: word_numeral_alt word_sbin.eq_norm)
-lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) =
- sbintrunc (len_of TYPE ('a :: len) - 1) (- numeral bin)"
+lemma sint_sbintrunc_neg [simp]:
+ "sint (- numeral bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) (- numeral bin)"
by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
lemma unat_bintrunc [simp]:
- "unat (numeral bin :: 'a :: len0 word) =
- nat (bintrunc (len_of TYPE('a)) (numeral bin))"
+ "unat (numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (numeral bin))"
by (simp only: unat_def uint_bintrunc)
lemma unat_bintrunc_neg [simp]:
- "unat (- numeral bin :: 'a :: len0 word) =
- nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
+ "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
by (simp only: unat_def uint_bintrunc_neg)
-lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
+lemma size_0_eq: "size (w :: 'a::len0 word) = 0 \<Longrightarrow> v = w"
apply (unfold word_size)
apply (rule word_uint.Rep_eqD)
apply (rule box_equals)
@@ -689,51 +612,50 @@
apply simp
done
-lemma uint_ge_0 [iff]: "0 \<le> uint (x::'a::len0 word)"
+lemma uint_ge_0 [iff]: "0 \<le> uint x"
+ for x :: "'a::len0 word"
using word_uint.Rep [of x] by (simp add: uints_num)
-lemma uint_lt2p [iff]: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
+lemma uint_lt2p [iff]: "uint x < 2 ^ len_of TYPE('a)"
+ for x :: "'a::len0 word"
using word_uint.Rep [of x] by (simp add: uints_num)
-lemma sint_ge: "- (2 ^ (len_of TYPE('a) - 1)) \<le> sint (x::'a::len word)"
+lemma sint_ge: "- (2 ^ (len_of TYPE('a) - 1)) \<le> sint x"
+ for x :: "'a::len word"
using word_sint.Rep [of x] by (simp add: sints_num)
-lemma sint_lt: "sint (x::'a::len word) < 2 ^ (len_of TYPE('a) - 1)"
+lemma sint_lt: "sint x < 2 ^ (len_of TYPE('a) - 1)"
+ for x :: "'a::len word"
using word_sint.Rep [of x] by (simp add: sints_num)
-lemma sign_uint_Pls [simp]:
- "bin_sign (uint x) = 0"
+lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0"
by (simp add: sign_Pls_ge_0)
-lemma uint_m2p_neg: "uint (x::'a::len0 word) - 2 ^ len_of TYPE('a) < 0"
+lemma uint_m2p_neg: "uint x - 2 ^ len_of TYPE('a) < 0"
+ for x :: "'a::len0 word"
by (simp only: diff_less_0_iff_less uint_lt2p)
-lemma uint_m2p_not_non_neg:
- "\<not> 0 \<le> uint (x::'a::len0 word) - 2 ^ len_of TYPE('a)"
+lemma uint_m2p_not_non_neg: "\<not> 0 \<le> uint x - 2 ^ len_of TYPE('a)"
+ for x :: "'a::len0 word"
by (simp only: not_le uint_m2p_neg)
-lemma lt2p_lem:
- "len_of TYPE('a) \<le> n \<Longrightarrow> uint (w :: 'a::len0 word) < 2 ^ n"
+lemma lt2p_lem: "len_of TYPE('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
+ for w :: "'a::len0 word"
by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
lemma uint_nat: "uint w = int (unat w)"
- unfolding unat_def by auto
-
-lemma uint_numeral:
- "uint (numeral b :: 'a :: len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
- unfolding word_numeral_alt
- by (simp only: int_word_uint)
-
-lemma uint_neg_numeral:
- "uint (- numeral b :: 'a :: len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
- unfolding word_neg_numeral_alt
- by (simp only: int_word_uint)
-
-lemma unat_numeral:
- "unat (numeral b::'a::len0 word) = numeral b mod 2 ^ len_of TYPE ('a)"
+ by (auto simp: unat_def)
+
+lemma uint_numeral: "uint (numeral b :: 'a::len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
+ by (simp only: word_numeral_alt int_word_uint)
+
+lemma uint_neg_numeral: "uint (- numeral b :: 'a::len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
+ by (simp only: word_neg_numeral_alt int_word_uint)
+
+lemma unat_numeral: "unat (numeral b :: 'a::len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
apply (unfold unat_def)
apply (clarsimp simp only: uint_numeral)
apply (rule nat_mod_distrib [THEN trans])
@@ -741,119 +663,113 @@
apply (simp_all add: nat_power_eq)
done
-lemma sint_numeral: "sint (numeral b :: 'a :: len word) = (numeral b +
- 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
- 2 ^ (len_of TYPE('a) - 1)"
+lemma sint_numeral:
+ "sint (numeral b :: 'a::len word) =
+ (numeral b +
+ 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
+ 2 ^ (len_of TYPE('a) - 1)"
unfolding word_numeral_alt by (rule int_word_sint)
-lemma word_of_int_0 [simp, code_post]:
- "word_of_int 0 = 0"
+lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0"
unfolding word_0_wi ..
-lemma word_of_int_1 [simp, code_post]:
- "word_of_int 1 = 1"
+lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
unfolding word_1_wi ..
lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
by (simp add: wi_hom_syms)
-lemma word_of_int_numeral [simp] :
- "(word_of_int (numeral bin) :: 'a :: len0 word) = (numeral bin)"
- unfolding word_numeral_alt ..
+lemma word_of_int_numeral [simp] : "(word_of_int (numeral bin) :: 'a::len0 word) = numeral bin"
+ by (simp only: word_numeral_alt)
lemma word_of_int_neg_numeral [simp]:
- "(word_of_int (- numeral bin) :: 'a :: len0 word) = (- numeral bin)"
- unfolding word_numeral_alt wi_hom_syms ..
-
-lemma word_int_case_wi:
- "word_int_case f (word_of_int i :: 'b word) =
- f (i mod 2 ^ len_of TYPE('b::len0))"
- unfolding word_int_case_def by (simp add: word_uint.eq_norm)
-
-lemma word_int_split:
- "P (word_int_case f x) =
- (ALL i. x = (word_of_int i :: 'b :: len0 word) &
- 0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))"
- unfolding word_int_case_def
- by (auto simp: word_uint.eq_norm mod_pos_pos_trivial)
-
-lemma word_int_split_asm:
- "P (word_int_case f x) =
- (~ (EX n. x = (word_of_int n :: 'b::len0 word) &
- 0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))"
- unfolding word_int_case_def
- by (auto simp: word_uint.eq_norm mod_pos_pos_trivial)
+ "(word_of_int (- numeral bin) :: 'a::len0 word) = - numeral bin"
+ by (simp only: word_numeral_alt wi_hom_syms)
+
+lemma word_int_case_wi:
+ "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ len_of TYPE('b::len0))"
+ by (simp add: word_int_case_def word_uint.eq_norm)
+
+lemma word_int_split:
+ "P (word_int_case f x) =
+ (\<forall>i. x = (word_of_int i :: 'b::len0 word) \<and> 0 \<le> i \<and> i < 2 ^ len_of TYPE('b) \<longrightarrow> P (f i))"
+ by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
+
+lemma word_int_split_asm:
+ "P (word_int_case f x) =
+ (\<nexists>n. x = (word_of_int n :: 'b::len0 word) \<and> 0 \<le> n \<and> n < 2 ^ len_of TYPE('b::len0) \<and> \<not> P (f n))"
+ by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
-lemma uint_range_size: "0 <= uint w & uint w < 2 ^ size w"
+lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w"
unfolding word_size by (rule uint_range')
-lemma sint_range_size:
- "- (2 ^ (size w - Suc 0)) <= sint w & sint w < 2 ^ (size w - Suc 0)"
+lemma sint_range_size: "- (2 ^ (size w - Suc 0)) \<le> sint w \<and> sint w < 2 ^ (size w - Suc 0)"
unfolding word_size by (rule sint_range')
-lemma sint_above_size: "2 ^ (size (w::'a::len word) - 1) \<le> x \<Longrightarrow> sint w < x"
+lemma sint_above_size: "2 ^ (size w - 1) \<le> x \<Longrightarrow> sint w < x"
+ for w :: "'a::len word"
unfolding word_size by (rule less_le_trans [OF sint_lt])
-lemma sint_below_size:
- "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
+lemma sint_below_size: "x \<le> - (2 ^ (size w - 1)) \<Longrightarrow> x \<le> sint w"
+ for w :: "'a::len word"
unfolding word_size by (rule order_trans [OF _ sint_ge])
subsection \<open>Testing bits\<close>
-lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
+lemma test_bit_eq_iff: "test_bit u = test_bit v \<longleftrightarrow> u = v"
+ for u v :: "'a::len0 word"
unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
-lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w"
+lemma test_bit_size [rule_format] : "w !! n \<longrightarrow> n < size w"
+ for w :: "'a::len0 word"
apply (unfold word_test_bit_def)
apply (subst word_ubin.norm_Rep [symmetric])
apply (simp only: nth_bintr word_size)
apply fast
done
-lemma word_eq_iff:
- fixes x y :: "'a::len0 word"
- shows "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
+lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
+ for x y :: "'a::len0 word"
unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
by (metis test_bit_size [unfolded word_size])
-lemma word_eqI [rule_format]:
- fixes u :: "'a::len0 word"
- shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
+lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"
+ for u :: "'a::len0 word"
by (simp add: word_size word_eq_iff)
-lemma word_eqD: "(u::'a::len0 word) = v \<Longrightarrow> u !! x = v !! x"
+lemma word_eqD: "u = v \<Longrightarrow> u !! x = v !! x"
+ for u v :: "'a::len0 word"
by simp
-lemma test_bit_bin': "w !! n = (n < size w & bin_nth (uint w) n)"
- unfolding word_test_bit_def word_size
- by (simp add: nth_bintr [symmetric])
+lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bin_nth (uint w) n"
+ by (simp add: word_test_bit_def word_size nth_bintr [symmetric])
lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
-lemma bin_nth_uint_imp:
- "bin_nth (uint (w::'a::len0 word)) n \<Longrightarrow> n < len_of TYPE('a)"
+lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < len_of TYPE('a)"
+ for w :: "'a::len0 word"
apply (rule nth_bintr [THEN iffD1, THEN conjunct1])
apply (subst word_ubin.norm_Rep)
apply assumption
done
lemma bin_nth_sint:
- fixes w :: "'a::len word"
- shows "len_of TYPE('a) \<le> n \<Longrightarrow>
- bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
+ "len_of TYPE('a) \<le> n \<Longrightarrow> bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
+ for w :: "'a::len word"
apply (subst word_sbin.norm_Rep [symmetric])
apply (auto simp add: nth_sbintr)
done
(* type definitions theorem for in terms of equivalent bool list *)
-lemma td_bl:
- "type_definition (to_bl :: 'a::len0 word => bool list)
- of_bl
- {bl. length bl = len_of TYPE('a)}"
+lemma td_bl:
+ "type_definition
+ (to_bl :: 'a::len0 word \<Rightarrow> bool list)
+ of_bl
+ {bl. length bl = len_of TYPE('a)}"
apply (unfold type_definition_def of_bl_def to_bl_def)
apply (simp add: word_ubin.eq_norm)
apply safe
@@ -862,25 +778,25 @@
done
interpretation word_bl:
- type_definition "to_bl :: 'a::len0 word => bool list"
- of_bl
- "{bl. length bl = len_of TYPE('a::len0)}"
+ type_definition
+ "to_bl :: 'a::len0 word \<Rightarrow> bool list"
+ of_bl
+ "{bl. length bl = len_of TYPE('a::len0)}"
by (fact td_bl)
lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
lemma word_size_bl: "size w = size (to_bl w)"
- unfolding word_size by auto
-
-lemma to_bl_use_of_bl:
- "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
+ by (auto simp: word_size)
+
+lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
- unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
+ by (simp add: word_reverse_def word_bl.Abs_inverse)
lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
- unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
+ by (simp add: word_reverse_def word_bl.Abs_inverse)
lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
by (metis word_rev_rev)
@@ -888,13 +804,16 @@
lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"
by simp
-lemma length_bl_gt_0 [iff]: "0 < length (to_bl (x::'a::len word))"
+lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
+ for x :: "'a::len word"
unfolding word_bl_Rep' by (rule len_gt_0)
-lemma bl_not_Nil [iff]: "to_bl (x::'a::len word) \<noteq> []"
+lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
+ for x :: "'a::len word"
by (fact length_bl_gt_0 [unfolded length_greater_0_conv])
-lemma length_bl_neq_0 [iff]: "length (to_bl (x::'a::len word)) \<noteq> 0"
+lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
+ for x :: "'a::len word"
by (fact length_bl_gt_0 [THEN gr_implies_not0])
lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
@@ -903,32 +822,26 @@
apply simp
done
-lemma of_bl_drop':
- "lend = length bl - len_of TYPE ('a :: len0) \<Longrightarrow>
+lemma of_bl_drop':
+ "lend = length bl - len_of TYPE('a::len0) \<Longrightarrow>
of_bl (drop lend bl) = (of_bl bl :: 'a word)"
- apply (unfold of_bl_def)
- apply (clarsimp simp add : trunc_bl2bin [symmetric])
- done
-
-lemma test_bit_of_bl:
+ by (auto simp: of_bl_def trunc_bl2bin [symmetric])
+
+lemma test_bit_of_bl:
"(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
- apply (unfold of_bl_def word_test_bit_def)
- apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
- done
-
-lemma no_of_bl:
- "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) (numeral bin))"
- unfolding of_bl_def by simp
+ by (auto simp add: of_bl_def word_test_bit_def word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
+
+lemma no_of_bl: "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE('a)) (numeral bin))"
+ by (simp add: of_bl_def)
lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
- unfolding word_size to_bl_def by auto
+ by (auto simp: word_size to_bl_def)
lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
- unfolding uint_bl by (simp add : word_size)
-
-lemma to_bl_of_bin:
- "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
- unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
+ by (simp add: uint_bl word_size)
+
+lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
+ by (auto simp: uint_bl word_ubin.eq_norm word_size)
lemma to_bl_numeral [simp]:
"to_bl (numeral bin::'a::len0 word) =
@@ -941,40 +854,39 @@
unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
- unfolding uint_bl by (simp add : word_size)
-
-lemma uint_bl_bin:
- fixes x :: "'a::len0 word"
- shows "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
+ by (simp add: uint_bl word_size)
+
+lemma uint_bl_bin: "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
+ for x :: "'a::len0 word"
by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
(* naturals *)
lemma uints_unats: "uints n = int ` unats n"
apply (unfold unats_def uints_num)
apply safe
- apply (rule_tac image_eqI)
- apply (erule_tac nat_0_le [symmetric])
- apply auto
- apply (erule_tac nat_less_iff [THEN iffD2])
- apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
- apply (auto simp add : nat_power_eq of_nat_power)
+ apply (rule_tac image_eqI)
+ apply (erule_tac nat_0_le [symmetric])
+ apply auto
+ apply (erule_tac nat_less_iff [THEN iffD2])
+ apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
+ apply (auto simp: nat_power_eq)
done
lemma unats_uints: "unats n = nat ` uints n"
- by (auto simp add : uints_unats image_iff)
-
-lemmas bintr_num = word_ubin.norm_eq_iff
- [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
-lemmas sbintr_num = word_sbin.norm_eq_iff
- [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
+ by (auto simp: uints_unats image_iff)
+
+lemmas bintr_num =
+ word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
+lemmas sbintr_num =
+ word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
lemma num_of_bintr':
- "bintrunc (len_of TYPE('a :: len0)) (numeral a) = (numeral b) \<Longrightarrow>
+ "bintrunc (len_of TYPE('a::len0)) (numeral a) = (numeral b) \<Longrightarrow>
numeral a = (numeral b :: 'a word)"
unfolding bintr_num by (erule subst, simp)
lemma num_of_sbintr':
- "sbintrunc (len_of TYPE('a :: len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
+ "sbintrunc (len_of TYPE('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
numeral a = (numeral b :: 'a word)"
unfolding sbintr_num by (erule subst, simp)
@@ -992,34 +904,30 @@
thus in "cast w = w, the type means cast to length of w! **)
lemma ucast_id: "ucast w = w"
- unfolding ucast_def by auto
+ by (auto simp: ucast_def)
lemma scast_id: "scast w = w"
- unfolding scast_def by auto
+ by (auto simp: scast_def)
lemma ucast_bl: "ucast w = of_bl (to_bl w)"
- unfolding ucast_def of_bl_def uint_bl
- by (auto simp add : word_size)
-
-lemma nth_ucast:
- "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))"
- apply (unfold ucast_def test_bit_bin)
- apply (simp add: word_ubin.eq_norm nth_bintr word_size)
- apply (fast elim!: bin_nth_uint_imp)
- done
+ by (auto simp: ucast_def of_bl_def uint_bl word_size)
+
+lemma nth_ucast: "(ucast w::'a::len0 word) !! n = (w !! n \<and> n < len_of TYPE('a))"
+ by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
+ (fast elim!: bin_nth_uint_imp)
(* for literal u(s)cast *)
lemma ucast_bintr [simp]:
- "ucast (numeral w ::'a::len0 word) =
- word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
- unfolding ucast_def by simp
+ "ucast (numeral w ::'a::len0 word) = word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
+ by (simp add: ucast_def)
+
(* TODO: neg_numeral *)
lemma scast_sbintr [simp]:
- "scast (numeral w ::'a::len word) =
- word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (numeral w))"
- unfolding scast_def by simp
+ "scast (numeral w ::'a::len word) =
+ word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (numeral w))"
+ by (simp add: scast_def)
lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"
unfolding source_size_def word_size Let_def ..
@@ -1027,15 +935,13 @@
lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"
unfolding target_size_def word_size Let_def ..
-lemma is_down:
- fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
- shows "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
- unfolding is_down_def source_size target_size ..
-
-lemma is_up:
- fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
- shows "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
- unfolding is_up_def source_size target_size ..
+lemma is_down: "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
+ for c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+ by (simp only: is_down_def source_size target_size)
+
+lemma is_up: "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
+ for c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+ by (simp only: is_up_def source_size target_size)
lemmas is_up_down = trans [OF is_up is_down [symmetric]]
@@ -1051,8 +957,7 @@
lemma word_rev_tf:
"to_bl (of_bl bl::'a::len0 word) =
rev (takefill False (len_of TYPE('a)) (rev bl))"
- unfolding of_bl_def uint_bl
- by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
+ by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size)
lemma word_rep_drop:
"to_bl (of_bl bl::'a::len0 word) =
@@ -1060,10 +965,10 @@
drop (length bl - len_of TYPE('a)) bl"
by (simp add: word_rev_tf takefill_alt rev_take)
-lemma to_bl_ucast:
- "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) =
- replicate (len_of TYPE('a) - len_of TYPE('b)) False @
- drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
+lemma to_bl_ucast:
+ "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) =
+ replicate (len_of TYPE('a) - len_of TYPE('b)) False @
+ drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
apply (unfold ucast_bl)
apply (rule trans)
apply (rule word_rep_drop)
@@ -1071,17 +976,17 @@
done
lemma ucast_up_app [OF refl]:
- "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow>
+ "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow>
to_bl (uc w) = replicate n False @ (to_bl w)"
by (auto simp add : source_size target_size to_bl_ucast)
lemma ucast_down_drop [OF refl]:
- "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
+ "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
to_bl (uc w) = drop n (to_bl w)"
by (auto simp add : source_size target_size to_bl_ucast)
lemma scast_down_drop [OF refl]:
- "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
+ "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
to_bl (sc w) = drop n (to_bl w)"
apply (subgoal_tac "sc = ucast")
apply safe
@@ -1091,8 +996,7 @@
apply (simp add : source_size target_size is_down)
done
-lemma sint_up_scast [OF refl]:
- "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
+lemma sint_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
apply (unfold is_up)
apply safe
apply (simp add: scast_def word_sbin.eq_norm)
@@ -1106,8 +1010,7 @@
apply simp
done
-lemma uint_up_ucast [OF refl]:
- "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
+lemma uint_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
apply (unfold is_up)
apply safe
apply (rule bin_eqI)
@@ -1116,20 +1019,17 @@
apply (auto simp add: test_bit_bin)
done
-lemma ucast_up_ucast [OF refl]:
- "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
+lemma ucast_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
apply (simp (no_asm) add: ucast_def)
apply (clarsimp simp add: uint_up_ucast)
done
-
-lemma scast_up_scast [OF refl]:
- "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
+
+lemma scast_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
apply (simp (no_asm) add: scast_def)
apply (clarsimp simp add: sint_up_scast)
done
-
-lemma ucast_of_bl_up [OF refl]:
- "w = of_bl bl \<Longrightarrow> size bl <= size w \<Longrightarrow> ucast w = of_bl bl"
+
+lemma ucast_of_bl_up [OF refl]: "w = of_bl bl \<Longrightarrow> size bl \<le> size w \<Longrightarrow> ucast w = of_bl bl"
by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id]
@@ -1141,42 +1041,39 @@
lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
lemma up_ucast_surj:
- "is_up (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow>
- surj (ucast :: 'a word => 'b word)"
- by (rule surjI, erule ucast_up_ucast_id)
+ "is_up (ucast :: 'b::len0 word \<Rightarrow> 'a::len0 word) \<Longrightarrow>
+ surj (ucast :: 'a word \<Rightarrow> 'b word)"
+ by (rule surjI) (erule ucast_up_ucast_id)
lemma up_scast_surj:
- "is_up (scast :: 'b::len word => 'a::len word) \<Longrightarrow>
- surj (scast :: 'a word => 'b word)"
- by (rule surjI, erule scast_up_scast_id)
+ "is_up (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow>
+ surj (scast :: 'a word \<Rightarrow> 'b word)"
+ by (rule surjI) (erule scast_up_scast_id)
lemma down_scast_inj:
- "is_down (scast :: 'b::len word => 'a::len word) \<Longrightarrow>
- inj_on (ucast :: 'a word => 'b word) A"
+ "is_down (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow>
+ inj_on (ucast :: 'a word \<Rightarrow> 'b word) A"
by (rule inj_on_inverseI, erule scast_down_scast_id)
lemma down_ucast_inj:
- "is_down (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow>
- inj_on (ucast :: 'a word => 'b word) A"
- by (rule inj_on_inverseI, erule ucast_down_ucast_id)
+ "is_down (ucast :: 'b::len0 word \<Rightarrow> 'a::len0 word) \<Longrightarrow>
+ inj_on (ucast :: 'a word \<Rightarrow> 'b word) A"
+ by (rule inj_on_inverseI) (erule ucast_down_ucast_id)
lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
-lemma ucast_down_wi [OF refl]:
- "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x"
+lemma ucast_down_wi [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x"
apply (unfold is_down)
apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
apply (rule word_ubin.norm_eq_iff [THEN iffD1])
apply (erule bintrunc_bintrunc_ge)
done
-lemma ucast_down_no [OF refl]:
- "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (numeral bin) = numeral bin"
+lemma ucast_down_no [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (numeral bin) = numeral bin"
unfolding word_numeral_alt by clarify (rule ucast_down_wi)
-lemma ucast_down_bl [OF refl]:
- "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
+lemma ucast_down_bl [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
unfolding of_bl_def by clarify (erule ucast_down_wi)
lemmas slice_def' = slice_def [unfolded word_size]
@@ -1187,39 +1084,33 @@
subsection \<open>Word Arithmetic\<close>
-lemma word_less_alt: "(a < b) = (uint a < uint b)"
+lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b"
by (fact word_less_def)
lemma signed_linorder: "class.linorder word_sle word_sless"
- by standard (unfold word_sle_def word_sless_def, auto)
+ by standard (auto simp: word_sle_def word_sless_def)
interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
-lemma udvdI:
- "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
+lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
by (auto simp: udvd_def)
lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b
-
lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b
-
lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b
-
lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b
-
lemmas word_sless_no [simp] = word_sless_def [of "numeral a" "numeral b"] for a b
-
lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b
-lemma word_m1_wi: "- 1 = word_of_int (- 1)"
- using word_neg_numeral_alt [of Num.One] by simp
+lemma word_m1_wi: "- 1 = word_of_int (- 1)"
+ by (simp add: word_neg_numeral_alt [of Num.One])
lemma word_0_bl [simp]: "of_bl [] = 0"
- unfolding of_bl_def by simp
-
-lemma word_1_bl: "of_bl [True] = 1"
- unfolding of_bl_def by (simp add: bl_to_bin_def)
+ by (simp add: of_bl_def)
+
+lemma word_1_bl: "of_bl [True] = 1"
+ by (simp add: of_bl_def bl_to_bin_def)
lemma uint_eq_0 [simp]: "uint 0 = 0"
unfolding word_0_wi word_ubin.eq_norm by simp
@@ -1227,25 +1118,20 @@
lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
by (simp add: of_bl_def bl_to_bin_rep_False)
-lemma to_bl_0 [simp]:
- "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
- unfolding uint_bl
- by (simp add: word_size bin_to_bl_zero)
-
-lemma uint_0_iff:
- "uint x = 0 \<longleftrightarrow> x = 0"
+lemma to_bl_0 [simp]: "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
+ by (simp add: uint_bl word_size bin_to_bl_zero)
+
+lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
by (simp add: word_uint_eq_iff)
-lemma unat_0_iff:
- "unat x = 0 \<longleftrightarrow> x = 0"
- unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
-
-lemma unat_0 [simp]:
- "unat 0 = 0"
- unfolding unat_def by auto
-
-lemma size_0_same':
- "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
+lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
+ by (auto simp: unat_def nat_eq_iff uint_0_iff)
+
+lemma unat_0 [simp]: "unat 0 = 0"
+ by (auto simp: unat_def)
+
+lemma size_0_same': "size w = 0 \<Longrightarrow> w = v"
+ for v w :: "'a::len0 word"
apply (unfold word_size)
apply (rule box_equals)
defer
@@ -1259,45 +1145,44 @@
lemmas unat_eq_0 = unat_0_iff
lemmas unat_eq_zero = unat_0_iff
-lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
-by (auto simp: unat_0_iff [symmetric])
+lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0"
+ by (auto simp: unat_0_iff [symmetric])
lemma ucast_0 [simp]: "ucast 0 = 0"
- unfolding ucast_def by simp
+ by (simp add: ucast_def)
lemma sint_0 [simp]: "sint 0 = 0"
- unfolding sint_uint by simp
+ by (simp add: sint_uint)
lemma scast_0 [simp]: "scast 0 = 0"
- unfolding scast_def by simp
+ by (simp add: scast_def)
lemma sint_n1 [simp] : "sint (- 1) = - 1"
- unfolding word_m1_wi word_sbin.eq_norm by simp
+ by (simp only: word_m1_wi word_sbin.eq_norm) simp
lemma scast_n1 [simp]: "scast (- 1) = - 1"
- unfolding scast_def by simp
+ by (simp add: scast_def)
lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
- unfolding unat_def by simp
+ by (simp add: unat_def)
lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
- unfolding ucast_def by simp
+ by (simp add: ucast_def)
(* now, to get the weaker results analogous to word_div/mod_def *)
subsection \<open>Transferring goals from words to ints\<close>
-lemma word_ths:
- shows
- word_succ_p1: "word_succ a = a + 1" and
- word_pred_m1: "word_pred a = a - 1" and
- word_pred_succ: "word_pred (word_succ a) = a" and
- word_succ_pred: "word_succ (word_pred a) = a" and
- word_mult_succ: "word_succ a * b = b + a * b"
+lemma word_ths:
+ shows word_succ_p1: "word_succ a = a + 1"
+ and word_pred_m1: "word_pred a = a - 1"
+ and word_pred_succ: "word_pred (word_succ a) = a"
+ and word_succ_pred: "word_succ (word_pred a) = a"
+ and word_mult_succ: "word_succ a * b = b + a * b"
by (transfer, simp add: algebra_simps)+
lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
@@ -1350,28 +1235,27 @@
unfolding word_pred_m1 by simp
lemma succ_pred_no [simp]:
- "word_succ (numeral w) = numeral w + 1"
- "word_pred (numeral w) = numeral w - 1"
- "word_succ (- numeral w) = - numeral w + 1"
- "word_pred (- numeral w) = - numeral w - 1"
- unfolding word_succ_p1 word_pred_m1 by simp_all
-
-lemma word_sp_01 [simp] :
- "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0"
- unfolding word_succ_p1 word_pred_m1 by simp_all
+ "word_succ (numeral w) = numeral w + 1"
+ "word_pred (numeral w) = numeral w - 1"
+ "word_succ (- numeral w) = - numeral w + 1"
+ "word_pred (- numeral w) = - numeral w - 1"
+ by (simp_all add: word_succ_p1 word_pred_m1)
+
+lemma word_sp_01 [simp]:
+ "word_succ (- 1) = 0 \<and> word_succ 0 = 1 \<and> word_pred 0 = - 1 \<and> word_pred 1 = 0"
+ by (simp_all add: word_succ_p1 word_pred_m1)
(* alternative approach to lifting arithmetic equalities *)
-lemma word_of_int_Ex:
- "\<exists>y. x = word_of_int y"
+lemma word_of_int_Ex: "\<exists>y. x = word_of_int y"
by (rule_tac x="uint x" in exI) simp
subsection \<open>Order on fixed-length words\<close>
lemma word_zero_le [simp] :
- "0 <= (y :: 'a :: len0 word)"
+ "0 <= (y :: 'a::len0 word)"
unfolding word_le_def by auto
-
+
lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
unfolding word_le_def
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
@@ -1380,10 +1264,10 @@
unfolding word_le_def
by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
-lemmas word_not_simps [simp] =
+lemmas word_not_simps [simp] =
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
-lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> (y :: 'a :: len0 word)"
+lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> (y :: 'a::len0 word)"
by (simp add: less_le)
lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
@@ -1399,14 +1283,14 @@
lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
unfolding unat_def word_less_alt
by (rule nat_less_eq_zless [symmetric]) simp
-
-lemma wi_less:
- "(word_of_int n < (word_of_int m :: 'a :: len0 word)) =
+
+lemma wi_less:
+ "(word_of_int n < (word_of_int m :: 'a::len0 word)) =
(n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
unfolding word_less_alt by (simp add: word_uint.eq_norm)
-lemma wi_le:
- "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) =
+lemma wi_le:
+ "(word_of_int n <= (word_of_int m :: 'a::len0 word)) =
(n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
unfolding word_le_def by (simp add: word_uint.eq_norm)
@@ -1446,29 +1330,29 @@
lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
-
+
lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
-lemma uint_sub_lt2p [simp]:
- "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) <
+lemma uint_sub_lt2p [simp]:
+ "uint (x :: 'a::len0 word) - uint (y :: 'b::len0 word) <
2 ^ len_of TYPE('a)"
using uint_ge_0 [of y] uint_lt2p [of x] by arith
subsection \<open>Conditions for the addition (etc) of two words to overflow\<close>
-lemma uint_add_lem:
- "(uint x + uint y < 2 ^ len_of TYPE('a)) =
- (uint (x + y :: 'a :: len0 word) = uint x + uint y)"
+lemma uint_add_lem:
+ "(uint x + uint y < 2 ^ len_of TYPE('a)) =
+ (uint (x + y :: 'a::len0 word) = uint x + uint y)"
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
-lemma uint_mult_lem:
- "(uint x * uint y < 2 ^ len_of TYPE('a)) =
- (uint (x * y :: 'a :: len0 word) = uint x * uint y)"
+lemma uint_mult_lem:
+ "(uint x * uint y < 2 ^ len_of TYPE('a)) =
+ (uint (x * y :: 'a::len0 word) = uint x * uint y)"
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
-lemma uint_sub_lem:
+lemma uint_sub_lem:
"(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
@@ -1479,7 +1363,7 @@
unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
lemma mod_add_if_z:
- "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= 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)
@@ -1490,7 +1374,7 @@
using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
lemma mod_sub_if_z:
- "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= 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)
@@ -1504,7 +1388,7 @@
subsection \<open>Definition of \<open>uint_arith\<close>\<close>
lemma word_of_int_inverse:
- "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
+ "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
uint (a::'a::len0 word) = r"
apply (erule word_uint.Abs_inverse' [rotated])
apply (simp add: uints_num)
@@ -1512,7 +1396,7 @@
lemma uint_split:
fixes x::"'a::len0 word"
- shows "P (uint x) =
+ shows "P (uint x) =
(ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
apply (fold word_int_case_def)
apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
@@ -1521,48 +1405,48 @@
lemma uint_split_asm:
fixes x::"'a::len0 word"
- shows "P (uint x) =
+ shows "P (uint x) =
(~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
- by (auto dest!: word_of_int_inverse
+ by (auto dest!: word_of_int_inverse
simp: int_word_uint mod_pos_pos_trivial
split: uint_split)
lemmas uint_splits = uint_split uint_split_asm
-lemmas uint_arith_simps =
+lemmas uint_arith_simps =
word_le_def word_less_alt
- word_uint.Rep_inject [symmetric]
+ word_uint.Rep_inject [symmetric]
uint_sub_if' uint_plus_if'
-(* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
-lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
+(* use this to stop, eg, 2 ^ len_of TYPE(32) being simplified *)
+lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
by auto
(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
ML \<open>
-fun uint_arith_simpset ctxt =
+fun uint_arith_simpset ctxt =
ctxt addsimps @{thms uint_arith_simps}
delsimps @{thms word_uint.Rep_inject}
|> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
-fun uint_arith_tacs ctxt =
+fun uint_arith_tacs ctxt =
let
fun arith_tac' n t =
Arith_Data.arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
- in
+ in
[ clarify_tac ctxt 1,
full_simp_tac (uint_arith_simpset ctxt) 1,
ALLGOALS (full_simp_tac
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms uint_splits}
|> fold Simplifier.add_cong @{thms power_False_cong})),
- rewrite_goals_tac ctxt @{thms word_size},
+ rewrite_goals_tac ctxt @{thms word_size},
ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
REPEAT (eresolve_tac ctxt [conjE] n) THEN
- REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n
- THEN assume_tac ctxt n
+ REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n
+ THEN assume_tac ctxt n
THEN assume_tac ctxt n)),
TRYALL arith_tac' ]
end
@@ -1570,20 +1454,20 @@
fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
\<close>
-method_setup uint_arith =
+method_setup uint_arith =
\<open>Scan.succeed (SIMPLE_METHOD' o uint_arith_tac)\<close>
"solving word arithmetic via integers and arith"
subsection \<open>More on overflows and monotonicity\<close>
-lemma no_plus_overflow_uint_size:
- "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
+lemma no_plus_overflow_uint_size:
+ "((x :: 'a::len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
unfolding word_size by uint_arith
lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
-lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
+lemma no_ulen_sub: "((x :: 'a::len0 word) >= x - y) = (uint y <= uint x)"
by uint_arith
lemma no_olen_add':
@@ -1600,127 +1484,127 @@
lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
-lemma word_less_sub1:
- "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
+lemma word_less_sub1:
+ "(x :: 'a::len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
by uint_arith
-lemma word_le_sub1:
- "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
+lemma word_le_sub1:
+ "(x :: 'a::len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
by uint_arith
-lemma sub_wrap_lt:
- "((x :: 'a :: len0 word) < x - z) = (x < z)"
+lemma sub_wrap_lt:
+ "((x :: 'a::len0 word) < x - z) = (x < z)"
by uint_arith
-lemma sub_wrap:
- "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
+lemma sub_wrap:
+ "((x :: 'a::len0 word) <= x - z) = (z = 0 | x < z)"
by uint_arith
-lemma plus_minus_not_NULL_ab:
- "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
+lemma plus_minus_not_NULL_ab:
+ "(x :: 'a::len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
by uint_arith
-lemma plus_minus_no_overflow_ab:
- "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c"
+lemma plus_minus_no_overflow_ab:
+ "(x :: 'a::len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c"
by uint_arith
-lemma le_minus':
- "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
+lemma le_minus':
+ "(a :: 'a::len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
by uint_arith
-lemma le_plus':
- "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
+lemma le_plus':
+ "(a :: 'a::len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
by uint_arith
lemmas le_plus = le_plus' [rotated]
lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
-lemma word_plus_mono_right:
- "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
+lemma word_plus_mono_right:
+ "(y :: 'a::len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
by uint_arith
-lemma word_less_minus_cancel:
- "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
+lemma word_less_minus_cancel:
+ "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a::len0 word) < z"
by uint_arith
-lemma word_less_minus_mono_left:
- "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
+lemma word_less_minus_mono_left:
+ "(y :: 'a::len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
by uint_arith
-lemma word_less_minus_mono:
- "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c
+lemma word_less_minus_mono:
+ "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c
\<Longrightarrow> a - b < c - (d::'a::len word)"
by uint_arith
-lemma word_le_minus_cancel:
- "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
+lemma word_le_minus_cancel:
+ "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a::len0 word) <= z"
by uint_arith
-lemma word_le_minus_mono_left:
- "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
+lemma word_le_minus_mono_left:
+ "(y :: 'a::len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
by uint_arith
-lemma word_le_minus_mono:
- "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c
+lemma word_le_minus_mono:
+ "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c
\<Longrightarrow> a - b <= c - (d::'a::len word)"
by uint_arith
-lemma plus_le_left_cancel_wrap:
- "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
+lemma plus_le_left_cancel_wrap:
+ "(x :: 'a::len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
by uint_arith
-lemma plus_le_left_cancel_nowrap:
- "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow>
- (x + y' < x + y) = (y' < y)"
+lemma plus_le_left_cancel_nowrap:
+ "(x :: 'a::len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow>
+ (x + y' < x + y) = (y' < y)"
by uint_arith
-lemma word_plus_mono_right2:
- "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
+lemma word_plus_mono_right2:
+ "(a :: 'a::len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
by uint_arith
-lemma word_less_add_right:
- "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
+lemma word_less_add_right:
+ "(x :: 'a::len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
by uint_arith
-lemma word_less_sub_right:
- "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
+lemma word_less_sub_right:
+ "(x :: 'a::len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
by uint_arith
-lemma word_le_plus_either:
- "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
+lemma word_le_plus_either:
+ "(x :: 'a::len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
by uint_arith
-lemma word_less_nowrapI:
- "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
+lemma word_less_nowrapI:
+ "(x :: 'a::len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
by uint_arith
-lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
+lemma inc_le: "(i :: 'a::len word) < m \<Longrightarrow> i + 1 <= m"
by uint_arith
-lemma inc_i:
- "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
+lemma inc_i:
+ "(1 :: 'a::len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
by uint_arith
lemma udvd_incr_lem:
- "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
+ "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
apply clarsimp
-
+
apply (drule less_le_mult)
apply safe
done
-lemma udvd_incr':
- "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
- uint q = ua + n' * uint K \<Longrightarrow> p + K <= q"
+lemma udvd_incr':
+ "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
+ uint q = ua + n' * uint K \<Longrightarrow> p + K <= q"
apply (unfold word_less_alt word_le_def)
apply (drule (2) udvd_incr_lem)
apply (erule uint_add_le [THEN order_trans])
done
-lemma udvd_decr':
- "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
+lemma udvd_decr':
+ "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
apply (unfold word_less_alt word_le_def)
apply (drule (2) udvd_incr_lem)
@@ -1733,21 +1617,21 @@
lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
-lemma udvd_minus_le':
+lemma udvd_minus_le':
"xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
apply (unfold udvd_def)
apply clarify
apply (erule (2) udvd_decr0)
done
-lemma udvd_incr2_K:
- "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
+lemma udvd_incr2_K:
+ "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
using [[simproc del: linordered_ring_less_cancel_factor]]
apply (unfold udvd_def)
apply clarify
apply (simp add: uint_arith_simps split: if_split_asm)
- prefer 2
+ prefer 2
apply (insert uint_range' [of s])[1]
apply arith
apply (drule add.commute [THEN xtr1])
@@ -1775,7 +1659,7 @@
done
lemma word_add_rbl:
- "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
+ "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
apply (unfold word_add_def)
apply clarify
@@ -1784,7 +1668,7 @@
done
lemma word_mult_rbl:
- "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
+ "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
apply (unfold word_mult_def)
apply clarify
@@ -1797,7 +1681,7 @@
"rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
"rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
"rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
- by (auto simp: rev_swap [symmetric] word_succ_rbl
+ by (auto simp: rev_swap [symmetric] word_succ_rbl
word_pred_rbl word_mult_rbl word_add_rbl)
@@ -1806,18 +1690,18 @@
lemmas word_le_0_iff [simp] =
word_zero_le [THEN leD, THEN linorder_antisym_conv1]
-lemma word_of_int_nat:
+lemma word_of_int_nat:
"0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
by (simp add: of_nat_nat word_of_int)
(* note that iszero_def is only for class comm_semiring_1_cancel,
- which requires word length >= 1, ie 'a :: len word *)
+ which requires word length >= 1, ie 'a::len word *)
lemma iszero_word_no [simp]:
- "iszero (numeral bin :: 'a :: len word) =
+ "iszero (numeral bin :: 'a::len word) =
iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
by (simp add: iszero_def [symmetric])
-
+
text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close>
lemmas word_eq_numeral_iff_iszero [simp] =
@@ -1827,8 +1711,8 @@
subsection \<open>Word and nat\<close>
lemma td_ext_unat [OF refl]:
- "n = len_of TYPE ('a :: len) \<Longrightarrow>
- td_ext (unat :: 'a word => nat) of_nat
+ "n = len_of TYPE('a::len) \<Longrightarrow>
+ td_ext (unat :: 'a word => nat) of_nat
(unats n) (%i. i mod 2 ^ n)"
apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
apply (auto intro!: imageI simp add : word_of_int_hom_syms)
@@ -1839,8 +1723,8 @@
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
interpretation word_unat:
- td_ext "unat::'a::len word => nat"
- of_nat
+ td_ext "unat::'a::len word => nat"
+ of_nat
"unats (len_of TYPE('a::len))"
"%i. i mod 2 ^ len_of TYPE('a::len)"
by (rule td_ext_unat)
@@ -1849,14 +1733,14 @@
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
-lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
+lemma unat_le: "y <= unat (z :: 'a::len word) \<Longrightarrow> y : unats (len_of TYPE('a))"
apply (unfold unats_def)
apply clarsimp
- apply (rule xtrans, rule unat_lt2p, assumption)
+ apply (rule xtrans, rule unat_lt2p, assumption)
done
lemma word_nchotomy:
- "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
+ "ALL w. EX n. (w :: 'a::len word) = of_nat n & n < 2 ^ len_of TYPE('a)"
apply (rule allI)
apply (rule word_unat.Abs_cases)
apply (unfold unats_def)
@@ -1874,7 +1758,7 @@
apply clarsimp
done
-lemma of_nat_eq_size:
+lemma of_nat_eq_size:
"(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
unfolding word_size by (rule of_nat_eq)
@@ -1889,8 +1773,8 @@
lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
by (cases k) auto
-lemma of_nat_neq_0:
- "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
+lemma of_nat_neq_0:
+ "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE('a::len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
by (clarsimp simp add : of_nat_0)
lemma Abs_fnat_hom_add:
@@ -1898,7 +1782,7 @@
by simp
lemma Abs_fnat_hom_mult:
- "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
+ "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
by (simp add: word_of_nat wi_hom_mult)
lemma Abs_fnat_hom_Suc:
@@ -1911,18 +1795,18 @@
lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
by simp
-lemmas Abs_fnat_homs =
- Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
+lemmas Abs_fnat_homs =
+ Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
Abs_fnat_hom_0 Abs_fnat_hom_1
lemma word_arith_nat_add:
- "a + b = of_nat (unat a + unat b)"
+ "a + b = of_nat (unat a + unat b)"
by simp
lemma word_arith_nat_mult:
"a * b = of_nat (unat a * unat b)"
by (simp add: of_nat_mult)
-
+
lemma word_arith_nat_Suc:
"word_succ a = of_nat (Suc (unat a))"
by (subst Abs_fnat_hom_Suc [symmetric]) simp
@@ -1939,33 +1823,33 @@
word_arith_nat_add word_arith_nat_mult
word_arith_nat_Suc Abs_fnat_hom_0
Abs_fnat_hom_1 word_arith_nat_div
- word_arith_nat_mod
+ word_arith_nat_mod
lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
by simp
-
+
lemmas unat_word_ariths = word_arith_nat_defs
[THEN trans [OF unat_cong unat_of_nat]]
lemmas word_sub_less_iff = word_sub_le_iff
[unfolded linorder_not_less [symmetric] Not_eq_iff]
-lemma unat_add_lem:
- "(unat x + unat y < 2 ^ len_of TYPE('a)) =
- (unat (x + y :: 'a :: len word) = unat x + unat y)"
+lemma unat_add_lem:
+ "(unat x + unat y < 2 ^ len_of TYPE('a)) =
+ (unat (x + y :: 'a::len word) = unat x + unat y)"
unfolding unat_word_ariths
by (auto intro!: trans [OF _ nat_mod_lem])
-lemma unat_mult_lem:
- "(unat x * unat y < 2 ^ len_of TYPE('a)) =
- (unat (x * y :: 'a :: len word) = unat x * unat y)"
+lemma unat_mult_lem:
+ "(unat x * unat y < 2 ^ len_of TYPE('a)) =
+ (unat (x * y :: 'a::len word) = unat x * unat y)"
unfolding unat_word_ariths
by (auto intro!: trans [OF _ nat_mod_lem])
lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]
-lemma le_no_overflow:
- "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
+lemma le_no_overflow:
+ "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a::len0 word)"
apply (erule order_trans)
apply (erule olen_add_eqv [THEN iffD1])
done
@@ -1973,8 +1857,8 @@
lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]
lemma unat_sub_if_size:
- "unat (x - y) = (if unat y <= unat x
- then unat x - unat y
+ "unat (x - y) = (if unat y <= unat x
+ then unat x - unat y
else unat x + 2 ^ size x - unat y)"
apply (unfold word_size)
apply (simp add: un_ui_le)
@@ -1993,13 +1877,13 @@
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
-lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
+lemma unat_div: "unat ((x :: 'a::len word) div y) = unat x div unat y"
apply (simp add : unat_word_ariths)
apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
apply (rule div_le_dividend)
done
-lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
+lemma unat_mod: "unat ((x :: 'a::len word) mod y) = unat x mod unat y"
apply (clarsimp simp add : unat_word_ariths)
apply (cases "unat y")
prefer 2
@@ -2008,10 +1892,10 @@
apply auto
done
-lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
+lemma uint_div: "uint ((x :: 'a::len word) div y) = uint x div uint y"
unfolding uint_nat by (simp add : unat_div zdiv_int)
-lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
+lemma uint_mod: "uint ((x :: 'a::len word) mod y) = uint x mod uint y"
unfolding uint_nat by (simp add : unat_mod zmod_int)
@@ -2019,17 +1903,17 @@
lemma unat_split:
fixes x::"'a::len word"
- shows "P (unat x) =
+ shows "P (unat x) =
(ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
by (auto simp: unat_of_nat)
lemma unat_split_asm:
fixes x::"'a::len word"
- shows "P (unat x) =
+ shows "P (unat x) =
(~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
by (auto simp: unat_of_nat)
-lemmas of_nat_inverse =
+lemmas of_nat_inverse =
word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
lemmas unat_splits = unat_split unat_split_asm
@@ -2039,51 +1923,51 @@
word_unat.Rep_inject [symmetric]
unat_sub_if' unat_plus_if' unat_div unat_mod
-(* unat_arith_tac: tactic to reduce word arithmetic to nat,
+(* unat_arith_tac: tactic to reduce word arithmetic to nat,
try to solve via arith *)
ML \<open>
-fun unat_arith_simpset ctxt =
+fun unat_arith_simpset ctxt =
ctxt addsimps @{thms unat_arith_simps}
delsimps @{thms word_unat.Rep_inject}
|> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
-fun unat_arith_tacs ctxt =
+fun unat_arith_tacs ctxt =
let
fun arith_tac' n t =
Arith_Data.arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty;
- in
+ in
[ clarify_tac ctxt 1,
full_simp_tac (unat_arith_simpset ctxt) 1,
ALLGOALS (full_simp_tac
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms unat_splits}
|> fold Simplifier.add_cong @{thms power_False_cong})),
- rewrite_goals_tac ctxt @{thms word_size},
+ rewrite_goals_tac ctxt @{thms word_size},
ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
REPEAT (eresolve_tac ctxt [conjE] n) THEN
REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)),
- TRYALL arith_tac' ]
+ TRYALL arith_tac' ]
end
fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
\<close>
-method_setup unat_arith =
+method_setup unat_arith =
\<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
"solving word arithmetic via natural numbers and arith"
-lemma no_plus_overflow_unat_size:
- "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)"
+lemma no_plus_overflow_unat_size:
+ "((x :: 'a::len word) <= x + y) = (unat x + unat y < 2 ^ size x)"
unfolding word_size by unat_arith
lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem]
-lemma word_div_mult:
- "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow>
+lemma word_div_mult:
+ "(0 :: 'a::len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow>
x * y div y = x"
apply unat_arith
apply clarsimp
@@ -2091,7 +1975,7 @@
apply auto
done
-lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow>
+lemma div_lt': "(i :: 'a::len word) <= k div x \<Longrightarrow>
unat i * unat x < 2 ^ len_of TYPE('a)"
apply unat_arith
apply clarsimp
@@ -2102,7 +1986,7 @@
lemmas div_lt'' = order_less_imp_le [THEN div_lt']
-lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
+lemma div_lt_mult: "(i :: 'a::len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
apply (simp add: unat_arith_simps)
apply (drule (1) mult_less_mono1)
@@ -2110,8 +1994,8 @@
apply (rule div_mult_le)
done
-lemma div_le_mult:
- "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
+lemma div_le_mult:
+ "(i :: 'a::len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
apply (simp add: unat_arith_simps)
apply (drule mult_le_mono1)
@@ -2119,16 +2003,16 @@
apply (rule div_mult_le)
done
-lemma div_lt_uint':
- "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
+lemma div_lt_uint':
+ "(i :: 'a::len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
apply (unfold uint_nat)
apply (drule div_lt')
by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
-lemma word_le_exists':
- "(x :: 'a :: len0 word) <= y \<Longrightarrow>
+lemma word_le_exists':
+ "(x :: 'a::len0 word) <= y \<Longrightarrow>
(EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
apply (rule exI)
apply (rule conjI)
@@ -2140,7 +2024,7 @@
lemmas plus_minus_no_overflow =
order_less_imp_le [THEN plus_minus_no_overflow_ab]
-
+
lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
word_le_minus_cancel word_le_minus_mono_left
@@ -2152,10 +2036,10 @@
lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
-lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
+lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
lemma word_mod_div_equality:
- "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
+ "(n div b) * b + (n mod b) = (n :: 'a::len word)"
apply (unfold word_less_nat_alt word_arith_nat_defs)
apply (cut_tac y="unat b" in gt_or_eq_0)
apply (erule disjE)
@@ -2171,24 +2055,24 @@
apply simp
done
-lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
+lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a::len word)"
apply (simp only: word_less_nat_alt word_arith_nat_defs)
apply (clarsimp simp add : uno_simps)
done
-lemma word_of_int_power_hom:
- "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
+lemma word_of_int_power_hom:
+ "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
by (induct n) (simp_all add: wi_hom_mult [symmetric])
-lemma word_arith_power_alt:
- "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
+lemma word_arith_power_alt:
+ "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
by (simp add : word_of_int_power_hom [symmetric])
-lemma of_bl_length_less:
- "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
+lemma of_bl_length_less:
+ "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a::len word) < 2 ^ k"
apply (unfold of_bl_def word_less_alt word_numeral_alt)
apply safe
- apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
+ apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
del: word_of_int_numeral)
apply (simp add: mod_pos_pos_trivial)
apply (subst mod_pos_pos_trivial)
@@ -2208,15 +2092,15 @@
lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
-lemma card_word_size:
- "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"
+lemma card_word_size:
+ "card (UNIV :: 'a::len0 word set) = (2 ^ size (x :: 'a word))"
unfolding word_size by (rule card_word)
subsection \<open>Bitwise Operations on Words\<close>
lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
-
+
(* following definitions require both arithmetic and bit-wise word operations *)
(* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
@@ -2225,7 +2109,7 @@
(* the binary operations only *)
(* BH: why is this needed? *)
-lemmas word_log_binary_defs =
+lemmas word_log_binary_defs =
word_and_def word_or_def word_xor_def
lemma word_wi_log_defs:
@@ -2299,16 +2183,16 @@
unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
lemma word_ops_nth_size:
- "n < size (x::'a::len0 word) \<Longrightarrow>
- (x OR y) !! n = (x !! n | y !! n) &
- (x AND y) !! n = (x !! n & y !! n) &
- (x XOR y) !! n = (x !! n ~= y !! n) &
+ "n < size (x::'a::len0 word) \<Longrightarrow>
+ (x OR y) !! n = (x !! n | y !! n) &
+ (x AND y) !! n = (x !! n & y !! n) &
+ (x XOR y) !! n = (x !! n ~= y !! n) &
(NOT x) !! n = (~ x !! n)"
unfolding word_size by transfer (simp add: bin_nth_ops)
lemma word_ao_nth:
fixes x :: "'a::len0 word"
- shows "(x OR y) !! n = (x !! n | y !! n) &
+ shows "(x OR y) !! n = (x !! n | y !! n) &
(x AND y) !! n = (x !! n & y !! n)"
by transfer (auto simp add: bin_nth_ops)
@@ -2324,7 +2208,7 @@
lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
by transfer auto
-
+
lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
by transfer simp
@@ -2334,7 +2218,7 @@
(* get from commutativity, associativity etc of int_and etc
to same for word_and etc *)
-lemmas bwsimps =
+lemmas bwsimps =
wi_hom_add
word_wi_log_defs
@@ -2345,7 +2229,7 @@
"(x OR y) OR z = x OR y OR z"
"(x XOR y) XOR z = x XOR y XOR z"
by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
-
+
lemma word_bw_comms:
fixes x :: "'a::len0 word"
shows
@@ -2353,7 +2237,7 @@
"x OR y = y OR x"
"x XOR y = y XOR x"
by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
-
+
lemma word_bw_lcs:
fixes x :: "'a::len0 word"
shows
@@ -2421,7 +2305,7 @@
shows "x AND y OR z = (x OR z) AND (y OR z)"
by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
-lemma word_add_not [simp]:
+lemma word_add_not [simp]:
fixes x :: "'a::len0 word"
shows "x + NOT x = -1"
by transfer (simp add: bin_add_not)
@@ -2431,12 +2315,12 @@
shows "(x AND y) + (x OR y) = x + y"
by transfer (simp add: plus_and_or)
-lemma leoa:
+lemma leoa:
fixes x :: "'a::len0 word"
shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
-lemma leao:
+lemma leao:
fixes x' :: "'a::len0 word"
- shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
+ shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
lemma word_ao_equiv:
fixes w w' :: "'a::len0 word"
@@ -2445,25 +2329,25 @@
lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
unfolding word_le_def uint_or
- by (auto intro: le_int_or)
+ by (auto intro: le_int_or)
lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
-lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
+lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
unfolding to_bl_def word_log_defs bl_not_bin
by (simp add: word_ubin.eq_norm)
-lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)"
+lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)"
unfolding to_bl_def word_log_defs bl_xor_bin
by (simp add: word_ubin.eq_norm)
-lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)"
+lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)"
unfolding to_bl_def word_log_defs bl_or_bin
by (simp add: word_ubin.eq_norm)
-lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)"
+lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)"
unfolding to_bl_def word_log_defs bl_and_bin
by (simp add: word_ubin.eq_norm)
@@ -2474,7 +2358,7 @@
unfolding word_lsb_def uint_eq_0 uint_1 by simp
lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
- apply (unfold word_lsb_def uint_bl bin_to_bl_def)
+ apply (unfold word_lsb_def uint_bl bin_to_bl_def)
apply (rule_tac bin="uint w" in bin_exhaust)
apply (cases "size w")
apply auto
@@ -2484,7 +2368,7 @@
lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
unfolding word_lsb_def bin_last_def by auto
-lemma word_msb_sint: "msb w = (sint w < 0)"
+lemma word_msb_sint: "msb w = (sint w < 0)"
unfolding word_msb_def sign_Min_lt_0 ..
lemma msb_word_of_int:
@@ -2544,15 +2428,15 @@
apply (auto simp add: word_size)
done
-lemma test_bit_set:
+lemma test_bit_set:
fixes w :: "'a::len0 word"
shows "(set_bit w n x) !! n = (n < size w & x)"
unfolding word_size word_test_bit_def word_set_bit_def
by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
-lemma test_bit_set_gen:
+lemma test_bit_set_gen:
fixes w :: "'a::len0 word"
- shows "test_bit (set_bit w n x) m =
+ shows "test_bit (set_bit w n x) m =
(if m = n then n < size w & x else test_bit w m)"
apply (unfold word_size word_test_bit_def word_set_bit_def)
apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
@@ -2562,7 +2446,7 @@
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
unfolding of_bl_def bl_to_bin_rep_F by auto
-
+
lemma msb_nth:
fixes w :: "'a::len word"
shows "msb w = w !! (len_of TYPE('a) - 1)"
@@ -2576,7 +2460,7 @@
lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
- "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
+ "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
apply (unfold word_size td_ext_def')
apply safe
@@ -2605,28 +2489,28 @@
lemma word_set_set_same [simp]:
fixes w :: "'a::len0 word"
- shows "set_bit (set_bit w n x) n y = set_bit w n y"
+ shows "set_bit (set_bit w n x) n y = set_bit w n y"
by (rule word_eqI) (simp add : test_bit_set_gen word_size)
-
-lemma word_set_set_diff:
+
+lemma word_set_set_diff:
fixes w :: "'a::len0 word"
assumes "m ~= n"
- shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
+ shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
-lemma nth_sint:
+lemma nth_sint:
fixes w :: "'a::len word"
- defines "l \<equiv> len_of TYPE ('a)"
+ defines "l \<equiv> len_of TYPE('a)"
shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
unfolding sint_uint l_def
by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
lemma word_lsb_numeral [simp]:
- "lsb (numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (numeral bin)"
+ "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
unfolding word_lsb_alt test_bit_numeral by simp
lemma word_lsb_neg_numeral [simp]:
- "lsb (- numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (- numeral bin)"
+ "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
unfolding word_lsb_alt test_bit_neg_numeral by simp
lemma set_bit_word_of_int:
@@ -2637,12 +2521,12 @@
done
lemma word_set_numeral [simp]:
- "set_bit (numeral bin::'a::len0 word) n b =
+ "set_bit (numeral bin::'a::len0 word) n b =
word_of_int (bin_sc n b (numeral bin))"
unfolding word_numeral_alt by (rule set_bit_word_of_int)
lemma word_set_neg_numeral [simp]:
- "set_bit (- numeral bin::'a::len0 word) n b =
+ "set_bit (- numeral bin::'a::len0 word) n b =
word_of_int (bin_sc n b (- numeral bin))"
unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
@@ -2662,8 +2546,8 @@
"clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
by (simp add: clearBit_def)
-lemma to_bl_n1:
- "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
+lemma to_bl_n1:
+ "to_bl (-1::'a::len0 word) = replicate (len_of TYPE('a)) True"
apply (rule word_bl.Abs_inverse')
apply simp
apply (rule word_eqI)
@@ -2674,7 +2558,7 @@
lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
unfolding word_msb_alt to_bl_n1 by simp
-lemma word_set_nth_iff:
+lemma word_set_nth_iff:
"(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
apply (rule iffI)
apply (rule disjCI)
@@ -2699,10 +2583,10 @@
unfolding test_bit_2p [symmetric] word_of_int [symmetric]
by simp
-lemma uint_2p:
+lemma uint_2p:
"(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
apply (unfold word_arith_power_alt)
- apply (case_tac "len_of TYPE ('a)")
+ apply (case_tac "len_of TYPE('a)")
apply clarsimp
apply (case_tac "nat")
apply clarsimp
@@ -2720,17 +2604,17 @@
apply simp_all
done
-lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
+lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
by (induct n) (simp_all add: wi_hom_syms)
-lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)"
- apply (rule xtr3)
+lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a::len word)"
+ apply (rule xtr3)
apply (rule_tac [2] y = "x" in le_word_or2)
apply (rule word_eqI)
apply (auto simp add: word_ao_nth nth_w2p word_size)
done
-lemma word_clr_le:
+lemma word_clr_le:
fixes w :: "'a::len0 word"
shows "w >= set_bit w n False"
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
@@ -2739,7 +2623,7 @@
apply simp
done
-lemma word_set_ge:
+lemma word_set_ge:
fixes w :: "'a::len word"
shows "w <= set_bit w n True"
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
@@ -2812,7 +2696,7 @@
apply arith
done
-lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
+lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
apply (unfold shiftr1_def word_test_bit_def)
@@ -2822,36 +2706,36 @@
apply simp
done
-lemma nth_shiftr:
+lemma nth_shiftr:
"\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
apply (unfold shiftr_def)
apply (induct "m")
apply (auto simp add : nth_shiftr1)
done
-
+
(* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
where f (ie bin_rest) takes normal arguments to normal results,
thus we get (2) from (1) *)
-lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
+lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
apply (subst bintr_uint [symmetric, OF order_refl])
apply (simp only : bintrunc_bintrunc_l)
- apply simp
+ apply simp
done
-lemma nth_sshiftr1:
+lemma nth_sshiftr1:
"sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
apply (unfold sshiftr1_def word_test_bit_def)
apply (simp add: nth_bintr word_ubin.eq_norm
- bin_nth.Suc [symmetric] word_size
+ bin_nth.Suc [symmetric] word_size
del: bin_nth.simps)
apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
apply (auto simp add: bin_nth_sint)
done
-lemma nth_sshiftr [rule_format] :
- "ALL n. sshiftr w m !! n = (n < size w &
+lemma nth_sshiftr [rule_format] :
+ "ALL n. sshiftr w m !! n = (n < size w &
(if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
apply (unfold sshiftr_def)
apply (induct_tac "m")
@@ -2872,7 +2756,7 @@
apply simp
apply arith+
done
-
+
lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
apply (unfold shiftr1_def bin_rest_def)
apply (rule word_uint.Abs_inverse)
@@ -2914,7 +2798,7 @@
subsubsection \<open>shift functions in terms of lists of bools\<close>
-lemmas bshiftr1_numeral [simp] =
+lemmas bshiftr1_numeral [simp] =
bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
@@ -2931,7 +2815,7 @@
qed
lemma bl_shiftl1:
- "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
+ "to_bl (shiftl1 (w :: 'a::len word)) = tl (to_bl w) @ [False]"
apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
apply (fast intro!: Suc_leI)
done
@@ -2948,8 +2832,8 @@
apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
done
-lemma bl_shiftr1:
- "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
+lemma bl_shiftr1:
+ "to_bl (shiftr1 (w :: 'a::len word)) = False # butlast (to_bl w)"
unfolding shiftr1_bl
by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
@@ -2961,7 +2845,7 @@
apply (simp add: shiftr1_bl of_bl_def)
done
-lemma shiftl1_rev:
+lemma shiftl1_rev:
"shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
apply (unfold word_reverse_def)
apply (rule word_bl.Rep_inverse' [symmetric])
@@ -2970,7 +2854,7 @@
apply auto
done
-lemma shiftl_rev:
+lemma shiftl_rev:
"shiftl w n = word_reverse (shiftr (word_reverse w) n)"
apply (unfold shiftl_def shiftr_def)
apply (induct "n")
@@ -2987,7 +2871,7 @@
by (simp add: shiftr_rev)
lemma bl_sshiftr1:
- "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
+ "to_bl (sshiftr1 (w :: 'a::len word)) = hd (to_bl w) # butlast (to_bl w)"
apply (unfold sshiftr1_def uint_bl word_size)
apply (simp add: butlast_rest_bin word_ubin.eq_norm)
apply (simp add: sint_uint)
@@ -2996,8 +2880,8 @@
apply clarsimp
apply (case_tac i)
apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
- nth_bin_to_bl bin_nth.Suc [symmetric]
- nth_sbintr
+ nth_bin_to_bl bin_nth.Suc [symmetric]
+ nth_sbintr
del: bin_nth.Suc)
apply force
apply (rule impI)
@@ -3005,8 +2889,8 @@
apply simp
done
-lemma drop_shiftr:
- "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)"
+lemma drop_shiftr:
+ "drop n (to_bl ((w :: 'a::len word) >> n)) = take (size w - n) (to_bl w)"
apply (unfold shiftr_def)
apply (induct n)
prefer 2
@@ -3015,8 +2899,8 @@
apply (auto simp: word_size)
done
-lemma drop_sshiftr:
- "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
+lemma drop_sshiftr:
+ "drop n (to_bl ((w :: 'a::len word) >>> n)) = take (size w - n) (to_bl w)"
apply (unfold sshiftr_def)
apply (induct n)
prefer 2
@@ -3036,8 +2920,8 @@
done
lemma take_sshiftr' [rule_format] :
- "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
- take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
+ "n <= size (w :: 'a::len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
+ take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
apply (unfold sshiftr_def)
apply (induct n)
prefer 2
@@ -3074,7 +2958,7 @@
"to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
by (simp add: shiftl_bl word_rep_drop word_size)
-lemma shiftl_zero_size:
+lemma shiftl_zero_size:
fixes x :: "'a::len0 word"
shows "size x <= n \<Longrightarrow> x << n = 0"
apply (unfold word_size)
@@ -3082,27 +2966,27 @@
apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
done
-(* note - the following results use 'a :: len word < number_ring *)
-
-lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
+(* note - the following results use 'a::len word < number_ring *)
+
+lemma shiftl1_2t: "shiftl1 (w :: 'a::len word) = 2 * w"
by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
-lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
+lemma shiftl1_p: "shiftl1 (w :: 'a::len word) = w + w"
by (simp add: shiftl1_2t)
-lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
- unfolding shiftl_def
+lemma shiftl_t2n: "shiftl (w :: 'a::len word) n = 2 ^ n * w"
+ unfolding shiftl_def
by (induct n) (auto simp: shiftl1_2t)
lemma shiftr1_bintr [simp]:
- "(shiftr1 (numeral w) :: 'a :: len0 word) =
- word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (numeral w)))"
+ "(shiftr1 (numeral w) :: 'a::len0 word) =
+ word_of_int (bin_rest (bintrunc (len_of TYPE('a)) (numeral w)))"
unfolding shiftr1_def word_numeral_alt
by (simp add: word_ubin.eq_norm)
lemma sshiftr1_sbintr [simp]:
- "(sshiftr1 (numeral w) :: 'a :: len word) =
- word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (numeral w)))"
+ "(sshiftr1 (numeral w) :: 'a::len word) =
+ word_of_int (bin_rest (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
unfolding sshiftr1_def word_numeral_alt
by (simp add: word_sbin.eq_norm)
@@ -3126,7 +3010,7 @@
lemma shiftr1_bl_of:
"length bl \<le> len_of TYPE('a) \<Longrightarrow>
shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
- by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin
+ by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin
word_ubin.eq_norm trunc_bl2bin)
lemma shiftr_bl_of:
@@ -3155,14 +3039,14 @@
done
lemma zip_replicate:
- "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
+ "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
apply (induct ys arbitrary: n, simp_all)
apply (case_tac n, simp_all)
done
lemma align_lem_or [rule_format] :
- "ALL x m. length x = n + m --> length y = n + m -->
- drop m x = replicate n False --> take m y = replicate m False -->
+ "ALL x m. length x = n + m --> length y = n + m -->
+ drop m x = replicate n False --> take m y = replicate m False -->
map2 op | x y = take m x @ drop m y"
apply (induct_tac y)
apply force
@@ -3174,8 +3058,8 @@
done
lemma align_lem_and [rule_format] :
- "ALL x m. length x = n + m --> length y = n + m -->
- drop m x = replicate n False --> take m y = replicate m False -->
+ "ALL x m. length x = n + m --> length y = n + m -->
+ drop m x = replicate n False --> take m y = replicate m False -->
map2 op & x y = replicate (n + m) False"
apply (induct_tac y)
apply force
@@ -3188,7 +3072,7 @@
lemma aligned_bl_add_size [OF refl]:
"size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
- take m (to_bl y) = replicate m False \<Longrightarrow>
+ take m (to_bl y) = replicate m False \<Longrightarrow>
to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
apply (subgoal_tac "x AND y = 0")
prefer 2
@@ -3240,8 +3124,8 @@
unfolding word_numeral_alt by (rule and_mask_wi)
lemma bl_and_mask':
- "to_bl (w AND mask n :: 'a :: len word) =
- replicate (len_of TYPE('a) - n) False @
+ "to_bl (w AND mask n :: 'a::len word) =
+ replicate (len_of TYPE('a) - n) False @
drop (len_of TYPE('a) - n) (to_bl w)"
apply (rule nth_equalityI)
apply simp
@@ -3284,24 +3168,24 @@
lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
apply (unfold unat_def)
apply (rule trans [OF _ and_mask_dvd])
- apply (unfold dvd_def)
- apply auto
+ apply (unfold dvd_def)
+ apply auto
apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
apply (simp add : of_nat_mult of_nat_power)
apply (simp add : nat_mult_distrib nat_power_eq)
done
-lemma word_2p_lem:
- "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
+lemma word_2p_lem:
+ "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a::len word) < 2 ^ n)"
apply (unfold word_size word_less_alt word_numeral_alt)
- apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
+ apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
mod_pos_pos_trivial
simp del: word_of_int_numeral)
done
-lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
+lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a::len word)"
apply (unfold word_less_alt word_numeral_alt)
- apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
+ apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
word_uint.eq_norm
simp del: word_of_int_numeral)
apply (drule xtr8 [rotated])
@@ -3317,8 +3201,8 @@
unfolding word_size by (erule and_mask_less')
lemma word_mod_2p_is_mask [OF refl]:
- "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n"
- by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
+ "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a::len word) AND mask n"
+ by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
lemma mask_eqs:
"(a AND mask n) + b AND mask n = a + b AND mask n"
@@ -3348,16 +3232,16 @@
lemmas revcast_def'' = revcast_def' [simplified word_size]
lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
-lemma to_bl_revcast:
- "to_bl (revcast w :: 'a :: len0 word) =
- takefill False (len_of TYPE ('a)) (to_bl w)"
+lemma to_bl_revcast:
+ "to_bl (revcast w :: 'a::len0 word) =
+ takefill False (len_of TYPE('a)) (to_bl w)"
apply (unfold revcast_def' word_size)
apply (rule word_bl.Abs_inverse)
apply simp
done
-lemma revcast_rev_ucast [OF refl refl refl]:
- "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
+lemma revcast_rev_ucast [OF refl refl refl]:
+ "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
rc = word_reverse uc"
apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
@@ -3379,8 +3263,8 @@
lemmas wsst_TYs = source_size target_size word_size
lemma revcast_down_uu [OF refl]:
- "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
- rc (w :: 'a :: len word) = ucast (w >> n)"
+ "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
+ rc (w :: 'a::len word) = ucast (w >> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule ucast_down_drop)
@@ -3390,8 +3274,8 @@
done
lemma revcast_down_us [OF refl]:
- "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
- rc (w :: 'a :: len word) = ucast (w >>> n)"
+ "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
+ rc (w :: 'a::len word) = ucast (w >>> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule ucast_down_drop)
@@ -3401,8 +3285,8 @@
done
lemma revcast_down_su [OF refl]:
- "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
- rc (w :: 'a :: len word) = scast (w >> n)"
+ "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
+ rc (w :: 'a::len word) = scast (w >> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule scast_down_drop)
@@ -3412,8 +3296,8 @@
done
lemma revcast_down_ss [OF refl]:
- "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
- rc (w :: 'a :: len word) = scast (w >>> n)"
+ "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
+ rc (w :: 'a::len word) = scast (w >>> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule scast_down_drop)
@@ -3423,9 +3307,9 @@
done
(* FIXME: should this also be [OF refl] ? *)
-lemma cast_down_rev:
- "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
- uc w = revcast ((w :: 'a :: len word) << n)"
+lemma cast_down_rev:
+ "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
+ uc w = revcast ((w :: 'a::len word) << n)"
apply (unfold shiftl_rev)
apply clarify
apply (simp add: revcast_rev_ucast)
@@ -3436,8 +3320,8 @@
done
lemma revcast_up [OF refl]:
- "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
- rc w = (ucast w :: 'a :: len word) << n"
+ "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
+ rc w = (ucast w :: 'a::len word) << n"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (simp add: takefill_alt)
@@ -3446,26 +3330,26 @@
apply (auto simp add: wsst_TYs)
done
-lemmas rc1 = revcast_up [THEN
+lemmas rc1 = revcast_up [THEN
revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
-lemmas rc2 = revcast_down_uu [THEN
+lemmas rc2 = revcast_down_uu [THEN
revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
lemmas ucast_up =
rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
-lemmas ucast_down =
+lemmas ucast_down =
rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
subsubsection \<open>Slices\<close>
lemma slice1_no_bin [simp]:
- "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
+ "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
by (simp add: slice1_def) (* TODO: neg_numeral *)
lemma slice_no_bin [simp]:
- "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
- (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
+ "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b::len0) - n)
+ (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
by (simp add: slice_def word_size) (* TODO: neg_numeral *)
lemma slice1_0 [simp] : "slice1 n 0 = 0"
@@ -3480,7 +3364,7 @@
lemmas slice_take = slice_take' [unfolded word_size]
-\<comment> "shiftr to a word of the same size is just slice,
+\<comment> "shiftr to a word of the same size is just slice,
slice is just shiftr then ucast"
lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
@@ -3490,34 +3374,34 @@
apply (simp add: word_size)
done
-lemma nth_slice:
- "(slice n w :: 'a :: len0 word) !! m =
- (w !! (m + n) & m < len_of TYPE ('a))"
- unfolding slice_shiftr
+lemma nth_slice:
+ "(slice n w :: 'a::len0 word) !! m =
+ (w !! (m + n) & m < len_of TYPE('a))"
+ unfolding slice_shiftr
by (simp add : nth_ucast nth_shiftr)
-lemma slice1_down_alt':
- "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
+lemma slice1_down_alt':
+ "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
to_bl sl = takefill False fs (drop k (to_bl w))"
unfolding slice1_def word_size of_bl_def uint_bl
by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
-lemma slice1_up_alt':
- "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
+lemma slice1_up_alt':
+ "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
apply (unfold slice1_def word_size of_bl_def uint_bl)
- apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
+ apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
takefill_append [symmetric])
apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
(replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
apply arith
done
-
+
lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
-lemmas slice1_up_alts =
- le_add_diff_inverse [symmetric, THEN su1]
+lemmas slice1_up_alts =
+ le_add_diff_inverse [symmetric, THEN su1]
le_add_diff_inverse2 [symmetric, THEN su1]
lemma ucast_slice1: "ucast w = slice1 (size w) w"
@@ -3530,21 +3414,21 @@
lemma slice_id: "slice 0 t = t"
by (simp only: ucast_slice [symmetric] ucast_id)
-lemma revcast_slice1 [OF refl]:
+lemma revcast_slice1 [OF refl]:
"rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
unfolding slice1_def revcast_def' by (simp add : word_size)
-lemma slice1_tf_tf':
- "to_bl (slice1 n w :: 'a :: len0 word) =
+lemma slice1_tf_tf':
+ "to_bl (slice1 n w :: 'a::len0 word) =
rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
unfolding slice1_def by (rule word_rev_tf)
lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
lemma rev_slice1:
- "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
- slice1 n (word_reverse w :: 'b :: len0 word) =
- word_reverse (slice1 k w :: 'a :: len0 word)"
+ "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
+ slice1 n (word_reverse w :: 'b::len0 word) =
+ word_reverse (slice1 k w :: 'a::len0 word)"
apply (unfold word_reverse_def slice1_tf_tf)
apply (rule word_bl.Rep_inverse')
apply (rule rev_swap [THEN iffD1])
@@ -3562,17 +3446,17 @@
apply arith
done
-lemmas sym_notr =
+lemmas sym_notr =
not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
\<comment> \<open>problem posed by TPHOLs referee:
criterion for overflow of addition of signed integers\<close>
lemma sofl_test:
- "(sint (x :: 'a :: len word) + sint y = sint (x + y)) =
+ "(sint (x :: 'a::len word) + sint y = sint (x + y)) =
((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
apply (unfold word_size)
- apply (cases "len_of TYPE('a)", simp)
+ apply (cases "len_of TYPE('a)", simp)
apply (subst msb_shift [THEN sym_notr])
apply (simp add: word_ops_msb)
apply (simp add: word_msb_sint)
@@ -3583,7 +3467,7 @@
apply safe
apply (insert sint_range' [where x=x])
apply (insert sint_range' [where x=y])
- defer
+ defer
apply (simp (no_asm), arith)
apply (simp (no_asm), arith)
defer
@@ -3592,7 +3476,7 @@
apply (simp (no_asm), arith)
apply (rule notI [THEN notnotD],
drule leI not_le_imp_less,
- drule sbintrunc_inc sbintrunc_dec,
+ drule sbintrunc_inc sbintrunc_dec,
simp)+
done
@@ -3603,8 +3487,8 @@
lemmas word_cat_bin' = word_cat_def
lemma word_rsplit_no:
- "(word_rsplit (numeral bin :: 'b :: len0 word) :: 'a word list) =
- map word_of_int (bin_rsplit (len_of TYPE('a :: len))
+ "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
+ map word_of_int (bin_rsplit (len_of TYPE('a::len))
(len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
@@ -3612,7 +3496,7 @@
[unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
lemma test_bit_cat:
- "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
+ "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
(if n < size b then b !! n else a !! (n - size b)))"
apply (unfold word_cat_bin' test_bit_bin)
apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
@@ -3625,7 +3509,7 @@
done
lemma of_bl_append:
- "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
+ "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
apply (unfold of_bl_def)
apply (simp add: bl_to_bin_app_cat bin_cat_num)
apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
@@ -3645,7 +3529,7 @@
"of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
by (cases x) simp_all
-lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow>
+lemma split_uint_lem: "bin_split n (uint (w :: 'a::len0 word)) = (a, b) \<Longrightarrow>
a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
apply (frule word_ubin.norm_Rep [THEN ssubst])
apply (drule bin_split_trunc1)
@@ -3654,8 +3538,8 @@
apply safe
done
-lemma word_split_bl':
- "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
+lemma word_split_bl':
+ "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
(a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
apply (unfold word_split_bin')
apply safe
@@ -3665,7 +3549,7 @@
apply (drule word_ubin.norm_Rep [THEN ssubst])
apply (drule split_bintrunc)
apply (simp add : of_bl_def bl2bin_drop word_size
- word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
+ word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
apply (clarsimp split: prod.splits)
apply (frule split_uint_lem [THEN conjunct1])
apply (unfold word_size)
@@ -3682,8 +3566,8 @@
apply (simp add : word_ubin.norm_eq_iff [symmetric])
done
-lemma word_split_bl: "std = size c - size b \<Longrightarrow>
- (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
+lemma word_split_bl: "std = size c - size b \<Longrightarrow>
+ (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
word_split c = (a, b)"
apply (rule iffI)
defer
@@ -3695,7 +3579,7 @@
done
lemma word_split_bl_eq:
- "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
+ "(word_split (c::'a::len word) :: ('c::len0 word * 'd::len0 word)) =
(of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
apply (rule word_split_bl [THEN iffD1])
@@ -3705,7 +3589,7 @@
\<comment> "keep quantifiers for use in simplification"
lemma test_bit_split':
- "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
+ "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
a !! m = (m < size a & c !! (m + size b)))"
apply (unfold word_split_bin' test_bit_bin)
apply (clarify)
@@ -3721,7 +3605,7 @@
(\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
by (simp add: test_bit_split')
-lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow>
+lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow>
((ALL n::nat. b !! n = (n < size b & c !! n)) &
(ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
apply (rule_tac iffI)
@@ -3734,7 +3618,7 @@
apply (fastforce intro ! : word_eqI simp add : word_size)
done
-\<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
+\<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
result to the length given by the result type\<close>
lemma word_cat_id: "word_cat a b = b"
@@ -3742,11 +3626,11 @@
\<comment> "limited hom result"
lemma word_cat_hom:
- "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
+ "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE('c::len0)
\<Longrightarrow>
- (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
+ (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
word_of_int (bin_cat w (size b) (uint b))"
- apply (unfold word_cat_def word_size)
+ apply (unfold word_cat_def word_size)
apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
word_ubin.eq_norm bintr_cat min.absorb1)
done
@@ -3765,7 +3649,7 @@
subsubsection \<open>Split and slice\<close>
-lemma split_slices:
+lemma split_slices:
"word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
apply (drule test_bit_split)
apply (rule conjI)
@@ -3809,19 +3693,19 @@
word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
text \<open>this odd result arises from the fact that the statement of the
- result implies that the decoded words are of the same type,
+ result implies that the decoded words are of the same type,
and therefore of the same length, as the original word\<close>
lemma word_rsplit_same: "word_rsplit w = [w]"
unfolding word_rsplit_def by (simp add : bin_rsplit_all)
lemma word_rsplit_empty_iff_size:
- "(word_rsplit w = []) = (size w = 0)"
+ "(word_rsplit w = []) = (size w = 0)"
unfolding word_rsplit_def bin_rsplit_def word_size
by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
lemma test_bit_rsplit:
- "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow>
+ "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
apply (unfold word_rsplit_def word_test_bit_def)
apply (rule trans)
@@ -3858,71 +3742,71 @@
apply (induct "wl")
apply clarsimp
apply (clarsimp simp add : nth_append size_rcat_lem)
- apply (simp (no_asm_use) only: mult_Suc [symmetric]
+ apply (simp (no_asm_use) only: mult_Suc [symmetric]
td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
apply clarsimp
done
lemma test_bit_rcat:
- "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
+ "sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
(n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
apply (unfold word_rcat_bl word_size)
- apply (clarsimp simp add :
+ apply (clarsimp simp add :
test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
apply safe
- apply (auto simp add :
+ apply (auto simp add :
test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
done
lemma foldl_eq_foldr:
- "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
+ "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
by (induct xs arbitrary: x) (auto simp add : add.assoc)
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
-lemmas test_bit_rsplit_alt =
- trans [OF nth_rev_alt [THEN test_bit_cong]
+lemmas test_bit_rsplit_alt =
+ trans [OF nth_rev_alt [THEN test_bit_cong]
test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
\<comment> "lazy way of expressing that u and v, and su and sv, have same types"
lemma word_rsplit_len_indep [OF refl refl refl refl]:
- "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
+ "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
word_rsplit v = sv \<Longrightarrow> length su = length sv"
apply (unfold word_rsplit_def)
apply (auto simp add : bin_rsplit_len_indep)
done
-lemma length_word_rsplit_size:
- "n = len_of TYPE ('a :: len) \<Longrightarrow>
+lemma length_word_rsplit_size:
+ "n = len_of TYPE('a::len) \<Longrightarrow>
(length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
apply (unfold word_rsplit_def word_size)
apply (clarsimp simp add : bin_rsplit_len_le)
done
-lemmas length_word_rsplit_lt_size =
+lemmas length_word_rsplit_lt_size =
length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
lemma length_word_rsplit_exp_size:
- "n = len_of TYPE ('a :: len) \<Longrightarrow>
+ "n = len_of TYPE('a::len) \<Longrightarrow>
length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
-lemma length_word_rsplit_even_size:
- "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow>
+lemma length_word_rsplit_even_size:
+ "n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
length (word_rsplit w :: 'a word list) = m"
by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
(* alternative proof of word_rcat_rsplit *)
-lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
+lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
lemmas dtle = xtr4 [OF tdle mult.commute]
lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
apply (rule word_eqI)
apply (clarsimp simp add : test_bit_rcat word_size)
apply (subst refl [THEN test_bit_rsplit])
- apply (simp_all add: word_size
+ apply (simp_all add: word_size
refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
apply safe
apply (erule xtr7, rule len_gt_0 [THEN dtle])+
@@ -3943,8 +3827,8 @@
by (auto simp: add.commute)
lemma word_rsplit_rcat_size [OF refl]:
- "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>
- size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws"
+ "word_rcat (ws :: 'a::len word list) = frcw \<Longrightarrow>
+ size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
apply (frule size_word_rsplit_rcat_size, assumption)
apply (clarsimp simp add : word_size)
apply (rule nth_equalityI, assumption)
@@ -3973,7 +3857,7 @@
lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
-lemma rotate_eq_mod:
+lemma rotate_eq_mod:
"m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
apply (rule box_equals)
defer
@@ -3981,11 +3865,11 @@
apply simp
done
-lemmas rotate_eqs =
+lemmas rotate_eqs =
trans [OF rotate0 [THEN fun_cong] id_apply]
- rotate_rotate [symmetric]
+ rotate_rotate [symmetric]
rotate_id
- rotate_conv_mod
+ rotate_conv_mod
rotate_eq_mod
@@ -4009,31 +3893,31 @@
apply (simp add : rotater1_def)
apply (simp add : rotate1_rl')
done
-
+
lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
using rotater_rev' [where xs = "rev ys"] by simp
-lemma rotater_drop_take:
- "rotater n xs =
+lemma rotater_drop_take:
+ "rotater n xs =
drop (length xs - n mod length xs) xs @
take (length xs - n mod length xs) xs"
by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
-lemma rotater_Suc [simp] :
+lemma rotater_Suc [simp] :
"rotater (Suc n) xs = rotater1 (rotater n xs)"
unfolding rotater_def by auto
lemma rotate_inv_plus [rule_format] :
- "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
- rotate k (rotater n xs) = rotate m xs &
- rotater n (rotate k xs) = rotate m xs &
+ "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
+ rotate k (rotater n xs) = rotate m xs &
+ rotater n (rotate k xs) = rotate m xs &
rotate n (rotater k xs) = rotater m xs"
unfolding rotater_def rotate_def
by (induct n) (auto intro: funpow_swap1 [THEN trans])
-
+
lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
@@ -4047,7 +3931,7 @@
lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
by auto
-lemma length_rotater [simp]:
+lemma length_rotater [simp]:
"length (rotater n xs) = length xs"
by (simp add : rotater_rev)
@@ -4056,7 +3940,7 @@
shows "(x = z) = (y = z)"
using assms by simp
-lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
+lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
lemmas rotater_eqs = rrs1 [simplified length_rotater]
@@ -4070,28 +3954,28 @@
"xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
by (induct xs) auto
-lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
+lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
unfolding rotater1_def
by (cases xs) (auto simp add: last_map butlast_map)
lemma rotater_map:
- "rotater n (map f xs) = map f (rotater n xs)"
+ "rotater n (map f xs) = map f (rotater n xs)"
unfolding rotater_def
by (induct n) (auto simp add : rotater1_map)
lemma but_last_zip [rule_format] :
- "ALL ys. length xs = length ys --> xs ~= [] -->
- last (zip xs ys) = (last xs, last ys) &
- butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
+ "ALL ys. length xs = length ys --> xs ~= [] -->
+ last (zip xs ys) = (last xs, last ys) &
+ butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
apply (induct "xs")
apply auto
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
done
lemma but_last_map2 [rule_format] :
- "ALL ys. length xs = length ys --> xs ~= [] -->
- last (map2 f xs ys) = f (last xs) (last ys) &
- butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
+ "ALL ys. length xs = length ys --> xs ~= [] -->
+ last (map2 f xs ys) = f (last xs) (last ys) &
+ butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
apply (induct "xs")
apply auto
apply (unfold map2_def)
@@ -4099,8 +3983,8 @@
done
lemma rotater1_zip:
- "length xs = length ys \<Longrightarrow>
- rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
+ "length xs = length ys \<Longrightarrow>
+ rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
apply (unfold rotater1_def)
apply (cases "xs")
apply auto
@@ -4108,40 +3992,40 @@
done
lemma rotater1_map2:
- "length xs = length ys \<Longrightarrow>
- rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
+ "length xs = length ys \<Longrightarrow>
+ rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
unfolding map2_def by (simp add: rotater1_map rotater1_zip)
-lemmas lrth =
- box_equals [OF asm_rl length_rotater [symmetric]
- length_rotater [symmetric],
+lemmas lrth =
+ box_equals [OF asm_rl length_rotater [symmetric]
+ length_rotater [symmetric],
THEN rotater1_map2]
-lemma rotater_map2:
- "length xs = length ys \<Longrightarrow>
- rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
+lemma rotater_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
by (induct n) (auto intro!: lrth)
lemma rotate1_map2:
- "length xs = length ys \<Longrightarrow>
- rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
+ "length xs = length ys \<Longrightarrow>
+ rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
apply (unfold map2_def)
apply (cases xs)
apply (cases ys, auto)+
done
-lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
+lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
length_rotate [symmetric], THEN rotate1_map2]
-lemma rotate_map2:
- "length xs = length ys \<Longrightarrow>
- rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
+lemma rotate_map2:
+ "length xs = length ys \<Longrightarrow>
+ rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
by (induct n) (auto intro!: lth)
\<comment> "corresponding equalities for word rotation"
-lemma to_bl_rotl:
+lemma to_bl_rotl:
"to_bl (word_rotl n w) = rotate n (to_bl w)"
by (simp add: word_bl.Abs_inverse' word_rotl_def)
@@ -4150,7 +4034,7 @@
lemmas word_rotl_eqs =
blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
-lemma to_bl_rotr:
+lemma to_bl_rotr:
"to_bl (word_rotr n w) = rotater n (to_bl w)"
by (simp add: word_bl.Abs_inverse' word_rotr_def)
@@ -4174,31 +4058,31 @@
"(word_rotr n v = w) = (word_rotl n w = v)" and
word_rot_gal':
"(w = word_rotr n v) = (v = word_rotl n w)"
- by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
+ by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
dest: sym)
lemma word_rotr_rev:
"word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
to_bl_rotr to_bl_rotl rotater_rev)
-
+
lemma word_roti_0 [simp]: "word_roti 0 w = w"
by (unfold word_rot_defs) auto
lemmas abl_cong = arg_cong [where f = "of_bl"]
-lemma word_roti_add:
+lemma word_roti_add:
"word_roti (m + n) w = word_roti m (word_roti n w)"
proof -
- have rotater_eq_lem:
+ have rotater_eq_lem:
"\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
by auto
- have rotate_eq_lem:
+ have rotate_eq_lem:
"\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
by auto
- note rpts [symmetric] =
+ note rpts [symmetric] =
rotate_inv_plus [THEN conjunct1]
rotate_inv_plus [THEN conjunct2, THEN conjunct1]
rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
@@ -4211,16 +4095,16 @@
apply (unfold word_rot_defs)
apply (simp only: split: if_split)
apply (safe intro!: abl_cong)
- apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
+ apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
to_bl_rotl
to_bl_rotr [THEN word_bl.Rep_inverse']
to_bl_rotr)
apply (rule rrp rrrp rpts,
- simp add: nat_add_distrib [symmetric]
+ simp add: nat_add_distrib [symmetric]
nat_diff_distrib [symmetric])+
done
qed
-
+
lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
apply (unfold word_rot_defs)
apply (cut_tac y="size w" in gt_or_eq_0)
@@ -4244,7 +4128,7 @@
subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
(* using locale to not pollute lemma namespace *)
-locale word_rotate
+locale word_rotate
begin
lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
@@ -4267,11 +4151,11 @@
"word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
"word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
"word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
- "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
+ "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
by (rule word_bl.Rep_eqD,
rule word_rot_defs' [THEN trans],
simp only: blwl_syms [symmetric],
- rule th1s [THEN trans],
+ rule th1s [THEN trans],
rule refl)+
end
@@ -4283,8 +4167,8 @@
lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
simplified word_bl_Rep']
-lemma bl_word_roti_dt':
- "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow>
+lemma bl_word_roti_dt':
+ "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
apply (unfold word_roti_def)
apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
@@ -4292,7 +4176,7 @@
apply (simp add: zmod_zminus1_eq_if)
apply safe
apply (simp add: nat_mult_distrib)
- apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
+ apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
[THEN conjunct2, THEN order_less_imp_le]]
nat_mod_distrib)
apply (simp add: nat_mod_distrib)
@@ -4300,7 +4184,7 @@
lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
-lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
+lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
@@ -4310,11 +4194,11 @@
lemma word_roti_0' [simp] : "word_roti n 0 = 0"
unfolding word_roti_def by auto
-lemmas word_rotr_dt_no_bin' [simp] =
+lemmas word_rotr_dt_no_bin' [simp] =
word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
(* FIXME: negative numerals, 0 and 1 *)
-lemmas word_rotl_dt_no_bin' [simp] =
+lemmas word_rotl_dt_no_bin' [simp] =
word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
(* FIXME: negative numerals, 0 and 1 *)
@@ -4337,7 +4221,7 @@
lemma max_word_max [simp,intro!]: "n \<le> max_word"
by (cases n rule: word_int_cases)
(simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
-
+
lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
by (subst word_uint.Abs_norm [symmetric]) simp
@@ -4356,7 +4240,7 @@
apply (simp add: word_pow_0)
done
-lemma max_word_minus:
+lemma max_word_minus:
"max_word = (-1::'a::len word)"
proof -
have "-1 + 1 = (0::'a word)" by simp
@@ -4430,8 +4314,8 @@
"(x::'a::len0 word) >> 0 = x"
by (simp add: shiftr_bl)
-lemma shiftl_x_0 [simp]:
- "(x :: 'a :: len word) << 0 = x"
+lemma shiftl_x_0 [simp]:
+ "(x :: 'a::len word) << 0 = x"
by (simp add: shiftl_t2n)
lemma shiftl_1 [simp]:
@@ -4442,21 +4326,21 @@
"uint x < 0 = False"
by (simp add: linorder_not_less)
-lemma shiftr1_1 [simp]:
+lemma shiftr1_1 [simp]:
"shiftr1 (1::'a::len word) = 0"
unfolding shiftr1_def by simp
-lemma shiftr_1[simp]:
+lemma shiftr_1[simp]:
"(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
by (induct n) (auto simp: shiftr_def)
-lemma word_less_1 [simp]:
+lemma word_less_1 [simp]:
"((x::'a::len word) < 1) = (x = 0)"
by (simp add: word_less_nat_alt unat_0_iff)
lemma to_bl_mask:
- "to_bl (mask n :: 'a::len word) =
- replicate (len_of TYPE('a) - n) False @
+ "to_bl (mask n :: 'a::len word) =
+ replicate (len_of TYPE('a) - n) False @
replicate (min (len_of TYPE('a)) n) True"
by (simp add: mask_bl word_rep_drop min_def)
@@ -4475,15 +4359,15 @@
fixes n
defines "n' \<equiv> len_of TYPE('a) - n"
shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
-proof -
+proof -
note [simp] = map_replicate_True map_replicate_False
- have "to_bl (w AND mask n) =
+ have "to_bl (w AND mask n) =
map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
by (simp add: bl_word_and)
also
have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
also
- have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
+ have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
replicate n' False @ drop n' (to_bl w)"
unfolding to_bl_mask n'_def map2_def
by (subst zip_append) auto
@@ -4501,41 +4385,41 @@
by (induct xs) auto
lemma uint_plus_if_size:
- "uint (x + y) =
- (if uint x + uint y < 2^size x then
- uint x + uint y
- else
- uint x + uint y - 2^size x)"
- by (simp add: word_arith_wis int_word_uint mod_add_if_z
+ "uint (x + y) =
+ (if uint x + uint y < 2^size x then
+ uint x + uint y
+ else
+ uint x + uint y - 2^size x)"
+ by (simp add: word_arith_wis int_word_uint mod_add_if_z
word_size)
lemma unat_plus_if_size:
- "unat (x + (y::'a::len word)) =
- (if unat x + unat y < 2^size x then
- unat x + unat y
- else
- unat x + unat y - 2^size x)"
+ "unat (x + (y::'a::len word)) =
+ (if unat x + unat y < 2^size x then
+ unat x + unat y
+ else
+ unat x + unat y - 2^size x)"
apply (subst word_arith_nat_defs)
apply (subst unat_of_nat)
apply (simp add: mod_nat_add word_size)
done
lemma word_neq_0_conv:
- fixes w :: "'a :: len word"
+ fixes w :: "'a::len word"
shows "(w \<noteq> 0) = (0 < w)"
unfolding word_gt_0 by simp
lemma max_lt:
- "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
+ "unat (max a b div c) = unat (max a b) div unat (c:: 'a::len word)"
by (fact unat_div)
lemma uint_sub_if_size:
- "uint (x - y) =
- (if uint y \<le> uint x then
- uint x - uint y
- else
+ "uint (x - y) =
+ (if uint y \<le> uint x then
+ uint x - uint y
+ else
uint x - uint y + 2^size x)"
- by (simp add: word_arith_wis int_word_uint mod_sub_if_z
+ by (simp add: word_arith_wis int_word_uint mod_sub_if_z
word_size)
lemma unat_sub:
@@ -4544,8 +4428,8 @@
lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
-
-lemma word_of_int_minus:
+
+lemma word_of_int_minus:
"word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
proof -
have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
@@ -4555,8 +4439,8 @@
apply simp
done
qed
-
-lemmas word_of_int_inj =
+
+lemmas word_of_int_inj =
word_uint.Abs_inject [unfolded uints_num, simplified]
lemma word_le_less_eq:
@@ -4586,7 +4470,7 @@
using 1 2 3 4 [symmetric]
by (auto intro: mod_diff_cong)
-lemma word_induct_less:
+lemma word_induct_less:
"\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
apply (cases m)
apply atomize
@@ -4608,12 +4492,12 @@
apply (clarsimp simp: unat_of_nat)
apply simp
done
-
-lemma word_induct:
+
+lemma word_induct:
"\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
by (erule word_induct_less, simp)
-lemma word_induct2 [induct type]:
+lemma word_induct2 [induct type]:
"\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
apply (rule word_induct, simp)
apply (case_tac "1+n = 0", auto)
@@ -4629,7 +4513,7 @@
lemma word_rec_0: "word_rec z s 0 = z"
by (simp add: word_rec_def)
-lemma word_rec_Suc:
+lemma word_rec_Suc:
"1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
apply (simp add: word_rec_def unat_word_ariths)
apply (subst nat_mod_eq')
@@ -4637,7 +4521,7 @@
apply simp
done
-lemma word_rec_Pred:
+lemma word_rec_Pred:
"n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
apply (rule subst[where t="n" and s="1 + (n - 1)"])
apply simp
@@ -4646,15 +4530,15 @@
apply simp
done
-lemma word_rec_in:
+lemma word_rec_in:
"f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
-lemma word_rec_in2:
+lemma word_rec_in2:
"f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
-lemma word_rec_twice:
+lemma word_rec_twice:
"m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
apply (erule rev_mp)
apply (rule_tac x=z in spec)
@@ -4699,7 +4583,7 @@
apply simp
done
-lemma word_rec_max:
+lemma word_rec_max:
"\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
apply simp
@@ -4708,7 +4592,7 @@
apply clarsimp
apply (drule spec, rule mp, erule mp)
apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
- prefer 2
+ prefer 2
apply assumption
apply simp
apply (erule contrapos_pn)
@@ -4717,7 +4601,7 @@
apply simp
done
-lemma unatSuc:
+lemma unatSuc:
"1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
by unat_arith