author  wenzelm 
Wed, 29 Oct 2014 11:19:27 +0100  
changeset 58813  625d04d4fd2a 
parent 58310  91ea607a34d8 
child 61952  546958347e05 
permissions  rwrr 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

1 
theory Needham_Schroeder_Base 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

2 
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

3 
begin 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

4 

58310  5 
datatype agent = Alice  Bob  Spy 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

6 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

7 
definition agents :: "agent set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

8 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

9 
"agents = {Spy, Alice, Bob}" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

10 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

11 
definition bad :: "agent set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

12 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

13 
"bad = {Spy}" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

14 

58310  15 
datatype key = pubEK agent  priEK agent 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

16 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

17 
fun invKey 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

18 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

19 
"invKey (pubEK A) = priEK A" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

20 
 "invKey (priEK A) = pubEK A" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

21 

58310  22 
datatype 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

23 
msg = Agent agent 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

24 
 Key key 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

25 
 Nonce nat 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

26 
 MPair msg msg 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

27 
 Crypt key msg 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

28 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

29 
syntax 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

30 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})") 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

31 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

32 
syntax (xsymbols) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

33 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

34 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

35 
translations 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

36 
"{x, y, z}" == "{x, {y, z}}" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

37 
"{x, y}" == "CONST MPair x y" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

38 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

39 
inductive_set 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

40 
parts :: "msg set => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

41 
for H :: "msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

42 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

43 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

44 
 Fst: "{X,Y} \<in> parts H ==> X \<in> parts H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

45 
 Snd: "{X,Y} \<in> parts H ==> Y \<in> parts H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

46 
 Body: "Crypt K X \<in> parts H ==> X \<in> parts H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

47 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

48 
inductive_set 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

49 
analz :: "msg set => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

50 
for H :: "msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

51 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

52 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

53 
 Fst: "{X,Y} \<in> analz H ==> X \<in> analz H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

54 
 Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

55 
 Decrypt [dest]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

56 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

57 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

58 
inductive_set 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

59 
synth :: "msg set => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

60 
for H :: "msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

61 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

62 
Inj [intro]: "X \<in> H ==> X \<in> synth H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

63 
 Agent [intro]: "Agent agt \<in> synth H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

64 
 MPair [intro]: "[X \<in> synth H; Y \<in> synth H] ==> {X,Y} \<in> synth H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

65 
 Crypt [intro]: "[X \<in> synth H; Key(K) \<in> H] ==> Crypt K X \<in> synth H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

66 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

67 
primrec initState 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

68 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

69 
initState_Alice: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

70 
"initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

71 
 initState_Bob: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

72 
"initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

73 
 initState_Spy: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

74 
"initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

75 

58310  76 
datatype 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

77 
event = Says agent agent msg 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

78 
 Gets agent msg 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

79 
 Notes agent msg 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

80 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

81 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

82 
primrec knows :: "agent => event list => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

83 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

84 
knows_Nil: "knows A [] = initState A" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

85 
 knows_Cons: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

86 
"knows A (ev # evs) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

