equal
deleted
inserted
replaced
39 Goal "knows Spy (Gets A X # evs) = knows Spy evs"; |
39 Goal "knows Spy (Gets A X # evs) = knows Spy evs"; |
40 by (Simp_tac 1); |
40 by (Simp_tac 1); |
41 qed "knows_Spy_Gets"; |
41 qed "knows_Spy_Gets"; |
42 |
42 |
43 Goal "knows Spy evs <= knows Spy (Says A B X # evs)"; |
43 Goal "knows Spy evs <= knows Spy (Says A B X # evs)"; |
44 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
44 by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1); |
45 qed "knows_Spy_subset_knows_Spy_Says"; |
45 qed "knows_Spy_subset_knows_Spy_Says"; |
46 |
46 |
47 Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; |
47 Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; |
48 by (Simp_tac 1); |
48 by (Simp_tac 1); |
49 by (Fast_tac 1); |
49 by (Fast_tac 1); |
50 qed "knows_Spy_subset_knows_Spy_Notes"; |
50 qed "knows_Spy_subset_knows_Spy_Notes"; |
51 |
51 |
52 Goal "knows Spy evs <= knows Spy (Gets A X # evs)"; |
52 Goal "knows Spy evs <= knows Spy (Gets A X # evs)"; |
53 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
53 by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1); |
54 qed "knows_Spy_subset_knows_Spy_Gets"; |
54 qed "knows_Spy_subset_knows_Spy_Gets"; |
55 |
55 |
56 (*Spy sees what is sent on the traffic*) |
56 (*Spy sees what is sent on the traffic*) |
57 Goal "Says A B X : set evs --> X : knows Spy evs"; |
57 Goal "Says A B X : set evs --> X : knows Spy evs"; |
58 by (induct_tac "evs" 1); |
58 by (induct_tac "evs" 1); |
87 by (Simp_tac 1); |
87 by (Simp_tac 1); |
88 qed "knows_Gets"; |
88 qed "knows_Gets"; |
89 |
89 |
90 |
90 |
91 Goal "knows A evs <= knows A (Says A B X # evs)"; |
91 Goal "knows A evs <= knows A (Says A B X # evs)"; |
92 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
92 by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1); |
93 qed "knows_subset_knows_Says"; |
93 qed "knows_subset_knows_Says"; |
94 |
94 |
95 Goal "knows A evs <= knows A (Notes A X # evs)"; |
95 Goal "knows A evs <= knows A (Notes A X # evs)"; |
96 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
96 by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1); |
97 qed "knows_subset_knows_Notes"; |
97 qed "knows_subset_knows_Notes"; |
98 |
98 |
99 Goal "knows A evs <= knows A (Gets A X # evs)"; |
99 Goal "knows A evs <= knows A (Gets A X # evs)"; |
100 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
100 by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1); |
101 qed "knows_subset_knows_Gets"; |
101 qed "knows_subset_knows_Gets"; |
102 |
102 |
103 (*Agents know what they say*) |
103 (*Agents know what they say*) |
104 Goal "Says A B X : set evs --> X : knows A evs"; |
104 Goal "Says A B X : set evs --> X : knows A evs"; |
105 by (induct_tac "evs" 1); |
105 by (induct_tac "evs" 1); |