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.

Sparse Binary Numbers

This is the task corresponding to exercise 2. Sparse Binary Numbers.

Resources

Definitions File

theory Defs
imports Main
begin

declare [[names_short]]

type_synonym rank = nat
type_synonym snat = "rank list"

abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> sorted_wrt (<) s"
definition \<alpha> :: "snat \<Rightarrow> nat" where "\<alpha> s = (\<Sum>i\<leftarrow>s. 2^i)"

lemma \<alpha>_Nil[simp]: "\<alpha> [] = 0"
unfolding \<alpha>_def by auto

lemma \<alpha>_Cons[simp]: "\<alpha> (r#rs) = 2^r + \<alpha> rs"
unfolding \<alpha>_def by auto

lemma \<alpha>_append[simp]: "\<alpha> (rs\<^sub>1@rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
unfolding \<alpha>_def by auto

end

Template File

theory Submission
imports Defs
begin

lemma SBN_upper_bound:
assumes "invar s"
assumes "\<forall>r\<in>set s. r<K"
shows "\<alpha> s < 2^K"
sorry

lemma SBN_unique:
assumes "invar s\<^sub>1" "invar s\<^sub>2" "\<alpha> s\<^sub>1 = \<alpha> s\<^sub>2"
shows "s\<^sub>1 = s\<^sub>2"
sorry

end

Check File

theory Check
imports Submission
begin

lemma SBN_upper_bound:
assumes "invar s"
assumes "\<forall>r\<in>set s. r<K"
shows "\<alpha> s < 2^K"
using assms by (rule Submission.SBN_upper_bound)

lemma SBN_unique:
assumes "invar s\<^sub>1" "invar s\<^sub>2" "\<alpha> s\<^sub>1 = \<alpha> s\<^sub>2"
shows "s\<^sub>1 = s\<^sub>2"
using assms by (rule Submission.SBN_unique)

end

Terms and Conditions