--- a/src/HOL/Auth/Message.thy Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Auth/Message.thy Wed Jul 11 11:14:51 2007 +0200
@@ -72,13 +72,14 @@
subsubsection{*Inductive Definition of All Parts" of a Message*}
-consts parts :: "msg set => msg set"
-inductive "parts H"
- intros
+inductive_set
+ parts :: "msg set => msg set"
+ 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"
- Body: "Crypt K X \<in> parts 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"
+ | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
text{*Monotonicity*}
@@ -335,13 +336,14 @@
messages, including keys. A form of downward closure. Pairs can
be taken apart; messages decrypted with known keys. *}
-consts analz :: "msg set => msg set"
-inductive "analz H"
- intros
+inductive_set
+ analz :: "msg set => msg set"
+ 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"
- Decrypt [dest]:
+ | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+ | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ | Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
@@ -460,14 +462,14 @@
analz (insert (Crypt K X) H) \<subseteq>
insert (Crypt K X) (analz (insert X H))"
apply (rule subsetI)
-apply (erule_tac xa = x in analz.induct, auto)
+apply (erule_tac x = x in analz.induct, auto)
done
lemma lemma2: "Key (invKey K) \<in> analz H ==>
insert (Crypt K X) (analz (insert X H)) \<subseteq>
analz (insert (Crypt K X) H)"
apply auto
-apply (erule_tac xa = x in analz.induct, auto)
+apply (erule_tac x = x in analz.induct, auto)
apply (blast intro: analz_insertI analz.Decrypt)
done
@@ -579,15 +581,16 @@
encrypted with known keys. Agent names are public domain.
Numbers can be guessed, but Nonces cannot be. *}
-consts synth :: "msg set => msg set"
-inductive "synth H"
- intros
+inductive_set
+ synth :: "msg set => msg set"
+ for H :: "msg set"
+ where
Inj [intro]: "X \<in> H ==> X \<in> synth H"
- 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"
- Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+ | 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"
+ | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
text{*Monotonicity*}
lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"