* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.
* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
(*
ID: $Id$
Author: Jeremy Dawson and Gerwin Klein, NICTA
definition and basic theorems for bit-wise logical operations
for integers expressed using Pls, Min, BIT,
and converting them to and from lists of bools
*)
theory BinOperations imports BinGeneral
begin
-- "bit-wise logical operations on the int type"
consts
int_and :: "int => int => int"
int_or :: "int => int => int"
bit_not :: "bit => bit"
bit_and :: "bit => bit => bit"
bit_or :: "bit => bit => bit"
bit_xor :: "bit => bit => bit"
int_not :: "int => int"
int_xor :: "int => int => int"
bin_sc :: "nat => bit => int => int"
primrec
B0 : "bit_not bit.B0 = bit.B1"
B1 : "bit_not bit.B1 = bit.B0"
primrec
B1 : "bit_xor bit.B1 x = bit_not x"
B0 : "bit_xor bit.B0 x = x"
primrec
B1 : "bit_or bit.B1 x = bit.B1"
B0 : "bit_or bit.B0 x = x"
primrec
B0 : "bit_and bit.B0 x = bit.B0"
B1 : "bit_and bit.B1 x = x"
primrec
Z : "bin_sc 0 b w = bin_rest w BIT b"
Suc :
"bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
defs
int_not_def : "int_not == bin_rec Numeral.Min Numeral.Pls
(%w b s. s BIT bit_not b)"
int_and_def : "int_and == bin_rec (%x. Numeral.Pls) (%y. y)
(%w b s y. s (bin_rest y) BIT (bit_and b (bin_last y)))"
int_or_def : "int_or == bin_rec (%x. x) (%y. Numeral.Min)
(%w b s y. s (bin_rest y) BIT (bit_or b (bin_last y)))"
int_xor_def : "int_xor == bin_rec (%x. x) int_not
(%w b s y. s (bin_rest y) BIT (bit_xor b (bin_last y)))"
consts
bin_to_bl :: "nat => int => bool list"
bin_to_bl_aux :: "nat => int => bool list => bool list"
bl_to_bin :: "bool list => int"
bl_to_bin_aux :: "int => bool list => int"
bl_of_nth :: "nat => (nat => bool) => bool list"
primrec
Nil : "bl_to_bin_aux w [] = w"
Cons : "bl_to_bin_aux w (b # bs) =
bl_to_bin_aux (w BIT (if b then bit.B1 else bit.B0)) bs"
primrec
Z : "bin_to_bl_aux 0 w bl = bl"
Suc : "bin_to_bl_aux (Suc n) w bl =
bin_to_bl_aux n (bin_rest w) ((bin_last w = bit.B1) # bl)"
defs
bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Numeral.Pls bs"
primrec
Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
Z : "bl_of_nth 0 f = []"
consts
takefill :: "'a => nat => 'a list => 'a list"
app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
-- "takefill - like take but if argument list too short,"
-- "extends result to get requested length"
primrec
Z : "takefill fill 0 xs = []"
Suc : "takefill fill (Suc n) xs = (
case xs of [] => fill # takefill fill n xs
| y # ys => y # takefill fill n ys)"
defs
app2_def : "app2 f as bs == map (split f) (zip as bs)"
-- "rcat and rsplit"
consts
bin_rcat :: "nat => int list => int"
bin_rsplit_aux :: "nat * int list * nat * int => int list"
bin_rsplit :: "nat => (nat * int) => int list"
bin_rsplitl_aux :: "nat * int list * nat * int => int list"
bin_rsplitl :: "nat => (nat * int) => int list"
recdef bin_rsplit_aux "measure (fst o snd o snd)"
"bin_rsplit_aux (n, bs, (m, c)) =
(if m = 0 | n = 0 then bs else
let (a, b) = bin_split n c
in bin_rsplit_aux (n, b # bs, (m - n, a)))"
recdef bin_rsplitl_aux "measure (fst o snd o snd)"
"bin_rsplitl_aux (n, bs, (m, c)) =
(if m = 0 | n = 0 then bs else
let (a, b) = bin_split (min m n) c
in bin_rsplitl_aux (n, b # bs, (m - n, a)))"
defs
bin_rcat_def : "bin_rcat n bs == foldl (%u v. bin_cat u n v) Numeral.Pls bs"
bin_rsplit_def : "bin_rsplit n w == bin_rsplit_aux (n, [], w)"
bin_rsplitl_def : "bin_rsplitl n w == bin_rsplitl_aux (n, [], w)"
lemma int_not_simps [simp]:
"int_not Numeral.Pls = Numeral.Min"
"int_not Numeral.Min = Numeral.Pls"
"int_not (w BIT b) = int_not w BIT bit_not b"
by (unfold int_not_def) (auto intro: bin_rec_simps)
lemma bit_extra_simps [simp]:
"bit_and x bit.B0 = bit.B0"
"bit_and x bit.B1 = x"
"bit_or x bit.B1 = bit.B1"
"bit_or x bit.B0 = x"
"bit_xor x bit.B1 = bit_not x"
"bit_xor x bit.B0 = x"
by (cases x, auto)+
lemma bit_ops_comm:
"bit_and x y = bit_and y x"
"bit_or x y = bit_or y x"
"bit_xor x y = bit_xor y x"
by (cases y, auto)+
lemma bit_ops_same [simp]:
"bit_and x x = x"
"bit_or x x = x"
"bit_xor x x = bit.B0"
by (cases x, auto)+
lemma bit_not_not [simp]: "bit_not (bit_not x) = x"
by (cases x) auto
lemma int_xor_Pls [simp]:
"int_xor Numeral.Pls x = x"
unfolding int_xor_def by (simp add: bin_rec_PM)
lemma int_xor_Min [simp]:
"int_xor Numeral.Min x = int_not x"
unfolding int_xor_def by (simp add: bin_rec_PM)
lemma int_xor_Bits [simp]:
"int_xor (x BIT b) (y BIT c) = int_xor x y BIT bit_xor b c"
apply (unfold int_xor_def)
apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
apply (rule ext, simp)
prefer 2
apply simp
apply (rule ext)
apply (simp add: int_not_simps [symmetric])
done
lemma int_xor_x_simps':
"int_xor w (Numeral.Pls BIT bit.B0) = w"
"int_xor w (Numeral.Min BIT bit.B1) = int_not w"
apply (induct w rule: bin_induct)
apply simp_all[4]
apply (unfold int_xor_Bits)
apply clarsimp+
done
lemmas int_xor_extra_simps [simp] = int_xor_x_simps' [simplified arith_simps]
lemma int_or_Pls [simp]:
"int_or Numeral.Pls x = x"
by (unfold int_or_def) (simp add: bin_rec_PM)
lemma int_or_Min [simp]:
"int_or Numeral.Min x = Numeral.Min"
by (unfold int_or_def) (simp add: bin_rec_PM)
lemma int_or_Bits [simp]:
"int_or (x BIT b) (y BIT c) = int_or x y BIT bit_or b c"
unfolding int_or_def by (simp add: bin_rec_simps)
lemma int_or_x_simps':
"int_or w (Numeral.Pls BIT bit.B0) = w"
"int_or w (Numeral.Min BIT bit.B1) = Numeral.Min"
apply (induct w rule: bin_induct)
apply simp_all[4]
apply (unfold int_or_Bits)
apply clarsimp+
done
lemmas int_or_extra_simps [simp] = int_or_x_simps' [simplified arith_simps]
lemma int_and_Pls [simp]:
"int_and Numeral.Pls x = Numeral.Pls"
unfolding int_and_def by (simp add: bin_rec_PM)
lemma int_and_Min [simp]:
"int_and Numeral.Min x = x"
unfolding int_and_def by (simp add: bin_rec_PM)
lemma int_and_Bits [simp]:
"int_and (x BIT b) (y BIT c) = int_and x y BIT bit_and b c"
unfolding int_and_def by (simp add: bin_rec_simps)
lemma int_and_x_simps':
"int_and w (Numeral.Pls BIT bit.B0) = Numeral.Pls"
"int_and w (Numeral.Min BIT bit.B1) = w"
apply (induct w rule: bin_induct)
apply simp_all[4]
apply (unfold int_and_Bits)
apply clarsimp+
done
lemmas int_and_extra_simps [simp] = int_and_x_simps' [simplified arith_simps]
(* commutativity of the above *)
lemma bin_ops_comm:
shows
int_and_comm: "!!y. int_and x y = int_and y x" and
int_or_comm: "!!y. int_or x y = int_or y x" and
int_xor_comm: "!!y. int_xor x y = int_xor y x"
apply (induct x rule: bin_induct)
apply simp_all[6]
apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
done
lemma bin_ops_same [simp]:
"int_and x x = x"
"int_or x x = x"
"int_xor x x = Numeral.Pls"
by (induct x rule: bin_induct) auto
lemma int_not_not [simp]: "int_not (int_not x) = x"
by (induct x rule: bin_induct) auto
lemmas bin_log_esimps =
int_and_extra_simps int_or_extra_simps int_xor_extra_simps
int_and_Pls int_and_Min int_or_Pls int_or_Min int_xor_Pls int_xor_Min
(* potential for looping *)
declare bin_rsplit_aux.simps [simp del]
declare bin_rsplitl_aux.simps [simp del]
lemma bin_sign_cat:
"!!y. bin_sign (bin_cat x n y) = bin_sign x"
by (induct n) 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:
"!!n y. 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)
apply clarsimp
apply (case_tac n, auto)
done
lemma bin_nth_split:
"!!b c. bin_split n c = (a, b) ==>
(ALL k. bin_nth a k = bin_nth c (n + k)) &
(ALL k. bin_nth b k = (k < n & bin_nth c k))"
apply (induct n)
apply clarsimp
apply (clarsimp simp: Let_def split: ls_splits)
apply (case_tac k)
apply auto
done
lemma bin_cat_assoc:
"!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
by (induct n) auto
lemma bin_cat_assoc_sym: "!!z m.
bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
apply (induct n, clarsimp)
apply (case_tac m, auto)
done
lemma bin_cat_Pls [simp]:
"!!w. bin_cat Numeral.Pls n w = bintrunc n w"
by (induct n) auto
lemma bintr_cat1:
"!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
by (induct n) 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]:
"!!b. bin_cat a n (bintrunc n b) = bin_cat a n b"
by (induct n) auto
lemma split_bintrunc:
"!!b c. bin_split n c = (a, b) ==> b = bintrunc n c"
by (induct n) (auto simp: Let_def split: ls_splits)
lemma bin_cat_split:
"!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v"
by (induct n) (auto simp: Let_def split: ls_splits)
lemma bin_split_cat:
"!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
by (induct n) auto
lemma bin_split_Pls [simp]:
"bin_split n Numeral.Pls = (Numeral.Pls, Numeral.Pls)"
by (induct n) (auto simp: Let_def split: ls_splits)
lemma bin_split_Min [simp]:
"bin_split n Numeral.Min = (Numeral.Min, bintrunc n Numeral.Min)"
by (induct n) (auto simp: Let_def split: ls_splits)
lemma bin_split_trunc:
"!!m b c. bin_split (min m n) c = (a, b) ==>
bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
apply (induct n, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: ls_splits)
apply (case_tac m)
apply (auto simp: Let_def split: ls_splits)
done
lemma bin_split_trunc1:
"!!m b c. bin_split n c = (a, b) ==>
bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
apply (induct n, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: ls_splits)
apply (case_tac m)
apply (auto simp: Let_def split: ls_splits)
done
lemma bin_cat_num:
"!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
apply (induct n, clarsimp)
apply (simp add: Bit_def cong: number_of_False_cong)
done
lemma bin_split_num:
"!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
apply (induct n, clarsimp)
apply (simp add: bin_rest_div zdiv_zmult2_eq)
apply (case_tac b rule: bin_exhaust)
apply simp
apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
split: bit.split
cong: number_of_False_cong)
done
(* basic properties of logical (bit-wise) operations *)
lemma bbw_ao_absorb:
"!!y. int_and x (int_or y x) = x & int_or x (int_and y x) = x"
apply (induct x rule: bin_induct)
apply auto
apply (case_tac [!] y rule: bin_exhaust)
apply auto
apply (case_tac [!] bit)
apply auto
done
lemma bbw_ao_absorbs_other:
"int_and x (int_or x y) = x \<and> int_or (int_and y x) x = x"
"int_and (int_or y x) x = x \<and> int_or x (int_and x y) = x"
"int_and (int_or x y) x = x \<and> int_or (int_and x y) x = x"
apply (auto simp: bbw_ao_absorb int_or_comm)
apply (subst int_or_comm)
apply (simp add: bbw_ao_absorb)
apply (subst int_and_comm)
apply (subst int_or_comm)
apply (simp add: bbw_ao_absorb)
apply (subst int_and_comm)
apply (simp add: bbw_ao_absorb)
done
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
lemma int_xor_not:
"!!y. int_xor (int_not x) y = int_not (int_xor x y) &
int_xor x (int_not y) = int_not (int_xor x y)"
apply (induct x rule: bin_induct)
apply auto
apply (case_tac y rule: bin_exhaust, auto,
case_tac b, auto)+
done
lemma bbw_assocs':
"!!y z. int_and (int_and x y) z = int_and x (int_and y z) &
int_or (int_or x y) z = int_or x (int_or y z) &
int_xor (int_xor x y) z = int_xor x (int_xor y z)"
apply (induct x rule: bin_induct)
apply (auto simp: int_xor_not)
apply (case_tac [!] y rule: bin_exhaust)
apply (case_tac [!] z rule: bin_exhaust)
apply (case_tac [!] bit)
apply (case_tac [!] b)
apply auto
done
lemma int_and_assoc:
"int_and (int_and x y) z = int_and x (int_and y z)"
by (simp add: bbw_assocs')
lemma int_or_assoc:
"int_or (int_or x y) z = int_or x (int_or y z)"
by (simp add: bbw_assocs')
lemma int_xor_assoc:
"int_xor (int_xor x y) z = int_xor x (int_xor y z)"
by (simp add: bbw_assocs')
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
lemma bbw_lcs [simp]:
"int_and y (int_and x z) = int_and x (int_and y z)"
"int_or y (int_or x z) = int_or x (int_or y z)"
"int_xor y (int_xor x z) = int_xor x (int_xor y z)"
apply (auto simp: bbw_assocs [symmetric])
apply (auto simp: bin_ops_comm)
done
lemma bbw_not_dist:
"!!y. int_not (int_or x y) = int_and (int_not x) (int_not y)"
"!!y. int_not (int_and x y) = int_or (int_not x) (int_not y)"
apply (induct x rule: bin_induct)
apply auto
apply (case_tac [!] y rule: bin_exhaust)
apply (case_tac [!] bit, auto)
done
lemma bbw_oa_dist:
"!!y z. int_or (int_and x y) z =
int_and (int_or x z) (int_or y z)"
apply (induct x rule: bin_induct)
apply auto
apply (case_tac y rule: bin_exhaust)
apply (case_tac z rule: bin_exhaust)
apply (case_tac ba, auto)
done
lemma bbw_ao_dist:
"!!y z. int_and (int_or x y) z =
int_or (int_and x z) (int_and y z)"
apply (induct x rule: bin_induct)
apply auto
apply (case_tac y rule: bin_exhaust)
apply (case_tac z rule: bin_exhaust)
apply (case_tac ba, auto)
done
declare bin_ops_comm [simp] bbw_assocs [simp]
lemma plus_and_or [rule_format]:
"ALL y. int_and x y + int_or x y = x + y"
apply (induct x rule: bin_induct)
apply clarsimp
apply clarsimp
apply clarsimp
apply (case_tac y rule: bin_exhaust)
apply clarsimp
apply (unfold Bit_def)
apply clarsimp
apply (erule_tac x = "x" in allE)
apply (simp split: bit.split)
done
lemma le_int_or:
"!!x. bin_sign y = Numeral.Pls ==> x <= int_or x y"
apply (induct y rule: bin_induct)
apply clarsimp
apply clarsimp
apply (case_tac x rule: bin_exhaust)
apply (case_tac b)
apply (case_tac [!] bit)
apply (auto simp: less_eq_numeral_code)
done
lemmas int_and_le =
xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ;
(** nth bit, set/clear **)
lemma bin_nth_sc [simp]:
"!!w. bin_nth (bin_sc n b w) n = (b = bit.B1)"
by (induct n) auto
lemma bin_sc_sc_same [simp]:
"!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w"
by (induct n) auto
lemma bin_sc_sc_diff:
"!!w m. m ~= n ==>
bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
apply (induct n)
apply safe
apply (case_tac [!] m)
apply auto
done
lemma bin_nth_sc_gen:
"!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = bit.B1 else bin_nth w m)"
by (induct n) (case_tac [!] m, auto)
lemma bin_sc_nth [simp]:
"!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w"
by (induct n) auto
lemma bin_sign_sc [simp]:
"!!w. bin_sign (bin_sc n b w) = bin_sign w"
by (induct n) auto
lemma bin_sc_bintr [simp]:
"!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
apply (induct n)
apply (case_tac [!] w rule: bin_exhaust)
apply (case_tac [!] m, auto)
done
lemma bin_clr_le:
"!!w. bin_sc n bit.B0 w <= w"
apply (induct n)
apply (case_tac [!] w rule: bin_exhaust)
apply auto
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
lemma bin_set_ge:
"!!w. bin_sc n bit.B1 w >= w"
apply (induct n)
apply (case_tac [!] w rule: bin_exhaust)
apply auto
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
lemma bintr_bin_clr_le:
"!!w m. bintrunc n (bin_sc m bit.B0 w) <= bintrunc n w"
apply (induct n)
apply simp
apply (case_tac w rule: bin_exhaust)
apply (case_tac m)
apply auto
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
lemma bintr_bin_set_ge:
"!!w m. bintrunc n (bin_sc m bit.B1 w) >= bintrunc n w"
apply (induct n)
apply simp
apply (case_tac w rule: bin_exhaust)
apply (case_tac m)
apply auto
apply (unfold Bit_def)
apply (simp_all split: bit.split)
done
lemma bin_nth_ops:
"!!x y. bin_nth (int_and x y) n = (bin_nth x n & bin_nth y n)"
"!!x y. bin_nth (int_or x y) n = (bin_nth x n | bin_nth y n)"
"!!x y. bin_nth (int_xor x y) n = (bin_nth x n ~= bin_nth y n)"
"!!x. bin_nth (int_not x) n = (~ bin_nth x n)"
apply (induct n)
apply safe
apply (case_tac [!] x rule: bin_exhaust)
apply simp_all
apply (case_tac [!] y rule: bin_exhaust)
apply simp_all
apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
done
lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Numeral.Pls = Numeral.Pls"
by (induct n) auto
lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Numeral.Min = Numeral.Min"
by (induct n) auto
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
lemma bin_sc_minus:
"0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
by auto
lemmas bin_sc_Suc_minus =
trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard]
lemmas bin_sc_Suc_pred [simp] =
bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
(* interaction between bit-wise and arithmetic *)
(* good example of bin_induction *)
lemma bin_add_not: "x + int_not x = Numeral.Min"
apply (induct x rule: bin_induct)
apply clarsimp
apply clarsimp
apply (case_tac bit, auto)
done
(* truncating results of bit-wise operations *)
lemma bin_trunc_ao:
"!!x y. int_and (bintrunc n x) (bintrunc n y) = bintrunc n (int_and x y)"
"!!x y. int_or (bintrunc n x) (bintrunc n y) = bintrunc n (int_or x y)"
apply (induct n)
apply auto
apply (case_tac [!] x rule: bin_exhaust)
apply (case_tac [!] y rule: bin_exhaust)
apply auto
done
lemma bin_trunc_xor:
"!!x y. bintrunc n (int_xor (bintrunc n x) (bintrunc n y)) =
bintrunc n (int_xor x y)"
apply (induct n)
apply auto
apply (case_tac [!] x rule: bin_exhaust)
apply (case_tac [!] y rule: bin_exhaust)
apply auto
done
lemma bin_trunc_not:
"!!x. bintrunc n (int_not (bintrunc n x)) = bintrunc n (int_not x)"
apply (induct n)
apply auto
apply (case_tac [!] x rule: bin_exhaust)
apply auto
done
(* want theorems of the form of bin_trunc_xor *)
lemma bintr_bintr_i:
"x = bintrunc n y ==> bintrunc n x = bintrunc n y"
by auto
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 nth_2p_bin:
"!!m. bin_nth (2 ^ n) m = (m = n)"
apply (induct n)
apply clarsimp
apply safe
apply (case_tac m)
apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
apply (case_tac m)
apply (auto simp: Bit_B0_2t [symmetric])
done
(* for use when simplifying with bin_nth_Bit *)
lemma ex_eq_or:
"(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
by auto
end