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  ("(_/ : _)" [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]" ("'(_:')")
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]" ("[(_)]")
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) = (eqxy andalso eq_listxsys)"

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

end

instance list :: (Eq_sym) Eq_sym
proof
  fix xs ys :: "['a]"
  show "eqxsys = eqysxs"
  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 "eqxsxs  FF"
    by (induct xs, simp_all)
  assume "eqxsys = TT" and "eqyszs = TT" then show "eqxszs = 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 "eqxsxs  FF"
    by (induct xs) simp_all
  assume "eqxsys = 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(comparexy)(compare_listxsys)"

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(comparexsys) = compareysxs"
  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 "comparexsys = 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 "comparexszs = LT" if "comparexsys = LT" and "compareyszs = 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 "eqxsys = is_EQ(comparexsys)"
  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 "comparexsxs  EQ"
    by (induct xs) simp_all
qed

fixrec zipWith :: "('a  'b  'c)  ['a]  ['b]  ['c]" where
  "zipWithf(x : xs)(y : ys) = fxy : zipWithfxsys" |
  "zipWithf(x : xs)[] = []" |
  "zipWithf[]ys = []"

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

fixrec zipWith3 :: "('a  'b  'c  'd)  ['a]  ['b]  ['c]  ['d]" where
  "zipWith3f(x : xs)(y : ys)(z : zs) = fxyz : zipWith3fxsyszs" |
  (unchecked) "zipWith3fxsyszs = []"

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

fixrec map :: "('a  'b)  ['a]  ['b]" where
  "mapf[] = []" |
  "mapf(x : xs) = fx : mapfxs"

fixrec filter :: "('a  tr)  ['a]  ['a]" where
  "filterP[] = []" |
  "filterP(x : xs) =
    If (Px) then x : filterPxs else filterPxs"

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

fixrec takeWhile :: "('a  tr)  ['a]  ['a]" where
 "takeWhilep[]     =  []" |
 "takeWhilep(x:xs) = If px then x : takeWhilepxs else  []"

fixrec dropWhile :: "('a  tr)  ['a]  ['a]" where
 "dropWhilep[]     =  []" |
 "dropWhilep(x:xs) = If px then dropWhilepxs else (x:xs)"

fixrec span :: "('a -> tr) -> ['a] -> ['a],['a]" where
 "spanp[]     = [],[]" |
 "spanp(x:xs) = If px then (case spanpxs of ys, zs  x:ys,zs) else [], x:xs"

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

fixrec nth :: "['a]  Integer  'a" where
  "nth[]n = " |
  nth_Cons [simp del]:
  "nth(x : xs)n = If eqn0 then x else nthxs(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  nthxsn"

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

fixrec iterate :: "('a  'a)  'a  ['a]" where
  "iteratefx = x : iteratef(fx)"

fixrec foldl ::  "('a -> 'b -> 'a) -> 'a -> ['b] -> 'a" where
  "foldlfz[]     = z" |
  "foldlfz(x:xs) = foldlf(fzx)xs"

fixrec foldl1 ::  "('a -> 'a -> 'a) -> ['a] -> 'a" where
  "foldl1f[]     = " |
  "foldl1f(x:xs) = foldlfxxs"

fixrec foldr :: "('a  'b  'b)  'b  ['a]  'b" where
  "foldrfd[] = d" |
  "foldrfd(x : xs) = fx(foldrfdxs)"

fixrec foldr1 :: "('a  'a  'a)  ['a]  'a" where
  "foldr1f[] = " |
  "foldr1f[x] = x" |
  "foldr1f(x : (x':xs)) = fx(foldr1f(x':xs))"

fixrec elem :: "'a::Eq  ['a]  tr" where
  "elemx[] = FF" |
  "elemx(y : ys) = (eqyx orelse elemxys)"

fixrec notElem :: "'a::Eq  ['a]  tr" where
  "notElemx[] = TT" |
  "notElemx(y : ys) = (neqyx andalso notElemxys)"

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

