Homework 7

Definitions File

theory Defs
  imports "HOL-Library.Extended_Nat"
begin

declare Let_def[simp]
declare [[names_short]]

datatype interval = I nat enat ("[_,_')")
type_synonym intervals = "interval list"

fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
  "inv' k [] = True"
| "inv' k [[l,\<infinity>)] = (k \<le> l)"
| "inv' k ([l,r)#ins) = (k\<le>l \<and> l<r \<and> inv' (Suc r) ins)"
| "inv' _ _ = False"

definition inv where "inv = inv' 0"

consts set_of :: "intervals \<Rightarrow> nat set"

consts list_intvls' :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> interval list"

consts compl' :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"

consts compl :: "intervals \<Rightarrow> intervals"


end

Template File

theory Submission
  imports Defs
begin

value "[1,\<infinity>)"

fun set_of :: "intervals \<Rightarrow> nat set"  where
  "set_of _ = undefined"

lemma "set_of [[4,10), [42,\<infinity>)] = {4..9} \<union> {42..}"
  by (auto simp: numeral_eq_enat)

fun list_intvls' :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> interval list"  where
  "list_intvls' _ = undefined"

definition "list_intervals xs = (case xs of [] \<Rightarrow> [] | (x#xs) \<Rightarrow> list_intvls' x (Suc x) xs)"

lemma list_intvls'_inv[simp]: "sorted (x#xs) \<Longrightarrow> l \<le> x \<Longrightarrow> inv' l (list_intvls' l (Suc x) xs)"
  sorry

theorem list_intervals_inv: "sorted (x#xs) \<Longrightarrow> inv (list_intervals (x#xs))"
  sorry

theorem list_intervals_set: "sorted (x#xs) \<Longrightarrow> set (x#xs) = set_of (list_intervals (x#xs))"
  sorry

fun compl' :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"  where
  "compl' _ = undefined"

definition compl :: "intervals \<Rightarrow> intervals"  where
  "compl _ = undefined"

theorem compl_inv[simp]: "inv is \<Longrightarrow> inv (compl is)"
  sorry

theorem compl_set: "inv is \<Longrightarrow> set_of (compl is) = -set_of is"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma list_intvls'_inv: "sorted (x#xs) \<Longrightarrow> l \<le> x \<Longrightarrow> inv' l (list_intvls' l (Suc x) xs)"
  by (rule Submission.list_intvls'_inv)

theorem list_intervals_inv: "sorted (x#xs) \<Longrightarrow> inv (list_intervals (x#xs))"
  by (rule Submission.list_intervals_inv)

theorem list_intervals_set: "sorted (x#xs) \<Longrightarrow> set (x#xs) = set_of (list_intervals (x#xs))"
  by (rule Submission.list_intervals_set)

theorem compl_inv: "inv is \<Longrightarrow> inv (compl is)"
  by (rule Submission.compl_inv)

theorem compl_set: "inv is \<Longrightarrow> set_of (compl is) = -set_of is"
  by (rule Submission.compl_set)

end