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

This is the task corresponding to homework 3.

## Resources

Download Files

### Definitions File

```theory Defs imports "HOL-IMP.ASM" begin

inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r  where
refl:  "star r x x"
| step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"

lemma star_prepend: "\<lbrakk>r x y; star r y z\<rbrakk> \<Longrightarrow> star r x z"
by (rule step)

lemma star_append: "\<lbrakk> star r x y; r y z \<rbrakk> \<Longrightarrow> star r x z"
by (induct rule: star.induct) (auto intro: star.intros)

inductive star' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r  where
refl': "star' r x x"
| step': "\<lbrakk>star' r x y; r y z\<rbrakk> \<Longrightarrow> star' r x z"

lemma star'_prepend: "\<lbrakk>star' r y z; r x y\<rbrakk> \<Longrightarrow> star' r x z"
apply (induction rule: star'.induct)
apply (auto intro: star'.intros)
done

lemma "star r x y = star' r x y"
proof
assume "star r x y"
thus "star' r x y"
by induct (auto intro: star'.intros star'_prepend)
next
assume "star' r x y"
thus "star r x y"
by induct (auto intro: star.intros star_append)
qed

fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack option"  where
"exec1 (LOADI n) _ stk = Some (n # stk)"
| "exec1 (LOAD x) s stk = Some (s(x) # stk)"
| "exec1 ADD _ stk = (case stk of
a # b # c \<Rightarrow> Some ((a + b) # c)
| _ \<Rightarrow> None)"

fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack option"  where
"exec [] _ stk = Some stk"
| "exec (i # ins) s stk = (case exec1 i s stk of
Some stk \<Rightarrow> exec ins s stk
| None \<Rightarrow> None)"

lemma exec_append[simp]:
"exec (ins1 @ ins2) s stk = (case exec ins1 s stk of
Some stk \<Rightarrow> exec ins2 s stk
| None \<Rightarrow> None)"
apply(induction ins1 arbitrary: stk)
apply (auto split: option.split)
done

theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)"
apply(induction a arbitrary: stk)
apply (auto)
done

lemma
assumes total: "\<forall> x y. T x y \<or> T y x"
and anti: "\<forall> x y. A x y \<and> A y x \<longrightarrow> x = y"
and subset: "\<forall> x y. T x y \<longrightarrow> A x y"
shows "A x y \<longrightarrow> T x y"
proof
fix x y assume "A x y"
from total have "T x y \<or> T y x" by simp
then show "T x y"
proof
assume "T x y"
then show ?thesis .
next
assume "T y x"
with subset have "A y x" by simp
with \<open>A x y\<close> anti have "x = y" by simp
with \<open>T y x\<close> show ?thesis by simp
qed
qed

end```

### Template File

```theory Submission imports Defs begin

fun can_execute :: "nat \<Rightarrow> instr list \<Rightarrow> bool" where
"can_execute _ = undefined"

theorem can_exec_correct:
"can_execute (length stk) ins \<Longrightarrow> exec ins s stk \<noteq> None"
sorry

theorem can_exec_complete:
"exec ins s stk = Some res \<Longrightarrow> can_execute (length stk) ins"
sorry

inductive exec1r :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack \<Rightarrow> bool"

inductive execr :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack \<Rightarrow> bool"

theorem step_equiv: "exec1r i s stk stk' \<longleftrightarrow> exec1 i s stk = Some stk'"
sorry

theorem exec_equiv: "execr ins s stk stk' \<longleftrightarrow> (exec ins s stk = Some stk')"
sorry

datatype bexp = Var vname | Not bexp | And bexp bexp | Or bexp bexp

type_synonym state = "vname \<Rightarrow> bool"

fun is_var :: "bexp \<Rightarrow> bool" where
"is_var (Var _) = True"
| "is_var _ = False" where
"is_var _ = undefined"

fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval _ = undefined"

inductive is_nnf :: "bexp \<Rightarrow> bool"

fun sub :: "bexp \<Rightarrow> bexp set" where
"sub _ = undefined"

value "sub (And (Not (Var ''x'')) (Var ''y'')) =
{
Var ''x'',
Var ''y'',
Not (Var (''x'')),
And (Not (Var ''x'')) (Var ''y'')
}"

theorem nnf_not: "is_nnf b = (\<forall>b'. Not b' \<in> sub b \<longrightarrow> is_var b')"
sorry

fun nnf :: "bexp \<Rightarrow> bexp" where
"nnf _ = undefined"

theorem nnf_sound: "is_nnf (nnf b)"
sorry

theorem nnf_compl: "bval (nnf b) s = bval b s"
sorry

end```

### Check File

```theory Check imports Submission begin

theorem can_exec_correct:
"can_execute (length stk) ins \<Longrightarrow> exec ins s stk \<noteq> None"
by (rule Submission.can_exec_correct)

theorem can_exec_complete:
"exec ins s stk = Some res \<Longrightarrow> can_execute (length stk) ins"
by (rule Submission.can_exec_complete)

theorem step_equiv: "exec1r i s stk stk' \<longleftrightarrow> exec1 i s stk = Some stk'"
by (rule Submission.step_equiv)

theorem exec_equiv: "execr ins s stk stk' \<longleftrightarrow> (exec ins s stk = Some stk')"
by (rule Submission.exec_equiv)

theorem nnf_not: "is_nnf b = (\<forall>b'. Not b' \<in> sub b \<longrightarrow> is_var b')"
by (rule Submission.nnf_not)

theorem nnf_sound: "is_nnf (nnf b)"
by (rule Submission.nnf_sound)

theorem nnf_compl: "bval (nnf b) s = bval b s"
by (rule Submission.nnf_compl)

end```

Terms and Conditions