abbreviation append_syn :: "['a]  ['a]  ['a]" (infixr "++" 65) where
  "xs ++ ys  appendxsys"

definition concat :: "[['a]]  ['a]" where
  "concat = foldrappend[]"

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

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 = foldrtrandTT"

fixrec the_or :: "[tr]  tr" where
  "the_or = foldrtrorFF"

fixrec all :: "('a  tr)  ['a]  tr" where
  "allP = the_and oo (mapP)"

fixrec any :: "('a  tr)  ['a]  tr" where
  "anyP = the_or oo (mapP)"

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

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

fixrec scanr :: "('a  'b  'b)  'b  ['a]  ['b]"
where
  "scanrfq0[] = [q0]" |
  "scanrfq0(x : xs) = (
    let qs = scanrfq0xs in
    (case qs of
      []  
    | q : qs'  fxq : qs))"

fixrec scanr1 :: "('a  'a  'a)  ['a]  ['a]"
where
  "scanr1f[] = []" |
  "scanr1f(x : xs) =
    (case xs of
      []  [x]
    | x' : xs'  (
      let qs = scanr1fxs in
      (case qs of
        []  
      | q : qs'  fxq : qs)))"

fixrec scanl :: "('a  'b  'a)  'a  ['b]  ['a]" where
  "scanlfqls = q : (case ls of
    []  []
  | x : xs  scanlf(fqx)xs)"

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

subsubsection ‹Arithmetic Sequences›

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

fixrec intsFrom :: "Integer  [Integer]" where
  [simp del]: "intsFromx = seqx(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. maptoEnum(intsFrom(fromEnumx)))"

definition enumFromTo :: "'a  'a  ['a]" where
  "enumFromTo = (Λ x y. maptoEnum(upto(fromEnumx)(fromEnumy)))"

end

abbreviation enumFrom_To_syn :: "'a::Enum  'a  ['a]" ("(1[_../_])") where
  "[m..n]  enumFromTomn"

abbreviation enumFrom_syn :: "'a::Enum  ['a]" ("(1[_..])") where
  "[n..]  enumFromn"

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

fixrec take :: "Integer  ['a]  ['a]" where
  [simp del]: "takenxs = If len0 then [] else
    (case xs of []  [] | y : ys  y : take(n - 1)ys)"

fixrec drop :: "Integer  ['a]  ['a]" where
  [simp del]: "dropnxs = If len0 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) = (eqxy andalso isPrefixOfxsys)"

fixrec isSuffixOf :: "['a::Eq]  ['a]  tr" where
  "isSuffixOfxy = isPrefixOf(reversex)(reversey)"

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

fixrec intercalate :: "['a]  [['a]]  ['a]" where
  "intercalatexsxss = concat(interspersexsxss)"

definition replicate :: "Integer  'a  ['a]" where
  "replicate = (Λ n x. taken(repeatx))"

definition findIndices :: "('a  tr)  ['a]  [Integer]" where
  "findIndices = (Λ P xs.
    mapsnd(filter(Λ x, i. Px)(zipxs[0..])))"

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

fixrec delete :: "'a::Eq  ['a]  ['a]" where
  "deletex[] = []" |
  "deletex(y : ys) = If eqxy then ys else y : deletexys"

fixrec diff :: "['a::Eq]  ['a]  ['a]" where
  "diffxs[] = xs" |
  "diffxs(y : ys) = diff(deleteyxs)ys"

abbreviation diff_syn :: "['a::Eq]  ['a]  ['a]" (infixl "\\\\" 70) where
  "xs \\\\ ys  diffxsys"


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]:
  "mapP = "
  by (fixrec_simp)

lemma map_ID [simp]:
  "mapIDxs = 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]:
  "zipWithfys = "
  "zipWithf(x : xs) = "
  by fixrec_simp+

lemma zip_simps [simp]:
  "zip(x : xs)(y : ys) = x, y : zipxsys"
  "zip(x : xs)[] = []"
  "zip(x : xs) = "
  "zip[]ys = []"
  "zipys = "
  unfolding zip_def by simp_all

lemma zip_Nil2 [simp]:
  "xs    zipxs[] = []"
  by (cases xs) simp_all

lemma nth_strict [simp]:
  "nthn = "
  "nthxs = "
  by (fixrec_simp) (cases xs, fixrec_simp+)

lemma upto_strict [simp]:
  "uptoy = "
  "uptox = "
  by fixrec_simp+

lemma upto_simps [simp]:
  "n < m  upto(MkIm)(MkIn) = []"
  "m  n  upto(MkIm)(MkIn) = MkIm : [MkIm+1..MkIn]"
  by (subst upto.simps, simp)+

lemma filter_strict [simp]:
  "filterP = "
  by (fixrec_simp)

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

lemma nth_Cons_split:
   "P (nth(x : xs)n) = ((eqn0 = FF  P (nth(x : xs)n)) 
                              (eqn0 = 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]:
  "takexs = "
  by (fixrec_simp)

lemma take_strict_2 [simp]:
  "le1i = TT  takei = "
  by (subst take.simps, cases "lei0") (auto dest: le_trans)

lemma drop_strict [simp]:
  "dropxs = "
  by (fixrec_simp)

lemma isPrefixOf_strict [simp]:
  "isPrefixOfxs = "
  "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  lastxs = "
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. fx = )  foldrfxs = "
  by (induct xs, auto) fixrec_simp

