Homework 3

Definitions File

theory Defs imports "HOL-IMP.ASM" begin

inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r  where
  refl:  "star r x x"
| step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"

lemma star_prepend: "\<lbrakk>r x y; star r y z\<rbrakk> \<Longrightarrow> star r x z"
  by (rule step)

lemma star_append: "\<lbrakk> star r x y; r y z \<rbrakk> \<Longrightarrow> star r x z"
  by (induct rule: star.induct) (auto intro: star.intros)

inductive star' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r  where
  refl': "star' r x x"
| step': "\<lbrakk>star' r x y; r y z\<rbrakk> \<Longrightarrow> star' r x z"

lemma star'_prepend: "\<lbrakk>star' r y z; r x y\<rbrakk> \<Longrightarrow> star' r x z"
  apply (induction rule: star'.induct)
   apply (auto intro: star'.intros)
  done

lemma "star r x y = star' r x y"
proof
  assume "star r x y"
  thus "star' r x y"
    by induct (auto intro: star'.intros star'_prepend)
next
  assume "star' r x y"
  thus "star r x y"
    by induct (auto intro: star.intros star_append)
qed

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

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

lemma
  assumes total: "\<forall> x y. T x y \<or> T y x"
    and anti: "\<forall> x y. A x y \<and> A y x \<longrightarrow> x = y"
    and subset: "\<forall> x y. T x y \<longrightarrow> A x y"
  shows "A x y \<longrightarrow> T x y"
proof
  fix x y assume "A x y"
  from total have "T x y \<or> T y x" by simp
  then show "T x y"
  proof
    assume "T x y"
    then show ?thesis .
  next
    assume "T y x"
    with subset have "A y x" by simp
    with \<open>A x y\<close> anti have "x = y" by simp
    with \<open>T y x\<close> show ?thesis by simp
  qed
qed

end

Template File

theory Submission imports Defs begin

fun can_execute :: "nat \<Rightarrow> instr list \<Rightarrow> bool" where
  "can_execute _ = undefined"

theorem can_exec_correct:
  "can_execute (length stk) ins \<Longrightarrow> exec ins s stk \<noteq> None"
  sorry

theorem can_exec_complete:
   "exec ins s stk = Some res \<Longrightarrow> can_execute (length stk) ins"
  sorry

inductive exec1r :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack \<Rightarrow> bool"

inductive execr :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack \<Rightarrow> bool"

theorem step_equiv: "exec1r i s stk stk' \<longleftrightarrow> exec1 i s stk = Some stk'"
  sorry

theorem exec_equiv: "execr ins s stk stk' \<longleftrightarrow> (exec ins s stk = Some stk')"
  sorry

datatype bexp = Var vname | Not bexp | And bexp bexp | Or bexp bexp

type_synonym state = "vname \<Rightarrow> bool"

fun is_var :: "bexp \<Rightarrow> bool" where
  "is_var (Var _) = True"
| "is_var _ = False" where
  "is_var _ = undefined"

fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
  "bval _ = undefined"

inductive is_nnf :: "bexp \<Rightarrow> bool"

fun sub :: "bexp \<Rightarrow> bexp set" where
  "sub _ = undefined"

value "sub (And (Not (Var ''x'')) (Var ''y'')) =
 {
  Var ''x'',
  Var ''y'',
  Not (Var (''x'')),
  And (Not (Var ''x'')) (Var ''y'')
}"

theorem nnf_not: "is_nnf b = (\<forall>b'. Not b' \<in> sub b \<longrightarrow> is_var b')"
  sorry

fun nnf :: "bexp \<Rightarrow> bexp" where
  "nnf _ = undefined"

theorem nnf_sound: "is_nnf (nnf b)"
  sorry

theorem nnf_compl: "bval (nnf b) s = bval b s"
  sorry

end

Check File

theory Check imports Submission begin

theorem can_exec_correct:
  "can_execute (length stk) ins \<Longrightarrow> exec ins s stk \<noteq> None"
  by (rule Submission.can_exec_correct)

theorem can_exec_complete:
   "exec ins s stk = Some res \<Longrightarrow> can_execute (length stk) ins"
  by (rule Submission.can_exec_complete)

theorem step_equiv: "exec1r i s stk stk' \<longleftrightarrow> exec1 i s stk = Some stk'"
  by (rule Submission.step_equiv)

theorem exec_equiv: "execr ins s stk stk' \<longleftrightarrow> (exec ins s stk = Some stk')"
  by (rule Submission.exec_equiv)

theorem nnf_not: "is_nnf b = (\<forall>b'. Not b' \<in> sub b \<longrightarrow> is_var b')"
  by (rule Submission.nnf_not)

theorem nnf_sound: "is_nnf (nnf b)"
  by (rule Submission.nnf_sound)

theorem nnf_compl: "bval (nnf b) s = bval b s"
  by (rule Submission.nnf_compl)

end