equal
deleted
inserted
replaced
182 While': |
182 While': |
183 "\<lbrakk> sec b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" | |
183 "\<lbrakk> sec b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" | |
184 anti_mono': |
184 anti_mono': |
185 "\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c" |
185 "\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c" |
186 |
186 |
187 lemma "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c" |
187 lemma sec_type_sec_type': |
|
188 "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c" |
188 apply(induction rule: sec_type.induct) |
189 apply(induction rule: sec_type.induct) |
189 apply (metis Skip') |
190 apply (metis Skip') |
190 apply (metis Assign') |
191 apply (metis Assign') |
191 apply (metis Seq') |
192 apply (metis Seq') |
192 apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono') |
193 apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono') |
193 by (metis While') |
194 by (metis While') |
194 |
195 |
195 |
196 |
196 lemma "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c" |
197 lemma sec_type'_sec_type: |
|
198 "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c" |
197 apply(induction rule: sec_type'.induct) |
199 apply(induction rule: sec_type'.induct) |
198 apply (metis Skip) |
200 apply (metis Skip) |
199 apply (metis Assign) |
201 apply (metis Assign) |
200 apply (metis Seq) |
202 apply (metis Seq) |
201 apply (metis min_max.sup_absorb2 If) |
203 apply (metis min_max.sup_absorb2 If) |
202 apply (metis While) |
204 apply (metis While) |
203 by (metis anti_mono) |
205 by (metis anti_mono) |
204 |
206 |
|
207 corollary sec_type_eq: "l \<turnstile> c \<longleftrightarrow> l \<turnstile>' c" |
|
208 by (metis sec_type'_sec_type sec_type_sec_type') |
|
209 |
205 end |
210 end |