--- a/src/HOL/SET_Protocol/Message_SET.thy Wed Dec 30 18:07:10 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Wed Dec 30 18:17:28 2015 +0100
@@ -67,16 +67,12 @@
| Crypt key msg --{*Encryption, public- or shared-key*}
-(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
+(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
-
-syntax (xsymbols)
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
-
translations
- "{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "CONST MPair x y"
+ "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
definition nat_of_agent :: "agent => nat" where
@@ -104,8 +100,8 @@
for H :: "msg set"
where
Inj [intro]: "X \<in> H ==> X \<in> parts H"
- | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
- | Snd: "{|X,Y|} \<in> parts H ==> Y \<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"
@@ -180,7 +176,7 @@
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
by (unfold keysFor_def, auto)
-lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H"
+lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
by (unfold keysFor_def, auto)
lemma keysFor_insert_Crypt [simp]:
@@ -197,7 +193,7 @@
subsection{*Inductive relation "parts"*}
lemma MPair_parts:
- "[| {|X,Y|} \<in> parts H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> parts H;
[| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
by (blast dest: parts.Fst parts.Snd)
@@ -346,8 +342,8 @@
done
lemma parts_insert_MPair [simp]:
- "parts (insert {|X,Y|} H) =
- insert {|X,Y|} (parts (insert X (insert Y H)))"
+ "parts (insert \<lbrace>X,Y\<rbrace> H) =
+ insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule parts.induct, auto)
@@ -398,8 +394,8 @@
for H :: "msg set"
where
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
- | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
- | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ | 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"
@@ -413,7 +409,7 @@
text{*Making it safe speeds up proofs*}
lemma MPair_analz [elim!]:
- "[| {|X,Y|} \<in> analz H;
+ "[| \<lbrace>X,Y\<rbrace> \<in> analz H;
[| X \<in> analz H; Y \<in> analz H |] ==> P
|] ==> P"
by (blast dest: analz.Fst analz.Snd)
@@ -497,8 +493,8 @@
done
lemma analz_insert_MPair [simp]:
- "analz (insert {|X,Y|} H) =
- insert {|X,Y|} (analz (insert X (insert Y H)))"
+ "analz (insert \<lbrace>X,Y\<rbrace> H) =
+ insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))"
apply (rule equalityI)
apply (rule subsetI)
apply (erule analz.induct, auto)
@@ -619,7 +615,7 @@
(*If there are no pairs or encryptions then analz does nothing*)
lemma analz_trivial:
- "[| \<forall>X Y. {|X,Y|} \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
+ "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H"
apply safe
apply (erule analz.induct, blast+)
done
@@ -650,7 +646,7 @@
| Agent [intro]: "Agent agt \<in> synth H"
| Number [intro]: "Number n \<in> synth H"
| Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
- | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
| Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
(*Monotonicity*)
@@ -664,7 +660,7 @@
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"
-inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
+inductive_cases MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
inductive_cases Pan_synth [elim!]: "Pan A \<in> synth H"
@@ -790,7 +786,7 @@
(*Without this equation, other rules for synth and analz would yield
redundant cases*)
lemma MPair_synth_analz [iff]:
- "({|X,Y|} \<in> synth (analz H)) =
+ "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) =
(X \<in> synth (analz H) & Y \<in> synth (analz H))"
by blast
@@ -802,7 +798,7 @@
lemma Hash_synth_analz [simp]:
"X \<notin> synth (analz H)
- ==> (Hash{|X,Y|} \<in> synth (analz H)) = (Hash{|X,Y|} \<in> analz H)"
+ ==> (Hash\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = (Hash\<lbrace>X,Y\<rbrace> \<in> analz H)"
by blast