examples/diningcryptos/dining_cryptosScript.sml

70    `(set_announcements (high: bool state) (low:bool state)
77                         low s) /\
78     (set_announcements high low random n (SUC i) s =
84                         (set_announcements high low random n i) s)`;
87   `(XOR_announces (low:bool state) (0:num) = low (STRCAT "announces" (toString 0))) /\
88    (XOR_announces low (SUC i) = (low (STRCAT "announces" (toString (SUC i)))) xor
89                                 (XOR_announces low i))`;
92    `compute_result (low:bool state) (n:num) (s:string) =
93         if (s = "result") then XOR_announces low n else low s`;
96    `dcprog (SUC(SUC(SUC n))) = (\((high:bool state, low:bool state), random:bool state).
97         compute_result (set_announcements high low random (SUC(SUC n)) (SUC(SUC n)))
140    ``!high low random n i.
141         (set_announcements high low random n 0 =
146                         low s)) /\
147         (set_announcements high low random n (SUC i) =
152                         (set_announcements high low random n i) s))``,
156    ``!low n. compute_result low n = (\s. if (s = "result") then XOR_announces low n else low s)``,
503    ``!high low random n i. i <= SUC (SUC n) /\ (high (STRCAT "pays" (toString i))) /\ (!j. (~(j = i)) ==> ~(high (STRCAT "pays" (toString j)))) ==>
505                 (XOR_announces (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) k =
518    ``!high low random n i. i <= SUC (SUC n) /\ (high (STRCAT "pays" (toString i))) /\ (!j. (~(j = i)) ==> ~(high (STRCAT "pays" (toString j)))) ==>
519         (XOR_announces (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) i =
526        o Q.SPECL [`high`, `low`, `random`, `n`, `(SUC n')`]) dc_XOR_announces_result1
532    ``!high low random n i. i <= SUC (SUC n) /\ (high (STRCAT "pays" (toString i))) /\ (!j. (~(j = i)) ==> ~(high (STRCAT "pays" (toString j)))) ==>
534                 (XOR_announces (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) k =
540    >- ((ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o Q.SPECL [`high`, `low`, `random`, `n`, `i`]) dc_XOR_announces_result2
554    ``!high low random n i. i <= SUC (SUC n) /\ (high (STRCAT "pays" (toString i))) /\ (!j. (~(j = i)) ==> ~(high (STRCAT "pays" (toString j)))) ==>
555                 (XOR_announces (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) (SUC (SUC n)))``,
559                       o Q.SPECL [`high`, `low`, `random`, `n`, `i`]) dc_XOR_announces_result3, xor_refl]);
563    ``!high low random n. high IN dc_high_states F (SUC (SUC (SUC n)))  ==>
564                 (XOR_announces (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) (SUC (SUC n)))``,
576    ``!high low random n. dcprog (SUC (SUC (SUC n))) ((high, low), random) "result" =
577                          XOR_announces (set_announcements high low random
583    ``!high low random n x. (~(x = "result")) ==>
584         (dcprog (SUC (SUC (SUC n))) ((high, low), random) x =
585          (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) x)``,
590    ``!high low random n i. XOR_announces (dcprog (SUC (SUC (SUC n))) ((high, low), random)) i =
591                          XOR_announces (set_announcements high low random
600    ``!high low random n. XOR_announces (dcprog (SUC (SUC (SUC n))) ((high, low), random)) (SUC (SUC n)) =
601                          (dcprog (SUC (SUC (SUC n))) ((high, low), random)) "result"``,
607    ``!high low random n. high IN dc_high_states F (SUC (SUC (SUC n))) ==>
608         ((dcprog (SUC (SUC (SUC n))) ((high, low), random)) "result")``,
613    ``!high low random n i.
614         (dcprog (SUC (SUC (SUC n))) ((high, low), random) (STRCAT "announces" (toString i)) =
615          (set_announcements high low random (SUC (SUC n)) (SUC (SUC n))) (STRCAT "announces" (toString i)))``,
1758 val insider_set_announcements_def = Define   `(insider_set_announcements (high: bool state) (low:bool state) (random:bool state) (n:num) (0:num) (s:string) =           if (s = (STRCAT "announces" (toString 0))) then                 ((high (STRCAT "pays" (toString 0)))) xor                       ((low (STRCAT "coin" (toString 0))) xor (random (STRCAT "coin" (toString n))))          else                    low s) /\
1759     (insider_set_announcements (high: bool state) (low:bool state) (random:bool state) (n:num) (SUC(0:num)) (s:string) =                if (s = (STRCAT "announces" (toString (SUC 0)))) then                   ((high (STRCAT "pays" (toString (SUC 0))))) xor                 ((random (STRCAT "coin" (toString (SUC 0)))) xor (low (STRCAT "coin" (toString 0))))            else                    (insider_set_announcements high low random n 0) s) /\    (insider_set_announcements high low random n (SUC (SUC i)) s =         if (s = (STRCAT "announces" (toString (SUC (SUC i))))) then                     ((high (STRCAT "pays" (toString (SUC (SUC i)))))) xor                   ((random (STRCAT "coin" (toString (SUC (SUC i))))) xor (random (STRCAT "coin" (toString (SUC i)))))             else                    (insider_set_announcements high low random n (SUC i)) s)`;
1761 val insider_set_announcements_alt = store_thm  ("insider_set_announcements_alt",   ``!high low random n i.      (insider_set_announcements high low random n 0 =         (\s. if (s = (STRCAT "announces" (toString 0))) then                   ((high (STRCAT "pays" (toString 0)))) xor                       ((low (STRCAT "coin" (toString 0))) xor (random (STRCAT "coin" (toString n))))          else                    low s)) /\
1762         (insider_set_announcements high low random n (SUC 0) =   (\s. if (s = (STRCAT "announces" (toString (SUC 0)))) then                     ((high (STRCAT "pays" (toString (SUC 0))))) xor                 ((random (STRCAT "coin" (toString (SUC 0)))) xor (low (STRCAT "coin" (toString 0))))            else                    (insider_set_announcements high low random n 0) s)) /\  (insider_set_announcements high low random n (SUC(SUC i)) =      (\s. if (s = (STRCAT "announces" (toString (SUC(SUC i))))) then                        ((high (STRCAT "pays" (toString (SUC(SUC i)))))) xor                    ((random (STRCAT "coin" (toString (SUC(SUC i))))) xor (random (STRCAT "coin" (toString (SUC i)))))              else                    (insider_set_announcements high low random n (SUC i)) s))``,
1764 val insider_dcprog_def = Define   `insider_dcprog (SUC(SUC(SUC n))) = (\((high:bool state, low:bool state), random:bool state). compute_result (insider_set_announcements high low random (SUC(SUC n)) (SUC(SUC n)))                   (SUC(SUC n)))`;
1852    `biased_dist high low random =
1854                 (1 / 2) * (unif_prog_dist high low random s)
1856                 (3 / 2) * (unif_prog_dist high low random s))`;
3341    `biased_dist2 high low random =
3343                 (1 / 2) * (unif_prog_dist high low random s)
3345                 (3 / 2) * (unif_prog_dist high low random s))`;