src/HOL/IMP/Sec_TypingT.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45015 fdac1e9880eb
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
theory Sec_TypingT imports Sec_Type_Expr
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
subsection "A Termination-Sensitive Syntax Directed System"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
Skip:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
  "l \<turnstile> SKIP"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
Assign:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
Semi:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
  "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
If:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
  "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
   \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
While:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
  "sec_bexp b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
code_pred (expected_modes: i => i => bool) sec_type .
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
inductive_cases [elim!]:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
  "l \<turnstile> x ::= a"  "l \<turnstile> c\<^isub>1;c\<^isub>2"  "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2"  "l \<turnstile> WHILE b DO c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    26
apply(induction arbitrary: l' rule: sec_type.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
apply (metis sec_type.intros(1))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
apply (metis le_trans sec_type.intros(2))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
apply (metis sec_type.intros(3))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
apply (metis If le_refl sup_mono sup_nat_def)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
by (metis While le_0_eq)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    35
proof(induction rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
  case Skip thus ?case by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
  case Assign thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
  case Semi thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
  case (IfTrue b s c1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
  hence "max (sec_bexp b) l \<turnstile> c1" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
  hence "l \<turnstile> c1" by (metis le_maxI2 anti_mono)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    45
  thus ?case using IfTrue.IH by metis
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
  case (IfFalse b s c2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
  hence "max (sec_bexp b) l \<turnstile> c2" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
  hence "l \<turnstile> c2" by (metis le_maxI2 anti_mono)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    50
  thus ?case using IfFalse.IH by metis
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
  case WhileFalse thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
  case (WhileTrue b s1 c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
  hence "l \<turnstile> c" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
  thus ?case using WhileTrue by metis
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    59
lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    60
apply(induction arbitrary: s rule: sec_type.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
apply (metis big_step.Skip)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
apply (metis big_step.Assign)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    63
apply (metis big_step.Semi)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    64
apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
apply simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow>  s = t (\<le> l)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
  \<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
    70
proof(induction arbitrary: t rule: big_step_induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    71
  case Skip thus ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
  case (Assign x a s)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
  have "sec x >= sec_aexp a" using `0 \<turnstile> x ::= a` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
  have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
  moreover
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
  have "s(x := aval a s) = t(x := aval a t) (\<le> l)"
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"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    80
    with `sec x \<ge> sec_aexp a` have "sec_aexp a \<le> l" by arith
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
  ultimately show ?case by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    88
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    89
  case Semi thus ?case by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    90
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    91
  case (IfTrue b s c1 s' c2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    92
  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
  obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    94
    using IfTrue(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c1`] IfTrue.prems(2)] by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    95
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    96
  proof cases
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    97
    assume "sec_bexp b \<le> l"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    98
    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    99
    hence "bval b t" using `bval b s` by(simp add: bval_eq_if_eq_le)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   100
    thus ?thesis by (metis t' big_step.IfTrue)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   101
  next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   102
    assume "\<not> sec_bexp b \<le> l"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   103
    hence 0: "sec_bexp b \<noteq> 0" by arith
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   104
    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   105
      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   106
    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   107
    have "s = s' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   108
    moreover
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   109
    from termi_if_non0[OF 1 0, of t] obtain t' where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   110
      "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   111
    moreover
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   112
    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   113
    have "t = t' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   114
    ultimately
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   115
    show ?case using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   116
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   117
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   118
  case (IfFalse b s c2 s' c1)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   119
  have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfFalse.prems by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   120
  obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   121
    using IfFalse(3)[OF anti_mono[OF `sec_bexp b \<turnstile> c2`] IfFalse.prems(2)] by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   122
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   123
  proof cases
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   124
    assume "sec_bexp b \<le> l"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   125
    hence "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   126
    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
   127
    thus ?thesis by (metis t' big_step.IfFalse)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   128
  next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   129
    assume "\<not> sec_bexp b \<le> l"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   130
    hence 0: "sec_bexp b \<noteq> 0" by arith
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   131
    have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   132
      by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   133
    from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] `\<not> sec_bexp b \<le> l`
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   134
    have "s = s' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   135
    moreover
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   136
    from termi_if_non0[OF 1 0, of t] obtain t' where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   137
      "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" ..
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   138
    moreover
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   139
    from confinement[OF this 1] `\<not> sec_bexp b \<le> l`
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   140
    have "t = t' (\<le> l)" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   141
    ultimately
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   142
    show ?case using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   143
  qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   144
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   145
  case (WhileFalse b s c)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   146
  hence [simp]: "sec_bexp b = 0" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   147
  have "s = t (\<le> sec_bexp b)" using `s = t (\<le> l)` by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   148
  hence "\<not> bval b t" using `\<not> bval b s` by (metis bval_eq_if_eq_le le_refl)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   149
  with WhileFalse.prems(2) show ?case by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   150
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   151
  case (WhileTrue b s c s'' s')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   152
  let ?w = "WHILE b DO c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   153
  from `0 \<turnstile> ?w` have [simp]: "sec_bexp b = 0" by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   154
  have "0 \<turnstile> c" using WhileTrue.prems(1) by auto
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   155
  from WhileTrue.IH(1)[OF this WhileTrue.prems(2)]
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   156
  obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   157
  from WhileTrue.IH(2)[OF `0 \<turnstile> ?w` this(2)]
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   158
  obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   159
  from `bval b s` have "bval b t"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   160
    using bval_eq_if_eq_le[OF `s = t (\<le>l)`] by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   161
  show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   162
    using big_step.WhileTrue[OF `bval b t` `(c,t) \<Rightarrow> t''` `(?w,t'') \<Rightarrow> t'`]
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   163
    by (metis `s' = t' (\<le> l)`)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   164
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   165
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   166
subsection "The Standard Termination-Sensitive System"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   167
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   168
text{* The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   169
standard formulation, however, is slightly different, replacing the maximum
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   170
computation by an antimonotonicity rule. We introduce the standard system now
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   171
and show the equivalence with our formulation. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   172
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   173
inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   174
Skip':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   175
  "l \<turnstile>' SKIP"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   176
Assign':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   177
  "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   178
Semi':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   179
  "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   180
If':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   181
  "\<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"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   182
While':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   183
  "\<lbrakk> sec_bexp b = 0;  0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   184
anti_mono':
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   185
  "\<lbrakk> l \<turnstile>' c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   186
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   187
lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   188
apply(induction rule: sec_type.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   189
apply (metis Skip')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   190
apply (metis Assign')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   191
apply (metis Semi')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   192
apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   193
by (metis While')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   194
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   195
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   196
lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43158
diff changeset
   197
apply(induction rule: sec_type'.induct)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   198
apply (metis Skip)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   199
apply (metis Assign)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   200
apply (metis Semi)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   201
apply (metis min_max.sup_absorb2 If)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   202
apply (metis While)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   203
by (metis anti_mono)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   204
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
   205
end