Theory Bounded_List

section ‹ Bounded Lists ›

theory Bounded_List
  imports "List_Extra" "HOL-Library.Numeral_Type"
begin

text ‹ The term @{term "CARD('n)"} retrieves the cardinality of a finite type @{typ 'n}. Examples
  include the types @{typ 1}, @{typ 2} and @{typ 3}.›

typedef ('a, 'n::finite) blist = "{xs :: 'a list. length xs ≤ CARD('n)}"
  morphisms list_of_blist blist_of_list
proof 
  show "[] ∈ {xs. length xs ≤ CARD('n)}"
    by simp
qed

declare list_of_blist_inverse [simp]

syntax "_blist" :: "type ⇒ type ⇒ type" ("_ blist[_]" [100, 0] 100)
translations (type) "'a blist['n]" == (type) "('a, 'n) blist"

text ‹ We construct various functions using the lifting package to lift corresponding list functions. ›

setup_lifting type_definition_blist

lift_definition blength :: "'a blist['n::finite] ⇒ nat" is length .

lift_definition bnth :: "'a blist['n::finite] ⇒ nat ⇒ 'a" is nth .

lift_definition bappend :: "'a blist['m::finite] ⇒ 'a blist['n::finite] ⇒ 'a blist['m + 'n]" (infixr "@⇩s" 65) is append
  by auto

lift_definition bmake :: "'n itself ⇒ 'a list ⇒ 'a blist['n::finite]" is "λ _. take CARD('n)"
  by auto

code_datatype bmake

lemma bmake_length_card:
  "blength (bmake TYPE('n::finite) xs) = (if length xs ≤ CARD('n) then length xs else CARD('n))"
  by (simp add: blength_def bmake_def, auto simp add: blist_of_list_inverse)

lemma blist_always_bounded:
  "length (list_of_blist (bl::'a blist['n::finite])) ≤ CARD('n)"
  using list_of_blist by blast

lemma blist_remove_head:
  fixes bl :: "'a blist['n::finite]"
  assumes "blength bl > 0"
  shows "blength (bmake TYPE('n::finite) (tl (list_of_blist (bl::'a blist['n::finite])))) < blength bl"
  by (metis One_nat_def Suc_pred assms blength.rep_eq bmake_length_card length_tl less_Suc_eq_le linear)

text ‹ This proof is performed by transfer ›

lemma bappend_bmake [code]: 
  "bmake TYPE('a::finite) xs @⇩s bmake TYPE('b::finite) ys 
    = bmake TYPE('a + 'b) (take CARD('a) xs @ take CARD('b) ys)"
  by (transfer, simp)

instantiation blist :: (type, finite) equal
begin

definition equal_blist :: "'a blist['b] ⇒ 'a blist['b] ⇒ bool" where
"equal_blist m1 m2 ⟷ (list_of_blist m1 = list_of_blist m2)"

instance proof 
  fix x y :: "'a blist['b]"
  show "equal_class.equal x y = (x = y)"
    by (simp add: equal_blist_def, transfer, simp)
qed

end

lemma list_of_blist_code [code]:
  "list_of_blist (bmake TYPE('n::finite) xs) = take CARD('n) xs"
  by (transfer, simp)+

definition blists :: "'n::finite itself ⇒ 'a list ⇒ ('a blist['n]) list" where
"blists n xs = map blist_of_list (b_lists CARD('n) xs)"

lemma n_blists_as_b_lists:
  fixes n::"'n::finite itself"
  shows "map list_of_blist (blists n xs) = b_lists CARD('n) xs" (is "?lhs = ?rhs")
proof -
  have "?lhs = map (list_of_blist ∘ (blist_of_list :: _ ⇒ _ blist['n])) (b_lists CARD('n) xs)"
    by (simp add: blists_def)
  also have "... = map id (b_lists CARD('n) xs)"
    by (rule map_cong, auto simp add: blist_of_list_inverse length_b_lists_elem)
  also have "... = b_lists CARD('n) xs"
    by simp
  finally show ?thesis .
qed

lemma set_blists_enum_UNIV: "set (blists TYPE('n::finite) (enum_class.enum ::'a::enum list)) = UNIV"
proof -
  have "⋀x:: 'a blist['n]. list_of_blist x ∈ set (b_lists CARD('n) enum_class.enum)"
  proof (rule in_blistsI)
    fix x::"'a blist['n]"
    show "length (list_of_blist x) ≤ CARD('n)"
      by (simp add: blist_always_bounded)
    show "list_of_blist x ∈ lists (set enum_class.enum)"
      by (auto simp add: lists_eq_set enum_UNIV)
  qed
  thus ?thesis
    by (force simp add: blists_def image_iff)
qed

lemma distinct_blists: "distinct xs ⟹ distinct (blists n xs)"
  by (metis distinct_b_lists distinct_map n_blists_as_b_lists)

definition all_blists :: "(('a::enum) blist['n::finite] ⇒ bool) ⇒ bool"
where
  "all_blists P ⟷ (∀xs ∈ set (blists TYPE('n) Enum.enum). P xs)"

definition ex_blists :: "(('a :: enum) blist['n::finite] ⇒ bool) ⇒ bool"
where
  "ex_blists P ⟷ (∃xs ∈ set (blists TYPE('n) Enum.enum). P xs)"

instantiation blist :: (enum, finite) enum
begin

definition enum_blist :: "('a blist['b]) list" where
"enum_blist = blists TYPE('b) Enum.enum"

definition enum_all_blist :: "('a blist['b] ⇒ bool) ⇒ bool" where
"enum_all_blist P = all_blists P"

definition enum_ex_blist :: "('a blist['b] ⇒ bool) ⇒ bool" where
"enum_ex_blist P = ex_blists P"

instance 
  by (intro_classes)
     (simp_all add: enum_blist_def set_blists_enum_UNIV distinct_blists enum_distinct enum_all_blist_def enum_ex_blist_def all_blists_def ex_blists_def)

end
  
end