Homework 03

Definitions File

theory Defs
  imports Main
begin

abbreviation a where "a ≡ CHR ''a''"
abbreviation b where "b ≡ CHR ''b''"

definition
  "L = {w. ∃n. w = replicate n a @ replicate n b}"



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

type_synonym rstate = "nat ⇒ int"

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

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

end

Template File

theory Submission
  imports Defs
begin

inductive_set G :: "string set"

theorem G_is_replicate:
  "w ∈ G ⟹ ∃n. w = replicate n a @ replicate n b"
  sorry

theorem replicate_G:
  "w = replicate n a @ replicate n b ⟹ w ∈ G"
  sorry

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



fun exec :: "instr ⇒ rstate ⇒ rstate" where
  "exec _ _ = undefined"

fun execs :: "instr list ⇒ rstate ⇒ rstate" where
  "execs _ _= undefined"

theorem execs_append[simp]: "⋀s. execs (xs @ ys) s = execs ys (execs xs s)"
  sorry

fun cmp :: "expr ⇒ nat ⇒ instr list" where
  "cmp _ _ = undefined"

fun maxvar :: "expr ⇒ nat" where
  "maxvar _ = undefined"

theorem val_maxvar_same[simp]:
  "ALL n <= maxvar e. s n = s' n ⟹ 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:
  assumes "w ∈ G"
  shows "∃n. w = replicate n a @ replicate n b"
  using assms by (rule Submission.G_is_replicate)

theorem replicate_G:
  assumes "w = replicate n a @ replicate n b"
  shows "w ∈ G"
  using assms by (rule Submission.replicate_G)

theorem execs_append: "⋀s. execs (xs @ ys) s = execs ys (execs xs s)"
  by (rule Submission.execs_append)

theorem val_maxvar_same:
  "ALL n <= maxvar e. s n = s' n ⟹ 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