Theory Sequence_Toolkit

section ‹ Sequence Toolkit ›

theory Sequence_Toolkit
  imports Number_Toolkit
begin

subsection ‹ Conversion ›

text ‹ We define a number of coercions for mapping a list to finite function. ›

abbreviation rel_of_list :: "'a list ⇒ nat ↔ 'a" ("[_]⇩s") where
"rel_of_list xs ≡ [list_pfun xs]⇩⇸"

abbreviation seq_nth ("_'(_')⇩s" [999,0] 999) where
"seq_nth xs i ≡ xs ! (i - 1)"

declare [[coercion list_ffun]]
declare [[coercion list_pfun]]
declare [[coercion rel_of_list]]
declare [[coercion seq_nth]]

subsection ‹ Number range›

lemma number_range: "{i..j} = {k :: ℤ. i ≤ k ∧ k ≤ j}"
  by (auto)

text ‹ The number range from $i$ to $j$ is the set of all integers greater than or equal to $i$, 
  which are also less than or equal to $j$.›

subsection ‹ Iteration ›

definition iter :: "ℤ ⇒ ('X ↔ 'X) ⇒ ('X ↔ 'X)" where
"iter n R = (if (n ≥ 0) then R ^^ (nat n) else (R⇧∼) ^^ (nat n))"

lemma iter_eqs:
  "iter 0 r = Id"
  "n ≥ 0 ⟹ iter (n + 1) r = r ❙; (iter n r)"
  "n < 0 ⟹ iter (n + 1) r = iter n (r⇧∼)"
  by (simp_all add: iter_def, metis Suc_nat_eq_nat_zadd1 add.commute relpow.simps(2) relpow_commute)

subsection ‹ Number of members of a set ›

lemma size_rel_of_list: 
  "#xs = length xs" 
  by simp

subsection ‹ Minimum ›

text ‹ Implemented by the function @{const Min}. ›

subsection ‹ Maximum ›

text ‹ Implemented by the function @{const Max}. ›

subsection ‹ Finite sequences ›

definition "seq A = lists A"

lemma seq_iff [simp]: "xs ∈ seq A ⟷ set xs ⊆ A"
  by (simp add: in_lists_conv_set seq_def subset_code(1))
  
lemma seq_ffun_set: "range list_ffun = {f :: ℕ ⇻ 'X. dom(f) = {1..#f}}"
  by (simp add: range_list_ffun, force)

subsection ‹ Non-empty finite sequences ›

definition "seq⇩1 A = seq A - {[]}"

lemma seq⇩1_iff [simp]: "xs ∈ seq⇩1(A) ⟷ (xs ∈ seq A ∧ #xs > 0)"
  by (simp add: seq⇩1_def)

subsection ‹ Injective sequences ›

definition "iseq A = seq A ∩ Collect distinct"

lemma iseq_iff [simp]: "xs ∈ iseq(A) ⟷ (xs ∈ seq A ∧ distinct xs)"
  by (simp add: iseq_def)

subsection ‹ Bounded sequences ›

definition bseq :: "ℕ ⇒ 'a set ⇒ 'a list set" ("bseq[_]") where
"bseq n A = bounded_lists n A"

(* Proof that this corresponds to the Z definition required *)

subsection ‹ Sequence brackets ›

text ‹ Provided by the HOL list notation @{term "[x, y, z]"}. ›

subsection ‹ Concatenation ›

text ‹ Provided by the HOL concatenation operator @{term "(@)"}. ›

subsection ‹ Reverse ›

text ‹ Provided by the HOL function @{const rev}. ›

subsection ‹ Head of a sequence ›

definition head :: "'a list ⇸ 'a" where
"head = (λ xs :: 'a list | #xs > 0 ∙ hd xs)"

lemma dom_head: "dom head = {xs. #xs > 0}"
  by (simp add: head_def)

lemma head_app: "#xs > 0 ⟹ head xs = hd xs"
  by (simp add: head_def)

lemma head_z_def: "xs ∈ seq⇩1(A) ⟹ head xs = xs 1"
  by (simp add: hd_conv_nth head_app seq⇩1_def)

subsection ‹ Last of a sequence ›

definition slast :: "'a list ⇸ 'a" where
"slast = (λ xs :: 'a list | #xs > 0 ∙ List.last xs)"

lemma dom_last: "dom slast = {xs. #xs > 0}"
  by (simp add: slast_def)

lemma slast_app: "#xs > 0 ⟹ slast xs = last xs"
  by (simp add: slast_def)

lemma slast_eq: "#s > 0 ⟹ last s = s (#s)"
  by (simp add: slast_app last_conv_nth)

subsection ‹ Tail of a sequence ›

definition tail :: "'a list ⇸ 'a list" where
"tail = (λ xs :: 'a list | #xs > 0 ∙ tl xs)"

lemma dom_tail: "dom tail = {xs. #xs > 0}"
  by (simp add: tail_def)

lemma tail_app: "#xs > 0 ⟹ tail xs = tl xs"
  by (simp add: tail_def)

subsection ‹ Domain ›

definition dom_seq :: "'a list ⇒ ℕ set" where
[simp]: "dom_seq xs = {0..<#xs}"

adhoc_overloading dom ⇌ dom_seq

subsection ‹ Range ›

definition ran_seq :: "'a list ⇒ 'a set" where
[simp]: "ran_seq xs = set xs"

adhoc_overloading ran ⇌ ran_seq

subsection ‹ Filter ›

notation seq_filter (infix "↾" 80)

lemma seq_filter_Nil: "[] ↾ V = []" by simp

lemma seq_filter_append: "(s @ t) ↾ V = (s ↾ V) @ (t ↾ V)" 
  by (simp add: seq_filter_append)

lemma seq_filter_subset_iff: "ran s ⊆ V ⟷ (s ↾ V = s)"
  by (auto simp add: seq_filter_def subsetD, meson filter_id_conv)

lemma seq_filter_empty: "s ↾ {} = []" by simp

lemma seq_filter_size: "#(s ↾ V) ≤ #s"
  by (simp add: seq_filter_def)

lemma seq_filter_twice: "(s ↾ V) ↾ W = s ↾ (V ∩ W)" by simp

subsection ‹ Examples ›

lemma "([1,2,3] ❙; (λ x ∙ x + 1)) 1 = 2"
  by (simp add: pfun_graph_comp[THEN sym] list_pfun_def pcomp_pabs)

end