src/HOL/IMP/Sec_TypingT.thy
changeset 50342 e77b0dbcae5b
parent 47818 151d137f1095
child 51456 a6e3a5ec9847
     1.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Tue Dec 04 10:02:51 2012 +0100
     1.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Tue Dec 04 12:19:19 2012 +0100
     1.3 @@ -7,14 +7,14 @@
     1.4  Skip:
     1.5    "l \<turnstile> SKIP"  |
     1.6  Assign:
     1.7 -  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
     1.8 +  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
     1.9  Seq:
    1.10    "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
    1.11  If:
    1.12 -  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
    1.13 +  "\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1;  max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk>
    1.14     \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
    1.15  While:
    1.16 -  "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
    1.17 +  "sec b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
    1.18  
    1.19  code_pred (expected_modes: i => i => bool) sec_type .
    1.20  
    1.21 @@ -40,12 +40,12 @@
    1.22    case Seq thus ?case by auto
    1.23  next
    1.24    case (IfTrue b s c1)
    1.25 -  hence "max (sec_bexp b) l \<turnstile> c1" by auto
    1.26 +  hence "max (sec b) l \<turnstile> c1" by auto
    1.27    hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
    1.28    thus ?case using IfTrue.IH by metis
    1.29  next
    1.30    case (IfFalse b s c2)
    1.31 -  hence "max (sec_bexp b) l \<turnstile> c2" by auto
    1.32 +  hence "max (sec b) l \<turnstile> c2" by auto
    1.33    hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
    1.34    thus ?case using IfFalse.IH by metis
    1.35  next
    1.36 @@ -71,13 +71,13 @@
    1.37    case Skip thus ?case by auto
    1.38  next
    1.39    case (Assign x a s)
    1.40 -  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
    1.41 +  have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto
    1.42    have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto
    1.43    moreover
    1.44    have "s(x := aval a s) = t(x := aval a t) (\<le> l)"
    1.45    proof auto
    1.46      assume "sec x \<le> l"
    1.47 -    with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith
    1.48 +    with `sec x \<ge> sec a` have "sec a \<le> l" by arith
    1.49      thus "aval a s = aval a t"
    1.50        by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
    1.51    next
    1.52 @@ -89,68 +89,68 @@
    1.53    case Seq thus ?case by blast
    1.54  next
    1.55    case (IfTrue b s c1 s' c2)
    1.56 -  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
    1.57 +  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfTrue.prems by auto
    1.58    obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
    1.59 -    using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast
    1.60 +    using IfTrue(3)[OF anti_mono[OF `sec b \<turnstile> c1`] IfTrue.prems(2)] by blast
    1.61    show ?case
    1.62    proof cases
    1.63 -    assume "sec_bexp b \<le> l"
    1.64 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
    1.65 +    assume "sec b \<le> l"
    1.66 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
    1.67      hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
    1.68      thus ?thesis by (metis t' big_step.IfTrue)
    1.69    next
    1.70 -    assume "\<not> sec_bexp b \<le> l"
    1.71 -    hence 0: "sec_bexp b \<noteq> 0" by arith
    1.72 -    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
    1.73 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
    1.74 -    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
    1.75 +    assume "\<not> sec b \<le> l"
    1.76 +    hence 0: "sec b \<noteq> 0" by arith
    1.77 +    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
    1.78 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
    1.79 +    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec b \<le> l`
    1.80      have "s = s' (\<le> l)" by auto
    1.81      moreover
    1.82      from termi_if_non0[OF 1 0, of t] obtain t' where
    1.83        "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
    1.84      moreover
    1.85 -    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
    1.86 +    from confinement[OF this 1] `\<not> sec b \<le> l`
    1.87      have "t = t' (\<le> l)" by auto
    1.88      ultimately
    1.89      show ?case using `s = t (\<le> l)` by auto
    1.90    qed
    1.91  next
    1.92    case (IfFalse b s c2 s' c1)
    1.93 -  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto
    1.94 +  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using IfFalse.prems by auto
    1.95    obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
    1.96 -    using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast
    1.97 +    using IfFalse(3)[OF anti_mono[OF `sec b \<turnstile> c2`] IfFalse.prems(2)] by blast
    1.98    show ?case
    1.99    proof cases
   1.100 -    assume "sec_bexp b \<le> l"
   1.101 -    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   1.102 +    assume "sec b \<le> l"
   1.103 +    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
   1.104      hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
   1.105      thus ?thesis by (metis t' big_step.IfFalse)
   1.106    next
   1.107 -    assume "\<not> sec_bexp b \<le> l"
   1.108 -    hence 0: "sec_bexp b \<noteq> 0" by arith
   1.109 -    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
   1.110 -      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
   1.111 -    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
   1.112 +    assume "\<not> sec b \<le> l"
   1.113 +    hence 0: "sec b \<noteq> 0" by arith
   1.114 +    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
   1.115 +      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
   1.116 +    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
   1.117      have "s = s' (\<le> l)" by auto
   1.118      moreover
   1.119      from termi_if_non0[OF 1 0, of t] obtain t' where
   1.120        "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
   1.121      moreover
   1.122 -    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
   1.123 +    from confinement[OF this 1] `\<not> sec b \<le> l`
   1.124      have "t = t' (\<le> l)" by auto
   1.125      ultimately
   1.126      show ?case using `s = t (\<le> l)` by auto
   1.127    qed
   1.128  next
   1.129    case (WhileFalse b s c)
   1.130 -  hence [simp]: "sec_bexp b = 0" by auto
   1.131 -  have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
   1.132 +  hence [simp]: "sec b = 0" by auto
   1.133 +  have "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
   1.134    hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl)
   1.135    with WhileFalse.prems(2) show ?case by auto
   1.136  next
   1.137    case (WhileTrue b s c s'' s')
   1.138    let ?w = "WHILE b DO c"
   1.139 -  from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
   1.140 +  from `0 \<turnstile> ?w` have [simp]: "sec b = 0" by auto
   1.141    have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
   1.142    from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
   1.143    obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
   1.144 @@ -174,13 +174,13 @@
   1.145  Skip':
   1.146    "l \<turnstile>' SKIP"  |
   1.147  Assign':
   1.148 -  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
   1.149 +  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
   1.150  Seq':
   1.151    "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
   1.152  If':
   1.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"  |
   1.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"  |
   1.155  While':
   1.156 -  "\<lbrakk> sec_bexp b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
   1.157 +  "\<lbrakk> sec b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
   1.158  anti_mono':
   1.159    "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
   1.160