I agree 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.
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
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
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