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 4

This is the task corresponding to homework 4.

## Resources

### Definitions File

```theory Defs
imports Main "HOL-IMP.Vars"
begin

declare [[names_short]]

type_synonym ('q,'l) lts = "'q \<Rightarrow> 'l \<Rightarrow> 'q \<Rightarrow> bool"

inductive word :: " ('q,'l) lts \<Rightarrow> 'q \<Rightarrow> 'l list \<Rightarrow> 'q \<Rightarrow> bool" for \<delta> where
empty: " word \<delta> q [] q"
| prepend: "\<lbrakk>\<delta> p l ph; word \<delta> ph ls q\<rbrakk> \<Longrightarrow> word \<delta> p (l # ls) q"

type_synonym stack = "val list"

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

fun comp :: "aexp \<Rightarrow> instr list" where
"comp (N n) = [LOADI n]" |
"comp (V x) = [LOAD x]" |
"comp (Plus e\<^sub>1 e\<^sub>2) = comp e\<^sub>1 @ comp e\<^sub>2 @ [ADD]"

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

definition "correct a ins \<equiv> \<forall>s stk. exec ins s stk = Some (aval a s # stk)"

consts prod :: "('q\<^sub>1,'l) lts \<Rightarrow> ('q\<^sub>2,'l) lts \<Rightarrow> 'q\<^sub>1\<times>'q\<^sub>2 \<Rightarrow> 'l \<Rightarrow> 'q\<^sub>1\<times>'q\<^sub>2 \<Rightarrow> bool"

end```

### Template File

```theory Submission
imports Defs
begin

inductive prod :: "('q\<^sub>1,'l) lts \<Rightarrow> ('q\<^sub>2,'l) lts \<Rightarrow> 'q\<^sub>1\<times>'q\<^sub>2 \<Rightarrow> 'l \<Rightarrow> 'q\<^sub>1\<times>'q\<^sub>2 \<Rightarrow> bool" for \<delta>\<^sub>1 \<delta>\<^sub>2

theorem prod_sound:
assumes "word (prod \<delta>\<^sub>1 \<delta>\<^sub>2) (p\<^sub>1,p\<^sub>2) ls (q\<^sub>1,q\<^sub>2)"
shows "word \<delta>\<^sub>1 p\<^sub>1 ls q\<^sub>1 \<and> word \<delta>\<^sub>2 p\<^sub>2 ls q\<^sub>2"
sorry

lemma prod_complete:
assumes "word \<delta>\<^sub>1 p\<^sub>1 ls q\<^sub>1"
and "word \<delta>\<^sub>2 p\<^sub>2 ls q\<^sub>2"
shows "word (prod \<delta>\<^sub>1 \<delta>\<^sub>2) (p\<^sub>1,p\<^sub>2) ls (q\<^sub>1,q\<^sub>2)"
sorry

corollary "{w. word (prod \<delta>\<^sub>1 \<delta>\<^sub>2) (p\<^sub>1,p\<^sub>2) w (q\<^sub>1,q\<^sub>2)} = {w. word \<delta>\<^sub>1 p\<^sub>1 w q\<^sub>1} \<inter> {w. word \<delta>\<^sub>2 p\<^sub>2 w q\<^sub>2}"
using prod_sound prod_complete by fast

theorem vars_in_ins:
assumes "x \<in> vars a"
shows "correct a ins \<Longrightarrow> LOAD x \<in> set ins"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem prod_sound: "(word (prod \<delta>\<^sub>1 \<delta>\<^sub>2) (p\<^sub>1,p\<^sub>2) ls (q\<^sub>1,q\<^sub>2)) \<Longrightarrow> word \<delta>\<^sub>1 p\<^sub>1 ls q\<^sub>1 \<and> word \<delta>\<^sub>2 p\<^sub>2 ls q\<^sub>2"
by (rule Submission.prod_sound)

lemma prod_complete: "(word \<delta>\<^sub>1 p\<^sub>1 ls q\<^sub>1) \<Longrightarrow> (word \<delta>\<^sub>2 p\<^sub>2 ls q\<^sub>2) \<Longrightarrow> word (prod \<delta>\<^sub>1 \<delta>\<^sub>2) (p\<^sub>1,p\<^sub>2) ls (q\<^sub>1,q\<^sub>2)"
by (rule Submission.prod_complete)

theorem vars_in_ins: "(x \<in> vars a) \<Longrightarrow> correct a ins \<Longrightarrow> LOAD x \<in> set ins"
by (rule Submission.vars_in_ins)

end```

Terms and Conditions