Adapted to new inductive definition package.
authorberghofe
Wed Jul 11 11:28:13 2007 +0200 (2007-07-11)
changeset 237551c4672d130b1
parent 23754 75873e94357c
child 23756 14008ce7df96
Adapted to new inductive definition package.
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Zorn.thy
src/HOL/MetisExamples/Message.thy
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/OpSem.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Nominal/Nominal.thy
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/SET-Protocol/Cardholder_Registration.thy
src/HOL/SET-Protocol/Merchant_Registration.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/Purchase.thy
     1.1 --- a/src/HOL/Library/Coinductive_List.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/Library/Coinductive_List.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -38,17 +38,27 @@
     1.4  
     1.5  subsection {* Corecursive lists *}
     1.6  
     1.7 -consts
     1.8 +coinductive_set
     1.9    LList  :: "'a Datatype.item set \<Rightarrow> 'a Datatype.item set"
    1.10 -
    1.11 -coinductive "LList A"
    1.12 -  intros
    1.13 +  for A :: "'a Datatype.item set"
    1.14 +  where
    1.15      NIL [intro]:  "NIL \<in> LList A"
    1.16 -    CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
    1.17 +  | CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
    1.18  
    1.19 -lemma LList_mono: "A \<subseteq> B \<Longrightarrow> LList A \<subseteq> LList B"
    1.20 +lemma LList_mono:
    1.21 +  assumes subset: "A \<subseteq> B"
    1.22 +  shows "LList A \<subseteq> LList B"
    1.23      -- {* This justifies using @{text LList} in other recursive type definitions. *}
    1.24 -  unfolding LList.defs by (blast intro!: gfp_mono)
    1.25 +proof
    1.26 +  fix x
    1.27 +  assume "x \<in> LList A"
    1.28 +  then show "x \<in> LList B"
    1.29 +  proof coinduct
    1.30 +    case LList
    1.31 +    then show ?case using subset
    1.32 +      by cases blast+
    1.33 +  qed
    1.34 +qed
    1.35  
    1.36  consts
    1.37    LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
    1.38 @@ -92,7 +102,7 @@
    1.39  
    1.40  lemma LList_corec_type: "LList_corec a f \<in> LList UNIV"
    1.41  proof -
    1.42 -  have "LList_corec a f \<in> {LList_corec a f | a. True}" by blast
    1.43 +  have "\<exists>x. LList_corec a f = LList_corec x f" by blast
    1.44    then show ?thesis
    1.45    proof coinduct
    1.46      case (LList L)
    1.47 @@ -185,7 +195,7 @@
    1.48      with Abs_llist have "l = LNil" by (simp add: LNil_def)
    1.49      with LNil show ?thesis .
    1.50    next
    1.51 -    case (CONS K a)
    1.52 +    case (CONS a K)
    1.53      then have "K \<in> llist" by (blast intro: llistI)
    1.54      then obtain l' where "K = Rep_llist l'" by cases
    1.55      with CONS and Abs_llist obtain x where "l = LCons x l'"
    1.56 @@ -228,7 +238,7 @@
    1.57    (is "?corec a \<in> _")
    1.58  proof (unfold llist_def)
    1.59    let "LList_corec a ?g" = "?corec a"
    1.60 -  have "?corec a \<in> {?corec x | x. True}" by blast
    1.61 +  have "\<exists>x. ?corec a = ?corec x" by blast
    1.62    then show "?corec a \<in> LList (range Datatype.Leaf)"
    1.63    proof coinduct
    1.64      case (LList L)
    1.65 @@ -282,14 +292,13 @@
    1.66  
    1.67  subsection {* Equality as greatest fixed-point -- the bisimulation principle *}
    1.68  
    1.69 -consts
    1.70 +coinductive_set
    1.71    EqLList :: "('a Datatype.item \<times> 'a Datatype.item) set \<Rightarrow>
    1.72      ('a Datatype.item \<times> 'a Datatype.item) set"
    1.73 -
    1.74 -coinductive "EqLList r"
    1.75 -  intros
    1.76 +  for r :: "('a Datatype.item \<times> 'a Datatype.item) set"
    1.77 +  where
    1.78      EqNIL: "(NIL, NIL) \<in> EqLList r"
    1.79 -    EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
    1.80 +  | EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
    1.81        (CONS a M, CONS b N) \<in> EqLList r"
    1.82  
    1.83  lemma EqLList_unfold:
    1.84 @@ -310,10 +319,10 @@
    1.85    done
    1.86  
    1.87  lemma Domain_EqLList: "Domain (EqLList (diag A)) \<subseteq> LList A"
    1.88 -  apply (simp add: LList.defs NIL_def CONS_def)
    1.89 -  apply (rule gfp_upperbound)
    1.90 -  apply (subst EqLList_unfold)
    1.91 -  apply auto
    1.92 +  apply (rule subsetI)
    1.93 +  apply (erule LList.coinduct)
    1.94 +  apply (subst (asm) EqLList_unfold)
    1.95 +  apply (auto simp add: NIL_def CONS_def)
    1.96    done
    1.97  
    1.98  lemma EqLList_diag: "EqLList (diag A) = diag (LList A)"
    1.99 @@ -328,23 +337,23 @@
   1.100         assumption)
   1.101      apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
   1.102      done
   1.103 -  show "?rhs \<subseteq> ?lhs"
   1.104 -  proof
   1.105 -    fix p assume "p \<in> diag (LList A)"
   1.106 -    then show "p \<in> EqLList (diag A)"
   1.107 +  {
   1.108 +    fix M N assume "(M, N) \<in> diag (LList A)"
   1.109 +    then have "(M, N) \<in> EqLList (diag A)"
   1.110      proof coinduct
   1.111 -      case (EqLList q)
   1.112 -      then obtain L where L: "L \<in> LList A" and q: "q = (L, L)" ..
   1.113 +      case (EqLList M N)
   1.114 +      then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
   1.115        from L show ?case
   1.116        proof cases
   1.117 -        case NIL with q have ?EqNIL by simp
   1.118 +        case NIL with MN have ?EqNIL by simp
   1.119          then show ?thesis ..
   1.120        next
   1.121 -        case CONS with q have ?EqCONS by (simp add: diagI)
   1.122 +        case CONS with MN have ?EqCONS by (simp add: diagI)
   1.123          then show ?thesis ..
   1.124        qed
   1.125      qed
   1.126 -  qed
   1.127 +  }
   1.128 +  then show "?rhs \<subseteq> ?lhs" by auto
   1.129  qed
   1.130  
   1.131  lemma EqLList_diag_iff [iff]: "(p \<in> EqLList (diag A)) = (p \<in> diag (LList A))"
   1.132 @@ -359,11 +368,11 @@
   1.133  lemma LList_equalityI
   1.134    [consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]:
   1.135    assumes r: "(M, N) \<in> r"
   1.136 -    and step: "\<And>p. p \<in> r \<Longrightarrow>
   1.137 -      p = (NIL, NIL) \<or>
   1.138 -        (\<exists>M N a b.
   1.139 -          p = (CONS a M, CONS b N) \<and> (a, b) \<in> diag A \<and>
   1.140 -            (M, N) \<in> r \<union> EqLList (diag A))"
   1.141 +    and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
   1.142 +      M = NIL \<and> N = NIL \<or>
   1.143 +        (\<exists>a b M' N'.
   1.144 +          M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> diag A \<and>
   1.145 +            ((M', N') \<in> r \<or> (M', N') \<in> EqLList (diag A)))"
   1.146    shows "M = N"
   1.147  proof -
   1.148    from r have "(M, N) \<in> EqLList (diag A)"
   1.149 @@ -391,39 +400,39 @@
   1.150    have "(f M, g M) \<in> ?bisim" using M by blast
   1.151    then show ?thesis
   1.152    proof (coinduct taking: A rule: LList_equalityI)
   1.153 -    case (EqLList q)
   1.154 -    then obtain L where q: "q = (f L, g L)" and L: "L \<in> LList A" by blast
   1.155 +    case (EqLList M N)
   1.156 +    then obtain L where MN: "M = f L" "N = g L" and L: "L \<in> LList A" by blast
   1.157      from L show ?case
   1.158      proof (cases L)
   1.159        case NIL
   1.160 -      with fun_NIL and q have "q \<in> diag (LList A)" by auto
   1.161 -      then have "q \<in> EqLList (diag A)" ..
   1.162 +      with fun_NIL and MN have "(M, N) \<in> diag (LList A)" by auto
   1.163 +      then have "(M, N) \<in> EqLList (diag A)" ..
   1.164        then show ?thesis by cases simp_all
   1.165      next
   1.166 -      case (CONS K a)
   1.167 +      case (CONS a K)
   1.168        from fun_CONS and `a \<in> A` `K \<in> LList A`
   1.169        have "?fun_CONS a K" (is "?NIL \<or> ?CONS") .
   1.170        then show ?thesis
   1.171        proof
   1.172          assume ?NIL
   1.173 -        with q CONS have "q \<in> diag (LList A)" by auto
   1.174 -        then have "q \<in> EqLList (diag A)" ..
   1.175 +        with MN CONS have "(M, N) \<in> diag (LList A)" by auto
   1.176 +        then have "(M, N) \<in> EqLList (diag A)" ..
   1.177          then show ?thesis by cases simp_all
   1.178        next
   1.179          assume ?CONS
   1.180 -        with CONS obtain a b M N where
   1.181 -            fg: "(f L, g L) = (CONS a M, CONS b N)"
   1.182 +        with CONS obtain a b M' N' where
   1.183 +            fg: "(f L, g L) = (CONS a M', CONS b N')"
   1.184            and ab: "(a, b) \<in> diag A"
   1.185 -          and MN: "(M, N) \<in> ?bisim \<union> diag (LList A)"
   1.186 +          and M'N': "(M', N') \<in> ?bisim \<union> diag (LList A)"
   1.187            by blast
   1.188 -        from MN show ?thesis
   1.189 +        from M'N' show ?thesis
   1.190          proof
   1.191 -          assume "(M, N) \<in> ?bisim"
   1.192 -          with q fg ab show ?thesis by simp
   1.193 +          assume "(M', N') \<in> ?bisim"
   1.194 +          with MN fg ab show ?thesis by simp
   1.195          next
   1.196 -          assume "(M, N) \<in> diag (LList A)"
   1.197 -          then have "(M, N) \<in> EqLList (diag A)" ..
   1.198 -          with q fg ab show ?thesis by simp
   1.199 +          assume "(M', N') \<in> diag (LList A)"
   1.200 +          then have "(M', N') \<in> EqLList (diag A)" ..
   1.201 +          with MN fg ab show ?thesis by simp
   1.202          qed
   1.203        qed
   1.204      qed
   1.205 @@ -446,18 +455,18 @@
   1.206    have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
   1.207    then show "h x = h' x"
   1.208    proof (coinduct rule: LList_equalityI [where A = UNIV])
   1.209 -    case (EqLList q)
   1.210 -    then obtain x where q: "q = (h x, h' x)" by blast
   1.211 +    case (EqLList M N)
   1.212 +    then obtain x where MN: "M = h x" "N = h' x" by blast
   1.213      show ?case
   1.214      proof (cases "f x")
   1.215        case None
   1.216 -      with h h' q have ?EqNIL by simp
   1.217 +      with h h' MN have ?EqNIL by simp
   1.218        then show ?thesis ..
   1.219      next
   1.220        case (Some p)
   1.221 -      with h h' q have "q =
   1.222 -          (CONS (fst p) (h (snd p)), CONS (fst p) (h' (snd p)))"
   1.223 -        by (simp split: prod.split)
   1.224 +      with h h' MN have "M = CONS (fst p) (h (snd p))"
   1.225 +	and "N = CONS (fst p) (h' (snd p))"
   1.226 +        by (simp_all split: prod.split)
   1.227        then have ?EqCONS by (auto iff: diag_iff)
   1.228        then show ?thesis ..
   1.229      qed
   1.230 @@ -481,18 +490,18 @@
   1.231      by blast
   1.232    then have "M = N"
   1.233    proof (coinduct rule: LList_equalityI [where A = UNIV])
   1.234 -    case (EqLList q)
   1.235 +    case (EqLList M N)
   1.236      then obtain l1 l2 where
   1.237 -        q: "q = (Rep_llist l1, Rep_llist l2)" and r: "(l1, l2) \<in> r"
   1.238 +        MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> r"
   1.239        by auto
   1.240      from step [OF r] show ?case
   1.241      proof
   1.242        assume "?EqLNil (l1, l2)"
   1.243 -      with q have ?EqNIL by (simp add: Rep_llist_LNil)
   1.244 +      with MN have ?EqNIL by (simp add: Rep_llist_LNil)
   1.245        then show ?thesis ..
   1.246      next
   1.247        assume "?EqLCons (l1, l2)"
   1.248 -      with q have ?EqCONS
   1.249 +      with MN have ?EqCONS
   1.250          by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV)
   1.251        then show ?thesis ..
   1.252      qed
   1.253 @@ -546,7 +555,7 @@
   1.254    assumes "M \<in> A"
   1.255    shows "Lconst M \<in> LList A"
   1.256  proof -
   1.257 -  have "Lconst M \<in> {Lconst M}" by simp
   1.258 +  have "Lconst M \<in> {Lconst (id M)}" by simp
   1.259    then show ?thesis
   1.260    proof coinduct
   1.261      case (LList N)
   1.262 @@ -617,16 +626,16 @@
   1.263    then show ?thesis
   1.264    proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
   1.265        rule: LList_equalityI)
   1.266 -    case (EqLList q)
   1.267 -    then obtain N where q: "q = (?lhs N, ?rhs N)" and N: "N \<in> LList A" by blast
   1.268 +    case (EqLList L M)
   1.269 +    then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> LList A" by blast
   1.270      from N show ?case
   1.271      proof cases
   1.272        case NIL
   1.273 -      with q have ?EqNIL by simp
   1.274 +      with LM have ?EqNIL by simp
   1.275        then show ?thesis ..
   1.276      next
   1.277        case CONS
   1.278 -      with q have ?EqCONS by auto
   1.279 +      with LM have ?EqCONS by auto
   1.280        then show ?thesis ..
   1.281      qed
   1.282    qed
   1.283 @@ -640,16 +649,16 @@
   1.284    then show ?thesis
   1.285    proof (coinduct taking: "range (\<lambda>N :: 'a Datatype.item. N)"
   1.286        rule: LList_equalityI)
   1.287 -    case (EqLList q)
   1.288 -    then obtain N where q: "q = (?lmap N, N)" and N: "N \<in> LList A" by blast
   1.289 +    case (EqLList L M)
   1.290 +    then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> LList A" by blast
   1.291      from N show ?case
   1.292      proof cases
   1.293        case NIL
   1.294 -      with q have ?EqNIL by simp
   1.295 +      with LM have ?EqNIL by simp
   1.296        then show ?thesis ..
   1.297      next
   1.298        case CONS
   1.299 -      with q have ?EqCONS by auto
   1.300 +      with LM have ?EqCONS by auto
   1.301        then show ?thesis ..
   1.302      qed
   1.303    qed
     2.1 --- a/src/HOL/Library/Graphs.thy	Wed Jul 11 11:27:46 2007 +0200
     2.2 +++ b/src/HOL/Library/Graphs.thy	Wed Jul 11 11:28:13 2007 +0200
     2.3 @@ -321,7 +321,7 @@
     2.4  
     2.5  types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
     2.6  
     2.7 -inductive2  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
     2.8 +inductive  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
     2.9    for G :: "('n, 'e) graph"
    2.10  where
    2.11    has_fpath_empty: "has_fpath G (n, [])"
     3.1 --- a/src/HOL/Library/Permutation.thy	Wed Jul 11 11:27:46 2007 +0200
     3.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jul 11 11:28:13 2007 +0200
     3.3 @@ -8,19 +8,13 @@
     3.4  imports Multiset
     3.5  begin
     3.6  
     3.7 -consts
     3.8 -  perm :: "('a list * 'a list) set"
     3.9 -
    3.10 -abbreviation
    3.11 -  perm_rel :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50) where
    3.12 -  "x <~~> y == (x, y) \<in> perm"
    3.13 -
    3.14 -inductive perm
    3.15 -  intros
    3.16 +inductive
    3.17 +  perm :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50)
    3.18 +  where
    3.19      Nil  [intro!]: "[] <~~> []"
    3.20 -    swap [intro!]: "y # x # l <~~> x # y # l"
    3.21 -    Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
    3.22 -    trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    3.23 +  | swap [intro!]: "y # x # l <~~> x # y # l"
    3.24 +  | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
    3.25 +  | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    3.26  
    3.27  lemma perm_refl [iff]: "l <~~> l"
    3.28    by (induct l) auto
     4.1 --- a/src/HOL/Library/Zorn.thy	Wed Jul 11 11:27:46 2007 +0200
     4.2 +++ b/src/HOL/Library/Zorn.thy	Wed Jul 11 11:28:13 2007 +0200
     4.3 @@ -33,12 +33,12 @@
     4.4      (if c \<notin> chain S | c \<in> maxchain S
     4.5      then c else SOME c'. c' \<in> super S c)"
     4.6  
     4.7 -consts
     4.8 +inductive_set
     4.9    TFin :: "'a set set => 'a set set set"
    4.10 -inductive "TFin S"
    4.11 -  intros
    4.12 +  for S :: "'a set set"
    4.13 +  where
    4.14      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    4.15 -    Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    4.16 +  | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    4.17    monos          Pow_mono
    4.18  
    4.19  
     5.1 --- a/src/HOL/MetisExamples/Message.thy	Wed Jul 11 11:27:46 2007 +0200
     5.2 +++ b/src/HOL/MetisExamples/Message.thy	Wed Jul 11 11:28:13 2007 +0200
     5.3 @@ -68,13 +68,14 @@
     5.4  
     5.5  subsubsection{*Inductive Definition of All Parts" of a Message*}
     5.6  
     5.7 -consts  parts   :: "msg set => msg set"
     5.8 -inductive "parts H"
     5.9 -  intros 
    5.10 +inductive_set
    5.11 +  parts :: "msg set => msg set"
    5.12 +  for H :: "msg set"
    5.13 +  where
    5.14      Inj [intro]:               "X \<in> H ==> X \<in> parts H"
    5.15 -    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    5.16 -    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    5.17 -    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    5.18 +  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
    5.19 +  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
    5.20 +  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
    5.21  
    5.22  
    5.23  ML{*ResAtp.problem_name := "Message__parts_mono"*}
    5.24 @@ -329,13 +330,14 @@
    5.25      messages, including keys.  A form of downward closure.  Pairs can
    5.26      be taken apart; messages decrypted with known keys.  *}
    5.27  
    5.28 -consts  analz   :: "msg set => msg set"
    5.29 -inductive "analz H"
    5.30 -  intros 
    5.31 +inductive_set
    5.32 +  analz :: "msg set => msg set"
    5.33 +  for H :: "msg set"
    5.34 +  where
    5.35      Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
    5.36 -    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    5.37 -    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    5.38 -    Decrypt [dest]: 
    5.39 +  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
    5.40 +  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
    5.41 +  | Decrypt [dest]: 
    5.42               "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
    5.43  
    5.44  
    5.45 @@ -456,14 +458,14 @@
    5.46                 analz (insert (Crypt K X) H) \<subseteq>  
    5.47                 insert (Crypt K X) (analz (insert X H))" 
    5.48  apply (rule subsetI)
    5.49 -apply (erule_tac xa = x in analz.induct, auto)
    5.50 +apply (erule_tac x = x in analz.induct, auto)
    5.51  done
    5.52  
    5.53  lemma lemma2: "Key (invKey K) \<in> analz H ==>   
    5.54                 insert (Crypt K X) (analz (insert X H)) \<subseteq>  
    5.55                 analz (insert (Crypt K X) H)"
    5.56  apply auto
    5.57 -apply (erule_tac xa = x in analz.induct, auto)
    5.58 +apply (erule_tac x = x in analz.induct, auto)
    5.59  apply (blast intro: analz_insertI analz.Decrypt)
    5.60  done
    5.61  
    5.62 @@ -579,15 +581,16 @@
    5.63      encrypted with known keys.  Agent names are public domain.
    5.64      Numbers can be guessed, but Nonces cannot be.  *}
    5.65  
    5.66 -consts  synth   :: "msg set => msg set"
    5.67 -inductive "synth H"
    5.68 -  intros 
    5.69 +inductive_set
    5.70 +  synth :: "msg set => msg set"
    5.71 +  for H :: "msg set"
    5.72 +  where
    5.73      Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
    5.74 -    Agent  [intro]:   "Agent agt \<in> synth H"
    5.75 -    Number [intro]:   "Number n  \<in> synth H"
    5.76 -    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
    5.77 -    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    5.78 -    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    5.79 +  | Agent  [intro]:   "Agent agt \<in> synth H"
    5.80 +  | Number [intro]:   "Number n  \<in> synth H"
    5.81 +  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
    5.82 +  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
    5.83 +  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
    5.84  
    5.85  text{*Monotonicity*}
    5.86  lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
     6.1 --- a/src/HOL/NanoJava/AxSem.thy	Wed Jul 11 11:27:46 2007 +0200
     6.2 +++ b/src/HOL/NanoJava/AxSem.thy	Wed Jul 11 11:28:13 2007 +0200
     6.3 @@ -18,116 +18,102 @@
     6.4    "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times>  assn"
     6.5   "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
     6.6  
     6.7 -consts   hoare   :: "(triple set \<times>  triple set) set"
     6.8 -consts  ehoare   :: "(triple set \<times> etriple    ) set"
     6.9 -syntax (xsymbols)
    6.10 - "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
    6.11 - "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
    6.12 -                                   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    6.13 -"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ |\<turnstile>\<^sub>e/ _"[61,61]60)
    6.14 -"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
    6.15 -                                  ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
    6.16 -syntax
    6.17 - "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
    6.18 - "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
    6.19 -                                  ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
    6.20 -"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ ||-e/ _"[61,61] 60)
    6.21 -"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
    6.22 -                                 ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
    6.23 -
    6.24 -translations "A |\<turnstile> C"        \<rightleftharpoons> "(A,C) \<in> hoare"
    6.25 -             "A  \<turnstile> {P}c{Q}"  \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
    6.26 -             "A |\<turnstile>\<^sub>e t"       \<rightleftharpoons> "(A,t) \<in> ehoare"
    6.27 -             "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *)
    6.28 -             "A  \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)"
    6.29 -
    6.30  
    6.31  subsection "Hoare Logic Rules"
    6.32  
    6.33 -inductive hoare ehoare
    6.34 -intros
    6.35 -
    6.36 -  Skip:  "A |- {P} Skip {P}"
    6.37 -
    6.38 -  Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
    6.39 +inductive
    6.40 + hoare :: "[triple set, triple set] => bool"  ("_ |\<turnstile>/ _" [61, 61] 60)
    6.41 + and ehoare :: "[triple set, etriple] => bool"  ("_ |\<turnstile>\<^sub>e/ _" [61, 61] 60)
    6.42 + and hoare1 :: "[triple set, assn,stmt,assn] => bool" 
    6.43 +   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
    6.44 + and ehoare1 :: "[triple set, assn,expr,vassn]=> bool"
    6.45 +   ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
    6.46 +where
    6.47  
    6.48 -  Cond: "[| A |-e {P} e {Q}; 
    6.49 -            \<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
    6.50 -            A |- {P} If(e) c1 Else c2 {R}"
    6.51 +  "A  \<turnstile> {P}c{Q} \<equiv> A |\<turnstile> {(P,c,Q)}"
    6.52 +| "A  \<turnstile>\<^sub>e {P}e{Q} \<equiv> A |\<turnstile>\<^sub>e (P,e,Q)"
    6.53  
    6.54 -  Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
    6.55 -         A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
    6.56 +| Skip:  "A \<turnstile> {P} Skip {P}"
    6.57 +
    6.58 +| Comp: "[| A \<turnstile> {P} c1 {Q}; A \<turnstile> {Q} c2 {R} |] ==> A \<turnstile> {P} c1;;c2 {R}"
    6.59  
    6.60 -  LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
    6.61 +| Cond: "[| A \<turnstile>\<^sub>e {P} e {Q}; 
    6.62 +            \<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
    6.63 +            A \<turnstile> {P} If(e) c1 Else c2 {R}"
    6.64  
    6.65 -  LAss: "A |-e {P} e {\<lambda>v s.  Q (lupd(x\<mapsto>v) s)} ==>
    6.66 -         A |-  {P} x:==e {Q}"
    6.67 +| Loop: "A \<turnstile> {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
    6.68 +         A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
    6.69 +
    6.70 +| LAcc: "A \<turnstile>\<^sub>e {\<lambda>s. P (s<x>) s} LAcc x {P}"
    6.71  
    6.72 -  FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
    6.73 -         A |-e {P} e..f {Q}"
    6.74 +| LAss: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s.  Q (lupd(x\<mapsto>v) s)} ==>
    6.75 +         A \<turnstile>  {P} x:==e {Q}"
    6.76 +
    6.77 +| FAcc: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
    6.78 +         A \<turnstile>\<^sub>e {P} e..f {Q}"
    6.79  
    6.80 -  FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
    6.81 -        \<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
    6.82 -            A |-  {P} e1..f:==e2 {R}"
    6.83 +| FAss: "[| A \<turnstile>\<^sub>e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
    6.84 +        \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
    6.85 +            A \<turnstile>  {P} e1..f:==e2 {R}"
    6.86  
    6.87 -  NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
    6.88 +| NewC: "A \<turnstile>\<^sub>e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
    6.89                  new C {P}"
    6.90  
    6.91 -  Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True 
    6.92 +| Cast: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. (case v of Null => True 
    6.93                                   | Addr a => obj_class s a <=C C) --> Q v s} ==>
    6.94 -         A |-e {P} Cast C e {Q}"
    6.95 +         A \<turnstile>\<^sub>e {P} Cast C e {Q}"
    6.96  
    6.97 -  Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
    6.98 -    \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 
    6.99 +| Call: "[| A \<turnstile>\<^sub>e {P} e1 {Q}; \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {R a};
   6.100 +    \<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 
   6.101                      s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
   6.102                    Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
   6.103 -             A |-e {P} {C}e1..m(e2) {S}"
   6.104 +             A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"
   6.105  
   6.106 -  Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> 
   6.107 +| Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> 
   6.108                          P s \<and> s' = init_locs D m s}
   6.109                    Impl (D,m) {Q} ==>
   6.110 -             A |- {P} Meth (C,m) {Q}"
   6.111 +             A \<turnstile> {P} Meth (C,m) {Q}"
   6.112  
   6.113    --{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\
   6.114         Z restricted to type state due to limitations of the inductive package *}
   6.115 -  Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- 
   6.116 +| Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
   6.117                              (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
   6.118 -                      A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
   6.119 +                      A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
   6.120  
   6.121  --{* structural rules *}
   6.122  
   6.123 -  Asm:  "   a \<in> A ==> A ||- {a}"
   6.124 +| Asm:  "   a \<in> A ==> A |\<turnstile> {a}"
   6.125  
   6.126 -  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
   6.127 +| ConjI: " \<forall>c \<in> C. A |\<turnstile> {c} ==> A |\<turnstile> C"
   6.128  
   6.129 -  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
   6.130 +| ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}"
   6.131  
   6.132    --{* Z restricted to type state due to limitations of the inductive package *}
   6.133 -  Conseq:"[| \<forall>Z::state. A |- {P' Z} c {Q' Z};
   6.134 +| Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z};
   6.135               \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
   6.136 -            A |- {P} c {Q }"
   6.137 +            A \<turnstile> {P} c {Q }"
   6.138  
   6.139    --{* Z restricted to type state due to limitations of the inductive package *}
   6.140 - eConseq:"[| \<forall>Z::state. A |-e {P' Z} e {Q' Z};
   6.141 +| eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
   6.142               \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
   6.143 -            A |-e {P} e {Q }"
   6.144 +            A \<turnstile>\<^sub>e {P} e {Q }"
   6.145  
   6.146  
   6.147  subsection "Fully polymorphic variants, required for Example only"
   6.148  
   6.149  axioms
   6.150  
   6.151 -  Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z};
   6.152 +  Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
   6.153               \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
   6.154 -                 A |- {P} c {Q }"
   6.155 +                 A \<turnstile> {P} c {Q }"
   6.156  
   6.157 - eConseq:"[| \<forall>Z. A |-e {P' Z} e {Q' Z};
   6.158 + eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
   6.159               \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
   6.160 -                 A |-e {P} e {Q }"
   6.161 +                 A \<turnstile>\<^sub>e {P} e {Q }"
   6.162  
   6.163 - Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- 
   6.164 + Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
   6.165                            (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
   6.166 -                    A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
   6.167 +                    A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
   6.168  
   6.169  subsection "Derived Rules"
   6.170  
     7.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Jul 11 11:27:46 2007 +0200
     7.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Jul 11 11:28:13 2007 +0200
     7.3 @@ -12,17 +12,17 @@
     7.4  
     7.5  constdefs
     7.6    valid   :: "[assn,stmt, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
     7.7 - "|=  {P} c {Q} \<equiv> \<forall>s   t. P s --> (\<exists>n. s -c  -n-> t) --> Q   t"
     7.8 + "|=  {P} c {Q} \<equiv> \<forall>s   t. P s --> (\<exists>n. s -c  -n\<rightarrow> t) --> Q   t"
     7.9  
    7.10   evalid   :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    7.11 - "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e>v-n-> t) --> Q v t"
    7.12 + "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e\<succ>v-n\<rightarrow> t) --> Q v t"
    7.13  
    7.14  
    7.15   nvalid   :: "[nat, triple    ] => bool" ("|=_: _"  [61,61] 60)
    7.16 - "|=n:  t \<equiv> let (P,c,Q) = t in \<forall>s   t. s -c  -n-> t --> P s --> Q   t"
    7.17 + "|=n:  t \<equiv> let (P,c,Q) = t in \<forall>s   t. s -c  -n\<rightarrow> t --> P s --> Q   t"
    7.18  
    7.19  envalid   :: "[nat,etriple    ] => bool" ("|=_:e _" [61,61] 60)
    7.20 - "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e>v-n-> t --> P s --> Q v t"
    7.21 + "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e\<succ>v-n\<rightarrow> t --> P s --> Q v t"
    7.22  
    7.23    nvalids :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
    7.24   "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
    7.25 @@ -108,8 +108,8 @@
    7.26  apply (rule hoare_ehoare.induct)
    7.27  (*18*)
    7.28  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
    7.29 -apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x :  hoare") *})
    7.30 -apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
    7.31 +apply (tactic {* ALLGOALS (REPEAT o thin_tac "hoare ?x ?y") *})
    7.32 +apply (tactic {* ALLGOALS (REPEAT o thin_tac "ehoare ?x ?y") *})
    7.33  apply (simp_all only: cnvalid1_eq cenvalid_def2)
    7.34                   apply fast
    7.35                  apply fast
    7.36 @@ -161,9 +161,9 @@
    7.37  subsection "(Relative) Completeness"
    7.38  
    7.39  constdefs MGT    :: "stmt => state =>  triple"
    7.40 -         "MGT  c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda>  t. \<exists>n. Z -c-  n-> t)"
    7.41 +         "MGT  c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda>  t. \<exists>n. Z -c-  n\<rightarrow> t)"
    7.42            MGTe   :: "expr => state => etriple"
    7.43 -         "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
    7.44 +         "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
    7.45  syntax (xsymbols)
    7.46           MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
    7.47  syntax (HTML output)
     8.1 --- a/src/HOL/NanoJava/OpSem.thy	Wed Jul 11 11:27:46 2007 +0200
     8.2 +++ b/src/HOL/NanoJava/OpSem.thy	Wed Jul 11 11:28:13 2007 +0200
     8.3 @@ -8,61 +8,51 @@
     8.4  
     8.5  theory OpSem imports State begin
     8.6  
     8.7 -consts
     8.8 - exec :: "(state \<times> stmt       \<times> nat \<times> state) set"
     8.9 - eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
    8.10 -syntax (xsymbols)
    8.11 - exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
    8.12 - eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
    8.13 -syntax
    8.14 - exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   65,98]89)
    8.15 - eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89)
    8.16 -translations
    8.17 - "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
    8.18 - "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
    8.19 +inductive
    8.20 +  exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
    8.21 +  and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
    8.22 +where
    8.23 +  Skip: "   s -Skip-n\<rightarrow> s"
    8.24 +
    8.25 +| Comp: "[| s0 -c1-n\<rightarrow> s1; s1 -c2-n\<rightarrow> s2 |] ==>
    8.26 +            s0 -c1;; c2-n\<rightarrow> s2"
    8.27  
    8.28 -inductive exec eval intros
    8.29 -  Skip: "   s -Skip-n-> s"
    8.30 -
    8.31 -  Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
    8.32 -            s0 -c1;; c2-n-> s2"
    8.33 +| Cond: "[| s0 -e\<succ>v-n\<rightarrow> s1; s1 -(if v\<noteq>Null then c1 else c2)-n\<rightarrow> s2 |] ==>
    8.34 +            s0 -If(e) c1 Else c2-n\<rightarrow> s2"
    8.35  
    8.36 -  Cond: "[| s0 -e>v-n-> s1; s1 -(if v\<noteq>Null then c1 else c2)-n-> s2 |] ==>
    8.37 -            s0 -If(e) c1 Else c2-n-> s2"
    8.38 +| LoopF:"   s0<x> = Null ==>
    8.39 +            s0 -While(x) c-n\<rightarrow> s0"
    8.40 +| LoopT:"[| s0<x> \<noteq> Null; s0 -c-n\<rightarrow> s1; s1 -While(x) c-n\<rightarrow> s2 |] ==>
    8.41 +            s0 -While(x) c-n\<rightarrow> s2"
    8.42  
    8.43 -  LoopF:"   s0<x> = Null ==>
    8.44 -            s0 -While(x) c-n-> s0"
    8.45 -  LoopT:"[| s0<x> \<noteq> Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==>
    8.46 -            s0 -While(x) c-n-> s2"
    8.47 +| LAcc: "   s -LAcc x\<succ>s<x>-n\<rightarrow> s"
    8.48 +
    8.49 +| LAss: "   s -e\<succ>v-n\<rightarrow> s' ==>
    8.50 +            s -x:==e-n\<rightarrow> lupd(x\<mapsto>v) s'"
    8.51  
    8.52 -  LAcc: "   s -LAcc x>s<x>-n-> s"
    8.53 -
    8.54 -  LAss: "   s -e>v-n-> s' ==>
    8.55 -            s -x:==e-n-> lupd(x\<mapsto>v) s'"
    8.56 +| FAcc: "   s -e\<succ>Addr a-n\<rightarrow> s' ==>
    8.57 +            s -e..f\<succ>get_field s' a f-n\<rightarrow> s'"
    8.58  
    8.59 -  FAcc: "   s -e>Addr a-n-> s' ==>
    8.60 -            s -e..f>get_field s' a f-n-> s'"
    8.61 +| FAss: "[| s0 -e1\<succ>Addr a-n\<rightarrow> s1;  s1 -e2\<succ>v-n\<rightarrow> s2 |] ==>
    8.62 +            s0 -e1..f:==e2-n\<rightarrow> upd_obj a f v s2"
    8.63  
    8.64 -  FAss: "[| s0 -e1>Addr a-n-> s1;  s1 -e2>v-n-> s2 |] ==>
    8.65 -            s0 -e1..f:==e2-n-> upd_obj a f v s2"
    8.66 -
    8.67 -  NewC: "   new_Addr s = Addr a ==>
    8.68 -            s -new C>Addr a-n-> new_obj a C s"
    8.69 +| NewC: "   new_Addr s = Addr a ==>
    8.70 +            s -new C\<succ>Addr a-n\<rightarrow> new_obj a C s"
    8.71  
    8.72 -  Cast: "[| s -e>v-n-> s';
    8.73 +| Cast: "[| s -e\<succ>v-n\<rightarrow> s';
    8.74              case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
    8.75 -            s -Cast C e>v-n-> s'"
    8.76 +            s -Cast C e\<succ>v-n\<rightarrow> s'"
    8.77  
    8.78 -  Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
    8.79 -            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n-> s3
    8.80 -     |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
    8.81 +| Call: "[| s0 -e1\<succ>a-n\<rightarrow> s1; s1 -e2\<succ>p-n\<rightarrow> s2; 
    8.82 +            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n\<rightarrow> s3
    8.83 +     |] ==> s0 -{C}e1..m(e2)\<succ>s3<Res>-n\<rightarrow> set_locs s2 s3"
    8.84  
    8.85 -  Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
    8.86 -            init_locs D m s -Impl (D,m)-n-> s' |] ==>
    8.87 -            s -Meth (C,m)-n-> s'"
    8.88 +| Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
    8.89 +            init_locs D m s -Impl (D,m)-n\<rightarrow> s' |] ==>
    8.90 +            s -Meth (C,m)-n\<rightarrow> s'"
    8.91  
    8.92 -  Impl: "   s -body Cm-    n-> s' ==>
    8.93 -            s -Impl Cm-Suc n-> s'"
    8.94 +| Impl: "   s -body Cm-    n\<rightarrow> s' ==>
    8.95 +            s -Impl Cm-Suc n\<rightarrow> s'"
    8.96  
    8.97  
    8.98  inductive_cases exec_elim_cases':
     9.1 --- a/src/HOL/NanoJava/TypeRel.thy	Wed Jul 11 11:27:46 2007 +0200
     9.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Wed Jul 11 11:28:13 2007 +0200
     9.3 @@ -9,22 +9,18 @@
     9.4  theory TypeRel imports Decl begin
     9.5  
     9.6  consts
     9.7 -  widen   :: "(ty    \<times> ty   ) set"  --{* widening *}
     9.8    subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
     9.9  
    9.10  syntax (xsymbols)
    9.11 -  widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
    9.12    subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _"  [71,71] 70)
    9.13    subcls  :: "[cname, cname] => bool" ("_ \<preceq>C _"   [71,71] 70)
    9.14  syntax
    9.15 -  widen   :: "[ty   , ty   ] => bool" ("_ <= _"   [71,71] 70)
    9.16    subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
    9.17    subcls  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
    9.18  
    9.19  translations
    9.20    "C \<prec>C1 D" == "(C,D) \<in> subcls1"
    9.21    "C \<preceq>C  D" == "(C,D) \<in> subcls1^*"
    9.22 -  "S \<preceq>   T" == "(S,T) \<in> widen"
    9.23  
    9.24  consts
    9.25    method :: "cname => (mname \<rightharpoonup> methd)"
    9.26 @@ -38,10 +34,12 @@
    9.27   subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
    9.28  
    9.29  text{* Widening, viz. method invocation conversion *}
    9.30 -inductive widen intros 
    9.31 -  refl   [intro!, simp]:           "T \<preceq> T"
    9.32 -  subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    9.33 -  null   [intro!]:                "NT \<preceq> R"
    9.34 +inductive
    9.35 +  widen :: "ty => ty => bool"  ("_ \<preceq> _" [71,71] 70)
    9.36 +where
    9.37 +  refl [intro!, simp]: "T \<preceq> T"
    9.38 +| subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    9.39 +| null [intro!]: "NT \<preceq> R"
    9.40  
    9.41  lemma subcls1D: 
    9.42    "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
    10.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Jul 11 11:27:46 2007 +0200
    10.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Jul 11 11:28:13 2007 +0200
    10.3 @@ -3048,10 +3048,9 @@
    10.4  
    10.5  section {* abstraction type for the parsing in nominal datatype *}
    10.6  (*==============================================================*)
    10.7 -consts
    10.8 -  "ABS_set" :: "('x\<Rightarrow>('a noption)) set"
    10.9 -inductive ABS_set
   10.10 -  intros
   10.11 +
   10.12 +inductive_set ABS_set :: "('x\<Rightarrow>('a noption)) set"
   10.13 +  where
   10.14    ABS_in: "(abs_fun a x)\<in>ABS_set"
   10.15  
   10.16  typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
    11.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Wed Jul 11 11:27:46 2007 +0200
    11.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Wed Jul 11 11:28:13 2007 +0200
    11.3 @@ -15,13 +15,12 @@
    11.4    \bigskip
    11.5  *}
    11.6  
    11.7 -consts
    11.8 +inductive_set
    11.9    bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
   11.10 -
   11.11 -inductive "bijR P"
   11.12 -  intros
   11.13 +  for P :: "'a => 'b => bool"
   11.14 +where
   11.15    empty [simp]: "({}, {}) \<in> bijR P"
   11.16 -  insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
   11.17 +| insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
   11.18      ==> (insert a A, insert b B) \<in> bijR P"
   11.19  
   11.20  text {*
   11.21 @@ -41,14 +40,13 @@
   11.22    symP :: "('a => 'a => bool) => bool" where
   11.23    "symP P = (\<forall>a b. P a b = P b a)"
   11.24  
   11.25 -consts
   11.26 +inductive_set
   11.27    bijER :: "('a => 'a => bool) => 'a set set"
   11.28 -
   11.29 -inductive "bijER P"
   11.30 -  intros
   11.31 +  for P :: "'a => 'a => bool"
   11.32 +where
   11.33    empty [simp]: "{} \<in> bijER P"
   11.34 -  insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
   11.35 -  insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
   11.36 +| insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
   11.37 +| insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
   11.38      ==> insert a (insert b A) \<in> bijER P"
   11.39  
   11.40  
    12.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Wed Jul 11 11:27:46 2007 +0200
    12.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Wed Jul 11 11:28:13 2007 +0200
    12.3 @@ -17,13 +17,12 @@
    12.4  
    12.5  subsection {* Definitions and lemmas *}
    12.6  
    12.7 -consts
    12.8 +inductive_set
    12.9    RsetR :: "int => int set set"
   12.10 -
   12.11 -inductive "RsetR m"
   12.12 -  intros
   12.13 +  for m :: int
   12.14 +  where
   12.15      empty [simp]: "{} \<in> RsetR m"
   12.16 -    insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
   12.17 +  | insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
   12.18        \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
   12.19  
   12.20  consts
    13.1 --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy	Wed Jul 11 11:27:46 2007 +0200
    13.2 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy	Wed Jul 11 11:28:13 2007 +0200
    13.3 @@ -92,26 +92,26 @@
    13.4  
    13.5  subsection{*Formal protocol definition *}
    13.6  
    13.7 -consts  set_cr  :: "event list set"
    13.8 -inductive set_cr
    13.9 - intros
   13.10 +inductive_set
   13.11 +  set_cr :: "event list set"
   13.12 +where
   13.13  
   13.14    Nil:    --{*Initial trace is empty*}
   13.15  	  "[] \<in> set_cr"
   13.16  
   13.17 -  Fake:    --{*The spy MAY say anything he CAN say.*}
   13.18 +| Fake:    --{*The spy MAY say anything he CAN say.*}
   13.19  	   "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
   13.20  	    ==> Says Spy B X  # evsf \<in> set_cr"
   13.21  
   13.22 -  Reception: --{*If A sends a message X to B, then B might receive it*}
   13.23 +| Reception: --{*If A sends a message X to B, then B might receive it*}
   13.24  	     "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
   13.25                ==> Gets B X  # evsr \<in> set_cr"
   13.26  
   13.27 -  SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
   13.28 +| SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
   13.29  	     "[| evs1 \<in> set_cr;  C = Cardholder k;  Nonce NC1 \<notin> used evs1 |]
   13.30  	      ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
   13.31  
   13.32 -  SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
   13.33 +| SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
   13.34  	     "[| evs2 \<in> set_cr;
   13.35  		 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
   13.36  	      ==> Says (CA i) C
   13.37 @@ -120,7 +120,7 @@
   13.38  			 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
   13.39  		    # evs2 \<in> set_cr"
   13.40  
   13.41 -  SET_CR3:
   13.42 +| SET_CR3:
   13.43     --{*RegFormReq: C sends his PAN and a new nonce to CA.
   13.44     C verifies that
   13.45      - nonce received is the same as that sent;
   13.46 @@ -144,7 +144,7 @@
   13.47         # Notes C {|Key KC1, Agent (CA i)|}
   13.48         # evs3 \<in> set_cr"
   13.49  
   13.50 -  SET_CR4:
   13.51 +| SET_CR4:
   13.52      --{*RegFormRes:
   13.53      CA responds sending NC2 back with a new nonce NCA, after checking that
   13.54       - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
   13.55 @@ -160,7 +160,7 @@
   13.56  	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
   13.57         # evs4 \<in> set_cr"
   13.58  
   13.59 -  SET_CR5:
   13.60 +| SET_CR5:
   13.61     --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
   13.62         and its half of the secret value to CA.
   13.63         We now assume that C has a fixed key pair, and he submits (pubSK C).
   13.64 @@ -196,7 +196,7 @@
   13.65     which is just @{term "Crypt K (sign SK X)"}.
   13.66  *}
   13.67  
   13.68 -SET_CR6:
   13.69 +| SET_CR6:
   13.70  "[| evs6 \<in> set_cr;
   13.71      Nonce NonceCCA \<notin> used evs6;
   13.72      KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;
    14.1 --- a/src/HOL/SET-Protocol/Merchant_Registration.thy	Wed Jul 11 11:27:46 2007 +0200
    14.2 +++ b/src/HOL/SET-Protocol/Merchant_Registration.thy	Wed Jul 11 11:28:13 2007 +0200
    14.3 @@ -13,30 +13,30 @@
    14.4    encryption keys (@{term "priEK C"}). *}
    14.5  
    14.6  
    14.7 -consts  set_mr  :: "event list set"
    14.8 -inductive set_mr
    14.9 - intros
   14.10 +inductive_set
   14.11 +  set_mr :: "event list set"
   14.12 +where
   14.13  
   14.14    Nil:    --{*Initial trace is empty*}
   14.15  	   "[] \<in> set_mr"
   14.16  
   14.17  
   14.18 -  Fake:    --{*The spy MAY say anything he CAN say.*}
   14.19 +| Fake:    --{*The spy MAY say anything he CAN say.*}
   14.20  	   "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |]
   14.21  	    ==> Says Spy B X  # evsf \<in> set_mr"
   14.22  	
   14.23  
   14.24 -  Reception: --{*If A sends a message X to B, then B might receive it*}
   14.25 +| Reception: --{*If A sends a message X to B, then B might receive it*}
   14.26  	     "[| evsr \<in> set_mr; Says A B X \<in> set evsr |]
   14.27                ==> Gets B X  # evsr \<in> set_mr"
   14.28  
   14.29  
   14.30 -  SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
   14.31 +| SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
   14.32   	   "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
   14.33              ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr"
   14.34  
   14.35  
   14.36 -  SET_MR2: --{*RegFormRes: CA replies with the registration form and the 
   14.37 +| SET_MR2: --{*RegFormRes: CA replies with the registration form and the 
   14.38                 certificates for her keys*}
   14.39    "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2;
   14.40        Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
   14.41 @@ -45,7 +45,7 @@
   14.42                         cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
   14.43  	 # evs2 \<in> set_mr"
   14.44  
   14.45 -  SET_MR3:
   14.46 +| SET_MR3:
   14.47           --{*CertReq: M submits the key pair to be certified.  The Notes
   14.48               event allows KM1 to be lost if M is compromised. Piero remarks
   14.49               that the agent mentioned inside the signature is not verified to
   14.50 @@ -66,7 +66,7 @@
   14.51  	 # Notes M {|Key KM1, Agent (CA i)|}
   14.52  	 # evs3 \<in> set_mr"
   14.53  
   14.54 -  SET_MR4:
   14.55 +| SET_MR4:
   14.56           --{*CertRes: CA issues the certificates for merSK and merEK,
   14.57               while checking never to have certified the m even
   14.58               separately. NOTE: In Cardholder Registration the
    15.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Jul 11 11:27:46 2007 +0200
    15.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Jul 11 11:28:13 2007 +0200
    15.3 @@ -100,13 +100,14 @@
    15.4  
    15.5  subsubsection{*Inductive definition of all "parts" of a message.*}
    15.6  
    15.7 -consts  parts   :: "msg set => msg set"
    15.8 -inductive "parts H"
    15.9 -  intros
   15.10 +inductive_set
   15.11 +  parts :: "msg set => msg set"
   15.12 +  for H :: "msg set"
   15.13 +  where
   15.14      Inj [intro]:               "X \<in> H ==> X \<in> parts H"
   15.15 -    Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
   15.16 -    Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
   15.17 -    Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
   15.18 +  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
   15.19 +  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
   15.20 +  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
   15.21  
   15.22  
   15.23  (*Monotonicity*)
   15.24 @@ -391,13 +392,14 @@
   15.25      messages, including keys.  A form of downward closure.  Pairs can
   15.26      be taken apart; messages decrypted with known keys.*}
   15.27  
   15.28 -consts  analz   :: "msg set => msg set"
   15.29 -inductive "analz H"
   15.30 -  intros
   15.31 +inductive_set
   15.32 +  analz :: "msg set => msg set"
   15.33 +  for H :: "msg set"
   15.34 +  where
   15.35      Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
   15.36 -    Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   15.37 -    Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   15.38 -    Decrypt [dest]:
   15.39 +  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
   15.40 +  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
   15.41 +  | Decrypt [dest]:
   15.42               "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
   15.43  
   15.44  
   15.45 @@ -521,14 +523,14 @@
   15.46                 analz (insert (Crypt K X) H) \<subseteq>
   15.47                 insert (Crypt K X) (analz (insert X H))"
   15.48  apply (rule subsetI)
   15.49 -apply (erule_tac xa = x in analz.induct, auto)
   15.50 +apply (erule_tac x = x in analz.induct, auto)
   15.51  done
   15.52  
   15.53  lemma lemma2: "Key (invKey K) \<in> analz H ==>
   15.54                 insert (Crypt K X) (analz (insert X H)) \<subseteq>
   15.55                 analz (insert (Crypt K X) H)"
   15.56  apply auto
   15.57 -apply (erule_tac xa = x in analz.induct, auto)
   15.58 +apply (erule_tac x = x in analz.induct, auto)
   15.59  apply (blast intro: analz_insertI analz.Decrypt)
   15.60  done
   15.61  
   15.62 @@ -639,15 +641,16 @@
   15.63      encrypted with known keys.  Agent names are public domain.
   15.64      Numbers can be guessed, but Nonces cannot be.*}
   15.65  
   15.66 -consts  synth   :: "msg set => msg set"
   15.67 -inductive "synth H"
   15.68 -  intros
   15.69 +inductive_set
   15.70 +  synth :: "msg set => msg set"
   15.71 +  for H :: "msg set"
   15.72 +  where
   15.73      Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
   15.74 -    Agent  [intro]:   "Agent agt \<in> synth H"
   15.75 -    Number [intro]:   "Number n  \<in> synth H"
   15.76 -    Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   15.77 -    MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   15.78 -    Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   15.79 +  | Agent  [intro]:   "Agent agt \<in> synth H"
   15.80 +  | Number [intro]:   "Number n  \<in> synth H"
   15.81 +  | Hash   [intro]:   "X \<in> synth H ==> Hash X \<in> synth H"
   15.82 +  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
   15.83 +  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
   15.84  
   15.85  (*Monotonicity*)
   15.86  lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
    16.1 --- a/src/HOL/SET-Protocol/Purchase.thy	Wed Jul 11 11:27:46 2007 +0200
    16.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Wed Jul 11 11:28:13 2007 +0200
    16.3 @@ -57,24 +57,23 @@
    16.4      PANSecret :: "nat => nat"
    16.5       --{*Maps Cardholders to PANSecrets.*}
    16.6  
    16.7 -    set_pur  :: "event list set"
    16.8 -
    16.9 -inductive set_pur
   16.10 - intros
   16.11 +inductive_set
   16.12 +  set_pur :: "event list set"
   16.13 +where
   16.14  
   16.15    Nil:   --{*Initial trace is empty*}
   16.16  	 "[] \<in> set_pur"
   16.17  
   16.18 -  Fake:  --{*The spy MAY say anything he CAN say.*}
   16.19 +| Fake:  --{*The spy MAY say anything he CAN say.*}
   16.20  	 "[| evsf \<in> set_pur;  X \<in> synth(analz(knows Spy evsf)) |]
   16.21  	  ==> Says Spy B X  # evsf \<in> set_pur"
   16.22  
   16.23  
   16.24 -  Reception: --{*If A sends a message X to B, then B might receive it*}
   16.25 +| Reception: --{*If A sends a message X to B, then B might receive it*}
   16.26  	     "[| evsr \<in> set_pur;  Says A B X \<in> set evsr |]
   16.27  	      ==> Gets B X  # evsr \<in> set_pur"
   16.28  
   16.29 -  Start: 
   16.30 +| Start: 
   16.31        --{*Added start event which is out-of-band for SET: the Cardholder and
   16.32  	  the merchant agree on the amounts and uses @{text LID_M} as an
   16.33            identifier.
   16.34 @@ -91,7 +90,7 @@
   16.35         # Notes M {|Number LID_M, Agent P, Transaction|}
   16.36         # evsStart \<in> set_pur"
   16.37  
   16.38 -  PInitReq:
   16.39 +| PInitReq:
   16.40       --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
   16.41     "[|evsPIReq \<in> set_pur;
   16.42        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   16.43 @@ -100,7 +99,7 @@
   16.44        Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
   16.45      ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
   16.46  
   16.47 -  PInitRes:
   16.48 +| PInitRes:
   16.49       --{*Merchant replies with his own label XID and the encryption
   16.50  	 key certificate of his chosen Payment Gateway. Page 74 of Formal
   16.51           Protocol Desc. We use @{text LID_M} to identify Cardholder*}
   16.52 @@ -118,7 +117,7 @@
   16.53  			 cert P (pubEK P) onlyEnc (priSK RCA)|})
   16.54            # evsPIRes \<in> set_pur"
   16.55  
   16.56 -  PReqUns:
   16.57 +| PReqUns:
   16.58        --{*UNSIGNED Purchase request (CardSecret = 0).
   16.59  	Page 79 of Formal Protocol Desc.
   16.60  	Merchant never sees the amount in clear. This holds of the real
   16.61 @@ -126,7 +125,8 @@
   16.62  	Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
   16.63  	the CardSecret is 0 and because AuthReq treated the unsigned case
   16.64  	very differently from the signed one anyway.*}
   16.65 -   "[|evsPReqU \<in> set_pur;
   16.66 +   "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
   16.67 +    [|evsPReqU \<in> set_pur;
   16.68        C = Cardholder k; CardSecret k = 0;
   16.69        Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;
   16.70        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   16.71 @@ -146,14 +146,17 @@
   16.72  	  # Notes C {|Key KC1, Agent M|}
   16.73  	  # evsPReqU \<in> set_pur"
   16.74  
   16.75 -  PReqS:
   16.76 +| PReqS:
   16.77        --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
   16.78            We could specify the equation
   16.79  	  @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
   16.80  	  Formal Desc. gives PIHead the same format in the unsigned case.
   16.81  	  However, there's little point, as P treats the signed and 
   16.82            unsigned cases differently.*}
   16.83 -   "[|evsPReqS \<in> set_pur;
   16.84 +   "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData
   16.85 +      OIDualSigned OrderDesc P PANData PIData PIDualSigned
   16.86 +      PIHead PurchAmt Transaction XID evsPReqS k.
   16.87 +    [|evsPReqS \<in> set_pur;
   16.88        C = Cardholder k;
   16.89        CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;
   16.90        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   16.91 @@ -179,7 +182,7 @@
   16.92  
   16.93    --{*Authorization Request.  Page 92 of Formal Protocol Desc.
   16.94      Sent in response to Purchase Request.*}
   16.95 -  AuthReq:
   16.96 +| AuthReq:
   16.97     "[| evsAReq \<in> set_pur;
   16.98         Key KM \<notin> used evsAReq;  KM \<in> symKeys;
   16.99         Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
  16.100 @@ -208,7 +211,7 @@
  16.101      full protocol is [CapToken], [AcqCardMsg], [AuthToken]:
  16.102      optional items for split shipments, recurring payments, etc.*}
  16.103  
  16.104 -  AuthResUns:
  16.105 +| AuthResUns:
  16.106      --{*Authorization Response, UNSIGNED*}
  16.107     "[| evsAResU \<in> set_pur;
  16.108         C = Cardholder k; M = Merchant i;
  16.109 @@ -225,7 +228,7 @@
  16.110  	      authCode)
  16.111         # evsAResU \<in> set_pur"
  16.112  
  16.113 -  AuthResS:
  16.114 +| AuthResS:
  16.115      --{*Authorization Response, SIGNED*}
  16.116     "[| evsAResS \<in> set_pur;
  16.117         C = Cardholder k;
  16.118 @@ -247,7 +250,7 @@
  16.119  	      authCode)
  16.120         # evsAResS \<in> set_pur"
  16.121  
  16.122 -  PRes:
  16.123 +| PRes:
  16.124      --{*Purchase response.*}
  16.125     "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;
  16.126         Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};