Theory Theory_Of_Lists

(*<*)
theory Theory_Of_Lists
imports
  HOLCF_ROOT
begin

(*>*)
section‹ Strict lists \label{sec:theory_of_lists} ›

text‹

Head- and tail-strict lists. Many technical Isabelle details are
lifted from ‹HOLCF-Prelude.Data_List›; names follow
HOL, prefixed with ‹s›.

›

domain 'a slist (‹[:_:]›) =
  snil (‹[::]›)
| scons (shead :: "'a") (stail :: "'a slist") (infixr ‹:#› 65)

lemma scons_strict[simp]: "scons⋅⊥ = ⊥"
by (clarsimp simp: cfun_eq_iff)

lemma shead_bottom_iff[simp]: "(shead⋅xs = ⊥) ⟷ (xs = ⊥ ∨ xs = [::])"
by (cases xs) simp_all

lemma stail_bottom_iff[simp]: "(stail⋅xs = ⊥) ⟷ (xs = ⊥ ∨ xs = [::])"
by (cases xs) simp_all

lemma match_snil_match_scons_slist_case: "match_snil⋅xs⋅k1 +++ match_scons⋅xs⋅k2 = slist_case⋅k1⋅k2⋅xs"
by (cases xs) simp_all

lemma slist_bottom': "slist_case⋅⊥⋅⊥⋅xs = ⊥"
by (cases xs; simp)

lemma slist_bottom[simp]: "slist_case⋅⊥⋅⊥ = ⊥"
by (simp add: cfun_eq_iff slist_bottom')

lemma slist_case_distr:
  "f⋅⊥ = ⊥ ⟹ f⋅(slist_case⋅g⋅h⋅xs) = slist_case⋅(f⋅g)⋅(Λ x xs. f⋅(h⋅x⋅xs))⋅xs"
  "slist_case⋅g'⋅h'⋅xs⋅z = slist_case⋅(g'⋅z)⋅(Λ x xs. h'⋅x⋅xs⋅z)⋅xs"
by (case_tac [!] xs) simp_all

lemma slist_case_cong:
  assumes "xs = xs'"
  assumes "xs' = [::] ⟹ n = n'"
  assumes "⋀y ys. ⟦xs' = y :# ys; y ≠ ⊥; ys ≠ ⊥⟧ ⟹ c y ys = c' y ys"
  assumes "cont (λ(x, y). c x y)"
  assumes "cont (λ(x, y). c' x y)"
  shows "slist_case⋅n⋅(Λ x xs. c x xs)⋅xs = slist_case⋅n'⋅(Λ x xs. c' x xs)⋅xs'"
using assms by (cases xs; cases xs'; clarsimp simp: prod_cont_iff)


text‹

Section syntax for @{const ‹scons›} ala Haskell.

›

syntax
  "_scons_section" :: "'a → [:'a:] → [:'a:]" (‹'(:#')›)
  "_scons_section_left" :: "'a ⇒ [:'a:] → [:'a:]" (‹'(_:#')›)
syntax_consts
  "_scons_section_left" == scons
translations
  "(x:#)" == "(CONST Rep_cfun) (CONST scons) x"

abbreviation scons_section_right :: "[:'a:] ⇒ 'a → [:'a:]" (‹'(:#_')›) where
  "(:#xs) ≡ Λ x. x :# xs"

syntax
  "_strict_list" :: "args ⇒ [:'a:]" (‹[:(_):]›)
syntax_consts
  "_strict_list" == scons
translations
  "[:x, xs:]" == "x :# [:xs:]"
  "[:x:]" == "x :# [::]"


text‹

Class instances.

›

instantiation slist :: (Eq) Eq_strict
begin

fixrec eq_slist :: "[:'a:] → [:'a:] → tr" where
  "eq_slist⋅[::]⋅[::] = TT"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ eq_slist⋅(x :# xs)⋅[::] = FF"
| "⟦y ≠ ⊥; ys ≠ ⊥⟧ ⟹ eq_slist⋅[::]⋅(y :# ys) = FF"
| "⟦x ≠ ⊥; xs ≠ ⊥; y ≠ ⊥; ys ≠ ⊥⟧ ⟹ eq_slist⋅(x :# xs)⋅(y :# ys) = (eq⋅x⋅y andalso eq_slist⋅xs⋅ys)"

instance proof
  fix xs :: "[:'a:]"
  show "eq⋅xs⋅⊥ = ⊥"
    by (cases xs) (subst eq_slist.unfold; simp)+
  show "eq⋅⊥⋅xs = ⊥"
    by (cases xs) (subst eq_slist.unfold; simp)+
qed

end

instance slist :: (Eq_sym) Eq_sym
proof
  fix xs ys :: "[:'a:]"
  show "eq⋅xs⋅ys = eq⋅ys⋅xs"
  proof (induct xs arbitrary: ys)
    case snil
    show ?case by (cases ys; simp)
  next
    case scons
    then show ?case by (cases ys; simp add: eq_sym)
  qed simp_all
qed

instance slist :: (Eq_equiv) Eq_equiv
proof
  fix xs ys zs :: "[:'a:]"
  show "eq⋅xs⋅xs ≠ FF"
    by (induct xs) simp_all
  assume "eq⋅xs⋅ys = TT" and "eq⋅ys⋅zs = TT" then show "eq⋅xs⋅zs = TT"
  proof (induct xs arbitrary: ys zs)
    case (snil ys zs) then show ?case by (cases ys, simp_all)
  next
    case (scons x xs ys zs) with eq_trans show ?case
      by (cases ys; cases zs) auto
  qed simp_all
qed

instance slist :: (Eq_eq) Eq_eq
proof
  fix xs ys :: "[:'a:]"
  show "eq⋅xs⋅xs ≠ FF"
    by (induct xs) simp_all
  assume "eq⋅xs⋅ys = TT" then show "xs = ys"
  proof (induct xs arbitrary: ys)
    case (snil ys) then show ?case by (cases ys) simp_all
  next
    case (scons x xs ys) then show ?case by (cases ys) auto
  qed simp
qed

instance slist :: (Eq_def) Eq_def
proof
  fix xs ys :: "[:'a:]"
  assume "xs ≠ ⊥" and "ys ≠ ⊥"
  then show "eq⋅xs⋅ys ≠ ⊥"
  proof(induct xs arbitrary: ys)
    case (snil ys) then show ?case by (cases ys) simp_all
  next
    case (scons a xs) then show ?case by (cases ys) simp_all
  qed simp
qed

lemma slist_eq_TT_snil[simp]:
  fixes xs :: "[:'a::Eq:]"
  shows "(eq⋅xs⋅[::] = TT) ⟷ (xs = [::])"
        "(eq⋅[::]⋅xs = TT) ⟷ (xs = [::])"
by (cases xs; simp)+

lemma slist_eq_FF_snil[simp]:
  fixes xs :: "[:'a::Eq:]"
  shows "(eq⋅xs⋅[::] = FF) ⟷ (∃y ys. y ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs = y :# ys)"
        "(eq⋅[::]⋅xs = FF) ⟷ (∃y ys. y ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs = y :# ys)"
by (cases xs; force)+


subsection‹ Some of the usual reasoning infrastructure ›

inductive slistmem :: "'a ⇒ [:'a:] ⇒ bool" where
  "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ slistmem x (x :# xs)"
| "⟦slistmem x xs; y ≠ ⊥⟧ ⟹ slistmem x (y :# xs)"

lemma slistmem_bottom1[iff]:
  fixes x :: "'a"
  shows "¬ slistmem x ⊥"
by rule (induct x "⊥::[:'a:]" rule: slistmem.induct; fastforce)

lemma slistmem_bottom2[iff]:
  fixes xs :: "[:'a:]"
  shows "¬ slistmem ⊥ xs"
by rule (induct "⊥::'a" xs rule: slistmem.induct; fastforce)

lemma slistmem_nil[iff]:
  shows "¬ slistmem x [::]"
by (fastforce elim: slistmem.cases)

lemma slistmem_scons[simp]:
  shows "slistmem x (y :# ys) ⟷ (x = y ∧ x ≠ ⊥ ∧ ys ≠ ⊥) ∨ (slistmem x ys ∧ y ≠ ⊥)"
proof -
  have "x = y ∨ slistmem x ys" if "slistmem x (y :# ys)"
    using that by (induct "x" "y :# ys" arbitrary: y ys rule: slistmem.induct; force)
  then show ?thesis by (auto elim: slistmem.cases intro: slistmem.intros)
qed

definition sset :: "[:'a:] ⇒ 'a set" where
  "sset xs = {x. slistmem x xs}"

lemma sset_simp[simp]:
  shows "sset ⊥ = {}"
    and "sset [::] = {}"
    and "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sset (x :# xs) = insert x (sset xs)"
unfolding sset_def by (auto elim: slistmem.cases intro: slistmem.intros)

lemma sset_defined[simp]:
  assumes "x ∈ sset xs"
  shows "x ≠ ⊥"
using assms sset_def by force

lemma sset_below:
  assumes "y ∈ sset ys"
  assumes "xs ⊑ ys"
  assumes "xs ≠ ⊥"
  obtains x where "x ∈ sset xs" and "x ⊑ y"
using assms
proof(induct ys arbitrary: xs)
  case (scons y ys xs) then show ?case by (cases xs) auto
qed simp_all


subsection‹ Some of the usual operations ›

text‹

A variety of functions on lists. Drawn from \<^citet>‹"Bird:1987"›, @{theory ‹HOL.List›} and
@{theory ‹HOLCF-Prelude.Data_List›}. The definitions vary because,
for instance, the strictness of some of those in
@{theory ‹HOLCF-Prelude.Data_List›} correspond neither to those in
Haskell nor Bird's expectations (specifically ‹stails›,
‹inits›, ‹sscanl›).

