Theory Data_List

section ‹Data: List›

theory Data_List
  imports
    Type_Classes
    Data_Function
    Data_Bool
    Data_Tuple
    Data_Integer
    Numeral_Cpo
begin

no_notation (ASCII)
  Set.member  (‹'(:')›) and
  Set.member  (‹(‹notation=‹infix :››_/ : _)› [51, 51] 50)

subsection ‹Datatype definition›

domain 'a list (‹[_]›) =
  Nil (‹[]›) |
  Cons (lazy head :: 'a) (lazy tail :: "['a]") (infixr ‹:› 65)
(*FIXME: We need to standardize a mapping from Haskell fixities
(0 to 9) to Isabelle ones (between 50 and 100).*)


subsubsection ‹Section syntax for @{const Cons}›

syntax
  "_Cons_section" :: "'a → ['a] → ['a]" (‹'(:')›)
  "_Cons_section_left" :: "'a ⇒ ['a] → ['a]" (‹'(_:')›)
syntax_consts
  "_Cons_section_left" == Cons
translations
  "(x:)" == "(CONST Rep_cfun) (CONST Cons) x"

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

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

abbreviation null :: "['a] → tr" where "null ≡ is_Nil"


subsection ‹Haskell function definitions›

instantiation list :: (Eq) Eq_strict
begin

fixrec eq_list :: "['a] → ['a] → tr" where
  "eq_list⋅[]⋅[] = TT" |
  "eq_list⋅(x : xs)⋅[] = FF" |
  "eq_list⋅[]⋅(y : ys) = FF" |
  "eq_list⋅(x : xs)⋅(y : ys) = (eq⋅x⋅y andalso eq_list⋅xs⋅ys)"

instance proof
  fix xs :: "['a]"
  show "eq⋅xs⋅⊥ = ⊥"
    by (cases xs, fixrec_simp+)
  show "eq⋅⊥⋅xs = ⊥"
    by fixrec_simp
qed

end

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

