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

hide_const D

fun AV :: "com \<Rightarrow> vname set" where
  "AV _ = undefined"

fun D :: "vname set \<Rightarrow> com \<Rightarrow> bool" where
  "D _ = undefined"

lemma D_progress:
  assumes "c \<noteq> SKIP"
  shows "D (dom s) c \<Longrightarrow> \<exists> cs'. (c,s) \<rightarrow> cs'"
  using assms
proof (induction c arbitrary: s)
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
next
  case (If b c1 c2)
  then obtain bv where "bval b s = Some bv" by (auto dest!: bval_Some)
  then show ?case
    by(cases bv) (auto intro: small_step.IfTrue small_step.IfFalse)
qed (fastforce intro: small_step.intros)+

lemma D_incr: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> dom s \<union> AV c \<subseteq> dom s' \<union> AV c'"
  sorry

lemma D_mono: "A \<subseteq> A' \<Longrightarrow> D A c \<Longrightarrow> D A' c"
  sorry

theorem D_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c \<Longrightarrow> D (dom s') c'"
  sorry

theorem D_sound: "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> c' \<noteq> SKIP \<Longrightarrow> D (dom s) c \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
  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)

theorem D_preservation: "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c \<Longrightarrow> D (dom s') c'"
  by (rule Submission.D_preservation)

theorem D_sound: "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> c' \<noteq> SKIP \<Longrightarrow> D (dom s) c \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
  by (rule Submission.D_sound)

end