src/HOL/IMP/Sec_Typing.thy
author haftmann
Wed, 25 Dec 2013 17:39:06 +0100
changeset 54863 82acc20ded73
parent 53015 a1119cf551e8
child 54864 a064732223ad
permissions -rw-r--r--
prefer more canonical names for lemmas on min/max
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
theory Sec_Typing imports Sec_Type_Expr
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
subsection "Syntax Directed Typing"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
Skip:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
  "l \<turnstile> SKIP" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
Assign:
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    12
  "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
    13
Seq:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
    14
  "\<lbrakk> l \<turnstile> c\<^sub>1;  l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^sub>1;;c\<^sub>2" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
If:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
    16
  "\<lbrakk> max (sec b) l \<turnstile> c\<^sub>1;  max (sec b) l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
While:
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    18
  "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
code_pred (expected_modes: i => i => bool) sec_type .
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
value "0 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
value "1 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x''  ::= N 0 ELSE SKIP"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
inductive_cases [elim!]:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
    27
  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^sub>1;;c\<^sub>2"  "l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2"  "l \<turnstile> WHILE b DO c"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
text{* An important property: anti-monotonicity. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    33
apply(induction arbitrary: l' rule: sec_type.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
apply (metis sec_type.intros(1))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
apply (metis le_trans sec_type.intros(2))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
apply (metis sec_type.intros(3))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
apply (metis If le_refl sup_mono sup_nat_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
apply (metis While le_refl sup_mono sup_nat_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
lemma confinement: "\<lbrakk> (c,s) \<Rightarrow> t;  l \<turnstile> c \<rbrakk> \<Longrightarrow> s = t (< l)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    42
proof(induction rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
  case Skip thus ?case by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
  case Assign thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
next
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
    47
  case Seq thus ?case by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
  case (IfTrue b s c1)
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    50
  hence "max (sec b) l \<turnstile> c1" by auto
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
    51
  hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    52
  thus ?case using IfTrue.IH by metis
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
  case (IfFalse b s c2)
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    55
  hence "max (sec b) l \<turnstile> c2" by auto
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
    56
  hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    57
  thus ?case using IfFalse.IH by metis
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    59
  case WhileFalse thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    60
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
  case (WhileTrue b s1 c)
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    62
  hence "max (sec b) l \<turnstile> c" by auto
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
    63
  hence "l \<turnstile> c" by (metis max.cobounded2 anti_mono)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    64
  thus ?case using WhileTrue by metis
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
theorem noninterference:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
  "\<lbrakk> (c,s) \<Rightarrow> s'; (c,t) \<Rightarrow> t';  0 \<turnstile> c;  s = t (\<le> l) \<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
   \<Longrightarrow> s' = t' (\<le> l)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    71
proof(induction arbitrary: t t' rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
  case Skip thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
  case (Assign x a s)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
  have [simp]: "t' = t(x := aval a t)" using Assign by auto
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    76
  have "sec x >= sec a" using `0 \<turnstile> x ::= a` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
  proof auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
    assume "sec x \<le> l"
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    80
    with `sec x >= sec a` have "sec a \<le> l" by arith
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    81
    thus "aval a s = aval a t"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    82
      by (rule aval_eq_if_eq_le[OF `s = t (\<le> l)`])
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
  next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    84
    fix y assume "y \<noteq> x" "sec y \<le> l"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    85
    thus "s y = t y" using `s = t (\<le> l)` by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    86
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    87
next
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
    88
  case Seq thus ?case by blast
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    89
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    90
  case (IfTrue b s c1 s' c2)
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
    91
  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    92
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
  proof cases
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    94
    assume "sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    95
    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    96
    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
    97
    with IfTrue.IH IfTrue.prems(1,3) `sec b \<turnstile> c1`  anti_mono
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    98
    show ?thesis by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    99
  next
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   100
    assume "\<not> sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   101
    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   102
      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   103
    from confinement[OF `(c1, s) \<Rightarrow> s'` `sec b \<turnstile> c1`] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   104
    have "s = s' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   105
    moreover
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   106
    from confinement[OF `(IF b THEN c1 ELSE c2, t) \<Rightarrow> t'` 1] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   107
    have "t = t' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   108
    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   109
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   110
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   111
  case (IfFalse b s c2 s' c1)
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   112
  have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   113
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   114
  proof cases
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   115
    assume "sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   116
    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   117
    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   118
    with IfFalse.IH IfFalse.prems(1,3) `sec b \<turnstile> c2` anti_mono
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   119
    show ?thesis by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   120
  next
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   121
    assume "\<not> sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   122
    have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   123
      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c1` `sec b \<turnstile> c2`)
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   124
    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   125
    have "s = s' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   126
    moreover
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   127
    from confinement[OF `(IF b THEN c1 ELSE c2, t) \<Rightarrow> t'` 1] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   128
    have "t = t' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   129
    ultimately show "s' = t' (\<le> l)" using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   130
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   131
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   132
  case (WhileFalse b s c)
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   133
  have "sec b \<turnstile> c" using WhileFalse.prems(2) by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   134
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   135
  proof cases
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   136
    assume "sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   137
    hence "s = t (\<le> sec b)" using `s = t (\<le> l)` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   138
    hence "\<not> bval b t" using `\<not> bval b s` by(simp add: bval_eq_if_eq_le)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   139
    with WhileFalse.prems(1,3) show ?thesis by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   140
  next
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   141
    assume "\<not> sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   142
    have 1: "sec b \<turnstile> WHILE b DO c"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   143
      by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   144
    from confinement[OF `(WHILE b DO c, t) \<Rightarrow> t'` 1] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   145
    have "t = t' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   146
    thus "s = t' (\<le> l)" using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   147
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   148
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   149
  case (WhileTrue b s1 c s2 s3 t1 t3)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   150
  let ?w = "WHILE b DO c"
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   151
  have "sec b \<turnstile> c" using `0 \<turnstile> WHILE b DO c` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   152
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   153
  proof cases
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   154
    assume "sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   155
    hence "s1 = t1 (\<le> sec b)" using `s1 = t1 (\<le> l)` by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   156
    hence "bval b t1"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   157
      using `bval b s1` by(simp add: bval_eq_if_eq_le)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   158
    then obtain t2 where "(c,t1) \<Rightarrow> t2" "(?w,t2) \<Rightarrow> t3"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   159
      using `(?w,t1) \<Rightarrow> t3` by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   160
    from WhileTrue.IH(2)[OF `(?w,t2) \<Rightarrow> t3` `0 \<turnstile> ?w`
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   161
      WhileTrue.IH(1)[OF `(c,t1) \<Rightarrow> t2` anti_mono[OF `sec b \<turnstile> c`]
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   162
        `s1 = t1 (\<le> l)`]]
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   163
    show ?thesis by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   164
  next
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   165
    assume "\<not> sec b \<le> l"
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   166
    have 1: "sec b \<turnstile> ?w" by(rule sec_type.intros)(simp_all add: `sec b \<turnstile> c`)
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   167
    from confinement[OF big_step.WhileTrue[OF WhileTrue.hyps] 1] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   168
    have "s1 = s3 (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   169
    moreover
52382
741d10d7f2c1 made proofs more readable
nipkow
parents: 52046
diff changeset
   170
    from confinement[OF `(WHILE b DO c, t1) \<Rightarrow> t3` 1] `\<not> sec b \<le> l`
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   171
    have "t1 = t3 (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   172
    ultimately show "s3 = t3 (\<le> l)" using `s1 = t1 (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   173
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   174
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   175
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   176
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   177
subsection "The Standard Typing System"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   178
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   179
text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   180
standard formulation, however, is slightly different, replacing the maximum
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   181
computation by an antimonotonicity rule. We introduce the standard system now
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   182
and show the equivalence with our formulation. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   183
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   184
inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   185
Skip':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   186
  "l \<turnstile>' SKIP" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   187
Assign':
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   188
  "\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
   189
Seq':
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
   190
  "\<lbrakk> l \<turnstile>' c\<^sub>1;  l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^sub>1;;c\<^sub>2" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   191
If':
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
   192
  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c\<^sub>1;  l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^sub>1 ELSE c\<^sub>2" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   193
While':
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   194
  "\<lbrakk> sec b \<le> l;  l \<turnstile>' c \<rbrakk> \<Longrightarrow> l \<turnstile>' WHILE b DO c" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   195
anti_mono':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   196
  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   197
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   198
lemma sec_type_sec_type': "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   199
apply(induction rule: sec_type.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   200
apply (metis Skip')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   201
apply (metis Assign')
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
   202
apply (metis Seq')
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   203
apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   204
by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   205
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   206
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   207
lemma sec_type'_sec_type: "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   208
apply(induction rule: sec_type'.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   209
apply (metis Skip)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   210
apply (metis Assign)
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
   211
apply (metis Seq)
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   212
apply (metis max.absorb2 If)
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   213
apply (metis max.absorb2 While)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   214
by (metis anti_mono)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   215
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   216
subsection "A Bottom-Up Typing System"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   217
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   218
inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   219
Skip2:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   220
  "\<turnstile> SKIP : l" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   221
Assign2:
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   222
  "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45823
diff changeset
   223
Seq2:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
   224
  "\<lbrakk> \<turnstile> c\<^sub>1 : l\<^sub>1;  \<turnstile> c\<^sub>2 : l\<^sub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^sub>1;;c\<^sub>2 : min l\<^sub>1 l\<^sub>2 " |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   225
If2:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
   226
  "\<lbrakk> sec b \<le> min l\<^sub>1 l\<^sub>2;  \<turnstile> c\<^sub>1 : l\<^sub>1;  \<turnstile> c\<^sub>2 : l\<^sub>2 \<rbrakk>
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52382
diff changeset
   227
  \<Longrightarrow> \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2 : min l\<^sub>1 l\<^sub>2" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   228
While2:
50342
e77b0dbcae5b tuned defs of sec_xyz
nipkow
parents: 47818
diff changeset
   229
  "\<lbrakk> sec b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   230
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   231
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   232
lemma sec_type2_sec_type': "\<turnstile> c : l \<Longrightarrow> l \<turnstile>' c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   233
apply(induction rule: sec_type2.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   234
apply (metis Skip')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   235
apply (metis Assign' eq_imp_le)
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   236
apply (metis Seq' anti_mono' min.cobounded1 min.cobounded2)
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   237
apply (metis If' anti_mono' min.absorb2 min.absorb_iff1 nat_le_linear)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   238
by (metis While')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   239
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   240
lemma sec_type'_sec_type2: "l \<turnstile>' c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   241
apply(induction rule: sec_type'.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   242
apply (metis Skip2 le_refl)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   243
apply (metis Assign2)
54863
82acc20ded73 prefer more canonical names for lemmas on min/max
haftmann
parents: 53015
diff changeset
   244
apply (metis Seq2 min.boundedI)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   245
apply (metis If2 inf_greatest inf_nat_def le_trans)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   246
apply (metis While2 le_trans)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   247
by (metis le_trans)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   248
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   249
end