--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Thu Feb 15 13:04:36 2018 +0100
@@ -49,7 +49,7 @@
| Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
| Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
| Decrypt [dest]:
- "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
+ "[|Crypt K X \<in> analz H; Key(invKey K) \<in> analz H|] ==> X \<in> analz H"
inductive_set
synth :: "msg set => msg set"
@@ -168,7 +168,7 @@
lemma [code]:
"analz H = (let
- H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+ H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) \<in> H then {X} else {} | _ => {}) ` H))
in if H' = H then H else analz H')"
sorry
@@ -180,7 +180,7 @@
definition synth' :: "msg set => msg => bool"
where
- "synth' H m = (m : synth H)"
+ "synth' H m = (m \<in> synth H)"
lemmas [code_pred_intro] = synth.intros[folded synth'_def]
--- a/src/Doc/Prog_Prove/Isar.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy Thu Feb 15 13:04:36 2018 +0100
@@ -332,7 +332,7 @@
\begin{minipage}[t]{.4\textwidth}
\isa{%
\<close>
-(*<*)lemma "ALL x. P x" proof-(*>*)
+(*<*)lemma "\<forall>x. P x" proof-(*>*)
show "\<forall>x. P(x)"
proof
fix x
@@ -346,7 +346,7 @@
\begin{minipage}[t]{.4\textwidth}
\isa{%
\<close>
-(*<*)lemma "EX x. P(x)" proof-(*>*)
+(*<*)lemma "\<exists>x. P(x)" proof-(*>*)
show "\<exists>x. P(x)"
proof
text_raw\<open>\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}\<close>
@@ -370,7 +370,7 @@
How to reason forward from \noquotes{@{prop[source] "\<exists>x. P(x)"}}:
\end{isamarkuptext}%
\<close>
-(*<*)lemma True proof- assume 1: "EX x. P x"(*>*)
+(*<*)lemma True proof- assume 1: "\<exists>x. P x"(*>*)
have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw\<open>\ \isasymproof\\\<close>
then obtain x where p: "P(x)" by blast
(*<*)oops(*>*)
@@ -1066,7 +1066,7 @@
reasoning backwards: by which rules could some given fact have been proved?
For the inductive definition of @{const ev}, rule inversion can be summarized
like this:
-@{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (EX k. n = Suc(Suc k) \<and> ev k)"}
+@{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (\<exists>k. n = Suc(Suc k) \<and> ev k)"}
The realisation in Isabelle is a case analysis.
A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n - 2)"}. We
already went through the details informally in \autoref{sec:Logic:even}. This
@@ -1223,7 +1223,7 @@
\begin{exercise}
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
-and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
+and prove @{prop "x \<in> elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
\end{exercise}
\begin{exercise}
--- a/src/Doc/Prog_Prove/Logic.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Thu Feb 15 13:04:36 2018 +0100
@@ -97,7 +97,7 @@
\noquotes{@{term[source] "{t | x y. P}"}}\index{$IMP042@@{text"{t |x. P}"}},
where @{text "x y"} are those free variables in @{text t}
that occur in @{text P}.
-This is just a shorthand for @{term"{v. EX x y. v = t \<and> P}"}, where
+This is just a shorthand for @{term"{v. \<exists>x y. v = t \<and> P}"}, where
@{text v} is a new variable. For example, @{term"{x+y|x. x \<in> A}"}
is short for \noquotes{@{term[source]"{v. \<exists>x. v = x+y \<and> x \<in> A}"}}.
\end{warn}
@@ -111,8 +111,8 @@
@{text "\<inter>"} & \texttt{\char`\\\char`\<inter>} & \texttt{Int}
\end{tabular}
\end{center}
-Sets also allow bounded quantifications @{prop"ALL x : A. P"} and
-@{prop"EX x : A. P"}.
+Sets also allow bounded quantifications @{prop"\<forall>x \<in> A. P"} and
+@{prop"\<exists>x \<in> A. P"}.
For the more ambitious, there are also @{text"\<Union>"}\index{$HOLSet6@\isasymUnion}
and @{text"\<Inter>"}\index{$HOLSet7@\isasymInter}:
@@ -703,7 +703,7 @@
that maps a binary predicate to another binary predicate: if @{text r} is of
type @{text"\<tau> \<Rightarrow> \<tau> \<Rightarrow> bool"} then @{term "star r"} is again of type @{text"\<tau> \<Rightarrow>
\<tau> \<Rightarrow> bool"}, and @{prop"star r x y"} means that @{text x} and @{text y} are in
-the relation @{term"star r"}. Think @{term"r^*"} when you see @{term"star
+the relation @{term"star r"}. Think @{term"r\<^sup>*"} when you see @{term"star
r"}, because @{text"star r"} is meant to be the reflexive transitive closure.
That is, @{prop"star r x y"} is meant to be true if from @{text x} we can
reach @{text y} in finitely many @{text r} steps. This concept is naturally
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Thu Feb 15 13:04:36 2018 +0100
@@ -525,7 +525,7 @@
simplify to @{const True}.
We can split case-expressions similarly. For @{text nat} the rule looks like this:
-@{prop[display,margin=65,indent=4]"P(case e of 0 \<Rightarrow> a | Suc n \<Rightarrow> b n) = ((e = 0 \<longrightarrow> P a) & (ALL n. e = Suc n \<longrightarrow> P(b n)))"}
+@{prop[display,margin=65,indent=4]"P(case e of 0 \<Rightarrow> a | Suc n \<Rightarrow> b n) = ((e = 0 \<longrightarrow> P a) \<and> (\<forall>n. e = Suc n \<longrightarrow> P(b n)))"}
Case expressions are not split automatically by @{text simp}, but @{text simp}
can be instructed to do so:
\begin{quote}
--- a/src/Doc/Sugar/Sugar.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Sugar/Sugar.thy Thu Feb 15 13:04:36 2018 +0100
@@ -55,7 +55,7 @@
\subsection{Logic}
-The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
+The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"\<not>(\<exists>x. P x)"}.
The predefined constructs @{text"if"}, @{text"let"} and
@{text"case"} are set in sans serif font to distinguish them from
--- a/src/Doc/Tutorial/CTL/CTL.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/CTL/CTL.thy Thu Feb 15 13:04:36 2018 +0100
@@ -153,7 +153,7 @@
done
text\<open>\noindent
-We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
+We assume the negation of the conclusion and prove @{term"s \<in> lfp(af A)"}.
Unfolding @{const lfp} once and
simplifying with the definition of @{const af} finishes the proof.
@@ -214,14 +214,14 @@
txt\<open>\noindent
After simplification, the base case boils down to
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
-The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
+The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t)\<in>M"}
holds. However, we first have to show that such a @{term t} actually exists! This reasoning
is embodied in the theorem @{thm[source]someI2_ex}:
@{thm[display,eta_contract=false]someI2_ex}
When we apply this theorem as an introduction rule, @{text"?P x"} becomes
-@{prop"(s, x) : M & Q x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove
-two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and
-@{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
+@{prop"(s, x) \<in> M \<and> Q x"} and @{text"?Q x"} becomes @{prop"(s,x) \<in> M"} and we have to prove
+two subgoals: @{prop"\<exists>a. (s, a) \<in> M \<and> Q a"}, which follows from the assumptions, and
+@{prop"(s, x) \<in> M \<and> Q x \<Longrightarrow> (s,x) \<in> M"}, which is trivial. Thus it is not surprising that
@{text fast} can prove the base case quickly:
\<close>
--- a/src/Doc/Tutorial/CTL/PDL.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/CTL/PDL.thy Thu Feb 15 13:04:36 2018 +0100
@@ -129,7 +129,7 @@
forward direction. Fortunately the converse induction theorem
@{thm[source]converse_rtrancl_induct} already exists:
@{thm[display,margin=60]converse_rtrancl_induct[no_vars]}
-It says that if @{prop"(a,b):r\<^sup>*"} and we know @{prop"P b"} then we can infer
+It says that if @{prop"(a,b)\<in>r\<^sup>*"} and we know @{prop"P b"} then we can infer
@{prop"P a"} provided each step backwards from a predecessor @{term z} of
@{term b} preserves @{term P}.
\<close>
@@ -176,7 +176,7 @@
\footnote{We cannot use the customary @{text EX}: it is reserved
as the \textsc{ascii}-equivalent of @{text"\<exists>"}.}
with the intended semantics
-@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
+@{prop[display]"(s \<Turnstile> EN f) = (\<exists>t. (s,t) \<in> M \<and> t \<Turnstile> f)"}
Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
Show that the semantics for @{term EF} satisfies the following recursion equation:
@@ -190,7 +190,7 @@
apply(auto simp add: EF_lemma)
done
-lemma aux: "s \<Turnstile> f = (s : mc f)"
+lemma aux: "s \<Turnstile> f = (s \<in> mc f)"
apply(simp add: main)
done
--- a/src/Doc/Tutorial/Ifexpr/Ifexpr.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Ifexpr/Ifexpr.thy Thu Feb 15 13:04:36 2018 +0100
@@ -201,7 +201,7 @@
(case b of CIF b => False | VIF x => True | IF x y z => False))"
lemma [simp]:
- "ALL t e. valif (normif2 b t e) env = valif (IF b t e) env"
+ "\<forall>t e. valif (normif2 b t e) env = valif (IF b t e) env"
apply(induct b)
by(auto)
@@ -209,7 +209,7 @@
apply(induct b)
by(auto)
-lemma [simp]: "ALL t e. normal2 t & normal2 e --> normal2(normif2 b t e)"
+lemma [simp]: "\<forall>t e. normal2 t & normal2 e --> normal2(normif2 b t e)"
apply(induct b)
by(auto)
--- a/src/Doc/Tutorial/Inductive/Mutual.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/Mutual.thy Thu Feb 15 13:04:36 2018 +0100
@@ -67,7 +67,7 @@
text\<open>\noindent Everything works as before, except that
you write \commdx{inductive} instead of \isacommand{inductive\_set} and
-@{prop"evn n"} instead of @{prop"n : Even"}.
+@{prop"evn n"} instead of @{prop"n \<in> Even"}.
When defining an n-ary relation as a predicate, it is recommended to curry
the predicate: its type should be \mbox{@{text"\<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> bool"}}
rather than
--- a/src/Doc/Tutorial/Inductive/Star.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/Star.thy Thu Feb 15 13:04:36 2018 +0100
@@ -77,7 +77,7 @@
is what we want, it is merely due to the order in which the assumptions occur
in the subgoal, which it is not good practice to rely on. As a result,
@{text"?xb"} becomes @{term x}, @{text"?xa"} becomes
-@{term y} and @{text"?P"} becomes @{term"%u v. (u,z) : r*"}, thus
+@{term y} and @{text"?P"} becomes @{term"\<lambda>u v. (u,z) \<in> r*"}, thus
yielding the above subgoal. So what went wrong?
When looking at the instantiation of @{text"?P"} we see that it does not
@@ -85,7 +85,7 @@
goal, of the pair @{term"(x,y)"} only @{term x} appears also in the
conclusion, but not @{term y}. Thus our induction statement is too
general. Fortunately, it can easily be specialized:
-transfer the additional premise @{prop"(y,z):r*"} into the conclusion:\<close>
+transfer the additional premise @{prop"(y,z)\<in>r*"} into the conclusion:\<close>
(*<*)oops(*>*)
lemma rtc_trans[rule_format]:
"(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
@@ -157,7 +157,7 @@
\begin{exercise}\label{ex:converse-rtc-step}
Show that the converse of @{thm[source]rtc_step} also holds:
-@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
+@{prop[display]"[| (x,y) \<in> r*; (y,z) \<in> r |] ==> (x,z) \<in> r*"}
\end{exercise}
\begin{exercise}
Repeat the development of this section, but starting with a definition of
@@ -166,7 +166,7 @@
\end{exercise}
\<close>
(*<*)
-lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
+lemma rtc_step2[rule_format]: "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r \<longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)
apply blast
apply(blast intro: rtc_step)
--- a/src/Doc/Tutorial/Misc/Plus.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Misc/Plus.thy Thu Feb 15 13:04:36 2018 +0100
@@ -10,7 +10,7 @@
text\<open>\noindent and prove\<close>
(*<*)
-lemma [simp]: "!m. add m n = m+n"
+lemma [simp]: "\<forall>m. add m n = m+n"
apply(induct_tac n)
by(auto)
(*>*)
--- a/src/Doc/Tutorial/Misc/Tree2.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Misc/Tree2.thy Thu Feb 15 13:04:36 2018 +0100
@@ -14,7 +14,7 @@
text\<open>\noindent and prove\<close>
(*<*)
-lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs"
+lemma [simp]: "\<forall>xs. flatten2 t xs = flatten t @ xs"
apply(induct_tac t)
by(auto)
(*>*)
--- a/src/Doc/Tutorial/Misc/prime_def.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Misc/prime_def.thy Thu Feb 15 13:04:36 2018 +0100
@@ -7,12 +7,12 @@
A common mistake when writing definitions is to introduce extra free
variables on the right-hand side. Consider the following, flawed definition
(where @{text"dvd"} means ``divides''):
-@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
+@{term[display,quotes]"prime(p) \<equiv> 1 < p \<and> (m dvd p \<longrightarrow> (m=1 \<or> m=p))"}
\par\noindent\hangindent=0pt
Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
right-hand side, which would introduce an inconsistency (why?).
The correct version is
-@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
+@{term[display,quotes]"prime(p) \<equiv> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> (m=1 \<or> m=p))"}
\end{warn}
\<close>
(*<*)
--- a/src/Doc/Tutorial/Protocol/Event.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy Thu Feb 15 13:04:36 2018 +0100
@@ -12,7 +12,7 @@
theory Event imports Message begin
consts (*Initial states of agents -- parameter of the construction*)
- initState :: "agent => msg set"
+ initState :: "agent \<Rightarrow> msg set"
datatype
event = Says agent agent msg
@@ -26,28 +26,28 @@
text\<open>The constant "spies" is retained for compatibility's sake\<close>
primrec
- knows :: "agent => event list => msg set"
+ knows :: "agent \<Rightarrow> event list \<Rightarrow> msg set"
where
knows_Nil: "knows A [] = initState A"
| knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
- Says A' B X => insert X (knows Spy evs)
- | Gets A' X => knows Spy evs
- | Notes A' X =>
+ Says A' B X \<Rightarrow> insert X (knows Spy evs)
+ | Gets A' X \<Rightarrow> knows Spy evs
+ | Notes A' X \<Rightarrow>
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
else
(case ev of
- Says A' B X =>
+ Says A' B X \<Rightarrow>
if A'=A then insert X (knows A evs) else knows A evs
- | Gets A' X =>
+ | Gets A' X \<Rightarrow>
if A'=A then insert X (knows A evs) else knows A evs
- | Notes A' X =>
+ | Notes A' X \<Rightarrow>
if A'=A then insert X (knows A evs) else knows A evs))"
abbreviation (input)
- spies :: "event list => msg set" where
+ spies :: "event list \<Rightarrow> msg set" where
"spies == knows Spy"
text\<open>Spy has access to his own key for spoof messages, but Server is secure\<close>
@@ -65,24 +65,24 @@
primrec
(*Set of items that might be visible to somebody:
complement of the set of fresh items*)
- used :: "event list => msg set"
+ used :: "event list \<Rightarrow> msg set"
where
used_Nil: "used [] = (UN B. parts (initState B))"
| used_Cons: "used (ev # evs) =
(case ev of
- Says A B X => parts {X} \<union> used evs
- | Gets A X => used evs
- | Notes A X => parts {X} \<union> used evs)"
+ Says A B X \<Rightarrow> parts {X} \<union> used evs
+ | Gets A X \<Rightarrow> used evs
+ | Notes A X \<Rightarrow> parts {X} \<union> used evs)"
\<comment> \<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
follows @{term Says} in real protocols. Seems difficult to change.
See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}.\<close>
-lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
+lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
apply (induct_tac evs)
apply (auto split: event.split)
done
-lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
+lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> used evs"
apply (induct_tac evs)
apply (auto split: event.split)
done
@@ -103,7 +103,7 @@
on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}\<close>
lemma knows_Spy_Notes [simp]:
"knows Spy (Notes A X # evs) =
- (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
+ (if A\<in>bad then insert X (knows Spy evs) else knows Spy evs)"
by simp
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
@@ -123,13 +123,13 @@
text\<open>Spy sees what is sent on the traffic\<close>
lemma Says_imp_knows_Spy [rule_format]:
- "Says A B X \<in> set evs --> X \<in> knows Spy evs"
+ "Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
done
lemma Notes_imp_knows_Spy [rule_format]:
- "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
+ "Notes A X \<in> set evs \<longrightarrow> A \<in> bad \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
done
@@ -158,7 +158,7 @@
by simp
lemma knows_Gets:
- "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
+ "A \<noteq> Spy \<longrightarrow> knows A (Gets A X # evs) = insert X (knows A evs)"
by simp
@@ -172,14 +172,14 @@
by (simp add: subset_insertI)
text\<open>Agents know what they say\<close>
-lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
+lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
text\<open>Agents know what they note\<close>
-lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
+lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
apply blast
@@ -187,7 +187,7 @@
text\<open>Agents know what they receive\<close>
lemma Gets_imp_knows_agents [rule_format]:
- "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
+ "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
done
@@ -196,8 +196,8 @@
text\<open>What agents DIFFERENT FROM Spy know
was either said, or noted, or got, or known initially\<close>
lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
- "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.
- Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
+ "[| X \<in> knows A evs; A \<noteq> Spy |] ==> \<exists>B.
+ Says A B X \<in> set evs \<or> Gets A X \<in> set evs \<or> Notes A X \<in> set evs \<or> X \<in> initState A"
apply (erule rev_mp)
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
@@ -207,8 +207,8 @@
text\<open>What the Spy knows -- for the time being --
was either said or noted, or known initially\<close>
lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
- "[| X \<in> knows Spy evs |] ==> EX A B.
- Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
+ "[| X \<in> knows Spy evs |] ==> \<exists>A B.
+ Says A B X \<in> set evs \<or> Notes A X \<in> set evs \<or> X \<in> initState Spy"
apply (erule rev_mp)
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
@@ -222,7 +222,7 @@
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
-lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
+lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs"
apply (induct_tac "evs")
apply (simp_all add: parts_insert_knows_A split: event.split, blast)
done
@@ -246,7 +246,7 @@
used_Nil [simp del] used_Cons [simp del]
-text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
+text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) \<longrightarrow> P"}
New events added by induction to "evs" are discarded. Provided
this information isn't needed, the proof will be much shorter, since
it will omit complicated reasoning about @{term analz}.\<close>
@@ -286,7 +286,7 @@
method_setup analz_mono_contra = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\<close>
- "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
+ "for proving theorems of the form X \<notin> analz (knows Spy evs) \<longrightarrow> P"
subsubsection\<open>Useful for case analysis on whether a hash is a spoof or not\<close>
@@ -343,7 +343,7 @@
method_setup synth_analz_mono_contra = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt)))\<close>
- "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
+ "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) \<longrightarrow> P"
(*>*)
section\<open>Event Traces \label{sec:events}\<close>
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Thu Feb 15 13:04:36 2018 +0100
@@ -39,7 +39,7 @@
specification (invKey)
invKey [simp]: "invKey (invKey K) = K"
- invKey_symmetric: "all_symmetric --> invKey = id"
+ invKey_symmetric: "all_symmetric \<longrightarrow> invKey = id"
by (rule exI [of _ id], auto)
@@ -81,13 +81,13 @@
(*<*)
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
-definition keysFor :: "msg set => key set" where
+definition keysFor :: "msg set \<Rightarrow> key set" where
\<comment> \<open>Keys useful to decrypt elements of a message set\<close>
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
@@ -95,17 +95,17 @@
subsubsection\<open>Inductive Definition of All Parts" of a Message\<close>
inductive_set
- parts :: "msg set => msg set"
+ parts :: "msg set \<Rightarrow> msg set"
for H :: "msg set"
where
- Inj [intro]: "X \<in> H ==> X \<in> parts H"
- | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
- | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
- | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
+ Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> parts H"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H \<Longrightarrow> X \<in> parts H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H \<Longrightarrow> Y \<in> parts H"
+ | Body: "Crypt K X \<in> parts H \<Longrightarrow> X \<in> parts H"
text\<open>Monotonicity\<close>
-lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
+lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts(G) \<subseteq> parts(H)"
apply auto
apply (erule parts.induct)
apply (blast dest: parts.Fst parts.Snd parts.Body)+
@@ -113,7 +113,7 @@
text\<open>Equations hold because constructors are injective.\<close>
-lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
+lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x\<in>A)"
by auto
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
@@ -143,7 +143,7 @@
by (unfold keysFor_def, blast)
text\<open>Monotonicity\<close>
-lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)"
+lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor(G) \<subseteq> keysFor(H)"
by (unfold keysFor_def, blast)
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
@@ -165,7 +165,7 @@
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
by (unfold keysFor_def, auto)
-lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H"
+lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H"
by (unfold keysFor_def, blast)
@@ -192,11 +192,11 @@
apply (erule parts.induct, blast+)
done
-lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P"
+lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P"
by simp
text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close>
-lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}"
+lemma parts_singleton: "X\<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X\<in> parts {Y}"
by (erule parts.induct, fast+)
@@ -252,7 +252,7 @@
subsubsection\<open>Idempotence and transitivity\<close>
-lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H"
+lemma parts_partsD [dest!]: "X \<in> parts (parts H) \<Longrightarrow> X\<in> parts H"
by (erule parts.induct, blast+)
lemma parts_idem [simp]: "parts (parts H) = parts H"
@@ -324,7 +324,7 @@
text\<open>In any message, there is an upper bound N on its greatest nonce.\<close>
-lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
+lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> parts {msg}"
apply (induct_tac "msg")
apply (simp_all (no_asm_simp) add: exI parts_insert2)
txt\<open>MPair case: blast works out the necessary sum itself!\<close>
@@ -363,7 +363,7 @@
\<Longrightarrow> X \<in> analz H"
(*<*)
text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close>
-lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)"
+lemma analz_mono: "G\<subseteq>H \<Longrightarrow> analz(G) \<subseteq> analz(H)"
apply auto
apply (erule analz.induct)
apply (auto dest: analz.Fst analz.Snd)
@@ -435,7 +435,7 @@
text\<open>Can only pull out Keys if they are not needed to decrypt the rest\<close>
lemma analz_insert_Key [simp]:
- "K \<notin> keysFor (analz H) ==>
+ "K \<notin> keysFor (analz H) \<Longrightarrow>
analz (insert (Key K) H) = insert (Key K) (analz H)"
apply (unfold keysFor_def)
apply (rule analz_insert_eq_I)
@@ -455,20 +455,20 @@
text\<open>Can pull out enCrypted message if the Key is not known\<close>
lemma analz_insert_Crypt:
"Key (invKey K) \<notin> analz H
- ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
+ \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)"
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
-lemma lemma1: "Key (invKey K) \<in> analz H ==>
+lemma lemma1: "Key (invKey K) \<in> analz H \<Longrightarrow>
analz (insert (Crypt K X) H) \<subseteq>
insert (Crypt K X) (analz (insert X H))"
apply (rule subsetI)
apply (erule_tac x = x in analz.induct, auto)
done
-lemma lemma2: "Key (invKey K) \<in> analz H ==>
+lemma lemma2: "Key (invKey K) \<in> analz H \<Longrightarrow>
insert (Crypt K X) (analz (insert X H)) \<subseteq>
analz (insert (Crypt K X) H)"
apply auto
@@ -477,7 +477,7 @@
done
lemma analz_insert_Decrypt:
- "Key (invKey K) \<in> analz H ==>
+ "Key (invKey K) \<in> analz H \<Longrightarrow>
analz (insert (Crypt K X) H) =
insert (Crypt K X) (analz (insert X H))"
by (intro equalityI lemma1 lemma2)
@@ -511,7 +511,7 @@
subsubsection\<open>Idempotence and transitivity\<close>
-lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H"
+lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X\<in> analz H"
by (erule analz.induct, blast+)
lemma analz_idem [simp]: "analz (analz H) = analz H"
@@ -531,13 +531,13 @@
by (erule analz_trans, blast)
(*Cut can be proved easily by induction on
- "Y: analz (insert X H) ==> X: analz H --> Y: analz H"
+ "Y \<in> analz (insert X H) \<Longrightarrow> X \<in> analz H \<longrightarrow> Y \<in> analz H"
*)
text\<open>This rewrite rule helps in the simplification of messages that involve
the forwarding of unknown components (X). Without it, removing occurrences
of X can be very complicated.\<close>
-lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H"
+lemma analz_insert_eq: "X\<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
by (blast intro: analz_cut analz_insertI)
@@ -556,7 +556,7 @@
by (intro equalityI analz_subset_cong, simp_all)
lemma analz_insert_cong:
- "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"
+ "analz H = analz H' \<Longrightarrow> analz(insert X H) = analz(insert X H')"
by (force simp only: insert_def intro!: analz_cong)
text\<open>If there are no pairs or encryptions then analz does nothing\<close>
@@ -568,7 +568,7 @@
text\<open>These two are obsolete (with a single Spy) but cost little to prove...\<close>
lemma analz_UN_analz_lemma:
- "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
+ "X\<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X\<in> analz (\<Union>i\<in>A. H i)"
apply (erule analz.induct)
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
done
@@ -598,7 +598,7 @@
| Crypt [intro]:
"\<lbrakk>X \<in> synth H; Key K \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
(*<*)
-lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
+lemma synth_mono: "G\<subseteq>H \<Longrightarrow> synth(G) \<subseteq> synth(H)"
by (auto, erule synth.induct, auto)
inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
@@ -668,7 +668,7 @@
subsubsection\<open>Idempotence and transitivity\<close>
-lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
+lemma synth_synthD [dest!]: "X\<in> synth (synth H) \<Longrightarrow> X\<in> synth H"
by (erule synth.induct, blast+)
lemma synth_idem: "synth (synth H) = synth H"
@@ -697,7 +697,7 @@
by blast
lemma Crypt_synth_eq [simp]:
- "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
+ "Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)"
by blast
@@ -724,13 +724,13 @@
subsubsection\<open>For reasoning about the Fake rule in traces\<close>
-lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
+lemma parts_insert_subset_Un: "X \<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H"
by (rule subset_trans [OF parts_mono parts_Un_subset2], blast)
text\<open>More specifically for Fake. Very occasionally we could do with a version
of the form @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"}\<close>
lemma Fake_parts_insert:
- "X \<in> synth (analz H) ==>
+ "X \<in> synth (analz H) \<Longrightarrow>
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
apply (drule parts_insert_subset_Un)
apply (simp (no_asm_use))
@@ -738,14 +738,14 @@
done
lemma Fake_parts_insert_in_Un:
- "[|Z \<in> parts (insert X H); X: synth (analz H)|]
+ "[|Z \<in> parts (insert X H); X \<in> synth (analz H)|]
==> Z \<in> synth (analz H) \<union> parts H"
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
text\<open>@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put
@{term "G=H"}.\<close>
lemma Fake_analz_insert:
- "X\<in> synth (analz G) ==>
+ "X \<in> synth (analz G) \<Longrightarrow>
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
apply (rule subsetI)
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
@@ -869,11 +869,11 @@
lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A"
by auto
-lemma synth_analz_mono: "G\<subseteq>H ==> synth (analz(G)) \<subseteq> synth (analz(H))"
+lemma synth_analz_mono: "G\<subseteq>H \<Longrightarrow> synth (analz(G)) \<subseteq> synth (analz(H))"
by (iprover intro: synth_mono analz_mono)
lemma Fake_analz_eq [simp]:
- "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
+ "X \<in> synth(analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)"
apply (drule Fake_analz_insert[of _ _ "H"])
apply (simp add: synth_increasing[THEN Un_absorb2])
apply (drule synth_mono)
@@ -885,18 +885,18 @@
text\<open>Two generalizations of @{text analz_insert_eq}\<close>
lemma gen_analz_insert_eq [rule_format]:
- "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
+ "X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
lemma synth_analz_insert_eq [rule_format]:
"X \<in> synth (analz H)
- ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
+ \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
apply (erule synth.induct)
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
done
lemma Fake_parts_sing:
- "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
+ "X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H"
apply (rule subset_trans)
apply (erule_tac [2] Fake_parts_insert)
apply (rule parts_mono, blast)
--- a/src/Doc/Tutorial/Protocol/Public.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Public.thy Thu Feb 15 13:04:36 2018 +0100
@@ -32,7 +32,7 @@
| initState_Friend: "initState (Friend i) =
insert (Key (priK (Friend i))) (Key ` range pubK)"
| initState_Spy: "initState Spy =
- (Key`invKey`pubK`bad) Un (Key ` range pubK)"
+ (Key`invKey`pubK`bad) \<union> (Key ` range pubK)"
end
(*>*)
@@ -77,14 +77,14 @@
(** "Image" equations that hold for injective functions **)
-lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)"
+lemma invKey_image_eq[simp]: "(invKey x \<in> invKey`A) = (x\<in>A)"
by auto
(*holds because invKey is injective*)
-lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)"
+lemma pubK_image_eq[simp]: "(pubK x \<in> pubK`A) = (x\<in>A)"
by auto
-lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)"
+lemma priK_pubK_image_eq[simp]: "(priK x \<notin> pubK`A)"
by auto
@@ -101,15 +101,15 @@
(*** Function "spies" ***)
(*Agents see their own private keys!*)
-lemma priK_in_initState[iff]: "Key (priK A) : initState A"
+lemma priK_in_initState[iff]: "Key (priK A) \<in> initState A"
by (induct A) auto
(*All public keys are visible*)
-lemma spies_pubK[iff]: "Key (pubK A) : spies evs"
+lemma spies_pubK[iff]: "Key (pubK A) \<in> spies evs"
by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
(*Spy sees private keys of bad agents!*)
-lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs"
+lemma Spy_spies_bad[intro!]: "A \<in> bad \<Longrightarrow> Key (priK A) \<in> spies evs"
by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
lemmas [iff] = spies_pubK [THEN analz.Inj]
@@ -117,17 +117,17 @@
(*** Fresh nonces ***)
-lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)"
+lemma Nonce_notin_initState[iff]: "Nonce N \<notin> parts (initState B)"
by (induct B) auto
-lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []"
+lemma Nonce_notin_used_empty[simp]: "Nonce N \<notin> used []"
by (simp add: used_Nil)
(*** Supply fresh nonces for possibility theorems. ***)
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
+lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
@@ -135,10 +135,10 @@
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done
-lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
+lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
by (rule Nonce_supply_lemma [THEN exE], blast)
-lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
+lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs"
apply (rule Nonce_supply_lemma [THEN exE])
apply (rule someI, fast)
done
@@ -146,10 +146,10 @@
(*** Specialized rewriting for the analz_image_... theorems ***)
-lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
+lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
by blast
-lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
+lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
by blast
--- a/src/Doc/Tutorial/Rules/TPrimes.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Rules/TPrimes.thy Thu Feb 15 13:04:36 2018 +0100
@@ -96,7 +96,7 @@
definition is_gcd :: "[nat,nat,nat] \<Rightarrow> bool" where (*gcd as a relation*)
"is_gcd p m n == p dvd m \<and> p dvd n \<and>
- (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
+ (\<forall>d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
(*Function gcd yields the Greatest Common Divisor*)
lemma is_gcd: "is_gcd (gcd m n) m n"
--- a/src/Doc/Tutorial/Sets/Examples.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/Doc/Tutorial/Sets/Examples.thy Thu Feb 15 13:04:36 2018 +0100
@@ -155,7 +155,7 @@
by blast
definition prime :: "nat set" where
- "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
+ "prime == {p. 1<p & (\<forall>m. m dvd p \<longrightarrow> m=1 \<or> m=p)}"
lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} =
{z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
--- a/src/HOL/Algebra/AbelCoset.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Thu Feb 15 13:04:36 2018 +0100
@@ -554,7 +554,7 @@
..
lemma (in abelian_group_hom) hom_add [simp]:
- "[| x : carrier G; y : carrier G |]
+ "[| x \<in> carrier G; y \<in> carrier G |]
==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
by (rule group_hom.hom_mult[OF a_group_hom,
simplified ring_record_simps])
--- a/src/HOL/Algebra/FiniteProduct.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Thu Feb 15 13:04:36 2018 +0100
@@ -22,7 +22,7 @@
for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a
where
emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e"
- | insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
+ | insertI [intro]: "[| x \<notin> A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
(insert x A, f x y) \<in> foldSetD D f e"
inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
@@ -178,7 +178,7 @@
done
lemma (in LCD) foldD_insert:
- "[| finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
+ "[| finite A; x \<notin> A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
foldD D f e (insert x A) = f x (foldD D f e A)"
apply (unfold foldD_def)
apply (simp add: foldD_insert_aux)
@@ -423,13 +423,13 @@
proof (intro finprod_insert)
show "finite B" by fact
next
- show "x ~: B" by fact
+ show "x \<notin> B" by fact
next
- assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+ assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
thus "f \<in> B \<rightarrow> carrier G" by fastforce
next
- assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+ assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
thus "f x \<in> carrier G" by fastforce
qed
@@ -491,8 +491,8 @@
(* The following two were contributed by Jeremy Avigad. *)
lemma finprod_reindex:
- "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow>
- inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
+ "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow>
+ inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A"
proof (induct A rule: infinite_finite_induct)
case (infinite A)
hence "\<not> finite (h ` A)"
@@ -501,8 +501,8 @@
qed (auto simp add: Pi_def)
lemma finprod_const:
- assumes a [simp]: "a : carrier G"
- shows "finprod G (%x. a) A = a [^] card A"
+ assumes a [simp]: "a \<in> carrier G"
+ shows "finprod G (\<lambda>x. a) A = a [^] card A"
proof (induct A rule: infinite_finite_induct)
case (insert b A)
show ?case
--- a/src/HOL/Algebra/Group.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/Group.thy Thu Feb 15 13:04:36 2018 +0100
@@ -435,7 +435,7 @@
"x \<in> carrier G \<Longrightarrow> x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
proof -
have [simp]: "-i - j = -j - i" by simp
- assume "x : carrier G" then
+ assume "x \<in> carrier G" then
show ?thesis
by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
qed
--- a/src/HOL/Algebra/Order.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/Order.thy Thu Feb 15 13:04:36 2018 +0100
@@ -379,7 +379,7 @@
proof -
have "Upper L A \<subseteq> carrier L" by simp
moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
- moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
+ moreover from below have "\<forall>x \<in> Upper L A. s \<sqsubseteq> x" by fast
ultimately show ?thesis by (simp add: least_def)
qed
@@ -439,7 +439,7 @@
proof -
have "Lower L A \<subseteq> carrier L" by simp
moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
- moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
+ moreover from above have "\<forall>x \<in> Lower L A. x \<sqsubseteq> i" by fast
ultimately show ?thesis by (simp add: greatest_def)
qed
--- a/src/HOL/Algebra/Ring.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/Ring.thy Thu Feb 15 13:04:36 2018 +0100
@@ -74,7 +74,7 @@
and a_comm:
"!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
and l_zero: "!!x. x \<in> carrier R ==> \<zero> \<oplus> x = x"
- and l_inv_ex: "!!x. x \<in> carrier R ==> EX y : carrier R. y \<oplus> x = \<zero>"
+ and l_inv_ex: "\<And>x. x \<in> carrier R \<Longrightarrow> \<exists>y \<in> carrier R. y \<oplus> x = \<zero>"
shows "abelian_group R"
by (auto intro!: abelian_group.intro abelian_monoidI
abelian_group_axioms.intro comm_monoidI comm_groupI
--- a/src/HOL/Algebra/RingHom.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/RingHom.thy Thu Feb 15 13:04:36 2018 +0100
@@ -39,8 +39,8 @@
assumes "ring R" "ring S"
assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
- and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
- and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
+ and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
+ and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
proof -
@@ -72,7 +72,7 @@
lemma ring_hom_ringI3:
fixes R (structure) and S (structure)
assumes "abelian_group_hom R S h" "ring R" "ring S"
- assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
+ assumes compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
proof -
--- a/src/HOL/Algebra/Sylow.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/Sylow.thy Thu Feb 15 13:04:36 2018 +0100
@@ -257,7 +257,7 @@
lemmas H_elem_map_eq = H_elem_map [THEN someI_ex, THEN conjunct2]
lemma rcosets_H_funcset_M:
- "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
+ "(\<lambda>C \<in> rcosets H. M1 #> (SOME g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
apply (simp add: RCOSETS_def)
apply (fast intro: someI2
intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
--- a/src/HOL/Algebra/UnivPoly.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Feb 15 13:04:36 2018 +0100
@@ -284,7 +284,7 @@
lemma UP_l_neg_ex:
assumes R: "p \<in> carrier P"
- shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
+ shows "\<exists>q \<in> carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
proof -
let ?q = "\<lambda>i. \<ominus> (p i)"
from R have closed: "?q \<in> carrier P"
--- a/src/HOL/Analysis/Arcwise_Connected.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Thu Feb 15 13:04:36 2018 +0100
@@ -21,12 +21,12 @@
where "inj B" "\<And>n. open(B n)" and open_cov: "\<And>S. open S \<Longrightarrow> \<exists>K. S = \<Union>(B ` K)"
by (metis Setcompr_eq_image that univ_second_countable_sequence)
define A where "A \<equiv> rec_nat S (\<lambda>n a. if \<exists>U. U \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
- then @U. U \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
+ then SOME U. U \<subseteq> a \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
else a)"
have [simp]: "A 0 = S"
by (simp add: A_def)
have ASuc: "A(Suc n) = (if \<exists>U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
- then @U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
+ then SOME U. U \<subseteq> A n \<and> closed U \<and> \<phi> U \<and> U \<inter> (B n) = {}
else A n)" for n
by (auto simp: A_def)
have sub: "\<And>n. A(Suc n) \<subseteq> A n"
@@ -1801,7 +1801,7 @@
and peq: "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; open_segment x y \<inter> T = {}\<rbrakk> \<Longrightarrow> p x = p y"
unfolding \<phi>_def by metis+
then have "T \<noteq> {}" by auto
- define h where "h \<equiv> \<lambda>x. p(@y. y \<in> T \<and> open_segment x y \<inter> T = {})"
+ define h where "h \<equiv> \<lambda>x. p(SOME y. y \<in> T \<and> open_segment x y \<inter> T = {})"
have "p y = p z" if "y \<in> T" "z \<in> T" and xyT: "open_segment x y \<inter> T = {}" and xzT: "open_segment x z \<inter> T = {}"
for x y z
proof (cases "x \<in> T")
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Feb 15 13:04:36 2018 +0100
@@ -714,9 +714,9 @@
where "f contour_integrable_on g \<equiv> \<exists>i. (f has_contour_integral i) g"
definition contour_integral
- where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g \<or> ~ f contour_integrable_on g \<and> i=0"
-
-lemma not_integrable_contour_integral: "~ f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0"
+ where "contour_integral g f \<equiv> SOME i. (f has_contour_integral i) g \<or> \<not> f contour_integrable_on g \<and> i=0"
+
+lemma not_integrable_contour_integral: "\<not> f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0"
unfolding contour_integrable_on_def contour_integral_def by blast
lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i"
@@ -3327,7 +3327,7 @@
definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where
"winding_number \<gamma> z \<equiv>
- @n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
+ SOME n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
pathstart p = pathstart \<gamma> \<and>
pathfinish p = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
--- a/src/HOL/Analysis/Continuous_Extension.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy Thu Feb 15 13:04:36 2018 +0100
@@ -309,7 +309,7 @@
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (cases "S = {}")
case True then show thesis
- apply (rule_tac g="\<lambda>x. @y. y \<in> C" in that)
+ apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
apply (rule continuous_intros)
apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
done
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Feb 15 13:04:36 2018 +0100
@@ -1944,7 +1944,7 @@
using \<open>u + v = 1\<close> by auto
ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S"
using h1 by auto
- then have "u *\<^sub>R x + v *\<^sub>R y : S" by auto
+ then have "u *\<^sub>R x + v *\<^sub>R y \<in> S" by auto
}
then show ?thesis unfolding affine_def by auto
qed
@@ -2031,7 +2031,7 @@
have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
have "affine ((\<lambda>x. (-a)+x) ` S)"
using affine_translation assms by auto
- moreover have "0 : ((\<lambda>x. (-a)+x) ` S)"
+ moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
ultimately show ?thesis using subspace_affine by auto
qed
@@ -2130,7 +2130,7 @@
lemma mem_cone:
assumes "cone S" "x \<in> S" "c \<ge> 0"
- shows "c *\<^sub>R x : S"
+ shows "c *\<^sub>R x \<in> S"
using assms cone_def[of S] by auto
lemma cone_contains_0:
@@ -3409,7 +3409,7 @@
assumes "a \<notin> S"
shows "affine_dependent (insert a S) \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` S)"
proof -
- have "((+) (- a) ` S) = {x - a| x . x : S}" by auto
+ have "((+) (- a) ` S) = {x - a| x . x \<in> S}" by auto
then show ?thesis
using affine_dependent_translation_eq[of "(insert a S)" "-a"]
affine_dependent_imp_dependent2 assms
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Feb 15 13:04:36 2018 +0100
@@ -1324,7 +1324,7 @@
using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
done
have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
- proof (rule measure_mono_fmeasurable [OF _ _ \<open>T : lmeasurable\<close>])
+ proof (rule measure_mono_fmeasurable [OF _ _ \<open>T \<in> lmeasurable\<close>])
show "(\<Union>\<D>') \<in> sets lebesgue"
using div lmeasurable_division by auto
have "\<Union>\<D>' \<subseteq> \<Union>\<D>"
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Feb 15 13:04:36 2018 +0100
@@ -159,7 +159,7 @@
then obtain b where b: "Inf S - e < b" "b < Inf S"
using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"]
by auto
- then have "b: {Inf S - e <..< Inf S + e}"
+ then have "b \<in> {Inf S - e <..< Inf S + e}"
using e fin ereal_between[of "Inf S" e]
by auto
then have "b \<in> S"
--- a/src/HOL/Analysis/Polytope.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy Thu Feb 15 13:04:36 2018 +0100
@@ -3201,7 +3201,7 @@
finite \<C> \<and>
(\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
(\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
- (!S S'. S \<in> \<C> \<and> S' \<in> \<C>
+ (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
\<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
definition triangulation where
@@ -3350,7 +3350,7 @@
and convex\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> convex C"
and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
- have in_rel_interior: "(@z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
+ have in_rel_interior: "(SOME z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
have *: "\<exists>T. ~affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
if "K \<in> \<U>" for K
@@ -3396,7 +3396,7 @@
by fastforce
qed
let ?\<T> = "(\<Union>C \<in> \<N>. \<Union>K \<in> \<U> \<inter> Pow (rel_frontier C).
- {convex hull (insert (@z. z \<in> rel_interior C) K)})"
+ {convex hull (insert (SOME z. z \<in> rel_interior C) K)})"
have "\<exists>\<T>. simplicial_complex \<T> \<and>
(\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
(\<forall>C \<in> \<M>. \<exists>F. F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
@@ -3415,9 +3415,9 @@
using S face\<U> that by blast
moreover have "F \<in> \<U> \<union> ?\<T>"
if "F face_of S" "C \<in> \<N>" "K \<in> \<U>" and "K \<subseteq> rel_frontier C"
- and S: "S = convex hull insert (@z. z \<in> rel_interior C) K" for C K
+ and S: "S = convex hull insert (SOME z. z \<in> rel_interior C) K" for C K
proof -
- let ?z = "@z. z \<in> rel_interior C"
+ let ?z = "SOME z. z \<in> rel_interior C"
have "?z \<in> rel_interior C"
by (simp add: in_rel_interior \<open>C \<in> \<N>\<close>)
moreover
@@ -3490,13 +3490,13 @@
proof -
obtain C K
where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
- and Y: "Y = convex hull insert (@z. z \<in> rel_interior C) K"
+ and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
using XY by blast
have "convex C"
by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
have "K \<subseteq> C"
by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
- let ?z = "(@z. z \<in> rel_interior C)"
+ let ?z = "(SOME z. z \<in> rel_interior C)"
have z: "?z \<in> rel_interior C"
using \<open>C \<in> \<N>\<close> in_rel_interior by blast
obtain D where "D \<in> \<S>" "X \<subseteq> D"
@@ -3533,11 +3533,11 @@
proof -
obtain C K D L
where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
- and X: "X = convex hull insert (@z. z \<in> rel_interior C) K"
+ and X: "X = convex hull insert (SOME z. z \<in> rel_interior C) K"
and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
- and Y: "Y = convex hull insert (@z. z \<in> rel_interior D) L"
+ and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior D) L"
using XY by blast
- let ?z = "(@z. z \<in> rel_interior C)"
+ let ?z = "(SOME z. z \<in> rel_interior C)"
have z: "?z \<in> rel_interior C"
using \<open>C \<in> \<N>\<close> in_rel_interior by blast
have "convex C"
@@ -3564,7 +3564,7 @@
by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
have "L \<subseteq> D"
by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
- let ?w = "(@w. w \<in> rel_interior D)"
+ let ?w = "(SOME w. w \<in> rel_interior D)"
have w: "?w \<in> rel_interior D"
using \<open>D \<in> \<N>\<close> in_rel_interior by blast
have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
@@ -3663,7 +3663,7 @@
case False
then have "C \<in> \<N>"
by (simp add: \<N>_def \<S>_def aff\<M> less_le that)
- let ?z = "@z. z \<in> rel_interior C"
+ let ?z = "SOME z. z \<in> rel_interior C"
have z: "?z \<in> rel_interior C"
using \<open>C \<in> \<N>\<close> in_rel_interior by blast
let ?F = "\<Union>K \<in> \<U> \<inter> Pow (rel_frontier C). {convex hull (insert ?z K)}"
@@ -3726,7 +3726,7 @@
next
assume "L \<in> ?\<T>"
then obtain C K where "C \<in> \<N>"
- and L: "L = convex hull insert (@z. z \<in> rel_interior C) K"
+ and L: "L = convex hull insert (SOME z. z \<in> rel_interior C) K"
and K: "K \<in> \<U>" "K \<subseteq> rel_frontier C"
by auto
then have "convex hull C = C"
--- a/src/HOL/Analysis/Starlike.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Thu Feb 15 13:04:36 2018 +0100
@@ -1272,7 +1272,7 @@
fix x :: "'a::euclidean_space"
fix u
assume as: "\<forall>x\<in>?D. 0 \<le> u x" "sum u ?D \<le> 1" "(\<Sum>x\<in>?D. u x *\<^sub>R x) = x"
- have *: "\<forall>i\<in>Basis. i:d \<longrightarrow> u i = x\<bullet>i"
+ have *: "\<forall>i\<in>Basis. i \<in> d \<longrightarrow> u i = x\<bullet>i"
and "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
using as(3)
unfolding substdbasis_expansion_unique[OF assms]
@@ -1590,7 +1590,7 @@
case True
have "norm (x - y) < x\<bullet>i"
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
- using Min_gr_iff[of "(\<bullet>) x ` d" "norm (x - y)"] \<open>0 < card d\<close> \<open>i:d\<close>
+ using Min_gr_iff[of "(\<bullet>) x ` d" "norm (x - y)"] \<open>0 < card d\<close> \<open>i \<in> d\<close>
by (simp add: card_gt_0_iff)
then show "0 \<le> y\<bullet>i"
using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
@@ -1833,7 +1833,7 @@
then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (x - a) \<le> e"
using \<open>x \<noteq> a\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (x - a)"]
by simp_all
- then have *: "x - e1 *\<^sub>R (x - a) : rel_interior S"
+ then have *: "x - e1 *\<^sub>R (x - a) \<in> rel_interior S"
using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
by auto
have "\<exists>y. y \<in> rel_interior S \<and> y \<noteq> x \<and> dist y x \<le> e"
@@ -2442,11 +2442,11 @@
subsubsection \<open>Relative interior and closure under common operations\<close>
-lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S : I} \<subseteq> \<Inter>I"
+lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S \<in> I} \<subseteq> \<Inter>I"
proof -
{
fix y
- assume "y \<in> \<Inter>{rel_interior S |S. S : I}"
+ assume "y \<in> \<Inter>{rel_interior S |S. S \<in> I}"
then have y: "\<forall>S \<in> I. y \<in> rel_interior S"
by auto
{
@@ -2824,13 +2824,13 @@
fix x
assume "x \<in> f ` S"
then obtain x1 where x1: "x1 \<in> S" "f x1 = x" by auto
- then obtain e where e: "e > 1" "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1 : S"
+ then obtain e where e: "e > 1" "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1 \<in> S"
using convex_rel_interior_iff[of S z1] \<open>convex S\<close> x1 z1 by auto
moreover have "f ((1 - e) *\<^sub>R x1 + e *\<^sub>R z1) = (1 - e) *\<^sub>R x + e *\<^sub>R z"
using x1 z1 \<open>linear f\<close> by (simp add: linear_add_cmul)
- ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S"
+ ultimately have "(1 - e) *\<^sub>R x + e *\<^sub>R z \<in> f ` S"
using imageI[of "(1 - e) *\<^sub>R x1 + e *\<^sub>R z1" S f] by auto
- then have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z : f ` S"
+ then have "\<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> f ` S"
using e by auto
}
then have "z \<in> rel_interior (f ` S)"
@@ -2861,7 +2861,7 @@
{
fix z
assume "z \<in> f -` (rel_interior S)"
- then have z: "f z : rel_interior S"
+ then have z: "f z \<in> rel_interior S"
by auto
{
fix x
@@ -3115,7 +3115,7 @@
by (metis Domain_iff fst_eq_Domain)
then have "y \<in> rel_interior {t. f t \<noteq> {}}"
using h1 by auto
- then have "y \<in> rel_interior {t. f t \<noteq> {}}" and "(z : rel_interior (f y))"
+ then have "y \<in> rel_interior {t. f t \<noteq> {}}" and "(z \<in> rel_interior (f y))"
using h2 asm by auto
}
then show ?thesis using h2 by blast
@@ -3238,7 +3238,7 @@
have "?lhs \<supseteq> ?rhs"
proof
fix x
- assume "x : ?rhs"
+ assume "x \<in> ?rhs"
then obtain c s where *: "sum (\<lambda>i. c i *\<^sub>R s i) I = x" "sum c I = 1"
"(\<forall>i\<in>I. c i \<ge> 0) \<and> (\<forall>i\<in>I. s i \<in> S i)" by auto
then have "\<forall>i\<in>I. s i \<in> convex hull (\<Union>(S ` I))"
@@ -3676,7 +3676,7 @@
by auto
define k where "k i = (c i, c i *\<^sub>R s i)" for i
{
- fix i assume "i:I"
+ fix i assume "i \<in> I"
then have "k i \<in> rel_interior (K i)"
using k_def K_def assms cs rel_interior_convex_cone[of "S i"]
by auto
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Feb 15 13:04:36 2018 +0100
@@ -2353,7 +2353,7 @@
by (meson Int_mono closure_mono closure_subset order_refl)
qed
-lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
+lemma islimpt_in_closure: "(x islimpt S) = (x\<in>closure(S-{x}))"
unfolding closure_def using islimpt_punctured by blast
lemma connected_imp_connected_closure: "connected S \<Longrightarrow> connected (closure S)"
--- a/src/HOL/Auth/CertifiedEmail.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/CertifiedEmail.thy Thu Feb 15 13:04:36 2018 +0100
@@ -11,7 +11,7 @@
"TTP == Server"
abbreviation
- RPwd :: "agent => key" where
+ RPwd :: "agent \<Rightarrow> key" where
"RPwd == shrK"
@@ -24,7 +24,7 @@
BothAuth :: nat
text\<open>We formalize a fixed way of computing responses. Could be better.\<close>
-definition "response" :: "agent => agent => nat => msg" where
+definition "response" :: "agent \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> msg" where
"response S R q == Hash \<lbrace>Agent S, Key (shrK R), Nonce q\<rbrace>"
@@ -129,9 +129,9 @@
lemma hr_form_lemma [rule_format]:
"evs \<in> certified_mail
- ==> hr \<notin> synth (analz (spies evs)) -->
+ \<Longrightarrow> hr \<notin> synth (analz (spies evs)) \<longrightarrow>
(\<forall>S2TTP. Notes TTP \<lbrace>Agent R, Agent TTP, S2TTP, pwd, hr\<rbrace>
- \<in> set evs -->
+ \<in> set evs \<longrightarrow>
(\<exists>clt q S em. hr = Hash \<lbrace>Number clt, Nonce q, response S R q, em\<rbrace>))"
apply (erule certified_mail.induct)
apply (synth_analz_mono_contra, simp_all, blast+)
@@ -201,7 +201,7 @@
done
lemma Spy_dont_know_RPwd [rule_format]:
- "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
+ "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) \<longrightarrow> A \<in> bad"
apply (erule certified_mail.induct, simp_all)
txt\<open>Fake\<close>
apply (blast dest: Fake_parts_insert_in_Un)
@@ -247,8 +247,8 @@
lemma analz_image_freshK [rule_format]:
"evs \<in> certified_mail ==>
- \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
- (Key K \<in> analz (Key`KK Un (spies evs))) =
+ \<forall>K KK. invKey (pubEK TTP) \<notin> KK \<longrightarrow>
+ (Key K \<in> analz (Key`KK \<union> (spies evs))) =
(K \<in> KK | Key K \<in> analz (spies evs))"
apply (erule certified_mail.induct)
apply (drule_tac [6] A=TTP in symKey_neq_priEK)
@@ -281,11 +281,11 @@
isn't inductive: message 3 case can't be proved *)
lemma S2TTP_sender_lemma [rule_format]:
"evs \<in> certified_mail ==>
- Key K \<notin> analz (spies evs) -->
+ Key K \<notin> analz (spies evs) \<longrightarrow>
(\<forall>AO. Crypt (pubEK TTP)
- \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs -->
+ \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace> \<in> used evs \<longrightarrow>
(\<exists>m ctxt q.
- hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
+ hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> \<and>
Says S R
\<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number ctxt, Nonce q,
@@ -314,7 +314,7 @@
Key K \<notin> analz (spies evs);
evs \<in> certified_mail|]
==> \<exists>m ctxt q.
- hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> &
+ hs = Hash\<lbrace>Number ctxt, Nonce q, response S R q, Crypt K (Number m)\<rbrace> \<and>
Says S R
\<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number ctxt, Nonce q,
@@ -345,19 +345,19 @@
where @{term K} is secure.\<close>
lemma Key_unique_lemma [rule_format]:
"evs \<in> certified_mail ==>
- Key K \<notin> analz (spies evs) -->
+ Key K \<notin> analz (spies evs) \<longrightarrow>
(\<forall>m cleartext q hs.
Says S R
\<lbrace>Agent S, Agent TTP, Crypt K (Number m), Number AO,
Number cleartext, Nonce q,
Crypt (pubEK TTP) \<lbrace>Agent S, Number AO, Key K, Agent R, hs\<rbrace>\<rbrace>
- \<in> set evs -->
+ \<in> set evs \<longrightarrow>
(\<forall>m' cleartext' q' hs'.
Says S' R'
\<lbrace>Agent S', Agent TTP, Crypt K (Number m'), Number AO',
Number cleartext', Nonce q',
Crypt (pubEK TTP) \<lbrace>Agent S', Number AO', Key K, Agent R', hs'\<rbrace>\<rbrace>
- \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))"
+ \<in> set evs \<longrightarrow> R' = R \<and> S' = S \<and> AO' = AO \<and> hs' = hs))"
apply (erule certified_mail.induct, analz_mono_contra, simp_all)
prefer 2
txt\<open>Message 1\<close>
@@ -380,7 +380,7 @@
\<in> set evs;
Key K \<notin> analz (spies evs);
evs \<in> certified_mail|]
- ==> R' = R & S' = S & AO' = AO & hs' = hs"
+ ==> R' = R \<and> S' = S \<and> AO' = AO \<and> hs' = hs"
by (rule Key_unique_lemma, assumption+)
@@ -396,7 +396,7 @@
Key K \<in> analz (spies evs);
evs \<in> certified_mail;
S\<noteq>Spy|]
- ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
+ ==> R \<in> bad \<and> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
apply (erule rev_mp)
apply (erule ssubst)
apply (erule rev_mp)
--- a/src/HOL/Auth/Event.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Event.thy Thu Feb 15 13:04:36 2018 +0100
@@ -13,7 +13,7 @@
theory Event imports Message begin
consts (*Initial states of agents -- parameter of the construction*)
- initState :: "agent => msg set"
+ initState :: "agent \<Rightarrow> msg set"
datatype
event = Says agent agent msg
@@ -29,24 +29,24 @@
Server_not_bad [iff]: "Server \<notin> bad"
by (rule exI [of _ "{Spy}"], simp)
-primrec knows :: "agent => event list => msg set"
+primrec knows :: "agent \<Rightarrow> event list \<Rightarrow> msg set"
where
knows_Nil: "knows A [] = initState A"
| knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
- Says A' B X => insert X (knows Spy evs)
- | Gets A' X => knows Spy evs
- | Notes A' X =>
+ Says A' B X \<Rightarrow> insert X (knows Spy evs)
+ | Gets A' X \<Rightarrow> knows Spy evs
+ | Notes A' X \<Rightarrow>
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
else
(case ev of
- Says A' B X =>
+ Says A' B X \<Rightarrow>
if A'=A then insert X (knows A evs) else knows A evs
- | Gets A' X =>
+ | Gets A' X \<Rightarrow>
if A'=A then insert X (knows A evs) else knows A evs
- | Notes A' X =>
+ | Notes A' X \<Rightarrow>
if A'=A then insert X (knows A evs) else knows A evs))"
(*
Case A=Spy on the Gets event
@@ -57,31 +57,31 @@
text\<open>The constant "spies" is retained for compatibility's sake\<close>
abbreviation (input)
- spies :: "event list => msg set" where
+ spies :: "event list \<Rightarrow> msg set" where
"spies == knows Spy"
(*Set of items that might be visible to somebody:
complement of the set of fresh items*)
-primrec used :: "event list => msg set"
+primrec used :: "event list \<Rightarrow> msg set"
where
used_Nil: "used [] = (UN B. parts (initState B))"
| used_Cons: "used (ev # evs) =
(case ev of
- Says A B X => parts {X} \<union> used evs
- | Gets A X => used evs
- | Notes A X => parts {X} \<union> used evs)"
+ Says A B X \<Rightarrow> parts {X} \<union> used evs
+ | Gets A X \<Rightarrow> used evs
+ | Notes A X \<Rightarrow> parts {X} \<union> used evs)"
\<comment> \<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
follows @{term Says} in real protocols. Seems difficult to change.
See \<open>Gets_correct\<close> in theory \<open>Guard/Extensions.thy\<close>.\<close>
-lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
+lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
apply (induct_tac evs)
apply (auto split: event.split)
done
-lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
+lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> used evs"
apply (induct_tac evs)
apply (auto split: event.split)
done
@@ -102,7 +102,7 @@
on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}\<close>
lemma knows_Spy_Notes [simp]:
"knows Spy (Notes A X # evs) =
- (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
+ (if A\<in>bad then insert X (knows Spy evs) else knows Spy evs)"
by simp
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
@@ -122,13 +122,13 @@
text\<open>Spy sees what is sent on the traffic\<close>
lemma Says_imp_knows_Spy [rule_format]:
- "Says A B X \<in> set evs --> X \<in> knows Spy evs"
+ "Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
done
lemma Notes_imp_knows_Spy [rule_format]:
- "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
+ "Notes A X \<in> set evs \<longrightarrow> A \<in> bad \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
done
@@ -162,14 +162,14 @@
by (simp add: subset_insertI)
text\<open>Agents know what they say\<close>
-lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
+lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
text\<open>Agents know what they note\<close>
-lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
+lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
apply blast
@@ -177,7 +177,7 @@
text\<open>Agents know what they receive\<close>
lemma Gets_imp_knows_agents [rule_format]:
- "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
+ "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
done
@@ -186,8 +186,8 @@
text\<open>What agents DIFFERENT FROM Spy know
was either said, or noted, or got, or known initially\<close>
lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
- "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.
- Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
+ "[| X \<in> knows A evs; A \<noteq> Spy |] ==> \<exists> B.
+ Says A B X \<in> set evs \<or> Gets A X \<in> set evs \<or> Notes A X \<in> set evs \<or> X \<in> initState A"
apply (erule rev_mp)
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
@@ -197,8 +197,8 @@
text\<open>What the Spy knows -- for the time being --
was either said or noted, or known initially\<close>
lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
- "[| X \<in> knows Spy evs |] ==> EX A B.
- Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
+ "X \<in> knows Spy evs \<Longrightarrow> \<exists>A B.
+ Says A B X \<in> set evs \<or> Notes A X \<in> set evs \<or> X \<in> initState Spy"
apply (erule rev_mp)
apply (induct_tac "evs")
apply (simp_all (no_asm_simp) split: event.split)
@@ -212,7 +212,7 @@
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
-lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
+lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs"
apply (induct_tac "evs")
apply (simp_all add: parts_insert_knows_A split: event.split, blast)
done
@@ -236,7 +236,7 @@
used_Nil [simp del] used_Cons [simp del]
-text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
+text\<open>For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) \<longrightarrow> P"}
New events added by induction to "evs" are discarded. Provided
this information isn't needed, the proof will be much shorter, since
it will omit complicated reasoning about @{term analz}.\<close>
@@ -278,7 +278,7 @@
method_setup analz_mono_contra = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\<close>
- "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
+ "for proving theorems of the form X \<notin> analz (knows Spy evs) \<longrightarrow> P"
subsubsection\<open>Useful for case analysis on whether a hash is a spoof or not\<close>
@@ -299,6 +299,6 @@
method_setup synth_analz_mono_contra = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt)))\<close>
- "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
+ "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) \<longrightarrow> P"
end
--- a/src/HOL/Auth/Guard/Analz.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy Thu Feb 15 13:04:36 2018 +0100
@@ -16,37 +16,37 @@
pparts :: "msg set => msg set"
for H :: "msg set"
where
- Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H"
-| Fst [dest]: "[| \<lbrace>X,Y\<rbrace>:pparts H; is_MPair X |] ==> X:pparts H"
-| Snd [dest]: "[| \<lbrace>X,Y\<rbrace>:pparts H; is_MPair Y |] ==> Y:pparts H"
+ Inj [intro]: "[| X \<in> H; is_MPair X |] ==> X \<in> pparts H"
+| Fst [dest]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; is_MPair X |] ==> X \<in> pparts H"
+| Snd [dest]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; is_MPair Y |] ==> Y \<in> pparts H"
subsection\<open>basic facts about @{term pparts}\<close>
-lemma pparts_is_MPair [dest]: "X:pparts H ==> is_MPair X"
+lemma pparts_is_MPair [dest]: "X \<in> pparts H \<Longrightarrow> is_MPair X"
by (erule pparts.induct, auto)
-lemma Crypt_notin_pparts [iff]: "Crypt K X ~:pparts H"
+lemma Crypt_notin_pparts [iff]: "Crypt K X \<notin> pparts H"
by auto
-lemma Key_notin_pparts [iff]: "Key K ~:pparts H"
+lemma Key_notin_pparts [iff]: "Key K \<notin> pparts H"
by auto
-lemma Nonce_notin_pparts [iff]: "Nonce n ~:pparts H"
+lemma Nonce_notin_pparts [iff]: "Nonce n \<notin> pparts H"
by auto
-lemma Number_notin_pparts [iff]: "Number n ~:pparts H"
+lemma Number_notin_pparts [iff]: "Number n \<notin> pparts H"
by auto
-lemma Agent_notin_pparts [iff]: "Agent A ~:pparts H"
+lemma Agent_notin_pparts [iff]: "Agent A \<notin> pparts H"
by auto
lemma pparts_empty [iff]: "pparts {} = {}"
by (auto, erule pparts.induct, auto)
-lemma pparts_insertI [intro]: "X:pparts H ==> X:pparts (insert Y H)"
+lemma pparts_insertI [intro]: "X \<in> pparts H \<Longrightarrow> X \<in> pparts (insert Y H)"
by (erule pparts.induct, auto)
-lemma pparts_sub: "[| X:pparts G; G<=H |] ==> X:pparts H"
+lemma pparts_sub: "[| X \<in> pparts G; G \<subseteq> H |] ==> X \<in> pparts H"
by (erule pparts.induct, auto)
lemma pparts_insert2 [iff]: "pparts (insert X (insert Y H))
@@ -78,13 +78,13 @@
lemma pparts_insert_Hash [iff]: "pparts (insert (Hash X) H) = pparts H"
by (rule eq, erule pparts.induct, auto)
-lemma pparts_insert: "X:pparts (insert Y H) ==> X:pparts {Y} Un pparts H"
+lemma pparts_insert: "X \<in> pparts (insert Y H) \<Longrightarrow> X \<in> pparts {Y} \<union> pparts H"
by (erule pparts.induct, blast+)
-lemma insert_pparts: "X:pparts {Y} Un pparts H ==> X:pparts (insert Y H)"
+lemma insert_pparts: "X \<in> pparts {Y} \<union> pparts H \<Longrightarrow> X \<in> pparts (insert Y H)"
by (safe, erule pparts.induct, auto)
-lemma pparts_Un [iff]: "pparts (G Un H) = pparts G Un pparts H"
+lemma pparts_Un [iff]: "pparts (G \<union> H) = pparts G \<union> pparts H"
by (rule eq, erule pparts.induct, auto dest: pparts_sub)
lemma pparts_pparts [iff]: "pparts (pparts H) = pparts H"
@@ -95,21 +95,21 @@
lemmas pparts_insert_substI = pparts_insert_eq [THEN ssubst]
-lemma in_pparts: "Y:pparts H ==> EX X. X:H & Y:pparts {X}"
+lemma in_pparts: "Y \<in> pparts H \<Longrightarrow> \<exists>X. X \<in> H \<and> Y \<in> pparts {X}"
by (erule pparts.induct, auto)
subsection\<open>facts about @{term pparts} and @{term parts}\<close>
-lemma pparts_no_Nonce [dest]: "[| X:pparts {Y}; Nonce n ~:parts {Y} |]
-==> Nonce n ~:parts {X}"
+lemma pparts_no_Nonce [dest]: "[| X \<in> pparts {Y}; Nonce n \<notin> parts {Y} |]
+==> Nonce n \<notin> parts {X}"
by (erule pparts.induct, simp_all)
subsection\<open>facts about @{term pparts} and @{term analz}\<close>
-lemma pparts_analz: "X:pparts H ==> X:analz H"
+lemma pparts_analz: "X \<in> pparts H \<Longrightarrow> X \<in> analz H"
by (erule pparts.induct, auto)
-lemma pparts_analz_sub: "[| X:pparts G; G<=H |] ==> X:analz H"
+lemma pparts_analz_sub: "[| X \<in> pparts G; G \<subseteq> H |] ==> X \<in> analz H"
by (auto dest: pparts_sub pparts_analz)
subsection\<open>messages that contribute to analz\<close>
@@ -118,23 +118,23 @@
kparts :: "msg set => msg set"
for H :: "msg set"
where
- Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H"
-| Fst [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair X |] ==> X:kparts H"
-| Snd [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair Y |] ==> Y:kparts H"
+ Inj [intro]: "[| X \<in> H; not_MPair X |] ==> X \<in> kparts H"
+| Fst [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair X |] ==> X \<in> kparts H"
+| Snd [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair Y |] ==> Y \<in> kparts H"
subsection\<open>basic facts about @{term kparts}\<close>
-lemma kparts_not_MPair [dest]: "X:kparts H ==> not_MPair X"
+lemma kparts_not_MPair [dest]: "X \<in> kparts H \<Longrightarrow> not_MPair X"
by (erule kparts.induct, auto)
lemma kparts_empty [iff]: "kparts {} = {}"
by (rule eq, erule kparts.induct, auto)
-lemma kparts_insertI [intro]: "X:kparts H ==> X:kparts (insert Y H)"
+lemma kparts_insertI [intro]: "X \<in> kparts H \<Longrightarrow> X \<in> kparts (insert Y H)"
by (erule kparts.induct, auto dest: pparts_insertI)
lemma kparts_insert2 [iff]: "kparts (insert X (insert Y H))
-= kparts {X} Un kparts {Y} Un kparts H"
+= kparts {X} \<union> kparts {Y} \<union> kparts H"
by (rule eq, (erule kparts.induct, auto)+)
lemma kparts_insert_MPair [iff]: "kparts (insert \<lbrace>X,Y\<rbrace> H)
@@ -165,17 +165,17 @@
= insert (Hash X) (kparts H)"
by (rule eq, erule kparts.induct, auto)
-lemma kparts_insert: "X:kparts (insert X H) ==> X:kparts {X} Un kparts H"
+lemma kparts_insert: "X \<in> kparts (insert X H) \<Longrightarrow> X \<in> kparts {X} \<union> kparts H"
by (erule kparts.induct, (blast dest: pparts_insert)+)
-lemma kparts_insert_fst [rule_format,dest]: "X:kparts (insert Z H) ==>
-X ~:kparts H --> X:kparts {Z}"
+lemma kparts_insert_fst [rule_format,dest]: "X \<in> kparts (insert Z H) \<Longrightarrow>
+X \<notin> kparts H \<longrightarrow> X \<in> kparts {Z}"
by (erule kparts.induct, (blast dest: pparts_insert)+)
-lemma kparts_sub: "[| X:kparts G; G<=H |] ==> X:kparts H"
+lemma kparts_sub: "[| X \<in> kparts G; G \<subseteq> H |] ==> X \<in> kparts H"
by (erule kparts.induct, auto dest: pparts_sub)
-lemma kparts_Un [iff]: "kparts (G Un H) = kparts G Un kparts H"
+lemma kparts_Un [iff]: "kparts (G \<union> H) = kparts G \<union> kparts H"
by (rule eq, erule kparts.induct, auto dest: kparts_sub)
lemma pparts_kparts [iff]: "pparts (kparts H) = {}"
@@ -184,12 +184,12 @@
lemma kparts_kparts [iff]: "kparts (kparts H) = kparts H"
by (rule eq, erule kparts.induct, auto)
-lemma kparts_insert_eq: "kparts (insert X H) = kparts {X} Un kparts H"
+lemma kparts_insert_eq: "kparts (insert X H) = kparts {X} \<union> kparts H"
by (rule_tac A=H in insert_Un, rule kparts_Un)
lemmas kparts_insert_substI = kparts_insert_eq [THEN ssubst]
-lemma in_kparts: "Y:kparts H ==> EX X. X:H & Y:kparts {X}"
+lemma in_kparts: "Y \<in> kparts H \<Longrightarrow> \<exists>X. X \<in> H \<and> Y \<in> kparts {X}"
by (erule kparts.induct, auto dest: in_pparts)
lemma kparts_has_no_pair [iff]: "has_no_pair (kparts H)"
@@ -197,59 +197,59 @@
subsection\<open>facts about @{term kparts} and @{term parts}\<close>
-lemma kparts_no_Nonce [dest]: "[| X:kparts {Y}; Nonce n ~:parts {Y} |]
-==> Nonce n ~:parts {X}"
+lemma kparts_no_Nonce [dest]: "[| X \<in> kparts {Y}; Nonce n \<notin> parts {Y} |]
+==> Nonce n \<notin> parts {X}"
by (erule kparts.induct, auto)
-lemma kparts_parts: "X:kparts H ==> X:parts H"
+lemma kparts_parts: "X \<in> kparts H \<Longrightarrow> X \<in> parts H"
by (erule kparts.induct, auto dest: pparts_analz)
-lemma parts_kparts: "X:parts (kparts H) ==> X:parts H"
+lemma parts_kparts: "X \<in> parts (kparts H) \<Longrightarrow> X \<in> parts H"
by (erule parts.induct, auto dest: kparts_parts
intro: parts.Fst parts.Snd parts.Body)
-lemma Crypt_kparts_Nonce_parts [dest]: "[| Crypt K Y:kparts {Z};
-Nonce n:parts {Y} |] ==> Nonce n:parts {Z}"
+lemma Crypt_kparts_Nonce_parts [dest]: "[| Crypt K Y \<in> kparts {Z};
+Nonce n \<in> parts {Y} |] ==> Nonce n \<in> parts {Z}"
by auto
subsection\<open>facts about @{term kparts} and @{term analz}\<close>
-lemma kparts_analz: "X:kparts H ==> X:analz H"
+lemma kparts_analz: "X \<in> kparts H \<Longrightarrow> X \<in> analz H"
by (erule kparts.induct, auto dest: pparts_analz)
-lemma kparts_analz_sub: "[| X:kparts G; G<=H |] ==> X:analz H"
+lemma kparts_analz_sub: "[| X \<in> kparts G; G \<subseteq> H |] ==> X \<in> analz H"
by (erule kparts.induct, auto dest: pparts_analz_sub)
-lemma analz_kparts [rule_format,dest]: "X:analz H ==>
-Y:kparts {X} --> Y:analz H"
+lemma analz_kparts [rule_format,dest]: "X \<in> analz H \<Longrightarrow>
+Y \<in> kparts {X} \<longrightarrow> Y \<in> analz H"
by (erule analz.induct, auto dest: kparts_analz_sub)
-lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H"
+lemma analz_kparts_analz: "X \<in> analz (kparts H) \<Longrightarrow> X \<in> analz H"
by (erule analz.induct, auto dest: kparts_analz)
-lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)"
+lemma analz_kparts_insert: "X \<in> analz (kparts (insert Z H)) \<Longrightarrow> X \<in> analz (kparts {Z} \<union> kparts H)"
by (rule analz_sub, auto)
-lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
-==> Nonce n:kparts {Y} --> Nonce n:analz G"
+lemma Nonce_kparts_synth [rule_format]: "Y \<in> synth (analz G)
+\<Longrightarrow> Nonce n \<in> kparts {Y} \<longrightarrow> Nonce n \<in> analz G"
by (erule synth.induct, auto)
-lemma kparts_insert_synth: "[| Y:parts (insert X G); X:synth (analz G);
-Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G"
+lemma kparts_insert_synth: "[| Y \<in> parts (insert X G); X \<in> synth (analz G);
+Nonce n \<in> kparts {Y}; Nonce n \<notin> analz G |] ==> Y \<in> parts G"
apply (drule parts_insert_substD, clarify)
apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
apply (auto dest: Nonce_kparts_synth)
done
lemma Crypt_insert_synth:
- "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |]
- ==> Crypt K Y:parts G"
+ "[| Crypt K Y \<in> parts (insert X G); X \<in> synth (analz G); Nonce n \<in> kparts {Y}; Nonce n \<notin> analz G |]
+ ==> Crypt K Y \<in> parts G"
by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))
subsection\<open>analz is pparts + analz of kparts\<close>
-lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)"
+lemma analz_pparts_kparts: "X \<in> analz H \<Longrightarrow> X \<in> pparts H \<or> X \<in> analz (kparts H)"
by (erule analz.induct, auto)
lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)"
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Thu Feb 15 13:04:36 2018 +0100
@@ -11,13 +11,13 @@
subsection\<open>Extensions to Theory \<open>Set\<close>\<close>
-lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B"
+lemma eq: "[| \<And>x. x\<in>A \<Longrightarrow> x\<in>B; \<And>x. x\<in>B \<Longrightarrow> x\<in>A |] ==> A=B"
by auto
-lemma insert_Un: "P ({x} Un A) ==> P (insert x A)"
+lemma insert_Un: "P ({x} \<union> A) \<Longrightarrow> P (insert x A)"
by simp
-lemma in_sub: "x:A ==> {x}<=A"
+lemma in_sub: "x\<in>A \<Longrightarrow> {x}\<subseteq>A"
by auto
@@ -51,7 +51,7 @@
subsubsection\<open>messages that are pairs\<close>
definition is_MPair :: "msg => bool" where
-"is_MPair X == EX Y Z. X = \<lbrace>Y,Z\<rbrace>"
+"is_MPair X == \<exists>Y Z. X = \<lbrace>Y,Z\<rbrace>"
declare is_MPair_def [simp]
@@ -86,7 +86,7 @@
declare is_MPair_def [simp del]
definition has_no_pair :: "msg set => bool" where
-"has_no_pair H == ALL X Y. \<lbrace>X,Y\<rbrace> \<notin> H"
+"has_no_pair H == \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H"
declare has_no_pair_def [simp]
@@ -98,38 +98,38 @@
lemma wf_Crypt2 [iff]: "X ~= Crypt K X"
by (induct X, auto)
-lemma parts_size: "X:parts {Y} ==> X=Y | size X < size Y"
+lemma parts_size: "X \<in> parts {Y} \<Longrightarrow> X=Y \<or> size X < size Y"
by (erule parts.induct, auto)
-lemma wf_Crypt_parts [iff]: "Crypt K X ~:parts {X}"
+lemma wf_Crypt_parts [iff]: "Crypt K X \<notin> parts {X}"
by (auto dest: parts_size)
subsubsection\<open>lemmas on keysFor\<close>
definition usekeys :: "msg set => key set" where
-"usekeys G == {K. EX Y. Crypt K Y:G}"
+"usekeys G \<equiv> {K. \<exists>Y. Crypt K Y \<in> G}"
lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)"
apply (simp add: keysFor_def)
apply (rule finite_imageI)
apply (induct G rule: finite_induct)
apply auto
-apply (case_tac "EX K X. x = Crypt K X", clarsimp)
-apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F}
+apply (case_tac "\<exists>K X. x = Crypt K X", clarsimp)
+apply (subgoal_tac "{Ka. \<exists>Xa. (Ka=K \<and> Xa=X) \<or> Crypt Ka Xa \<in> F}
= insert K (usekeys F)", auto simp: usekeys_def)
-by (subgoal_tac "{K. EX X. Crypt K X = x | Crypt K X:F} = usekeys F",
+by (subgoal_tac "{K. \<exists>X. Crypt K X = x \<or> Crypt K X \<in> F} = usekeys F",
auto simp: usekeys_def)
subsubsection\<open>lemmas on parts\<close>
-lemma parts_sub: "[| X:parts G; G<=H |] ==> X:parts H"
+lemma parts_sub: "[| X \<in> parts G; G \<subseteq> H |] ==> X \<in> parts H"
by (auto dest: parts_mono)
-lemma parts_Diff [dest]: "X:parts (G - H) ==> X:parts G"
+lemma parts_Diff [dest]: "X \<in> parts (G - H) \<Longrightarrow> X \<in> parts G"
by (erule parts_sub, auto)
-lemma parts_Diff_notin: "[| Y ~:H; Nonce n ~:parts (H - {Y}) |]
-==> Nonce n ~:parts H"
+lemma parts_Diff_notin: "[| Y \<notin> H; Nonce n \<notin> parts (H - {Y}) |]
+==> Nonce n \<notin> parts H"
by simp
lemmas parts_insert_substI = parts_insert [THEN ssubst]
@@ -138,39 +138,39 @@
lemma finite_parts_msg [iff]: "finite (parts {X})"
by (induct X, auto)
-lemma finite_parts [intro]: "finite H ==> finite (parts H)"
+lemma finite_parts [intro]: "finite H \<Longrightarrow> finite (parts H)"
apply (erule finite_induct, simp)
by (rule parts_insert_substI, simp)
-lemma parts_parts: "[| X:parts {Y}; Y:parts G |] ==> X:parts G"
+lemma parts_parts: "[| X \<in> parts {Y}; Y \<in> parts G |] ==> X \<in> parts G"
by (frule parts_cut, auto)
-lemma parts_parts_parts: "[| X:parts {Y}; Y:parts {Z}; Z:parts G |] ==> X:parts G"
+lemma parts_parts_parts: "[| X \<in> parts {Y}; Y \<in> parts {Z}; Z \<in> parts G |] ==> X \<in> parts G"
by (auto dest: parts_parts)
-lemma parts_parts_Crypt: "[| Crypt K X:parts G; Nonce n:parts {X} |]
-==> Nonce n:parts G"
+lemma parts_parts_Crypt: "[| Crypt K X \<in> parts G; Nonce n \<in> parts {X} |]
+==> Nonce n \<in> parts G"
by (blast intro: parts.Body dest: parts_parts)
subsubsection\<open>lemmas on synth\<close>
-lemma synth_sub: "[| X:synth G; G<=H |] ==> X:synth H"
+lemma synth_sub: "[| X \<in> synth G; G \<subseteq> H |] ==> X \<in> synth H"
by (auto dest: synth_mono)
-lemma Crypt_synth [rule_format]: "[| X:synth G; Key K ~:G |] ==>
-Crypt K Y:parts {X} --> Crypt K Y:parts G"
+lemma Crypt_synth [rule_format]: "[| X \<in> synth G; Key K \<notin> G |] ==>
+Crypt K Y \<in> parts {X} \<longrightarrow> Crypt K Y \<in> parts G"
by (erule synth.induct, auto dest: parts_sub)
subsubsection\<open>lemmas on analz\<close>
-lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)"
+lemma analz_UnI1 [intro]: "X \<in> analz G ==> X \<in> analz (G \<union> H)"
by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+
-lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H"
+lemma analz_sub: "[| X \<in> analz G; G \<subseteq> H |] ==> X \<in> analz H"
by (auto dest: analz_mono)
-lemma analz_Diff [dest]: "X:analz (G - H) ==> X:analz G"
+lemma analz_Diff [dest]: "X \<in> analz (G - H) \<Longrightarrow> X \<in> analz G"
by (erule analz.induct, auto)
lemmas in_analz_subset_cong = analz_subset_cong [THEN subsetD]
@@ -181,32 +181,32 @@
lemmas insert_commute_substI = insert_commute [THEN ssubst]
lemma analz_insertD:
- "[| Crypt K Y:H; Key (invKey K):H |] ==> analz (insert Y H) = analz H"
+ "[| Crypt K Y \<in> H; Key (invKey K) \<in> H |] ==> analz (insert Y H) = analz H"
by (blast intro: analz.Decrypt analz_insert_eq)
-lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==>
-X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)"
+lemma must_decrypt [rule_format,dest]: "[| X \<in> analz H; has_no_pair H |] ==>
+X \<notin> H \<longrightarrow> (\<exists>K Y. Crypt K Y \<in> H \<and> Key (invKey K) \<in> H)"
by (erule analz.induct, auto)
-lemma analz_needs_only_finite: "X:analz H ==> EX G. G <= H & finite G"
+lemma analz_needs_only_finite: "X \<in> analz H \<Longrightarrow> \<exists>G. G \<subseteq> H \<and> finite G"
by (erule analz.induct, auto)
-lemma notin_analz_insert: "X ~:analz (insert Y G) ==> X ~:analz G"
+lemma notin_analz_insert: "X \<notin> analz (insert Y G) \<Longrightarrow> X \<notin> analz G"
by auto
subsubsection\<open>lemmas on parts, synth and analz\<close>
-lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
-X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
+lemma parts_invKey [rule_format,dest]:"X \<in> parts {Y} \<Longrightarrow>
+X \<in> analz (insert (Crypt K Y) H) \<longrightarrow> X \<notin> analz H \<longrightarrow> Key (invKey K) \<in> analz H"
by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
-lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
+lemma in_analz: "Y \<in> analz H \<Longrightarrow> \<exists>X. X \<in> H \<and> Y \<in> parts {X}"
by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
lemmas in_analz_subset_parts = analz_subset_parts [THEN subsetD]
-lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
-Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
+lemma Crypt_synth_insert: "[| Crypt K X \<in> parts (insert Y H);
+Y \<in> synth (analz H); Key K \<notin> analz H |] ==> Crypt K X \<in> parts H"
apply (drule parts_insert_substD, clarify)
apply (frule in_sub)
apply (frule parts_mono)
@@ -222,24 +222,24 @@
| "greatest_msg (Crypt K X) = greatest_msg X"
| "greatest_msg other = 0"
-lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
+lemma greatest_msg_is_greatest: "Nonce n \<in> parts {X} \<Longrightarrow> n \<le> greatest_msg X"
by (induct X, auto)
subsubsection\<open>sets of keys\<close>
definition keyset :: "msg set => bool" where
-"keyset G == ALL X. X:G --> (EX K. X = Key K)"
+"keyset G \<equiv> \<forall>X. X \<in> G \<longrightarrow> (\<exists>K. X = Key K)"
-lemma keyset_in [dest]: "[| keyset G; X:G |] ==> EX K. X = Key K"
+lemma keyset_in [dest]: "[| keyset G; X \<in> G |] ==> \<exists>K. X = Key K"
by (auto simp: keyset_def)
lemma MPair_notin_keyset [simp]: "keyset G ==> \<lbrace>X,Y\<rbrace> \<notin> G"
by auto
-lemma Crypt_notin_keyset [simp]: "keyset G ==> Crypt K X ~:G"
+lemma Crypt_notin_keyset [simp]: "keyset G \<Longrightarrow> Crypt K X \<notin> G"
by auto
-lemma Nonce_notin_keyset [simp]: "keyset G ==> Nonce n ~:G"
+lemma Nonce_notin_keyset [simp]: "keyset G \<Longrightarrow> Nonce n \<notin> G"
by auto
lemma parts_keyset [simp]: "keyset G ==> parts G = G"
@@ -256,10 +256,10 @@
lemma keyset_Diff_keysfor [simp]: "keyset H ==> keyset (H - keysfor G)"
by (auto simp: keyset_def)
-lemma keysfor_Crypt: "Crypt K X:parts G ==> Key (invKey K):keysfor G"
+lemma keysfor_Crypt: "Crypt K X \<in> parts G \<Longrightarrow> Key (invKey K) \<in> keysfor G"
by (auto simp: keysfor_def Crypt_imp_invKey_keysFor)
-lemma no_key_no_Crypt: "Key K ~:keysfor G ==> Crypt (invKey K) X ~:parts G"
+lemma no_key_no_Crypt: "Key K \<notin> keysfor G \<Longrightarrow> Crypt (invKey K) X \<notin> parts G"
by (auto dest: keysfor_Crypt)
lemma finite_keysfor [intro]: "finite G ==> finite (keysfor G)"
@@ -273,7 +273,7 @@
apply (erule analz.induct, blast)
apply (simp, blast)
apply (simp, blast)
-apply (case_tac "Key (invKey K):H - keysfor G", clarsimp)
+apply (case_tac "Key (invKey K) \<in> H - keysfor G", clarsimp)
apply (drule_tac X=X in no_key_no_Crypt)
by (auto intro: analz_sub)
@@ -286,7 +286,7 @@
subsubsection\<open>general protocol properties\<close>
definition is_Says :: "event => bool" where
-"is_Says ev == (EX A B X. ev = Says A B X)"
+"is_Says ev == (\<exists>A B X. ev = Says A B X)"
lemma is_Says_Says [iff]: "is_Says (Says A B X)"
by (simp add: is_Says_def)
@@ -294,36 +294,36 @@
(* one could also require that Gets occurs after Says
but this is sufficient for our purpose *)
definition Gets_correct :: "event list set => bool" where
-"Gets_correct p == ALL evs B X. evs:p --> Gets B X:set evs
---> (EX A. Says A B X:set evs)"
+"Gets_correct p == \<forall>evs B X. evs \<in> p \<longrightarrow> Gets B X \<in> set evs
+\<longrightarrow> (\<exists>A. Says A B X \<in> set evs)"
-lemma Gets_correct_Says: "[| Gets_correct p; Gets B X # evs:p |]
-==> EX A. Says A B X:set evs"
+lemma Gets_correct_Says: "[| Gets_correct p; Gets B X # evs \<in> p |]
+==> \<exists>A. Says A B X \<in> set evs"
apply (simp add: Gets_correct_def)
by (drule_tac x="Gets B X # evs" in spec, auto)
definition one_step :: "event list set => bool" where
-"one_step p == ALL evs ev. ev#evs:p --> evs:p"
+"one_step p == \<forall>evs ev. ev#evs \<in> p \<longrightarrow> evs \<in> p"
-lemma one_step_Cons [dest]: "[| one_step p; ev#evs:p |] ==> evs:p"
+lemma one_step_Cons [dest]: "[| one_step p; ev#evs \<in> p |] ==> evs \<in> p"
by (unfold one_step_def, blast)
-lemma one_step_app: "[| evs@evs':p; one_step p; []:p |] ==> evs':p"
+lemma one_step_app: "[| evs@evs' \<in> p; one_step p; [] \<in> p |] ==> evs' \<in> p"
by (induct evs, auto)
-lemma trunc: "[| evs @ evs':p; one_step p |] ==> evs':p"
+lemma trunc: "[| evs @ evs' \<in> p; one_step p |] ==> evs' \<in> p"
by (induct evs, auto)
definition has_only_Says :: "event list set => bool" where
-"has_only_Says p == ALL evs ev. evs:p --> ev:set evs
---> (EX A B X. ev = Says A B X)"
+"has_only_Says p \<equiv> \<forall>evs ev. evs \<in> p \<longrightarrow> ev \<in> set evs
+\<longrightarrow> (\<exists>A B X. ev = Says A B X)"
-lemma has_only_SaysD: "[| ev:set evs; evs:p; has_only_Says p |]
-==> EX A B X. ev = Says A B X"
+lemma has_only_SaysD: "[| ev \<in> set evs; evs \<in> p; has_only_Says p |]
+==> \<exists>A B X. ev = Says A B X"
by (unfold has_only_Says_def, blast)
-lemma in_has_only_Says [dest]: "[| has_only_Says p; evs:p; ev:set evs |]
-==> EX A B X. ev = Says A B X"
+lemma in_has_only_Says [dest]: "[| has_only_Says p; evs \<in> p; ev \<in> set evs |]
+==> \<exists>A B X. ev = Says A B X"
by (auto simp: has_only_Says_def)
lemma has_only_Says_imp_Gets_correct [simp]: "has_only_Says p
@@ -332,11 +332,11 @@
subsubsection\<open>lemma on knows\<close>
-lemma Says_imp_spies2: "Says A B \<lbrace>X,Y\<rbrace> \<in> set evs ==> Y \<in> parts (spies evs)"
+lemma Says_imp_spies2: "Says A B \<lbrace>X,Y\<rbrace> \<in> set evs \<Longrightarrow> Y \<in> parts (spies evs)"
by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp)
-lemma Says_not_parts: "[| Says A B X:set evs; Y ~:parts (spies evs) |]
-==> Y ~:parts {X}"
+lemma Says_not_parts: "[| Says A B X \<in> set evs; Y \<notin> parts (spies evs) |]
+==> Y \<notin> parts {X}"
by (auto dest: Says_imp_spies parts_parts)
subsubsection\<open>knows without initState\<close>
@@ -349,7 +349,7 @@
case ev of
Says A' B X => insert X (knows' A evs)
| Gets A' X => knows' A evs
- | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs
+ | Notes A' X => if A' \<in> bad then insert X (knows' A evs) else knows' A evs
) else (
case ev of
Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs
@@ -390,8 +390,8 @@
lemmas knows_Cons_substI = knows_Cons [THEN ssubst]
lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst]
-lemma knows'_sub_spies': "[| evs:p; has_only_Says p; one_step p |]
-==> knows' A evs <= spies' evs"
+lemma knows'_sub_spies': "[| evs \<in> p; has_only_Says p; one_step p |]
+==> knows' A evs \<subseteq> spies' evs"
by (induct evs, auto split: event.splits)
subsubsection\<open>knows' is finite\<close>
@@ -404,7 +404,7 @@
lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)"
by(cases A, induct evs, auto simp: knows.simps split:event.split)
-lemma knows_ConsI: "X:knows A evs ==> X:knows A (ev#evs)"
+lemma knows_ConsI: "X \<in> knows A evs \<Longrightarrow> X \<in> knows A (ev#evs)"
by (auto dest: knows_sub_Cons [THEN subsetD])
lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')"
@@ -424,7 +424,7 @@
Says A' B X => insert X (knows_max' A evs)
| Gets A' X => knows_max' A evs
| Notes A' X =>
- if A':bad then insert X (knows_max' A evs) else knows_max' A evs
+ if A' \<in> bad then insert X (knows_max' A evs) else knows_max' A evs
) else (
case ev of
Says A' B X =>
@@ -466,22 +466,22 @@
lemma finite_knows_max' [iff]: "finite (knows_max' A evs)"
by (induct evs, auto split: event.split)
-lemma knows_max'_sub_spies': "[| evs:p; has_only_Says p; one_step p |]
-==> knows_max' A evs <= spies' evs"
+lemma knows_max'_sub_spies': "[| evs \<in> p; has_only_Says p; one_step p |]
+==> knows_max' A evs \<subseteq> spies' evs"
by (induct evs, auto split: event.splits)
-lemma knows_max'_in_spies' [dest]: "[| evs:p; X:knows_max' A evs;
-has_only_Says p; one_step p |] ==> X:spies' evs"
+lemma knows_max'_in_spies' [dest]: "[| evs \<in> p; X \<in> knows_max' A evs;
+has_only_Says p; one_step p |] ==> X \<in> spies' evs"
by (rule knows_max'_sub_spies' [THEN subsetD], auto)
lemma knows_max'_app: "knows_max' A (evs @ evs')
= knows_max' A evs Un knows_max' A evs'"
by (induct evs, auto split: event.splits)
-lemma Says_to_knows_max': "Says A B X:set evs ==> X:knows_max' B evs"
+lemma Says_to_knows_max': "Says A B X \<in> set evs \<Longrightarrow> X \<in> knows_max' B evs"
by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app)
-lemma Says_from_knows_max': "Says A B X:set evs ==> X:knows_max' A evs"
+lemma Says_from_knows_max': "Says A B X \<in> set evs \<Longrightarrow> X \<in> knows_max' A evs"
by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app)
subsubsection\<open>used without initState\<close>
@@ -501,10 +501,10 @@
lemma used_decomp: "used evs = init Un used' evs"
by (induct evs, auto simp: init_def split: event.split)
-lemma used'_sub_app: "used' evs <= used' (evs@evs')"
+lemma used'_sub_app: "used' evs \<subseteq> used' (evs@evs')"
by (induct evs, auto split: event.split)
-lemma used'_parts [rule_format]: "X:used' evs ==> Y:parts {X} --> Y:used' evs"
+lemma used'_parts [rule_format]: "X \<in> used' evs \<Longrightarrow> Y \<in> parts {X} \<longrightarrow> Y \<in> used' evs"
apply (induct evs, simp)
apply (rename_tac a b)
apply (case_tac a, simp_all)
@@ -516,35 +516,35 @@
lemma used_sub_Cons: "used evs <= used (ev#evs)"
by (induct evs, (induct ev, auto)+)
-lemma used_ConsI: "X:used evs ==> X:used (ev#evs)"
+lemma used_ConsI: "X \<in> used evs \<Longrightarrow> X \<in> used (ev#evs)"
by (auto dest: used_sub_Cons [THEN subsetD])
-lemma notin_used_ConsD: "X ~:used (ev#evs) ==> X ~:used evs"
+lemma notin_used_ConsD: "X \<notin> used (ev#evs) \<Longrightarrow> X \<notin> used evs"
by (auto dest: used_sub_Cons [THEN subsetD])
-lemma used_appD [dest]: "X:used (evs @ evs') ==> X:used evs | X:used evs'"
+lemma used_appD [dest]: "X \<in> used (evs @ evs') \<Longrightarrow> X \<in> used evs \<or> X \<in> used evs'"
by (induct evs, auto, rename_tac a b, case_tac a, auto)
-lemma used_ConsD: "X:used (ev#evs) ==> X:used [ev] | X:used evs"
+lemma used_ConsD: "X \<in> used (ev#evs) \<Longrightarrow> X \<in> used [ev] \<or> X \<in> used evs"
by (case_tac ev, auto)
lemma used_sub_app: "used evs <= used (evs@evs')"
by (auto simp: used_decomp dest: used'_sub_app [THEN subsetD])
-lemma used_appIL: "X:used evs ==> X:used (evs' @ evs)"
+lemma used_appIL: "X \<in> used evs \<Longrightarrow> X \<in> used (evs' @ evs)"
by (induct evs', auto intro: used_ConsI)
-lemma used_appIR: "X:used evs ==> X:used (evs @ evs')"
+lemma used_appIR: "X \<in> used evs \<Longrightarrow> X \<in> used (evs @ evs')"
by (erule used_sub_app [THEN subsetD])
-lemma used_parts: "[| X:parts {Y}; Y:used evs |] ==> X:used evs"
+lemma used_parts: "[| X \<in> parts {Y}; Y \<in> used evs |] ==> X \<in> used evs"
apply (auto simp: used_decomp dest: used'_parts)
by (auto simp: init_def used_Nil dest: parts_trans)
-lemma parts_Says_used: "[| Says A B X:set evs; Y:parts {X} |] ==> Y:used evs"
+lemma parts_Says_used: "[| Says A B X \<in> set evs; Y \<in> parts {X} |] ==> Y \<in> used evs"
by (induct evs, simp_all, safe, auto intro: used_ConsI)
-lemma parts_used_app: "X:parts {Y} ==> X:used (evs @ Says A B Y # evs')"
+lemma parts_used_app: "X \<in> parts {Y} \<Longrightarrow> X \<in> used (evs @ Says A B Y # evs')"
apply (drule_tac evs="[Says A B Y]" in used_parts, simp, blast)
apply (drule_tac evs'=evs' in used_appIR)
apply (drule_tac evs'=evs in used_appIL)
@@ -552,67 +552,67 @@
subsubsection\<open>lemmas on used and knows\<close>
-lemma initState_used: "X:parts (initState A) ==> X:used evs"
+lemma initState_used: "X \<in> parts (initState A) \<Longrightarrow> X \<in> used evs"
by (induct evs, auto simp: used.simps split: event.split)
-lemma Says_imp_used: "Says A B X:set evs ==> parts {X} <= used evs"
+lemma Says_imp_used: "Says A B X \<in> set evs \<Longrightarrow> parts {X} \<subseteq> used evs"
by (induct evs, auto intro: used_ConsI)
-lemma not_used_not_spied: "X ~:used evs ==> X ~:parts (spies evs)"
+lemma not_used_not_spied: "X \<notin> used evs \<Longrightarrow> X \<notin> parts (spies evs)"
by (induct evs, auto simp: used_Nil)
-lemma not_used_not_parts: "[| Y ~:used evs; Says A B X:set evs |]
-==> Y ~:parts {X}"
+lemma not_used_not_parts: "[| Y \<notin> used evs; Says A B X \<in> set evs |]
+==> Y \<notin> parts {X}"
by (induct evs, auto intro: used_ConsI)
-lemma not_used_parts_false: "[| X ~:used evs; Y:parts (spies evs) |]
-==> X ~:parts {Y}"
+lemma not_used_parts_false: "[| X \<notin> used evs; Y \<in> parts (spies evs) |]
+==> X \<notin> parts {Y}"
by (auto dest: parts_parts)
-lemma known_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
-==> X:parts (knows A evs) --> X:used evs"
+lemma known_used [rule_format]: "[| evs \<in> p; Gets_correct p; one_step p |]
+==> X \<in> parts (knows A evs) \<longrightarrow> X \<in> used evs"
apply (case_tac "A=Spy", blast)
apply (induct evs)
apply (simp add: used.simps, blast)
apply (rename_tac a evs)
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
-apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
+apply (drule_tac P="\<lambda>G. X \<in> parts G" in knows_Cons_substD, safe)
apply (erule initState_used)
apply (case_tac a, auto)
apply (rename_tac msg)
apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
by (auto dest: Says_imp_used intro: used_ConsI)
-lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
-==> X:parts (knows_max A evs) --> X:used evs"
+lemma known_max_used [rule_format]: "[| evs \<in> p; Gets_correct p; one_step p |]
+==> X \<in> parts (knows_max A evs) \<longrightarrow> X \<in> used evs"
apply (case_tac "A=Spy")
apply force
apply (induct evs)
apply (simp add: knows_max_def used.simps, blast)
apply (rename_tac a evs)
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
-apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
+apply (drule_tac P="\<lambda>G. X \<in> parts G" in knows_max_Cons_substD, safe)
apply (case_tac a, auto)
apply (rename_tac msg)
apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
-lemma not_used_not_known: "[| evs:p; X ~:used evs;
-Gets_correct p; one_step p |] ==> X ~:parts (knows A evs)"
+lemma not_used_not_known: "[| evs \<in> p; X \<notin> used evs;
+Gets_correct p; one_step p |] ==> X \<notin> parts (knows A evs)"
by (case_tac "A=Spy", auto dest: not_used_not_spied known_used)
-lemma not_used_not_known_max: "[| evs:p; X ~:used evs;
-Gets_correct p; one_step p |] ==> X ~:parts (knows_max A evs)"
+lemma not_used_not_known_max: "[| evs \<in> p; X \<notin> used evs;
+Gets_correct p; one_step p |] ==> X \<notin> parts (knows_max A evs)"
by (case_tac "A=Spy", auto dest: not_used_not_spied known_max_used)
subsubsection\<open>a nonce or key in a message cannot equal a fresh nonce or key\<close>
-lemma Nonce_neq [dest]: "[| Nonce n' ~:used evs;
-Says A B X:set evs; Nonce n:parts {X} |] ==> n ~= n'"
+lemma Nonce_neq [dest]: "[| Nonce n' \<notin> used evs;
+Says A B X \<in> set evs; Nonce n \<in> parts {X} |] ==> n \<noteq> n'"
by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)
-lemma Key_neq [dest]: "[| Key n' ~:used evs;
-Says A B X:set evs; Key n:parts {X} |] ==> n ~= n'"
+lemma Key_neq [dest]: "[| Key n' \<notin> used evs;
+Says A B X \<in> set evs; Key n \<in> parts {X} |] ==> n ~= n'"
by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)
subsubsection\<open>message of an event\<close>
@@ -623,7 +623,7 @@
| "msg (Gets A X) = X"
| "msg (Notes A X) = X"
-lemma used_sub_parts_used: "X:used (ev # evs) ==> X:parts {msg ev} Un used evs"
+lemma used_sub_parts_used: "X \<in> used (ev # evs) ==> X \<in> parts {msg ev} \<union> used evs"
by (induct ev, auto)
end
--- a/src/HOL/Auth/Guard/Guard.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Thu Feb 15 13:04:36 2018 +0100
@@ -13,82 +13,82 @@
******************************************************************************)
inductive_set
- guard :: "nat => key set => msg set"
+ guard :: "nat \<Rightarrow> key set \<Rightarrow> msg set"
for n :: nat and Ks :: "key set"
where
- No_Nonce [intro]: "Nonce n ~:parts {X} ==> X:guard n Ks"
-| Guard_Nonce [intro]: "invKey K:Ks ==> Crypt K X:guard n Ks"
-| Crypt [intro]: "X:guard n Ks ==> Crypt K X:guard n Ks"
-| Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> \<lbrace>X,Y\<rbrace> \<in> guard n Ks"
+ No_Nonce [intro]: "Nonce n \<notin> parts {X} \<Longrightarrow> X \<in> guard n Ks"
+| Guard_Nonce [intro]: "invKey K \<in> Ks \<Longrightarrow> Crypt K X \<in> guard n Ks"
+| Crypt [intro]: "X \<in> guard n Ks \<Longrightarrow> Crypt K X \<in> guard n Ks"
+| Pair [intro]: "[| X \<in> guard n Ks; Y \<in> guard n Ks |] ==> \<lbrace>X,Y\<rbrace> \<in> guard n Ks"
subsection\<open>basic facts about @{term guard}\<close>
-lemma Key_is_guard [iff]: "Key K:guard n Ks"
+lemma Key_is_guard [iff]: "Key K \<in> guard n Ks"
by auto
-lemma Agent_is_guard [iff]: "Agent A:guard n Ks"
+lemma Agent_is_guard [iff]: "Agent A \<in> guard n Ks"
by auto
-lemma Number_is_guard [iff]: "Number r:guard n Ks"
+lemma Number_is_guard [iff]: "Number r \<in> guard n Ks"
by auto
-lemma Nonce_notin_guard: "X:guard n Ks ==> X ~= Nonce n"
+lemma Nonce_notin_guard: "X \<in> guard n Ks \<Longrightarrow> X \<noteq> Nonce n"
by (erule guard.induct, auto)
-lemma Nonce_notin_guard_iff [iff]: "Nonce n ~:guard n Ks"
+lemma Nonce_notin_guard_iff [iff]: "Nonce n \<notin> guard n Ks"
by (auto dest: Nonce_notin_guard)
-lemma guard_has_Crypt [rule_format]: "X:guard n Ks ==> Nonce n:parts {X}
---> (EX K Y. Crypt K Y:kparts {X} & Nonce n:parts {Y})"
+lemma guard_has_Crypt [rule_format]: "X \<in> guard n Ks ==> Nonce n \<in> parts {X}
+\<longrightarrow> (\<exists>K Y. Crypt K Y \<in> kparts {X} \<and> Nonce n \<in> parts {Y})"
by (erule guard.induct, auto)
-lemma Nonce_notin_kparts_msg: "X:guard n Ks ==> Nonce n ~:kparts {X}"
+lemma Nonce_notin_kparts_msg: "X \<in> guard n Ks \<Longrightarrow> Nonce n \<notin> kparts {X}"
by (erule guard.induct, auto)
-lemma Nonce_in_kparts_imp_no_guard: "Nonce n:kparts H
-==> EX X. X:H & X ~:guard n Ks"
+lemma Nonce_in_kparts_imp_no_guard: "Nonce n \<in> kparts H
+\<Longrightarrow> \<exists>X. X \<in> H \<and> X \<notin> guard n Ks"
apply (drule in_kparts, clarify)
apply (rule_tac x=X in exI, clarify)
by (auto dest: Nonce_notin_kparts_msg)
-lemma guard_kparts [rule_format]: "X:guard n Ks ==>
-Y:kparts {X} --> Y:guard n Ks"
+lemma guard_kparts [rule_format]: "X \<in> guard n Ks \<Longrightarrow>
+Y \<in> kparts {X} \<longrightarrow> Y \<in> guard n Ks"
by (erule guard.induct, auto)
-lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks"
- by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI)
+lemma guard_Crypt: "[| Crypt K Y \<in> guard n Ks; K \<notin> invKey`Ks |] ==> Y \<in> guard n Ks"
+ by (ind_cases "Crypt K Y \<in> guard n Ks") (auto intro!: image_eqI)
lemma guard_MPair [iff]: "(\<lbrace>X,Y\<rbrace> \<in> guard n Ks) = (X \<in> guard n Ks \<and> Y \<in> guard n Ks)"
by (auto, (ind_cases "\<lbrace>X,Y\<rbrace> \<in> guard n Ks", auto)+)
-lemma guard_not_guard [rule_format]: "X:guard n Ks ==>
-Crypt K Y:kparts {X} --> Nonce n:kparts {Y} --> Y ~:guard n Ks"
+lemma guard_not_guard [rule_format]: "X \<in> guard n Ks \<Longrightarrow>
+Crypt K Y \<in> kparts {X} \<longrightarrow> Nonce n \<in> kparts {Y} \<longrightarrow> Y \<notin> guard n Ks"
by (erule guard.induct, auto dest: guard_kparts)
-lemma guard_extand: "[| X:guard n Ks; Ks <= Ks' |] ==> X:guard n Ks'"
+lemma guard_extand: "[| X \<in> guard n Ks; Ks \<subseteq> Ks' |] ==> X \<in> guard n Ks'"
by (erule guard.induct, auto)
subsection\<open>guarded sets\<close>
-definition Guard :: "nat => key set => msg set => bool" where
-"Guard n Ks H == ALL X. X:H --> X:guard n Ks"
+definition Guard :: "nat \<Rightarrow> key set \<Rightarrow> msg set \<Rightarrow> bool" where
+"Guard n Ks H \<equiv> \<forall>X. X \<in> H \<longrightarrow> X \<in> guard n Ks"
subsection\<open>basic facts about @{term Guard}\<close>
lemma Guard_empty [iff]: "Guard n Ks {}"
by (simp add: Guard_def)
-lemma notin_parts_Guard [intro]: "Nonce n ~:parts G ==> Guard n Ks G"
+lemma notin_parts_Guard [intro]: "Nonce n \<notin> parts G \<Longrightarrow> Guard n Ks G"
apply (unfold Guard_def, clarify)
-apply (subgoal_tac "Nonce n ~:parts {X}")
+apply (subgoal_tac "Nonce n \<notin> parts {X}")
by (auto dest: parts_sub)
-lemma Nonce_notin_kparts [simplified]: "Guard n Ks H ==> Nonce n ~:kparts H"
+lemma Nonce_notin_kparts [simplified]: "Guard n Ks H \<Longrightarrow> Nonce n \<notin> kparts H"
by (auto simp: Guard_def dest: in_kparts Nonce_notin_kparts_msg)
-lemma Guard_must_decrypt: "[| Guard n Ks H; Nonce n:analz H |] ==>
-EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H"
-apply (drule_tac P="%G. Nonce n:G" in analz_pparts_kparts_substD, simp)
+lemma Guard_must_decrypt: "[| Guard n Ks H; Nonce n \<in> analz H |] ==>
+\<exists>K Y. Crypt K Y \<in> kparts H \<and> Key (invKey K) \<in> kparts H"
+apply (drule_tac P="\<lambda>G. Nonce n \<in> G" in analz_pparts_kparts_substD, simp)
by (drule must_decrypt, auto dest: Nonce_notin_kparts)
lemma Guard_kparts [intro]: "Guard n Ks H ==> Guard n Ks (kparts H)"
@@ -98,7 +98,7 @@
by (auto simp: Guard_def)
lemma Guard_insert [iff]: "Guard n Ks (insert X H)
-= (Guard n Ks H & X:guard n Ks)"
+= (Guard n Ks H \<and> X \<in> guard n Ks)"
by (auto simp: Guard_def)
lemma Guard_Un [iff]: "Guard n Ks (G Un H) = (Guard n Ks G & Guard n Ks H)"
@@ -107,51 +107,51 @@
lemma Guard_synth [intro]: "Guard n Ks G ==> Guard n Ks (synth G)"
by (auto simp: Guard_def, erule synth.induct, auto)
-lemma Guard_analz [intro]: "[| Guard n Ks G; ALL K. K:Ks --> Key K ~:analz G |]
+lemma Guard_analz [intro]: "[| Guard n Ks G; \<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G |]
==> Guard n Ks (analz G)"
apply (auto simp: Guard_def)
apply (erule analz.induct, auto)
-by (ind_cases "Crypt K Xa:guard n Ks" for K Xa, auto)
+by (ind_cases "Crypt K Xa \<in> guard n Ks" for K Xa, auto)
-lemma in_Guard [dest]: "[| X:G; Guard n Ks G |] ==> X:guard n Ks"
+lemma in_Guard [dest]: "[| X \<in> G; Guard n Ks G |] ==> X \<in> guard n Ks"
by (auto simp: Guard_def)
-lemma in_synth_Guard: "[| X:synth G; Guard n Ks G |] ==> X:guard n Ks"
+lemma in_synth_Guard: "[| X \<in> synth G; Guard n Ks G |] ==> X \<in> guard n Ks"
by (drule Guard_synth, auto)
-lemma in_analz_Guard: "[| X:analz G; Guard n Ks G;
-ALL K. K:Ks --> Key K ~:analz G |] ==> X:guard n Ks"
+lemma in_analz_Guard: "[| X \<in> analz G; Guard n Ks G;
+\<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G |] ==> X \<in> guard n Ks"
by (drule Guard_analz, auto)
lemma Guard_keyset [simp]: "keyset G ==> Guard n Ks G"
by (auto simp: Guard_def)
-lemma Guard_Un_keyset: "[| Guard n Ks G; keyset H |] ==> Guard n Ks (G Un H)"
+lemma Guard_Un_keyset: "[| Guard n Ks G; keyset H |] ==> Guard n Ks (G \<union> H)"
by auto
-lemma in_Guard_kparts: "[| X:G; Guard n Ks G; Y:kparts {X} |] ==> Y:guard n Ks"
+lemma in_Guard_kparts: "[| X \<in> G; Guard n Ks G; Y \<in> kparts {X} |] ==> Y \<in> guard n Ks"
by blast
-lemma in_Guard_kparts_neq: "[| X:G; Guard n Ks G; Nonce n':kparts {X} |]
-==> n ~= n'"
+lemma in_Guard_kparts_neq: "[| X \<in> G; Guard n Ks G; Nonce n' \<in> kparts {X} |]
+==> n \<noteq> n'"
by (blast dest: in_Guard_kparts)
-lemma in_Guard_kparts_Crypt: "[| X:G; Guard n Ks G; is_MPair X;
-Crypt K Y:kparts {X}; Nonce n:kparts {Y} |] ==> invKey K:Ks"
+lemma in_Guard_kparts_Crypt: "[| X \<in> G; Guard n Ks G; is_MPair X;
+Crypt K Y \<in> kparts {X}; Nonce n \<in> kparts {Y} |] ==> invKey K \<in> Ks"
apply (drule in_Guard, simp)
apply (frule guard_not_guard, simp+)
apply (drule guard_kparts, simp)
-by (ind_cases "Crypt K Y:guard n Ks", auto)
+by (ind_cases "Crypt K Y \<in> guard n Ks", auto)
-lemma Guard_extand: "[| Guard n Ks G; Ks <= Ks' |] ==> Guard n Ks' G"
+lemma Guard_extand: "[| Guard n Ks G; Ks \<subseteq> Ks' |] ==> Guard n Ks' G"
by (auto simp: Guard_def dest: guard_extand)
-lemma guard_invKey [rule_format]: "[| X:guard n Ks; Nonce n:kparts {Y} |] ==>
-Crypt K Y:kparts {X} --> invKey K:Ks"
+lemma guard_invKey [rule_format]: "[| X \<in> guard n Ks; Nonce n \<in> kparts {Y} |] ==>
+Crypt K Y \<in> kparts {X} \<longrightarrow> invKey K \<in> Ks"
by (erule guard.induct, auto)
-lemma Crypt_guard_invKey [rule_format]: "[| Crypt K Y:guard n Ks;
-Nonce n:kparts {Y} |] ==> invKey K:Ks"
+lemma Crypt_guard_invKey [rule_format]: "[| Crypt K Y \<in> guard n Ks;
+Nonce n \<in> kparts {Y} |] ==> invKey K \<in> Ks"
by (auto dest: guard_invKey)
subsection\<open>set obtained by decrypting a message\<close>
@@ -160,14 +160,14 @@
decrypt :: "msg set => key => msg => msg set" where
"decrypt H K Y == insert Y (H - {Crypt K Y})"
-lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |]
-==> Nonce n:analz (decrypt H K Y)"
-apply (drule_tac P="%H. Nonce n:analz H" in ssubst [OF insert_Diff])
+lemma analz_decrypt: "[| Crypt K Y \<in> H; Key (invKey K) \<in> H; Nonce n \<in> analz H |]
+==> Nonce n \<in> analz (decrypt H K Y)"
+apply (drule_tac P="\<lambda>H. Nonce n \<in> analz H" in ssubst [OF insert_Diff])
apply assumption
apply (simp only: analz_Crypt_if, simp)
done
-lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
+lemma parts_decrypt: "[| Crypt K Y \<in> H; X \<in> parts (decrypt H K Y) |] ==> X \<in> parts H"
by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
subsection\<open>number of Crypt's in a message\<close>
@@ -180,7 +180,7 @@
subsection\<open>basic facts about @{term crypt_nb}\<close>
-lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
+lemma non_empty_crypt_msg: "Crypt K Y \<in> parts {X} \<Longrightarrow> crypt_nb X \<noteq> 0"
by (induct X, simp_all, safe, simp_all)
subsection\<open>number of Crypt's in a message list\<close>
@@ -206,16 +206,16 @@
apply simp
done
-lemma parts_cnb: "Z:parts (set l) ==>
+lemma parts_cnb: "Z \<in> parts (set l) \<Longrightarrow>
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
by (erule parts.induct, auto simp: in_set_conv_decomp)
-lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
+lemma non_empty_crypt: "Crypt K Y \<in> parts (set l) \<Longrightarrow> cnb l \<noteq> 0"
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
subsection\<open>list of kparts\<close>
-lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X"
+lemma kparts_msg_set: "\<exists>l. kparts {X} = set l \<and> cnb l = crypt_nb X"
apply (induct X, simp_all)
apply (rename_tac agent, rule_tac x="[Agent agent]" in exI, simp)
apply (rename_tac nat, rule_tac x="[Number nat]" in exI, simp)
@@ -225,11 +225,11 @@
apply (clarify, rule_tac x="l@la" in exI, simp)
by (clarify, rename_tac nat X y, rule_tac x="[Crypt nat X]" in exI, simp)
-lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
+lemma kparts_set: "\<exists>l'. kparts (set l) = set l' \<and> cnb l' = cnb l"
apply (induct l)
apply (rule_tac x="[]" in exI, simp, clarsimp)
apply (rename_tac a b l')
-apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
+apply (subgoal_tac "\<exists>l''. kparts {a} = set l'' \<and> cnb l'' = crypt_nb a", clarify)
apply (rule_tac x="l''@l'" in exI, simp)
apply (rule kparts_insert_substI, simp)
by (rule kparts_msg_set)
@@ -249,28 +249,28 @@
subsection\<open>if the analyse of a finite guarded set gives n then it must also gives
one of the keys of Ks\<close>
-lemma Guard_invKey_by_list [rule_format]: "ALL l. cnb l = p
---> Guard n Ks (set l) --> Nonce n:analz (set l)
---> (EX K. K:Ks & Key K:analz (set l))"
+lemma Guard_invKey_by_list [rule_format]: "\<forall>l. cnb l = p
+\<longrightarrow> Guard n Ks (set l) \<longrightarrow> Nonce n \<in> analz (set l)
+\<longrightarrow> (\<exists>K. K \<in> Ks \<and> Key K \<in> analz (set l))"
apply (induct p)
(* case p=0 *)
apply (clarify, drule Guard_must_decrypt, simp, clarify)
apply (drule kparts_parts, drule non_empty_crypt, simp)
(* case p>0 *)
apply (clarify, frule Guard_must_decrypt, simp, clarify)
-apply (drule_tac P="%G. Nonce n:G" in analz_pparts_kparts_substD, simp)
+apply (drule_tac P="\<lambda>G. Nonce n \<in> G" in analz_pparts_kparts_substD, simp)
apply (frule analz_decrypt, simp_all)
-apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp)
+apply (subgoal_tac "\<exists>l'. kparts (set l) = set l' \<and> cnb l' = cnb l", clarsimp)
apply (drule_tac G="insert Y (set l' - {Crypt K Y})"
and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus)
apply (rule_tac analz_pparts_kparts_substI, simp)
-apply (case_tac "K:invKey`Ks")
+apply (case_tac "K \<in> invKey`Ks")
(* K:invKey`Ks *)
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))")
apply (drule_tac x="decrypt' l' K Y" in spec, simp)
-apply (subgoal_tac "Crypt K Y:parts (set l)")
+apply (subgoal_tac "Crypt K Y \<in> parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
apply (rule insert_mono, rule set_remove)
@@ -286,21 +286,21 @@
apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
by (rule kparts_set)
-lemma Guard_invKey_finite: "[| Nonce n:analz G; Guard n Ks G; finite G |]
-==> EX K. K:Ks & Key K:analz G"
+lemma Guard_invKey_finite: "[| Nonce n \<in> analz G; Guard n Ks G; finite G |]
+==> \<exists>K. K \<in> Ks \<and> Key K \<in> analz G"
apply (drule finite_list, clarify)
by (rule Guard_invKey_by_list, auto)
-lemma Guard_invKey: "[| Nonce n:analz G; Guard n Ks G |]
-==> EX K. K:Ks & Key K:analz G"
+lemma Guard_invKey: "[| Nonce n \<in> analz G; Guard n Ks G |]
+==> \<exists>K. K \<in> Ks \<and> Key K \<in> analz G"
by (auto dest: analz_needs_only_finite Guard_invKey_finite)
subsection\<open>if the analyse of a finite guarded set and a (possibly infinite) set of keys
gives n then it must also gives Ks\<close>
-lemma Guard_invKey_keyset: "[| Nonce n:analz (G Un H); Guard n Ks G; finite G;
-keyset H |] ==> EX K. K:Ks & Key K:analz (G Un H)"
-apply (frule_tac P="%G. Nonce n:G" and G=G in analz_keyset_substD, simp_all)
+lemma Guard_invKey_keyset: "[| Nonce n \<in> analz (G \<union> H); Guard n Ks G; finite G;
+keyset H |] ==> \<exists>K. K \<in> Ks \<and> Key K \<in> analz (G \<union> H)"
+apply (frule_tac P="\<lambda>G. Nonce n \<in> G" and G=G in analz_keyset_substD, simp_all)
apply (drule_tac G="G Un (H Int keysfor G)" in Guard_invKey_finite)
by (auto simp: Guard_def intro: analz_sub)
--- a/src/HOL/Auth/Guard/GuardK.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Thu Feb 15 13:04:36 2018 +0100
@@ -23,149 +23,149 @@
guardK :: "nat => key set => msg set"
for n :: nat and Ks :: "key set"
where
- No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks"
-| Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks"
-| Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks"
-| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> \<lbrace>X,Y\<rbrace>:guardK n Ks"
+ No_Key [intro]: "Key n \<notin> parts {X} \<Longrightarrow> X \<in> guardK n Ks"
+| Guard_Key [intro]: "invKey K \<in> Ks ==> Crypt K X \<in> guardK n Ks"
+| Crypt [intro]: "X \<in> guardK n Ks \<Longrightarrow> Crypt K X \<in> guardK n Ks"
+| Pair [intro]: "[| X \<in> guardK n Ks; Y \<in> guardK n Ks |] ==> \<lbrace>X,Y\<rbrace> \<in> guardK n Ks"
subsection\<open>basic facts about @{term guardK}\<close>
-lemma Nonce_is_guardK [iff]: "Nonce p:guardK n Ks"
+lemma Nonce_is_guardK [iff]: "Nonce p \<in> guardK n Ks"
by auto
-lemma Agent_is_guardK [iff]: "Agent A:guardK n Ks"
+lemma Agent_is_guardK [iff]: "Agent A \<in> guardK n Ks"
by auto
-lemma Number_is_guardK [iff]: "Number r:guardK n Ks"
+lemma Number_is_guardK [iff]: "Number r \<in> guardK n Ks"
by auto
-lemma Key_notin_guardK: "X:guardK n Ks ==> X ~= Key n"
+lemma Key_notin_guardK: "X \<in> guardK n Ks \<Longrightarrow> X \<noteq> Key n"
by (erule guardK.induct, auto)
-lemma Key_notin_guardK_iff [iff]: "Key n ~:guardK n Ks"
+lemma Key_notin_guardK_iff [iff]: "Key n \<notin> guardK n Ks"
by (auto dest: Key_notin_guardK)
-lemma guardK_has_Crypt [rule_format]: "X:guardK n Ks ==> Key n:parts {X}
---> (EX K Y. Crypt K Y:kparts {X} & Key n:parts {Y})"
+lemma guardK_has_Crypt [rule_format]: "X \<in> guardK n Ks \<Longrightarrow> Key n \<in> parts {X}
+\<longrightarrow> (\<exists>K Y. Crypt K Y \<in> kparts {X} \<and> Key n \<in> parts {Y})"
by (erule guardK.induct, auto)
-lemma Key_notin_kparts_msg: "X:guardK n Ks ==> Key n ~:kparts {X}"
+lemma Key_notin_kparts_msg: "X \<in> guardK n Ks \<Longrightarrow> Key n \<notin> kparts {X}"
by (erule guardK.induct, auto dest: kparts_parts)
-lemma Key_in_kparts_imp_no_guardK: "Key n:kparts H
-==> EX X. X:H & X ~:guardK n Ks"
+lemma Key_in_kparts_imp_no_guardK: "Key n \<in> kparts H
+\<Longrightarrow> \<exists>X. X \<in> H \<and> X \<notin> guardK n Ks"
apply (drule in_kparts, clarify)
apply (rule_tac x=X in exI, clarify)
by (auto dest: Key_notin_kparts_msg)
-lemma guardK_kparts [rule_format]: "X:guardK n Ks ==>
-Y:kparts {X} --> Y:guardK n Ks"
+lemma guardK_kparts [rule_format]: "X \<in> guardK n Ks \<Longrightarrow>
+Y \<in> kparts {X} \<longrightarrow> Y \<in> guardK n Ks"
by (erule guardK.induct, auto dest: kparts_parts parts_sub)
-lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
- by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
+lemma guardK_Crypt: "[| Crypt K Y \<in> guardK n Ks; K \<notin> invKey`Ks |] ==> Y \<in> guardK n Ks"
+ by (ind_cases "Crypt K Y \<in> guardK n Ks") (auto intro!: image_eqI)
-lemma guardK_MPair [iff]: "(\<lbrace>X,Y\<rbrace>:guardK n Ks)
-= (X:guardK n Ks & Y:guardK n Ks)"
-by (auto, (ind_cases "\<lbrace>X,Y\<rbrace>:guardK n Ks", auto)+)
+lemma guardK_MPair [iff]: "(\<lbrace>X,Y\<rbrace> \<in> guardK n Ks)
+= (X \<in> guardK n Ks \<and> Y \<in> guardK n Ks)"
+by (auto, (ind_cases "\<lbrace>X,Y\<rbrace> \<in> guardK n Ks", auto)+)
-lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==>
-Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks"
+lemma guardK_not_guardK [rule_format]: "X \<in>guardK n Ks \<Longrightarrow>
+Crypt K Y \<in> kparts {X} \<longrightarrow> Key n \<in> kparts {Y} \<longrightarrow> Y \<notin> guardK n Ks"
by (erule guardK.induct, auto dest: guardK_kparts)
-lemma guardK_extand: "[| X:guardK n Ks; Ks <= Ks';
-[| K:Ks'; K ~:Ks |] ==> Key K ~:parts {X} |] ==> X:guardK n Ks'"
+lemma guardK_extand: "[| X \<in> guardK n Ks; Ks \<subseteq> Ks';
+[| K \<in> Ks'; K \<notin> Ks |] ==> Key K \<notin> parts {X} |] ==> X \<in> guardK n Ks'"
by (erule guardK.induct, auto)
subsection\<open>guarded sets\<close>
-definition GuardK :: "nat => key set => msg set => bool" where
-"GuardK n Ks H == ALL X. X:H --> X:guardK n Ks"
+definition GuardK :: "nat \<Rightarrow> key set \<Rightarrow> msg set \<Rightarrow> bool" where
+"GuardK n Ks H \<equiv> \<forall>X. X \<in> H \<longrightarrow> X \<in> guardK n Ks"
subsection\<open>basic facts about @{term GuardK}\<close>
lemma GuardK_empty [iff]: "GuardK n Ks {}"
by (simp add: GuardK_def)
-lemma Key_notin_kparts [simplified]: "GuardK n Ks H ==> Key n ~:kparts H"
+lemma Key_notin_kparts [simplified]: "GuardK n Ks H \<Longrightarrow> Key n \<notin> kparts H"
by (auto simp: GuardK_def dest: in_kparts Key_notin_kparts_msg)
-lemma GuardK_must_decrypt: "[| GuardK n Ks H; Key n:analz H |] ==>
-EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H"
-apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp)
+lemma GuardK_must_decrypt: "[| GuardK n Ks H; Key n \<in> analz H |] ==>
+\<exists>K Y. Crypt K Y \<in> kparts H \<and> Key (invKey K) \<in> kparts H"
+apply (drule_tac P="\<lambda>G. Key n \<in> G" in analz_pparts_kparts_substD, simp)
by (drule must_decrypt, auto dest: Key_notin_kparts)
-lemma GuardK_kparts [intro]: "GuardK n Ks H ==> GuardK n Ks (kparts H)"
+lemma GuardK_kparts [intro]: "GuardK n Ks H \<Longrightarrow> GuardK n Ks (kparts H)"
by (auto simp: GuardK_def dest: in_kparts guardK_kparts)
-lemma GuardK_mono: "[| GuardK n Ks H; G <= H |] ==> GuardK n Ks G"
+lemma GuardK_mono: "[| GuardK n Ks H; G \<subseteq> H |] ==> GuardK n Ks G"
by (auto simp: GuardK_def)
lemma GuardK_insert [iff]: "GuardK n Ks (insert X H)
-= (GuardK n Ks H & X:guardK n Ks)"
+= (GuardK n Ks H \<and> X \<in> guardK n Ks)"
by (auto simp: GuardK_def)
lemma GuardK_Un [iff]: "GuardK n Ks (G Un H) = (GuardK n Ks G & GuardK n Ks H)"
by (auto simp: GuardK_def)
-lemma GuardK_synth [intro]: "GuardK n Ks G ==> GuardK n Ks (synth G)"
+lemma GuardK_synth [intro]: "GuardK n Ks G \<Longrightarrow> GuardK n Ks (synth G)"
by (auto simp: GuardK_def, erule synth.induct, auto)
-lemma GuardK_analz [intro]: "[| GuardK n Ks G; ALL K. K:Ks --> Key K ~:analz G |]
+lemma GuardK_analz [intro]: "[| GuardK n Ks G; \<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G |]
==> GuardK n Ks (analz G)"
apply (auto simp: GuardK_def)
apply (erule analz.induct, auto)
-by (ind_cases "Crypt K Xa:guardK n Ks" for K Xa, auto)
+by (ind_cases "Crypt K Xa \<in> guardK n Ks" for K Xa, auto)
-lemma in_GuardK [dest]: "[| X:G; GuardK n Ks G |] ==> X:guardK n Ks"
+lemma in_GuardK [dest]: "[| X \<in> G; GuardK n Ks G |] ==> X \<in> guardK n Ks"
by (auto simp: GuardK_def)
-lemma in_synth_GuardK: "[| X:synth G; GuardK n Ks G |] ==> X:guardK n Ks"
+lemma in_synth_GuardK: "[| X \<in> synth G; GuardK n Ks G |] ==> X \<in> guardK n Ks"
by (drule GuardK_synth, auto)
-lemma in_analz_GuardK: "[| X:analz G; GuardK n Ks G;
-ALL K. K:Ks --> Key K ~:analz G |] ==> X:guardK n Ks"
+lemma in_analz_GuardK: "[| X \<in> analz G; GuardK n Ks G;
+\<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G |] ==> X \<in> guardK n Ks"
by (drule GuardK_analz, auto)
-lemma GuardK_keyset [simp]: "[| keyset G; Key n ~:G |] ==> GuardK n Ks G"
+lemma GuardK_keyset [simp]: "[| keyset G; Key n \<notin> G |] ==> GuardK n Ks G"
by (simp only: GuardK_def, clarify, drule keyset_in, auto)
-lemma GuardK_Un_keyset: "[| GuardK n Ks G; keyset H; Key n ~:H |]
+lemma GuardK_Un_keyset: "[| GuardK n Ks G; keyset H; Key n \<notin> H |]
==> GuardK n Ks (G Un H)"
by auto
-lemma in_GuardK_kparts: "[| X:G; GuardK n Ks G; Y:kparts {X} |] ==> Y:guardK n Ks"
+lemma in_GuardK_kparts: "[| X \<in> G; GuardK n Ks G; Y \<in> kparts {X} |] ==> Y \<in> guardK n Ks"
by blast
-lemma in_GuardK_kparts_neq: "[| X:G; GuardK n Ks G; Key n':kparts {X} |]
-==> n ~= n'"
+lemma in_GuardK_kparts_neq: "[| X \<in> G; GuardK n Ks G; Key n' \<in> kparts {X} |]
+==> n \<noteq> n'"
by (blast dest: in_GuardK_kparts)
-lemma in_GuardK_kparts_Crypt: "[| X:G; GuardK n Ks G; is_MPair X;
-Crypt K Y:kparts {X}; Key n:kparts {Y} |] ==> invKey K:Ks"
+lemma in_GuardK_kparts_Crypt: "[| X \<in> G; GuardK n Ks G; is_MPair X;
+Crypt K Y \<in> kparts {X}; Key n \<in> kparts {Y} |] ==> invKey K \<in> Ks"
apply (drule in_GuardK, simp)
apply (frule guardK_not_guardK, simp+)
apply (drule guardK_kparts, simp)
-by (ind_cases "Crypt K Y:guardK n Ks", auto)
+by (ind_cases "Crypt K Y \<in> guardK n Ks", auto)
-lemma GuardK_extand: "[| GuardK n Ks G; Ks <= Ks';
-[| K:Ks'; K ~:Ks |] ==> Key K ~:parts G |] ==> GuardK n Ks' G"
+lemma GuardK_extand: "[| GuardK n Ks G; Ks \<subseteq> Ks';
+[| K \<in> Ks'; K \<notin> Ks |] ==> Key K \<notin> parts G |] ==> GuardK n Ks' G"
by (auto simp: GuardK_def dest: guardK_extand parts_sub)
subsection\<open>set obtained by decrypting a message\<close>
abbreviation (input)
- decrypt :: "msg set => key => msg => msg set" where
- "decrypt H K Y == insert Y (H - {Crypt K Y})"
+ decrypt :: "msg set \<Rightarrow> key \<Rightarrow> msg \<Rightarrow> msg set" where
+ "decrypt H K Y \<equiv> insert Y (H - {Crypt K Y})"
-lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
-==> Key n:analz (decrypt H K Y)"
-apply (drule_tac P="%H. Key n:analz H" in ssubst [OF insert_Diff])
+lemma analz_decrypt: "[| Crypt K Y \<in> H; Key (invKey K) \<in> H; Key n \<in> analz H |]
+==> Key n \<in> analz (decrypt H K Y)"
+apply (drule_tac P="\<lambda>H. Key n \<in> analz H" in ssubst [OF insert_Diff])
apply assumption
apply (simp only: analz_Crypt_if, simp)
done
-lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
+lemma parts_decrypt: "[| Crypt K Y \<in> H; X \<in> parts (decrypt H K Y) |] ==> X \<in> parts H"
by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
subsection\<open>number of Crypt's in a message\<close>
@@ -177,7 +177,7 @@
subsection\<open>basic facts about @{term crypt_nb}\<close>
-lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
+lemma non_empty_crypt_msg: "Crypt K Y \<in> parts {X} \<Longrightarrow> crypt_nb X \<noteq> 0"
by (induct X, simp_all, safe, simp_all)
subsection\<open>number of Crypt's in a message list\<close>
@@ -200,16 +200,16 @@
apply (induct l, auto)
by (erule_tac l=l and x=x in mem_cnb_minus_substI, simp)
-lemma parts_cnb: "Z:parts (set l) ==>
+lemma parts_cnb: "Z \<in> parts (set l) \<Longrightarrow>
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
by (erule parts.induct, auto simp: in_set_conv_decomp)
-lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
+lemma non_empty_crypt: "Crypt K Y \<in> parts (set l) \<Longrightarrow> cnb l \<noteq> 0"
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
subsection\<open>list of kparts\<close>
-lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X"
+lemma kparts_msg_set: "\<exists>l. kparts {X} = set l \<and> cnb l = crypt_nb X"
apply (induct X, simp_all)
apply (rename_tac agent, rule_tac x="[Agent agent]" in exI, simp)
apply (rename_tac nat, rule_tac x="[Number nat]" in exI, simp)
@@ -219,11 +219,11 @@
apply (clarify, rule_tac x="l@la" in exI, simp)
by (clarify, rename_tac nat X y, rule_tac x="[Crypt nat X]" in exI, simp)
-lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
+lemma kparts_set: "\<exists>l'. kparts (set l) = set l' & cnb l' = cnb l"
apply (induct l)
apply (rule_tac x="[]" in exI, simp, clarsimp)
apply (rename_tac a b l')
-apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
+apply (subgoal_tac "\<exists>l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
apply (rule_tac x="l''@l'" in exI, simp)
apply (rule kparts_insert_substI, simp)
by (rule kparts_msg_set)
@@ -243,28 +243,28 @@
text\<open>if the analysis of a finite guarded set gives n then it must also give
one of the keys of Ks\<close>
-lemma GuardK_invKey_by_list [rule_format]: "ALL l. cnb l = p
---> GuardK n Ks (set l) --> Key n:analz (set l)
---> (EX K. K:Ks & Key K:analz (set l))"
+lemma GuardK_invKey_by_list [rule_format]: "\<forall>l. cnb l = p
+\<longrightarrow> GuardK n Ks (set l) \<longrightarrow> Key n \<in> analz (set l)
+\<longrightarrow> (\<exists>K. K \<in> Ks \<and> Key K \<in> analz (set l))"
apply (induct p)
(* case p=0 *)
apply (clarify, drule GuardK_must_decrypt, simp, clarify)
apply (drule kparts_parts, drule non_empty_crypt, simp)
(* case p>0 *)
apply (clarify, frule GuardK_must_decrypt, simp, clarify)
-apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp)
+apply (drule_tac P="\<lambda>G. Key n \<in> G" in analz_pparts_kparts_substD, simp)
apply (frule analz_decrypt, simp_all)
-apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp)
+apply (subgoal_tac "\<exists>l'. kparts (set l) = set l' \<and> cnb l' = cnb l", clarsimp)
apply (drule_tac G="insert Y (set l' - {Crypt K Y})"
and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus)
apply (rule_tac analz_pparts_kparts_substI, simp)
-apply (case_tac "K:invKey`Ks")
+apply (case_tac "K \<in> invKey`Ks")
(* K:invKey`Ks *)
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
apply (drule_tac x="decrypt' l' K Y" in spec, simp)
-apply (subgoal_tac "Crypt K Y:parts (set l)")
+apply (subgoal_tac "Crypt K Y \<in> parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
apply (rule insert_mono, rule set_remove)
@@ -280,21 +280,21 @@
apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
by (rule kparts_set)
-lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |]
-==> EX K. K:Ks & Key K:analz G"
+lemma GuardK_invKey_finite: "[| Key n \<in> analz G; GuardK n Ks G; finite G |]
+==> \<exists>K. K \<in> Ks \<and> Key K \<in> analz G"
apply (drule finite_list, clarify)
by (rule GuardK_invKey_by_list, auto)
-lemma GuardK_invKey: "[| Key n:analz G; GuardK n Ks G |]
-==> EX K. K:Ks & Key K:analz G"
+lemma GuardK_invKey: "[| Key n \<in> analz G; GuardK n Ks G |]
+==> \<exists>K. K \<in> Ks \<and> Key K \<in> analz G"
by (auto dest: analz_needs_only_finite GuardK_invKey_finite)
text\<open>if the analyse of a finite guarded set and a (possibly infinite) set of
keys gives n then it must also gives Ks\<close>
-lemma GuardK_invKey_keyset: "[| Key n:analz (G Un H); GuardK n Ks G; finite G;
-keyset H; Key n ~:H |] ==> EX K. K:Ks & Key K:analz (G Un H)"
-apply (frule_tac P="%G. Key n:G" and G=G in analz_keyset_substD, simp_all)
+lemma GuardK_invKey_keyset: "[| Key n \<in> analz (G \<union> H); GuardK n Ks G; finite G;
+keyset H; Key n \<notin> H |] ==> \<exists>K. K \<in> Ks \<and> Key K \<in> analz (G \<union> H)"
+apply (frule_tac P="\<lambda>G. Key n \<in> G" and G=G in analz_keyset_substD, simp_all)
apply (drule_tac G="G Un (H Int keysfor G)" in GuardK_invKey_finite)
apply (auto simp: GuardK_def intro: analz_sub)
by (drule keyset_in, auto)
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Thu Feb 15 13:04:36 2018 +0100
@@ -37,17 +37,17 @@
inductive_set nsp :: "event list set"
where
- Nil: "[]:nsp"
+ Nil: "[] \<in> nsp"
-| Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
+| Fake: "[| evs \<in> nsp; X \<in> synth (analz (spies evs)) |] ==> Says Spy B X # evs \<in> nsp"
-| NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
+| NS1: "[| evs1 \<in> nsp; Nonce NA \<notin> used evs1 |] ==> ns1 A B NA # evs1 \<in> nsp"
-| NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
- ns2 B A NA NB # evs2:nsp"
+| NS2: "[| evs2 \<in> nsp; Nonce NB \<notin> used evs2; ns1' A' A B NA \<in> set evs2 |] ==>
+ ns2 B A NA NB # evs2 \<in> nsp"
-| NS3: "!!A B B' NA NB evs3. [| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
- ns3 A B NB # evs3:nsp"
+| NS3: "\<And>A B B' NA NB evs3. [| evs3 \<in> nsp; ns1 A B NA \<in> set evs3; ns2' B' B A NA NB \<in> set evs3 |] ==>
+ ns3 A B NB # evs3 \<in> nsp"
subsection\<open>declarations for tactics\<close>
@@ -57,17 +57,17 @@
subsection\<open>general properties of nsp\<close>
-lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
+lemma nsp_has_no_Gets: "evs \<in> nsp \<Longrightarrow> \<forall>A X. Gets A X \<notin> set evs"
by (erule nsp.induct, auto)
lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
lemma nsp_is_one_step [iff]: "one_step nsp"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp" for ev evs, auto)
+by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> nsp" for ev evs, auto)
-lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
+lemma nsp_has_only_Says' [rule_format]: "evs \<in> nsp \<Longrightarrow>
+ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
by (erule nsp.induct, auto)
lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
@@ -79,37 +79,37 @@
subsection\<open>nonce are used only once\<close>
-lemma NA_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
---> Crypt (pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace>:parts (spies evs)
---> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
+lemma NA_is_uniq [rule_format]: "evs \<in> nsp \<Longrightarrow>
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Crypt (pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Nonce NA \<notin> analz (spies evs) \<longrightarrow> A=A' \<and> B=B'"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
-lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
-Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace>:parts (spies evs)
---> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
---> Nonce NA:analz (spies evs)"
+lemma no_Nonce_NS1_NS2 [rule_format]: "evs \<in> nsp \<Longrightarrow>
+Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Nonce NA \<in> analz (spies evs)"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
lemma no_Nonce_NS1_NS2' [rule_format]:
-"[| Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace>:parts (spies evs);
-Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs); evs:nsp |]
-==> Nonce NA:analz (spies evs)"
+"[| Crypt (pubK B') \<lbrace>Nonce NA', Nonce NA, Agent A'\<rbrace> \<in> parts (spies evs);
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs); evs \<in> nsp |]
+==> Nonce NA \<in> analz (spies evs)"
by (rule no_Nonce_NS1_NS2, auto)
-lemma NB_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>:parts (spies evs)
---> Crypt (pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace>:parts (spies evs)
---> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
+lemma NB_is_uniq [rule_format]: "evs \<in> nsp \<Longrightarrow>
+Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Crypt (pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Nonce NB \<notin> analz (spies evs) \<longrightarrow> A=A' \<and> B=B' \<and> NA=NA'"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
subsection\<open>guardedness of NA\<close>
-lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
+lemma ns1_imp_Guard [rule_format]: "[| evs \<in> nsp; A \<notin> bad; B \<notin> bad |] ==>
+ns1 A B NA \<in> set evs \<longrightarrow> Guard NA {priK A,priK B} (spies evs)"
apply (erule nsp.induct)
(* Nil *)
apply simp_all
@@ -135,8 +135,8 @@
subsection\<open>guardedness of NB\<close>
-lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)"
+lemma ns2_imp_Guard [rule_format]: "[| evs \<in> nsp; A \<notin> bad; B \<notin> bad |] ==>
+ns2 B A NA NB \<in> set evs \<longrightarrow> Guard NB {priK A,priK B} (spies evs)"
apply (erule nsp.induct)
(* Nil *)
apply simp_all
@@ -165,15 +165,15 @@
subsection\<open>Agents' Authentication\<close>
-lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>:parts (spies evs)
---> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
+lemma B_trusts_NS1: "[| evs \<in> nsp; A \<notin> bad; B \<notin> bad |] ==>
+Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Nonce NA \<notin> analz (spies evs) \<longrightarrow> ns1 A B NA \<in> set evs"
apply (erule nsp.induct, simp_all)
by (blast intro: analz_insertI)+
-lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
---> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>:parts (spies evs)
---> ns2 B A NA NB:set evs"
+lemma A_trusts_NS2: "[| evs \<in> nsp; A \<notin> bad; B \<notin> bad |] ==> ns1 A B NA \<in> set evs
+\<longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> ns2 B A NA NB \<in> set evs"
apply (erule nsp.induct, simp_all, safe)
apply (frule_tac B=B in ns1_imp_Guard, simp+)
apply (drule Guard_Nonce_analz, simp+, blast)
@@ -182,8 +182,8 @@
apply (frule_tac B=B in ns1_imp_Guard, simp+)
by (drule Guard_Nonce_analz, simp+, blast+)
-lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
---> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
+lemma B_trusts_NS3: "[| evs \<in> nsp; A \<notin> bad; B \<notin> bad |] ==> ns2 B A NA NB \<in> set evs
+\<longrightarrow> Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow> ns3 A B NB \<in> set evs"
apply (erule nsp.induct, simp_all, safe)
apply (frule_tac B=B in ns2_imp_Guard, simp+)
apply (drule Guard_Nonce_analz, simp+, blast)
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Thu Feb 15 13:04:36 2018 +0100
@@ -59,20 +59,20 @@
inductive_set or :: "event list set"
where
- Nil: "[]:or"
+ Nil: "[] \<in> or"
-| Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or"
+| Fake: "[| evs \<in> or; X \<in> synth (analz (spies evs)) |] ==> Says Spy B X # evs \<in> or"
-| OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or"
+| OR1: "[| evs1 \<in> or; Nonce NA \<notin> used evs1 |] ==> or1 A B NA # evs1 \<in> or"
-| OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |]
- ==> or2 A B NA NB X # evs2:or"
+| OR2: "[| evs2 \<in> or; or1' A' A B NA X \<in> set evs2; Nonce NB \<notin> used evs2 |]
+ ==> or2 A B NA NB X # evs2 \<in> or"
-| OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
- ==> or3 A B NA NB K # evs3:or"
+| OR3: "[| evs3 \<in> or; or2' B' A B NA NB \<in> set evs3; Key K \<notin> used evs3 |]
+ ==> or3 A B NA NB K # evs3 \<in> or"
-| OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |]
- ==> or4 A B NA X # evs4:or"
+| OR4: "[| evs4 \<in> or; or2 A B NA NB X \<in> set evs4; or3' S Y A B NA NB K \<in> set evs4 |]
+ ==> or4 A B NA X # evs4 \<in> or"
subsection\<open>declarations for tactics\<close>
@@ -82,17 +82,17 @@
subsection\<open>general properties of or\<close>
-lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs"
+lemma or_has_no_Gets: "evs \<in> or \<Longrightarrow> \<forall>A X. Gets A X \<notin> set evs"
by (erule or.induct, auto)
lemma or_is_Gets_correct [iff]: "Gets_correct or"
by (auto simp: Gets_correct_def dest: or_has_no_Gets)
lemma or_is_one_step [iff]: "one_step or"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:or" for ev evs, auto)
+by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> or" for ev evs, auto)
-lemma or_has_only_Says' [rule_format]: "evs:or ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
+lemma or_has_only_Says' [rule_format]: "evs \<in> or \<Longrightarrow>
+ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
by (erule or.induct, auto)
lemma or_has_only_Says [iff]: "has_only_Says or"
@@ -100,16 +100,16 @@
subsection\<open>or is regular\<close>
-lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs
-==> X:parts (spies evs)"
+lemma or1'_parts_spies [dest]: "or1' A' A B NA X \<in> set evs
+\<Longrightarrow> X \<in> parts (spies evs)"
by blast
-lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs
-==> X:parts (spies evs)"
+lemma or2_parts_spies [dest]: "or2 A B NA NB X \<in> set evs
+\<Longrightarrow> X \<in> parts (spies evs)"
by blast
-lemma or3_parts_spies [dest]: "Says S B \<lbrace>NA, Y, Ciph B \<lbrace>NB, K\<rbrace>\<rbrace>:set evs
-==> K:parts (spies evs)"
+lemma or3_parts_spies [dest]: "Says S B \<lbrace>NA, Y, Ciph B \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs
+\<Longrightarrow> K \<in> parts (spies evs)"
by blast
lemma or_is_regular [iff]: "regular or"
@@ -119,8 +119,8 @@
subsection\<open>guardedness of KAB\<close>
-lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==>
-or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)"
+lemma Guard_KAB [rule_format]: "[| evs \<in> or; A \<notin> bad; B \<notin> bad |] ==>
+or3 A B NA NB K \<in> set evs \<longrightarrow> GuardK K {shrK A,shrK B} (spies evs)"
apply (erule or.induct)
(* Nil *)
apply simp_all
@@ -140,8 +140,8 @@
subsection\<open>guardedness of NB\<close>
-lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==>
-or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)"
+lemma Guard_NB [rule_format]: "[| evs \<in> or; B \<notin> bad |] ==>
+or2 A B NA NB X \<in> set evs \<longrightarrow> Guard NB {shrK B} (spies evs)"
apply (erule or.induct)
(* Nil *)
apply simp_all
--- a/src/HOL/Auth/Guard/Guard_Public.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Thu Feb 15 13:04:36 2018 +0100
@@ -22,7 +22,7 @@
subsubsection\<open>agent associated to a key\<close>
definition agt :: "key => agent" where
-"agt K == @A. K = priK A | K = pubK A"
+"agt K == SOME A. K = priK A | K = pubK A"
lemma agt_priK [simp]: "agt (priK A) = A"
by (simp add: agt_def)
@@ -32,18 +32,18 @@
subsubsection\<open>basic facts about @{term initState}\<close>
-lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
+lemma no_Crypt_in_parts_init [simp]: "Crypt K X \<notin> parts (initState A)"
by (cases A, auto simp: initState.simps)
-lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"
+lemma no_Crypt_in_analz_init [simp]: "Crypt K X \<notin> analz (initState A)"
by auto
-lemma no_priK_in_analz_init [simp]: "A ~:bad
-==> Key (priK A) ~:analz (initState Spy)"
+lemma no_priK_in_analz_init [simp]: "A \<notin> bad
+\<Longrightarrow> Key (priK A) \<notin> analz (initState Spy)"
by (auto simp: initState.simps)
-lemma priK_notin_initState_Friend [simp]: "A ~= Friend C
-==> Key (priK A) ~: parts (initState (Friend C))"
+lemma priK_notin_initState_Friend [simp]: "A \<noteq> Friend C
+\<Longrightarrow> Key (priK A) \<notin> parts (initState (Friend C))"
by (auto simp: initState.simps)
lemma keyset_init [iff]: "keyset (initState A)"
@@ -52,9 +52,9 @@
subsubsection\<open>sets of private keys\<close>
definition priK_set :: "key set => bool" where
-"priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)"
+"priK_set Ks \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> (\<exists>A. K = priK A)"
-lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A"
+lemma in_priK_set: "[| priK_set Ks; K \<in> Ks |] ==> \<exists>A. K = priK A"
by (simp add: priK_set_def)
lemma priK_set1 [iff]: "priK_set {priK A}"
@@ -66,15 +66,15 @@
subsubsection\<open>sets of good keys\<close>
definition good :: "key set => bool" where
-"good Ks == ALL K. K:Ks --> agt K ~:bad"
+"good Ks == \<forall>K. K \<in> Ks \<longrightarrow> agt K \<notin> bad"
-lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
+lemma in_good: "[| good Ks; K \<in> Ks |] ==> agt K \<notin> bad"
by (simp add: good_def)
-lemma good1 [simp]: "A ~:bad ==> good {priK A}"
+lemma good1 [simp]: "A \<notin> bad \<Longrightarrow> good {priK A}"
by (simp add: good_def)
-lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {priK A, priK B}"
+lemma good2 [simp]: "[| A \<notin> bad; B \<notin> bad |] ==> good {priK A, priK B}"
by (simp add: good_def)
subsubsection\<open>greatest nonce used in a trace, 0 if there is no nonce\<close>
@@ -84,7 +84,7 @@
"greatest [] = 0"
| "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
-lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs"
+lemma greatest_is_greatest: "Nonce n \<in> used evs \<Longrightarrow> n \<le> greatest evs"
apply (induct evs, auto simp: initState.simps)
apply (drule used_sub_parts_used, safe)
apply (drule greatest_msg_is_greatest, arith)
@@ -92,10 +92,10 @@
subsubsection\<open>function giving a new nonce\<close>
-definition new :: "event list => nat" where
-"new evs == Suc (greatest evs)"
+definition new :: "event list \<Rightarrow> nat" where
+"new evs \<equiv> Suc (greatest evs)"
-lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs"
+lemma new_isnt_used [iff]: "Nonce (new evs) \<notin> used evs"
by (clarify, drule greatest_is_greatest, auto simp: new_def)
subsection\<open>Proofs About Guarded Messages\<close>
@@ -109,13 +109,13 @@
lemmas invKey_invKey_substI = invKey [THEN ssubst]
-lemma "Nonce n:parts {X} ==> Crypt (pubK A) X:guard n {priK A}"
+lemma "Nonce n \<in> parts {X} \<Longrightarrow> Crypt (pubK A) X \<in> guard n {priK A}"
apply (rule pubK_is_invKey_priK_substI, rule invKey_invKey_substI)
by (rule Guard_Nonce, simp+)
subsubsection\<open>guardedness results\<close>
-lemma sign_guard [intro]: "X:guard n Ks ==> sign A X:guard n Ks"
+lemma sign_guard [intro]: "X \<in> guard n Ks \<Longrightarrow> sign A X \<in> guard n Ks"
by (auto simp: sign_def)
lemma Guard_init [iff]: "Guard n Ks (initState B)"
@@ -125,38 +125,38 @@
==> Guard n Ks (knows_max C evs)"
by (simp add: knows_max_def)
-lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs
-==> Guard n Ks (spies evs)"
+lemma Nonce_not_used_Guard_spies [dest]: "Nonce n \<notin> used evs
+\<Longrightarrow> Guard n Ks (spies evs)"
by (auto simp: Guard_def dest: not_used_not_known parts_sub)
-lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)"
by (auto simp: Guard_def dest: known_used parts_trans)
-lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard_max [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)"
by (auto simp: Guard_def dest: known_max_used parts_trans)
-lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard_max' [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)"
apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono)
by (auto simp: knows_max_def)
subsubsection\<open>regular protocols\<close>
-definition regular :: "event list set => bool" where
-"regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)"
+definition regular :: "event list set \<Rightarrow> bool" where
+"regular p \<equiv> \<forall>evs A. evs \<in> p \<longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
-lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>
-(Key (priK A):parts (spies evs)) = (A:bad)"
+lemma priK_parts_iff_bad [simp]: "[| evs \<in> p; regular p |] ==>
+(Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
by (auto simp: regular_def)
-lemma priK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==>
-(Key (priK A):analz (spies evs)) = (A:bad)"
+lemma priK_analz_iff_bad [simp]: "[| evs \<in> p; regular p |] ==>
+(Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
-lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p;
-priK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)"
+lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs \<in> p;
+priK_set Ks; good Ks; regular p |] ==> Nonce n \<notin> analz (spies evs)"
apply (clarify, simp only: knows_decomp)
apply (drule Guard_invKey_keyset, simp+, safe)
apply (drule in_good, simp)
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Thu Feb 15 13:04:36 2018 +0100
@@ -20,25 +20,25 @@
subsubsection\<open>agent associated to a key\<close>
definition agt :: "key => agent" where
-"agt K == @A. K = shrK A"
+"agt K == SOME A. K = shrK A"
lemma agt_shrK [simp]: "agt (shrK A) = A"
by (simp add: agt_def)
subsubsection\<open>basic facts about @{term initState}\<close>
-lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
+lemma no_Crypt_in_parts_init [simp]: "Crypt K X \<notin> parts (initState A)"
by (cases A, auto simp: initState.simps)
-lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"
+lemma no_Crypt_in_analz_init [simp]: "Crypt K X \<notin> analz (initState A)"
by auto
-lemma no_shrK_in_analz_init [simp]: "A ~:bad
-==> Key (shrK A) ~:analz (initState Spy)"
+lemma no_shrK_in_analz_init [simp]: "A \<notin> bad
+\<Longrightarrow> Key (shrK A) \<notin> analz (initState Spy)"
by (auto simp: initState.simps)
-lemma shrK_notin_initState_Friend [simp]: "A ~= Friend C
-==> Key (shrK A) ~: parts (initState (Friend C))"
+lemma shrK_notin_initState_Friend [simp]: "A \<noteq> Friend C
+\<Longrightarrow> Key (shrK A) \<notin> parts (initState (Friend C))"
by (auto simp: initState.simps)
lemma keyset_init [iff]: "keyset (initState A)"
@@ -47,9 +47,9 @@
subsubsection\<open>sets of symmetric keys\<close>
definition shrK_set :: "key set => bool" where
-"shrK_set Ks == ALL K. K:Ks --> (EX A. K = shrK A)"
+"shrK_set Ks \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> (\<exists>A. K = shrK A)"
-lemma in_shrK_set: "[| shrK_set Ks; K:Ks |] ==> EX A. K = shrK A"
+lemma in_shrK_set: "[| shrK_set Ks; K \<in> Ks |] ==> \<exists>A. K = shrK A"
by (simp add: shrK_set_def)
lemma shrK_set1 [iff]: "shrK_set {shrK A}"
@@ -60,16 +60,16 @@
subsubsection\<open>sets of good keys\<close>
-definition good :: "key set => bool" where
-"good Ks == ALL K. K:Ks --> agt K ~:bad"
+definition good :: "key set \<Rightarrow> bool" where
+"good Ks \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> agt K \<notin> bad"
-lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
+lemma in_good: "[| good Ks; K \<in> Ks |] ==> agt K \<notin> bad"
by (simp add: good_def)
-lemma good1 [simp]: "A ~:bad ==> good {shrK A}"
+lemma good1 [simp]: "A \<notin> bad \<Longrightarrow> good {shrK A}"
by (simp add: good_def)
-lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {shrK A, shrK B}"
+lemma good2 [simp]: "[| A \<notin> bad; B \<notin> bad |] ==> good {shrK A, shrK B}"
by (simp add: good_def)
@@ -84,16 +84,16 @@
lemmas invKey_invKey_substI = invKey [THEN ssubst]
-lemma "Nonce n:parts {X} ==> Crypt (shrK A) X:guard n {shrK A}"
+lemma "Nonce n \<in> parts {X} \<Longrightarrow> Crypt (shrK A) X \<in> guard n {shrK A}"
apply (rule shrK_is_invKey_shrK_substI, rule invKey_invKey_substI)
by (rule Guard_Nonce, simp+)
subsubsection\<open>guardedness results on nonces\<close>
-lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guard n Ks"
+lemma guard_ciph [simp]: "shrK A \<in> Ks \<Longrightarrow> Ciph A X \<in> guard n Ks"
by (rule Guard_Nonce, simp)
-lemma guardK_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks"
+lemma guardK_ciph [simp]: "shrK A \<in> Ks \<Longrightarrow> Ciph A X \<in> guardK n Ks"
by (rule Guard_Key, simp)
lemma Guard_init [iff]: "Guard n Ks (initState B)"
@@ -103,45 +103,45 @@
==> Guard n Ks (knows_max C evs)"
by (simp add: knows_max_def)
-lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs
-==> Guard n Ks (spies evs)"
+lemma Nonce_not_used_Guard_spies [dest]: "Nonce n \<notin> used evs
+\<Longrightarrow> Guard n Ks (spies evs)"
by (auto simp: Guard_def dest: not_used_not_known parts_sub)
-lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)"
by (auto simp: Guard_def dest: known_used parts_trans)
-lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard_max [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)"
by (auto simp: Guard_def dest: known_max_used parts_trans)
-lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard_max' [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)"
apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono)
by (auto simp: knows_max_def)
subsubsection\<open>guardedness results on keys\<close>
-lemma GuardK_init [simp]: "n ~:range shrK ==> GuardK n Ks (initState B)"
+lemma GuardK_init [simp]: "n \<notin> range shrK \<Longrightarrow> GuardK n Ks (initState B)"
by (induct B, auto simp: GuardK_def initState.simps)
-lemma GuardK_knows_max': "[| GuardK n A (knows_max' C evs); n ~:range shrK |]
+lemma GuardK_knows_max': "[| GuardK n A (knows_max' C evs); n \<notin> range shrK |]
==> GuardK n A (knows_max C evs)"
by (simp add: knows_max_def)
-lemma Key_not_used_GuardK_spies [dest]: "Key n ~:used evs
-==> GuardK n A (spies evs)"
+lemma Key_not_used_GuardK_spies [dest]: "Key n \<notin> used evs
+\<Longrightarrow> GuardK n A (spies evs)"
by (auto simp: GuardK_def dest: not_used_not_known parts_sub)
-lemma Key_not_used_GuardK [dest]: "[| evs:p; Key n ~:used evs;
+lemma Key_not_used_GuardK [dest]: "[| evs \<in> p; Key n \<notin> used evs;
Gets_correct p; one_step p |] ==> GuardK n A (knows (Friend C) evs)"
by (auto simp: GuardK_def dest: known_used parts_trans)
-lemma Key_not_used_GuardK_max [dest]: "[| evs:p; Key n ~:used evs;
+lemma Key_not_used_GuardK_max [dest]: "[| evs \<in> p; Key n \<notin> used evs;
Gets_correct p; one_step p |] ==> GuardK n A (knows_max (Friend C) evs)"
by (auto simp: GuardK_def dest: known_max_used parts_trans)
-lemma Key_not_used_GuardK_max' [dest]: "[| evs:p; Key n ~:used evs;
+lemma Key_not_used_GuardK_max' [dest]: "[| evs \<in> p; Key n \<notin> used evs;
Gets_correct p; one_step p |] ==> GuardK n A (knows_max' (Friend C) evs)"
apply (rule_tac H="knows_max (Friend C) evs" in GuardK_mono)
by (auto simp: knows_max_def)
@@ -149,18 +149,18 @@
subsubsection\<open>regular protocols\<close>
definition regular :: "event list set => bool" where
-"regular p == ALL evs A. evs:p --> (Key (shrK A):parts (spies evs)) = (A:bad)"
+"regular p \<equiv> \<forall>evs A. evs \<in> p \<longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-lemma shrK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>
-(Key (shrK A):parts (spies evs)) = (A:bad)"
+lemma shrK_parts_iff_bad [simp]: "[| evs \<in> p; regular p |] ==>
+(Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
by (auto simp: regular_def)
-lemma shrK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==>
-(Key (shrK A):analz (spies evs)) = (A:bad)"
+lemma shrK_analz_iff_bad [simp]: "[| evs \<in> p; regular p |] ==>
+(Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
-lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p;
-shrK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)"
+lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs \<in> p;
+shrK_set Ks; good Ks; regular p |] ==> Nonce n \<notin> analz (spies evs)"
apply (clarify, simp only: knows_decomp)
apply (drule Guard_invKey_keyset, simp+, safe)
apply (drule in_good, simp)
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Feb 15 13:04:36 2018 +0100
@@ -50,20 +50,20 @@
inductive_set ya :: "event list set"
where
- Nil: "[]:ya"
+ Nil: "[] \<in> ya"
-| Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
+| Fake: "[| evs \<in> ya; X \<in> synth (analz (spies evs)) |] ==> Says Spy B X # evs \<in> ya"
-| YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
+| YA1: "[| evs1 \<in> ya; Nonce NA \<notin> used evs1 |] ==> ya1 A B NA # evs1 \<in> ya"
-| YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
- ==> ya2 A B NA NB # evs2:ya"
+| YA2: "[| evs2 \<in> ya; ya1' A' A B NA \<in> set evs2; Nonce NB \<notin> used evs2 |]
+ ==> ya2 A B NA NB # evs2 \<in> ya"
-| YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
- ==> ya3 A B NA NB K # evs3:ya"
+| YA3: "[| evs3 \<in> ya; ya2' B' A B NA NB \<in> set evs3; Key K \<notin> used evs3 |]
+ ==> ya3 A B NA NB K # evs3 \<in> ya"
-| YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
- ==> ya4 A B K NB Y # evs4:ya"
+| YA4: "[| evs4 \<in> ya; ya1 A B NA \<in> set evs4; ya3' S Y A B NA NB K \<in> set evs4 |]
+ ==> ya4 A B K NB Y # evs4 \<in> ya"
subsection\<open>declarations for tactics\<close>
@@ -73,17 +73,17 @@
subsection\<open>general properties of ya\<close>
-lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
+lemma ya_has_no_Gets: "evs \<in> ya \<Longrightarrow> \<forall>A X. Gets A X \<notin> set evs"
by (erule ya.induct, auto)
lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
lemma ya_is_one_step [iff]: "one_step ya"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:ya" for ev evs, auto)
+by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> ya" for ev evs, auto)
-lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
+lemma ya_has_only_Says' [rule_format]: "evs \<in> ya \<Longrightarrow>
+ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
by (erule ya.induct, auto)
lemma ya_has_only_Says [iff]: "has_only_Says ya"
@@ -96,8 +96,8 @@
subsection\<open>guardedness of KAB\<close>
-lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
-ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)"
+lemma Guard_KAB [rule_format]: "[| evs \<in> ya; A \<notin> bad; B \<notin> bad |] ==>
+ya3 A B NA NB K \<in> set evs \<longrightarrow> GuardK K {shrK A,shrK B} (spies evs)"
apply (erule ya.induct)
(* Nil *)
apply simp_all
@@ -117,55 +117,55 @@
subsection\<open>session keys are not symmetric keys\<close>
-lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
-ya3 A B NA NB K:set evs --> K ~:range shrK"
+lemma KAB_isnt_shrK [rule_format]: "evs \<in> ya \<Longrightarrow>
+ya3 A B NA NB K \<in> set evs \<longrightarrow> K \<notin> range shrK"
by (erule ya.induct, auto)
-lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
+lemma ya3_shrK: "evs \<in> ya \<Longrightarrow> ya3 A B NA NB (shrK C) \<notin> set evs"
by (blast dest: KAB_isnt_shrK)
subsection\<open>ya2' implies ya1'\<close>
lemma ya2'_parts_imp_ya1'_parts [rule_format]:
- "[| evs:ya; B ~:bad |] ==>
- Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs) -->
- \<lbrace>Agent A, Nonce NA\<rbrace>:spies evs"
+ "[| evs \<in> ya; B \<notin> bad |] ==>
+ Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ \<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs"
by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
-lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
-==> \<lbrace>Agent A, Nonce NA\<rbrace>:spies evs"
+lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB \<in> set evs; evs \<in> ya; B \<notin> bad |]
+==> \<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs"
by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
subsection\<open>uniqueness of NB\<close>
-lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
-Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs) -->
-Ciph B' \<lbrace>Agent A', Nonce NA', Nonce NB\<rbrace>:parts (spies evs) -->
-A=A' & B=B' & NA=NA'"
+lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs \<in> ya; B \<notin> bad; B' \<notin> bad |] ==>
+Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+Ciph B' \<lbrace>Agent A', Nonce NA', Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+A=A' \<and> B=B' \<and> NA=NA'"
apply (erule ya.induct, simp_all, clarify)
apply (drule Crypt_synth_insert, simp+)
apply (drule Crypt_synth_insert, simp+, safe)
apply (drule not_used_parts_false, simp+)+
by (drule Says_not_parts, simp+)+
-lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
-ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
-==> A=A' & B=B' & NA=NA'"
+lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB \<in> set evs;
+ya2' C' A' B' NA' NB \<in> set evs; evs \<in> ya; B \<notin> bad; B' \<notin> bad |]
+==> A=A' \<and> B=B' \<and> NA=NA'"
by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
subsection\<open>ya3' implies ya2'\<close>
-lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)
---> Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)"
+lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==>
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)"
apply (erule ya.induct, simp_all)
apply (clarify, drule Crypt_synth_insert, simp+)
apply (blast intro: parts_sub, blast)
by (auto dest: Says_imp_spies parts_parts)
-lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts (spies evs)
---> (EX B'. ya2' B' A B NA NB:set evs)"
+lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==>
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)
+\<longrightarrow> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)"
apply (erule ya.induct, simp_all, safe)
apply (drule Crypt_synth_insert, simp+)
apply (drule Crypt_synth_insert, simp+, blast)
@@ -173,30 +173,30 @@
apply blast
by (auto dest: Says_imp_spies2 parts_parts)
-lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
-==> (EX B'. ya2' B' A B NA NB:set evs)"
+lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad |]
+==> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)"
by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
subsection\<open>ya3' implies ya3\<close>
-lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>:parts(spies evs)
---> ya3 A B NA NB K:set evs"
+lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==>
+Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs)
+\<longrightarrow> ya3 A B NA NB K \<in> set evs"
apply (erule ya.induct, simp_all, safe)
apply (drule Crypt_synth_insert, simp+)
by (blast dest: Says_imp_spies2 parts_parts)
-lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
-==> ya3 A B NA NB K:set evs"
+lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad |]
+==> ya3 A B NA NB K \<in> set evs"
by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
subsection\<open>guardedness of NB\<close>
-definition ya_keys :: "agent => agent => nat => nat => event list => key set" where
-"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
+definition ya_keys :: "agent \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> event list \<Rightarrow> key set" where
+"ya_keys A B NA NB evs \<equiv> {shrK A,shrK B} \<union> {K. ya3 A B NA NB K \<in> set evs}"
-lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
-ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
+lemma Guard_NB [rule_format]: "[| evs \<in> ya; A \<notin> bad; B \<notin> bad |] ==>
+ya2 A B NA NB \<in> set evs \<longrightarrow> Guard NB (ya_keys A B NA NB evs) (spies evs)"
apply (erule ya.induct)
(* Nil *)
apply (simp_all add: ya_keys_def)
--- a/src/HOL/Auth/Guard/List_Msg.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy Thu Feb 15 13:04:36 2018 +0100
@@ -37,7 +37,7 @@
"len (cons x l) = Suc (len l)" |
"len other = 0"
-lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
+lemma len_not_empty: "n < len l \<Longrightarrow> \<exists>x l'. l = cons x l'"
by (cases l) auto
subsubsection\<open>membership\<close>
@@ -113,36 +113,36 @@
inductive_set agl :: "msg set"
where
- Nil[intro]: "nil:agl"
-| Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl"
+ Nil[intro]: "nil \<in> agl"
+| Cons[intro]: "[| A \<in> agent; I \<in> agl |] ==> cons (Agent A) I \<in> agl"
subsubsection\<open>basic facts about agent lists\<close>
-lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl"
+lemma del_in_agl [intro]: "I \<in> agl \<Longrightarrow> del (a,I) \<in> agl"
by (erule agl.induct, auto)
-lemma app_in_agl [intro]: "[| I:agl; J:agl |] ==> app (I,J):agl"
+lemma app_in_agl [intro]: "[| I \<in> agl; J \<in> agl |] ==> app (I,J) \<in> agl"
by (erule agl.induct, auto)
-lemma no_Key_in_agl: "I:agl ==> Key K ~:parts {I}"
+lemma no_Key_in_agl: "I \<in> agl \<Longrightarrow> Key K \<notin> parts {I}"
by (erule agl.induct, auto)
-lemma no_Nonce_in_agl: "I:agl ==> Nonce n ~:parts {I}"
+lemma no_Nonce_in_agl: "I \<in> agl \<Longrightarrow> Nonce n \<notin> parts {I}"
by (erule agl.induct, auto)
-lemma no_Key_in_appdel: "[| I:agl; J:agl |] ==>
-Key K ~:parts {app (J, del (Agent B, I))}"
+lemma no_Key_in_appdel: "[| I \<in> agl; J \<in> agl |] ==>
+Key K \<notin> parts {app (J, del (Agent B, I))}"
by (rule no_Key_in_agl, auto)
-lemma no_Nonce_in_appdel: "[| I:agl; J:agl |] ==>
-Nonce n ~:parts {app (J, del (Agent B, I))}"
+lemma no_Nonce_in_appdel: "[| I \<in> agl; J \<in> agl |] ==>
+Nonce n \<notin> parts {app (J, del (Agent B, I))}"
by (rule no_Nonce_in_agl, auto)
-lemma no_Crypt_in_agl: "I:agl ==> Crypt K X ~:parts {I}"
+lemma no_Crypt_in_agl: "I \<in> agl \<Longrightarrow> Crypt K X \<notin> parts {I}"
by (erule agl.induct, auto)
-lemma no_Crypt_in_appdel: "[| I:agl; J:agl |] ==>
-Crypt K X ~:parts {app (J, del (Agent B,I))}"
+lemma no_Crypt_in_appdel: "[| I \<in> agl; J \<in> agl |] ==>
+Crypt K X \<notin> parts {app (J, del (Agent B,I))}"
by (rule no_Crypt_in_agl, auto)
end
--- a/src/HOL/Auth/Guard/P1.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Thu Feb 15 13:04:36 2018 +0100
@@ -45,7 +45,7 @@
= (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')"
by (auto simp: chain_def Let_def)
-lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}"
+lemma Nonce_in_chain [iff]: "Nonce ofr \<in> parts {chain B ofr A L C}"
by (auto simp: chain_def sign_def)
subsubsection\<open>agent whose key is used to sign an offer\<close>
@@ -81,7 +81,7 @@
= (A=A' & n=n' & B=B')"
by (auto simp: anchor_def)
-lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}"
+lemma Nonce_in_anchor [iff]: "Nonce n \<in> parts {anchor A n B}"
by (auto simp: anchor_def)
lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A"
@@ -103,7 +103,7 @@
= (A=A' & r=r' & n=n' & I=I' & B=B')"
by (auto simp: reqm_def)
-lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}"
+lemma Nonce_in_reqm [iff]: "Nonce n \<in> parts {reqm A r n I B}"
by (auto simp: reqm_def)
definition req :: "agent => nat => nat => msg => agent => event" where
@@ -125,7 +125,7 @@
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
by (auto simp: prom_def)
-lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}"
+lemma Nonce_in_prom [iff]: "Nonce ofr \<in> parts {prom B ofr A r I L J C}"
by (auto simp: prom_def)
definition pro :: "agent => nat => agent => nat => msg => msg =>
@@ -141,21 +141,21 @@
inductive_set p1 :: "event list set"
where
- Nil: "[]:p1"
+ Nil: "[] \<in> p1"
-| Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1"
+| Fake: "[| evsf \<in> p1; X \<in> synth (analz (spies evsf)) |] ==> Says Spy B X # evsf \<in> p1"
-| Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1"
+| Request: "[| evsr \<in> p1; Nonce n \<notin> used evsr; I \<in> agl |] ==> req A r n I B # evsr \<in> p1"
-| Propose: "[| evsp:p1; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace>:set evsp;
- I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
- Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1"
+| Propose: "[| evsp \<in> p1; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace> \<in> set evsp;
+ I \<in> agl; J \<in> agl; isin (Agent C, app (J, del (Agent B, I)));
+ Nonce ofr \<notin> used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp \<in> p1"
subsubsection\<open>Composition of Traces\<close>
-lemma "evs':p1 ==>
- evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) -->
- evs'@evs : p1"
+lemma "evs' \<in> p1 \<Longrightarrow>
+ evs \<in> p1 \<and> (\<forall>n. Nonce n \<in> used evs' \<longrightarrow> Nonce n \<notin> used evs) \<longrightarrow>
+ evs' @ evs \<in> p1"
apply (erule p1.induct, safe)
apply (simp_all add: used_ConsI)
apply (erule p1.Fake, erule synth_sub, rule analz_mono, rule knows_sub_app)
@@ -168,30 +168,30 @@
subsubsection\<open>Valid Offer Lists\<close>
inductive_set
- valid :: "agent => nat => agent => msg set"
+ valid :: "agent \<Rightarrow> nat \<Rightarrow> agent \<Rightarrow> msg set"
for A :: agent and n :: nat and B :: agent
where
- Request [intro]: "cons (anchor A n B) nil:valid A n B"
+ Request [intro]: "cons (anchor A n B) nil \<in> valid A n B"
-| Propose [intro]: "L:valid A n B
-==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B"
+| Propose [intro]: "L \<in> valid A n B
+\<Longrightarrow> cons (chain (next_shop (head L)) ofr A L C) L \<in> valid A n B"
subsubsection\<open>basic properties of valid\<close>
-lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'"
+lemma valid_not_empty: "L \<in> valid A n B \<Longrightarrow> \<exists>M L'. L = cons M L'"
by (erule valid.cases, auto)
-lemma valid_pos_len: "L:valid A n B ==> 0 < len L"
+lemma valid_pos_len: "L \<in> valid A n B \<Longrightarrow> 0 < len L"
by (erule valid.induct, auto)
subsubsection\<open>offers of an offer list\<close>
-definition offer_nonces :: "msg => msg set" where
-"offer_nonces L == {X. X:parts {L} & (EX n. X = Nonce n)}"
+definition offer_nonces :: "msg \<Rightarrow> msg set" where
+"offer_nonces L \<equiv> {X. X \<in> parts {L} \<and> (\<exists>n. X = Nonce n)}"
subsubsection\<open>the originator can get the offers\<close>
-lemma "L:valid A n B ==> offer_nonces L <= analz (insert L (initState A))"
+lemma "L \<in> valid A n B \<Longrightarrow> offer_nonces L \<subseteq> analz (insert L (initState A))"
by (erule valid.induct, auto simp: anchor_def chain_def sign_def
offer_nonces_def initState.simps)
@@ -207,22 +207,22 @@
"shops (cons M L) = cons (shop M) (shops L)" |
"shops other = other"
-lemma shops_in_agl: "L:valid A n B ==> shops L:agl"
+lemma shops_in_agl: "L \<in> valid A n B \<Longrightarrow> shops L \<in> agl"
by (erule valid.induct, auto simp: anchor_def chain_def sign_def)
subsubsection\<open>builds a trace from an itinerary\<close>
-fun offer_list :: "agent * nat * agent * msg * nat => msg" where
+fun offer_list :: "agent \<times> nat \<times> agent \<times> msg \<times> nat \<Rightarrow> msg" where
"offer_list (A,n,B,nil,ofr) = cons (anchor A n B) nil" |
"offer_list (A,n,B,cons (Agent C) I,ofr) = (
let L = offer_list (A,n,B,I,Suc ofr) in
cons (chain (next_shop (head L)) ofr A L C) L)"
-lemma "I:agl ==> ALL ofr. offer_list (A,n,B,I,ofr):valid A n B"
+lemma "I \<in> agl \<Longrightarrow> \<forall>ofr. offer_list (A,n,B,I,ofr) \<in> valid A n B"
by (erule agl.induct, auto)
-fun trace :: "agent * nat * agent * nat * msg * msg * msg
-=> event list" where
+fun trace :: "agent \<times> nat \<times> agent \<times> nat \<times> msg \<times> msg \<times> msg
+\<Rightarrow> event list" where
"trace (B,ofr,A,r,I,L,nil) = []" |
"trace (B,ofr,A,r,I,L,cons (Agent D) K) = (
let C = (if K=nil then B else agt_nb (head K)) in
@@ -232,8 +232,8 @@
pro C (Suc ofr) A r I' L nil D
# trace (B,Suc ofr,A,r,I'',tail L,K))"
-definition trace' :: "agent => nat => nat => msg => agent => nat => event list" where
-"trace' A r n I B ofr == (
+definition trace' :: "agent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> msg \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> event list" where
+"trace' A r n I B ofr \<equiv> (
let AI = cons (Agent A) I in
let L = offer_list (A,n,B,AI,ofr) in
trace (B,ofr,A,r,nil,L,AI))"
@@ -242,8 +242,8 @@
subsubsection\<open>there is a trace in which the originator receives a valid answer\<close>
-lemma p1_not_empty: "evs:p1 ==> req A r n I B:set evs -->
-(EX evs'. evs'@evs:p1 & pro B' ofr A r I' L J A:set evs' & L:valid A n B)"
+lemma p1_not_empty: "evs \<in> p1 \<Longrightarrow> req A r n I B \<in> set evs \<longrightarrow>
+(\<exists>evs'. evs' @ evs \<in> p1 \<and> pro B' ofr A r I' L J A \<in> set evs' \<and> L \<in> valid A n B)"
oops
@@ -255,66 +255,66 @@
subsubsection\<open>strong forward integrity:
except the last one, no offer can be modified\<close>
-lemma strong_forward_integrity: "ALL L. Suc i < len L
---> L:valid A n B & repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)"
+lemma strong_forward_integrity: "\<forall>L. Suc i < len L
+\<longrightarrow> L \<in> valid A n B \<and> repl (L,Suc i,M) \<in> valid A n B \<longrightarrow> M = ith (L,Suc i)"
apply (induct i)
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace>:valid A n B" for x xa l'a)
-apply (ind_cases "\<lbrace>x,M,l'a\<rbrace>:valid A n B" for x l'a)
+apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace> \<in> valid A n B" for x xa l'a)
+apply (ind_cases "\<lbrace>x,M,l'a\<rbrace> \<in> valid A n B" for x l'a)
apply (simp add: chain_def)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,repl(l',Suc na,M)\<rbrace> \<in> valid A n B" for x l' na)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l')
by (drule_tac x=l' in spec, simp, blast)
subsubsection\<open>insertion resilience:
except at the beginning, no offer can be inserted\<close>
-lemma chain_isnt_head [simp]: "L:valid A n B ==>
-head L ~= chain (next_shop (head L)) ofr A L C"
+lemma chain_isnt_head [simp]: "L \<in> valid A n B \<Longrightarrow>
+head L \<noteq> chain (next_shop (head L)) ofr A L C"
by (erule valid.induct, auto simp: chain_def sign_def anchor_def)
-lemma insertion_resilience: "ALL L. L:valid A n B --> Suc i < len L
---> ins (L,Suc i,M) ~:valid A n B"
+lemma insertion_resilience: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L
+\<longrightarrow> ins (L,Suc i,M) \<notin> valid A n B"
apply (induct i)
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l', simp)
-apply (ind_cases "\<lbrace>x,M,l'\<rbrace>:valid A n B" for x l', clarsimp)
-apply (ind_cases "\<lbrace>head l',l'\<rbrace>:valid A n B" for l', simp, simp)
+apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l', simp)
+apply (ind_cases "\<lbrace>x,M,l'\<rbrace> \<in> valid A n B" for x l', clarsimp)
+apply (ind_cases "\<lbrace>head l',l'\<rbrace> \<in> valid A n B" for l', simp, simp)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace>:valid A n B" for x l' na)
+apply (ind_cases "\<lbrace>x,ins(l',Suc na,M)\<rbrace> \<in> valid A n B" for x l' na)
apply (frule len_not_empty, clarsimp)
by (drule_tac x=l' in spec, clarsimp)
subsubsection\<open>truncation resilience:
only shop i can truncate at offer i\<close>
-lemma truncation_resilience: "ALL L. L:valid A n B --> Suc i < len L
---> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))"
+lemma truncation_resilience: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L
+\<longrightarrow> cons M (trunc (L,Suc i)) \<in> valid A n B \<longrightarrow> shop M = shop (ith (L,i))"
apply (induct i)
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>M,l'\<rbrace>:valid A n B" for l')
+apply (ind_cases "\<lbrace>M,l'\<rbrace> \<in> valid A n B" for l')
apply (frule len_not_empty, clarsimp, simp)
(* i > 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,l'\<rbrace>:valid A n B" for x l')
+apply (ind_cases "\<lbrace>x,l'\<rbrace> \<in> valid A n B" for x l')
apply (frule len_not_empty, clarsimp)
by (drule_tac x=l' in spec, clarsimp)
@@ -326,37 +326,37 @@
subsubsection\<open>get components of a message\<close>
-lemma get_ML [dest]: "Says A' B \<lbrace>A,r,I,M,L\<rbrace>:set evs ==>
-M:parts (spies evs) & L:parts (spies evs)"
+lemma get_ML [dest]: "Says A' B \<lbrace>A,r,I,M,L\<rbrace> \<in> set evs \<Longrightarrow>
+M \<in> parts (spies evs) \<and> L \<in> parts (spies evs)"
by blast
subsubsection\<open>general properties of p1\<close>
lemma reqm_neq_prom [iff]:
-"reqm A r n I B ~= prom B' ofr A' r' I' (cons M L) J C"
+"reqm A r n I B \<noteq> prom B' ofr A' r' I' (cons M L) J C"
by (auto simp: reqm_def prom_def)
lemma prom_neq_reqm [iff]:
-"prom B' ofr A' r' I' (cons M L) J C ~= reqm A r n I B"
+"prom B' ofr A' r' I' (cons M L) J C \<noteq> reqm A r n I B"
by (auto simp: reqm_def prom_def)
-lemma req_neq_pro [iff]: "req A r n I B ~= pro B' ofr A' r' I' (cons M L) J C"
+lemma req_neq_pro [iff]: "req A r n I B \<noteq> pro B' ofr A' r' I' (cons M L) J C"
by (auto simp: req_def pro_def)
-lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C ~= req A r n I B"
+lemma pro_neq_req [iff]: "pro B' ofr A' r' I' (cons M L) J C \<noteq> req A r n I B"
by (auto simp: req_def pro_def)
-lemma p1_has_no_Gets: "evs:p1 ==> ALL A X. Gets A X ~:set evs"
+lemma p1_has_no_Gets: "evs \<in> p1 \<Longrightarrow> \<forall>A X. Gets A X \<notin> set evs"
by (erule p1.induct, auto simp: req_def pro_def)
lemma p1_is_Gets_correct [iff]: "Gets_correct p1"
by (auto simp: Gets_correct_def dest: p1_has_no_Gets)
lemma p1_is_one_step [iff]: "one_step p1"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:p1" for ev evs, auto)
+by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> p1" for ev evs, auto)
-lemma p1_has_only_Says' [rule_format]: "evs:p1 ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
+lemma p1_has_only_Says' [rule_format]: "evs \<in> p1 \<Longrightarrow>
+ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
by (erule p1.induct, auto simp: req_def pro_def)
lemma p1_has_only_Says [iff]: "has_only_Says p1"
@@ -372,8 +372,8 @@
subsubsection\<open>private keys are safe\<close>
lemma priK_parts_Friend_imp_bad [rule_format,dest]:
- "[| evs:p1; Friend B ~= A |]
- ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
+ "[| evs \<in> p1; Friend B \<noteq> A |]
+ ==> (Key (priK A) \<in> parts (knows (Friend B) evs)) \<longrightarrow> (A \<in> bad)"
apply (erule p1.induct)
apply (simp_all add: initState.simps knows.simps pro_def prom_def
req_def reqm_def anchor_def chain_def sign_def)
@@ -383,12 +383,12 @@
done
lemma priK_analz_Friend_imp_bad [rule_format,dest]:
- "[| evs:p1; Friend B ~= A |]
-==> (Key (priK A):analz (knows (Friend B) evs)) --> (A:bad)"
+ "[| evs \<in> p1; Friend B \<noteq> A |]
+==> (Key (priK A) \<in> analz (knows (Friend B) evs)) \<longrightarrow> (A \<in> bad)"
by auto
-lemma priK_notin_knows_max_Friend: "[| evs:p1; A ~:bad; A ~= Friend C |]
-==> Key (priK A) ~:analz (knows_max (Friend C) evs)"
+lemma priK_notin_knows_max_Friend: "[| evs \<in> p1; A \<notin> bad; A \<noteq> Friend C |]
+==> Key (priK A) \<notin> analz (knows_max (Friend C) evs)"
apply (rule not_parts_not_analz, simp add: knows_max_def, safe)
apply (drule_tac H="spies' evs" in parts_sub)
apply (rule_tac p=p1 in knows_max'_sub_spies', simp+)
@@ -397,78 +397,78 @@
subsubsection\<open>general guardedness properties\<close>
-lemma agl_guard [intro]: "I:agl ==> I:guard n Ks"
+lemma agl_guard [intro]: "I \<in> agl \<Longrightarrow> I \<in> guard n Ks"
by (erule agl.induct, auto)
-lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace>:set evs;
-Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
+lemma Says_to_knows_max'_guard: "[| Says A' C \<lbrace>A'',r,I,L\<rbrace> \<in> set evs;
+Guard n Ks (knows_max' C evs) |] ==> L \<in> guard n Ks"
by (auto dest: Says_to_knows_max')
-lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace>:set evs;
-Guard n Ks (knows_max' C evs) |] ==> L:guard n Ks"
+lemma Says_from_knows_max'_guard: "[| Says C A' \<lbrace>A'',r,I,L\<rbrace> \<in> set evs;
+Guard n Ks (knows_max' C evs) |] ==> L \<in> guard n Ks"
by (auto dest: Says_from_knows_max')
-lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace>:set evs;
-Nonce n ~:used evs |] ==> L:guard n Ks"
+lemma Says_Nonce_not_used_guard: "[| Says A' B \<lbrace>A'',r,I,L\<rbrace> \<in> set evs;
+Nonce n \<notin> used evs |] ==> L \<in> guard n Ks"
by (drule not_used_not_parts, auto)
subsubsection\<open>guardedness of messages\<close>
-lemma chain_guard [iff]: "chain B ofr A L C:guard n {priK A}"
+lemma chain_guard [iff]: "chain B ofr A L C \<in> guard n {priK A}"
by (case_tac "ofr=n", auto simp: chain_def sign_def)
-lemma chain_guard_Nonce_neq [intro]: "n ~= ofr
-==> chain B ofr A' L C:guard n {priK A}"
+lemma chain_guard_Nonce_neq [intro]: "n \<noteq> ofr
+\<Longrightarrow> chain B ofr A' L C \<in> guard n {priK A}"
by (auto simp: chain_def sign_def)
-lemma anchor_guard [iff]: "anchor A n' B:guard n {priK A}"
+lemma anchor_guard [iff]: "anchor A n' B \<in> guard n {priK A}"
by (case_tac "n'=n", auto simp: anchor_def)
-lemma anchor_guard_Nonce_neq [intro]: "n ~= n'
-==> anchor A' n' B:guard n {priK A}"
+lemma anchor_guard_Nonce_neq [intro]: "n \<noteq> n'
+\<Longrightarrow> anchor A' n' B \<in> guard n {priK A}"
by (auto simp: anchor_def)
-lemma reqm_guard [intro]: "I:agl ==> reqm A r n' I B:guard n {priK A}"
+lemma reqm_guard [intro]: "I \<in> agl \<Longrightarrow> reqm A r n' I B \<in> guard n {priK A}"
by (case_tac "n'=n", auto simp: reqm_def)
-lemma reqm_guard_Nonce_neq [intro]: "[| n ~= n'; I:agl |]
-==> reqm A' r n' I B:guard n {priK A}"
+lemma reqm_guard_Nonce_neq [intro]: "[| n \<noteq> n'; I \<in> agl |]
+==> reqm A' r n' I B \<in> guard n {priK A}"
by (auto simp: reqm_def)
-lemma prom_guard [intro]: "[| I:agl; J:agl; L:guard n {priK A} |]
-==> prom B ofr A r I L J C:guard n {priK A}"
+lemma prom_guard [intro]: "[| I \<in> agl; J \<in> agl; L \<in> guard n {priK A} |]
+==> prom B ofr A r I L J C \<in> guard n {priK A}"
by (auto simp: prom_def)
-lemma prom_guard_Nonce_neq [intro]: "[| n ~= ofr; I:agl; J:agl;
-L:guard n {priK A} |] ==> prom B ofr A' r I L J C:guard n {priK A}"
+lemma prom_guard_Nonce_neq [intro]: "[| n \<noteq> ofr; I \<in> agl; J \<in> agl;
+L \<in> guard n {priK A} |] ==> prom B ofr A' r I L J C \<in> guard n {priK A}"
by (auto simp: prom_def)
subsubsection\<open>Nonce uniqueness\<close>
-lemma uniq_Nonce_in_chain [dest]: "Nonce k:parts {chain B ofr A L C} ==> k=ofr"
+lemma uniq_Nonce_in_chain [dest]: "Nonce k \<in> parts {chain B ofr A L C} \<Longrightarrow> k=ofr"
by (auto simp: chain_def sign_def)
-lemma uniq_Nonce_in_anchor [dest]: "Nonce k:parts {anchor A n B} ==> k=n"
+lemma uniq_Nonce_in_anchor [dest]: "Nonce k \<in> parts {anchor A n B} \<Longrightarrow> k=n"
by (auto simp: anchor_def chain_def sign_def)
-lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k:parts {reqm A r n I B};
-I:agl |] ==> k=n"
+lemma uniq_Nonce_in_reqm [dest]: "[| Nonce k \<in> parts {reqm A r n I B};
+I \<in> agl |] ==> k=n"
by (auto simp: reqm_def dest: no_Nonce_in_agl)
-lemma uniq_Nonce_in_prom [dest]: "[| Nonce k:parts {prom B ofr A r I L J C};
-I:agl; J:agl; Nonce k ~:parts {L} |] ==> k=ofr"
+lemma uniq_Nonce_in_prom [dest]: "[| Nonce k \<in> parts {prom B ofr A r I L J C};
+I \<in> agl; J \<in> agl; Nonce k \<notin> parts {L} |] ==> k=ofr"
by (auto simp: prom_def dest: no_Nonce_in_agl no_Nonce_in_appdel)
subsubsection\<open>requests are guarded\<close>
-lemma req_imp_Guard [rule_format]: "[| evs:p1; A ~:bad |] ==>
-req A r n I B:set evs --> Guard n {priK A} (spies evs)"
+lemma req_imp_Guard [rule_format]: "[| evs \<in> p1; A \<notin> bad |] ==>
+req A r n I B \<in> set evs \<longrightarrow> Guard n {priK A} (spies evs)"
apply (erule p1.induct, simp)
apply (simp add: req_def knows.simps, safe)
apply (erule in_synth_Guard, erule Guard_analz, simp)
by (auto simp: req_def pro_def dest: Says_imp_knows_Spy)
-lemma req_imp_Guard_Friend: "[| evs:p1; A ~:bad; req A r n I B:set evs |]
+lemma req_imp_Guard_Friend: "[| evs \<in> p1; A \<notin> bad; req A r n I B \<in> set evs |]
==> Guard n {priK A} (knows_max (Friend C) evs)"
apply (rule Guard_knows_max')
apply (rule_tac H="spies evs" in Guard_mono)
@@ -479,8 +479,8 @@
subsubsection\<open>propositions are guarded\<close>
-lemma pro_imp_Guard [rule_format]: "[| evs:p1; B ~:bad; A ~:bad |] ==>
-pro B ofr A r I (cons M L) J C:set evs --> Guard ofr {priK A} (spies evs)"
+lemma pro_imp_Guard [rule_format]: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad |] ==>
+pro B ofr A r I (cons M L) J C \<in> set evs \<longrightarrow> Guard ofr {priK A} (spies evs)"
apply (erule p1.induct) (* +3 subgoals *)
(* Nil *)
apply simp
@@ -516,8 +516,8 @@
apply (simp add: pro_def)
by (blast dest: Says_imp_knows_Spy)
-lemma pro_imp_Guard_Friend: "[| evs:p1; B ~:bad; A ~:bad;
-pro B ofr A r I (cons M L) J C:set evs |]
+lemma pro_imp_Guard_Friend: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad;
+pro B ofr A r I (cons M L) J C \<in> set evs |]
==> Guard ofr {priK A} (knows_max (Friend D) evs)"
apply (rule Guard_knows_max')
apply (rule_tac H="spies evs" in Guard_mono)
@@ -529,23 +529,23 @@
subsubsection\<open>data confidentiality:
no one other than the originator can decrypt the offers\<close>
-lemma Nonce_req_notin_spies: "[| evs:p1; req A r n I B:set evs; A ~:bad |]
-==> Nonce n ~:analz (spies evs)"
+lemma Nonce_req_notin_spies: "[| evs \<in> p1; req A r n I B \<in> set evs; A \<notin> bad |]
+==> Nonce n \<notin> analz (spies evs)"
by (frule req_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
-lemma Nonce_req_notin_knows_max_Friend: "[| evs:p1; req A r n I B:set evs;
-A ~:bad; A ~= Friend C |] ==> Nonce n ~:analz (knows_max (Friend C) evs)"
+lemma Nonce_req_notin_knows_max_Friend: "[| evs \<in> p1; req A r n I B \<in> set evs;
+A \<notin> bad; A \<noteq> Friend C |] ==> Nonce n \<notin> analz (knows_max (Friend C) evs)"
apply (clarify, frule_tac C=C in req_imp_Guard_Friend, simp+)
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
-lemma Nonce_pro_notin_spies: "[| evs:p1; B ~:bad; A ~:bad;
-pro B ofr A r I (cons M L) J C:set evs |] ==> Nonce ofr ~:analz (spies evs)"
+lemma Nonce_pro_notin_spies: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad;
+pro B ofr A r I (cons M L) J C \<in> set evs |] ==> Nonce ofr \<notin> analz (spies evs)"
by (frule pro_imp_Guard, simp+, erule Guard_Nonce_analz, simp+)
-lemma Nonce_pro_notin_knows_max_Friend: "[| evs:p1; B ~:bad; A ~:bad;
-A ~= Friend D; pro B ofr A r I (cons M L) J C:set evs |]
-==> Nonce ofr ~:analz (knows_max (Friend D) evs)"
+lemma Nonce_pro_notin_knows_max_Friend: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad;
+A \<noteq> Friend D; pro B ofr A r I (cons M L) J C \<in> set evs |]
+==> Nonce ofr \<notin> analz (knows_max (Friend D) evs)"
apply (clarify, frule_tac A=A in pro_imp_Guard_Friend, simp+)
apply (simp add: knows_max_def, drule Guard_invKey_keyset, simp+)
by (drule priK_notin_knows_max_Friend, auto simp: knows_max_def)
@@ -553,59 +553,59 @@
subsubsection\<open>non repudiability:
an offer signed by B has been sent by B\<close>
-lemma Crypt_reqm: "[| Crypt (priK A) X:parts {reqm A' r n I B}; I:agl |] ==> A=A'"
+lemma Crypt_reqm: "[| Crypt (priK A) X \<in> parts {reqm A' r n I B}; I \<in> agl |] ==> A=A'"
by (auto simp: reqm_def anchor_def chain_def sign_def dest: no_Crypt_in_agl)
-lemma Crypt_prom: "[| Crypt (priK A) X:parts {prom B ofr A' r I L J C};
-I:agl; J:agl |] ==> A=B | Crypt (priK A) X:parts {L}"
+lemma Crypt_prom: "[| Crypt (priK A) X \<in> parts {prom B ofr A' r I L J C};
+I \<in> agl; J \<in> agl |] ==> A=B \<or> Crypt (priK A) X \<in> parts {L}"
apply (simp add: prom_def anchor_def chain_def sign_def)
by (blast dest: no_Crypt_in_agl no_Crypt_in_appdel)
-lemma Crypt_safeness: "[| evs:p1; A ~:bad |] ==> Crypt (priK A) X:parts (spies evs)
---> (EX B Y. Says A B Y:set evs & Crypt (priK A) X:parts {Y})"
+lemma Crypt_safeness: "[| evs \<in> p1; A \<notin> bad |] ==> Crypt (priK A) X \<in> parts (spies evs)
+\<longrightarrow> (\<exists>B Y. Says A B Y \<in> set evs \<and> Crypt (priK A) X \<in> parts {Y})"
apply (erule p1.induct)
(* Nil *)
apply simp
(* Fake *)
apply clarsimp
-apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
+apply (drule_tac P="\<lambda>G. Crypt (priK A) X \<in> G" in parts_insert_substD, simp)
apply (erule disjE)
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
(* Request *)
apply (simp add: req_def, clarify)
-apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
+apply (drule_tac P="\<lambda>G. Crypt (priK A) X \<in> G" in parts_insert_substD, simp)
apply (erule disjE)
apply (frule Crypt_reqm, simp, clarify)
apply (rule_tac x=B in exI, rule_tac x="reqm A r n I B" in exI, simp, blast)
(* Propose *)
apply (simp add: pro_def, clarify)
-apply (drule_tac P="%G. Crypt (priK A) X:G" in parts_insert_substD, simp)
+apply (drule_tac P="\<lambda>G. Crypt (priK A) X \<in> G" in parts_insert_substD, simp)
apply (rotate_tac -1, erule disjE)
apply (frule Crypt_prom, simp, simp)
apply (rotate_tac -1, erule disjE)
apply (rule_tac x=C in exI)
apply (rule_tac x="prom B ofr Aa r I (cons M L) J C" in exI, blast)
-apply (subgoal_tac "cons M L:parts (spies evsp)")
+apply (subgoal_tac "cons M L \<in> parts (spies evsp)")
apply (drule_tac G="{cons M L}" and H="spies evsp" in parts_trans, blast, blast)
apply (drule Says_imp_spies, rotate_tac -1, drule parts.Inj)
apply (drule parts.Snd, drule parts.Snd, drule parts.Snd)
by auto
-lemma Crypt_Hash_imp_sign: "[| evs:p1; A ~:bad |] ==>
-Crypt (priK A) (Hash X):parts (spies evs)
---> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
+lemma Crypt_Hash_imp_sign: "[| evs \<in> p1; A \<notin> bad |] ==>
+Crypt (priK A) (Hash X) \<in> parts (spies evs)
+\<longrightarrow> (\<exists>B Y. Says A B Y \<in> set evs \<and> sign A X \<in> parts {Y})"
apply (erule p1.induct)
(* Nil *)
apply simp
(* Fake *)
apply clarsimp
-apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
+apply (drule_tac P="\<lambda>G. Crypt (priK A) (Hash X) \<in> G" in parts_insert_substD)
apply simp
apply (erule disjE)
apply (drule_tac K="priK A" in Crypt_synth, simp+, blast, blast)
(* Request *)
apply (simp add: req_def, clarify)
-apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
+apply (drule_tac P="\<lambda>G. Crypt (priK A) (Hash X) \<in> G" in parts_insert_substD)
apply simp
apply (erule disjE)
apply (frule Crypt_reqm, simp+)
@@ -614,7 +614,7 @@
apply (simp add: chain_def sign_def, blast)
(* Propose *)
apply (simp add: pro_def, clarify)
-apply (drule_tac P="%G. Crypt (priK A) (Hash X):G" in parts_insert_substD)
+apply (drule_tac P="\<lambda>G. Crypt (priK A) (Hash X) \<in> G" in parts_insert_substD)
apply simp
apply (rotate_tac -1, erule disjE)
apply (simp add: prom_def sign_def no_Crypt_in_agl no_Crypt_in_appdel)
@@ -628,8 +628,8 @@
apply (blast del: MPair_parts)+
done
-lemma sign_safeness: "[| evs:p1; A ~:bad |] ==> sign A X:parts (spies evs)
---> (EX B Y. Says A B Y:set evs & sign A X:parts {Y})"
+lemma sign_safeness: "[| evs \<in> p1; A \<notin> bad |] ==> sign A X \<in> parts (spies evs)
+\<longrightarrow> (\<exists>B Y. Says A B Y \<in> set evs \<and> sign A X \<in> parts {Y})"
apply (clarify, simp add: sign_def, frule parts.Snd)
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def])
done
--- a/src/HOL/Auth/Guard/P2.thy Wed Feb 14 16:32:09 2018 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Thu Feb 15 13:04:36 2018 +0100
@@ -32,7 +32,7 @@
= (B=B' & ofr=ofr' & A=A' & head L = head L' & C=C')"
by (auto simp: chain_def Let_def)
-lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}"
+lemma Nonce_in_chain [iff]: "Nonce ofr \<in> parts {chain B ofr A L C}"
by (auto simp: chain_def sign_def)
subsubsection\<open>agent whose key is used to sign an offer\<close>
@@ -65,10 +65,10 @@
"anchor A n B == chain A n A (cons nil nil) B"
lemma anchor_inj [iff]:
- "(anchor A n B = anchor A' n' B') = (A=A' & n=n' & B=B')"
+ "(anchor A n B = anchor A' n' B') = (A=A' \<and> n=n' \<and> B=B')"
by (auto simp: anchor_def)
-lemma Nonce_in_anchor [iff]: "Nonce n:parts {anchor A n B}"
+lemma Nonce_in_anchor [iff]: "Nonce n \<in> parts {anchor A n B}"
by (auto simp: anchor_def)
lemma shop_anchor [simp]: "shop (anchor A n B) = Agent A"
@@ -84,7 +84,7 @@
= (A=A' & r=r' & n=n' & I=I' & B=B')"
by (auto simp: reqm_def)
-lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}"
+lemma Nonce_in_reqm [iff]: "Nonce n \<in> parts {reqm A r n I B}"
by (auto simp: reqm_def)
definition req :: "agent => nat => nat => msg => agent => event" where
@@ -105,7 +105,7 @@
==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'"
by (auto simp: prom_def)
-lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}"
+lemma Nonce_in_prom [iff]: "Nonce ofr \<in> parts {prom B ofr A r I L J C}"
by (auto simp: prom_def)
definition pro :: "agent => nat => agent => nat => msg => msg =>
@@ -121,38 +121,38 @@
inductive_set p2 :: "event list set"
where
- Nil: "[]:p2"
+ Nil: "[] \<in> p2"
-| Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2"
+| Fake: "[| evsf \<in> p2; X \<in> synth (analz (spies evsf)) |] ==> Says Spy B X # evsf \<in> p2"
-| Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2"
+| Request: "[| evsr \<in> p2; Nonce n \<notin> used evsr; I \<in> agl |] ==> req A r n I B # evsr \<in> p2"
-| Propose: "[| evsp:p2; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace>:set evsp;
- I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I)));
- Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2"
+| Propose: "[| evsp \<in> p2; Says A' B \<lbrace>Agent A,Number r,I,cons M L\<rbrace> \<in> set evsp;
+ I \<in> agl; J \<in> agl; isin (Agent C, app (J, del (Agent B, I)));
+ Nonce ofr \<notin> used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp \<in> p2"
subsubsection\<open>valid offer lists\<close>
inductive_set
- valid :: "agent => nat => agent => msg set"
+ valid :: "agent \<Rightarrow> nat \<Rightarrow> agent \<Rightarrow> msg set"
for A :: agent and n :: nat and B :: agent
where
- Request [intro]: "cons (anchor A n B) nil:valid A n B"
+ Request [intro]: "cons (anchor A n B) nil \<in> valid A n B"
-| Propose [intro]: "L:valid A n B
- ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B"
+| Propose [intro]: "L \<in> valid A n B
+ \<Longrightarrow> cons (chain (next_shop (head L)) ofr A L C) L \<in> valid A n B"
subsubsection\<open>basic properties of valid\<close>
-lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'"
+lemma valid_not_empty: "L \<in> valid A n B \<Longrightarrow> \<exists>M L'. L = cons M L'"
by (erule valid.cases, auto)
-lemma valid_pos_len: "L:valid A n B ==> 0 < len L"
+lemma valid_pos_len: "L \<in> valid A n B \<Longrightarrow> 0 < len L"
by (erule valid.induct, auto)
subsubsection\<open>list of offers\<close>
-fun offers :: "msg => msg"
+fun offers :: "msg \<Rightarrow> msg"
where
"offers (cons M L) = cons \<lbrace>shop M, nonce M\<rbrace> (offers L)"
| "offers other = nil"
@@ -166,66 +166,66 @@
subsection\<open>strong forward integrity:
except the last one, no offer can be modified\<close>
-lemma strong_forward_integrity: "ALL L. Suc i < len L
---> L:valid A n B --> repl (L,Suc i,M):valid A n B --> M = ith (L,Suc i)"
+lemma strong_forward_integrity: "\<forall>L. Suc i < len L
+\<longrightarrow> L \<in> valid A n B \<longrightarrow> repl (L,Suc i,M) \<in> valid A n B \<longrightarrow> M = ith (L,Suc i)"
apply (induct i)
(* i = 0 *)
apply clarify
apply (frule len_not_empty, clarsimp)
apply (frule len_not_empty, clarsimp)
-apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace>:valid A n B" for x xa l'a)
-apply (ind_cases "\<lbrace>x,M,l'a\<rbrace>:valid A n B" for x l'a)
+apply (ind_cases "\<lbrace>x,xa,l'a\<rbrace> \<in> valid A n B" for x xa l'a)
+apply (ind_cases "\<lbrace>x,M,l'a\<rbrace> \<in> valid A n B" for x l'a)
apply (simp add: chain_def)
(* i > 0 *)