Cookies disclaimer

I agree 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 12

This is the task corresponding to homework 12.

Resources

Download Files

Definitions File

theory Defs
  imports Main
begin

declare [[names_short]]

end

Template File

theory Submission
  imports Defs
begin

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

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 = undefined"

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)

theorem inc_dec_seq_lbound: "length (oplist 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 inc_dec_seq_ubound)

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

end

end

Terms and Conditions