src/HOL/Auth/Event.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 6399 4a9040b85e2e
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
     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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    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
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    19
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    27
qed "expand_event_case";
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    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
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    32
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    33
(*The point of letting the Spy see "bad" agents' notes is to prevent
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    34
  redundant case-splits 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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    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
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    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
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    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
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
    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
42a726e008ce Now uses the generic induct_tac
paulson
parents: 3519
diff changeset
    59
by (induct_tac "evs" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
    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
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    64
by (induct_tac "evs" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
    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
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3667
diff changeset
    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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   148
(**** NOTE REMOVAL--laws 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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   155
by (induct_tac "evs" 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   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
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
   158
	                addsplits [expand_event_case])));
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   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
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   165
Goal "parts (initState B) <= used evs";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   166
by (induct_tac "evs" 1);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   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
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
   169
	                addsplits [expand_event_case])));
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   170
by (ALLGOALS Blast_tac);
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   171
bind_thm ("initState_into_used", impOfSubs (result()));
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   172
5076
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   173
Goal "used (Says A B X # evs) = parts{X} Un used evs";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   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
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   178
Goal "used (Notes A X # evs) = parts{X} Un used evs";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   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
fbc9d95b62ba Ran isatool fixgoal
paulson
parents: 4686
diff changeset
   188
Goal "used [] <= used evs";
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   189
by (Simp_tac 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   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
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   193
(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   194
Delsimps [used_Nil, used_Cons];   
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   195
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
   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
dab1833cb26d analz_mono_contra_tac was wrong
paulson
parents: 4091
diff changeset
   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
dab1833cb26d analz_mono_contra_tac was wrong
paulson
parents: 4091
diff changeset
   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;