From Compl(A) to -A
authorpaulson
Tue Sep 15 15:10:38 1998 +0200 (1998-09-15)
changeset 5492d9fc3457554e
parent 5491 22f8331cdf47
child 5493 e335c51808ac
From Compl(A) to -A
src/HOL/Auth/DB-ROOT.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/HOL.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Auth/DB-ROOT.ML	Tue Sep 15 15:06:29 1998 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,15 +0,0 @@
     1.4 -(*  Title:      HOL/Auth/DB-ROOT
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1996  University of Cambridge
     1.8 -
     1.9 -Root file for creating a **separate database** for protocol proofs.
    1.10 -             ** Use ROOT.ML to simply run the proofs. **
    1.11 -*)
    1.12 -
    1.13 -HOL_build_completed;    (*Make examples fail if HOL did*)
    1.14 -
    1.15 -val banner = "Security Protocols";
    1.16 -writeln banner;
    1.17 -
    1.18 -use_thy "Event";
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 15 15:06:29 1998 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 15 15:10:38 1998 +0200
     2.3 @@ -180,7 +180,7 @@
     2.4  (** Session keys are not used to encrypt other session keys **)
     2.5  
     2.6  Goal "evs : kerberos_ban ==>                          \
     2.7 -\  ALL K KK. KK <= Compl (range shrK) -->                \
     2.8 +\  ALL K KK. KK <= - (range shrK) -->                 \
     2.9  \         (Key K : analz (Key``KK Un (spies evs))) =  \
    2.10  \         (K : KK | Key K : analz (spies evs))";
    2.11  by (etac kerberos_ban.induct 1);
     3.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 15 15:06:29 1998 +0200
     3.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Sep 15 15:10:38 1998 +0200
     3.3 @@ -174,7 +174,7 @@
     3.4  
     3.5  (*The equality makes the induction hypothesis easier to apply*)
     3.6  Goal "evs : ns_shared ==>                             \
     3.7 -\  ALL K KK. KK <= Compl (range shrK) -->                \
     3.8 +\  ALL K KK. KK <= - (range shrK) -->                 \
     3.9  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    3.10  \            (K : KK | Key K : analz (spies evs))";
    3.11  by (etac ns_shared.induct 1);
     4.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 15 15:06:29 1998 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 15 15:10:38 1998 +0200
     4.3 @@ -134,7 +134,7 @@
     4.4  (** Session keys are not used to encrypt other session keys **)
     4.5  
     4.6  (*The equality makes the induction hypothesis easier to apply*)
     4.7 -Goal "evs : otway ==> ALL K KK. KK <= Compl (range shrK) -->       \
     4.8 +Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) -->           \
     4.9  \                      (Key K : analz (Key``KK Un (spies evs))) =  \
    4.10  \                      (K : KK | Key K : analz (spies evs))";
    4.11  by (etac otway.induct 1);
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 15 15:06:29 1998 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 15 15:10:38 1998 +0200
     5.3 @@ -128,7 +128,7 @@
     5.4  
     5.5  (*The equality makes the induction hypothesis easier to apply*)
     5.6  Goal "evs : otway ==>                                 \
     5.7 -\  ALL K KK. KK <= Compl (range shrK) -->                \
     5.8 +\  ALL K KK. KK <= -(range shrK) -->                  \
     5.9  \         (Key K : analz (Key``KK Un (spies evs))) =  \
    5.10  \         (K : KK | Key K : analz (spies evs))";
    5.11  by (etac otway.induct 1);
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 15 15:06:29 1998 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 15 15:10:38 1998 +0200
     6.3 @@ -139,7 +139,7 @@
     6.4  
     6.5  (*The equality makes the induction hypothesis easier to apply*)
     6.6  Goal "evs : otway ==>                                 \
     6.7 -\  ALL K KK. KK <= Compl (range shrK) -->             \
     6.8 +\  ALL K KK. KK <= - (range shrK) -->                 \
     6.9  \         (Key K : analz (Key``KK Un (spies evs))) =  \
    6.10  \         (K : KK | Key K : analz (spies evs))";
    6.11  by (etac otway.induct 1);
     7.1 --- a/src/HOL/Auth/Recur.ML	Tue Sep 15 15:06:29 1998 +0200
     7.2 +++ b/src/HOL/Auth/Recur.ML	Tue Sep 15 15:10:38 1998 +0200
     7.3 @@ -185,10 +185,10 @@
     7.4    Note that it holds for *any* set H (not just "spies evs")
     7.5    satisfying the inductive hypothesis.*)
     7.6  Goal "[| RB : responses evs;                             \
     7.7 -\        ALL K KK. KK <= Compl (range shrK) -->          \
     7.8 +\        ALL K KK. KK <= - (range shrK) -->              \
     7.9  \                  (Key K : analz (Key``KK Un H)) =      \
    7.10  \                  (K : KK | Key K : analz H) |]         \
    7.11 -\    ==> ALL K KK. KK <= Compl (range shrK) -->          \
    7.12 +\    ==> ALL K KK. KK <= - (range shrK) -->              \
    7.13  \                  (Key K : analz (insert RB (Key``KK Un H))) = \
    7.14  \                  (K : KK | Key K : analz (insert RB H))";
    7.15  by (etac responses.induct 1);
    7.16 @@ -197,7 +197,7 @@
    7.17  
    7.18  (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
    7.19  Goal "evs : recur ==>                                 \
    7.20 -\  ALL K KK. KK <= Compl (range shrK) -->                \
    7.21 +\  ALL K KK. KK <= - (range shrK) -->                 \
    7.22  \         (Key K : analz (Key``KK Un (spies evs))) =  \
    7.23  \         (K : KK | Key K : analz (spies evs))";
    7.24  by (etac recur.induct 1);
    7.25 @@ -215,7 +215,7 @@
    7.26  
    7.27  (*Instance of the lemma with H replaced by (spies evs):
    7.28     [| RB : responses evs;  evs : recur; |]
    7.29 -   ==> KK <= Compl (range shrK) --> 
    7.30 +   ==> KK <= - (range shrK) --> 
    7.31         Key K : analz (insert RB (Key``KK Un spies evs)) =
    7.32         (K : KK | Key K : analz (insert RB (spies evs))) 
    7.33  *)
    7.34 @@ -289,11 +289,11 @@
    7.35  Addsimps [shrK_in_analz_respond];
    7.36  
    7.37  
    7.38 -Goal "[| RB : responses evs;                             \
    7.39 -\        ALL K KK. KK <= Compl (range shrK) -->          \
    7.40 -\                  (Key K : analz (Key``KK Un H)) =      \
    7.41 -\                  (K : KK | Key K : analz H) |]         \
    7.42 -\    ==> (Key K : analz (insert RB H)) -->               \
    7.43 +Goal "[| RB : responses evs;                         \
    7.44 +\        ALL K KK. KK <= - (range shrK) -->          \
    7.45 +\                  (Key K : analz (Key``KK Un H)) =  \
    7.46 +\                  (K : KK | Key K : analz H) |]     \
    7.47 +\    ==> (Key K : analz (insert RB H)) -->           \
    7.48  \        (Key K : parts{RB} | Key K : analz H)";
    7.49  by (etac responses.induct 1);
    7.50  by (ALLGOALS
     8.1 --- a/src/HOL/Auth/Shared.ML	Tue Sep 15 15:06:29 1998 +0200
     8.2 +++ b/src/HOL/Auth/Shared.ML	Tue Sep 15 15:10:38 1998 +0200
     8.3 @@ -218,7 +218,7 @@
     8.4  
     8.5  (*** Specialized rewriting for analz_insert_freshK ***)
     8.6  
     8.7 -Goal "A <= Compl (range shrK) ==> shrK x ~: A";
     8.8 +Goal "A <= - (range shrK) ==> shrK x ~: A";
     8.9  by (Blast_tac 1);
    8.10  qed "subset_Compl_range";
    8.11  
     9.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Sep 15 15:06:29 1998 +0200
     9.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Sep 15 15:10:38 1998 +0200
     9.3 @@ -127,7 +127,7 @@
     9.4  (** Session keys are not used to encrypt other session keys **)
     9.5  
     9.6  Goal "evs : yahalom ==>                              \
     9.7 -\  ALL K KK. KK <= Compl (range shrK) -->               \
     9.8 +\  ALL K KK. KK <= - (range shrK) -->                \
     9.9  \         (Key K : analz (Key``KK Un (spies evs))) = \
    9.10  \         (K : KK | Key K : analz (spies evs))";
    9.11  by (etac yahalom.induct 1);
    9.12 @@ -340,7 +340,7 @@
    9.13  val Nonce_secrecy_lemma = result();
    9.14  
    9.15  Goal "evs : yahalom ==>                                      \
    9.16 -\     (ALL KK. KK <= Compl (range shrK) -->                  \
    9.17 +\     (ALL KK. KK <= - (range shrK) -->                      \
    9.18  \          (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
    9.19  \          (Nonce NB : analz (Key``KK Un (spies evs))) =     \
    9.20  \          (Nonce NB : analz (spies evs)))";
    10.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 15 15:06:29 1998 +0200
    10.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 15 15:10:38 1998 +0200
    10.3 @@ -132,7 +132,7 @@
    10.4  (** Session keys are not used to encrypt other session keys **)
    10.5  
    10.6  Goal "evs : yahalom ==>                               \
    10.7 -\  ALL K KK. KK <= Compl (range shrK) -->                \
    10.8 +\  ALL K KK. KK <= - (range shrK) -->                 \
    10.9  \         (Key K : analz (Key``KK Un (spies evs))) =  \
   10.10  \         (K : KK | Key K : analz (spies evs))";
   10.11  by (etac yahalom.induct 1);
    11.1 --- a/src/HOL/HOL.thy	Tue Sep 15 15:06:29 1998 +0200
    11.2 +++ b/src/HOL/HOL.thy	Tue Sep 15 15:10:38 1998 +0200
    11.3 @@ -70,6 +70,7 @@
    11.4  consts
    11.5    "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
    11.6    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    11.7 +  uminus        :: ['a::minus] => 'a                ("- _" [80] 80)
    11.8    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    11.9    (*See Nat.thy for "^"*)
   11.10  
    12.1 --- a/src/HOL/Set.thy	Tue Sep 15 15:06:29 1998 +0200
    12.2 +++ b/src/HOL/Set.thy	Tue Sep 15 15:10:38 1998 +0200
    12.3 @@ -28,7 +28,6 @@
    12.4    UNIV          :: 'a set
    12.5    insert        :: ['a, 'a set] => 'a set
    12.6    Collect       :: ('a => bool) => 'a set               (*comprehension*)
    12.7 -  Compl         :: ('a set) => 'a set                   (*complement*)
    12.8    Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    12.9    Un            :: ['a set, 'a set] => 'a set       (infixl 65)
   12.10    UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
   12.11 @@ -41,11 +40,15 @@
   12.12    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
   12.13  
   12.14  
   12.15 +(*For compatibility: DELETE after one release*)
   12.16 +syntax Compl :: ('a set) => 'a set   (*complement*)
   12.17 +translations "Compl A"  => "- A"
   12.18  
   12.19  (** Additional concrete syntax **)
   12.20  
   12.21  syntax
   12.22  
   12.23 +
   12.24    (* Infix syntax for non-membership *)
   12.25  
   12.26    "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
   12.27 @@ -144,7 +147,7 @@
   12.28    Bex_def       "Bex A P        == ? x. x:A & P(x)"
   12.29    subset_def    "A <= B         == ! x:A. x:B"
   12.30    psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
   12.31 -  Compl_def     "Compl A        == {x. ~x:A}"
   12.32 +  Compl_def     "- A            == {x. ~x:A}"
   12.33    Un_def        "A Un B         == {x. x:A | x:B}"
   12.34    Int_def       "A Int B        == {x. x:A & x:B}"
   12.35    set_diff_def  "A - B          == {x. x:A & ~x:B}"