Theory Infinite_Sequence

section ‹ Infinite Sequences ›

theory Infinite_Sequence
imports
  HOL.Real
  List_Extra
  "HOL-Library.Sublist"
  "HOL-Library.Nat_Bijection"
begin

typedef 'a infseq = "UNIV :: (nat ⇒ 'a) set"
  by (auto)

setup_lifting type_definition_infseq

definition ssubstr :: "nat ⇒ nat ⇒ 'a infseq ⇒ 'a list" where
"ssubstr i j xs = map (Rep_infseq xs) [i ..< j]"

lift_definition nth_infseq :: "'a infseq ⇒ nat ⇒ 'a" (infixl "!⇩s" 100)
is "λ f i. f i" .

abbreviation sinit :: "nat ⇒ 'a infseq ⇒ 'a list" where
"sinit i xs ≡ ssubstr 0 i xs"

lemma sinit_len [simp]:
  "length (sinit i xs) = i"
  by (simp add: ssubstr_def)

lemma sinit_0 [simp]: "sinit 0 xs = []"
  by (simp add: ssubstr_def)

lemma prefix_upt_0 [intro]:
  "i ≤ j ⟹ prefix [0..<i] [0..<j]"
  by (induct i, simp, metis append_prefixD le0 prefix_order.lift_Suc_mono_le prefix_order.order_refl upt_Suc)

lemma sinit_prefix:
  "i ≤ j ⟹ prefix (sinit i xs) (sinit j xs)"
  by (simp add: map_mono_prefix prefix_upt_0 ssubstr_def)

lemma sinit_strict_prefix:
  "i < j ⟹ strict_prefix (sinit i xs) (sinit j xs)"
  by (metis sinit_len sinit_prefix le_less nat_neq_iff prefix_order.dual_order.strict_iff_order)

lemma nth_sinit:
  "i < n ⟹ sinit n xs ! i = xs !⇩s i"
  apply (unfold ssubstr_def)
  apply (transfer, auto)
  done

lemma sinit_append_split:
  assumes "i < j"
  shows "sinit j xs = sinit i xs @ ssubstr i j xs"
proof -
  have "[0..<i] @ [i..<j] = [0..<j]"
    by (metis assms le0 le_add_diff_inverse le_less upt_add_eq_append)
  thus ?thesis
    by (simp add: ssubstr_def, transfer, simp add: map_append[THEN sym])
qed

lemma sinit_linear_asym_lemma1:
  assumes "asym R" "i < j" "(sinit i xs, sinit i ys) ∈ lexord R" "(sinit j ys, sinit j xs) ∈ lexord R"
  shows False
proof -
  have sinit_xs: "sinit j xs = sinit i xs @ ssubstr i j xs"
    by (metis assms(2) sinit_append_split)
  have sinit_ys: "sinit j ys = sinit i ys @ ssubstr i j ys"
    by (metis assms(2) sinit_append_split)
  from sinit_xs sinit_ys assms(4)
  have "(sinit i ys, sinit i xs) ∈ lexord R ∨ (sinit i ys = sinit i xs ∧ (ssubstr i j ys, ssubstr i j xs) ∈ lexord R)"
    by (auto dest: lexord_append)
  with assms lexord_asymmetric show False
    by (force)
qed

lemma sinit_linear_asym_lemma2:
  assumes "asym R" "(sinit i xs, sinit i ys) ∈ lexord R" "(sinit j ys, sinit j xs) ∈ lexord R"
  shows False
proof (cases i j rule: linorder_cases)
  case less with assms show ?thesis
    by (auto dest: sinit_linear_asym_lemma1)
next
  case equal with assms show ?thesis
    by (simp add: lexord_asymmetric)
next
  case greater with assms show ?thesis
    by (auto dest: sinit_linear_asym_lemma1)
qed

lemma range_ext:
  assumes "∀i :: nat. ∀x∈{0..<i}. f(x) = g(x)"
  shows "f = g"
proof (rule ext)
  fix x :: nat
  obtain i :: nat where "i > x"
    by (metis lessI)
  with assms show "f(x) = g(x)"
    by (auto)
qed

lemma sinit_ext:
  "(∀ i. sinit i xs = sinit i ys) ⟹ xs = ys"
  by (simp add: ssubstr_def, transfer, auto intro: range_ext)