lemma foldr_strict [simp]:
  "foldrfd = "
  "foldrf[] = "
  "foldrd(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]:
  "foldrfa(xs ++ ys) = foldrf(foldrfays)xs"
  by (induct xs) simp+

lemma foldl_strict [simp]:
  "foldlfd = "
  "foldlf[] = "
  by fixrec_simp+

lemma foldr1_strict [simp]:
  "foldr1f= "
  "foldr1f(x:)= "
  by fixrec_simp+

lemma foldl1_strict [simp]:
  "foldl1f= "
  by fixrec_simp

lemma foldl_spine_strict:
  "¬ finite_list xs  foldlfxxs = "
  by (induct xs arbitrary: x) auto

lemma foldl_assoc_foldr:
  assumes "finite_list xs"
    and assoc: "x y z. f(fxy)z = fx(fyz)"
    and neutr1: "x. fzx = x"
    and neutr2: "x. fxz = x"
  shows "foldlfzxs = foldrfzxs"
  using finite_list xs
proof (induct xs)
  case (Cons x xs)
  from finite_list xs have step: "y. fy(foldlfzxs) = foldlf(fzy)xs"
  proof (induct xs)
    case (Cons x xs y)
    have "fy(foldlfz(x : xs)) = fy(foldlf(fzx)xs)" by auto
    also have "... = fy(fx(foldlfzxs))" by (simp only: Cons.hyps)
    also have "... = f(fyx)(foldlfzxs)" by (simp only: assoc)
    also have "... = foldlf(fz(fyx))xs" by (simp only: Cons.hyps)
    also have "... = foldlf(f(fzy)x)xs" by (simp only: assoc)
    also have "... = foldlf(fzy)(x : xs)" by auto
    finally show ?case.
  qed (simp add: neutr1 neutr2)

  have "foldlfz(x : xs) = foldlf(fzx)xs" by auto
  also have "... = fx(foldlfzxs)" by (simp only: step)
  also have "... = fx(foldrfzxs)" by (simp only: Cons.hyps)
  also have "... = (foldrfz(x:xs))" by auto
  finally show ?case .
qed auto

lemma elem_strict [simp]:
  "elemx = "
  by fixrec_simp

lemma notElem_strict [simp]:
  "notElemx = "
  by fixrec_simp

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

