Theory Coinductive.Coinductive_List_Prefix

(*  Title:       Prefix ordering on coinductive lists as ordering for type class order
    Author:      Andreas Lochbihler
    Maintainer:  Andreas Lochbihler
*)

section ‹Instantiation of the order type classes for lazy lists›
theory Coinductive_List_Prefix imports
  Coinductive_List
  "HOL-Library.Prefix_Order"
begin

subsection ‹Instantiation of the order type class›

instantiation llist :: (type) order begin

definition [code_unfold]: "xs ≤ ys = lprefix xs ys"

definition [code_unfold]: "xs < ys = lstrict_prefix xs ys"

instance
proof(intro_classes)
  fix xs ys zs :: "'a llist"
  show "(xs < ys) = (xs ≤ ys ∧ ¬ ys ≤ xs)"
    unfolding less_llist_def less_eq_llist_def lstrict_prefix_def
    by(auto simp: lprefix_antisym)
  show "xs ≤ xs" unfolding less_eq_llist_def by(rule lprefix_refl)
  show "⟦xs ≤ ys; ys ≤ zs⟧ ⟹ xs ≤ zs"
    unfolding less_eq_llist_def by(rule lprefix_trans)
  show "⟦xs ≤ ys; ys ≤ xs⟧ ⟹ xs = ys"
    unfolding less_eq_llist_def by(rule lprefix_antisym)
qed

end

lemma le_llist_conv_lprefix [iff]: "(≤) = lprefix"
by(simp add: less_eq_llist_def fun_eq_iff)

lemma less_llist_conv_lstrict_prefix [iff]: "(<) = lstrict_prefix"
by(simp add: less_llist_def fun_eq_iff)

instantiation llist :: (type) order_bot begin

definition "bot = LNil"

instance
by(intro_classes)(simp add: bot_llist_def)

end

lemma llist_of_lprefix_llist_of [simp]:
  "lprefix (llist_of xs) (llist_of ys) ⟷ xs ≤ ys"
proof(induct xs arbitrary: ys)
  case (Cons x xs) thus ?case
    by(cases ys)(auto simp add: LCons_lprefix_conv)
qed simp

subsection ‹Prefix ordering as a lower semilattice›

instantiation llist :: (type) semilattice_inf begin

definition [code del]:
  "inf xs ys = 
   unfold_llist (λ(xs, ys). xs ≠ LNil ⟶ ys ≠ LNil ⟶ lhd xs ≠ lhd ys)
     (lhd ∘ snd) (map_prod ltl ltl) (xs, ys)"

lemma llist_inf_simps [simp, code, nitpick_simp]:
  "inf LNil xs = LNil"
  "inf xs LNil = LNil"
  "inf (LCons x xs) (LCons y ys) = (if x = y then LCons x (inf xs ys) else LNil)"
unfolding inf_llist_def by simp_all

lemma llist_inf_eq_LNil [simp]:
  "lnull (inf xs ys) ⟷ (xs ≠ LNil ⟶ ys ≠ LNil ⟶ lhd xs ≠ lhd ys)"
by(simp add: inf_llist_def)

lemma [simp]: assumes "xs ≠ LNil" "ys ≠ LNil" "lhd xs = lhd ys"
  shows lhd_llist_inf: "lhd (inf xs ys) = lhd ys"
  and  ltl_llist_inf: "ltl (inf xs ys) = inf (ltl xs) (ltl ys)"
using assms by(simp_all add: inf_llist_def)

instance
proof
  fix xs ys zs :: "'a llist"
  show "inf xs ys ≤ xs" unfolding le_llist_conv_lprefix
    by(coinduction arbitrary: xs ys) auto

  show "inf xs ys ≤ ys" unfolding le_llist_conv_lprefix
    by(coinduction arbitrary: xs ys) auto

  assume "xs ≤ ys" "xs ≤ zs"
  thus "xs ≤ inf ys zs" unfolding le_llist_conv_lprefix
  proof(coinduction arbitrary: xs ys zs)
    case (lprefix xs ys zs)
    thus ?case by(cases xs)(auto 4 4 simp add: LCons_lprefix_conv)
  qed
qed

end

lemma llength_inf [simp]: "llength (inf xs ys) = llcp xs ys"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto simp add: llcp_eq_0_iff epred_llength epred_llcp)

instantiation llist :: (type) ccpo
begin

definition "Sup A = lSup A"

instance
  by intro_classes
     (auto simp: Sup_llist_def less_eq_llist_def[abs_def] intro!: llist.lub_upper llist.lub_least)

end

end