tuned defs of sec_xyz
authornipkow
Tue Dec 04 12:19:19 2012 +0100 (2012-12-04)
changeset 50342e77b0dbcae5b
parent 50340 72519bf5f135
child 50343 40d5ec9149d5
tuned defs of sec_xyz
src/HOL/IMP/Sec_Type_Expr.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
     1.1 --- a/src/HOL/IMP/Sec_Type_Expr.thy	Tue Dec 04 10:02:51 2012 +0100
     1.2 +++ b/src/HOL/IMP/Sec_Type_Expr.thy	Tue Dec 04 12:19:19 2012 +0100
     1.3 @@ -7,23 +7,46 @@
     1.4  
     1.5  type_synonym level = nat
     1.6  
     1.7 +class sec =
     1.8 +fixes sec :: "'a \<Rightarrow> nat"
     1.9 +
    1.10  text{* The security/confidentiality level of each variable is globally fixed
    1.11  for simplicity. For the sake of examples --- the general theory does not rely
    1.12  on it! --- a variable of length @{text n} has security level @{text n}: *}
    1.13  
    1.14 -definition sec :: "vname \<Rightarrow> level" where 
    1.15 -  "sec n = size n"
    1.16 +instantiation list :: (type)sec
    1.17 +begin
    1.18 +
    1.19 +definition "sec(x :: 'a list) = length x"
    1.20 +
    1.21 +instance ..
    1.22 +
    1.23 +end
    1.24 +
    1.25 +instantiation aexp :: sec
    1.26 +begin
    1.27  
    1.28  fun sec_aexp :: "aexp \<Rightarrow> level" where
    1.29 -"sec_aexp (N n) = 0" |
    1.30 -"sec_aexp (V x) = sec x" |
    1.31 -"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
    1.32 +"sec (N n) = 0" |
    1.33 +"sec (V x) = sec x" |
    1.34 +"sec (Plus a\<^isub>1 a\<^isub>2) = max (sec a\<^isub>1) (sec a\<^isub>2)"
    1.35 +
    1.36 +instance ..
    1.37 +
    1.38 +end
    1.39 +
    1.40 +instantiation bexp :: sec
    1.41 +begin
    1.42  
    1.43  fun sec_bexp :: "bexp \<Rightarrow> level" where
    1.44 -"sec_bexp (Bc v) = 0" |
    1.45 -"sec_bexp (Not b) = sec_bexp b" |
    1.46 -"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
    1.47 -"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
    1.48 +"sec (Bc v) = 0" |
    1.49 +"sec (Not b) = sec b" |
    1.50 +"sec (And b\<^isub>1 b\<^isub>2) = max (sec b\<^isub>1) (sec b\<^isub>2)" |
    1.51 +"sec (Less a\<^isub>1 a\<^isub>2) = max (sec a\<^isub>1) (sec a\<^isub>2)"
    1.52 +
    1.53 +instance ..
    1.54 +
    1.55 +end
    1.56  
    1.57  
    1.58  abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
    1.59 @@ -35,11 +58,11 @@
    1.60  "s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
    1.61  
    1.62  lemma aval_eq_if_eq_le:
    1.63 -  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec_aexp a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
    1.64 +  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec a \<le> l \<rbrakk> \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
    1.65  by (induct a) auto
    1.66  
    1.67  lemma bval_eq_if_eq_le:
    1.68 -  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec_bexp b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
    1.69 +  "\<lbrakk> s\<^isub>1 = s\<^isub>2 (\<le> l);  sec b \<le> l \<rbrakk> \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
    1.70  by (induct b) (auto simp add: aval_eq_if_eq_le)
    1.71  
    1.72  end
     2.1 --- a/src/HOL/IMP/Sec_Typing.thy	Tue Dec 04 10:02:51 2012 +0100
     2.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Tue Dec 04 12:19:19 2012 +0100
     2.3 @@ -9,13 +9,13 @@
     2.4  Skip:
     2.5    "l \<turnstile> SKIP" |
     2.6  Assign:
     2.7 -  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
     2.8 +  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
     2.9  Seq:
    2.10    "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
    2.11  If:
    2.12 -  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
    2.13 +  "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
    2.14  While:
    2.15 -  "max (sec_bexp b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
    2.16 +  "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
    2.17  
    2.18  code_pred (expected_modes: i => i => bool) sec_type .
    2.19  
    2.20 @@ -47,19 +47,19 @@
    2.21    case Seq thus ?case by auto
    2.22  next
    2.23    case (IfTrue b s c1)
    2.24 -  hence "max (sec_bexp b) l \<turnstile> c1" by auto
    2.25 +  hence "max (sec b) l \<turnstile> c1" by auto
    2.26    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
    2.27    thus ?case using IfTrue.IH by metis
    2.28  next
    2.29    case (IfFalse b s c2)
    2.30 -  hence "max (sec_bexp b) l \<turnstile> c2" by auto
    2.31 +  hence "max (sec b) l \<turnstile> c2" by auto
    2.32    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
    2.33    thus ?case using IfFalse.IH by metis
    2.34  next
    2.35    case WhileFalse thus ?case by auto
    2.36  next
    2.37    case (WhileTrue b s1 c)
    2.38 -  hence "max (sec_bexp b) l \<turnstile> c" by auto
    2.39 +  hence "max (sec b) l \<turnstile> c" by auto
    2.40    hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
    2.41    thus ?case using WhileTrue by metis
    2.42  qed
    2.43 @@ -73,11 +73,11 @@
    2.44  next
    2.45    case (Assign x a s)
    2.46    have [simp]: "t' = t(x := aval a t)" using Assign by auto
    2.47 -  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
    2.48 +  have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto
    2.49    show ?case
    2.50    proof auto
    2.51      assume "sec x \<le> l"
    2.52 -    with `sec x >= sec_aexp a` have "sec_aexp a \<le> l" by arith
    2.53 +    with `sec x >= sec a` have "sec a \<le> l" by arith
    2.54      thus "aval a s = aval a t"
    2.55        by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
    2.56    next
    2.57 @@ -88,86 +88,86 @@
    2.58    case Seq thus ?case by blast
    2.59  next
    2.60    case (IfTrue b s c1 s' c2)
    2.61 -  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
    2.62 +  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems(2) by auto
    2.63    show ?case
    2.64    proof cases
    2.65 -    assume "sec_bexp b \<le> l"
    2.66 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
    2.67 +    assume "sec b \<le> l"
    2.68 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
    2.69      hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
    2.70 -    with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1`  anti_mono
    2.71 +    with IfTrue.IH IfTrue.prems(1,3) `sec b \<turnstile> c1`  anti_mono
    2.72      show ?thesis by auto
    2.73    next
    2.74 -    assume "\<not> sec_bexp b \<le> l"
    2.75 -    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
    2.76 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
    2.77 -    from confinement[OF IfTrue.hyps(2) `sec_bexp b \<turnstile> c1`] `\<not> sec_bexp b \<le> l`
    2.78 +    assume "\<not> sec b \<le> l"
    2.79 +    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
    2.80 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
    2.81 +    from confinement[OF IfTrue.hyps(2) `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
    2.82      have "s = s' (\<le> l)" by auto
    2.83      moreover
    2.84 -    from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
    2.85 +    from confinement[OF IfTrue.prems(1) 1] `\<not> sec b \<le> l`
    2.86      have "t = t' (\<le> l)" by auto
    2.87      ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
    2.88    qed
    2.89  next
    2.90    case (IfFalse b s c2 s' c1)
    2.91 -  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems(2) by auto
    2.92 +  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems(2) by auto
    2.93    show ?case
    2.94    proof cases
    2.95 -    assume "sec_bexp b \<le> l"
    2.96 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
    2.97 +    assume "sec b \<le> l"
    2.98 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
    2.99      hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
   2.100 -    with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
   2.101 +    with IfFalse.IH IfFalse.prems(1,3) `sec b \<turnstile> c2` anti_mono
   2.102      show ?thesis by auto
   2.103    next
   2.104 -    assume "\<not> sec_bexp b \<le> l"
   2.105 -    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
   2.106 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
   2.107 -    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
   2.108 +    assume "\<not> sec b \<le> l"
   2.109 +    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
   2.110 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
   2.111 +    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
   2.112      have "s = s' (\<le> l)" by auto
   2.113      moreover
   2.114 -    from confinement[OF IfFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
   2.115 +    from confinement[OF IfFalse.prems(1) 1] `\<not> sec b \<le> l`
   2.116      have "t = t' (\<le> l)" by auto
   2.117      ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
   2.118    qed
   2.119  next
   2.120    case (WhileFalse b s c)
   2.121 -  have "sec_bexp b \<turnstile> c" using WhileFalse.prems(2) by auto
   2.122 +  have "sec b \<turnstile> c" using WhileFalse.prems(2) by auto
   2.123    show ?case
   2.124    proof cases
   2.125 -    assume "sec_bexp b \<le> l"
   2.126 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   2.127 +    assume "sec b \<le> l"
   2.128 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
   2.129      hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
   2.130      with WhileFalse.prems(1,3) show ?thesis by auto
   2.131    next
   2.132 -    assume "\<not> sec_bexp b \<le> l"
   2.133 -    have 1: "sec_bexp b \<turnstile> WHILE b DO c"
   2.134 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
   2.135 -    from confinement[OF WhileFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
   2.136 +    assume "\<not> sec b \<le> l"
   2.137 +    have 1: "sec b \<turnstile> WHILE b DO c"
   2.138 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
   2.139 +    from confinement[OF WhileFalse.prems(1) 1] `\<not> sec b \<le> l`
   2.140      have "t = t' (\<le> l)" by auto
   2.141      thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
   2.142    qed
   2.143  next
   2.144    case (WhileTrue b s1 c s2 s3 t1 t3)
   2.145    let ?w = "WHILE b DO c"
   2.146 -  have "sec_bexp b \<turnstile> c" using WhileTrue.prems(2) by auto
   2.147 +  have "sec b \<turnstile> c" using WhileTrue.prems(2) by auto
   2.148    show ?case
   2.149    proof cases
   2.150 -    assume "sec_bexp b \<le> l"
   2.151 -    hence "s1 = t1 (\<le> sec_bexp b)" using `s1 = t1 (\<le> l)` by auto
   2.152 +    assume "sec b \<le> l"
   2.153 +    hence "s1 = t1 (\<le> sec b)" using `s1 = t1 (\<le> l)` by auto
   2.154      hence "bval b t1"
   2.155        using `bval b s1` by(simp add: bval_eq_if_eq_le)
   2.156      then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
   2.157        using `(?w,t1) \<Rightarrow> t3` by auto
   2.158      from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
   2.159 -      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
   2.160 +      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec b \<turnstile> c`]
   2.161          `s1 = t1 (\<le> l)`]]
   2.162      show ?thesis by simp
   2.163    next
   2.164 -    assume "\<not> sec_bexp b \<le> l"
   2.165 -    have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
   2.166 -    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
   2.167 +    assume "\<not> sec b \<le> l"
   2.168 +    have 1: "sec b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
   2.169 +    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec b \<le> l`
   2.170      have "s1 = s3 (\<le> l)" by auto
   2.171      moreover
   2.172 -    from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
   2.173 +    from confinement[OF WhileTrue.prems(1) 1] `\<not> sec b \<le> l`
   2.174      have "t1 = t3 (\<le> l)" by auto
   2.175      ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
   2.176    qed
   2.177 @@ -185,13 +185,13 @@
   2.178  Skip':
   2.179    "l \<turnstile>' SKIP" |
   2.180  Assign':
   2.181 -  "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
   2.182 +  "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
   2.183  Seq':
   2.184    "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
   2.185  If':
   2.186 -  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
   2.187 +  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
   2.188  While':
   2.189 -  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
   2.190 +  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
   2.191  anti_mono':
   2.192    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   2.193  
   2.194 @@ -219,14 +219,14 @@
   2.195  Skip2:
   2.196    "\<turnstile> SKIP : l" |
   2.197  Assign2:
   2.198 -  "sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
   2.199 +  "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
   2.200  Seq2:
   2.201    "\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " |
   2.202  If2:
   2.203 -  "\<lbrakk> sec_bexp b \<le> min l\<^isub>1 l\<^isub>2;  \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
   2.204 +  "\<lbrakk> sec b \<le> min l\<^isub>1 l\<^isub>2;  \<turnstile> c\<^isub>1 : l\<^isub>1;  \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
   2.205    \<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
   2.206  While2:
   2.207 -  "\<lbrakk> sec_bexp b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
   2.208 +  "\<lbrakk> sec b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
   2.209  
   2.210  
   2.211  lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
     3.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Tue Dec 04 10:02:51 2012 +0100
     3.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Tue Dec 04 12:19:19 2012 +0100
     3.3 @@ -7,14 +7,14 @@
     3.4  Skip:
     3.5    "l \<turnstile> SKIP"  |
     3.6  Assign:
     3.7 -  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
     3.8 +  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
     3.9  Seq:
    3.10    "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
    3.11  If:
    3.12 -  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
    3.13 +  "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk>
    3.14     \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
    3.15  While:
    3.16 -  "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
    3.17 +  "sec b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
    3.18  
    3.19  code_pred (expected_modes: i => i => bool) sec_type .
    3.20  
    3.21 @@ -40,12 +40,12 @@
    3.22    case Seq thus ?case by auto
    3.23  next
    3.24    case (IfTrue b s c1)
    3.25 -  hence "max (sec_bexp b) l \<turnstile> c1" by auto
    3.26 +  hence "max (sec b) l \<turnstile> c1" by auto
    3.27    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
    3.28    thus ?case using IfTrue.IH by metis
    3.29  next
    3.30    case (IfFalse b s c2)
    3.31 -  hence "max (sec_bexp b) l \<turnstile> c2" by auto
    3.32 +  hence "max (sec b) l \<turnstile> c2" by auto
    3.33    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
    3.34    thus ?case using IfFalse.IH by metis
    3.35  next
    3.36 @@ -71,13 +71,13 @@
    3.37    case Skip thus ?case by auto
    3.38  next
    3.39    case (Assign x a s)
    3.40 -  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
    3.41 +  have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto
    3.42    have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto
    3.43    moreover
    3.44    have "s(x := aval a s) = t(x := aval a t) (\<le> l)"
    3.45    proof auto
    3.46      assume "sec x \<le> l"
    3.47 -    with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith
    3.48 +    with `sec x \<ge> sec a` have "sec a \<le> l" by arith
    3.49      thus "aval a s = aval a t"
    3.50        by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
    3.51    next
    3.52 @@ -89,68 +89,68 @@
    3.53    case Seq thus ?case by blast
    3.54  next
    3.55    case (IfTrue b s c1 s' c2)
    3.56 -  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
    3.57 +  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems by auto
    3.58    obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
    3.59 -    using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast
    3.60 +    using IfTrue(3)[OF anti_mono[OF `sec b \<turnstile> c1`] IfTrue.prems(2)] by blast
    3.61    show ?case
    3.62    proof cases
    3.63 -    assume "sec_bexp b \<le> l"
    3.64 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
    3.65 +    assume "sec b \<le> l"
    3.66 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
    3.67      hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
    3.68      thus ?thesis by (metis t' big_step.IfTrue)
    3.69    next
    3.70 -    assume "\<not> sec_bexp b \<le> l"
    3.71 -    hence 0: "sec_bexp b \<noteq> 0" by arith
    3.72 -    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
    3.73 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
    3.74 -    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
    3.75 +    assume "\<not> sec b \<le> l"
    3.76 +    hence 0: "sec b \<noteq> 0" by arith
    3.77 +    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
    3.78 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
    3.79 +    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec b \<le> l`
    3.80      have "s = s' (\<le> l)" by auto
    3.81      moreover
    3.82      from termi_if_non0[OF 1 0, of t] obtain t' where
    3.83        "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
    3.84      moreover
    3.85 -    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
    3.86 +    from confinement[OF this 1] `\<not> sec b \<le> l`
    3.87      have "t = t' (\<le> l)" by auto
    3.88      ultimately
    3.89      show ?case using `s = t (\<le> l)` by auto
    3.90    qed
    3.91  next
    3.92    case (IfFalse b s c2 s' c1)
    3.93 -  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto
    3.94 +  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems by auto
    3.95    obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
    3.96 -    using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast
    3.97 +    using IfFalse(3)[OF anti_mono[OF `sec b \<turnstile> c2`] IfFalse.prems(2)] by blast
    3.98    show ?case
    3.99    proof cases
   3.100 -    assume "sec_bexp b \<le> l"
   3.101 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   3.102 +    assume "sec b \<le> l"
   3.103 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
   3.104      hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
   3.105      thus ?thesis by (metis t' big_step.IfFalse)
   3.106    next
   3.107 -    assume "\<not> sec_bexp b \<le> l"
   3.108 -    hence 0: "sec_bexp b \<noteq> 0" by arith
   3.109 -    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
   3.110 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
   3.111 -    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
   3.112 +    assume "\<not> sec b \<le> l"
   3.113 +    hence 0: "sec b \<noteq> 0" by arith
   3.114 +    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
   3.115 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
   3.116 +    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
   3.117      have "s = s' (\<le> l)" by auto
   3.118      moreover
   3.119      from termi_if_non0[OF 1 0, of t] obtain t' where
   3.120        "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
   3.121      moreover
   3.122 -    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
   3.123 +    from confinement[OF this 1] `\<not> sec b \<le> l`
   3.124      have "t = t' (\<le> l)" by auto
   3.125      ultimately
   3.126      show ?case using `s = t (\<le> l)` by auto
   3.127    qed
   3.128  next
   3.129    case (WhileFalse b s c)
   3.130 -  hence [simp]: "sec_bexp b = 0" by auto
   3.131 -  have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   3.132 +  hence [simp]: "sec b = 0" by auto
   3.133 +  have "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
   3.134    hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl)
   3.135    with WhileFalse.prems(2) show ?case by auto
   3.136  next
   3.137    case (WhileTrue b s c s'' s')
   3.138    let ?w = "WHILE b DO c"
   3.139 -  from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
   3.140 +  from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto
   3.141    have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
   3.142    from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
   3.143    obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
   3.144 @@ -174,13 +174,13 @@
   3.145  Skip':
   3.146    "l \<turnstile>' SKIP"  |
   3.147  Assign':
   3.148 -  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
   3.149 +  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
   3.150  Seq':
   3.151    "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
   3.152  If':
   3.153 -  "\<lbrakk> sec_bexp b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
   3.154 +  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
   3.155  While':
   3.156 -  "\<lbrakk> sec_bexp b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
   3.157 +  "\<lbrakk> sec b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
   3.158  anti_mono':
   3.159    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   3.160