lemma take_Nil [simp]:
  "n    taken[] = []"
  by (subst take.simps) (cases "len0"; simp)

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

lemma take_Cons [simp]:
  "le1i = TT  takei(x:xs) = x : take(i - 1)xs"
  by (subst take.simps, cases "lei0") (auto dest: le_trans)

lemma take_MkI_Cons [simp]:
  "0 < n  take(MkIn)(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]:
  "take1(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]:
  "drop0xs = xs"
  "drop(MkI0)xs = xs"
  by (subst drop.simps, simp add: zero_Integer_def)+

lemma drop_pos [simp]:
  "len0 = FF  dropnxs = (case xs of []  [] | y : ys  drop(n - 1)ys)"
  by (subst drop.simps, simp)

lemma drop_numeral_Cons [simp]:
  "drop1(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(MkIi)xs ++ drop(MkIi)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(MkIn)[MkIi..] = [MkIi..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 "[MkIi..] = MkIi : [MkIi + 1..]" by (simp, subst intsFrom.simps) simp
    ultimately
    have *: "take(MkIn)[MkIi..] = MkIi : 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(MkIn)[MkIi..] = [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 ++ concatxss"
  "concat = "
  unfolding concat_def by simp_all

lemma concatMap_simps [simp]:
  "concatMapf[] = []"
  "concatMapf(x : xs) = fx ++ concatMapfxs"
  "concatMapf = "
  unfolding concatMap_def by simp_all

lemma filter_append [simp]:
  "filterP(xs ++ ys) = filterPxs ++ filterPys"
proof (induct xs)
  case (Cons x xs) then show ?case by (cases "Px") (auto simp: If_and_if)
qed simp_all

lemma elem_append [simp]:
  "elemx(xs ++ ys) = (elemxxs orelse elemxys)"
    by (induct xs) auto

lemma filter_filter [simp]:
  "filterP(filterQxs) = filter(Λ x. Qx andalso Px)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]:
  "allP = "
  by fixrec_simp

lemma any_strict [simp]:
  "anyP = "
  by fixrec_simp

lemma tails_neq_Nil [simp]:
  "tailsxs  []"
  by (cases xs) simp_all

lemma inits_neq_Nil [simp]:
  "initsxs  []"
  by (cases xs) simp_all

lemma Nil_neq_tails [simp]:
  "[]  tailsxs"
  by (cases xs) simp_all

lemma Nil_neq_inits [simp]:
  "[]  initsxs"
  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 nullxs then headys else headxs"
  by (cases xs) simp_all

lemma filter_cong:
  "xset xs. px = qx  filterpxs = filterqxs"
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 "xset xs. Px = TT"
  shows "filterPxs = xs"
  by (rule filter_cong [of xs P "Λ _. TT", simplified, OF assms])

lemma filter_FF [simp]:
  assumes "finite_list xs"
    and "xset xs. Px = FF"
  shows "filterPxs = []"
  using assms by (induct xs) simp_all

lemma map_cong:
  "xset xs. px = qx  mappxs = mapqxs"
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(MkIm)(MkIn))" (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 "xset xs. (Qx andalso Px) = (Px andalso Qx)"
  shows "filterP(filterQxs) = filterQ(filterPxs)"
  using filter_cong [of xs "Λ x. Qx andalso Px" "Λ x. Px andalso Qx"]
    and assms by simp

lemma upto_append_intsFrom [simp]:
  assumes "m  n"
  shows "upto(MkIm)(MkIn) ++ intsFrom(MkIn+1) = intsFrom(MkIm)"
    (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) = (MkIm : ?u (m+1) n) ++ ?i (n+1)"
      by (simp add: one_Integer_def)
    also have " = MkIm : ?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(MkIm)(MkIn)) = {MkIi | 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 (MkIm : ?u (m+1) n)" by (simp add: one_Integer_def)
    also have " = insert (MkIm) (?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))) = lengthxs"
  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 "xset xs. eqax  "
  shows "set (deleteaxs) = set xs - {a}"
  using assms