instance list :: (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 (Nil ys zs) then show ?case by (cases ys, simp_all)
  next
    case (Cons x xs ys zs)
    from Cons.prems show ?case
      by (cases ys; cases zs) (auto intro: eq_trans Cons.hyps)
  qed simp_all
qed

instance list :: (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 Nil
    then show ?case by (cases ys) auto
  next
    case Cons
    then show ?case by (cases ys) auto
  qed auto
qed

instantiation list :: (Ord) Ord_strict
begin

fixrec compare_list :: "['a] → ['a] → Ordering" where
  "compare_list⋅[]⋅[] = EQ" |
  "compare_list⋅(x : xs)⋅[] = GT" |
  "compare_list⋅[]⋅(y : ys) = LT" |
  "compare_list⋅(x : xs)⋅(y : ys) =
    thenOrdering⋅(compare⋅x⋅y)⋅(compare_list⋅xs⋅ys)"

instance
  by standard (fixrec_simp, rename_tac x, case_tac x, fixrec_simp+)

end

instance list :: (Ord_linear) Ord_linear
proof
  fix xs ys zs :: "['a]"
  show "oppOrdering⋅(compare⋅xs⋅ys) = compare⋅ys⋅xs"
  proof (induct xs arbitrary: ys)
    case Nil
    show ?case by (cases ys; simp)
  next
    case Cons
    then show ?case by (cases ys; simp add: oppOrdering_thenOrdering)
  qed simp_all
  show "xs = ys" if "compare⋅xs⋅ys = EQ"
    using that
  proof (induct xs arbitrary: ys)
    case Nil
    then show ?case by (cases ys; simp)
  next
    case Cons
    then show ?case by (cases ys; auto elim: compare_EQ_dest)
  qed simp_all
  show "compare⋅xs⋅zs = LT" if "compare⋅xs⋅ys = LT" and "compare⋅ys⋅zs = LT"
    using that
  proof (induct xs arbitrary: ys zs)
    case Nil
    then show ?case by (cases ys; cases zs; simp)
  next
    case (Cons a xs)
    then show ?case
      by (cases ys; cases zs) (auto dest: compare_EQ_dest compare_LT_trans)
  qed simp_all
  show "eq⋅xs⋅ys = is_EQ⋅(compare⋅xs⋅ys)"
  proof (induct xs arbitrary: ys)
    case Nil
    show ?case by (cases ys; simp)
  next
    case Cons
    then show ?case by (cases ys; simp add: eq_conv_compare)
  qed simp_all
  show "compare⋅xs⋅xs ⊑ EQ"
    by (induct xs) simp_all
qed

fixrec zipWith :: "('a → 'b → 'c) → ['a] → ['b] → ['c]" where
  "zipWith⋅f⋅(x : xs)⋅(y : ys) = f⋅x⋅y : zipWith⋅f⋅xs⋅ys" |
  "zipWith⋅f⋅(x : xs)⋅[] = []" |
  "zipWith⋅f⋅[]⋅ys = []"

definition zip :: "['a] → ['b] → [⟨'a, 'b⟩]" where
  "zip = zipWith⋅⟨,⟩"

fixrec zipWith3 :: "('a → 'b → 'c → 'd) → ['a] → ['b] → ['c] → ['d]" where
  "zipWith3⋅f⋅(x : xs)⋅(y : ys)⋅(z : zs) = f⋅x⋅y⋅z : zipWith3⋅f⋅xs⋅ys⋅zs" |
  (unchecked) "zipWith3⋅f⋅xs⋅ys⋅zs = []"

definition zip3 :: "['a] → ['b] → ['c] → [⟨'a, 'b, 'c⟩]" where
  "zip3 = zipWith3⋅⟨,,⟩"

fixrec map :: "('a → 'b) → ['a] → ['b]" where
  "map⋅f⋅[] = []" |
  "map⋅f⋅(x : xs) = f⋅x : map⋅f⋅xs"

fixrec filter :: "('a → tr) → ['a] → ['a]" where
  "filter⋅P⋅[] = []" |
  "filter⋅P⋅(x : xs) =
    If (P⋅x) then x : filter⋅P⋅xs else filter⋅P⋅xs"

fixrec repeat :: "'a → ['a]" where
  [simp del]: "repeat⋅x = x : repeat⋅x"

fixrec takeWhile :: "('a → tr) → ['a] → ['a]" where
 "takeWhile⋅p⋅[]     =  []" |
 "takeWhile⋅p⋅(x:xs) = If p⋅x then x : takeWhile⋅p⋅xs else  []"

fixrec dropWhile :: "('a → tr) → ['a] → ['a]" where
 "dropWhile⋅p⋅[]     =  []" |
 "dropWhile⋅p⋅(x:xs) = If p⋅x then dropWhile⋅p⋅xs else (x:xs)"

fixrec span :: "('a -> tr) -> ['a] -> ⟨['a],['a]⟩" where
 "span⋅p⋅[]     = ⟨[],[]⟩" |
 "span⋅p⋅(x:xs) = If p⋅x then (case span⋅p⋅xs of ⟨ys, zs⟩ ⇒ ⟨x:ys,zs⟩) else ⟨[], x:xs⟩"

fixrec break :: "('a -> tr) -> ['a] -> ⟨['a],['a]⟩" where
 "break⋅p = span⋅(neg oo p)"

fixrec nth :: "['a] → Integer → 'a" where
  "nth⋅[]⋅n = ⊥" |
  nth_Cons [simp del]:
  "nth⋅(x : xs)⋅n = If eq⋅n⋅0 then x else nth⋅xs⋅(n - 1)"
(* bh: Perhaps we should rename this to 'index',
to match the standard Haskell function named 'genericIndex'. *)

abbreviation nth_syn :: "['a] ⇒ Integer ⇒ 'a" (infixl ‹!!› 100) where
  "xs !! n ≡ nth⋅xs⋅n"

definition partition :: "('a → tr) → ['a] → ⟨['a], ['a]⟩" where
  "partition = (Λ P xs. ⟨filter⋅P⋅xs, filter⋅(neg oo P)⋅xs⟩)"

fixrec iterate :: "('a → 'a) → 'a → ['a]" where
  "iterate⋅f⋅x = x : iterate⋅f⋅(f⋅x)"

fixrec foldl ::  "('a -> 'b -> 'a) -> 'a -> ['b] -> 'a" where
  "foldl⋅f⋅z⋅[]     = z" |
  "foldl⋅f⋅z⋅(x:xs) = foldl⋅f⋅(f⋅z⋅x)⋅xs"

fixrec foldl1 ::  "('a -> 'a -> 'a) -> ['a] -> 'a" where
  "foldl1⋅f⋅[]     = ⊥" |
  "foldl1⋅f⋅(x:xs) = foldl⋅f⋅x⋅xs"

fixrec foldr :: "('a → 'b → 'b) → 'b → ['a] → 'b" where
  "foldr⋅f⋅d⋅[] = d" |
  "foldr⋅f⋅d⋅(x : xs) = f⋅x⋅(foldr⋅f⋅d⋅xs)"

fixrec foldr1 :: "('a → 'a → 'a) → ['a] → 'a" where
  "foldr1⋅f⋅[] = ⊥" |
  "foldr1⋅f⋅[x] = x" |
  "foldr1⋅f⋅(x : (x':xs)) = f⋅x⋅(foldr1⋅f⋅(x':xs))"

fixrec elem :: "'a::Eq → ['a] → tr" where
  "elem⋅x⋅[] = FF" |
  "elem⋅x⋅(y : ys) = (eq⋅y⋅x orelse elem⋅x⋅ys)"

fixrec notElem :: "'a::Eq → ['a] → tr" where
  "notElem⋅x⋅[] = TT" |
  "notElem⋅x⋅(y : ys) = (neq⋅y⋅x andalso notElem⋅x⋅ys)"

fixrec append :: "['a] → ['a] → ['a]" where
  "append⋅[]⋅ys = ys" |
  "append⋅(x : xs)⋅ys = x : append⋅xs⋅ys"

abbreviation append_syn :: "['a] ⇒ ['a] ⇒ ['a]" (infixr ‹++› 65) where
  "xs ++ ys ≡ append⋅xs⋅ys"

definition concat :: "[['a]] → ['a]" where
  "concat = foldr⋅append⋅[]"

definition concatMap :: "('a → ['b]) → ['a] → ['b]" where
  "concatMap = (Λ f. concat oo map⋅f)"

fixrec last :: "['a] -> 'a" where
  "last⋅[x] = x" |
  "last⋅(_:(x:xs)) = last⋅(x:xs)"

fixrec init :: "['a] -> ['a]" where
  "init⋅[x] = []" |
  "init⋅(x:(y:xs)) = x:(init⋅(y:xs))"

fixrec reverse :: "['a] -> ['a]" where
  [simp del]:"reverse = foldl⋅(flip⋅(:))⋅[]"

fixrec the_and :: "[tr] → tr" where
  "the_and = foldr⋅trand⋅TT"

fixrec the_or :: "[tr] → tr" where
  "the_or = foldr⋅tror⋅FF"

fixrec all :: "('a → tr) → ['a] → tr" where
  "all⋅P = the_and oo (map⋅P)"

fixrec any :: "('a → tr) → ['a] → tr" where
  "any⋅P = the_or oo (map⋅P)"

fixrec tails :: "['a] → [['a]]" where
  "tails⋅[] = [[]]" |
  "tails⋅(x : xs) = (x : xs) : tails⋅xs"

fixrec inits :: "['a] → [['a]]" where
  "inits⋅[] = [[]]" |
  "inits⋅(x : xs) = [[]] ++ map⋅(x:)⋅(inits⋅xs)"

fixrec scanr :: "('a → 'b → 'b) → 'b → ['a] → ['b]"
where
  "scanr⋅f⋅q0⋅[] = [q0]" |
  "scanr⋅f⋅q0⋅(x : xs) = (
    let qs = scanr⋅f⋅q0⋅xs in
    (case qs of
      [] ⇒ ⊥
    | q : qs' ⇒ f⋅x⋅q : qs))"

fixrec scanr1 :: "('a → 'a → 'a) → ['a] → ['a]"
where
  "scanr1⋅f⋅[] = []" |
  "scanr1⋅f⋅(x : xs) =
    (case xs of
      [] ⇒ [x]
    | x' : xs' ⇒ (
      let qs = scanr1⋅f⋅xs in
      (case qs of
        [] ⇒ ⊥
      | q : qs' ⇒ f⋅x⋅q : qs)))"

fixrec scanl :: "('a → 'b → 'a) → 'a → ['b] → ['a]" where
  "scanl⋅f⋅q⋅ls = q : (case ls of
    [] ⇒ []
  | x : xs ⇒ scanl⋅f⋅(f⋅q⋅x)⋅xs)"

definition scanl1 :: "('a → 'a → 'a) → ['a] → ['a]" where
  "scanl1 = (Λ f ls. (case ls of
    [] ⇒ []
  | x : xs ⇒ scanl⋅f⋅x⋅xs))"

subsubsection ‹Arithmetic Sequences›

fixrec upto :: "Integer → Integer → [Integer]" where
  [simp del]: "upto⋅x⋅y = If le⋅x⋅y then x : upto⋅(x+1)⋅y else []"

fixrec intsFrom :: "Integer → [Integer]" where
  [simp del]: "intsFrom⋅x = seq⋅x⋅(x : intsFrom⋅(x+1))"

class Enum =
  fixes toEnum :: "Integer → 'a"
    and fromEnum :: "'a → Integer"
begin

definition succ :: "'a → 'a" where
  "succ = toEnum oo (+1) oo fromEnum"

definition pred :: "'a → 'a" where
  "pred = toEnum oo (-1) oo fromEnum"

definition enumFrom :: "'a → ['a]" where
  "enumFrom = (Λ x. map⋅toEnum⋅(intsFrom⋅(fromEnum⋅x)))"

definition enumFromTo :: "'a → 'a → ['a]" where
  "enumFromTo = (Λ x y. map⋅toEnum⋅(upto⋅(fromEnum⋅x)⋅(fromEnum⋅y)))"

end

abbreviation enumFrom_To_syn :: "'a::Enum ⇒ 'a ⇒ ['a]" (‹(1[_../_])›) where
  "[m..n] ≡ enumFromTo⋅m⋅n"

abbreviation enumFrom_syn :: "'a::Enum ⇒ ['a]" (‹(1[_..])›) where
  "[n..] ≡ enumFrom⋅n"

instantiation Integer :: Enum
begin
definition [simp]: "toEnum = ID"
definition [simp]: "fromEnum = ID"
instance ..
end

fixrec take :: "Integer → ['a] → ['a]" where
  [simp del]: "take⋅n⋅xs = If le⋅n⋅0 then [] else
    (case xs of [] ⇒ [] | y : ys ⇒ y : take⋅(n - 1)⋅ys)"

fixrec drop :: "Integer → ['a] → ['a]" where
  [simp del]: "drop⋅n⋅xs = If le⋅n⋅0 then xs else
    (case xs of [] ⇒ [] | y : ys ⇒ drop⋅(n - 1)⋅ys)"

fixrec isPrefixOf :: "['a::Eq] → ['a] → tr" where
  "isPrefixOf⋅[]⋅_ = TT" |
  "isPrefixOf⋅(x:xs)⋅[] = FF" |
  "isPrefixOf⋅(x:xs)⋅(y:ys) = (eq⋅x⋅y andalso isPrefixOf⋅xs⋅ys)"

fixrec isSuffixOf :: "['a::Eq] → ['a] → tr" where
  "isSuffixOf⋅x⋅y = isPrefixOf⋅(reverse⋅x)⋅(reverse⋅y)"

fixrec intersperse :: "'a → ['a] → ['a]" where
  "intersperse⋅sep⋅[] = []" |
  "intersperse⋅sep⋅[x] = [x]" |
  "intersperse⋅sep⋅(x:y:xs) = x:sep:intersperse⋅sep⋅(y:xs)"

fixrec intercalate :: "['a] → [['a]] → ['a]" where
  "intercalate⋅xs⋅xss = concat⋅(intersperse⋅xs⋅xss)"

definition replicate :: "Integer → 'a → ['a]" where
  "replicate = (Λ n x. take⋅n⋅(repeat⋅x))"

definition findIndices :: "('a → tr) → ['a] → [Integer]" where
  "findIndices = (Λ P xs.
    map⋅snd⋅(filter⋅(Λ ⟨x, i⟩. P⋅x)⋅(zip⋅xs⋅[0..])))"

fixrec length :: "['a] → Integer" where
  "length⋅[] = 0" |
  "length⋅(x : xs) = length⋅xs + 1"

fixrec delete :: "'a::Eq → ['a] → ['a]" where
  "delete⋅x⋅[] = []" |
  "delete⋅x⋅(y : ys) = If eq⋅x⋅y then ys else y : delete⋅x⋅ys"

fixrec diff :: "['a::Eq] → ['a] → ['a]" where
  "diff⋅xs⋅[] = xs" |
  "diff⋅xs⋅(y : ys) = diff⋅(delete⋅y⋅xs)⋅ys"

abbreviation diff_syn :: "['a::Eq] ⇒ ['a] ⇒ ['a]" (infixl ‹\\› 70) where
  "xs \\\\ ys ≡ diff⋅xs⋅ys"


subsection ‹Logical predicates on lists›

inductive finite_list :: "['a] ⇒ bool" where
  Nil [intro!, simp]: "finite_list []" |
  Cons [intro!, simp]: "⋀x xs. finite_list xs ⟹ finite_list (x : xs)"

inductive_cases finite_listE [elim!]: "finite_list (x : xs)"

lemma finite_list_upwards:
  assumes "finite_list xs" and "xs ⊑ ys"
  shows "finite_list ys"
using assms
proof (induct xs arbitrary: ys)
  case Nil
  then have "ys = []" by (cases ys) simp+
  then show ?case by auto
next
  case (Cons x xs)
  from ‹x : xs ⊑ ys› obtain y ys' where "ys = y : ys'" by (cases ys) auto
  with ‹x : xs ⊑ ys› have "xs ⊑ ys'" by auto
  then have "finite_list ys'" by (rule Cons.hyps)
  with ‹ys = _› show ?case by auto
qed

lemma adm_finite_list [simp]: "adm finite_list"
  by (metis finite_list_upwards adm_upward)

lemma bot_not_finite_list [simp]:
  "finite_list ⊥ = False"
  by (rule, cases rule: finite_list.cases) auto

inductive listmem :: "'a ⇒ ['a] ⇒ bool" where
  "listmem x (x : xs)" |
  "listmem x xs ⟹ listmem x (y : xs)"

lemma listmem_simps [simp]:
  shows "¬ listmem x ⊥" and "¬ listmem x []"
  and "listmem x (y : ys) ⟷ x = y ∨ listmem x ys"
  by (auto elim: listmem.cases intro: listmem.intros)

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

lemma set_simps [simp]:
  shows "set ⊥ = {}" and "set [] = {}"
  and "set (x : xs) = insert x (set xs)"
  unfolding set_def by auto

inductive distinct :: "['a] ⇒ bool" where
  Nil [intro!, simp]: "distinct []" |
  Cons [intro!, simp]: "⋀x xs. distinct xs ⟹ x ∉ set xs ⟹ distinct (x : xs)"


subsection ‹Properties›

lemma map_strict [simp]:
  "map⋅P⋅⊥ = ⊥"
  by (fixrec_simp)

lemma map_ID [simp]:
  "map⋅ID⋅xs = xs"
  by (induct xs) simp_all

lemma enumFrom_intsFrom_conv [simp]:
  "enumFrom = intsFrom"
  by (intro cfun_eqI) (simp add: enumFrom_def)

lemma enumFromTo_upto_conv [simp]:
  "enumFromTo = upto"
  by (intro cfun_eqI) (simp add: enumFromTo_def)

lemma zipWith_strict [simp]:
  "zipWith⋅f⋅⊥⋅ys = ⊥"
  "zipWith⋅f⋅(x : xs)⋅⊥ = ⊥"
  by fixrec_simp+

lemma zip_simps [simp]:
  "zip⋅(x : xs)⋅(y : ys) = ⟨x, y⟩ : zip⋅xs⋅ys"
  "zip⋅(x : xs)⋅[] = []"
  "zip⋅(x : xs)⋅⊥ = ⊥"
  "zip⋅[]⋅ys = []"
  "zip⋅⊥⋅ys = ⊥"
  unfolding zip_def by simp_all

lemma zip_Nil2 [simp]:
  "xs ≠ ⊥ ⟹ zip⋅xs⋅[] = []"
  by (cases xs) simp_all

lemma nth_strict [simp]:
  "nth⋅⊥⋅n = ⊥"
  "nth⋅xs⋅⊥ = ⊥"
  by (fixrec_simp) (cases xs, fixrec_simp+)

lemma upto_strict [simp]:
  "upto⋅⊥⋅y = ⊥"
  "upto⋅x⋅⊥ = ⊥"
  by fixrec_simp+

lemma upto_simps [simp]:
  "n < m ⟹ upto⋅(MkI⋅m)⋅(MkI⋅n) = []"
  "m ≤ n ⟹ upto⋅(MkI⋅m)⋅(MkI⋅n) = MkI⋅m : [MkI⋅m+1..MkI⋅n]"
  by (subst upto.simps, simp)+

lemma filter_strict [simp]:
  "filter⋅P⋅⊥ = ⊥"
  by (fixrec_simp)

lemma nth_Cons_simp [simp]:
  "eq⋅n⋅0 = TT ⟹ nth⋅(x : xs)⋅n = x"
  "eq⋅n⋅0 = FF ⟹ nth⋅(x : xs)⋅n = nth⋅xs⋅(n - 1)"
  by (subst nth.simps, simp)+

lemma nth_Cons_split:
   "P (nth⋅(x : xs)⋅n) = ((eq⋅n⋅0 = FF ⟶ P (nth⋅(x : xs)⋅n)) ∧
                              (eq⋅n⋅0 = TT ⟶ P (nth⋅(x : xs)⋅n)) ∧
                              (n = ⊥ ⟶ P (nth⋅(x : xs)⋅n)))"
(*   "!!x. P (test x) = (~ (∃a b. x = (a, b) & ~ P (test (a, b))))" *)
apply (cases n, simp)
apply (cases "n = 0", simp_all add: zero_Integer_def)
done



lemma nth_Cons_numeral [simp]:
  "(x : xs) !! 0 = x"
  "(x : xs) !! 1 = xs !! 0"
  "(x : xs) !! numeral (Num.Bit0 k) = xs !! numeral (Num.BitM k)"
  "(x : xs) !! numeral (Num.Bit1 k) = xs !! numeral (Num.Bit0 k)"
  by (simp_all add: nth_Cons numeral_Integer_eq
    zero_Integer_def one_Integer_def)

lemma take_strict [simp]:
  "take⋅⊥⋅xs = ⊥"
  by (fixrec_simp)

lemma take_strict_2 [simp]:
  "le⋅1⋅i = TT ⟹ take⋅i⋅⊥ = ⊥"
  by (subst take.simps, cases "le⋅i⋅0") (auto dest: le_trans)

lemma drop_strict [simp]:
  "drop⋅⊥⋅xs = ⊥"
  by (fixrec_simp)

lemma isPrefixOf_strict [simp]:
  "isPrefixOf⋅⊥⋅xs = ⊥"
  "isPrefixOf⋅(x:xs)⋅⊥ = ⊥"
  by (fixrec_simp)+

lemma last_strict[simp]:
  "last⋅⊥= ⊥"
  "last⋅(x:⊥) = ⊥"
  by (fixrec_simp+)

lemma last_nil [simp]:
  "last⋅[] = ⊥"
  by (fixrec_simp)

lemma last_spine_strict: "¬ finite_list xs ⟹ last⋅xs = ⊥"
proof (induct xs)
  case (Cons a xs)
  then show ?case by (cases xs) auto
qed auto

lemma init_strict [simp]:
  "init⋅⊥= ⊥"
  "init⋅(x:⊥) = ⊥"
  by (fixrec_simp+)

lemma init_nil [simp]:
  "init⋅[] = ⊥"
  by (fixrec_simp)

lemma strict_foldr_strict2 [simp]:
  "(⋀x. f⋅x⋅⊥ = ⊥) ⟹ foldr⋅f⋅⊥⋅xs = ⊥"
  by (induct xs, auto) fixrec_simp

lemma foldr_strict [simp]:
  "foldr⋅f⋅d⋅⊥ = ⊥"
  "foldr⋅f⋅⊥⋅[] = ⊥"
  "foldr⋅⊥⋅d⋅(x : xs) = ⊥"
  by fixrec_simp+

lemma foldr_Cons_Nil [simp]:
  "foldr⋅(:)⋅[]⋅xs = xs"
  by (induct xs) simp+

lemma append_strict1 [simp]:
  "⊥ ++ ys = ⊥"
  by fixrec_simp

lemma foldr_append [simp]:
  "foldr⋅f⋅a⋅(xs ++ ys) = foldr⋅f⋅(foldr⋅f⋅a⋅ys)⋅xs"
  by (induct xs) simp+

lemma foldl_strict [simp]:
  "foldl⋅f⋅d⋅⊥ = ⊥"
  "foldl⋅f⋅⊥⋅[] = ⊥"
  by fixrec_simp+

lemma foldr1_strict [simp]:
  "foldr1⋅f⋅⊥= ⊥"
  "foldr1⋅f⋅(x:⊥)= ⊥"
  by fixrec_simp+

lemma foldl1_strict [simp]:
  "foldl1⋅f⋅⊥= ⊥"
  by fixrec_simp

lemma foldl_spine_strict:
  "¬ finite_list xs ⟹ foldl⋅f⋅x⋅xs = ⊥"
  by (induct xs arbitrary: x) auto

lemma foldl_assoc_foldr:
  assumes "finite_list xs"
    and assoc: "⋀x y z. f⋅(f⋅x⋅y)⋅z = f⋅x⋅(f⋅y⋅z)"
    and neutr1: "⋀x. f⋅z⋅x = x"
    and neutr2: "⋀x. f⋅x⋅z = x"
  shows "foldl⋅f⋅z⋅xs = foldr⋅f⋅z⋅xs"
  using ‹finite_list xs›
proof (induct xs)
  case (Cons x xs)
  from ‹finite_list xs› have step: "⋀y. f⋅y⋅(foldl⋅f⋅z⋅xs) = foldl⋅f⋅(f⋅z⋅y)⋅xs"
  proof (induct xs)
    case (Cons x xs y)
    have "f⋅y⋅(foldl⋅f⋅z⋅(x : xs)) = f⋅y⋅(foldl⋅f⋅(f⋅z⋅x)⋅xs)" by auto
    also have "... = f⋅y⋅(f⋅x⋅(foldl⋅f⋅z⋅xs))" by (simp only: Cons.hyps)
    also have "... = f⋅(f⋅y⋅x)⋅(foldl⋅f⋅z⋅xs)" by (simp only: assoc)
    also have "... = foldl⋅f⋅(f⋅z⋅(f⋅y⋅x))⋅xs" by (simp only: Cons.hyps)
    also have "... = foldl⋅f⋅(f⋅(f⋅z⋅y)⋅x)⋅xs" by (simp only: assoc)
    also have "... = foldl⋅f⋅(f⋅z⋅y)⋅(x : xs)" by auto
    finally show ?case.
  qed (simp add: neutr1 neutr2)

  have "foldl⋅f⋅z⋅(x : xs) = foldl⋅f⋅(f⋅z⋅x)⋅xs" by auto
  also have "... = f⋅x⋅(foldl⋅f⋅z⋅xs)" by (simp only: step)
  also have "... = f⋅x⋅(foldr⋅f⋅z⋅xs)" by (simp only: Cons.hyps)
  also have "... = (foldr⋅f⋅z⋅(x:xs))" by auto
  finally show ?case .
qed auto

lemma elem_strict [simp]:
  "elem⋅x⋅⊥ = ⊥"
  by fixrec_simp

lemma notElem_strict [simp]:
  "notElem⋅x⋅⊥ = ⊥"
  by fixrec_simp

lemma list_eq_nil[simp]:
  "eq⋅l⋅[] = TT ⟷ l = []"
  "eq⋅[]⋅l = TT ⟷ l = []"
  by (cases l, auto)+

lemma take_Nil [simp]:
  "n ≠ ⊥ ⟹ take⋅n⋅[] = []"
  by (subst take.simps) (cases "le⋅n⋅0"; simp)

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

lemma take_Cons [simp]:
  "le⋅1⋅i = TT ⟹ take⋅i⋅(x:xs) = x : take⋅(i - 1)⋅xs"
  by (subst take.simps, cases "le⋅i⋅0") (auto dest: le_trans)

lemma take_MkI_Cons [simp]:
  "0 < n ⟹ take⋅(MkI⋅n)⋅(x : xs) = x : take⋅(MkI⋅(n - 1))⋅xs"
  by (subst take.simps) (simp add: zero_Integer_def one_Integer_def)

lemma take_numeral_Cons [simp]:
  "take⋅1⋅(x : xs) = [x]"
  "take⋅(numeral (Num.Bit0 k))⋅(x : xs) = x : take⋅(numeral (Num.BitM k))⋅xs"
  "take⋅(numeral (Num.Bit1 k))⋅(x : xs) = x : take⋅(numeral (Num.Bit0 k))⋅xs"
  by (subst take.simps,
      simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+

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

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

lemma drop_numeral_Cons [simp]:
  "drop⋅1⋅(x : xs) = xs"
  "drop⋅(numeral (Num.Bit0 k))⋅(x : xs) = drop⋅(numeral (Num.BitM k))⋅xs"
  "drop⋅(numeral (Num.Bit1 k))⋅(x : xs) = drop⋅(numeral (Num.Bit0 k))⋅xs"
  by (subst drop.simps,
      simp add: zero_Integer_def one_Integer_def numeral_Integer_eq)+

lemma take_drop_append:
  "take⋅(MkI⋅i)⋅xs ++ drop⋅(MkI⋅i)⋅xs = xs"
proof (cases i)
  case (nonneg n)
  then show ?thesis
  proof (induct n arbitrary : i xs)
    case (Suc n)
    thus ?case
      apply (subst drop.simps)
      apply (subst take.simps)
      apply (cases xs)
        apply (auto simp add: zero_Integer_def one_Integer_def )
      done
  qed simp
next
  case (neg nat)
  then show ?thesis
    apply (subst drop.simps)
    apply (subst take.simps)
    apply (auto simp add: zero_Integer_def one_Integer_def )
    done
qed

lemma take_intsFrom_enumFrom [simp]:
  "take⋅(MkI⋅n)⋅[MkI⋅i..] = [MkI⋅i..MkI⋅(n+i) - 1]"
proof (cases n)
  fix m
  assume "n = int m"
  then show ?thesis
  proof (induct m arbitrary: n i)
    case 0 then show ?case by (simp add: one_Integer_def)
  next
    case (Suc m)
    then have "n - 1 = int m" by simp
    from Suc(1) [OF this]
    have "take⋅(MkI⋅(n - 1))⋅[MkI⋅(i+1)..] = [MkI⋅(i+1)..MkI⋅(n - 1 + (i+1)) - 1]" .
    moreover have "(n - 1) + (i+1) - 1 = n + i - 1" by arith
    ultimately have IH: "take⋅(MkI⋅(n - 1))⋅[MkI⋅(i+1)..] = [MkI⋅(i+1)..MkI⋅(n+i) - 1]" by simp
    from Suc(2) have gt: "n > 0" by simp
    moreover have "[MkI⋅i..] = MkI⋅i : [MkI⋅i + 1..]" by (simp, subst intsFrom.simps) simp
    ultimately
    have *: "take⋅(MkI⋅n)⋅[MkI⋅i..] = MkI⋅i : take⋅(MkI⋅(n - 1))⋅[MkI⋅(i+1)..]"
      by (simp add: one_Integer_def)
    show ?case unfolding IH * using gt by (simp add: one_Integer_def)
  qed
next
  fix m
  assume "n = - int m"
  then have "n ≤ 0" by simp
  then show ?thesis
    by (subst take.simps) (simp add: zero_Integer_def one_Integer_def)
qed

lemma drop_intsFrom_enumFrom [simp]:
  assumes "n ≥ 0"
  shows "drop⋅(MkI⋅n)⋅[MkI⋅i..] = [MkI⋅(n+i)..]"
proof-
  from assms obtain n' where "n = int n'" by (cases n, auto)
  then show ?thesis
    apply(induct n' arbitrary: n i )
     apply simp
    apply (subst intsFrom.simps[unfolded enumFrom_intsFrom_conv[symmetric]])
    apply (subst drop.simps)
    apply (auto simp add: zero_Integer_def one_Integer_def)
    apply (rule cfun_arg_cong)
    apply (rule cfun_arg_cong)
    apply arith
    done
qed

lemma last_append_singleton:
  "finite_list xs ⟹ last⋅(xs ++ [x]) = x"
proof (induct xs rule:finite_list.induct)
  case (Cons x xs)
  then show ?case by (cases xs) auto
qed auto

lemma init_append_singleton:
  "finite_list xs ⟹ init⋅(xs ++ [x]) = xs"
proof (induct xs rule:finite_list.induct)
  case (Cons x xs)
  then show ?case by (cases xs) auto
qed auto

lemma append_Nil2 [simp]:
  "xs ++ [] = xs"
  by (induct xs) simp_all

lemma append_assoc [simp]:
  "(xs ++ ys) ++ zs = xs ++ ys ++ zs"
  by (induct xs) simp_all

lemma concat_simps [simp]:
  "concat⋅[] = []"
  "concat⋅(xs : xss) = xs ++ concat⋅xss"
  "concat⋅⊥ = ⊥"
  unfolding concat_def by simp_all

lemma concatMap_simps [simp]:
  "concatMap⋅f⋅[] = []"
  "concatMap⋅f⋅(x : xs) = f⋅x ++ concatMap⋅f⋅xs"
  "concatMap⋅f⋅⊥ = ⊥"
  unfolding concatMap_def by simp_all

lemma filter_append [simp]:
  "filter⋅P⋅(xs ++ ys) = filter⋅P⋅xs ++ filter⋅P⋅ys"
proof (induct xs)
  case (Cons x xs) then show ?case by (cases "P⋅x") (auto simp: If_and_if)
qed simp_all

lemma elem_append [simp]:
  "elem⋅x⋅(xs ++ ys) = (elem⋅x⋅xs orelse elem⋅x⋅ys)"
    by (induct xs) auto

lemma filter_filter [simp]:
  "filter⋅P⋅(filter⋅Q⋅xs) = filter⋅(Λ x. Q⋅x andalso P⋅x)⋅xs"
  by (induct xs) (auto simp: If2_def [symmetric] split: split_If2)

lemma filter_const_TT [simp]:
  "filter⋅(Λ _. TT)⋅xs = xs"
  by (induct xs) simp_all

lemma tails_strict [simp]:
  "tails⋅⊥ = ⊥"
  by fixrec_simp

lemma inits_strict [simp]:
  "inits⋅⊥ = ⊥"
  by fixrec_simp

lemma the_and_strict [simp]:
  "the_and⋅⊥ = ⊥"
  by fixrec_simp

lemma the_or_strict [simp]:
  "the_or⋅⊥ = ⊥"
  by fixrec_simp

lemma all_strict [simp]:
  "all⋅P⋅⊥ = ⊥"
  by fixrec_simp

lemma any_strict [simp]:
  "any⋅P⋅⊥ = ⊥"
  by fixrec_simp

lemma tails_neq_Nil [simp]:
  "tails⋅xs ≠ []"
  by (cases xs) simp_all

lemma inits_neq_Nil [simp]:
  "inits⋅xs ≠ []"
  by (cases xs) simp_all

lemma Nil_neq_tails [simp]:
  "[] ≠ tails⋅xs"
  by (cases xs) simp_all

lemma Nil_neq_inits [simp]:
  "[] ≠ inits⋅xs"
  by (cases xs) simp_all

lemma finite_list_not_bottom [simp]:
  assumes "finite_list xs" shows "xs ≠ ⊥"
  using assms by (cases) simp_all

lemma head_append [simp]:
  "head⋅(xs ++ ys) = If null⋅xs then head⋅ys else head⋅xs"
  by (cases xs) simp_all

lemma filter_cong:
  "∀x∈set xs. p⋅x = q⋅x ⟹ filter⋅p⋅xs = filter⋅q⋅xs"
proof (induct arbitrary: xs rule: filter.induct)
  case (3 x)
  then show ?case by (cases xs) auto
qed simp_all

lemma filter_TT [simp]:
  assumes "∀x∈set xs. P⋅x = TT"
  shows "filter⋅P⋅xs = xs"
  by (rule filter_cong [of xs P "Λ _. TT", simplified, OF assms])

lemma filter_FF [simp]:
  assumes "finite_list xs"
    and "∀x∈set xs. P⋅x = FF"
  shows "filter⋅P⋅xs = []"
  using assms by (induct xs) simp_all

lemma map_cong:
  "∀x∈set xs. p⋅x = q⋅x ⟹ map⋅p⋅xs = map⋅q⋅xs"
proof (induct arbitrary: xs rule: map.induct)
  case (3 x)
  then show ?case by (cases xs) auto
qed simp_all

lemma finite_list_upto:
  "finite_list (upto⋅(MkI⋅m)⋅(MkI⋅n))" (is "?P m n")
proof (cases "n - m")
  fix d
  assume "n - m = int d"
  then show "?P m n"
  proof (induct d arbitrary: m n)
    case (Suc d)
    then have "n - (m + 1) = int d" and le: "m ≤ n" by simp_all
    from Suc(1) [OF this(1)] have IH: "?P (m+1) n" .
    then show ?case using le by (simp add: one_Integer_def)
  qed (simp add: one_Integer_def)
next
  fix d
  assume "n - m = - int d"
  then have "n ≤ m" by auto
  moreover
  have "?P m n" if "n = m" using that by (simp add: one_Integer_def)
  moreover
  have "?P m n" if "n < m" using that by (simp add: one_Integer_def)
  ultimately show ?thesis by arith
qed

lemma filter_commute:
  assumes "∀x∈set xs. (Q⋅x andalso P⋅x) = (P⋅x andalso Q⋅x)"
  shows "filter⋅P⋅(filter⋅Q⋅xs) = filter⋅Q⋅(filter⋅P⋅xs)"
  using filter_cong [of xs "Λ x. Q⋅x andalso P⋅x" "Λ x. P⋅x andalso Q⋅x"]
    and assms by simp

lemma upto_append_intsFrom [simp]:
  assumes "m ≤ n"
  shows "upto⋅(MkI⋅m)⋅(MkI⋅n) ++ intsFrom⋅(MkI⋅n+1) = intsFrom⋅(MkI⋅m)"
    (is "?u m n ++ _ = ?i m")
proof (cases "n - m")
  case (nonneg i)
  with assms show ?thesis
  proof (induct i arbitrary: m n)
    case (Suc i)
    then have "m + 1 ≤ n" and "n - (m + 1) = int i" by simp_all
    from Suc(1) [OF this]
    have IH: "?u (m+1) n ++ ?i (n+1) = ?i (m+1)" by (simp add: one_Integer_def)
    from ‹m + 1 ≤ n› have "m ≤ n" by simp
    then have "?u m n ++ ?i (n+1) = (MkI⋅m : ?u (m+1) n) ++ ?i (n+1)"
      by (simp add: one_Integer_def)
    also have "… = MkI⋅m : ?i (m+1)" by (simp add: IH)
    finally show ?case by (subst (2) intsFrom.simps) (simp add: one_Integer_def)
  qed (subst (2) intsFrom.simps, simp add: one_Integer_def)
next
  case (neg i)
  then have "n < m" by simp
  with assms show ?thesis by simp
qed

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

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

text ‹This version of definedness rule for Nil is made necessary by
the reorient simproc.›

lemma bottom_neq_Nil [simp]: "⊥ ≠ []"
  by simp

text ‹Simproc to rewrite @{term "Nil = x"} to @{term "x = Nil"}.›

setup ‹
  Reorient_Proc.add
    (fn Const(@{const_name Nil}, _) => true | _ => false)
›

simproc_setup reorient_Nil ("Nil = x") = ‹K Reorient_Proc.proc›


lemma set_append [simp]:
  assumes "finite_list xs"
  shows "set (xs ++ ys) = set xs ∪ set ys"
  using assms by (induct) simp_all

lemma distinct_Cons [simp]:
  "distinct (x : xs) ⟷ distinct xs ∧ x ∉ set xs"
  (is "?l = ?r")
proof
  assume ?l then show ?r by (cases) simp_all
next
  assume ?r then show ?l by auto
qed

lemma finite_list_append [iff]:
  "finite_list (xs ++ ys) ⟷ finite_list xs ∧ finite_list ys"
  (is "?l = ?r")
proof
  presume "finite_list xs" and "finite_list ys"
  then show ?l by (induct) simp_all
next
  assume "?l" then show "?r"
  proof (induct "xs ++ ys" arbitrary: xs ys)
    case (Cons x xs)
    then show ?case by (cases xs) auto
  qed simp
qed simp_all

lemma distinct_append [simp]:
  assumes "finite_list (xs ++ ys)"
  shows "distinct (xs ++ ys) ⟷ distinct xs ∧ distinct ys ∧ set xs ∩ set ys = {}"
    (is "?P xs ys")
  using assms
proof (induct "xs ++ ys" arbitrary: xs ys)
  case Cons': (Cons z zs)
  show ?case
  proof (cases xs)
    case (Cons u us)
    with Cons' have "finite_list us"
      and [simp]: "zs = us ++ ys" "?P us ys" by simp_all
    then show ?thesis by (auto simp: Cons)
  qed (use Cons' in simp_all)
qed simp

lemma finite_set [simp]:
  assumes "distinct xs"
  shows "finite (set xs)"
  using assms by induct auto

lemma distinct_card:
  assumes "distinct xs"
  shows "MkI⋅(int (card (set xs))) = length⋅xs"
  using assms
  by (induct)
     (simp_all add: zero_Integer_def plus_MkI_MkI [symmetric] one_Integer_def ac_simps)

lemma set_delete [simp]:
  fixes xs :: "['a::Eq_eq]"
  assumes "distinct xs"
    and "∀x∈set xs. eq⋅a⋅x ≠ ⊥"
  shows "set (delete⋅a⋅xs) = set xs - {a}"
  using assms
proof induct
  case (Cons x xs)
  then show ?case by (cases "eq⋅a⋅x", force+)
qed simp

lemma distinct_delete [simp]:
  fixes xs :: "['a::Eq_eq]"
  assumes "distinct xs"
    and "∀x∈set xs. eq⋅a⋅x ≠ ⊥"
  shows "distinct (delete⋅a⋅xs)"
  using assms
proof induct
  case (Cons x xs)
  then show ?case by (cases "eq⋅a⋅x", force+)
qed simp

lemma set_diff [simp]:
  fixes xs ys :: "['a::Eq_eq]"
  assumes "distinct ys" and "distinct xs"
    and "∀a∈set ys. ∀x∈set xs. eq⋅a⋅x ≠ ⊥"
  shows "set (xs \\\\ ys) = set xs - set ys"
  using assms
proof (induct arbitrary: xs)
  case Nil then show ?case by (induct xs rule: distinct.induct) simp_all
next
  case (Cons y ys)
  let ?xs = "delete⋅y⋅xs"
  from Cons have *: "∀x∈set xs. eq⋅y⋅x ≠ ⊥" by simp
  from set_delete [OF ‹distinct xs› this]
  have **: "set ?xs = set xs - {y}" .
  with Cons have "∀a∈set ys. ∀x∈set ?xs. eq⋅a⋅x ≠ ⊥" by simp
  moreover from * and ‹distinct xs› have "distinct ?xs" by simp
  ultimately have "set (?xs \\\\ ys) = set ?xs - set ys"
    using Cons by blast
  then show ?case by (force simp: **)
qed

lemma distinct_delete_filter:
  fixes xs :: "['a::Eq_eq]"
  assumes "distinct xs"
    and "∀x∈set xs. eq⋅a⋅x ≠ ⊥"
  shows "delete⋅a⋅xs = filter⋅(Λ x. neq⋅a⋅x)⋅xs"
  using assms
proof (induct)
  case (Cons x xs)
  then have IH: "delete⋅a⋅xs = filter⋅(Λ x. neq⋅a⋅x)⋅xs" by simp
  show ?case
  proof (cases "eq⋅a⋅x")
    case TT
    have "∀x∈set xs. (Λ x. neq⋅a⋅x)⋅x = (Λ _. TT)⋅x"
    proof
      fix y
      assume "y ∈ set xs"
      with Cons(3, 4) have "x ≠ y" and "eq⋅a⋅y ≠ ⊥" by auto
      with TT have "eq⋅a⋅y = FF" by (metis (no_types) eqD(1) trE)
      then show "(Λ x. neq⋅a⋅x)⋅y = (Λ _. TT)⋅y" by simp
    qed
    from filter_cong [OF this] and TT
    show ?thesis by simp
  qed (simp_all add: IH)
qed simp

lemma distinct_diff_filter:
  fixes xs ys :: "['a::Eq_eq]"
  assumes "finite_list ys"
    and "distinct xs"
    and "∀a∈set ys. ∀x∈set xs. eq⋅a⋅x ≠ ⊥"
  shows "xs \\\\ ys = filter⋅(Λ x. neg⋅(elem⋅x⋅ys))⋅xs"
  using assms
proof (induct arbitrary: xs)
  case Nil then show ?case by simp
next
  case (Cons y ys)
  let ?xs = "delete⋅y⋅xs"
  from Cons have *: "∀x∈set xs. eq⋅y⋅x ≠ ⊥" by simp
  from set_delete [OF ‹distinct xs› this]
  have "set ?xs = set xs - {y}" .
  with Cons have "∀a∈set ys. ∀x∈set ?xs. eq⋅a⋅x ≠ ⊥" by simp
  moreover from * and ‹distinct xs› have "distinct ?xs" by simp
  ultimately have "?xs \\\\ ys = filter⋅(Λ x. neg⋅(elem⋅x⋅ys))⋅?xs"
    using Cons by blast
  then show ?case
    using ‹distinct xs› and *
    by (simp add: distinct_delete_filter)
qed

lemma distinct_upto [intro, simp]:
  "distinct [MkI⋅m..MkI⋅n]"
proof (cases "n - m")
  case (nonneg i)
  then show ?thesis
  proof (induct i arbitrary: m)
    case (Suc i)
    then have "n - (m + 1) = int i" and "m ≤ n" by simp_all
    with Suc have "distinct [MkI⋅(m+1)..MkI⋅n]" by force
    with ‹m ≤ n› show ?case by (simp add: one_Integer_def)
  qed (simp add: one_Integer_def)
qed simp

lemma set_intsFrom [simp]:
  "set (intsFrom⋅(MkI⋅m)) = {MkI⋅n | n. m ≤ n}"
  (is "set (?i m) = ?I")
proof
  show "set (?i m) ⊆ ?I"
  proof
    fix n
    assume "n ∈ set (?i m)"
    then have "listmem n (?i m)" by (simp add: set_def)
    then show "n ∈ ?I"
    proof (induct n "(?i m)" arbitrary: m)
      fix x xs m
      assume "x : xs = ?i m"
      then have "x : xs = MkI⋅m : ?i (m+1)"
        by (subst (asm) intsFrom.simps) (simp add: one_Integer_def)
      then have [simp]: "x = MkI⋅m" "xs = ?i (m+1)" by simp_all
      show "x ∈ {MkI⋅n | n. m ≤ n}" by simp
    next
      fix x xs y m
      assume IH: "listmem x xs"
        "⋀m. xs = ?i m ⟹ x ∈ {MkI⋅n | n. m ≤ n}"
        "y : xs = ?i m"
      then have "y : xs = MkI⋅m : ?i (m+1)"
        by (subst (asm) (2) intsFrom.simps) (simp add: one_Integer_def)
      then have [simp]: "y = MkI⋅m" "xs = ?i (m+1)" by simp_all
      from IH (2) [of "m+1"] have "x ∈ {MkI⋅n | n. m+1 ≤ n}" by (simp add: one_Integer_def)
      then show "x ∈ {MkI⋅n | n. m ≤ n}" by force
    qed
  qed
next
  show "?I ⊆ set (?i m)"
  proof
    fix x
    assume "x ∈ ?I"
    then obtain n where [simp]: "x = MkI⋅n" and "m ≤ n" by blast
    from upto_append_intsFrom [OF this(2), symmetric]
    have *: "set (?i m) = set (upto⋅(MkI⋅m)⋅(MkI⋅n)) ∪ set (?i (n+1))"
      using finite_list_upto [of m n] by (simp add: one_Integer_def)
    show "x ∈ set (?i m)" using ‹m ≤ n› by (auto simp: * one_Integer_def)
  qed
qed

lemma If_eq_bottom_iff [simp]: (* FIXME: move *)
  "(If b then x else y = ⊥) ⟷ b = ⊥ ∨ b = TT ∧ x = ⊥ ∨ b = FF ∧ y = ⊥"
  by (induct b) simp_all

lemma upto_eq_bottom_iff [simp]:
  "upto⋅m⋅n = ⊥ ⟷ m = ⊥ ∨ n = ⊥"
  by (subst upto.simps, simp)

lemma seq_eq_bottom_iff [simp]: (* FIXME: move *)
  "seq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (simp add: seq_conv_if)

lemma intsFrom_eq_bottom_iff [simp]:
  "intsFrom⋅m = ⊥ ⟷ m = ⊥"
  by (subst intsFrom.simps, simp)

lemma intsFrom_split:
  assumes "m ≥ n"
  shows "[MkI⋅n..] = [MkI⋅n .. MkI⋅(m - 1)] ++ [MkI⋅m..]"
proof-
  from assms have ge: "m - n ≥ 0" by arith
  have "[MkI⋅n..] = (take⋅(MkI⋅(m - n)) ⋅ [MkI⋅n..]) ++ (drop⋅(MkI⋅(m - n)) ⋅ [MkI⋅n..])"
    by (subst take_drop_append, rule)
  also have "... = [MkI⋅n.. MkI⋅(m - 1)] ++ [MkI⋅m..]"
    by (subst drop_intsFrom_enumFrom[OF ge], auto simp add:take_intsFrom_enumFrom[simplified] one_Integer_def)
  finally show ?thesis .
qed

lemma filter_fast_forward:
  assumes "n+1 ≤ n'"
    and  "∀k . n < k ⟶ k < n' ⟶ ¬ P k"
  shows "filter⋅(Λ (MkI⋅i) . Def (P i))⋅[MkI⋅(n+1)..] = filter⋅(Λ (MkI⋅i) . Def (P i))⋅[MkI⋅n'..]"
proof-
  from assms(1)
  have"[MkI⋅(n+1)..] = [MkI⋅(n+1).. MkI⋅(n'- 1)] ++ [MkI⋅n'..]" (is "_ = ?l1 ++ ?l2")
    by (subst intsFrom_split[of "n+1" n'], auto)
  moreover
  have "filter⋅(Λ (MkI⋅i) . Def (P i))⋅[MkI⋅(n+1).. MkI⋅(n'- 1)] = []"
    apply (rule filter_FF)
     apply (simp, rule finite_list_upto)
    using assms(2)
    apply auto
    done
  ultimately
  show ?thesis by simp
qed

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

lemma null_set_empty_conv:
  "xs ≠ ⊥ ⟹ null⋅xs = TT ⟷ set xs = {}"
  by (cases xs) simp_all

lemma elem_TT [simp]:
  fixes x :: "'a::Eq_eq" shows "elem⋅x⋅xs = TT ⟹ x ∈ set xs"
  apply (induct arbitrary: xs rule: elem.induct, simp_all)
  apply (rename_tac xs, case_tac xs, simp_all)
  apply (rename_tac a list, case_tac "eq⋅a⋅x", force+)
  done

lemma elem_FF [simp]:
  fixes x :: "'a::Eq_equiv" shows "elem⋅x⋅xs = FF ⟹ x ∉ set xs"
  by (induct arbitrary: xs rule: elem.induct, simp_all)
     (rename_tac xs, case_tac xs, simp_all, force)

lemma length_strict [simp]:
  "length⋅⊥ = ⊥"
  by (fixrec_simp)

lemma repeat_neq_bottom [simp]:
  "repeat⋅x ≠ ⊥"
  by (subst repeat.simps) simp

lemma list_case_repeat [simp]:
  "list_case⋅a⋅f⋅(repeat⋅x) = f⋅x⋅(repeat⋅x)"
  by (subst repeat.simps) simp

lemma length_append [simp]:
  "length⋅(xs ++ ys) = length⋅xs + length⋅ys"
  by (induct xs) (simp_all add: ac_simps)

lemma replicate_strict [simp]:
  "replicate⋅⊥⋅x = ⊥"
  by (simp add: replicate_def)

lemma replicate_0 [simp]:
  "replicate⋅0⋅x = []"
  "replicate⋅(MkI⋅0)⋅xs = []"
  by (simp add: replicate_def)+

lemma Integer_add_0 [simp]: "MkI⋅0 + n = n"
  by (cases n) simp_all

lemma replicate_MkI_plus_1 [simp]:
  "0 ≤ n ⟹ replicate⋅(MkI⋅(n+1))⋅x = x : replicate⋅(MkI⋅n)⋅x"
  "0 ≤ n ⟹ replicate⋅(MkI⋅(1+n))⋅x = x : replicate⋅(MkI⋅n)⋅x"
  by (simp add: replicate_def, subst take.simps, simp add: one_Integer_def zero_Integer_def)+

lemma replicate_append_plus_conv:
  assumes "0 ≤ m" and "0 ≤ n"
  shows "replicate⋅(MkI⋅m)⋅x ++ replicate⋅(MkI⋅n)⋅x
    = replicate⋅(MkI⋅m + MkI⋅n)⋅x"
proof (cases m)
  case (nonneg i)
  with assms show ?thesis
  proof (induct i arbitrary: m)
    case (Suc i)
    then have ge: "int i + n ≥ 0" by force
    have "replicate⋅(MkI⋅m)⋅x ++ replicate⋅(MkI⋅n)⋅x = x : (replicate⋅(MkI⋅(int i))⋅x ++ replicate⋅(MkI⋅n)⋅x)" by (simp add: Suc)
    also have "… = x : replicate⋅(MkI⋅(int i) + MkI⋅n)⋅x" using Suc by simp
    finally show ?case using ge by (simp add: Suc ac_simps)
  qed simp
next
  case (neg i)
  with assms show ?thesis by simp
qed

lemma replicate_MkI_1 [simp]:
  "replicate⋅(MkI⋅1)⋅x = x : []"
  by (simp add: replicate_def, subst take.simps, simp add: zero_Integer_def one_Integer_def)

lemma length_replicate [simp]:
  assumes "0 ≤ n"
  shows "length⋅(replicate⋅(MkI⋅n)⋅x) = MkI⋅n"
proof (cases n)
  case (nonneg i)
  with assms show ?thesis
    by (induct i arbitrary: n)
       (simp_all add: replicate_append_plus_conv zero_Integer_def one_Integer_def)
next
  case (neg i)
  with assms show ?thesis by (simp add: replicate_def)
qed

lemma map_oo [simp]:
  "map⋅f⋅(map⋅g⋅xs) = map⋅(f oo g)⋅xs"
  by (induct xs) simp_all

lemma nth_Cons_MkI [simp]:
  "0 < i ⟹ (a : xs) !! (MkI⋅i) = xs !! (MkI⋅(i - 1))"
  unfolding nth_Cons
  by (cases i, simp add: zero_Integer_def one_Integer_def) (case_tac n, simp_all)

lemma map_plus_intsFrom:
  "map⋅(+ MkI⋅n)⋅(intsFrom⋅(MkI⋅m)) = intsFrom⋅(MkI⋅(m+n))" (is "?l = ?r")
proof (rule list.take_lemma)
  fix i show "list_take i⋅?l = list_take i⋅?r"
  proof (induct i arbitrary: m)
    case (Suc i) then show ?case
      by (subst (1 2) intsFrom.simps) (simp add: ac_simps one_Integer_def)
  qed simp
qed

lemma plus_eq_MkI_conv:
  "l + n = MkI⋅m ⟷ (∃l' n'. l = MkI⋅l' ∧ n = MkI⋅n' ∧ m = l' + n')"
  by (cases l, simp) (cases n, auto)

lemma length_ge_0:
  "length⋅xs = MkI⋅n ⟹ n ≥ 0"
  by (induct xs arbitrary: n) (auto simp: one_Integer_def plus_eq_MkI_conv)

lemma length_0_conv [simp]:
  "length⋅xs = MkI⋅0 ⟷ xs = []"
  apply (cases xs)
    apply (simp_all add: one_Integer_def)
  apply (case_tac "length⋅list")
   apply (auto dest: length_ge_0)
  done

lemma length_ge_1 [simp]:
  "length⋅xs = MkI⋅(1 + int n)
    ⟷ (∃u us. xs = u : us ∧ length⋅us = MkI⋅(int n))"
  (is "?l = ?r")
proof
  assume ?r then show ?l by (auto simp: one_Integer_def)
next
  assume 1: ?l
  then obtain u us where [simp]: "xs = u : us" by (cases xs) auto
  from 1 have 2: "1 + length⋅us = MkI⋅(1 + int n)" by (simp add: ac_simps)
  then have "length⋅us ≠ ⊥" by (cases "length⋅us") simp_all
  moreover from 2 have "length⋅us + 1 = MkI⋅(int n) + 1" by (simp add: one_Integer_def ac_simps)
  ultimately have "length⋅us = MkI⋅(int n)"
    by (cases "length⋅us") (simp_all add: one_Integer_def)
  then show ?r by simp
qed

lemma finite_list_length_conv:
  "finite_list xs ⟷ (∃n. length⋅xs = MkI⋅(int n))" (is "?l = ?r")
proof
  assume "?l" then show "?r"
    by (induct, auto simp: one_Integer_def) presburger
next
  assume "?r"
  then obtain n where "length⋅xs = MkI⋅(int n)" by blast
  then show "?l" by (induct n arbitrary: xs) auto
qed

lemma nth_append:
  assumes "length⋅xs = MkI⋅n" and "n ≤ m"
  shows "(xs ++ ys) !! MkI⋅m = ys !! MkI⋅(m - n)"
  using assms
proof (induct xs arbitrary: n m)
  case (Cons x xs)
  then have ge: "n ≥ 0" by (blast intro: length_ge_0)
  from Cons(2)
  have len: "length⋅xs = MkI⋅(n - 1)"
    by (auto simp: plus_eq_MkI_conv one_Integer_def)
  from Cons(3) have le: "n - 1 ≤ m - 1" by simp
  consider "m < 0" | "m = 0" | "m > 0" by arith
  then show ?case
  proof cases
    case 1
    with ge show ?thesis using Cons(3) by simp
  next
    case 2
    with Cons(3) and ge have "n = 0" by simp
    with Cons(2) show ?thesis
      by (auto dest: length_ge_0 simp: one_Integer_def plus_eq_MkI_conv)
  next
    case 3
    then show ?thesis
      by (auto simp: Cons(1) [OF len le] zero_Integer_def one_Integer_def)
  qed
qed (simp_all add: zero_Integer_def)

lemma replicate_nth [simp]:
  assumes "0 ≤ n"
  shows "(replicate⋅(MkI⋅n)⋅x ++ xs) !! MkI⋅n = xs !! MkI⋅0"
  using nth_append [OF length_replicate [OF assms], of n]
    by simp

lemma map2_zip:
  "map⋅(Λ⟨x, y⟩. ⟨x, f⋅y⟩)⋅(zip⋅xs⋅ys) = zip⋅xs⋅(map⋅f⋅ys)"
  by (induct xs arbitrary: ys) (simp_all, case_tac ys, simp_all)

lemma map2_filter:
  "map⋅(Λ⟨x, y⟩. ⟨x, f⋅y⟩)⋅(filter⋅(Λ⟨x, y⟩. P⋅x)⋅xs)
    = filter⋅(Λ⟨x, y⟩. P⋅x)⋅(map⋅(Λ⟨x, y⟩. ⟨x, f⋅y⟩)⋅xs)"
  apply (induct xs, simp_all)
  apply (rename_tac x xs, case_tac x, simp, simp)
  apply (rename_tac a b, case_tac "P⋅a", auto)
done

lemma map_map_snd:
  "f⋅⊥ = ⊥ ⟹ map⋅f⋅(map⋅snd⋅xs)
    = map⋅snd⋅(map⋅(Λ⟨x, y⟩. ⟨x, f⋅y⟩)⋅xs)"
  by (induct xs, simp_all, rename_tac a b, case_tac a, simp_all)

lemma findIndices_Cons [simp]:
  "findIndices⋅P⋅(a : xs) =
    If P⋅a then 0 : map⋅(+1)⋅(findIndices⋅P⋅xs)
    else map⋅(+1)⋅(findIndices⋅P⋅xs)"
  by (auto simp: findIndices_def, subst intsFrom.simps, cases "P⋅a")
     (simp_all
       del: map_oo
       add: map_oo [symmetric] map_map_snd one_Integer_def zero_Integer_def
       map_plus_intsFrom [of 1 0, simplified, symmetric]
       map2_zip [of "(+ MkI⋅1)", simplified]
       map2_filter [of "(+ MkI⋅1)", simplified])

lemma filter_alt_def:
  fixes xs :: "['a]"
  shows "filter⋅P⋅xs = map⋅(nth⋅xs)⋅(findIndices⋅P⋅xs)"
proof -
  have 1: "map⋅f⋅(map⋅snd⋅(filter⋅(Λ⟨x, i⟩. P⋅x)⋅(zip⋅xs⋅[MkI⋅i..])))
    = map⋅g⋅(map⋅snd⋅(filter⋅(Λ⟨x, i⟩. P⋅x)⋅(zip⋅xs⋅[MkI⋅i..])))"
    if "∀j≥i. f⋅(MkI⋅j) = g⋅(MkI⋅j)"
    for f g :: "Integer → 'a"
      and P :: "'a → tr"
      and i xs
    using that
    by (induct xs arbitrary: i, simp_all, subst (1 2) intsFrom.simps)
      (rename_tac a b c, case_tac "P⋅a", simp_all add: one_Integer_def)
  have 2: "∀i≥0. nth⋅ys⋅(MkI⋅i) = (nth⋅(a : ys) oo (+1))⋅(MkI⋅i)"
    for a and ys :: "['a]"
    by (auto simp: one_Integer_def zero_Integer_def)
  have 3: "map⋅(nth⋅(a : ys) oo (+1))⋅(findIndices⋅P⋅xs)
    = map⋅(nth⋅ys)⋅(findIndices⋅P⋅xs)"
    for a P and ys xs :: "['a]"
    by (simp add: findIndices_def 1 [OF 2, simplified, of ys P xs a] zero_Integer_def)
  show ?thesis
    by (induct xs, simp_all, simp add: findIndices_def, simp add: findIndices_def)
       (rename_tac a b, case_tac "P⋅a", simp add: findIndices_def, simp_all add: 3)
qed

abbreviation cfun_image :: "('a → 'b) ⇒ 'a set ⇒ 'b set" (infixr ‹`⋅› 90) where
  "f `⋅ A ≡ Rep_cfun f ` A"

lemma set_map:
  "set (map⋅f⋅xs) = f `⋅ set xs" (is "?l = ?r")
proof
  have "listmem (f⋅a) (map⋅f⋅xs)" if "listmem a xs" for a
    using that by (induct) simp_all
  then show "?r ⊆ ?l" by (auto simp: set_def)
next
  have "∃b. a = f⋅b ∧ listmem b xs" if "listmem a (map⋅f⋅xs)" for a
    using that
    by (induct a "map⋅f⋅xs" arbitrary: xs)
       (rename_tac xsa, case_tac xsa, auto)+
  then show "?l ⊆ ?r" unfolding set_def by auto
qed


subsection ‹@{const reverse} and @{const reverse} induction›

text ‹Alternative simplification rules for @{const reverse} (easier
to use for equational reasoning):›
lemma reverse_Nil [simp]:
  "reverse⋅[] = []"
  by (simp add: reverse.simps)

lemma reverse_singleton [simp]:
  "reverse⋅[x] = [x]"
  by (simp add: reverse.simps)

lemma reverse_strict [simp]:
  "reverse⋅⊥ = ⊥"
  by (simp add: reverse.simps)

lemma foldl_flip_Cons_append:
  "foldl⋅(flip⋅(:))⋅ys⋅xs = foldl⋅(flip⋅(:))⋅[]⋅xs ++ ys"
proof (induct xs arbitrary: ys)
  case (Cons x xs)
  show ?case by simp (metis (no_types) Cons append.simps append_assoc)
qed simp+

lemma reverse_Cons [simp]:
  "reverse⋅(x:xs) = reverse⋅xs ++ [x]"
  by (simp add: reverse.simps)
     (subst foldl_flip_Cons_append, rule refl)

lemma reverse_append_below:
  "reverse⋅(xs ++ ys) ⊑ reverse⋅ys ++ reverse⋅xs"
  apply (induction xs)
     apply (simp del: append_assoc add: append_assoc [symmetric])+
  apply (blast intro: monofun_cfun append_assoc)
  done

lemma reverse_reverse_below:
  "reverse⋅(reverse⋅xs) ⊑ xs"
proof (induction xs)
  case (Cons x xs)
  have "reverse⋅(reverse⋅(x:xs)) = reverse⋅(reverse⋅xs ++ [x])" by simp
  also have "… ⊑ reverse⋅[x] ++ reverse⋅(reverse⋅xs)" by (rule reverse_append_below)
  also have "… = x : reverse⋅(reverse⋅xs)" by simp
  also have "… ⊑ x : xs" by (simp add: Cons)
  finally show ?case .
qed simp+

lemma reverse_append [simp]:
  assumes "finite_list xs"
  shows "reverse⋅(xs ++ ys) = reverse⋅ys ++ reverse⋅xs"
  using assms by (induct xs) simp+

lemma reverse_spine_strict:
  "¬ finite_list xs ⟹ reverse⋅xs = ⊥"
  by (auto simp add: reverse.simps foldl_spine_strict)

lemma reverse_finite [simp]:
  assumes "finite_list xs" shows "finite_list (reverse⋅xs)"
  using assms by (induct xs) simp+

lemma reverse_reverse [simp]:
  assumes "finite_list xs" shows "reverse⋅(reverse⋅xs) = xs"
  using assms by (induct xs) simp+

lemma reverse_induct [consumes 1, case_names Nil snoc]:
  "⟦finite_list xs; P []; ⋀x xs . finite_list xs ⟹ P xs ⟹ P (xs ++ [x])⟧ ⟹ P xs"
  apply (subst reverse_reverse [symmetric])
   apply assumption
  apply (rule finite_list.induct[where x = "reverse⋅xs"])
    apply simp+
  done

lemma length_plus_not_0:
  "le⋅1⋅n = TT ⟹ le⋅(length⋅xs + n)⋅0 = TT ⟹ False"
proof (induct xs arbitrary: n)
  case Nil then show ?case
    by auto (metis Ord_linear_class.le_trans dist_eq_tr(3) le_Integer_numeral_simps(3))
next
  case (Cons x xs)
  from Cons(1) [of "n + 1"] show ?case
    using Cons(2-) by (auto simp: ac_simps dest: le_plus_1)
qed simp+

lemma take_length_plus_1:
  "length⋅xs ≠ ⊥ ⟹ take⋅(length⋅xs + 1)⋅(y:ys) = y : take⋅(length⋅xs)⋅ys"
  by (subst take.simps, cases "le⋅(length⋅xs + 1)⋅0")
     (auto, metis (no_types) length_plus_not_0 le_Integer_numeral_simps(4))

lemma le_length_plus:
  "length⋅xs ≠ ⊥ ⟹ n ≠ ⊥ ⟹ le⋅n⋅(length⋅xs + n) = TT"
proof (induct xs arbitrary: n)
  case (Cons x xs)
  then have "le⋅(n + 1)⋅(length⋅xs + (n + 1)) = TT" by simp
  moreover have "le⋅n⋅(n + 1) = TT" using ‹n ≠ ⊥› by (metis le_plus_1 le_refl_Integer)
  ultimately have "le⋅n⋅(length⋅xs + (n + 1)) = TT" by (blast dest: le_trans)
  then show ?case by (simp add: ac_simps)
qed simp+

lemma eq_take_length_isPrefixOf:
  "eq⋅xs⋅(take⋅(length⋅xs)⋅ys) ⊑ isPrefixOf⋅xs⋅ys"
proof (induct xs arbitrary: ys)
  case IH: (Cons x xs)
  show ?case
  proof (cases "length⋅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_length_plus [of xs 1] by simp
    next
      case Nil then show ?thesis using False by simp
    next
      case (Cons z zs)
      then show ?thesis
        using False and IH [of zs]
        by (simp add: take_length_plus_1 monofun_cfun_arg)
    qed
  qed
qed simp+

end