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 13

This is the task corresponding to homework 13.

Resources

Definitions File

```theory Defs
imports Main
begin

declare [[names_short]]

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

fun T_incr :: "bool list \<Rightarrow> nat" where
"T_incr [] = 0" |
"T_incr (False#bs) = 1" |
"T_incr (True#bs) = T_incr 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]: "1 \<le> k"
begin

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

datatype op = Decr | Incr

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

fun T_exec1::"op \<Rightarrow> (bool list \<Rightarrow> nat)" where
"T_exec1 Incr = T_incr" |
"T_exec1 Decr = T_decr"

fun T_exec :: "op list \<Rightarrow> bool list \<Rightarrow> nat" where
"T_exec [] bs = 0" |
"T_exec (op # ops) bs = (T_exec1 op bs + T_exec ops (exec1 op bs))"

lemma induct_list012[case_names empty single multi]:
"P [] \<Longrightarrow> (\<And>x. P [x]) \<Longrightarrow> (\<And>x y xs. P xs \<Longrightarrow> P (x#y#xs)) \<Longrightarrow> P xs"
by (rule List.induct_list012)

lemma case_nat012[case_names zero one two]:
"\<lbrakk>n = 0 \<Longrightarrow> P; n = 1 \<Longrightarrow> P; \<And>n'. n = Suc (Suc n') \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (metis One_nat_def nat.exhaust)

end

consts oplist :: "nat \<Rightarrow> counter_with_decr.op list"

end```

Template File

```theory Submission
imports Defs
begin

context counter_with_decr begin

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

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

definition bs0 where
"bs0 \<equiv> undefined"

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

end

end
```

Check File

```theory Check
imports Submission
begin

context counter_with_decr begin

theorem inc_dec_seq_ubound: "length bs = k \<Longrightarrow> T_exec ops bs \<le> (length ops) * length bs"
by (rule Submission.inc_dec_seq_ubound)

theorem inc_dec_seq_lbound: "n * k \<le> 2 * (T_exec (oplist n) bs0)"
by (rule Submission.inc_dec_seq_lbound)

end

end```

Terms and Conditions