proof induct
  case (Cons x xs)
  then show ?case by (cases "eqax", force+)
qed simp

lemma distinct_delete [simp]:
  fixes xs :: "['a::Eq_eq]"
  assumes "distinct xs"
    and "xset xs. eqax  "
  shows "distinct (deleteaxs)"
  using assms
proof induct
  case (Cons x xs)
  then show ?case by (cases "eqax", force+)
qed simp

lemma set_diff [simp]:
  fixes xs ys :: "['a::Eq_eq]"
  assumes "distinct ys" and "distinct xs"
    and "aset ys. xset xs. eqax  "
  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 = "deleteyxs"
  from Cons have *: "xset xs. eqyx  " by simp
  from set_delete [OF distinct xs this]
  have **: "set ?xs = set xs - {y}" .
  with Cons have "aset ys. xset ?xs. eqax  " 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 "xset xs. eqax  "
  shows "deleteaxs = filter(Λ x. neqax)xs"
  using assms
proof (induct)
  case (Cons x xs)
  then have IH: "deleteaxs = filter(Λ x. neqax)xs" by simp
  show ?case
  proof (cases "eqax")
    case TT
    have "xset xs. (Λ x. neqax)x = (Λ _. TT)x"
    proof
      fix y
      assume "y  set xs"
      with Cons(3, 4) have "x  y" and "eqay  " by auto
      with TT have "eqay = FF" by (metis (no_types) eqD(1) trE)
      then show "(Λ x. neqax)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 "aset ys. xset xs. eqax  "
  shows "xs \\\\ ys = filter(Λ x. neg(elemxys))xs"
  using assms
proof (induct arbitrary: xs)
  case Nil then show ?case by simp
next
  case (Cons y ys)
  let ?xs = "deleteyxs"
  from Cons have *: "xset xs. eqyx  " by simp
  from set_delete [OF distinct xs this]
  have "set ?xs = set xs - {y}" .
  with Cons have "aset ys. xset ?xs. eqax  " by simp
  moreover from * and distinct xs have "distinct ?xs" by simp
  ultimately have "?xs \\\\ ys = filter(Λ x. neg(elemxys))?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 [MkIm..MkIn]"
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)..MkIn]" 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(MkIm)) = {MkIn | 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 = MkIm : ?i (m+1)"
        by (subst (asm) intsFrom.simps) (simp add: one_Integer_def)
      then have [simp]: "x = MkIm" "xs = ?i (m+1)" by simp_all
      show "x  {MkIn | n. m  n}" by simp
    next
      fix x xs y m
      assume IH: "listmem x xs"
        "m. xs = ?i m  x  {MkIn | n. m  n}"
        "y : xs = ?i m"
      then have "y : xs = MkIm : ?i (m+1)"
        by (subst (asm) (2) intsFrom.simps) (simp add: one_Integer_def)
      then have [simp]: "y = MkIm" "xs = ?i (m+1)" by simp_all
      from IH (2) [of "m+1"] have "x  {MkIn | n. m+1  n}" by (simp add: one_Integer_def)
      then show "x  {MkIn | 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 = MkIn" and "m  n" by blast
    from upto_append_intsFrom [OF this(2), symmetric]
    have *: "set (?i m) = set (upto(MkIm)(MkIn))  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]:
  "uptomn =   m =   n = "
  by (subst upto.simps, simp)

lemma seq_eq_bottom_iff [simp]: (* FIXME: move *)
  "seqxy =   x =   y = "
  by (simp add: seq_conv_if)

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

lemma intsFrom_split:
  assumes "m  n"
  shows "[MkIn..] = [MkIn .. MkI(m - 1)] ++ [MkIm..]"