87 
(if A = Spy then 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

88 
(case ev of 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

89 
Says A' B X => insert X (knows Spy evs) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

90 
 Gets A' X => knows Spy evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

91 
 Notes A' X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

92 
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

93 
else 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

94 
(case ev of 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

95 
Says A' B X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

96 
if A'=A then insert X (knows A evs) else knows A evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

97 
 Gets A' X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

98 
if A'=A then insert X (knows A evs) else knows A evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

99 
 Notes A' X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

100 
if A'=A then insert X (knows A evs) else knows A evs))" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

101 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

102 
abbreviation (input) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

103 
spies :: "event list => msg set" where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

104 
"spies == knows Spy" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

105 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

106 
primrec used :: "event list => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

107 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

108 
used_Nil: "used [] = Union (parts ` initState ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

109 
 used_Cons: "used (ev # evs) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

110 
(case ev of 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

111 
Says A B X => parts {X} \<union> used evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

112 
 Gets A X => used evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

113 
 Notes A X => parts {X} \<union> used evs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

114 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

115 
subsection {* Preparations for sets *} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

116 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

117 
fun find_first :: "('a => 'b option) => 'a list => 'b option" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

118 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

119 
"find_first f [] = None" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

120 
 "find_first f (x # xs) = (case f x of Some y => Some y  None => find_first f xs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

121 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

122 
consts cps_of_set :: "'a set => ('a => term list option) => term list option" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

123 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

124 
lemma 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

125 
[code]: "cps_of_set (set xs) f = find_first f xs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

126 
sorry 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

127 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48618
diff
changeset

128 
consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48618
diff
changeset

129 
consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued" 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

130 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

131 
lemma 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

132 
[code]: "pos_cps_of_set (set xs) f i = find_first f xs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

133 
sorry 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

134 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

135 
consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

136 
=> 'b list => 'a Quickcheck_Exhaustive.three_valued" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

137 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

138 
lemma [code]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

139 
"find_first' f [] = Quickcheck_Exhaustive.No_value" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

140 
"find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs  Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x  Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x  _ => Quickcheck_Exhaustive.Unknown_value))" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

141 
sorry 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

142 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

143 
lemma 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

144 
[code]: "neg_cps_of_set (set xs) f i = find_first' f xs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

145 
sorry 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

146 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

147 
setup {* 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

148 
let 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

149 
val Fun = Predicate_Compile_Aux.Fun 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

150 
val Input = Predicate_Compile_Aux.Input 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

151 
val Output = Predicate_Compile_Aux.Output 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

152 
val Bool = Predicate_Compile_Aux.Bool 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

153 
val oi = Fun (Output, Fun (Input, Bool)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

154 
val ii = Fun (Input, Fun (Input, Bool)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

155 
fun of_set compfuns (Type ("fun", [T, _])) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

156 
case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

157 
Type ("Quickcheck_Exhaustive.three_valued", _) => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

158 
Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T > (Predicate_Compile_Aux.mk_monadT compfuns T)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

159 
 Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T > Predicate_Compile_Aux.mk_monadT compfuns T) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

160 
 _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T > (Predicate_Compile_Aux.mk_monadT compfuns T)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

161 
fun member compfuns (U as Type ("fun", [T, _])) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

162 
(absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

163 
(Const (@{const_name "Set.member"}, T > HOLogic.mk_setT T > @{typ bool}) $ Bound 1 $ Bound 0)))) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

164 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

165 
in 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

166 
Core_Data.force_modes_and_compilations @{const_name Set.member} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

167 
[(oi, (of_set, false)), (ii, (member, false))] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

168 
end 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

169 
*} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

170 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

171 
subsection {* Derived equations for analz, parts and synth *} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

172 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

173 
lemma [code]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

174 
"analz H = (let 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

175 
H' = H \<union> (Union ((%m. case m of {X, Y} => {X, Y}  Crypt K X => if Key (invKey K) : H then {X} else {}  _ => {}) ` H)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

176 
in if H' = H then H else analz H')" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

177 
sorry 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

178 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

179 
lemma [code]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

180 
"parts H = (let 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

181 
H' = H \<union> (Union ((%m. case m of {X, Y} => {X, Y}  Crypt K X => {X}  _ => {}) ` H)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

182 
in if H' = H then H else parts H')" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

183 
sorry 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

184 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

185 
definition synth' :: "msg set => msg => bool" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

186 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

187 
"synth' H m = (m : synth H)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

188 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

189 
lemmas [code_pred_intro] = synth.intros[folded synth'_def] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

190 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

191 
code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+ 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

192 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

193 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

194 
declare ListMem_iff[symmetric, code_pred_inline] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

195 
declare [[quickcheck_timing]] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

196 

58813  197 
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

198 
declare [[quickcheck_full_support = false]] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

199 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

200 
end 