src/HOL/MetisExamples/Message.thy
 changeset 23755 1c4672d130b1 parent 23449 dd874e6a3282 child 24759 b448f94b1c88
```     1.1 --- a/src/HOL/MetisExamples/Message.thy	Wed Jul 11 11:27:46 2007 +0200
1.2 +++ b/src/HOL/MetisExamples/Message.thy	Wed Jul 11 11:28:13 2007 +0200
1.3 @@ -68,13 +68,14 @@
1.4
1.5  subsubsection{*Inductive Definition of All Parts" of a Message*}
1.6
1.7 -consts  parts   :: "msg set => msg set"
1.8 -inductive "parts H"
1.9 -  intros
1.10 +inductive_set
1.11 +  parts :: "msg set => msg set"
1.12 +  for H :: "msg set"
1.13 +  where
1.14      Inj [intro]:               "X \<in> H ==> X \<in> parts H"
1.15 -    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
1.16 -    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
1.17 -    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
1.18 +  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
1.19 +  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
1.20 +  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
1.21
1.22
1.23  ML{*ResAtp.problem_name := "Message__parts_mono"*}
1.24 @@ -329,13 +330,14 @@
1.25      messages, including keys.  A form of downward closure.  Pairs can
1.26      be taken apart; messages decrypted with known keys.  *}
1.27
1.28 -consts  analz   :: "msg set => msg set"
1.29 -inductive "analz H"
1.30 -  intros
1.31 +inductive_set
1.32 +  analz :: "msg set => msg set"
1.33 +  for H :: "msg set"
1.34 +  where
1.35      Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
1.36 -    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
1.37 -    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
1.38 -    Decrypt [dest]:
1.39 +  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
1.40 +  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
1.41 +  | Decrypt [dest]:
1.42               "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
1.43
1.44
1.45 @@ -456,14 +458,14 @@
1.46                 analz (insert (Crypt K X) H) \<subseteq>
1.47                 insert (Crypt K X) (analz (insert X H))"
1.48  apply (rule subsetI)
1.49 -apply (erule_tac xa = x in analz.induct, auto)
1.50 +apply (erule_tac x = x in analz.induct, auto)
1.51  done
1.52
1.53  lemma lemma2: "Key (invKey K) \<in> analz H ==>
1.54                 insert (Crypt K X) (analz (insert X H)) \<subseteq>
1.55                 analz (insert (Crypt K X) H)"
1.56  apply auto
1.57 -apply (erule_tac xa = x in analz.induct, auto)
1.58 +apply (erule_tac x = x in analz.induct, auto)
1.59  apply (blast intro: analz_insertI analz.Decrypt)
1.60  done
1.61
1.62 @@ -579,15 +581,16 @@
1.63      encrypted with known keys.  Agent names are public domain.
1.64      Numbers can be guessed, but Nonces cannot be.  *}
1.65
1.66 -consts  synth   :: "msg set => msg set"
1.67 -inductive "synth H"
1.68 -  intros
1.69 +inductive_set
1.70 +  synth :: "msg set => msg set"
1.71 +  for H :: "msg set"
1.72 +  where
1.73      Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
1.74 -    Agent  [intro]:   "Agent agt \<in> synth H"
1.75 -    Number [intro]:   "Number n  \<in> synth H"
1.76 -    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
1.77 -    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
1.78 -    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
1.79 +  | Agent  [intro]:   "Agent agt \<in> synth H"
1.80 +  | Number [intro]:   "Number n  \<in> synth H"
1.81 +  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
1.82 +  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
1.83 +  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
1.84
1.85  text{*Monotonicity*}
1.86  lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
```