(* 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))" using 2 apply(simp add: witness_length) 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 subsection "Average out the second sum for free-absch" 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)" by(simp add: 3) 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)))" by (simp add: Groups_Big.comm_monoid_add_class.sum.distrib) 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