equal
deleted
inserted
replaced
57 |
57 |
58 theorem correctness: |
58 theorem correctness: |
59 assumes "dc \<in> dining_cryptographers" |
59 assumes "dc \<in> dining_cryptographers" |
60 shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)" |
60 shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)" |
61 proof - |
61 proof - |
62 let ?XOR = "\<lambda>f l. foldl (op \<noteq>) False (map f [0..<l])" |
62 let ?XOR = "\<lambda>f l. foldl (\<noteq>) False (map f [0..<l])" |
63 |
63 |
64 have foldl_coin: |
64 have foldl_coin: |
65 "\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n" |
65 "\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n" |
66 proof - |
66 proof - |
67 define n' where "n' = n" \<comment> "Need to hide n, as it is hidden in coin" |
67 define n' where "n' = n" \<comment> "Need to hide n, as it is hidden in coin" |