--- a/src/HOL/Word/Bit_Representation.thy Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Tue Apr 16 19:50:03 2019 +0000
@@ -2,7 +2,7 @@
Author: Jeremy Dawson, NICTA
*)
-section \<open>Integers as implict bit strings\<close>
+section \<open>Integers as implicit bit strings\<close>
theory Bit_Representation
imports Misc_Numeric
@@ -25,6 +25,9 @@
lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
by (rule trans, rule Bit_B1) simp
+lemma power_BIT: "2 ^ Suc n - 1 = (2 ^ n - 1) BIT True"
+ by (simp add: Bit_B1)
+
definition bin_last :: "int \<Rightarrow> bool"
where "bin_last w \<longleftrightarrow> w mod 2 = 1"
@@ -242,6 +245,14 @@
bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1
bin_nth_numeral_simps
+lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)" \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
+ apply (induct n arbitrary: m)
+ apply clarsimp
+ apply safe
+ apply (case_tac m)
+ apply (auto simp: Bit_B0_2t [symmetric])
+ done
+
subsection \<open>Truncating binary integers\<close>
@@ -682,4 +693,129 @@
Z: "bin_cat w 0 v = w"
| Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
+lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
+ by (induct n arbitrary: y) auto
+
+lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
+ by auto
+
+lemma bin_cat_assoc: "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
+ by (induct n arbitrary: z) auto
+
+lemma bin_cat_assoc_sym: "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
+ apply (induct n arbitrary: z m)
+ apply clarsimp
+ apply (case_tac m, auto)
+ done
+
+definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
+ where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
+
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+ where "bin_rsplit_aux n m c bs =
+ (if m = 0 \<or> n = 0 then bs
+ else
+ let (a, b) = bin_split n c
+ in bin_rsplit_aux n (m - n) a (b # bs))"
+
+definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+ where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
+
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+ where "bin_rsplitl_aux n m c bs =
+ (if m = 0 \<or> n = 0 then bs
+ else
+ let (a, b) = bin_split (min m n) c
+ in bin_rsplitl_aux n (m - n) a (b # bs))"
+
+definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+ where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
+
+declare bin_rsplit_aux.simps [simp del]
+declare bin_rsplitl_aux.simps [simp del]
+
+lemma bin_nth_cat:
+ "bin_nth (bin_cat x k y) n =
+ (if n < k then bin_nth y n else bin_nth x (n - k))"
+ apply (induct k arbitrary: n y)
+ apply clarsimp
+ apply (case_tac n, auto)
+ done
+
+lemma bin_nth_split:
+ "bin_split n c = (a, b) \<Longrightarrow>
+ (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
+ (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
+ apply (induct n arbitrary: b c)
+ apply clarsimp
+ apply (clarsimp simp: Let_def split: prod.split_asm)
+ apply (case_tac k)
+ apply auto
+ done
+
+lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
+ by (induct n arbitrary: w) auto
+
+lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
+ by (induct n arbitrary: b) auto
+
+lemma bintr_cat: "bintrunc m (bin_cat a n b) =
+ bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
+ by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
+
+lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
+ by (auto simp add : bintr_cat)
+
+lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
+ by (induct n arbitrary: b) auto
+
+lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
+ by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
+
+lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
+ by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
+
+lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
+ by (induct n arbitrary: w) auto
+
+lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
+ by (induct n) auto
+
+lemma bin_split_minus1 [simp]:
+ "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
+ by (induct n) auto
+
+lemma bin_split_trunc:
+ "bin_split (min m n) c = (a, b) \<Longrightarrow>
+ bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
+ apply (induct n arbitrary: m b c, clarsimp)
+ apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
+ apply (case_tac m)
+ apply (auto simp: Let_def split: prod.split_asm)
+ done
+
+lemma bin_split_trunc1:
+ "bin_split n c = (a, b) \<Longrightarrow>
+ bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
+ apply (induct n arbitrary: m b c, clarsimp)
+ apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
+ apply (case_tac m)
+ apply (auto simp: Let_def split: prod.split_asm)
+ done
+
+lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
+ apply (induct n arbitrary: b)
+ apply clarsimp
+ apply (simp add: Bit_def)
+ done
+
+lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
+ apply (induct n arbitrary: b)
+ apply simp
+ apply (simp add: bin_rest_def zdiv_zmult2_eq)
+ apply (case_tac b rule: bin_exhaust)
+ apply simp
+ apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
+ done
+
end
--- a/src/HOL/Word/Bits_Int.thy Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:03 2019 +0000
@@ -9,7 +9,7 @@
section \<open>Bitwise Operations on Binary Integers\<close>
theory Bits_Int
- imports Bits Bit_Representation
+ imports Bits Bit_Representation Bool_List_Representation
begin
subsection \<open>Logical operations\<close>
@@ -365,6 +365,41 @@
apply (case_tac bit, auto)
done
+lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
+proof -
+ have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
+ by (simp add: mod_mult_mult1)
+ also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
+ by (simp add: ac_simps p1mod22k')
+ also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
+ by (simp only: mod_simps)
+ finally show ?thesis
+ by (auto simp add: Bit_def)
+qed
+
+lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
+ for x :: int
+proof (induct x arbitrary: n rule: bin_induct)
+ case 1
+ then show ?case
+ by simp
+next
+ case 2
+ then show ?case
+ by (simp, simp add: m1mod2k)
+next
+ case (3 bin bit)
+ show ?case
+ proof (cases n)
+ case 0
+ then show ?thesis by simp
+ next
+ case (Suc m)
+ with 3 show ?thesis
+ by (simp only: power_BIT mod_BIT int_and_Bits) simp
+ qed
+qed
+
subsubsection \<open>Truncating results of bit-wise operations\<close>
@@ -386,6 +421,53 @@
lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
+lemma bl_xor_aux_bin:
+ "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
+ apply (induct n arbitrary: v w bs cs)
+ apply simp
+ apply (case_tac v rule: bin_exhaust)
+ apply (case_tac w rule: bin_exhaust)
+ apply clarsimp
+ apply (case_tac b)
+ apply auto
+ done
+
+lemma bl_or_aux_bin:
+ "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
+ apply (induct n arbitrary: v w bs cs)
+ apply simp
+ apply (case_tac v rule: bin_exhaust)
+ apply (case_tac w rule: bin_exhaust)
+ apply clarsimp
+ done
+
+lemma bl_and_aux_bin:
+ "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
+ apply (induct n arbitrary: v w bs cs)
+ apply simp
+ apply (case_tac v rule: bin_exhaust)
+ apply (case_tac w rule: bin_exhaust)
+ apply clarsimp
+ done
+
+lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
+ by (induct n arbitrary: w cs) auto
+
+lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
+ by (simp add: bin_to_bl_def bl_not_aux_bin)
+
+lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
+ by (simp add: bin_to_bl_def bl_and_aux_bin)
+
+lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
+ by (simp add: bin_to_bl_def bl_or_aux_bin)
+
+lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+ by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
+
subsection \<open>Setting and clearing bits\<close>
@@ -470,186 +552,33 @@
bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
by (simp add: numeral_eq_Suc)
-
-subsection \<open>Splitting and concatenation\<close>
-
-definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
- where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
-
-fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
- where "bin_rsplit_aux n m c bs =
- (if m = 0 \<or> n = 0 then bs
- else
- let (a, b) = bin_split n c
- in bin_rsplit_aux n (m - n) a (b # bs))"
-
-definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
- where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
-
-fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
- where "bin_rsplitl_aux n m c bs =
- (if m = 0 \<or> n = 0 then bs
- else
- let (a, b) = bin_split (min m n) c
- in bin_rsplitl_aux n (m - n) a (b # bs))"
-
-definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
- where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
-
-declare bin_rsplit_aux.simps [simp del]
-declare bin_rsplitl_aux.simps [simp del]
-
-lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
- by (induct n arbitrary: y) auto
-
-lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
- by auto
-
-lemma bin_nth_cat:
- "bin_nth (bin_cat x k y) n =
- (if n < k then bin_nth y n else bin_nth x (n - k))"
- apply (induct k arbitrary: n y)
- apply clarsimp
- apply (case_tac n, auto)
- done
+instantiation int :: bitss
+begin
-lemma bin_nth_split:
- "bin_split n c = (a, b) \<Longrightarrow>
- (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
- (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
- apply (induct n arbitrary: b c)
- apply clarsimp
- apply (clarsimp simp: Let_def split: prod.split_asm)
- apply (case_tac k)
- apply auto
- done
-
-lemma bin_cat_assoc: "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
- by (induct n arbitrary: z) auto
-
-lemma bin_cat_assoc_sym: "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
- apply (induct n arbitrary: z m)
- apply clarsimp
- apply (case_tac m, auto)
- done
+definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
-lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
- by (induct n arbitrary: w) auto
-
-lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
- by (induct n arbitrary: b) auto
-
-lemma bintr_cat: "bintrunc m (bin_cat a n b) =
- bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
- by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
+definition "lsb i = i !! 0" for i :: int
-lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
- by (auto simp add : bintr_cat)
-
-lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
- by (induct n arbitrary: b) auto
-
-lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
- by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
-
-lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
- by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
-
-lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
- by (induct n arbitrary: w) auto
+definition "set_bit i n b = bin_sc n b i"
-lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
- by (induct n) auto
-
-lemma bin_split_minus1 [simp]:
- "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
- by (induct n) auto
-
-lemma bin_split_trunc:
- "bin_split (min m n) c = (a, b) \<Longrightarrow>
- bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
- apply (induct n arbitrary: m b c, clarsimp)
- apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
- apply (case_tac m)
- apply (auto simp: Let_def split: prod.split_asm)
- done
-
-lemma bin_split_trunc1:
- "bin_split n c = (a, b) \<Longrightarrow>
- bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
- apply (induct n arbitrary: m b c, clarsimp)
- apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
- apply (case_tac m)
- apply (auto simp: Let_def split: prod.split_asm)
- done
-
-lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
- apply (induct n arbitrary: b)
- apply clarsimp
- apply (simp add: Bit_def)
- done
-
-lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
- apply (induct n arbitrary: b)
- apply simp
- apply (simp add: bin_rest_def zdiv_zmult2_eq)
- apply (case_tac b rule: bin_exhaust)
- apply simp
- apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
- done
-
-
-subsection \<open>Miscellaneous lemmas\<close>
+definition
+ "set_bits f =
+ (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+ let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+ in bl_to_bin (rev (map f [0..<n]))
+ else if \<exists>n. \<forall>n'\<ge>n. f n' then
+ let n = LEAST n. \<forall>n'\<ge>n. f n'
+ in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+ else 0 :: int)"
-lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)"
- apply (induct n arbitrary: m)
- apply clarsimp
- apply safe
- apply (case_tac m)
- apply (auto simp: Bit_B0_2t [symmetric])
- done
+definition "shiftl x n = x * 2 ^ n" for x :: int
-\<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
-lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
- by auto
-
-lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
- by (induct n) (simp_all add: Bit_B1)
+definition "shiftr x n = x div 2 ^ n" for x :: int
-lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
-proof -
- have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
- by (simp add: mod_mult_mult1)
- also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
- by (simp add: ac_simps p1mod22k')
- also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
- by (simp only: mod_simps)
- finally show ?thesis
- by (auto simp add: Bit_def)
-qed
+definition "msb x \<longleftrightarrow> x < 0" for x :: int
-lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
- for x :: int
-proof (induct x arbitrary: n rule: bin_induct)
- case 1
- then show ?case
- by simp
-next
- case 2
- then show ?case
- by (simp, simp add: m1mod2k)
-next
- case (3 bin bit)
- show ?case
- proof (cases n)
- case 0
- then show ?thesis by simp
- next
- case (Suc m)
- with 3 show ?thesis
- by (simp only: power_BIT mod_BIT int_and_Bits) simp
- qed
-qed
+instance ..
end
+end
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Tue Apr 16 19:50:03 2019 +0000
@@ -6,10 +6,10 @@
and concatenation.
*)
-section "Bool lists and integers"
+section \<open>Bool lists and integers\<close>
theory Bool_List_Representation
- imports Bits_Int
+ imports Bit_Representation
begin
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -400,55 +400,6 @@
by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
-subsection \<open>Links between bit-wise operations and operations on bool lists\<close>
-
-lemma bl_xor_aux_bin:
- "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
- apply (induct n arbitrary: v w bs cs)
- apply simp
- apply (case_tac v rule: bin_exhaust)
- apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- apply (case_tac b)
- apply auto
- done
-
-lemma bl_or_aux_bin:
- "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
- apply (induct n arbitrary: v w bs cs)
- apply simp
- apply (case_tac v rule: bin_exhaust)
- apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- done
-
-lemma bl_and_aux_bin:
- "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
- apply (induct n arbitrary: v w bs cs)
- apply simp
- apply (case_tac v rule: bin_exhaust)
- apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- done
-
-lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
- by (induct n arbitrary: w cs) auto
-
-lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
- by (simp add: bin_to_bl_def bl_not_aux_bin)
-
-lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
- by (simp add: bin_to_bl_def bl_and_aux_bin)
-
-lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
- by (simp add: bin_to_bl_def bl_or_aux_bin)
-
-lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
- by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
-
lemma drop_bin2bl_aux:
"drop m (bin_to_bl_aux n bin bs) =
bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
@@ -1042,36 +993,4 @@
apply (rule refl)
done
-
-text \<open>Even more bit operations\<close>
-
-instantiation int :: bitss
-begin
-
-definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
-
-definition "lsb i = i !! 0" for i :: int
-
-definition "set_bit i n b = bin_sc n b i"
-
-definition
- "set_bits f =
- (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
- let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
- in bl_to_bin (rev (map f [0..<n]))
- else if \<exists>n. \<forall>n'\<ge>n. f n' then
- let n = LEAST n. \<forall>n'\<ge>n. f n'
- in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
- else 0 :: int)"
-
-definition "shiftl x n = x * 2 ^ n" for x :: int
-
-definition "shiftr x n = x div 2 ^ n" for x :: int
-
-definition "msb x \<longleftrightarrow> x < 0" for x :: int
-
-instance ..
-
end
-
-end
--- a/src/HOL/Word/Word.thy Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Word.thy Tue Apr 16 19:50:03 2019 +0000
@@ -9,7 +9,7 @@
"HOL-Library.Type_Length"
"HOL-Library.Boolean_Algebra"
Bits_Bit
- Bool_List_Representation
+ Bits_Int
Misc_Typedef
Word_Miscellaneous
begin
--- a/src/HOL/Word/Word_Miscellaneous.thy Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Tue Apr 16 19:50:03 2019 +0000
@@ -6,6 +6,9 @@
imports "HOL-Library.Bit" Misc_Numeric
begin
+lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
+ by auto
+
lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
by (auto dest: gr0_implies_Suc)