proof-
  from assms have ge: "m - n  0" by arith
  have "[MkIn..] = (take(MkI(m - n))  [MkIn..]) ++ (drop(MkI(m - n))  [MkIn..])"
    by (subst take_drop_append, rule)
  also have "... = [MkIn.. MkI(m - 1)] ++ [MkIm..]"
    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(Λ (MkIi) . Def (P i))[MkI(n+1)..] = filter(Λ (MkIi) . Def (P i))[MkIn'..]"
proof-
  from assms(1)
  have"[MkI(n+1)..] = [MkI(n+1).. MkI(n'- 1)] ++ [MkIn'..]" (is "_ = ?l1 ++ ?l2")
    by (subst intsFrom_split[of "n+1" n'], auto)
  moreover
  have "filter(Λ (MkIi) . 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]:
  "nullxs = TT  xs = []"
  by (cases xs) simp_all

lemma null_set_empty_conv:
  "xs    nullxs = TT  set xs = {}"
  by (cases xs) simp_all

lemma elem_TT [simp]:
  fixes x :: "'a::Eq_eq" shows "elemxxs = 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 "eqax", force+)
  done

lemma elem_FF [simp]:
  fixes x :: "'a::Eq_equiv" shows "elemxxs = 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]:
  "repeatx  "
  by (subst repeat.simps) simp

lemma list_case_repeat [simp]:
  "list_caseaf(repeatx) = fx(repeatx)"
  by (subst repeat.simps) simp

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

lemma replicate_strict [simp]:
  "replicatex = "
  by (simp add: replicate_def)

lemma replicate_0 [simp]:
  "replicate0x = []"
  "replicate(MkI0)xs = []"
  by (simp add: replicate_def)+

lemma Integer_add_0 [simp]: "MkI0 + n = n"
  by (cases n) simp_all

lemma replicate_MkI_plus_1 [simp]:
  "0  n  replicate(MkI(n+1))x = x : replicate(MkIn)x"
  "0  n  replicate(MkI(1+n))x = x : replicate(MkIn)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(MkIm)x ++ replicate(MkIn)x
    = replicate(MkIm + MkIn)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(MkIm)x ++ replicate(MkIn)x = x : (replicate(MkI(int i))x ++ replicate(MkIn)x)" by (simp add: Suc)
    also have " = x : replicate(MkI(int i) + MkIn)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(MkI1)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(MkIn)x) = MkIn"
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]:
  "mapf(mapgxs) = map(f oo g)xs"
  by (induct xs) simp_all

lemma nth_Cons_MkI [simp]:
  "0 < i  (a : xs) !! (MkIi) = 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(+ MkIn)(intsFrom(MkIm)) = 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 = MkIm  (l' n'. l = MkIl'  n = MkIn'  m = l' + n')"
  by (cases l, simp) (cases n, auto)

lemma length_ge_0:
  "lengthxs = MkIn  n  0"
  by (induct xs arbitrary: n) (auto simp: one_Integer_def plus_eq_MkI_conv)

lemma length_0_conv [simp]:
  "lengthxs = MkI0  xs = []"
  apply (cases xs)
    apply (simp_all add: one_Integer_def)
  apply (case_tac "lengthlist")
   apply (auto dest: length_ge_0)
  done

lemma length_ge_1 [simp]:
  "lengthxs = MkI(1 + int n)
     (u us. xs = u : us  lengthus = 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 + lengthus = MkI(1 + int n)" by (simp add: ac_simps)
  then have "lengthus  " by (cases "lengthus") simp_all
  moreover from 2 have "lengthus + 1 = MkI(int n) + 1" by (simp add: one_Integer_def ac_simps)
  ultimately have "lengthus = MkI(int n)"
    by (cases "lengthus") (simp_all add: one_Integer_def)
  then show ?r by simp
qed

lemma finite_list_length_conv:
  "finite_list xs  (n. lengthxs = 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 "lengthxs = MkI(int n)" by blast
  then show "?l" by (induct n arbitrary: xs) auto
qed

lemma nth_append:
  assumes "lengthxs = MkIn" and "n  m"
  shows "(xs ++ ys) !! MkIm = 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: "lengthxs = 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(MkIn)x ++ xs) !! MkIn = xs !! MkI0"
  using nth_append [OF length_replicate [OF assms], of n]
    by simp

lemma map2_zip:
  "map(Λx, y. x, fy)(zipxsys) = zipxs(mapfys)"
  by (induct xs arbitrary: ys) (simp_all, case_tac ys, simp_all)

lemma map2_filter:
  "map(Λx, y. x, fy)(filter(Λx, y. Px)xs)
    = filter(Λx, y. Px)(map(Λx, y. x, fy)xs)"
  apply (induct xs, simp_all)
  apply (rename_tac x xs, case_tac x, simp, simp)
  apply (rename_tac a b, case_tac "Pa", auto)
done

lemma map_map_snd:
  "f =   mapf(mapsndxs)
    = mapsnd(map(Λx, y. x, fy)xs)"
  by (induct xs, simp_all, rename_tac a b, case_tac a, simp_all)

lemma findIndices_Cons [simp]:
  "findIndicesP(a : xs) =
    If Pa then 0 : map(+1)(findIndicesPxs)
    else map(+1)(findIndicesPxs)"
  by (auto simp: findIndices_def, subst intsFrom.simps, cases "Pa")
     (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 "(+ MkI1)", simplified]
       map2_filter [of "(+ MkI1)", simplified])

lemma filter_alt_def:
  fixes xs :: "['a]"
  shows "filterPxs = map(nthxs)(findIndicesPxs)"
proof -
  have 1: "mapf(mapsnd(filter(Λx, i. Px)(zipxs[MkIi..])))
    = mapg(mapsnd(filter(Λx, i. Px)(zipxs[MkIi..])))"
    if "ji. f(MkIj) = g(MkIj)"
    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 "Pa", simp_all add: one_Integer_def)
  have 2: "i0. nthys(MkIi) = (nth(a : ys) oo (+1))(MkIi)"
    for a and ys :: "['a]"
    by (auto simp: one_Integer_def zero_Integer_def)
  have 3: "map(nth(a : ys) oo (+1))(findIndicesPxs)
    = map(nthys)(findIndicesPxs)"
    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 "Pa", 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 (mapfxs) = f `⋅ set xs" (is "?l = ?r")
proof
  have "listmem (fa) (mapfxs)" 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 = fb  listmem b xs" if "listmem a (mapfxs)" for a
    using that
    by (induct a "mapfxs" 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(:))ysxs = 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) = reversexs ++ [x]"
  by (simp add: reverse.simps)
     (subst foldl_flip_Cons_append, rule refl)

lemma reverse_append_below:
  "reverse(xs ++ ys)  reverseys ++ reversexs"
  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(reversexs)  xs"
proof (induction xs)
  case (Cons x xs)
  have "reverse(reverse(x:xs)) = reverse(reversexs ++ [x])" by simp
  also have "  reverse[x] ++ reverse(reversexs)" by (rule reverse_append_below)
  also have " = x : reverse(reversexs)" 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) = reverseys ++ reversexs"
  using assms by (induct xs) simp+

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

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

lemma reverse_reverse [simp]:
  assumes "finite_list xs" shows "reverse(reversexs) = 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 = "reversexs"])
    apply simp+
  done

lemma length_plus_not_0:
  "le1n = TT  le(lengthxs + 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:
  "lengthxs    take(lengthxs + 1)(y:ys) = y : take(lengthxs)ys"
  by (subst take.simps, cases "le(lengthxs + 1)0")
     (auto, metis (no_types) length_plus_not_0 le_Integer_numeral_simps(4))

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

lemma eq_take_length_isPrefixOf:
  "eqxs(take(lengthxs)ys)  isPrefixOfxsys"
proof (induct xs arbitrary: ys)
  case IH: (Cons x xs)
  show ?case
  proof (cases "lengthxs = ")
    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