Homework 3

Definitions File

theory Defs
  imports "HOL-IMP.BExp"
begin

declare [[names_short]]

datatype instr = LOADI val | LOAD vname | bADD | bSUB | bMAX | bMIN

type_synonym stack = "val list"

fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
"exec1 (LOADI n) _ stk  =  n # stk" |
"exec1 (LOAD x) s stk  =  s(x) # stk" |
"exec1 bADD _ (j # i # stk)  =  (i + j) # stk" |
"exec1 bSUB _ (j # i # stk)  =  (i - j) # stk" |
"exec1 bMAX _ (j # i # stk)  =  (max i j) # stk" |
"exec1 bMIN _ (j # i # stk)  =  (min i j) # stk"

fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
"exec [] _ stk = stk" |
"exec (i#is) s stk = exec is s (exec1 i s stk)"

lemma exec_append[simp]:
  "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
apply(induction is1 arbitrary: stk)
apply (auto)
done

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

theorem exec_acomp: "exec (acomp a) s stk = aval a s # stk"
apply(induction a arbitrary: stk)
  apply (auto)
done

type_synonym 'a word = "'a list"

type_synonym 'a lang = "'a word set"

definition concat :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
  where "concat L M \<equiv> {v @ w | v w. v \<in> L \<and> w \<in> M}"

fun pow :: "'a lang \<Rightarrow> nat \<Rightarrow> 'a lang" where
"pow L 0 = {[]}" |
"pow L (Suc n) = concat L (pow L n)"

datatype 'a rexp = Atom 'a | Concat "'a rexp" "'a rexp" |
  Or "'a rexp" "'a rexp" | Star "'a rexp"



consts bcomp :: "bexp \<Rightarrow> instr list"

consts lang :: "'a rexp \<Rightarrow> 'a lang"

consts or_outward :: "'a rexp \<Rightarrow> 'a rexp"

consts in_lang :: "'a rexp \<Rightarrow> 'a word \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

type_synonym stack = "val list"

fun bcomp :: "bexp \<Rightarrow> instr list"  where
  "bcomp _ = []"

theorem exec_bcomp: "exec (bcomp b) s stk = (if bval b s then 1 else 0) # stk"
  sorry

type_synonym 'a word = "'a list"

type_synonym 'a lang = "'a word set"

lemma empty_mem_pow_zero [simp, intro]: "[] \<in> pow L 0"
  by (auto simp: concat_def)

lemma append_mem_pow_SucI [intro]:
  "v \<in> L \<Longrightarrow> w \<in> pow L n \<Longrightarrow> (v @ w) \<in> pow L (Suc n)"
  by (auto simp: concat_def)

fun lang :: "'a rexp \<Rightarrow> 'a lang"  where
  "lang _ = {}"

fun or_outward :: "'a rexp \<Rightarrow> 'a rexp"  where
  "or_outward r = r"

value "or_outward (Star (Concat (Concat (Or (Atom ''a'') (Atom ''b'')) (Atom ''c'')) (Atom ''d''))) =
Star (Concat (Or (Concat (Atom ''a'') (Atom ''c'')) (Concat (Atom ''b'') (Atom ''c''))) (Atom ''d''))"
             
lemma lang_or_outward_eq_lang: "lang (or_outward r) = lang r"
  sorry

inductive in_lang :: "'a rexp \<Rightarrow> 'a word \<Rightarrow> bool" 

lemma mem_lang_if_in_lang: "in_lang r w \<Longrightarrow> w \<in> lang r"
  sorry

lemma in_lang_Star_if_mem_powI:
  "(\<And>w. w \<in> lang r \<Longrightarrow> in_lang r w) \<Longrightarrow>
  w \<in> pow (lang r) n \<Longrightarrow> in_lang (Star r) w"
  sorry

lemma in_lang_if_mem_lang: "w \<in> lang r \<Longrightarrow> in_lang r w"
  sorry

corollary in_lang_iff_mem_lang: "in_lang r w \<longleftrightarrow> w \<in> lang r"
  sorry

 end

Check File

theory Check
  imports Submission
begin

theorem exec_bcomp: "exec (bcomp b) s stk = (if bval b s then 1 else 0) # stk"
  by (rule Submission.exec_bcomp)

lemma lang_or_outward_eq_lang: "lang (or_outward r) = lang r"
  by (rule Submission.lang_or_outward_eq_lang)

lemma mem_lang_if_in_lang: "in_lang r w \<Longrightarrow> w \<in> lang r"
  by (rule Submission.mem_lang_if_in_lang)

lemma in_lang_Star_if_mem_powI: "(\<And>w. w \<in> lang r \<Longrightarrow> in_lang r w) \<Longrightarrow>
  w \<in> pow (lang r) n \<Longrightarrow> in_lang (Star r) w"
  by (rule Submission.in_lang_Star_if_mem_powI)

lemma in_lang_if_mem_lang: "w \<in> lang r \<Longrightarrow> in_lang r w"
  by (rule Submission.in_lang_if_mem_lang)

end