Homework 7

Definitions File

theory Defs
  imports "HOL-IMP.Sec_Type_Expr" "HOL-IMP.Def_Init_Small"
begin

inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
  Skip: "l \<turnstile> SKIP" |
  Assign: "\<lbrakk> sec x \<ge> sec a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
  Seq: "\<lbrakk> l \<turnstile> c\<^sub>1;  l \<turnstile> c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^sub>1;;c\<^sub>2" |
  If: "\<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" |
  While: "max (sec b) l \<turnstile> c \<Longrightarrow> l \<turnstile> WHILE b DO c"

inductive_cases [elim!]: "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"

lemma anti_mono: "\<lbrakk> l \<turnstile> c;  l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile> c"
  apply(induction arbitrary: l' rule: sec_type.induct)
  apply (metis sec_type.intros(1))
  apply (metis le_trans sec_type.intros(2))
  apply (metis sec_type.intros(3))
  apply (metis If le_refl sup_mono sup_nat_def)
  apply (metis While le_refl sup_mono sup_nat_def)
  done

inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
  Skip2: "\<turnstile> SKIP : l" |
  Assign2: "sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
  Seq2: "\<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 " |
  If2: "\<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> \<Longrightarrow> \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2 : min l\<^sub>1 l\<^sub>2" |
  While2:  "\<lbrakk> sec b \<le> l;  \<turnstile> c : l \<rbrakk> \<Longrightarrow> \<turnstile> WHILE b DO c : l"



end

Template File

theory Submission
  imports Defs
begin

theorem bottom_up_impl_top_down: "\<turnstile> c : l \<Longrightarrow> l \<turnstile> c"
  sorry

theorem top_down_impl_bottom_up: "l \<turnstile> c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem bottom_up_impl_top_down: "\<turnstile> c : l \<Longrightarrow> l \<turnstile> c"
  by (rule Submission.bottom_up_impl_top_down)

theorem top_down_impl_bottom_up: "l \<turnstile> c \<Longrightarrow> \<exists> l' \<ge> l. \<turnstile> c : l'"
  by (rule Submission.top_down_impl_bottom_up)

end