# Theory Bit_Strings

theory Bit_Strings
imports Complex_Main
```(*  Title:       Lemmas about lists of bools
Author:      Max Haslbeck
*)
theory Bit_Strings
imports Complex_Main
begin

section "Lemmas about BitStrings and sets theirof"

subsection "the set of bitstring of length m is finite"

lemma bitstrings_finite: "finite {xs::bool list. length xs = m}"
using finite_lists_length_eq[where A="UNIV"] by force

subsection "how to calculate the cardinality of the set of bitstrings with certain bits already set"

lemma fbool: "finite {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ f (xs!e)}"
by(rule finite_subset[where B="{xs. length xs = m}"])
(auto simp: bitstrings_finite)

fun witness :: "nat set ⇒ nat ⇒ bool list" where
"witness X 0 = []"
|"witness X (Suc n) = (witness X n) @ [n ∈ X]"

lemma witness_length: "length (witness X n) = n"
apply(induct n) by auto

lemma iswitness: "r<n ⟹ ((witness X n)!r) = (r∈X)"
proof (induct n)
case (Suc n)

have "witness X (Suc n) ! r = ((witness X n) @ [n ∈ X]) ! r" by simp
also have "… = (if r < length (witness X n) then (witness X n) ! r else [n ∈ X] ! (r - length (witness X n)))" by(rule nth_append)
also have "… = (if r < n then (witness X n) ! r else [n ∈ X] ! (r - n))" by (simp add: witness_length)
finally have 1: "witness X (Suc n) ! r = (if r < n then (witness X n) ! r else [n ∈ X] ! (r - n))" .

show ?case
proof (cases "r < n")
case True
with 1 have a: "witness X (Suc n) ! r = (witness X n) ! r" by auto
from Suc True have b: "witness X n ! r = (r ∈ X)" by auto
from a b show ?thesis by auto
next
case False
with Suc have "r = n" by auto
with 1 show "witness X (Suc n) ! r = (r ∈ X)" by auto
qed
qed simp

lemma card1: "finite S ⟹ finite X ⟹ finite Y ⟹ X ∩ Y = {} ⟹ S ∩ (X ∪ Y) = {} ⟹ S∪X∪Y={0..<m} ⟹
card {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i)  ∧ length xs = m} = 2^(m - card X - card Y)"
proof(induct arbitrary: X Y rule: finite_induct)
case empty
then have x: "X ⊆ {0..<m}" and y: "Y ⊆ {0..<m}" and xy: "X∪ Y = {0..<m}" by auto
then have "card (X ∪ Y) = m" by auto
with empty(3) have cardXY: "card X + card Y = m" using card_Un_Int[OF empty(1) empty(2)] by auto

from empty have ents: "∀i<m. (i∈Y) = (i∉X)" by auto

have "(∃! w. (∀i∈X. w ! i) ∧ (∀i∈Y. ¬ w ! i) ∧  length w = m)"
proof (rule ex1I, goal_cases)
case 1
show "(∀i∈X. (witness X m) ! i) ∧ (∀i∈Y. ¬ (witness X m) ! i) ∧ length (witness X m) = m"
proof (safe, goal_cases)
case (2 i)
with y have a: "i < m" by auto
with iswitness have "witness X m ! i = (i ∈ X)" by auto
with a ents 2 have "~ witness X m ! i" by auto
with 2(2) show "False" by auto
next
case (1 i)
with x have a: "i < m" by auto
with iswitness have "witness X m ! i = (i ∈ X)" by auto
with a ents 1 show "witness X m ! i" by auto
qed (rule witness_length)
next
case (2 w)
show "w = witness X m"
proof -
have "(length w = length (witness X m) ∧ (∀i<length w. w ! i = (witness X m) ! i))"
proof
fix i
assume as: "(∀i∈X. w ! i) ∧ (∀i∈Y. ¬ w ! i) ∧  length w = m"
have "i < m ⟶ (witness X m) ! i = (i ∈ X)" using iswitness by auto
then show "i < m ⟶ w ! i = (witness X m) ! i" using ents as by auto
qed
then show ?thesis using list_eq_iff_nth_eq by auto
qed
qed
then obtain w where " {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i)  ∧ length xs = m}
= { w }" using Nitpick.Ex1_unfold[where P="(λxs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i)  ∧ length xs = m)"]
by auto

then have "card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i)  ∧ length xs = m} = card { w }" by auto
also have "… = 1" by auto
also have "… = 2^(m - card X - card Y)" using cardXY by auto
finally show ?case .
next
case (insert e S)
then have eX: "e ∉ X" and eY: "e ∉ Y"  by auto
from insert(8) have "insert e S ⊆ {0..<m}" by auto
then have ebetween0m: "e∈{0..<m}" by auto

have fm: "finite {0..<m}" by auto
have cardm: "card {0..<m} =   m" by auto
from insert(8) eX eY ebetween0m have sub: "X ∪ Y ⊂ {0..<m}" by auto
from insert have "card (X ∩ Y) = 0" by auto
then have cardXY: "card (X ∪ Y) = card X + card Y" using card_Un_Int[OF insert(4) insert(5)] by auto

have "  m > card X + card Y" using psubset_card_mono[OF fm sub] cardm cardXY by(auto)
then have carde: "1 + (  m - card X - card Y - 1) =   m - card X - card Y" by auto

have is1: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m ∧ xs!e}
= {xs. Ball (insert e X) ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m}" by auto
have is2: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m ∧ ~xs!e}
= {xs. Ball X ((!) xs) ∧ (∀i∈(insert e Y). ¬ xs ! i) ∧ length xs =   m}" by auto

have 2: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m ∧ xs!e}
∪ {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m ∧ ~xs!e}
= {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m}" by auto

have 3: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m ∧ xs!e}
∩ {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m ∧ ~xs!e} = {}" by auto

have fX: "finite (insert e X)"
and disjeXY: "insert e X ∩ Y = {}"
and cutX: "S ∩ (insert e X ∪ Y) = {}"
and uniX: "S ∪ insert e X ∪ Y = {0..<m}" using insert by auto
have fY: "finite (insert e Y)"
and disjXeY: "X ∩ (insert e Y) = {}"
and cutY: "S ∩ (X ∪ insert e Y) = {}"
and uniY: "S ∪  X ∪ insert e Y = {0..<m}" using insert by auto

have "card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m}
= card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ xs!e}
+ card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ ~xs!e}"
apply(subst card_Un_Int)
apply(rule fbool) apply(rule fbool) using 2 3 by auto
also
have "… = card {xs. Ball (insert e X) ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs =   m}
+ card {xs. Ball X ((!) xs) ∧ (∀i∈(insert e Y). ¬ xs ! i) ∧ length xs =   m}" by (simp only: is1 is2)

also
have "… = 2 ^ (  m - card (insert e X) - card Y)
+ 2 ^ (  m - card X - card (insert e Y))"
apply(simp only: insert(3)[of "insert e X" Y, OF fX insert(5) disjeXY cutX uniX])
by(simp only: insert(3)[of "X" "insert e Y", OF insert(4) fY disjXeY cutY uniY])
also
have "… = 2 ^ (  m - card X - card Y - 1)
+ 2 ^ (  m - card X - card Y - 1)" using insert(4,5) eX eY by auto
also
have "… = 2 * 2 ^ (  m - card X - card Y - 1)"  by auto
also have "… = 2 ^ (1 + (  m - card X - card Y - 1))" by auto
also have "… = 2 ^ (  m - card X - card Y)" using carde by auto
finally show ?case .
qed

lemma card2: assumes "finite X" and "finite Y" and "X ∩ Y = {}" and x: "X ∪ Y ⊆ {0..<m}"
shows "card {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} = 2 ^ (m - card X - card Y)"
proof -
let ?S = "{0..<m}-(X ∪ Y)"
from x have a: "?S ∪ X ∪ Y = {0..<m}" by auto
have b: "?S ∩ (X ∪ Y) = {}" by auto
show ?thesis apply(rule card1[where ?S="?S"]) by(simp_all add: assms a b)
qed

lemma Expactation2or1: "finite S ⟹ finite Tr ⟹ finite Fa ⟹ card Tr + card Fa + card S ≤ l ⟹
S ∩ (Tr ∪ Fa) = {} ⟹ Tr ∩ Fa = {} ⟹ S ∪ Tr ∪ Fa ⊆ {0..<l} ⟹
(∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}. ∑j∈S. if x ! j then 2 else 1)
= 3 / 2 * real (card S) * 2 ^ (l - card Tr - card Fa)"
proof (induct arbitrary: Tr Fa rule: finite_induct)
case (insert e S)

from insert(7) have "e ∈ (insert e S)" and eTr: "e ∉ Tr" and eFa: "e ∉ Fa" by auto
from insert(9) have  tra: "Tr ⊆ {0..<l}" and trb: "Fa ⊆ {0..<l}" and  trc: "e < l" by auto

have ntrFa: "l > (card Tr + card Fa)" using insert(6) card_insert_if insert(1,2) by auto

have myhelp2: "1 + (l - card Tr - card Fa -1) = l - card Tr - card Fa" using ntrFa by auto

have juhuTr: "{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ xs!e}
= {xs. (∀i∈(insert e Tr). xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}"
by auto
have juhuFa: "{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ ~xs!e}
= {xs. (∀i∈Tr. xs ! i) ∧ (∀i∈(insert e Fa). ¬ xs ! i) ∧ length xs = l}"
by auto

let ?Tre = "{xs. (∀i∈(insert e Tr). xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}"

have "card ?Tre = 2 ^ (l - card (insert e Tr) - card Fa)"
apply(rule card2) using insert by simp_all
then have resi: "card ?Tre = 2^(l - card Tr - card Fa - 1)" using insert(4) eTr by auto
have yabaTr: "(∑x∈?Tre. 2::real) = 2 * 2^(l - card Tr - card Fa - 1)" using resi by (simp add: power_commutes)

let ?Fae = "{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈(insert e Fa). ¬ xs ! i) ∧ length xs = l}"

have "card ?Fae = 2 ^ (l - card Tr - card (insert e Fa))"
apply(rule card2) using insert by simp_all
then have resi2: "card ?Fae = 2^(l - card Tr - card Fa - 1)" using insert(5) eFa by auto
have yabaFa: "(∑x∈?Fae. 1::real) = 1 * 2 ^ (l - card Tr - card Fa - 1)" using resi2 by (simp add: power_commutes)

{ fix X Y
have "{xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = l ∧ xs!e}
∩ {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = l ∧ ~xs!e} = {}" by auto
} note 3=this

(* split it! *)
have "(∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}. ∑j∈(insert e S). if x ! j then (2::real) else 1)
= (∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ xs!e}. ∑j∈(insert e S). if x ! j then 2 else 1)
+ (∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ ~xs!e}. ∑j∈(insert e S). if x ! j then 2 else 1)"
(is "(∑x∈?all. ?f x) = (∑x∈?allT. ?f x) + (∑x∈?allF. ?f x)")
proof -
have "(∑x∈?all. ∑j∈(insert e S). if x ! j then 2 else 1)
= (∑x∈(?allT ∪ ?allF). ∑j∈(insert e S). if x ! j then 2 else 1)" apply(rule sum.cong) by(auto)
also have"… = ((∑x∈(?allT). ∑j∈(insert e S). if x ! j then (2::real) else 1)
+ (∑x∈(?allF). ∑j∈(insert e S). if x ! j then (2::real) else 1))
- (∑x∈(?allT ∩ ?allF). ∑j∈(insert e S). if x ! j then 2 else 1)"
apply (rule sum_Un) apply(rule fbool)+ done
also have "… =  (∑x∈(?allT). ∑j∈(insert e S). if x ! j then 2 else 1)
+ (∑x∈(?allF). ∑j∈(insert e S). if x ! j then 2 else 1)"
finally show ?thesis .
qed
also
have "… = (∑x∈?Tre. ∑j∈(insert e S). if x ! j then 2 else 1)
+ (∑x∈?Fae. ∑j∈(insert e S). if x ! j then 2 else 1)"
using juhuTr juhuFa by auto
also
have "… =  (∑x∈?Tre. (λx. 2) x + (λx. (∑j∈S. if x ! j then 2 else 1)) x)
+ (∑x∈?Fae. (λx. 1) x + (λx. (∑j∈S. if x ! j then 2 else 1)) x)"
using insert(1,2) by auto
also
have "… =  (∑x∈?Tre. 2) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1))
+ ((∑x∈?Fae. 1) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1)))"
also
have "… =  2 * 2^(l - card Tr - card Fa - 1) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1))
+ (1 * 2^(l - card Tr - card Fa - 1) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1)))"
by(simp only: yabaTr yabaFa)
also
have "… =  (2::real) * 2^(l - card Tr - card Fa - 1) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1))
+ (1::real) * 2^(l - card Tr - card Fa - 1) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1))"
by auto
also
have "… =  (3::real) * 2^(l - card Tr - card Fa - 1) +
(∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1)) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1))"
by simp
also
have "… =  3 * 2^(l - card Tr - card Fa - 1) +
3 / 2 * real (card S) * 2 ^ (l - card (insert e Tr) - card Fa) +
(∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1))"
apply(subst insert(3)) using insert by simp_all
also
have "… =  3 * 2^(l - card Tr - card Fa - 1) +
3 / 2 * real (card S) * 2 ^ (l - card (insert e Tr) - card Fa) +
3 / 2 * real (card S) * 2 ^ (l - card Tr - card (insert e Fa))"
apply(subst insert(3)) using insert by simp_all
also
have "… =  3 * 2^(l - card Tr - card Fa - 1) +
3 / 2 * real (card S) * 2^ (l - (card Tr + 1) - card Fa) +
3 / 2 * real (card S) * 2^ (l - card Tr - (card Fa + 1))" using card_insert_if insert(4,5) eTr eFa by auto
also
have "… =  3  * 2^(l - card Tr - card Fa - 1) +
3 / 2 * real (card S) * 2^ (l - card Tr - card Fa - 1) +
3 / 2 * real (card S) * 2^ (l - card Tr - card Fa - 1)" by auto
also
have "… =  ( 3/2 * 2  +  2 *  3 / 2 * real (card S)) * 2^ (l - card Tr - card Fa - 1)" by algebra
also
have "… =  (   3 / 2 * (1 + real (card S))) * 2 * 2^ (l - card Tr - card Fa - 1 )" by simp
also
have "… =  (   3 / 2 * (1 + real (card S))) * 2^ (Suc (l - card Tr - card Fa -1 ))" by simp
also
have "… =  (   3 / 2 * (1 + real (card S))) * 2^ (l - card Tr - card Fa )" using myhelp2 by auto
also
have "… =  (   3 / 2 * (real (1 + card S))) * 2^ (l - card Tr - card Fa )" by simp
also
have "… =  (   3 / 2 * real (card (insert e S))) * 2^ (l - card Tr - card Fa)" using insert(1,2) by auto
finally show ?case  .
qed simp

end
```