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 3

This is the task corresponding to homework 3.

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.AExp"
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])"

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)"

type_synonym reg = nat

datatype op = REG reg | VAL val

datatype instr =
LD reg vname

datatype v_or_reg = Var vname | Reg reg

type_synonym mstate = "v_or_reg \<Rightarrow> int"

definition "is_N a = (case a of N _ \<Rightarrow> True | _ \<Rightarrow> False)"

fun num_add :: "instr list \<Rightarrow> nat" where
| "num_add (x#xs) = (case x of (ADD _ _ _) \<Rightarrow> 1 | _ \<Rightarrow> 0) + num_add xs"

by (induct xs) auto

fun num_plus :: "aexp \<Rightarrow> nat" where
"num_plus (Plus a1 a2) = 1 + num_plus a1 + num_plus a2"
| "num_plus _ = 0"

consts T :: "paren list \<Rightarrow> bool"

consts op_val :: "op \<Rightarrow> mstate \<Rightarrow> int"

consts exec1 :: "instr \<Rightarrow> mstate \<Rightarrow> mstate"

consts exec :: "instr list \<Rightarrow> mstate \<Rightarrow> mstate"

consts cmp :: "aexp \<Rightarrow> reg \<Rightarrow> instr list"

end```

### Template File

```theory Submission
imports Defs
begin

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

inductive T :: "paren list \<Rightarrow> bool"

lemma example: "T [Open, Open]"
sorry

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

fun op_val :: "op \<Rightarrow> mstate \<Rightarrow> int"  where
"op_val _ = undefined"

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

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

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

theorem cmp_len: "\<not>is_N a \<Longrightarrow> num_add (cmp a r) \<le> num_plus a"
sorry

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

theorem cmp_correct: "exec (cmp a r) \<sigma> (Reg r) = aval a (\<sigma> o Var)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

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

lemma example: "T [Open, Open]"
by (rule Submission.example)

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_len: "\<not>is_N a \<Longrightarrow> num_add (cmp a r) \<le> num_plus a"
by (rule Submission.cmp_len)

theorem cmp_correct: "exec (cmp a r) \<sigma> (Reg r) = aval a (\<sigma> o Var)"
by (rule Submission.cmp_correct)

end```

Terms and Conditions