Homework 13

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