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.

# Week 13 homework

FDS Week 13 homework

## Resources

### Definitions File

```(*<*)
theory Defs
imports Main
begin
(*>*)

fun incr :: "bool list \<Rightarrow> bool list" where
"incr [] = []" |
"incr (False#bs) = True # bs" |
"incr (True#bs) = False # incr bs"

fun tincr :: "bool list \<Rightarrow> nat" where
"tincr [] = 0" |
"tincr (False#bs) = 1" |
"tincr (True#bs) = tincr bs + 1"

locale counter_with_decr =
fixes decr::"bool list \<Rightarrow> bool list" and k::"nat"
assumes
decr[simp]: "decr ((replicate (k-(Suc 0)) False) @ [True]) =
(replicate (k-(Suc 0)) True) @ [False]" and
decr_len_eq[simp]: "length (decr bs) = length bs" and
k[simp]: "Suc 0 \<le> k"
begin

fun tdecr::"bool list \<Rightarrow> nat" where
"tdecr _ = 1"

datatype op = Decr | Incr

fun t_op::"op \<Rightarrow> (bool list \<Rightarrow> nat)" where
"t_op Incr = tincr" |
"t_op Decr = tdecr"

fun exec_op::"op \<Rightarrow> (bool list \<Rightarrow> bool list)" where
"exec_op Incr = incr" |
"exec_op Decr = decr"

fun exec_time :: "op list \<Rightarrow> bool list \<Rightarrow> nat" where
"exec_time [] bs = 0" |
"exec_time (op # ops) bs = (t_op op bs + exec_time ops (exec_op op bs))"

end

end```

### Template File

```theory Submission
imports Defs
begin

context counter_with_decr
begin

lemma inc_dec_seq_ubound: "length bs = k \<Longrightarrow> exec_time ops bs \<le> (length ops) * length bs"
sorry

fun oplist:: "nat \<Rightarrow> op list" where
"oplist _ = undefined"

lemma len_oplist: "length (oplist n) = n"
sorry

definition bs0 where
"bs0 = undefined"

lemma "length bs0 = k"
sorry

lemma inc_dec_seq_lbound: "n * k \<le> 2 * (exec_time (oplist n) bs0)"
sorry

end

end```

### Check File

```theory Check
imports "Submission"
begin

context counter_with_decr
begin

lemma inc_dec_seq_ubound: "length bs = k \<Longrightarrow> exec_time ops bs \<le> (length ops) * length bs"
by(rule inc_dec_seq_ubound)

lemma len_oplist: "length (oplist n) = n"
by(rule len_oplist)

lemma inc_dec_seq_lbound: "n * k \<le> 2 * (exec_time (oplist n) bs0)"
by(rule inc_dec_seq_lbound)

end

end```

Terms and Conditions