Homework 3

Definitions File

theory Defs
  imports Main
begin

abbreviation a where "a \<equiv> CHR ''a''"
abbreviation b where "b \<equiv> CHR ''b''"

definition
  "L = {w. \<exists>n. w = replicate n a @ replicate n b}"

datatype instr = LDI int | LD nat | ST nat | ADD nat

type_synonym rstate = "nat \<Rightarrow> int"


datatype expr = C int | V nat | A expr expr

fun val :: "expr \<Rightarrow> (nat \<Rightarrow> int) \<Rightarrow> int" where
"val(C i) s = i" |
"val(V n) s = s n" |
"val(A e1 e2) s = val e1 s + val e2 s"


consts G :: "string set"

consts exec :: "instr \<Rightarrow> rstate \<Rightarrow> rstate"

consts execs :: "instr list \<Rightarrow> rstate \<Rightarrow> rstate"

consts cmp :: "expr \<Rightarrow> nat \<Rightarrow> instr list"

consts maxvar :: "expr \<Rightarrow> nat"


end

Template File

theory Submission
  imports Defs
begin

inductive_set G :: "string set" theorem G_is_replicate:
  assumes "w \<in> G"
  shows "\<exists>n. w = replicate n a @ replicate n b"
  sorry

theorem replicate_G:
  assumes "w = replicate n a @ replicate n b"
  shows "w \<in> G"
  sorry

corollary L_eq_G: "L = G"
  unfolding L_def using G_is_replicate replicate_G by auto


type_synonym rstate = "nat \<Rightarrow> int"

fun exec :: "instr \<Rightarrow> rstate \<Rightarrow> rstate"  where
  "exec _ = undefined"

fun execs :: "instr list \<Rightarrow> rstate \<Rightarrow> rstate"  where
  "execs _ = undefined"

theorem execs_append[simp]: "\<And>s. execs (xs @ ys) s = execs ys (execs xs s)"
  sorry

fun cmp :: "expr \<Rightarrow> nat \<Rightarrow> instr list"  where
  "cmp _ = undefined"

fun maxvar :: "expr \<Rightarrow> nat"  where
  "maxvar _ = undefined"

theorem val_maxvar_same[simp]:
  "\<forall>n \<le> maxvar e. s n = s' n \<Longrightarrow> val e s = val e s'"
  sorry

theorem compiler_correct: "execs (cmp e (maxvar e + 1)) s 0 = val e (s o Suc)"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem G_is_replicate: "(w \<in> G) \<Longrightarrow> \<exists>n. w = replicate n a @ replicate n b"
  by (rule Submission.G_is_replicate)

theorem replicate_G: "(w = replicate n a @ replicate n b) \<Longrightarrow> w \<in> G"
  by (rule Submission.replicate_G)

theorem execs_append: "\<And>s. execs (xs @ ys) s = execs ys (execs xs s)"
  by (rule Submission.execs_append)

theorem val_maxvar_same: "\<forall>n \<le> maxvar e. s n = s' n \<Longrightarrow> val e s = val e s'"
  by (rule Submission.val_maxvar_same)

theorem compiler_correct: "execs (cmp e (maxvar e + 1)) s 0 = val e (s o Suc)"
  by (rule Submission.compiler_correct)

end