author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 6399  4a9040b85e2e 
permissions  rwrr 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

1 
(* Title: HOL/Auth/Event 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

2 
ID: $Id$ 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

5 
*) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

6 

3683  7 
AddIffs [Spy_in_bad, Server_not_bad]; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

8 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

9 
Addsimps [knows_Cons, used_Cons]; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

10 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

11 
(**** Function "knows" ****) 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

12 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

13 
(** Simplifying parts (insert X (knows Spy evs)) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

14 
= parts {X} Un parts (knows Spy evs)  since general case loops*) 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

15 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

16 
bind_thm ("parts_insert_knows_Spy", 
3683  17 
parts_insert > 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

18 
read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]); 
3678  19 

20 

6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

21 
Goal "P(event_case sf gf nf ev) = \ 
3683  22 
\ ((ALL A B X. ev = Says A B X > P(sf A B X)) & \ 
6399
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

23 
\ (ALL A X. ev = Gets A X > P(gf A X)) & \ 
4a9040b85e2e
exchanged the order of Gets and Notes in datatype event
paulson
parents:
6308
diff
changeset

24 
\ (ALL A X. ev = Notes A X > P(nf A X)))"; 
3683  25 
by (induct_tac "ev" 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4266
diff
changeset

26 
by Auto_tac; 
3683  27 
qed "expand_event_case"; 
3678  28 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

29 
Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"; 
3683  30 
by (Simp_tac 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

31 
qed "knows_Spy_Says"; 
3678  32 

3683  33 
(*The point of letting the Spy see "bad" agents' notes is to prevent 
34 
redundant casesplits on whether A=Spy and whether A:bad*) 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

35 
Goal "knows Spy (Notes A X # evs) = \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

36 
\ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"; 
3683  37 
by (Simp_tac 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

38 
qed "knows_Spy_Notes"; 
3678  39 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

40 
Goal "knows Spy (Gets A X # evs) = knows Spy evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

41 
by (Simp_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

42 
qed "knows_Spy_Gets"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

43 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

44 
Goal "knows Spy evs <= knows Spy (Says A B X # evs)"; 
4091  45 
by (simp_tac (simpset() addsimps [subset_insertI]) 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

46 
qed "knows_Spy_subset_knows_Spy_Says"; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

47 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

48 
Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; 
4686  49 
by (Simp_tac 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

50 
by (Fast_tac 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

51 
qed "knows_Spy_subset_knows_Spy_Notes"; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

52 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

53 
Goal "knows Spy evs <= knows Spy (Gets A X # evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

54 
by (simp_tac (simpset() addsimps [subset_insertI]) 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

55 
qed "knows_Spy_subset_knows_Spy_Gets"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

56 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

57 
(*Spy sees what is sent on the traffic*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

58 
Goal "Says A B X : set evs > X : knows Spy evs"; 
3667  59 
by (induct_tac "evs" 1); 
4686  60 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

61 
qed_spec_mp "Says_imp_knows_Spy"; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

62 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

63 
Goal "Notes A X : set evs > A: bad > X : knows Spy evs"; 
3678  64 
by (induct_tac "evs" 1); 
4686  65 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

66 
qed_spec_mp "Notes_imp_knows_Spy"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

67 

3678  68 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

69 
(*Use with addSEs to derive contradictions from old Says events containing 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

70 
items known to be fresh*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

71 
val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

72 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

73 
Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets]; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

74 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

75 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

76 
(*Begin lemmas about agents' knowledge*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

77 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

78 
Goal "knows A (Says A B X # evs) = insert X (knows A evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

79 
by (Simp_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

80 
qed "knows_Says"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

81 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

82 
Goal "knows A (Notes A X # evs) = insert X (knows A evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

83 
by (Simp_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

84 
qed "knows_Notes"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

85 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

86 
Goal "A ~= Spy > knows A (Gets A X # evs) = insert X (knows A evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

87 
by (Simp_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

88 
qed "knows_Gets"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

89 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

90 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

91 
Goal "knows A evs <= knows A (Says A B X # evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

92 
by (simp_tac (simpset() addsimps [subset_insertI]) 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

93 
qed "knows_subset_knows_Says"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

94 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

95 
Goal "knows A evs <= knows A (Notes A X # evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

96 
by (simp_tac (simpset() addsimps [subset_insertI]) 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

97 
qed "knows_subset_knows_Notes"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

98 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

99 
Goal "knows A evs <= knows A (Gets A X # evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

100 
by (simp_tac (simpset() addsimps [subset_insertI]) 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

101 
qed "knows_subset_knows_Gets"; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

102 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

103 
(*Agents know what they say*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

104 
Goal "Says A B X : set evs > X : knows A evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

105 
by (induct_tac "evs" 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

106 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

107 
by (Blast_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

108 
qed_spec_mp "Says_imp_knows"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

109 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

110 
(*Agents know what they note*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

111 
Goal "Notes A X : set evs > X : knows A evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

112 
by (induct_tac "evs" 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

113 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

114 
by (Blast_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

115 
qed_spec_mp "Notes_imp_knows"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

116 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

117 
(*Agents know what they receive*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

118 
Goal "A ~= Spy > Gets A X : set evs > X : knows A evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

119 
by (induct_tac "evs" 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

120 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

121 
qed_spec_mp "Gets_imp_knows_agents"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

122 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

123 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

124 
(*What agents DIFFERENT FROM Spy know 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

125 
was either said, or noted, or got, or known initially*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

126 
Goal "[ X : knows A evs; A ~= Spy ] ==> EX B. \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

127 
\ Says A B X : set evs  Gets A X : set evs  Notes A X : set evs  X : initState A"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

128 
by (etac rev_mp 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

129 
by (induct_tac "evs" 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

130 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

131 
by (Blast_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

132 
qed_spec_mp "knows_imp_Says_Gets_Notes_initState"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

133 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

134 
(*What the Spy knows  for the time being  
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

135 
was either said or noted, or known initially*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

136 
Goal "[ X : knows Spy evs ] ==> EX A B. \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

137 
\ Says A B X : set evs  Notes A X : set evs  X : initState Spy"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

138 
by (etac rev_mp 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

139 
by (induct_tac "evs" 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

140 
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

141 
by (Blast_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

142 
qed_spec_mp "knows_Spy_imp_Says_Notes_initState"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

143 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

144 
(*END lemmas about agents' knowledge*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

145 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

146 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

147 

3683  148 
(**** NOTE REMOVALlaws above are cleaner, as they don't involve "case" ****) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

149 
Delsimps [knows_Cons]; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

150 

9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

151 

9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

152 
(*** Fresh nonces ***) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

153 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

154 
Goal "parts (knows Spy evs) <= used evs"; 
3683  155 
by (induct_tac "evs" 1); 
156 
by (ALLGOALS (asm_simp_tac 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

157 
(simpset() addsimps [parts_insert_knows_Spy] 
4686  158 
addsplits [expand_event_case]))); 
3683  159 
by (ALLGOALS Blast_tac); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

160 
qed "parts_knows_Spy_subset_used"; 
3701
6f0ed3eef1a9
Names and saves the theorem parts_spies_subset_used
paulson
parents:
3683
diff
changeset

161 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

162 
bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

163 
AddIs [usedI]; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

164 

5076  165 
Goal "parts (initState B) <= used evs"; 
3683  166 
by (induct_tac "evs" 1); 
167 
by (ALLGOALS (asm_simp_tac 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

168 
(simpset() addsimps [parts_insert_knows_Spy] 
4686  169 
addsplits [expand_event_case]))); 
3683  170 
by (ALLGOALS Blast_tac); 
171 
bind_thm ("initState_into_used", impOfSubs (result())); 

172 

5076  173 
Goal "used (Says A B X # evs) = parts{X} Un used evs"; 
3683  174 
by (Simp_tac 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

175 
qed "used_Says"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

176 
Addsimps [used_Says]; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

177 

5076  178 
Goal "used (Notes A X # evs) = parts{X} Un used evs"; 
3683  179 
by (Simp_tac 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

180 
qed "used_Notes"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

181 
Addsimps [used_Notes]; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

182 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

183 
Goal "used (Gets A X # evs) = used evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

184 
by (Simp_tac 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

185 
qed "used_Gets"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

186 
Addsimps [used_Gets]; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

187 

5076  188 
Goal "used [] <= used evs"; 
3683  189 
by (Simp_tac 1); 
4091  190 
by (blast_tac (claset() addIs [initState_into_used]) 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

191 
qed "used_nil_subset"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

192 

3683  193 
(**** NOTE REMOVALlaws above are cleaner, as they don't involve "case" ****) 
194 
Delsimps [used_Nil, used_Cons]; 

195 

196 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

197 
(*For proving theorems of the form X ~: analz (knows Spy evs) > P 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

198 
New events added by induction to "evs" are discarded. Provided 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

199 
this information isn't needed, the proof will be much shorter, since 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

200 
it will omit complicated reasoning about analz.*) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

201 
val analz_mono_contra_tac = 
4266  202 
let val analz_impI = read_instantiate_sg (sign_of thy) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

203 
[("P", "?Y ~: analz (knows Spy ?evs)")] impI; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

204 
in 
4266  205 
rtac analz_impI THEN' 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

206 
REPEAT1 o 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

207 
(dresolve_tac 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

208 
[knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD, 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

209 
knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD, 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

210 
knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]) 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

211 
THEN' 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

212 
mp_tac 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff
changeset

213 
end; 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

214 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

215 
fun Reception_tac i = 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

216 
blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

217 
impOfSubs (parts_insert RS equalityD1), 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

218 
parts_trans, 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

219 
Says_imp_knows_Spy RS analz.Inj, 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

220 
impOfSubs analz_mono, analz_cut] 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

221 
addIs [less_SucI]) i; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

222 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

223 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

224 
(*Compatibility for the old "spies" function*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

225 
val spies_partsEs = knows_Spy_partsEs; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

226 
val Says_imp_spies = Says_imp_knows_Spy; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

227 
val parts_insert_spies = parts_insert_knows_Spy; 