###### Cookies disclaimer

Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 13

The task corresponding to homework 13.

## Resources

Download Files

### 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```

Terms and Conditions