--- a/src/HOL/Auth/DB-ROOT.ML Tue Sep 15 15:06:29 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: HOL/Auth/DB-ROOT
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Root file for creating a **separate database** for protocol proofs.
- ** Use ROOT.ML to simply run the proofs. **
-*)
-
-HOL_build_completed; (*Make examples fail if HOL did*)
-
-val banner = "Security Protocols";
-writeln banner;
-
-use_thy "Event";
--- a/src/HOL/Auth/Kerberos_BAN.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML Tue Sep 15 15:10:38 1998 +0200
@@ -180,7 +180,7 @@
(** Session keys are not used to encrypt other session keys **)
Goal "evs : kerberos_ban ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac kerberos_ban.induct 1);
--- a/src/HOL/Auth/NS_Shared.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Tue Sep 15 15:10:38 1998 +0200
@@ -174,7 +174,7 @@
(*The equality makes the induction hypothesis easier to apply*)
Goal "evs : ns_shared ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac ns_shared.induct 1);
--- a/src/HOL/Auth/OtwayRees.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Tue Sep 15 15:10:38 1998 +0200
@@ -134,7 +134,7 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-Goal "evs : otway ==> ALL K KK. KK <= Compl (range shrK) --> \
+Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Sep 15 15:10:38 1998 +0200
@@ -128,7 +128,7 @@
(*The equality makes the induction hypothesis easier to apply*)
Goal "evs : otway ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= -(range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 15 15:10:38 1998 +0200
@@ -139,7 +139,7 @@
(*The equality makes the induction hypothesis easier to apply*)
Goal "evs : otway ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
--- a/src/HOL/Auth/Recur.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Recur.ML Tue Sep 15 15:10:38 1998 +0200
@@ -185,10 +185,10 @@
Note that it holds for *any* set H (not just "spies evs")
satisfying the inductive hypothesis.*)
Goal "[| RB : responses evs; \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un H)) = \
\ (K : KK | Key K : analz H) |] \
-\ ==> ALL K KK. KK <= Compl (range shrK) --> \
+\ ==> ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (insert RB (Key``KK Un H))) = \
\ (K : KK | Key K : analz (insert RB H))";
by (etac responses.induct 1);
@@ -197,7 +197,7 @@
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
Goal "evs : recur ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac recur.induct 1);
@@ -215,7 +215,7 @@
(*Instance of the lemma with H replaced by (spies evs):
[| RB : responses evs; evs : recur; |]
- ==> KK <= Compl (range shrK) -->
+ ==> KK <= - (range shrK) -->
Key K : analz (insert RB (Key``KK Un spies evs)) =
(K : KK | Key K : analz (insert RB (spies evs)))
*)
@@ -289,11 +289,11 @@
Addsimps [shrK_in_analz_respond];
-Goal "[| RB : responses evs; \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un H)) = \
-\ (K : KK | Key K : analz H) |] \
-\ ==> (Key K : analz (insert RB H)) --> \
+Goal "[| RB : responses evs; \
+\ ALL K KK. KK <= - (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
+\ ==> (Key K : analz (insert RB H)) --> \
\ (Key K : parts{RB} | Key K : analz H)";
by (etac responses.induct 1);
by (ALLGOALS
--- a/src/HOL/Auth/Shared.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Shared.ML Tue Sep 15 15:10:38 1998 +0200
@@ -218,7 +218,7 @@
(*** Specialized rewriting for analz_insert_freshK ***)
-Goal "A <= Compl (range shrK) ==> shrK x ~: A";
+Goal "A <= - (range shrK) ==> shrK x ~: A";
by (Blast_tac 1);
qed "subset_Compl_range";
--- a/src/HOL/Auth/Yahalom.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML Tue Sep 15 15:10:38 1998 +0200
@@ -127,7 +127,7 @@
(** Session keys are not used to encrypt other session keys **)
Goal "evs : yahalom ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac yahalom.induct 1);
@@ -340,7 +340,7 @@
val Nonce_secrecy_lemma = result();
Goal "evs : yahalom ==> \
-\ (ALL KK. KK <= Compl (range shrK) --> \
+\ (ALL KK. KK <= - (range shrK) --> \
\ (ALL K: KK. ~ KeyWithNonce K NB evs) --> \
\ (Nonce NB : analz (Key``KK Un (spies evs))) = \
\ (Nonce NB : analz (spies evs)))";
--- a/src/HOL/Auth/Yahalom2.ML Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Tue Sep 15 15:10:38 1998 +0200
@@ -132,7 +132,7 @@
(** Session keys are not used to encrypt other session keys **)
Goal "evs : yahalom ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+\ ALL K KK. KK <= - (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac yahalom.induct 1);
--- a/src/HOL/HOL.thy Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/HOL.thy Tue Sep 15 15:10:38 1998 +0200
@@ -70,6 +70,7 @@
consts
"+" :: ['a::plus, 'a] => 'a (infixl 65)
"-" :: ['a::minus, 'a] => 'a (infixl 65)
+ uminus :: ['a::minus] => 'a ("- _" [80] 80)
"*" :: ['a::times, 'a] => 'a (infixl 70)
(*See Nat.thy for "^"*)
--- a/src/HOL/Set.thy Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Set.thy Tue Sep 15 15:10:38 1998 +0200
@@ -28,7 +28,6 @@
UNIV :: 'a set
insert :: ['a, 'a set] => 'a set
Collect :: ('a => bool) => 'a set (*comprehension*)
- Compl :: ('a set) => 'a set (*complement*)
Int :: ['a set, 'a set] => 'a set (infixl 70)
Un :: ['a set, 'a set] => 'a set (infixl 65)
UNION, INTER :: ['a set, 'a => 'b set] => 'b set (*general*)
@@ -41,11 +40,15 @@
"op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50)
+(*For compatibility: DELETE after one release*)
+syntax Compl :: ('a set) => 'a set (*complement*)
+translations "Compl A" => "- A"
(** Additional concrete syntax **)
syntax
+
(* Infix syntax for non-membership *)
"op ~:" :: ['a, 'a set] => bool ("op ~:")
@@ -144,7 +147,7 @@
Bex_def "Bex A P == ? x. x:A & P(x)"
subset_def "A <= B == ! x:A. x:B"
psubset_def "A < B == (A::'a set) <= B & ~ A=B"
- Compl_def "Compl A == {x. ~x:A}"
+ Compl_def "- A == {x. ~x:A}"
Un_def "A Un B == {x. x:A | x:B}"
Int_def "A Int B == {x. x:A & x:B}"
set_diff_def "A - B == {x. x:A & ~x:B}"