definition infseq_lexord :: "'a rel ⇒ ('a infseq) rel" where
"infseq_lexord R = {(xs, ys). (∃ i. (sinit i xs, sinit i ys) ∈ lexord R)}"

lemma infseq_lexord_irreflexive:
  "∀x. (x, x) ∉ R ⟹ (xs, xs) ∉ infseq_lexord R"
  by (auto dest: lexord_irreflexive simp add: irrefl_def infseq_lexord_def)

lemma infseq_lexord_irrefl:
  "irrefl R ⟹ irrefl (infseq_lexord R)"
  by (simp add: irrefl_def infseq_lexord_irreflexive)

lemma infseq_lexord_transitive:
  assumes "trans R"
  shows "trans (infseq_lexord R)"
unfolding infseq_lexord_def
proof (rule transI, clarify)
  fix xs ys zs :: "'a infseq" and m n :: nat
  assume las: "(sinit m xs, sinit m ys) ∈ lexord R" "(sinit n ys, sinit n zs) ∈ lexord R"
  hence inz: "m > 0"
    using gr0I by force
  from las(1) obtain i where sinitm: "(sinit m xs!i, sinit m ys!i) ∈ R" "i < m" "∀ j<i. sinit m xs!j = sinit m ys!j"
    using lexord_eq_length by force
  from las(2) obtain j where sinitn: "(sinit n ys!j, sinit n zs!j) ∈ R" "j < n" "∀ k<j. sinit n ys!k = sinit n zs!k"
    using lexord_eq_length by force
  show "∃i. (sinit i xs, sinit i zs) ∈ lexord R"
  proof (cases "i ≤ j")
    case True note lt = this
    with sinitm sinitn have "(sinit n xs!i, sinit n zs!i) ∈ R"
      by (metis assms le_eq_less_or_eq le_less_trans nth_sinit transD)
    moreover from lt sinitm sinitn have "∀ j<i. sinit m xs!j = sinit m zs!j"
      by (metis less_le_trans less_trans nth_sinit)
    ultimately have "(sinit n xs, sinit n zs) ∈ lexord R"
      by (metis assms las(1,2) lexord_append lexord_sufI lexord_trans linorder_le_cases
          linorder_less_linear sinit_append_split sinit_len)
    thus ?thesis by auto
  next
    case False
    then have ge: "i > j" by auto
    with assms sinitm sinitn have "(sinit n xs!j, sinit n zs!j) ∈ R"
      by (metis less_trans nth_sinit)
    moreover from ge sinitm sinitn have "∀ k<j. sinit m xs!k = sinit m zs!k"
      by (metis dual_order.strict_trans nth_sinit)
    moreover hence "∀k<j. sinit n xs ! k = sinit n zs ! k"
      by (metis dual_order.strict_trans ge nth_sinit sinitm(2) sinitn(2))
    ultimately have "(sinit n xs, sinit n zs) ∈ lexord R"
      by (metis lexord_intro_elems sinit_len sinitn(2))
    thus ?thesis by auto
  qed
qed

lemma infseq_lexord_trans:
  "⟦ (xs, ys) ∈ infseq_lexord R; (ys, zs) ∈ infseq_lexord R; trans R ⟧ ⟹ (xs, zs) ∈ infseq_lexord R"
  by (meson infseq_lexord_transitive transE)

lemma infseq_lexord_antisym:
  "⟦ asym R; (a, b) ∈ infseq_lexord R ⟧ ⟹ (b, a) ∉ infseq_lexord R"
  by (auto dest: sinit_linear_asym_lemma2 simp add: infseq_lexord_def)

lemma infseq_lexord_asym:
  assumes "asym R"
  shows "asym (infseq_lexord R)"
  by (simp add: assms asym_onI infseq_lexord_antisym)

lemma infseq_lexord_total:
  assumes "total R"
  shows "total (infseq_lexord R)"
  using assms by (simp add: total_on_def infseq_lexord_def, meson lexord_linear sinit_ext)

lemma infseq_lexord_strict_linear_order:
  assumes "strict_linear_order R"
  shows "strict_linear_order (infseq_lexord R)"
  using assms
  by (auto simp add: strict_linear_order_on_def partial_order_on_def preorder_on_def
           intro: infseq_lexord_transitive infseq_lexord_irrefl infseq_lexord_total)

lemma infseq_lexord_linear:
  assumes "(∀ a b. (a,b)∈ R ∨ a = b ∨ (b,a) ∈ R)"
  shows "(x,y) ∈ infseq_lexord R ∨ x = y ∨ (y,x) ∈ infseq_lexord R"
