--- a/src/HOL/IMP/Sec_Type_Expr.thy Tue Dec 04 10:02:51 2012 +0100
+++ b/src/HOL/IMP/Sec_Type_Expr.thy Tue Dec 04 12:19:19 2012 +0100
@@ -7,23 +7,46 @@
type_synonym level = nat
+class sec =
+fixes sec :: "'a \<Rightarrow> nat"
+
text{* The security/confidentiality level of each variable is globally fixed
for simplicity. For the sake of examples --- the general theory does not rely
on it! --- a variable of length @{text n} has security level @{text n}: *}
-definition sec :: "vname \<Rightarrow> level" where
- "sec n = size n"
+instantiation list :: (type)sec
+begin
+
+definition "sec(x :: 'a list) = length x"
+
+instance ..
+
+end
+
+instantiation aexp :: sec
+begin
fun sec_aexp :: "aexp \<Rightarrow> level" where
-"sec_aexp (N n) = 0" |
-"sec_aexp (V x) = sec x" |
-"sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
+"sec (N n) = 0" |
+"sec (V x) = sec x" |
+"sec (Plus a\<^isub>1 a\<^isub>2) = max (sec a\<^isub>1) (sec a\<^isub>2)"
+
+instance ..
+
+end
+
+instantiation bexp :: sec
+begin
fun sec_bexp :: "bexp \<Rightarrow> level" where
-"sec_bexp (Bc v) = 0" |
-"sec_bexp (Not b) = sec_bexp b" |
-"sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
-"sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
+"sec (Bc v) = 0" |
+"sec (Not b) = sec b" |
+"sec (And b\<^isub>1 b\<^isub>2) = max (sec b\<^isub>1) (sec b\<^isub>2)" |
+"sec (Less a\<^isub>1 a\<^isub>2) = max (sec a\<^isub>1) (sec a\<^isub>2)"
+
+instance ..
+
+end
abbreviation eq_le :: "state \<Rightarrow> state \<Rightarrow> level \<Rightarrow> bool"
@@ -35,11 +58,11 @@
"s = s' (< l) == (\<forall> x. sec x < l \<longrightarrow> s x = s' x)"
lemma aval_eq_if_eq_le:
- "\<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"
+ "\<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"
by (induct a) auto
lemma bval_eq_if_eq_le:
- "\<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"
+ "\<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"
by (induct b) (auto simp add: aval_eq_if_eq_le)
end
--- a/src/HOL/IMP/Sec_Typing.thy Tue Dec 04 10:02:51 2012 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy Tue Dec 04 12:19:19 2012 +0100
@@ -9,13 +9,13 @@
Skip:
"l \<turnstile> SKIP" |
Assign:
- "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
+ "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
Seq:
"\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
If:
- "\<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" |
+ "\<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" |
While:
- "max (sec_bexp b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
+ "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
code_pred (expected_modes: i => i => bool) sec_type .
@@ -47,19 +47,19 @@
case Seq thus ?case by auto
next
case (IfTrue b s c1)
- hence "max (sec_bexp b) l \<turnstile> c1" by auto
+ hence "max (sec b) l \<turnstile> c1" by auto
hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
thus ?case using IfTrue.IH by metis
next
case (IfFalse b s c2)
- hence "max (sec_bexp b) l \<turnstile> c2" by auto
+ hence "max (sec b) l \<turnstile> c2" by auto
hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
thus ?case using IfFalse.IH by metis
next
case WhileFalse thus ?case by auto
next
case (WhileTrue b s1 c)
- hence "max (sec_bexp b) l \<turnstile> c" by auto
+ hence "max (sec b) l \<turnstile> c" by auto
hence "l \<turnstile> c" by (metis le_maxI2 anti_mono)
thus ?case using WhileTrue by metis
qed
@@ -73,11 +73,11 @@
next
case (Assign x a s)
have [simp]: "t' = t(x := aval a t)" using Assign by auto
- have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
+ have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto
show ?case
proof auto
assume "sec x \<le> l"
- with `sec x >= sec_aexp a` have "sec_aexp a \<le> l" by arith
+ with `sec x >= sec a` have "sec a \<le> l" by arith
thus "aval a s = aval a t"
by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
next
@@ -88,86 +88,86 @@
case Seq thus ?case by blast
next
case (IfTrue b s c1 s' c2)
- have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
+ have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems(2) by auto
show ?case
proof cases
- assume "sec_bexp b \<le> l"
- hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+ assume "sec b \<le> l"
+ hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
- with IfTrue.IH IfTrue.prems(1,3) `sec_bexp b \<turnstile> c1` anti_mono
+ with IfTrue.IH IfTrue.prems(1,3) `sec b \<turnstile> c1` anti_mono
show ?thesis by auto
next
- assume "\<not> sec_bexp b \<le> l"
- have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
- by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
- from confinement[OF IfTrue.hyps(2) `sec_bexp b \<turnstile> c1`] `\<not> sec_bexp b \<le> l`
+ assume "\<not> sec b \<le> l"
+ have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
+ by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
+ from confinement[OF IfTrue.hyps(2) `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
have "s = s' (\<le> l)" by auto
moreover
- from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
+ from confinement[OF IfTrue.prems(1) 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
qed
next
case (IfFalse b s c2 s' c1)
- have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems(2) by auto
+ have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems(2) by auto
show ?case
proof cases
- assume "sec_bexp b \<le> l"
- hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+ assume "sec b \<le> l"
+ hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
- with IfFalse.IH IfFalse.prems(1,3) `sec_bexp b \<turnstile> c2` anti_mono
+ with IfFalse.IH IfFalse.prems(1,3) `sec b \<turnstile> c2` anti_mono
show ?thesis by auto
next
- assume "\<not> sec_bexp b \<le> l"
- have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
- by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
- from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
+ assume "\<not> sec b \<le> l"
+ have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
+ by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
+ from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
have "s = s' (\<le> l)" by auto
moreover
- from confinement[OF IfFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
+ from confinement[OF IfFalse.prems(1) 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
qed
next
case (WhileFalse b s c)
- have "sec_bexp b \<turnstile> c" using WhileFalse.prems(2) by auto
+ have "sec b \<turnstile> c" using WhileFalse.prems(2) by auto
show ?case
proof cases
- assume "sec_bexp b \<le> l"
- hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+ assume "sec b \<le> l"
+ hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
with WhileFalse.prems(1,3) show ?thesis by auto
next
- assume "\<not> sec_bexp b \<le> l"
- have 1: "sec_bexp b \<turnstile> WHILE b DO c"
- by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
- from confinement[OF WhileFalse.prems(1) 1] `\<not> sec_bexp b \<le> l`
+ assume "\<not> sec b \<le> l"
+ have 1: "sec b \<turnstile> WHILE b DO c"
+ by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
+ from confinement[OF WhileFalse.prems(1) 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
qed
next
case (WhileTrue b s1 c s2 s3 t1 t3)
let ?w = "WHILE b DO c"
- have "sec_bexp b \<turnstile> c" using WhileTrue.prems(2) by auto
+ have "sec b \<turnstile> c" using WhileTrue.prems(2) by auto
show ?case
proof cases
- assume "sec_bexp b \<le> l"
- hence "s1 = t1 (\<le> sec_bexp b)" using `s1 = t1 (\<le> l)` by auto
+ assume "sec b \<le> l"
+ hence "s1 = t1 (\<le> sec b)" using `s1 = t1 (\<le> l)` by auto
hence "bval b t1"
using `bval b s1` by(simp add: bval_eq_if_eq_le)
then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
using `(?w,t1) \<Rightarrow> t3` by auto
from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
- WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec_bexp b \<turnstile> c`]
+ WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec b \<turnstile> c`]
`s1 = t1 (\<le> l)`]]
show ?thesis by simp
next
- assume "\<not> sec_bexp b \<le> l"
- have 1: "sec_bexp b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c`)
- from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec_bexp b \<le> l`
+ assume "\<not> sec b \<le> l"
+ have 1: "sec b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
+ from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec b \<le> l`
have "s1 = s3 (\<le> l)" by auto
moreover
- from confinement[OF WhileTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`
+ from confinement[OF WhileTrue.prems(1) 1] `\<not> sec b \<le> l`
have "t1 = t3 (\<le> l)" by auto
ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
qed
@@ -185,13 +185,13 @@
Skip':
"l \<turnstile>' SKIP" |
Assign':
- "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
+ "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
Seq':
"\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
If':
- "\<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" |
+ "\<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" |
While':
- "\<lbrakk> sec_bexp b \<le> l; l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
+ "\<lbrakk> sec b \<le> l; l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
anti_mono':
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
@@ -219,14 +219,14 @@
Skip2:
"\<turnstile> SKIP : l" |
Assign2:
- "sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
+ "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
Seq2:
"\<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 " |
If2:
- "\<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>
+ "\<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>
\<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
While2:
- "\<lbrakk> sec_bexp b \<le> l; \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
+ "\<lbrakk> sec b \<le> l; \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
--- a/src/HOL/IMP/Sec_TypingT.thy Tue Dec 04 10:02:51 2012 +0100
+++ b/src/HOL/IMP/Sec_TypingT.thy Tue Dec 04 12:19:19 2012 +0100
@@ -7,14 +7,14 @@
Skip:
"l \<turnstile> SKIP" |
Assign:
- "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
+ "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
Seq:
"l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
If:
- "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1; max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
+ "\<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" |
While:
- "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
+ "sec b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
code_pred (expected_modes: i => i => bool) sec_type .
@@ -40,12 +40,12 @@
case Seq thus ?case by auto
next
case (IfTrue b s c1)
- hence "max (sec_bexp b) l \<turnstile> c1" by auto
+ hence "max (sec b) l \<turnstile> c1" by auto
hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
thus ?case using IfTrue.IH by metis
next
case (IfFalse b s c2)
- hence "max (sec_bexp b) l \<turnstile> c2" by auto
+ hence "max (sec b) l \<turnstile> c2" by auto
hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
thus ?case using IfFalse.IH by metis
next
@@ -71,13 +71,13 @@
case Skip thus ?case by auto
next
case (Assign x a s)
- have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
+ have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto
have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto
moreover
have "s(x := aval a s) = t(x := aval a t) (\<le> l)"
proof auto
assume "sec x \<le> l"
- with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith
+ with `sec x \<ge> sec a` have "sec a \<le> l" by arith
thus "aval a s = aval a t"
by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
next
@@ -89,68 +89,68 @@
case Seq thus ?case by blast
next
case (IfTrue b s c1 s' c2)
- have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
+ have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems by auto
obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
- using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast
+ using IfTrue(3)[OF anti_mono[OF `sec b \<turnstile> c1`] IfTrue.prems(2)] by blast
show ?case
proof cases
- assume "sec_bexp b \<le> l"
- hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+ assume "sec b \<le> l"
+ hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
thus ?thesis by (metis t' big_step.IfTrue)
next
- assume "\<not> sec_bexp b \<le> l"
- hence 0: "sec_bexp b \<noteq> 0" by arith
- have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
- by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
- from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
+ assume "\<not> sec b \<le> l"
+ hence 0: "sec b \<noteq> 0" by arith
+ have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
+ by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
+ from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec b \<le> l`
have "s = s' (\<le> l)" by auto
moreover
from termi_if_non0[OF 1 0, of t] obtain t' where
"(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
moreover
- from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
+ from confinement[OF this 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
ultimately
show ?case using `s = t (\<le> l)` by auto
qed
next
case (IfFalse b s c2 s' c1)
- have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto
+ have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems by auto
obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
- using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast
+ using IfFalse(3)[OF anti_mono[OF `sec b \<turnstile> c2`] IfFalse.prems(2)] by blast
show ?case
proof cases
- assume "sec_bexp b \<le> l"
- hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+ assume "sec b \<le> l"
+ hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
thus ?thesis by (metis t' big_step.IfFalse)
next
- assume "\<not> sec_bexp b \<le> l"
- hence 0: "sec_bexp b \<noteq> 0" by arith
- have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
- by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
- from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
+ assume "\<not> sec b \<le> l"
+ hence 0: "sec b \<noteq> 0" by arith
+ have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
+ by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
+ from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
have "s = s' (\<le> l)" by auto
moreover
from termi_if_non0[OF 1 0, of t] obtain t' where
"(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
moreover
- from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
+ from confinement[OF this 1] `\<not> sec b \<le> l`
have "t = t' (\<le> l)" by auto
ultimately
show ?case using `s = t (\<le> l)` by auto
qed
next
case (WhileFalse b s c)
- hence [simp]: "sec_bexp b = 0" by auto
- have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
+ hence [simp]: "sec b = 0" by auto
+ have "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl)
with WhileFalse.prems(2) show ?case by auto
next
case (WhileTrue b s c s'' s')
let ?w = "WHILE b DO c"
- from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
+ from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto
have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
@@ -174,13 +174,13 @@
Skip':
"l \<turnstile>' SKIP" |
Assign':
- "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
+ "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
Seq':
"l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
If':
- "\<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" |
+ "\<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" |
While':
- "\<lbrakk> sec_bexp b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" |
+ "\<lbrakk> sec b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" |
anti_mono':
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"