Homework 13

Definitions File

theory Defs
  imports "IMP.Big_Step"
begin

class vars = fixes vars :: "'a \<Rightarrow> vname set"

instantiation aexp :: vars
begin
fun vars_aexp :: "aexp \<Rightarrow> vname set" where
"vars (N n) = {}" |
"vars (V x) = {x}" |
"vars (Plus a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
instance ..
end

instantiation bexp :: vars
begin
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
"vars (Bc v) = {}" |
"vars (Not b) = vars b" |
"vars (And b\<^sub>1 b\<^sub>2) = vars b\<^sub>1 \<union> vars b\<^sub>2" |
"vars (Less a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
instance ..
end

instantiation com :: vars
begin
fun vars_com :: "com \<Rightarrow> vname set" where
 "vars_com  SKIP = {}"
|"vars_com (x ::= a) = {x} \<union> vars a"
|"vars_com (c1 ;; c2) = vars_com c1 \<union> vars_com c2"
|"vars_com (IF b THEN c1 ELSE c2) = vars b \<union> vars_com c1 \<union> vars_com c2"
|"vars_com (WHILE b DO c) = vars b \<union> vars_com c"
instance ..
end

end

Template File

theory Submission
  imports Defs
begin

paragraph \<open>Question 1\<close>
theorem ex1:
  "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> vars c \<inter> vars b = {} \<Longrightarrow> \<not> bval b s"
  sorry

paragraph \<open>Question 2\<close>

theorem ex2:
  "no c \<Longrightarrow> \<forall> s. \<exists> t. (c, s) \<Rightarrow> t"
  sorry

fun AA :: "com \<Rightarrow> (vname \<times> vname) set \<Rightarrow> (vname \<times> vname) set" where
  "AA _ _ = undefined"

fun gen :: "com \<Rightarrow> (vname \<times> vname) set" and kill :: "com \<Rightarrow> (vname \<times> vname) set" where
  "gen _ = undefined" |
  "kill _ = undefined"

theorem AA_gen_kill: "AA c A = (A \<union> gen c) - kill c"
  sorry

lemma AA_distr: "AA c (A1 \<inter> A2) = AA c A1 \<inter> AA c A2"
  sorry

lemma AA_idemp: "AA c (AA c A) = AA c A"
  sorry

theorem AA_sound:
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> \<forall> (x,y) \<in> A. s x = s y \<Longrightarrow> \<forall> (x,y) \<in> AA c A. s' x = s' y"
  sorry

fun subst :: "(vname \<Rightarrow> vname) \<Rightarrow> aexp \<Rightarrow> aexp" where
  "subst f (N n) = N n" |
  "subst f (V y) = V (f y)" |
  "subst f (Plus a1 a2) = Plus (subst f a1) (subst f a2)"

lemma subst_lemma: "aval (subst \<sigma> a) s = aval a (\<lambda>x. s (\<sigma> x))"
  sorry

definition
  "to_map A x = (if \<exists> y. (x, y) \<in> A then SOME y. (x, y) \<in> A else x)"

fun CP where
  "CP SKIP A = SKIP"
| "CP (x ::= a) A = (x ::= subst (to_map A) a)"

lemma to_map_eq:
  assumes "\<forall>(x,y)\<in>A. s x = s y"
  shows "(\<lambda>x. s (to_map A x)) = s"
  using assms unfolding to_map_def
  by (auto del: ext intro!: ext) (metis (mono_tags, lifting) old.prod.case someI_ex)

theorem CP_correct1:
  assumes "(c, s) \<Rightarrow> t" "\<forall>(x,y)\<in>A. s x = s y"
  shows   "(CP c A, s) \<Rightarrow> t"
  sorry

theorem CP_correct2:
  assumes "(CP c A, s) \<Rightarrow> t" "\<forall>(x,y)\<in>A. s x = s y"
  shows "(c, s) \<Rightarrow> t"
  sorry

corollary CP_correct:
  "c \<sim> CP c {}"
  apply (rule equivI)
   apply (erule CP_correct1, simp)
  apply (erule CP_correct2, simp)
  done

end

Check File

theory Check
  imports Submission
begin

theorem ex2:
  "no c \<Longrightarrow> \<forall> s. \<exists> t. (c, s) \<Rightarrow> t"
  by (rule Submission.ex2)

theorem AA_gen_kill: "AA c A = (A \<union> gen c) - kill c"
  by (rule Submission.AA_gen_kill)

theorem AA_sound:
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> \<forall> (x,y) \<in> A. s x = s y \<Longrightarrow> \<forall> (x,y) \<in> AA c A. s' x = s' y"
  by (rule Submission.AA_sound)

theorem CP_correct1:
  assumes "(c, s) \<Rightarrow> t" "\<forall>(x,y)\<in>A. s x = s y"
  shows   "(CP c A, s) \<Rightarrow> t"
  using assms by (rule Submission.CP_correct1)

theorem CP_correct2:
  assumes "(CP c A, s) \<Rightarrow> t" "\<forall>(x,y)\<in>A. s x = s y"
  shows "(c, s) \<Rightarrow> t"
  using assms by (rule Submission.CP_correct2)

end