# HG changeset patch # User paulson # Date 905865038 -7200 # Node ID d9fc3457554e9ab3a490e0c89a7cf2a71373c208 # Parent 22f8331cdf47e6de9ef748e0dca0711211a8cd7c From Compl(A) to -A diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/DB-ROOT.ML --- 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"; diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/Kerberos_BAN.ML --- 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); diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/NS_Shared.ML --- 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); diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/OtwayRees.ML --- 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); diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/OtwayRees_AN.ML --- 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); diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/OtwayRees_Bad.ML --- 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); diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/Recur.ML --- 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 diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/Shared.ML --- 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"; diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/Yahalom.ML --- 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)))"; diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/Yahalom2.ML --- 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); diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/HOL.thy --- 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 "^"*) diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Set.thy --- 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}"