Cookies disclaimer

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.

Homework 4

This is the task corresponding to homework 4.


Download Files

Definitions File

theory Defs
  imports Main "HOL-IMP.Vars"

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"

datatype instr = LOADI val | LOAD vname | ADD
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)

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)

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"


Template File

theory Submission
  imports Defs

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"

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)"

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"


Check File

theory Check
  imports Submission

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)


Terms and Conditions