Week 13 homework

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