Homework 03

Definitions File

theory Defs
imports "HOL-IMP.ASM"
begin

text \<open>The \<open>count\<close> function from sheet 1.\<close>
fun count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
"count [] _ = 0" |
"count (x # xs) y = (if x = y then Suc (count xs y) else count xs y)"

end

Template File

theory Submission
  imports Defs
begin

datatype paren = Open | Close

inductive S where
  S_empty: "S []" |
  S_append: "S xs \<Longrightarrow> S ys \<Longrightarrow> S (xs @ ys)" |
  S_paren: "S xs \<Longrightarrow> S (Open # xs @ [Close])"

theorem S_T:
  "S xs \<Longrightarrow> T xs"
  sorry

theorem T_S:
  "T xs \<Longrightarrow> count xs Open = count xs Close \<Longrightarrow> S xs"
  sorry


type_synonym reg = nat

datatype op = REG reg | VAL int \<comment> \<open>An operand is either a register or a constant.\<close>

datatype instr =
  LD reg vname \<comment> \<open>Load a variable value in a register.\<close>
| ADD reg op op \<comment> \<open>Add the contents of the two operands, placing the result in the register.\<close>

datatype v_or_reg = Var vname | Reg reg
type_synonym mstate = "v_or_reg \<Rightarrow> int"

fun op_val :: "op \<Rightarrow> mstate \<Rightarrow> int" where
  "op_val (REG r) \<sigma> = \<sigma> (Reg r)" |
  "op_val (VAL n) _ = n"

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

fun execs :: "instr list \<Rightarrow> mstate \<Rightarrow> mstate" where
  "execs [] \<sigma> = \<sigma>" |
\<comment> \<open>Add recursive case here\<close>
  "execs _ _ = undefined"

fun cmp :: "aexp \<Rightarrow> reg \<Rightarrow> op \<times> instr list" where
  "cmp _ _ = undefined"

lemma [simp]: "s (Reg r := x) o Var = s o Var"
  by auto

theorem cmp_correct: "cmp a r = (x, prog) \<Longrightarrow>
  op_val x (execs prog \<sigma>) = aval a (\<sigma> o Var) \<and> execs prog \<sigma> o Var = \<sigma> o Var"
\<comment> \<open>The first conjunct states that the resulting operand contains the correct value,
    and the second conjunct states that the variable state is unchanged.\<close>
  sorry


definition
  "ex_split P xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ zs \<and> P ys zs)"

fun has_split where
  "has_split _ _ _ = undefined"

theorem ex_split_has_split[code]:
  "ex_split P xs \<longleftrightarrow> has_split P [] xs"
  sorry

definition
  "ex_balanced_sum xs = (\<exists>ys zs. sum_list ys = sum_list zs \<and> xs = ys @ zs \<and> ys \<noteq> [] \<and> zs \<noteq> [])"

value "ex_balanced_sum [1,2,3,3,2,1::nat]"

definition
  "linear_split (xs :: int list) \<equiv> (undefined :: bool)"

theorem linear_correct:
  "linear_split xs \<longleftrightarrow> ex_balanced_sum xs"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem S_T:
  "S xs \<Longrightarrow> T xs"
  by (rule Submission.S_T)

theorem T_S:
  "T xs \<Longrightarrow> count xs Open = count xs Close \<Longrightarrow> S xs"
  by (rule Submission.T_S)

theorem cmp_correct: "cmp a r = (x, prog) \<Longrightarrow>
  op_val x (execs prog \<sigma>) = aval a (\<sigma> o Var) \<and> execs prog \<sigma> o Var = \<sigma> o Var"
\<comment> \<open>The first conjunct states that the resulting operand contains the correct value,
    and the second conjunct states that the variable state is unchanged.\<close>
  by (rule Submission.cmp_correct)

theorem ex_split_has_split[code]:
  "ex_split P xs \<longleftrightarrow> has_split P [] xs"
  by (rule Submission.ex_split_has_split)

theorem linear_correct:
  "linear_split xs \<longleftrightarrow> ex_balanced_sum xs"
  by (rule Submission.linear_correct)

end