Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 03

This is the homework corresponding to exercise sheet 03.

## Resources

### 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>" |
"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```

Terms and Conditions