proof -
  have "total R"
    using assms total_on_def by blast
  hence "total (infseq_lexord R)"
    using infseq_lexord_total by blast
  thus ?thesis
    by (auto simp add: total_on_def)
qed

instantiation infseq :: (ord) ord
begin

definition less_infseq :: "'a infseq ⇒ 'a infseq ⇒ bool" where
"less_infseq xs ys ⟷ (xs, ys) ∈ infseq_lexord {(xs, ys). xs < ys}"

definition less_eq_infseq :: "'a infseq ⇒ 'a infseq ⇒ bool" where
"less_eq_infseq xs ys = (xs = ys ∨ xs < ys)"

instance ..

end

instance infseq :: (order) order
proof
  fix xs :: "'a infseq"
  show "xs ≤ xs" by (simp add: less_eq_infseq_def)
next
  fix xs ys zs :: "'a infseq"
  assume "xs ≤ ys" and "ys ≤ zs"
  then show "xs ≤ zs"
    by (force dest: infseq_lexord_trans simp add: less_eq_infseq_def less_infseq_def trans_def)
next
  fix xs ys :: "'a infseq"
  assume "xs ≤ ys" and "ys ≤ xs"
  then show "xs = ys"
    apply (simp_all add: less_eq_infseq_def less_infseq_def)
    apply safe
    apply (metis asym_onI case_prodD infseq_lexord_antisym mem_Collect_eq order_less_asym)
    done
next
  fix xs ys :: "'a infseq"
  show "xs < ys ⟷ xs ≤ ys ∧ ¬ ys ≤ xs"
    apply (simp_all add: less_infseq_def less_eq_infseq_def)
    apply safe
     apply (simp_all add: infseq_lexord_irreflexive)
    apply (metis asym_onI case_prodD infseq_lexord_antisym mem_Collect_eq order_less_imp_not_less)
    done
qed

instance infseq :: (linorder) linorder
proof
  fix xs ys :: "'a infseq"
  have "(xs, ys) ∈ infseq_lexord {(u, v). u < v} ∨ xs = ys ∨ (ys, xs) ∈ infseq_lexord {(u, v). u < v}"
    by (rule infseq_lexord_linear) auto
  then show "xs ≤ ys ∨ ys ≤ xs"
    by (auto simp add: less_eq_infseq_def less_infseq_def)
qed

lemma infseq_lexord_mono [mono]:
  "(⋀ x y. f x y ⟶ g x y) ⟹ (xs, ys) ∈ infseq_lexord {(x, y). f x y} ⟶ (xs, ys) ∈ infseq_lexord {(x, y). g x y}"
  apply (simp add: infseq_lexord_def)
  apply (metis case_prodD case_prodI lexord_take_index_conv mem_Collect_eq)
  done

fun insort_rel :: "'a rel ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"insort_rel R x [] = [x]" |
"insort_rel R x (y # ys) = (if (x = y ∨ (x,y) ∈ R) then x # y # ys else y # insort_rel R x ys)"

inductive sorted_rel :: "'a rel ⇒ 'a list ⇒ bool" where
Nil_rel [iff]: "sorted_rel R []" |
Cons_rel: "∀ y ∈ set xs. (x = y ∨ (x, y) ∈ R) ⟹ sorted_rel R xs ⟹ sorted_rel R (x # xs)"

definition list_of_set :: "'a rel ⇒ 'a set ⇒ 'a list" where
"list_of_set R = folding_on.F (insort_rel R) []"

lift_definition infseq_inj :: "'a infseq infseq ⇒ 'a infseq" is
"λ f i. f (fst (prod_decode i)) (snd (prod_decode i))" .

lift_definition infseq_proj :: "'a infseq ⇒ 'a infseq infseq" is
"λ f i j. f (prod_encode (i, j))" .

lemma infseq_inj_inverse: "infseq_proj (infseq_inj x) = x"
  by (transfer, simp)

lemma infseq_proj_inverse: "infseq_inj (infseq_proj x) = x"
  by (transfer, simp)

lemma infseq_inj: "inj infseq_inj"
  by (metis injI infseq_inj_inverse)

lemma infseq_inj_surj: "bij infseq_inj"
  apply (rule bijI)
   apply (simp add: infseq_inj, safe, simp_all)
  apply (metis rangeI infseq_proj_inverse)
  done

end