›

fixrec snull :: "[:'a:] → tr" where
  "snull⋅[::] = TT"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ snull⋅(x :# xs) = FF"

lemma snull_strict[simp]: "snull⋅⊥ = ⊥"
by fixrec_simp

lemma snull_bottom_iff[simp]: "(snull⋅xs = ⊥) ⟷ (xs = ⊥)"
by (cases xs) simp_all

lemma snull_FF_conv: "(snull⋅xxs = FF) ⟷ (∃x xs. xxs ≠ ⊥ ∧ xxs = x :# xs)"
by (cases xxs) simp_all

lemma snull_TT_conv[simp]: "(snull⋅xs = TT) ⟷ (xs = [::])"
by (cases xs) simp_all

lemma snull_eq_snil: "snull⋅xs = eq⋅xs⋅[::]"
by (cases xs) simp_all

fixrec smap :: "('a → 'b) → [:'a:] → [:'b:]" where
  "smap⋅f⋅[::] = [::]"
| "⟦x ≠⊥; xs ≠ ⊥⟧ ⟹ smap⋅f⋅(x :# xs) = f⋅x :# smap⋅f⋅xs"

lemma smap_strict[simp]: "smap⋅f⋅⊥ = ⊥"
by fixrec_simp

lemma smap_bottom_iff[simp]: "(smap⋅f⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (∃x∈sset xs. f⋅x = ⊥))"
by (induct xs) simp_all

lemma smap_is_snil_conv[simp]:
  "(smap⋅f⋅xs = [::]) ⟷ (xs = [::])"
  "( [::] = smap⋅f⋅xs) ⟷ (xs = [::])"
by (cases xs; simp)+

lemma smap_strict_scons[simp]:
  assumes "f⋅⊥ = ⊥"
  shows "smap⋅f⋅(x :# xs) = f⋅x :# smap⋅f⋅xs"
using assms by (cases "x :# xs = ⊥"; fastforce)

lemma smap_ID': "smap⋅ID⋅xs = xs"
by (induct xs) simp_all

lemma smap_ID[simp]: "smap⋅ID = ID"
by (clarsimp simp: cfun_eq_iff smap_ID')

lemma smap_cong:
  assumes "xs = xs'"
  assumes "⋀x. x ∈ sset xs ⟹ f⋅x = f'⋅x"
  shows "smap⋅f⋅xs = smap⋅f'⋅xs'"
using assms by (induct xs arbitrary: xs') auto

lemma smap_smap'[simp]:
  assumes "f⋅⊥ = ⊥"
  shows "smap⋅f⋅(smap⋅g⋅xs) = smap⋅(f oo g)⋅xs"
using assms by (induct xs) simp_all

lemma smap_smap[simp]:
  assumes "f⋅⊥ = ⊥"
  shows "smap⋅f oo smap⋅g = smap⋅(f oo g)"
using assms by (clarsimp simp: cfun_eq_iff)

lemma sset_smap[simp]:
  assumes "⋀x. x ∈ sset xs ⟹ f⋅x ≠ ⊥"
  shows "sset (smap⋅f⋅xs) = { f⋅x | x. x ∈ sset xs }"
using assms by (induct xs) auto

lemma shead_smap_distr:
  assumes "f⋅⊥ = ⊥"
  assumes "⋀x. x∈sset xs ⟹ f⋅x ≠ ⊥"
  shows "shead⋅(smap⋅f⋅xs) = f⋅(shead⋅xs)"
using assms by (induct xs) simp_all

fixrec sappend :: "[:'a:] → [:'a:] → [:'a:]" where
  "sappend⋅[::]⋅ys = ys"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sappend⋅(x :# xs)⋅ys = x :# sappend⋅xs⋅ys"

abbreviation sappend_syn :: "'a slist ⇒ 'a slist ⇒ 'a slist" (infixr ‹:@› 65) where
  "xs :@ ys ≡ sappend⋅xs⋅ys"

lemma sappend_strict[simp]: "sappend⋅⊥ = ⊥"
by fixrec_simp

lemma sappend_strict2[simp]: "xs :@ ⊥ = ⊥"
by (induct xs) simp_all

lemma sappend_bottom_iff[simp]: "(xs :@ ys = ⊥) ⟷ (xs = ⊥ ∨ ys = ⊥)"
by (induct xs) simp_all

lemma sappend_scons[simp]: "(x :# xs) :@ ys = x :# xs :@ ys"
by (cases "x :# xs = ⊥"; fastforce)

lemma sappend_assoc[simp]: "(xs :@ ys) :@ zs = xs :@ (ys :@ zs)"
by (induct xs) simp_all

lemma sappend_snil_id_left[simp]: "sappend⋅[::] = ID"
by (simp add: cfun_eq_iff)

lemma sappend_snil_id_right[iff]: "xs :@ [::] = xs"
by (induct xs) simp_all

lemma snil_append_iff[iff]: "xs :@ ys = [::] ⟷ xs = [::] ∧ ys = [::]"
by (induct xs) simp_all

lemma smap_sappend[simp]: "smap⋅f⋅(xs :@ ys) = smap⋅f⋅xs :@ smap⋅f⋅ys"
by (induct xs; cases "ys = ⊥"; simp)

lemma stail_sappend: "stail⋅(xs :@ ys) = (case xs of [::] ⇒ stail⋅ys | z :# zs ⇒ zs :@ ys)"
by (induct xs) simp_all

lemma stail_append2[simp]: "xs ≠ [::] ⟹ stail⋅(xs :@ ys) = stail⋅xs :@ ys"
by (induct xs) simp_all

lemma slist_case_snoc:
  "g⋅⊥⋅⊥ = ⊥ ⟹ slist_case⋅f⋅g⋅(xs :@ [:x:]) = g⋅(shead⋅(xs :@ [:x:]))⋅(stail⋅(xs :@ [:x:]))"
by (cases "x = ⊥"; cases xs; clarsimp)

fixrec sall :: "('a → tr) → [:'a:] → tr" where
  "sall⋅p⋅[::] = TT"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sall⋅p⋅(x :# xs) = (p⋅x andalso sall⋅p⋅xs)"

lemma sall_strict[simp]: "sall⋅p⋅⊥ = ⊥"
by fixrec_simp

lemma sall_const_TT[simp]:
  assumes "xs ≠ ⊥"
  shows "sall⋅(Λ x. TT)⋅xs = TT"
using assms by (induct xs) simp_all

lemma sall_const_TT_conv[simp]: "(sall⋅(Λ x. TT)⋅xs = TT) ⟷ (xs ≠ ⊥)"
by auto

lemma sall_TT[simp]: "(sall⋅p⋅xs = TT) ⟷ (xs ≠ ⊥ ∧ (∀x∈sset xs. p⋅x = TT))"
by (induct xs) simp_all

fixrec sfilter :: "('a → tr) → [:'a:] → [:'a:]" where
  "sfilter⋅p⋅[::] = [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sfilter⋅p⋅(x :# xs) = If p⋅x then x :# sfilter⋅p⋅xs else sfilter⋅p⋅xs"

lemma sfilter_strict[simp]: "sfilter⋅p⋅⊥ = ⊥"
by fixrec_simp

lemma sfilter_bottom_iff[simp]: "(sfilter⋅p⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (∃x∈sset xs. p⋅x = ⊥))"
by (induct xs) (use trE in auto)

lemma sset_sfilter[simp]:
  assumes "⋀x. x ∈ sset xs ⟹ p⋅x ≠ ⊥"
  shows "sset (sfilter⋅p⋅xs) = {x |x. x ∈ sset xs ∧ p⋅x = TT}"
using assms by (induct xs) (fastforce simp: If2_def[symmetric] split: If2_splits)+

lemma sfilter_strict_scons[simp]:
  assumes "p⋅⊥ = ⊥"
  shows "sfilter⋅p⋅(x :# xs) = If p⋅x then x :# sfilter⋅p⋅xs else sfilter⋅p⋅xs"
using assms by (cases "x = ⊥"; cases "xs = ⊥"; simp)

lemma sfilter_scons_let:
  assumes "p⋅⊥ = ⊥"
  shows "sfilter⋅p⋅(x :# xs) = (let xs' = sfilter⋅p⋅xs in If p⋅x then x :# xs' else xs')"
unfolding Let_def using assms by simp

lemma sfilter_sappend[simp]: "sfilter⋅p⋅(xs :@ ys) = sfilter⋅p⋅xs :@ sfilter⋅p⋅ys"
by (cases "ys"; clarsimp) (induct xs; fastforce simp: If2_def[symmetric] split: If2_splits)

lemma sfilter_const_FF[simp]:
  assumes "xs ≠ ⊥"
  shows "sfilter⋅(Λ x. FF)⋅xs = [::]"
using assms by (induct xs) simp_all

lemma sfilter_const_FF_conv[simp]: "(sfilter⋅(Λ x. FF)⋅xs = [::]) ⟷ (xs ≠ ⊥)"
by auto

lemma sfilter_const_TT[simp]: "sfilter⋅(Λ x. TT)⋅xs = xs"
by (induct xs) simp_all

lemma sfilter_cong:
  assumes "xs = xs'"
  assumes "⋀x. x ∈ sset xs ⟹ p⋅x = p'⋅x"
  shows "sfilter⋅p⋅xs = sfilter⋅p'⋅xs'"
using assms by (induct xs arbitrary: xs') auto

lemma sfilter_snil_conv[simp]: "sfilter⋅p⋅xs = [::] ⟷ sall⋅(neg oo p)⋅xs = TT"
by (induct xs; force simp: If2_def[symmetric] split: If2_splits)

lemma sfilter_sfilter': "sfilter⋅p⋅(sfilter⋅q⋅xs) = sfilter⋅(Λ x. q⋅x andalso p⋅x)⋅xs"
proof(induct xs)
  case (scons x xs) from scons(1, 2) show ?case
    by (cases "sfilter⋅q⋅xs = ⊥")
       (simp_all add: If_distr If_andalso scons(3)[symmetric] del: sfilter_bottom_iff)
qed simp_all

lemma sfilter_sfilter: "sfilter⋅p oo sfilter⋅q = sfilter⋅(Λ x. q⋅x andalso p⋅x)"
by (clarsimp simp: cfun_eq_iff sfilter_sfilter')

lemma sfilter_smap':
  assumes "p⋅⊥ = ⊥"
  shows "sfilter⋅p⋅(smap⋅f⋅xs) = smap⋅f⋅(sfilter⋅(p oo f)⋅xs)"
using assms by (induct xs; simp add: If2_def[symmetric] split: If2_splits) (metis slist.con_rews(2) smap.simps(2) smap_strict)

lemma sfilter_smap:
  assumes "p⋅⊥ = ⊥"
  shows "sfilter⋅p oo smap⋅f = smap⋅f oo sfilter⋅(p oo f)"
using assms by (clarsimp simp: cfun_eq_iff sfilter_smap')

fixrec sfoldl :: "('a::pcpo → 'b::domain → 'a) → 'a → [:'b:] → 'a" where
  "sfoldl⋅f⋅z⋅[::] = z"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sfoldl⋅f⋅z⋅(x :# xs) = sfoldl⋅f⋅(f⋅z⋅x)⋅xs"

lemma sfoldl_strict[simp]: "sfoldl⋅f⋅z⋅⊥ = ⊥"
by fixrec_simp

lemma sfoldl_strict_f[simp]:
  assumes "f⋅⊥ = ⊥"
  shows "sfoldl⋅f⋅⊥⋅xs = ⊥"
using assms by (induct xs) simp_all

lemma sfoldl_cong:
  assumes "xs = xs'"
  assumes "z = z'"
  assumes "⋀x z. x ∈ sset xs ⟹ f⋅z⋅x = f'⋅z⋅x"
  shows "sfoldl⋅f⋅z⋅xs = sfoldl⋅f'⋅z'⋅xs'"
using assms by (induct xs arbitrary: xs' z z') auto

lemma sfoldl_sappend[simp]:
  assumes "f⋅⊥ = ⊥"
  shows "sfoldl⋅f⋅z⋅(xs :@ ys) = sfoldl⋅f⋅(sfoldl⋅f⋅z⋅xs)⋅ys"
using assms by (cases "ys = ⊥", force) (induct xs arbitrary: z; simp)

fixrec sfoldr :: "('b → 'a::pcpo → 'a) → 'a → [:'b:] → 'a" where
  "sfoldr⋅f⋅z⋅[::] = z"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sfoldr⋅f⋅z⋅(x :# xs) = f⋅x⋅(sfoldr⋅f⋅z⋅xs)"

lemma sfoldr_strict[simp]: "sfoldr⋅f⋅z⋅⊥ = ⊥"
by fixrec_simp

fixrec sconcat :: "[:[:'a:]:] → [:'a:]" where
  "sconcat⋅[::] = [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sconcat⋅(x :# xs) = x :@ sconcat⋅xs"

lemma sconcat_strict[simp]: "sconcat⋅⊥ = ⊥"
by fixrec_simp

lemma sconcat_scons[simp]:
  shows "sconcat⋅(x :# xs) = x :@ sconcat⋅xs"
by (cases "x = ⊥", force) (induct xs; fastforce)

lemma sconcat_sfoldl_aux: "sfoldl⋅sappend⋅z⋅xs = z :@ sconcat⋅xs"
by (induct xs arbitrary: z) simp_all

lemma sconcat_sfoldl: "sconcat = sfoldl⋅sappend⋅[::]"
by (clarsimp simp: cfun_eq_iff sconcat_sfoldl_aux)

lemma sconcat_sappend[simp]: "sconcat⋅(xs :@ ys) = sconcat⋅xs :@ sconcat⋅ys"
by (induct xs) simp_all

fixrec slength :: "[:'a:] → Integer"
where
  "slength⋅[::] = 0"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ slength⋅(x :# xs) = slength⋅xs + 1"

lemma slength_strict[simp]: "slength⋅⊥ = ⊥"
by fixrec_simp

lemma slength_bottom_iff[simp]: "(slength⋅xs = ⊥) ⟷ (xs = ⊥)"
by (induct xs) force+

lemma slength_ge_0: "slength⋅xs = MkI⋅n ⟹ n ≥ 0"
by (induct xs arbitrary: n) (simp add: one_Integer_def plus_eq_MkI_conv; force)+

lemma slengthE:
  shows "⟦xs ≠ ⊥; ⋀n. ⟦slength⋅xs = MkI⋅n; 0 ≤ n⟧ ⟹ Q⟧ ⟹ Q"
by (meson Integer.exhaust slength_bottom_iff slength_ge_0)

lemma slength_0_conv[simp]:
  "(slength⋅xs = 0) ⟷ (xs = [::])"
  "(slength⋅xs = MkI⋅0) ⟷ (xs = [::])"
  "eq⋅0⋅(slength⋅xs) = snull⋅xs"
  "eq⋅(slength⋅xs)⋅0 = snull⋅xs"
by (induct xs) (auto simp: one_Integer_def elim: slengthE)

lemma le_slength_0[simp]: "(le⋅0⋅(slength⋅xs) = TT) ⟷ (xs ≠ ⊥)"
by (cases "slength⋅xs") (auto simp: slength_ge_0 zero_Integer_def)

lemma lt_slength_0[simp]:
  "xs ≠ ⊥ ⟹ lt⋅(slength⋅xs)⋅0 = FF"
  "xs ≠ ⊥ ⟹ lt⋅(slength⋅xs)⋅(slength⋅xs + 1) = TT"
unfolding zero_Integer_def one_Integer_def by (auto elim: slengthE)

lemma slength_smap[simp]:
  assumes "⋀x. x ≠ ⊥ ⟹ f⋅x ≠ ⊥"
  shows "slength⋅(smap⋅f⋅xs) = slength⋅xs"
using assms by (induct xs) simp_all

lemma slength_sappend[simp]: "slength⋅(xs :@ ys) = slength⋅xs + slength⋅ys"
by (cases "ys = ⊥", force) (induct xs; force simp: ac_simps)

lemma slength_sfoldl_aux: "sfoldl⋅(Λ i _. i + 1)⋅z⋅xs = z + slength⋅xs"
by (induct xs arbitrary: z) (simp_all add: ac_simps)

lemma slength_sfoldl: "slength = sfoldl⋅(Λ i _. i + 1)⋅0"
by (clarsimp simp: cfun_eq_iff slength_sfoldl_aux)

lemma le_slength_plus:
  assumes "xs ≠ ⊥"
  assumes "n ≠ ⊥"
  shows "le⋅n⋅(slength⋅xs + n) = TT"
using assms by (cases n; force elim: slengthE)

fixrec srev :: "[:'a:] → [:'a:]" where
  "srev⋅[::] = [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ srev⋅(x :# xs) = srev⋅xs :@ [:x:]"

lemma srev_strict[simp]: "srev⋅⊥ = ⊥"
by fixrec_simp

lemma srev_bottom_iff[simp]: "(srev⋅xs = ⊥) ⟷ (xs = ⊥)"
by (induct xs) simp_all

lemma srev_scons[simp]: "srev⋅(x :# xs) = srev⋅xs :@ [:x:]"
by (cases "x = ⊥", clarsimp) (induct xs; force)

lemma srev_sappend[simp]: "srev⋅(xs :@ ys) = srev⋅ys :@ srev⋅xs"
by (induct xs) simp_all

lemma srev_srev_ident[simp]: "srev⋅(srev⋅xs) = xs"
by (induct xs) auto

lemma srev_cases[case_names bottom snil ssnoc]:
  assumes "xs = ⊥ ⟹ P"
  assumes "xs = [::] ⟹ P"
  assumes "⋀y ys. ⟦y ≠ ⊥; ys ≠ ⊥; xs = ys :@ [:y:]⟧ ⟹ P"
  shows "P"
using assms by (metis slist.exhaust srev.simps(1) srev_scons srev_srev_ident srev_strict)

lemma srev_induct[case_names bottom snil ssnoc]:
  assumes "P ⊥"
  assumes "P [::]"
  assumes "⋀x xs. ⟦x ≠ ⊥; xs ≠ ⊥; P xs⟧ ⟹ P (xs :@ [:x:])"
  shows "P xs"
proof -
  have "P (srev⋅(srev⋅xs))" by (rule slist.induct[where x="srev⋅xs"]; simp add: assms)
  then show ?thesis by simp
qed

lemma sfoldr_conv_sfoldl:
  assumes "⋀x. f⋅x⋅⊥ = ⊥" ―‹‹f› must be strict in the accumulator.›
  shows "sfoldr⋅f⋅z⋅xs = sfoldl⋅(Λ acc x. f⋅x⋅acc)⋅z⋅(srev⋅xs)"
using assms by (induct xs arbitrary: z) simp_all

fixrec stake :: "Integer → [:'a:] → [:'a:]" where ―‹ Note: strict in both parameters. ›
  "stake⋅⊥⋅⊥ = ⊥"
| "i ≠ ⊥ ⟹ stake⋅i⋅[::] = [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ stake⋅i⋅(x :# xs) = If le⋅i⋅0 then [::] else x :# stake⋅(i - 1)⋅xs"

lemma stake_strict[simp]:
  "stake⋅⊥ = ⊥"
  "stake⋅i⋅⊥ = ⊥"
by fixrec_simp+

lemma stake_bottom_iff[simp]: "(stake⋅i⋅xs = ⊥) ⟷ (i = ⊥ ∨ xs = ⊥)"
by (induct xs arbitrary: i; clarsimp; case_tac i; clarsimp)

lemma stake_0[simp]:
  "xs ≠ ⊥ ⟹ stake⋅0⋅xs = [::]"
  "xs ≠ ⊥ ⟹ stake⋅(MkI⋅0)⋅xs = [::]"
  "stake⋅0⋅xs ⊑ [::]"
by (cases xs; simp add: zero_Integer_def)+

lemma stake_scons[simp]: "le⋅1⋅i = TT ⟹ stake⋅i⋅(x :# xs) = x :# stake⋅(i - 1)⋅xs"
by (cases i; cases "x = ⊥"; cases "xs = ⊥";
    simp add: zero_Integer_def one_Integer_def split: if_splits)

lemma take_MkI_scons[simp]:
  "0 < n ⟹ stake⋅(MkI⋅n)⋅(x :# xs) = x :# stake⋅(MkI⋅(n - 1))⋅xs"
by (cases "x = ⊥"; cases "xs = ⊥"; simp add: zero_Integer_def one_Integer_def)

lemma stake_numeral_scons[simp]:
  "xs ≠ ⊥ ⟹ stake⋅1⋅(x :# xs) = [:x:]"
  "stake⋅(numeral (Num.Bit0 k))⋅(x :# xs) = x :# stake⋅(numeral (Num.BitM k))⋅xs"
  "stake⋅(numeral (Num.Bit1 k))⋅(x :# xs) = x :# stake⋅(numeral (Num.Bit0 k))⋅xs"
by (cases "x = ⊥"; cases xs; simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+

lemma stake_all:
  assumes "le⋅(slength⋅xs)⋅i = TT"
  shows "stake⋅i⋅xs = xs"
using assms
proof(induct xs arbitrary: i)
  case (scons x xs i) then show ?case
    by (cases i; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits if_splits elim!: slengthE)
qed (simp_all add: le_defined)

lemma stake_all_triv[simp]: "stake⋅(slength⋅xs)⋅xs = xs"
by (cases "xs = ⊥") (auto simp: stake_all)

lemma stake_append[simp]: "stake⋅i⋅(xs :@ ys) = stake⋅i⋅xs :@ stake⋅(i - slength⋅xs)⋅ys"
proof(induct xs arbitrary: i)
  case (snil i) then show ?case by (cases i; simp add: zero_Integer_def)
next
  case (scons x xs i) then show ?case
    by (cases i; cases ys; clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits  elim!: slengthE)
qed simp_all

fixrec sdrop :: "Integer → [:'a:] → [:'a:]" where ―‹ Note: strict in both parameters. ›
  [simp del]: "sdrop⋅i⋅xs = If le⋅i⋅0 then xs else (case xs of [::] ⇒ [::] | y :# ys ⇒ sdrop⋅(i - 1)⋅ys)"

lemma sdrop_strict[simp]:
  "sdrop⋅⊥ = ⊥"
  "sdrop⋅i⋅⊥ = ⊥"
by fixrec_simp+

lemma sdrop_bottom_iff[simp]: "(sdrop⋅i⋅xs = ⊥) ⟷ (i = ⊥ ∨ xs = ⊥)"
proof(induct xs arbitrary: i)
  case (snil i) then show ?case by (subst sdrop.unfold) (cases i; simp)
next
  case (scons x xs i) then show ?case by (subst sdrop.unfold) fastforce
qed simp

lemma sdrop_snil[simp]:
  assumes "i ≠ ⊥"
  shows "sdrop⋅i⋅[::] = [::]"
using assms by (subst sdrop.unfold; fastforce)

lemma sdrop_snil_conv[simp]: "(sdrop⋅i⋅[::] = [::]) ⟷ (i ≠ ⊥)"
by (subst sdrop.unfold; fastforce)

lemma sdrop_0[simp]:
  "sdrop⋅0⋅xs = xs"
  "sdrop⋅(MkI⋅0)⋅xs = xs"
by (subst sdrop.simps, simp add: zero_Integer_def)+

lemma sdrop_pos:
  "le⋅i⋅0 = FF ⟹ sdrop⋅i⋅xs = (case xs of [::] ⇒ [::] | y :# ys ⇒ sdrop⋅(i - 1)⋅ys)"
by (subst sdrop.simps, simp)

lemma sdrop_neg:
  "le⋅i⋅0 = TT ⟹ sdrop⋅i⋅xs = xs"
by (subst sdrop.simps, simp)

lemma sdrop_numeral_scons[simp]:
  "x ≠ ⊥ ⟹ sdrop⋅1⋅(x :# xs) = xs"
  "x ≠ ⊥ ⟹ sdrop⋅(numeral (Num.Bit0 k))⋅(x :# xs) = sdrop⋅(numeral (Num.BitM k))⋅xs"
  "x ≠ ⊥ ⟹ sdrop⋅(numeral (Num.Bit1 k))⋅(x :# xs) = sdrop⋅(numeral (Num.Bit0 k))⋅xs"
by (subst sdrop.simps,
    simp add: zero_Integer_def one_Integer_def numeral_Integer_eq; cases xs; simp)+

lemma sdrop_sappend[simp]:
  "sdrop⋅i⋅(xs :@ ys) = sdrop⋅i⋅xs :@ sdrop⋅(i - slength⋅xs)⋅ys"
proof(induct xs arbitrary: i)
  case (snil i) then show ?case by (cases i; simp add: zero_Integer_def)
next
  case (scons x xs i) then show ?case
    by (cases "ys = ⊥"; cases "le⋅i⋅0"; cases i;
        clarsimp simp: zero_Integer_def one_Integer_def sdrop_neg sdrop_pos add.commute diff_diff_add
                split: if_splits elim!: slengthE)
qed simp

lemma sdrop_all:
  assumes "le⋅(slength⋅xs)⋅i = TT"
  shows "sdrop⋅i⋅xs = [::]"
using assms
proof(induct xs arbitrary: i)
  case (scons x xs i) then show ?case
    by (subst sdrop.unfold; cases i;
        clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits if_splits elim!: slengthE)
qed (simp_all add: le_defined)

lemma slength_sdrop[simp]:
  "slength⋅(sdrop⋅i⋅xs) = If le⋅i⋅0 then slength⋅xs else If le⋅(slength⋅xs)⋅i then 0 else slength⋅xs - i"
proof(induct xs arbitrary: i)
  case (snil i) then show ?case by (cases i; simp add: zero_Integer_def)
next
  case (scons x xs i) then show ?case
    by (subst sdrop.unfold; cases i; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE)
qed simp

lemma sdrop_not_snilD:
  assumes "sdrop⋅(MkI⋅i)⋅xs ≠ [::]"
  assumes "xs ≠ ⊥"
  shows "lt⋅(MkI⋅i)⋅(slength⋅xs) = TT ∧ xs ≠ [::]"
using assms
proof(induct xs arbitrary: i)
  case (scons x xs i) then show ?case
    by (subst (asm) (2) sdrop.unfold, clarsimp simp: zero_Integer_def one_Integer_def not_le sdrop_all elim!: slengthE)
qed simp_all

lemma sdrop_sappend_same:
  assumes "xs ≠ ⊥"
  shows "sdrop⋅(slength⋅xs)⋅(xs :@ ys) = ys"
using assms
proof(induct xs arbitrary: ys)
  case (scons x xs ys) then show ?case
    by (cases "ys = ⊥"; subst sdrop.unfold; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE)
qed simp_all

fixrec sscanl :: "('a → 'b → 'a) → 'a → [:'b:] → [:'a:]" where
  "sscanl⋅f⋅z⋅[::] = z :# [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sscanl⋅f⋅z⋅(x :# xs) = z :# sscanl⋅f⋅(f⋅z⋅x)⋅xs"

lemma sscanl_strict[simp]:
  "sscanl⋅f⋅⊥⋅xs = ⊥"
  "sscanl⋅f⋅z⋅⊥ = ⊥"
by (cases xs) fixrec_simp+

lemma sscanl_cong:
  assumes "xs = xs'"
  assumes "z = z'"
  assumes "⋀x z. x ∈ sset xs ⟹ f⋅z⋅x = f'⋅z⋅x"
  shows "sscanl⋅f⋅z⋅xs = sscanl⋅f'⋅z'⋅xs'"
using assms by (induct xs arbitrary: xs' z z') auto

lemma sscanl_lfp_fusion':
  assumes "g⋅⊥ = ⊥"
  assumes *: "⋀acc x. x ≠ ⊥ ⟹ g⋅(f⋅acc⋅x) = f'⋅(g⋅acc)⋅x"
  shows "smap⋅g⋅(sscanl⋅f⋅z⋅xs) = sscanl⋅f'⋅(g⋅z)⋅xs"
using assms by (induct xs arbitrary: z) simp_all

lemma sscanl_lfp_fusion:
  assumes "g⋅⊥ = ⊥"
  assumes *: "⋀acc x. x ≠ ⊥ ⟹ g⋅(f⋅acc⋅x) = f'⋅(g⋅acc)⋅x"
  shows "smap⋅g oo sscanl⋅f⋅z = sscanl⋅f'⋅(g⋅z)"
using assms by (clarsimp simp: cfun_eq_iff sscanl_lfp_fusion')

lemma sscanl_ww_fusion': ―‹ Worker/wrapper \<^citep>‹"GillHutton:2009" and "Gammie:2011"› specialised to @{const ‹sscanl›} ›
  fixes wrap :: "'b → 'a"
  fixes unwrap :: "'a → 'b"
  fixes z :: "'a"
  fixes f :: "'a → 'c → 'a"
  fixes f' :: "'b → 'c → 'b"
  assumes ww: "wrap oo unwrap = ID"
  assumes wb: "⋀z x. x ≠ ⊥ ⟹ unwrap⋅(f⋅(wrap⋅z)⋅x) = f'⋅(unwrap⋅(wrap⋅z))⋅x"
  shows "sscanl⋅f⋅z⋅xs = smap⋅wrap⋅(sscanl⋅f'⋅(unwrap⋅z)⋅xs)"
using assms
by (induct xs arbitrary: z) (simp add: cfun_eq_iff retraction_cfcomp_strict | metis)+

lemma sscanl_ww_fusion: ―‹ Worker/wrapper \<^citep>‹"GillHutton:2009" and "Gammie:2011"› specialised to @{const ‹sscanl›} ›
  fixes wrap :: "'b → 'a"
  fixes unwrap :: "'a → 'b"
  fixes z :: "'a"
  fixes f :: "'a → 'c → 'a"
  fixes f' :: "'b → 'c → 'b"
  assumes ww: "wrap oo unwrap = ID"
  assumes wb: "⋀z x. x ≠ ⊥ ⟹ unwrap⋅(f⋅(wrap⋅z)⋅x) = f'⋅(unwrap⋅(wrap⋅z))⋅x"
  shows "sscanl⋅f⋅z = smap⋅wrap oo sscanl⋅f'⋅(unwrap⋅z)"
using assms by (clarsimp simp: cfun_eq_iff sscanl_ww_fusion')

fixrec sinits :: "[:'a:] → [:[:'a:]:]" where
  "sinits⋅[::] = [::] :# [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sinits⋅(x :# xs) = [::] :# smap⋅(scons⋅x)⋅(sinits⋅xs)"

lemma sinits_strict[simp]: "sinits⋅⊥ = ⊥"
by fixrec_simp

lemma sinits_bottom_iff[simp]: "(sinits⋅xs = ⊥) ⟷ (xs = ⊥)"
by (induct xs) simp_all

lemma sinits_not_snil[iff]: "sinits⋅xs ≠ [::]"
by (cases xs) simp_all

lemma sinits_empty_bottom[simp]: "(sset (sinits⋅xs) = {}) ⟷ (xs = ⊥)"
by (cases xs) simp_all

lemma sinits_scons[simp]: "sinits⋅(x :# xs) = [::] :# smap⋅(x :#)⋅(sinits⋅xs)"
by (cases "x = ⊥", force) (induct xs; force)

lemma sinits_length[simp]: "slength⋅(sinits⋅xs) = slength⋅xs + 1"
by (induct xs) simp_all

lemma sinits_snoc[simp]: "sinits⋅(xs :@ [:x:]) = sinits⋅xs :@ [:xs :@ [:x:]:]"
by (induct xs) simp_all

lemma sinits_foldr': ―‹ \<^citet>‹‹p30› in "Bird:1987"› ›
  shows "sinits⋅xs = sfoldr⋅(Λ x xs. [:[::]:] :@ smap⋅(x :#)⋅xs)⋅[:[::]:]⋅xs"
by (induct xs) simp_all

lemma sinits_sscanl':
  shows "smap⋅(sfoldl⋅f⋅z)⋅(sinits⋅xs) = sscanl⋅f⋅z⋅xs"
by (induct xs arbitrary: z) (simp_all cong: smap_cong add: oo_def eta_cfun)

lemma sinits_sscanl: ―‹ \<^citet>‹‹Lemma~5› in "Bird:1987"›, \<^citet>‹‹p118 ``the scan lemma''› in "Bird:PearlsofFAD:2010"› ›
  shows "smap⋅(sfoldl⋅f⋅z) oo sinits = sscanl⋅f⋅z"
by (simp add: sinits_sscanl' cfun_eq_iff)

lemma sinits_all[simp]: "(xs ∈ sset (sinits⋅xs)) ⟷ (xs ≠ ⊥)"
by (induct xs) simp_all

fixrec stails :: "[:'a:] → [:[:'a:]:]" where
  "stails⋅[::] = [::] :# [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ stails⋅(x :# xs) = (x :# xs) :# stails⋅xs"

lemma stails_strict[simp]: "stails⋅⊥ = ⊥"
by fixrec_simp

lemma stails_bottom_iff[simp]: "(stails⋅xs = ⊥) ⟷ (xs = ⊥)"
by (induct xs) simp_all

lemma stails_not_snil[iff]: "stails⋅xs ≠ [::]"
by (cases xs) simp_all

lemma stails_scons[simp]: "stails⋅(x :# xs) = (x :# xs) :# stails⋅xs"
by (induct xs) (cases "x = ⊥"; simp)+

lemma stails_slength[simp]: "slength⋅(stails⋅xs) = slength⋅xs + 1"
by (induct xs) simp_all

lemma stails_snoc[simp]:
  shows "stails⋅(xs :@ [:x:]) = smap⋅(Λ ys. ys :@ [:x:])⋅(stails⋅xs) :@ [:[::]:]"
by (induct xs) simp_all

lemma stails_sfoldl':
  shows "stails⋅xs = sfoldl⋅(Λ xs x. smap⋅(Λ ys. ys :@ [:x:])⋅xs :@ [:[::]:])⋅[:[::]:]⋅xs"
by (induct xs rule: srev_induct) simp_all

lemma stails_sfoldl:
  shows "stails = sfoldl⋅(Λ xs x. smap⋅(Λ ys. ys :@ [:x:])⋅xs :@ [:[::]:])⋅[:[::]:]"
by (clarsimp simp: cfun_eq_iff stails_sfoldl')

lemma stails_all[simp]: "(xs ∈ sset (stails⋅xs)) ⟷ (xs ≠ ⊥)"
by (cases xs) simp_all

fixrec selem :: "'a::Eq_def → [:'a:] → tr" where
  "selem⋅x⋅[::] = FF"
| "⟦y ≠ ⊥; ys ≠ ⊥⟧ ⟹ selem⋅x⋅(y :# ys) = (eq⋅x⋅y orelse selem⋅x⋅ys)"

lemma selem_strict[simp]: "selem⋅x⋅⊥ = ⊥"
by fixrec_simp

lemma selem_bottom_iff[simp]: "(selem⋅x⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (xs ≠ [::] ∧ x = ⊥))"
by (induct xs) auto

lemma selem_sappend[simp]:
  assumes "ys ≠ ⊥"
  shows "selem⋅x⋅(xs :@ ys) = (selem⋅x⋅xs orelse selem⋅x⋅ys)"
using assms by (induct xs) simp_all

lemma elem_TT[simp]: "(selem⋅x⋅xs = TT) ⟷ (x ∈ sset xs)"
by (induct xs; auto) (metis sset_defined)+

lemma elem_FF[simp]: "(selem⋅x⋅xs = FF) ⟷ (xs = [::] ∨ (x ≠ ⊥ ∧ xs ≠ ⊥ ∧ x ∉ sset xs))"
by (induct xs) auto

lemma selem_snil_stails[iff]:
  assumes "xs ≠ ⊥"
  shows "selem⋅[::]⋅(stails⋅xs) = TT"
using assms by (induct xs) simp_all

fixrec sconcatMap :: "('a → [:'b:]) → [:'a:] → [:'b:]" where
[simp del]: "sconcatMap⋅f = sconcat oo smap⋅f"

lemma sconcatMap_strict[simp]: "sconcatMap⋅f⋅⊥ = ⊥"
by fixrec_simp

lemma sconcatMap_snil[simp]: "sconcatMap⋅f⋅[::] = [::]"
by fixrec_simp

lemma sconcatMap_scons[simp]: "x ≠ ⊥ ⟹ sconcatMap⋅f⋅(x :# xs) = f⋅x :@ sconcatMap⋅f⋅xs"
by (cases "xs = ⊥"; simp add: sconcatMap.unfold)

lemma sconcatMap_bottom_iff[simp]: "(sconcatMap⋅f⋅xs = ⊥) ⟷ (xs = ⊥ ∨ (∃x∈sset xs. f⋅x = ⊥))"
by (induct xs) simp_all

lemma sconcatMap_sappend[simp]: "sconcatMap⋅f⋅(xs :@ ys) = sconcatMap⋅f⋅xs :@ sconcatMap⋅f⋅ys"
by (induct xs) simp_all

lemma sconcatMap_monad_laws:
  "sconcatMap⋅(Λ x. [:x:])⋅xs = xs"
  "sconcatMap⋅g⋅(sconcatMap⋅f⋅xs) = sconcatMap⋅(Λ x. sconcatMap⋅g⋅(f⋅x))⋅xs"
by (induct xs) simp_all

fixrec supto :: "Integer → Integer → [:Integer:]" where
  [simp del]: "supto⋅i⋅j = If le⋅i⋅j then i :# supto⋅(i+1)⋅j else [::]"

lemma upto_strict[simp]:
  "supto⋅⊥ = ⊥"
  "supto⋅m⋅⊥ = ⊥"
by fixrec_simp+

lemma supto_is_snil_conv[simp]:
  "(supto⋅(MkI⋅i)⋅(MkI⋅j) = [::]) ⟷ (j < i)"
  "([::] = supto⋅(MkI⋅i)⋅(MkI⋅j)) ⟷ (j < i)"
by (subst supto.unfold; simp)+

lemma supto_simp[simp]:
  "j < i ⟹ supto⋅(MkI⋅i)⋅(MkI⋅j) = [::]"
  "i ≤ j ⟹ supto⋅(MkI⋅i)⋅(MkI⋅j) = MkI⋅i :# supto⋅(MkI⋅i+1)⋅(MkI⋅j)"
  "supto⋅0⋅0 = [:0:]"
by (subst supto.simps, simp)+

lemma supto_defined[simp]: "supto⋅(MkI⋅i)⋅(MkI⋅j) ≠ ⊥" (is "?P i j")
proof (cases "j - i")
  fix d
  assume "j - i = int d"
  then show "?P i j"
  proof (induct d arbitrary: i j)
    case (Suc d i j)
    then have "j - (i + 1) = int d" and le: "i ≤ j" by simp_all
    from Suc(1)[OF this(1)] have IH: "?P (i+1) j" .
    then show ?case using le by (simp add: one_Integer_def)
  qed (simp add: one_Integer_def)
next
  fix d
  assume "j - i = - int d"
  then have "j ≤ i" by auto
  moreover
  { assume "j = i" then have "?P i j" by (simp add: one_Integer_def) }
  moreover
  { assume "j < i" then have "?P i j" by (simp add: one_Integer_def) }
  ultimately show ?thesis by arith
qed

lemma supto_bottom_iff[simp]:
  "(supto⋅i⋅j = ⊥) ⟷ (i = ⊥ ∨ j = ⊥)"
by (cases i; simp; cases j; simp)

lemma supto_snoc[simp]:
  "i ≤ j ⟹ supto⋅(MkI⋅i)⋅(MkI⋅j) = supto⋅(MkI⋅i)⋅(MkI⋅j-1) :@ [:MkI⋅j:]"
proof(induct "nat(j - i)" arbitrary: i j)
  case 0 then show ?case by (simp add: one_Integer_def)
next
  case (Suc k i j)
  then have "k = nat (j - (i + 1))" "i < j" by linarith+
  from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) show ?case by (simp add: one_Integer_def)
qed

lemma slength_supto[simp]: "slength⋅(supto⋅(MkI⋅i)⋅(MkI⋅j)) = MkI⋅(if j < i then 0 else j - i + 1)" (is "?P i j")
proof (cases "j - i")
  fix d
  assume "j - i = int d"
  then show "?P i j"
  proof (induct d arbitrary: i j)
    case (Suc d i j)
    then have "j - (i + 1) = int d" and le: "i ≤ j" by simp_all
    from Suc(1)[OF this(1)] have IH: "?P (i+1) j" .
    then show ?case using le by (simp add: one_Integer_def)
  qed (simp add: one_Integer_def)
next
  fix d
  assume "j - i = - int d"
  then have "j ≤ i" by auto
  moreover
  { assume "j = i" then have "?P i j" by (simp add: one_Integer_def) }
  moreover
  { assume "j < i" then have "?P i j" by (simp add: one_Integer_def) }
  ultimately show ?thesis by arith
qed

lemma sset_supto[simp]:
  "sset (supto⋅(MkI⋅i)⋅(MkI⋅j)) = {MkI⋅k |k. i ≤ k ∧ k ≤ j}" (is "sset (?u i j) = ?R i j")
proof (cases "j - i")
  case (nonneg k)
  then show ?thesis
  proof (induct k arbitrary: i j)
    case (Suc k)
    then have *: "j - (i + 1) = int k" by simp
    from Suc(1)[OF *] have IH: "sset (?u (i+1) j) = ?R (i+1) j" .
    from * have "i ≤ j" by simp
    then have "sset (?u i j) = sset (MkI⋅i :# ?u (i+1) j)" by (simp add: one_Integer_def)
    also have "… = insert (MkI⋅i) (?R (i+1) j)" by (simp add: IH)
    also have "… = ?R i j" using ‹i ≤ j› by auto
    finally show ?case .
  qed (force simp: one_Integer_def)
qed simp

lemma supto_split1: ―‹From ‹HOL.List››
  assumes "i ≤ j"
  assumes "j ≤ k"
  shows "supto⋅(MkI⋅i)⋅(MkI⋅k) = supto⋅(MkI⋅i)⋅(MkI⋅(j - 1)) :@ supto⋅(MkI⋅j)⋅(MkI⋅k)"
using assms
proof (induct j rule: int_ge_induct)
  case (step l) with supto_simp(2) supto_snoc show ?case by (clarsimp simp: one_Integer_def)
qed simp

lemma supto_split2: ―‹From ‹HOL.List››
  assumes "i ≤ j"
  assumes "j ≤ k"
  shows "supto⋅(MkI⋅i)⋅(MkI⋅k) = supto⋅(MkI⋅i)⋅(MkI⋅j) :@ supto⋅(MkI⋅(j + 1))⋅(MkI⋅k)"
proof(cases "j + 1 ≤ k")
  case True with assms show ?thesis
    by (subst supto_split1[where j="j + 1" and k=k]; clarsimp simp: one_Integer_def)
next
  case False with assms show ?thesis by (clarsimp simp: one_Integer_def not_le)
qed

lemma supto_split3: ―‹From ‹HOL.List››
  assumes "i ≤ j"
  assumes "j ≤ k"
  shows "supto⋅(MkI⋅i)⋅(MkI⋅k) = supto⋅(MkI⋅i)⋅(MkI⋅(j - 1)) :@ MkI⋅j :# supto⋅(MkI⋅(j + 1))⋅(MkI⋅k)"
using assms supto_simp(2) supto_split1 by (metis one_Integer_def plus_MkI_MkI)

lemma sinits_stake':
  shows "sinits⋅xs = smap⋅(Λ i. stake⋅i⋅xs)⋅(supto⋅0⋅(slength⋅xs))"
proof(induct xs rule: srev_induct)
  case (ssnoc x xs) then show ?case
    apply (clarsimp simp: zero_Integer_def one_Integer_def stake_all
                simp del: supto_simp
                   elim!: slengthE)
    apply (rule arg_cong, rule smap_cong[OF refl])
    apply clarsimp
    done
qed simp_all

lemma stails_sdrop':
  shows "stails⋅xs = smap⋅(Λ i. sdrop⋅i⋅xs)⋅(supto⋅0⋅(slength⋅xs))"
proof(induct xs rule: srev_induct)
  case (ssnoc x xs) then show ?case
    apply (clarsimp simp: zero_Integer_def one_Integer_def sdrop_all
                simp del: supto_simp
                   elim!: slengthE)
    apply (rule arg_cong, rule smap_cong[OF refl])
    apply clarsimp
    apply (subst (3) sdrop_neg; fastforce simp: zero_Integer_def)
    done
qed simp_all

lemma sdrop_elem_stails[iff]:
  assumes "xs ≠ ⊥"
  shows "sdrop⋅(MkI⋅i)⋅xs ∈ sset (stails⋅xs)"
using assms
by (clarsimp simp: stails_sdrop' zero_Integer_def one_Integer_def elim!: slengthE)
   (metis add.left_neutral le_MkI_MkI le_cases not_less sdrop_all sdrop_neg zero_Integer_def zless_imp_add1_zle)

fixrec slast :: "[:'a:] → 'a" where
  "slast⋅[::] = ⊥"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ slast⋅(x :# xs) = (case xs of [::] ⇒ x | y :# ys ⇒ slast⋅xs)"

lemma slast_strict[simp]:
  "slast⋅⊥ = ⊥"
by fixrec_simp

lemma slast_singleton[simp]: "slast⋅[:x:] = x"
by (cases "x = ⊥"; simp)

lemma slast_sappend_ssnoc[simp]:
  assumes "xs ≠ ⊥"
  shows "slast⋅(xs :@ [:x:]) = x"
using assms
proof(induct xs)
  case (scons y ys) then show ?case by (cases "x = ⊥"; simp; cases ys; simp)
qed simp_all

fixrec sbutlast :: "[:'a:] → [:'a:]" where
  "sbutlast⋅[::] = [::]"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ sbutlast⋅(x :# xs) = (case xs of [::] ⇒ [::] | y :# ys ⇒ x :# sbutlast⋅xs)"

lemma sbutlast_strict[simp]:
  "sbutlast⋅⊥ = ⊥"
by fixrec_simp

lemma sbutlast_sappend_ssnoc[simp]:
  assumes "x ≠ ⊥"
  shows "sbutlast⋅(xs :@ [:x:]) = xs"
using assms
proof(induct xs)
  case (scons y ys) then show ?case by (cases ys; simp)
qed simp_all

fixrec prefix :: "[:'a::Eq_def:] → [:'a:] → tr" where
  "prefix⋅xs⋅⊥ = ⊥"
| "ys ≠ ⊥ ⟹ prefix⋅[::]⋅ys = TT"
| "⟦x ≠ ⊥; xs ≠ ⊥⟧ ⟹ prefix⋅(x :# xs)⋅[::] = FF"
| "⟦x ≠ ⊥; xs ≠ ⊥; y ≠ ⊥; ys ≠ ⊥⟧ ⟹ prefix⋅(x :# xs)⋅(y :# ys) = (eq⋅x⋅y andalso prefix⋅xs⋅ys)"

lemma prefix_strict[simp]: "prefix⋅⊥ = ⊥"
by (clarsimp simp: cfun_eq_iff) fixrec_simp

lemma prefix_bottom_iff[simp]: "(prefix⋅xs⋅ys = ⊥) ⟷ (xs = ⊥ ∨ ys = ⊥)"
proof(induct xs arbitrary: ys)
  case (snil ys) then show ?case by (cases ys) simp_all
next
  case (scons a xs) then show ?case by (cases ys) simp_all
qed simp

lemma prefix_definedD:
  assumes "prefix⋅xs⋅ys = TT"
  shows "xs ≠ ⊥ ∧ ys ≠ ⊥"
using assms by (induct xs arbitrary: ys) auto

lemma prefix_refl[simp]:
  assumes "xs ≠ ⊥"
  shows "prefix⋅xs⋅xs = TT"
using assms by (induct xs) simp_all

lemma prefix_refl_conv[simp]: "(prefix⋅xs⋅xs = TT) ⟷ (xs ≠ ⊥)"
by auto

lemma  prefix_of_snil[simp]: "prefix⋅xs⋅[::] = (case xs of [::] ⇒ TT | x :# xs ⇒ FF)"
by (cases xs) simp_all

lemma prefix_singleton_TT:
  shows "prefix⋅[:x:]⋅ys = TT ⟷ (x ≠ ⊥ ∧ (∃zs. zs ≠ ⊥ ∧ ys = x :# zs))"
by (cases "x = ⊥"; clarsimp; cases ys; fastforce)

lemma prefix_singleton_FF:
  shows "prefix⋅[:x:]⋅ys = FF ⟷ (x ≠ ⊥ ∧ (ys = [::] ∨ (∃z zs. z ≠ ⊥ ∧ zs ≠ ⊥ ∧ ys = z :# zs ∧ x ≠ z)))"
by (cases "x = ⊥"; clarsimp; cases ys; fastforce)

lemma prefix_FF_not_snilD:
  assumes "prefix⋅xs⋅ys = FF"
  shows "xs ≠ [::]"
using assms by (cases xs; cases ys; simp)

lemma prefix_slength:
  assumes "prefix⋅xs⋅ys = TT"
  shows "le⋅(slength⋅xs)⋅(slength⋅ys) = TT"
using assms
proof(induct ys arbitrary: xs)
  case (snil xs) then show ?case by (cases xs) simp_all
next
  case (scons a ys) then show ?case by (cases xs) (simp_all add: le_plus_1)
qed simp

lemma prefix_slength_strengthen: "prefix⋅xs⋅ys = (le⋅(slength⋅xs)⋅(slength⋅ys) andalso prefix⋅xs⋅ys)"
by (rule andalso_weaken_left) (auto dest: prefix_slength)

lemma prefix_scons_snil[simp]: "prefix⋅(x :# xs)⋅[::] ≠ TT"
by (cases "x :# xs ≠ ⊥") auto

lemma scons_prefix_scons[simp]:
  "(prefix⋅(x :# xs)⋅(y :# ys) = TT) ⟷ (eq⋅x⋅y = TT ∧ prefix⋅xs⋅ys = TT)"
by (cases "x :# xs ≠ ⊥ ∧ y :# ys ≠ ⊥") auto

lemma append_prefixD:
  assumes "prefix⋅(xs :@ ys)⋅zs = TT"
  shows "prefix⋅xs⋅zs = TT"
using assms
proof(induct xs arbitrary: zs)
  case (snil zs) then show ?case using prefix.simps(2) by force
next
  case (scons x xs zs) then show ?case
    by (metis prefix.simps(1) prefix_scons_snil sappend_scons scons_prefix_scons slist.exhaust)
qed simp

lemma same_prefix_prefix[simp]:
  assumes "xs ≠ ⊥"
  shows "prefix⋅(xs :@ ys)⋅(xs :@ zs) = prefix⋅ys⋅zs"
using assms
proof(cases "ys = ⊥" "zs = ⊥" rule: bool.exhaust[case_product bool.exhaust])
  case False_False with assms show ?thesis by (induct xs) simp_all
qed simp_all

lemma eq_prefix_TT:
  assumes "eq⋅xs⋅ys = TT"
  shows "prefix⋅xs⋅ys = TT"
using assms by (induct xs arbitrary: ys) (case_tac ys; simp)+

lemma prefix_eq_FF:
  assumes "prefix⋅xs⋅ys = FF"
  shows "eq⋅xs⋅ys = FF"
using assms by (induct xs arbitrary: ys) (case_tac ys; auto)+

lemma prefix_slength_eq:
  shows "eq⋅xs⋅ys = (eq⋅(slength⋅xs)⋅(slength⋅ys) andalso prefix⋅xs⋅ys)"
proof(induct xs arbitrary: ys)
  case (snil ys) then show ?case
    by (cases ys; clarsimp simp: one_Integer_def elim!: slengthE)
next
  case (scons x xs ys) then show ?case
    by (cases ys; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE)
qed simp

lemma stake_slength_plus_1:
  shows "stake⋅(slength⋅xs + 1)⋅(y :# ys) = y :# stake⋅(slength⋅xs)⋅ys"
by (cases "xs = ⊥" "y = ⊥" "ys = ⊥" rule: bool.exhaust[case_product bool.exhaust bool.exhaust]; clarsimp)
   (auto simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE)

lemma sdrop_slength_plus_1:
  assumes "y ≠ ⊥"
  shows "sdrop⋅(slength⋅xs + 1)⋅(y :# ys) = sdrop⋅(slength⋅xs)⋅ys"
using assms
by (subst sdrop.simps;
    cases "xs = ⊥"; clarsimp; cases "ys = ⊥";
    clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE)

lemma eq_take_length_prefix: "prefix⋅xs⋅ys = eq⋅xs⋅(stake⋅(slength⋅xs)⋅ys)"
proof (induct xs arbitrary: ys)
  case (snil ys) show ?case by (cases ys; clarsimp)
next
  case (scons x xs ys)
  note IH = this
  show ?case
  proof (cases "slength⋅xs = ⊥")
    case True then show ?thesis by simp
  next
    case False
    show ?thesis
    proof (cases ys)
      case bottom
      then show ?thesis using False
        using le_slength_plus[of xs 1] by simp
    next
      case snil then show ?thesis using False and IH(1,2) by simp
    next
      case (scons z zs)
      then show ?thesis
        using False and IH(1,2) IH(3)[of zs]
        by (simp add: stake_slength_plus_1 monofun_cfun_arg)
    qed
  qed
qed simp

lemma prefix_sdrop_slength:
  assumes "prefix⋅xs⋅ys = TT"
  shows "xs :@ sdrop⋅(slength⋅xs)⋅ys = ys"
using assms by (induct xs arbitrary: ys) (case_tac ys; simp add: sdrop_slength_plus_1)+

lemma prefix_sdrop_prefix_eq:
  assumes "prefix⋅xs⋅ys = TT"
  shows "eq⋅(sdrop⋅(slength⋅xs)⋅ys)⋅[::] = eq⋅ys⋅xs"
using assms by (induct xs arbitrary: ys) (case_tac ys; simp add: sdrop_slength_plus_1)+
(*<*)

end
(*>*)