Theory List2

(*  Title:      List2.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Additional definitions and results for lists›

theory List2
imports "../CommonSet/SetIntervalCut"
begin

subsection ‹Additional definitions and results for lists›

text ‹
  Infix syntactical abbreviations for operators @{term take} and @{term drop}.
  The abbreviations resemble to the operator symbols used later
  for take and drop operators on infinite lists in ListInf.›

abbreviation f_take' :: "'a list ⇒ nat ⇒ 'a list"  (infixl ‹↓› 100)
  where "xs ↓ n ≡ take n xs"
abbreviation f_drop' :: "'a list ⇒ nat ⇒ 'a list"  (infixl ‹↑› 100)
  where "xs ↑ n ≡ drop n xs"

lemma append_eq_Cons: "[x] @ xs = x # xs"
by simp

lemma length_Cons: "length (x # xs) = Suc (length xs)"
by simp

lemma length_snoc: "length (xs @ [x]) = Suc (length xs)"
by simp


subsubsection ‹Additional lemmata about list emptiness›

lemma length_greater_imp_not_empty:"n < length xs ⟹ xs ≠ []"
by fastforce

lemma length_ge_Suc_imp_not_empty:"Suc n ≤ length xs ⟹ xs ≠ []"
by fastforce

lemma length_take_le: "length (xs ↓ n) ≤ length xs"
by simp

lemma take_not_empty_conv:"(xs ↓ n ≠ []) = (0 < n ∧ xs ≠ [])"
by simp

lemma drop_not_empty_conv:"(xs ↑ n ≠ []) = (n < length xs)"
by fastforce

lemma zip_eq_Nil: "(zip xs ys = []) = (xs = [] ∨ ys = [])"
by (force simp: length_0_conv[symmetric] min_def simp del: length_0_conv)

lemma zip_not_empty_conv: "(zip xs ys ≠ []) = (xs ≠ [] ∧ ys ≠ [])"
by (simp add: zip_eq_Nil)


subsubsection ‹Additional lemmata about @{term take}, @{term drop}, @{term hd}, @{term last}, ‹nth› and ‹filter››

lemma nth_tl_eq_nth_Suc: "
  Suc n ≤ length xs ⟹ (tl xs) ! n = xs ! Suc n"
by (rule hd_Cons_tl[OF length_ge_Suc_imp_not_empty, THEN subst], simp+)
corollary nth_tl_eq_nth_Suc2: "
  n < length xs ⟹ (tl xs) ! n = xs ! Suc n"
by (simp add: nth_tl_eq_nth_Suc)

lemma hd_eq_first: "xs ≠ [] ⟹ xs ! 0 = hd xs"
by (induct xs, simp_all)
corollary take_first:"xs ≠ [] ⟹ xs ↓  (Suc 0) = [xs ! 0]"
by (induct xs, simp_all)
corollary take_hd:"xs ≠ [] ⟹ xs ↓  (Suc 0) = [hd xs]"
by (simp add: take_first hd_eq_first)

theorem last_nth: "xs ≠ [] ⟹ last xs = xs ! (length xs - Suc 0)"
by (simp add: last_conv_nth)

lemma last_take: "n < length xs ⟹ last (xs ↓ Suc n) = xs ! n"
by (simp add: last_nth length_greater_imp_not_empty min_eqR)
corollary last_take2:"
  ⟦ 0 < n; n ≤ length xs ⟧ ⟹ last (xs ↓ n) = xs ! (n - Suc 0)"
apply (frule diff_Suc_less[THEN order_less_le_trans, of _ "length xs" 0], assumption)
apply (drule last_take[of "n - Suc 0" xs])
apply simp
done

corollary nth_0_drop: "n ≤ length xs ⟹ (xs ↑ n) ! 0 = xs ! n"
  by (cut_tac nth_drop[of n xs 0], simp+)


lemma drop_eq_tl: "xs ↑ (Suc 0) = tl xs"
by (simp add: drop_Suc)

lemma drop_take_1: "
  n < length xs ⟹ xs ↑ n ↓ (Suc 0) = [xs ! n]"
by (simp add: take_hd hd_drop_conv_nth)

lemma upt_append: "m ≤ n ⟹ [0..<m] @ [m..<n] = [0..<n]"
by (insert upt_add_eq_append[of 0 m "n - m"], simp)

lemma nth_append1: "n < length xs ⟹ (xs @ ys) ! n = xs ! n"
by (simp add: nth_append)
lemma nth_append2: "length xs ≤ n ⟹ (xs @ ys) ! n = ys ! (n - length xs)"
by (simp add: nth_append)


lemma list_all_conv: "list_all P xs = (∀i<length xs. P (xs ! i))"
by (rule list_all_length)

lemma expand_list_eq: "
  ⋀ys. (xs = ys) = (length xs = length ys ∧ (∀i<length xs. xs ! i = ys ! i))"
by (rule list_eq_iff_nth_eq)
lemmas list_eq_iff = expand_list_eq


lemma list_take_drop_imp_eq: "
  ⟦ xs ↓ n = ys ↓ n;  xs ↑ n = ys ↑ n ⟧ ⟹ xs = ys"
apply (rule subst[OF append_take_drop_id[of n xs]])
apply (rule subst[OF append_take_drop_id[of n ys]])
apply simp
done

lemma list_take_drop_eq_conv: "
  (xs = ys) = (∃n. (xs ↓ n = ys ↓ n ∧ xs ↑ n = ys ↑ n))"
by (blast intro: list_take_drop_imp_eq)

lemma list_take_eq_conv: "(xs = ys) = (∀n. xs ↓ n = ys ↓ n)"
apply (rule iffI, simp)
apply (drule_tac x="max (length xs) (length ys)" in spec)
apply simp
done

lemma list_drop_eq_conv: "(xs = ys) = (∀n. xs ↑ n = ys ↑ n)"
apply (rule iffI, simp)
apply (drule_tac x=0 in spec)
apply simp
done


abbreviation replicate' :: "'a ⇒ nat ⇒ 'a list"  (‹_⇗_⇖› [1000,65])
  where "x⇗n⇖ ≡ replicate n x"

lemma replicate_snoc: "x⇗n⇖ @ [x] = x⇗Suc n⇖"
by (simp add: replicate_app_Cons_same)

lemma eq_replicate_conv: "(∀i<length xs. xs ! i = m) = (xs = m⇗length xs⇖)"
apply (rule iffI)
 apply (simp add: expand_list_eq)
apply clarsimp
apply (rule ssubst[of xs "replicate (length xs) m"], assumption)
apply (rule nth_replicate, simp)
done

lemma replicate_Cons_length: "length (x # a⇗n⇖) = Suc n"
by simp
lemma replicate_pred_Cons_length: "0 < n ⟹ length (x # a⇗n - Suc 0⇖) = n"
by simp

lemma replicate_le_diff: "m ≤ n ⟹ x⇗m⇖ @ x⇗n - m⇖ = x⇗n⇖"
by (simp add: replicate_add[symmetric])
lemma replicate_le_diff2: "⟦ k ≤ m; m ≤ n ⟧ ⟹ x⇗m - k⇖ @ x⇗n - m⇖ = x⇗n - k⇖"
by (subst replicate_add[symmetric], simp)

lemma append_constant_length_induct_aux: "⋀xs.
  ⟦ length xs div k = n; ⋀ys. k = 0 ∨ length ys < k ⟹ P ys;
    ⋀xs ys. ⟦ length xs = k; P ys ⟧ ⟹ P (xs @ ys) ⟧ ⟹ P xs"
apply (case_tac "k = 0", blast)
apply simp
apply (induct n)
 apply (simp add: div_eq_0_conv')
apply (subgoal_tac "k ≤ length xs")
 prefer 2
 apply (rule div_gr_imp_gr_divisor[of 0], simp)
apply (simp only: atomize_all atomize_imp, clarsimp)
apply (erule_tac x="drop k xs" in allE)
apply (simp add: div_diff_self2)
apply (erule_tac x=undefined in allE)
apply (erule_tac x="take k xs" in allE)
apply (simp add: min_eqR)
apply (erule_tac x="drop k xs" in allE)
apply simp
done

lemma append_constant_length_induct: "
  ⟦ ⋀ys. k = 0 ∨ length ys < k ⟹ P ys;
    ⋀xs ys. ⟦ length xs = k; P ys ⟧ ⟹ P (xs @ ys) ⟧ ⟹ P xs"
by (simp add: append_constant_length_induct_aux[of _ _ "length xs div k"])

lemma zip_swap: "map (λ(y,x). (x,y)) (zip ys xs) = (zip xs ys)"
by (simp add: expand_list_eq)

lemma zip_takeL: "(zip xs ys) ↓ n = zip (xs ↓ n) ys"
by (simp add: expand_list_eq)

lemma zip_takeR: "(zip xs ys) ↓ n = zip xs (ys ↓ n)"
apply (subst zip_swap[of ys, symmetric])
apply (subst take_map)
apply (subst zip_takeL)
apply (simp add: zip_swap)
done

lemma zip_take: "(zip xs ys) ↓ n = zip (xs ↓ n) (ys ↓ n)"
by (rule take_zip)

lemma hd_zip: "⟦ xs ≠ []; ys ≠ [] ⟧ ⟹ hd (zip xs ys) = (hd xs, hd ys)"
by (simp add: hd_conv_nth zip_not_empty_conv)

lemma map_id: "map id xs = xs"
by (simp add: id_def)

lemma map_id_subst: "P (map id xs) ⟹ P xs"
by (subst map_id[symmetric])

lemma map_one: "map f [x] = [f x]"
by simp

lemma map_last: "xs ≠ [] ⟹ last (map f xs) = f (last xs)"
by (rule last_map)


lemma filter_list_all: "list_all P xs ⟹ filter P xs = xs"
by (induct xs, simp+)

lemma filter_snoc: "filter P (xs @ [x]) = (if P x then (filter P xs) @ [x] else filter P xs)"
by (case_tac "P x", simp+)

lemma filter_filter_eq: "list_all (λx. P x = Q x) xs ⟹ filter P xs = filter Q xs"
by (induct xs, simp+)

lemma filter_nth: "⋀n.
  n < length (filter P xs) ⟹
  (filter P xs) ! n =
  xs ! (LEAST k.
    k < length xs ∧
    n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)})"
apply (induct xs rule: rev_induct, simp)
apply (rename_tac x xs n)
apply (simp only: filter_snoc)
apply (simp split del: if_split)
apply (case_tac "xs = []")
 apply (simp split del: if_split)
 apply (rule_tac
   t = "λk i. i = 0 ∧ i ≤ k ∧ P ([x] ! i)" and
   s = "λk i. i = 0 ∧ P x"
   in subst)
  apply (simp add: fun_eq_iff)
  apply fastforce
 apply (fastforce simp: Least_def)
apply (rule_tac
  t = "λk. card {i. i ≤ k ∧ i < Suc (length xs) ∧ P ((xs @ [x]) ! i)}" and
  s = "λk. (card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)} +
           (if k ≥ length xs ∧ P x then Suc 0 else 0))"
  in subst)
 apply (clarsimp simp: fun_eq_iff split del: if_split, rename_tac k)
 apply (simp split del: if_split add: less_Suc_eq conj_disj_distribL conj_disj_distribR Collect_disj_eq)
 apply (subst card_Un_disjoint)
    apply (rule_tac n="length xs" in bounded_nat_set_is_finite, blast)
   apply (rule_tac n="Suc (length xs)" in bounded_nat_set_is_finite, blast)
  apply blast
 apply (rule_tac
   t = "λi. i < length xs ∧ P ((xs @ [x]) ! i)" and
   s = "λi. i < length xs ∧ P (xs ! i)"
   in subst)
  apply (rule fun_eq_iff[THEN iffD2])
  apply (fastforce simp: nth_append1)
 apply (rule add_left_cancel[THEN iffD2])
 apply (rule_tac
   t = "λi. i = length xs ∧ i ≤ k ∧ P ((xs @ [x]) ! i)" and
   s = "λi. i = length xs ∧ i ≤ k ∧ P x"
   in subst)
  apply (rule fun_eq_iff[THEN iffD2])
  apply fastforce
 apply (case_tac "length xs ≤ k")
  apply clarsimp
  apply (rule_tac
    t = "λi. i = length xs ∧ i ≤ k" and
    s = "λi. i = length xs"
    in subst)
   apply (rule fun_eq_iff[THEN iffD2])
   apply fastforce
  apply simp
 apply simp
apply (simp split del: if_split add: less_Suc_eq conj_disj_distribL conj_disj_distribR)
apply (rule_tac
  t = "λk. k < length xs ∧
           n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)} + (if length xs ≤ k ∧ P x then Suc 0 else 0)" and
  s = "λk. k < length xs ∧ n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)}"
  in subst)
 apply (simp add: fun_eq_iff)
apply (rule_tac
  t = "λk. k = length xs ∧
           n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)} + (if length xs ≤ k ∧ P x then Suc 0 else 0)" and
  s = "λk. k = length xs ∧
           n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)} + (if P x then Suc 0 else 0)"
  in subst)
 apply (simp add: fun_eq_iff)
apply (case_tac "n < length (filter P xs)")
 apply (rule_tac
   t = "(if P x then filter P xs @ [x] else filter P xs) ! n" and
   s = "(filter P xs) ! n"
   in subst)
  apply (simp add: nth_append1)
 apply (simp split del: if_split)
 apply (subgoal_tac "∃k<length xs. n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)}")
  prefer 2
  apply (rule_tac x="length xs - Suc 0" in exI)
  apply (simp add: length_filter_conv_card less_eq_le_pred[symmetric])
 apply (subgoal_tac "∃k≤length xs. n < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)}")
  prefer 2
  apply (blast intro: less_imp_le)
 apply (subst Least_le_imp_le_disj)
   apply simp
  apply simp
 apply (rule sym, rule nth_append1)
 apply (rule LeastI2_ex, assumption)
 apply blast
apply (simp add: linorder_not_less)
apply (subgoal_tac "P x")
 prefer 2
 apply (rule ccontr, simp)
apply (simp add: length_snoc)
apply (drule less_Suc_eq_le[THEN iffD1], drule_tac x=n in order_antisym, assumption)
apply (simp add: nth_append2)
apply (simp add: length_filter_conv_card)
apply (rule_tac
  t = "λk. card {i. i < length xs ∧ P (xs ! i)} < card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)}" and
  s = "λk. False"
  in subst)
 apply (rule fun_eq_iff[THEN iffD2], rule allI, rename_tac k)
 apply (simp add: linorder_not_less)
 apply (rule card_mono)
  apply fastforce
 apply blast
apply simp
apply (rule_tac
  t = "(LEAST k. k = length xs ∧
                 card {i. i < length xs ∧ P (xs ! i)} < Suc (card {i. i ≤ k ∧ i < length xs ∧ P (xs ! i)}))" and
  s = "length xs"
  in subst)
 apply (rule sym, rule Least_equality)
  apply simp
  apply (rule le_imp_less_Suc)
  apply (rule card_mono)
   apply fastforce
  apply fastforce
 apply simp
apply simp
done


subsubsection ‹Ordered lists›

fun list_ord :: "('a ⇒ 'a ⇒ bool) ⇒ ('a::ord) list ⇒ bool"
where
  "list_ord ord (x1 # x2 # xs) = (ord x1 x2 ∧ list_ord ord (x2 # xs))"
| "list_ord ord xs = True"

definition list_asc :: "('a::ord) list ⇒ bool" where
  "list_asc xs ≡ list_ord (≤) xs"
definition list_strict_asc :: "('a::ord) list ⇒ bool" where
  "list_strict_asc xs ≡ list_ord (<) xs"
value "list_asc  [1::nat, 2, 2]"
value "list_strict_asc  [1::nat, 2, 2]"
definition list_desc :: "('a::ord) list ⇒ bool" where
  "list_desc xs ≡ list_ord (≥) xs"
definition list_strict_desc :: "('a::ord) list ⇒ bool" where
  "list_strict_desc xs ≡ list_ord (>) xs"

lemma list_ord_Nil: "list_ord ord []"
by simp
lemma list_ord_one: "list_ord ord [x]"
by simp
lemma list_ord_Cons: "
  list_ord ord (x # xs) =
  (xs = [] ∨ (ord x (hd xs) ∧ list_ord ord xs))"
by (induct xs, simp+)
lemma list_ord_Cons_imp: "⟦ list_ord ord xs; ord x (hd xs) ⟧ ⟹ list_ord ord (x # xs)"
by (induct xs, simp+)
lemma list_ord_append: "⋀ys.
  list_ord ord (xs @ ys) =
  (list_ord ord xs ∧
  (ys = [] ∨ (list_ord ord ys ∧ (xs = [] ∨ ord (last xs) (hd ys)))))"
apply (induct xs, fastforce)
apply (case_tac xs, case_tac ys, fastforce+)
done
lemma list_ord_snoc: "
  list_ord ord (xs @ [x]) =
  (xs = [] ∨ (ord (last xs) x ∧ list_ord ord xs))"
by (fastforce simp: list_ord_append)

lemma list_ord_all_conv: "
  (list_ord ord xs) = (∀n < length xs - 1. ord (xs ! n) (xs ! Suc n))"
apply (rule iffI)
 apply (induct xs, simp)
 apply clarsimp
 apply (simp add: list_ord_Cons)
 apply (erule disjE, simp)
 apply clarsimp
 apply (case_tac n)
  apply (simp add: hd_conv_nth)
 apply simp
apply (induct xs, simp)
apply (simp add: list_ord_Cons)
apply (case_tac "xs = []", simp)
apply (drule meta_mp)
 apply (intro allI impI, rename_tac n)
 apply (drule_tac x="Suc n" in spec, simp)
apply (drule_tac x=0 in spec)
apply (simp add: hd_conv_nth)
done

lemma list_ord_imp: "
  ⟦ ⋀x y. ord x y ⟹ ord' x y; list_ord ord xs ⟧ ⟹
  list_ord ord' xs"
apply (induct xs, simp)
apply (simp add: list_ord_Cons)
apply fastforce
done
corollary list_strict_asc_imp_list_asc: "
  list_strict_asc (xs::'a::preorder list) ⟹ list_asc xs"
by (unfold list_strict_asc_def list_asc_def, rule list_ord_imp[of "(<)"], rule order_less_imp_le)
corollary list_strict_desc_imp_list_desc: "
  list_strict_desc (xs::'a::preorder list) ⟹ list_desc xs"
by (unfold list_strict_desc_def list_desc_def, rule list_ord_imp[of "(>)"], rule order_less_imp_le)

lemma list_ord_trans_imp: "⋀i.
  ⟦ transP ord; list_ord ord xs; j < length xs; i < j ⟧ ⟹
  ord (xs ! i) (xs ! j)"
apply (simp add: list_ord_all_conv)
apply (induct j, simp)
apply (case_tac "j < i", simp)
apply (simp add: linorder_not_less)
apply (case_tac "i = j", simp)
apply (drule_tac x=i in meta_spec, simp)
apply (drule_tac x=j in spec, simp add: Suc_less_pred_conv)
apply (unfold trans_def)
apply (drule_tac x="xs ! i" in spec, drule_tac x="xs ! j" in spec, drule_tac x="xs ! Suc j" in spec)
apply simp
done

lemma list_ord_trans: "
  transP ord ⟹
  (list_ord ord xs) =
  (∀j < length xs. ∀i < j. ord (xs ! i) (xs ! j))"
apply (rule iffI)
 apply (simp add: list_ord_trans_imp)
apply (simp add: list_ord_all_conv)
done

lemma list_ord_trans_refl_le: "
  ⟦ transP ord; reflP ord ⟧ ⟹
  (list_ord ord xs) =
  (∀j < length xs. ∀i ≤ j. ord (xs ! i) (xs ! j))"
apply (subst list_ord_trans, simp)
apply (rule iffI)
 apply clarsimp
 apply (case_tac "i = j")
  apply (simp add: refl_on_def)
 apply simp+
done

lemma list_ord_trans_refl_le_imp: "
  ⟦ transP ord; ⋀x y. ord x y ⟹ ord' x y; reflP ord';
    list_ord ord xs ⟧ ⟹
  (∀j < length xs. ∀i ≤ j. ord' (xs ! i) (xs ! j))"
apply clarify
apply (case_tac "i = j")
 apply (simp add: refl_on_def)
apply (simp add: list_ord_trans_imp)
done

corollary
  list_asc_trans: "
    (list_asc (xs::'a::preorder list)) =
    (∀j < length xs. ∀i < j. xs ! i ≤ xs ! j)" and
  list_strict_asc_trans: "
    (list_strict_asc (xs::'a::preorder list)) =
    (∀j < length xs. ∀i < j. xs ! i < xs ! j)" and
  list_desc_trans: "
    (list_desc (xs::'a::preorder list)) =
    (∀j < length xs. ∀i < j. xs ! j ≤ xs ! i)" and
  list_strict_desc_trans: "
    (list_strict_desc (xs::'a::preorder list)) =
    (∀j < length xs. ∀i < j. xs ! j < xs ! i)"
apply (unfold list_asc_def list_strict_asc_def list_desc_def list_strict_desc_def)
apply (rule list_ord_trans, unfold trans_def, blast intro: order_trans order_less_trans)+
done

corollary
  list_asc_trans_le: "
    (list_asc (xs::'a::preorder list)) =
    (∀j < length xs. ∀i ≤ j. xs ! i ≤ xs ! j)" and
  list_desc_trans_le: "
    (list_desc (xs::'a::preorder list)) =
    (∀j < length xs. ∀i ≤ j. xs ! j ≤ xs ! i)"
apply (unfold list_asc_def list_strict_asc_def list_desc_def list_strict_desc_def)
apply (rule list_ord_trans_refl_le, unfold trans_def, blast intro: order_trans, simp add: refl_on_def)+
done

corollary
  list_strict_asc_trans_le: "
    (list_strict_asc (xs::'a::preorder list)) ⟹
    (∀j < length xs. ∀i ≤ j. xs ! i ≤ xs ! j)"
apply (unfold list_strict_asc_def)
apply (rule list_ord_trans_refl_le_imp[where ord="(≤)"])
   apply (unfold trans_def, blast intro: order_trans)
  apply assumption
 apply (unfold refl_on_def, clarsimp)
apply (rule list_ord_imp[where ord="(<)"], simp_all add: less_imp_le)
done

lemma list_ord_le_sorted_eq: "list_asc xs = sorted xs"
apply (rule sym)
apply (simp add: list_asc_def)
apply (induct xs, simp)
apply (rename_tac x xs)
apply (simp add: list_ord_Cons)
apply (case_tac "xs = []", simp_all)
apply (case_tac "list_ord (≤) xs", simp_all)
apply (rule iffI)
 apply (drule_tac x="hd xs" in bspec, simp_all)
apply clarify
apply (drule in_set_conv_nth[THEN iffD1], clarsimp, rename_tac i1)
apply (simp add: hd_conv_nth)
apply (case_tac i1, simp)
apply (rename_tac i2)
apply simp
apply (fold list_asc_def)
apply (fastforce simp: list_asc_trans)
done

corollary list_asc_upto: "list_asc [m..n]"
by (simp add: list_ord_le_sorted_eq)

lemma list_strict_asc_upt: "list_strict_asc [m..<n]"
by (simp add: list_strict_asc_def list_ord_all_conv)


lemma list_ord_distinct_aux: "
  ⟦ irrefl {(a, b). ord a b}; transP ord; list_ord ord xs;
    i < length xs; j < length xs; i < j ⟧ ⟹
  xs ! i ≠ xs ! j"
apply (subgoal_tac "⋀x y. ord x y ⟹ x ≠ y")
 prefer 2
 apply (rule ccontr)
 apply (simp add: irrefl_def)
apply (simp add: list_ord_trans)
done

lemma list_ord_distinct: "
  ⟦ irrefl {(a,b). ord a b}; transP ord; list_ord ord xs ⟧ ⟹
  distinct xs"
apply (simp add: distinct_conv_nth, intro allI impI, rename_tac i j)
apply (drule neq_iff[THEN iffD1], erule disjE)
 apply (simp add: list_ord_distinct_aux)
apply (simp add: list_ord_distinct_aux[THEN not_sym])
done

lemma list_strict_asc_distinct: "list_strict_asc (xs::'a::preorder list) ⟹ distinct xs"
apply (rule_tac ord="(<)" in list_ord_distinct)
apply (unfold irrefl_def list_strict_asc_def trans_def)
apply (blast intro: less_trans)+
done

lemma list_strict_desc_distinct: "list_strict_desc (xs::'a::preorder list) ⟹ distinct xs"
apply (rule_tac ord="(>)" in list_ord_distinct)
apply (unfold irrefl_def list_strict_desc_def trans_def)
apply (blast intro: less_trans)+
done


subsubsection ‹Additional definitions and results for sublists›

primrec sublist_list :: "'a list ⇒ nat list ⇒ 'a list"
where
  "sublist_list xs [] = []"
| "sublist_list xs (y # ys) = (xs ! y) # (sublist_list xs ys)"

value "sublist_list [0::int,10::int,20,30,40,50] [1::nat,2,3]"
value "sublist_list [0::int,10::int,20,30,40,50] [1::nat,1,2,3]"
value [nbe] "sublist_list [0::int,10::int,20,30,40,50] [1::nat,1,2,3,10]"

lemma sublist_list_length: "length (sublist_list xs ys) = length ys"
by (induct ys, simp_all)

lemma sublist_list_append: "
 ⋀zs. sublist_list xs (ys @ zs) = sublist_list xs ys @ sublist_list xs zs"
by (induct ys, simp_all)

lemma sublist_list_Nil: "sublist_list xs [] =[]"
by simp

lemma sublist_list_is_Nil_conv: "
  (sublist_list xs ys = []) = (ys = [])"
apply (rule iffI)
 apply (rule ccontr)
 apply (clarsimp simp: neq_Nil_conv)
apply simp
done

lemma sublist_list_eq_imp_length_eq: "
  sublist_list xs ys = sublist_list xs zs ⟹ length ys = length zs"
by (drule arg_cong[where f=length], simp add: sublist_list_length)

lemma sublist_list_nth: "
  ⋀n. n < length ys ⟹ sublist_list xs ys ! n = xs ! (ys ! n)"
apply (induct ys, simp)
apply (case_tac n, simp_all)
done

lemma take_drop_eq_sublist_list: "
  m + n ≤ length xs ⟹ xs ↑ m ↓ n = sublist_list xs [m..<m+n]"
apply (insert length_upt[of m "m+n"])
apply (simp add: expand_list_eq)
apply (simp add: sublist_list_length)
apply (frule add_le_imp_le_diff2)
apply (clarsimp, rename_tac i)
apply (simp add: sublist_list_nth)
done


primrec sublist_list_if :: "'a list ⇒ nat list ⇒ 'a list"
where
  "sublist_list_if xs [] = []"
| "sublist_list_if xs (y # ys) =
    (if y < length xs then (xs ! y) # (sublist_list_if xs ys)
     else (sublist_list_if xs ys))"

value "sublist_list_if [0::int,10::int,20,30,40,50] [1::nat,2,3]"
value "sublist_list_if [0::int,10::int,20,30,40,50] [1::nat,1,2,3]"
value "sublist_list_if [0::int,10::int,20,30,40,50] [1::nat,1,2,3,10]"

lemma sublist_list_if_sublist_list_filter_conv: "⋀xs.
  sublist_list_if xs ys = sublist_list xs (filter (λi. i < length xs) ys)"
by (induct ys, simp+)

corollary sublist_list_if_sublist_list_eq: "⋀xs.
  list_all (λi. i < length xs) ys ⟹
  sublist_list_if xs ys = sublist_list xs ys"
by (simp add: sublist_list_if_sublist_list_filter_conv filter_list_all)

corollary sublist_list_if_sublist_list_eq2: "⋀xs.
  ∀n<length ys. ys ! n < length xs ⟹
  sublist_list_if xs ys = sublist_list xs ys"
by (rule sublist_list_if_sublist_list_eq, rule list_all_conv[THEN iffD2])

lemma sublist_list_if_Nil_left: "sublist_list_if [] ys = []"
by (induct ys, simp+)
lemma sublist_list_if_Nil_right: "sublist_list_if xs [] = []"
by simp

lemma sublist_list_if_length: "
  length (sublist_list_if xs ys) = length (filter (λi. i < length xs) ys)"
by (simp add: sublist_list_if_sublist_list_filter_conv sublist_list_length)
lemma sublist_list_if_append: "
  sublist_list_if xs (ys @ zs) = sublist_list_if xs ys @ sublist_list_if xs zs"
by (simp add: sublist_list_if_sublist_list_filter_conv sublist_list_append)
lemma sublist_list_if_snoc: "
  sublist_list_if xs (ys @ [y]) = sublist_list_if xs ys @ (if y < length xs then [xs ! y] else [])"
by (simp add: sublist_list_if_append)


lemma sublist_list_if_is_Nil_conv: "
  (sublist_list_if xs ys = []) = (list_all (λi. length xs ≤ i) ys)"
by (simp add: sublist_list_if_sublist_list_filter_conv sublist_list_is_Nil_conv filter_empty_conv list_all_iff linorder_not_less)

lemma sublist_list_if_nth: "
  n < length ((filter (λi. i < length xs) ys)) ⟹
  sublist_list_if xs ys ! n = xs ! ((filter (λi. i < length xs) ys) ! n)"
by (simp add: sublist_list_if_sublist_list_filter_conv sublist_list_nth)

lemma take_drop_eq_sublist_list_if: "
  m + n ≤ length xs ⟹ xs ↑ m ↓ n = sublist_list_if xs [m..<m+n]"
by (simp add: sublist_list_if_sublist_list_filter_conv take_drop_eq_sublist_list)

lemma nths_empty_conv: "(nths xs I = []) = (∀i∈I. length xs ≤ i)"
  using [[hypsubst_thin = true]]
by (fastforce simp: set_empty[symmetric] set_nths linorder_not_le[symmetric])

lemma nths_singleton2: "nths xs {y} = (if y < length xs then [xs ! y] else [])"
apply (unfold nths_def)
apply (induct xs rule: rev_induct, simp)
apply (simp add: nth_append)
done

lemma nths_take_eq: "
  ⟦ finite I; Max I < n ⟧ ⟹ nths (xs ↓ n) I = nths xs I"
apply (case_tac "I = {}", simp)
apply (case_tac "n < length xs")
 prefer 2
 apply simp
apply (rule_tac
  t = "nths xs I" and
  s = "nths (xs ↓ n @ xs ↑ n) I"
  in subst)
 apply simp
apply (subst nths_append)
apply (simp add: min_eqR)
apply (rule_tac t="{j. j + n ∈ I}" and s="{}" in subst)
 apply blast
apply simp
done

lemma nths_drop_eq: "
  n ≤ iMin I ⟹ nths (xs ↑ n) {j. j + n ∈ I} = nths xs I"
apply (case_tac "I = {}", simp)
apply (case_tac "n < length xs")
 prefer 2
 apply (simp add: nths_def filter_empty_conv linorder_not_less)
 apply (clarsimp, rename_tac a b)
 apply (drule set_zip_rightD)
 apply fastforce
apply (rule_tac
  t = "nths xs I" and
  s = "nths (xs ↓ n @ xs ↑ n) I"
  in subst)
 apply simp
apply (subst nths_append)
apply (fastforce simp: nths_empty_conv min_eqR)
done

lemma nths_cut_less_eq: "
  length xs ≤ n ⟹ nths xs (I ↓< n) = nths xs I"
apply (simp add: nths_def cut_less_mem_iff)
apply (rule_tac f="λxs. map fst xs" in arg_cong)
apply (rule filter_filter_eq)
apply (simp add: list_all_conv)
done

lemma nths_disjoint_Un: "
  ⟦ finite A; Max A < iMin B ⟧ ⟹ nths xs (A ∪ B) = nths xs A @ nths xs B"
apply (case_tac "A = {}", simp)
apply (case_tac "B = {}", simp)
apply (case_tac "length xs ≤ iMin B")
 apply (subst nths_cut_less_eq[of xs "iMin B", symmetric], assumption)
 apply (simp (no_asm_simp) add: cut_less_Un cut_less_Min_empty cut_less_Max_all)
 apply (simp add: nths_empty_conv iMin_ge_iff)
apply (simp add: linorder_not_le)
apply (rule_tac
  t = "nths xs (A ∪ B)" and
  s = "nths (xs ↓ (iMin B) @ xs ↑ (iMin B)) (A ∪ B)"
  in subst)
 apply simp
apply (subst nths_append)
apply (simp add: min_eqR)
apply (subst nths_cut_less_eq[where xs="xs ↓ iMin B" and n="iMin B", symmetric], simp)
apply (simp add: cut_less_Un cut_less_Min_empty cut_less_Max_all)
apply (simp add: nths_take_eq)
apply (rule_tac
  t = "λj. j + iMin B ∈ A ∨ j + iMin B ∈ B" and
  s = "λj. j + iMin B ∈ B"
  in subst)
 apply (force simp: fun_eq_iff)
apply (simp add: nths_drop_eq)
done

corollary nths_disjoint_insert_left: "
  ⟦ finite I; x < iMin I ⟧ ⟹ nths xs (insert x I) = nths xs {x} @ nths xs I"
apply (rule_tac t="insert x I" and s="{x} ∪ I" in subst, simp)
apply (subst nths_disjoint_Un)
apply simp_all
done

corollary nths_disjoint_insert_right: "
  ⟦ finite I; Max I < x ⟧ ⟹ nths xs (insert x I) = nths xs I @ nths xs {x}"
apply (rule_tac t="insert x I" and s="I ∪ {x}" in subst, simp)
apply (subst nths_disjoint_Un)
apply simp_all
done

lemma nths_all: "{..<length xs} ⊆ I ⟹ nths xs I = xs"
apply (case_tac "xs = []", simp)
apply (rule_tac
  t = "I" and
  s = "I ↓< (length xs) ∪ I ↓≥ (length xs)"
  in subst)
 apply (simp add: cut_less_cut_ge_ident)
apply (rule_tac
  t = "I ↓< length xs" and
  s = "{..<length xs}"
  in subst)
 apply blast
apply (case_tac "I ↓≥ (length xs) = {}", simp)
apply (subst nths_disjoint_Un[OF finite_lessThan])
 apply (rule less_imp_Max_less_iMin[OF finite_lessThan])
   apply blast
  apply blast
 apply (blast intro: less_le_trans)
apply (fastforce simp: nths_empty_conv)
done

corollary nths_UNIV: "nths xs UNIV = xs"
by (rule nths_all[OF subset_UNIV])

lemma sublist_list_nths_eq: "⋀xs.
  list_strict_asc ys ⟹ sublist_list_if xs ys = nths xs (set ys)"
apply (case_tac "xs = []")
 apply (simp add: sublist_list_if_Nil_left)
apply (induct ys rule: rev_induct, simp)
apply (rename_tac y ys xs)
apply (case_tac "ys = []")
 apply (simp add: nths_singleton2)
apply (unfold list_strict_asc_def)
apply (simp add: sublist_list_if_snoc split del: if_split)
apply (frule list_ord_append[THEN iffD1])
apply (clarsimp split del: if_split)
apply (subst nths_disjoint_insert_right)
  apply simp
 apply (clarsimp simp: in_set_conv_nth, rename_tac i)
 apply (drule_tac i=i and j="length ys" in list_strict_asc_trans[unfolded list_strict_asc_def, THEN iffD1, rule_format])
 apply (simp add: nth_append split del: if_split)+
apply (simp add: nths_singleton2)
done

lemma set_sublist_list_if: "⋀xs. set (sublist_list_if xs ys) = {xs ! i |i. i < length xs ∧ i ∈ set ys}"
apply (induct ys, simp_all)
apply blast
done

lemma set_sublist_list: "
  list_all (λi. i < length xs) ys ⟹
  set (sublist_list xs ys) = {xs ! i |i. i < length xs ∧ i ∈ set ys}"
by (simp add: sublist_list_if_sublist_list_eq[symmetric] set_sublist_list_if)

lemma set_sublist_list_if_eq_set_sublist: "set (sublist_list_if xs ys) = set (nths xs (set ys))"
by (simp add: set_nths set_sublist_list_if)

lemma set_sublist_list_eq_set_sublist: "
  list_all (λi. i < length xs) ys ⟹
  set (sublist_list xs ys) = set (nths xs (set ys))"
by (simp add: sublist_list_if_sublist_list_eq[symmetric] set_sublist_list_if_eq_set_sublist)


subsubsection ‹Natural set images with lists›

definition f_image :: "'a list ⇒ nat set ⇒ 'a set"    (infixr ‹`⇧f› 90)
  where "xs `⇧f A ≡ {y. ∃n∈A. n < length xs ∧ y = xs ! n}"

abbreviation f_range :: "'a list ⇒ 'a set"
  where "f_range xs ≡ f_image xs UNIV"

lemma f_image_eqI[simp, intro]: "
  ⟦ x = xs ! n; n ∈ A; n < length xs ⟧ ⟹ x ∈ xs `⇧f A"
by (unfold f_image_def, blast)

lemma f_imageI: "⟦ n ∈ A; n < length xs ⟧ ⟹ xs ! n ∈ xs `⇧f A"
by blast

lemma rev_f_imageI: "⟦ n ∈ A; n < length xs; x = xs ! n ⟧ ⟹ x ∈ xs `⇧f A"
by (rule f_image_eqI)

lemma f_imageE[elim!]: "
  ⟦ x ∈ xs `⇧f A; ⋀n. ⟦ x = xs ! n; n ∈ A; n < length xs ⟧ ⟹ P ⟧ ⟹ P"
by (unfold f_image_def, blast)

lemma f_image_Un: "xs `⇧f (A ∪ B) = xs `⇧f A ∪ xs `⇧f B"
by blast

lemma f_image_mono: "A ⊆ B ==> xs `⇧f A ⊆ xs `⇧f B"
by blast

lemma f_image_iff: "(x ∈ xs `⇧f A) = (∃n∈A. n < length xs ∧ x = xs ! n)"
by blast

lemma f_image_subset_iff: "
  (xs `⇧f A ⊆ B) = (∀n∈A. n < length xs ⟶ xs ! n ∈ B)"
by blast

lemma subset_f_image_iff: "(B ⊆ xs `⇧f A) = (∃A'⊆A. B = xs `⇧f A')"
apply (rule iffI)
 apply (rule_tac x="{ n. n ∈ A ∧ n < length xs ∧ xs ! n ∈ B }" in exI)
 apply blast
apply (blast intro: f_image_mono)
done

lemma f_image_subsetI: "
  ⟦ ⋀n. n ∈ A ∧ n < length xs ⟹ xs ! n ∈ B ⟧ ⟹ xs `⇧f A ⊆ B"
by blast

lemma f_image_empty: "xs `⇧f {} = {}"
by blast

lemma f_image_insert_if: "
  xs `⇧f (insert n A) = (
  if n < length xs then insert (xs ! n) (xs `⇧f A) else (xs `⇧f A))"
by (split if_split, blast)

lemma f_image_insert_eq1: "
  n < length xs ⟹ xs `⇧f (insert n A) = insert (xs ! n) (xs `⇧f A)"
by (simp add: f_image_insert_if)

lemma f_image_insert_eq2: "
  length xs ≤ n ⟹ xs `⇧f (insert n A) = (xs `⇧f A)"
by (simp add: f_image_insert_if)

lemma insert_f_image: "
  ⟦ n ∈ A; n < length xs ⟧ ⟹ insert (xs ! n) (xs `⇧f A) = (xs `⇧f A)"
by blast

lemma f_image_is_empty: "(xs `⇧f A = {}) = ({x. x ∈ A ∧ x < length xs} = {})"
by blast

lemma f_image_Collect: "xs `⇧f {n. P n} = {xs ! n |n. P n ∧ n < length xs}"
by blast


lemma f_image_eq_set: "∀n<length xs. n ∈ A ⟹ xs `⇧f A = set xs"
by (fastforce simp: in_set_conv_nth)
lemma f_range_eq_set: "f_range xs = set xs"
by (simp add: f_image_eq_set)

lemma f_image_eq_set_nths: "xs `⇧f A = set (nths xs A)"
by (unfold set_nths, blast)
lemma f_image_eq_set_sublist_list_if: "xs `⇧f (set ys) = set (sublist_list_if xs ys)"
by (simp add: set_sublist_list_if_eq_set_sublist f_image_eq_set_nths)
lemma f_image_eq_set_sublist_list: "
  list_all (λi. i < length xs) ys ⟹ xs `⇧f (set ys) = set (sublist_list xs ys)"
by (simp add: sublist_list_if_sublist_list_eq f_image_eq_set_sublist_list_if)


lemma f_range_eqI: "⟦ x = xs ! n; n < length xs ⟧ ⟹ x ∈ f_range xs"
by blast

lemma f_rangeI: "n < length xs ⟹ xs ! n ∈ f_range xs"
by blast

lemma f_rangeE[elim?]: "
  ⟦ x ∈ f_range xs; ⋀n. ⟦ n < length xs; x = xs ! n ⟧ ⟹ P ⟧ ⟹ P"
by blast


subsubsection ‹Mapping lists of functions to lists›

primrec map_list :: "('a ⇒ 'b) list ⇒ 'a list ⇒ 'b list"
where
  "map_list [] xs = []"
| "map_list (f # fs) xs = f (hd xs) # map_list fs (tl xs)"

lemma map_list_Nil: "map_list [] xs = []"
by simp

lemma map_list_Cons_Cons: "
  map_list (f # fs) (x # xs) =
  (f x) # map_list fs xs"
by simp

lemma map_list_length: "⋀xs.
  length (map_list fs xs) = length fs"
by (induct fs, simp+)
corollary map_list_empty_conv: "
  (map_list fs xs = []) = (fs = [])"
by (simp del: length_0_conv add: length_0_conv[symmetric] map_list_length)
corollary map_list_not_empty_conv: "
  (map_list fs xs ≠ []) = (fs ≠ [])"
by (simp add: map_list_empty_conv)

lemma map_list_nth: "⋀n xs.
  ⟦ n < length fs; n < length xs ⟧ ⟹
  (map_list fs xs ! n) =
  (fs ! n) (xs ! n)"
apply (induct fs, simp+)
apply (case_tac n)
 apply (simp add: hd_conv_nth)
apply (simp add: nth_tl_eq_nth_Suc2)
done

lemma map_list_xs_take: "⋀n xs.
  length fs ≤ n ⟹
  map_list fs (xs ↓ n) =
  map_list fs xs"
apply (induct fs, simp+)
apply (rename_tac fs n xs)
apply (simp add: tl_take)
done

lemma map_list_take: "⋀n xs.
  (map_list fs xs) ↓ n =
  (map_list (fs ↓ n) xs)"
apply (induct fs, simp)
apply (case_tac n, simp+)
done
lemma map_list_take_take: "⋀n xs.
  (map_list fs xs) ↓ n =
  (map_list (fs ↓ n) (xs ↓ n))"
by (simp add: map_list_take map_list_xs_take)
lemma map_list_drop: "⋀n xs.
  (map_list fs xs) ↑ n =
  (map_list (fs ↑ n) (xs ↑ n))"
apply (induct fs, simp)
apply (case_tac n)
apply (simp add: drop_Suc)+
done



lemma map_list_append_append: "⋀xs1 .
  length fs1 = length xs1 ⟹
  map_list (fs1 @ fs2) (xs1 @ xs2) =
  map_list fs1 xs1 @
  map_list fs2 xs2"
apply (induct fs1, simp+)
apply (case_tac "xs1", simp+)
done
lemma map_list_snoc_snoc: "
  length fs = length xs ⟹
  map_list (fs @ [f]) (xs @ [x]) =
  map_list fs xs @ [f x]"
by (simp add: map_list_append_append)
lemma map_list_snoc: "⋀xs.
  length fs < length xs ⟹
  map_list (fs @ [f]) xs =
  map_list fs xs @  [f (xs ! (length fs))]"
apply (induct fs)
 apply (simp add: hd_conv_nth)
apply (simp add: nth_tl_eq_nth_Suc2)
done


lemma map_list_Cons_if: "
  map_list fs (x # xs) =
  (if (fs = []) then [] else (
    ((hd fs) x) # map_list (tl fs) xs))"
by (case_tac "fs", simp+)
lemma map_list_Cons_not_empty: "
  fs ≠ [] ⟹
  map_list fs (x # xs) =
  ((hd fs) x) # map_list (tl fs) xs"
by (simp add: map_list_Cons_if)

lemma map_eq_map_list_take: "⋀xs.
  ⟦ length fs ≤ length xs; list_all (λx. x = f) fs ⟧ ⟹
  map_list fs xs = map f (xs ↓ length fs)"
apply (induct fs, simp+)
apply (case_tac xs, simp+)
done
lemma map_eq_map_list_take2: "
  ⟦ length fs = length xs; list_all (λx. x = f) fs ⟧ ⟹
  map_list fs xs = map f xs"
by (simp add: map_eq_map_list_take)
lemma map_eq_map_list_replicate: "
  map_list (f⇗length xs⇖) xs = map f xs"
by (induct xs, simp+)


subsubsection ‹Mapping functions with two arguments to lists›

primrec map2 :: "
  ― ‹Function taking two parameters›
  ('a ⇒ 'b ⇒ 'c) ⇒
  ― ‹Lists of parameters›
  'a list ⇒ 'b list ⇒
  'c list"
where
  "map2 f [] ys = []"
| "map2 f (x # xs) ys = f x (hd ys) # map2 f xs (tl ys)"


lemma map2_map_list_conv: "⋀ys. map2 f xs ys = map_list (map f xs) ys"
by (induct xs, simp+)

lemma map2_Nil: "map2 f [] ys = []"
by simp
lemma map2_Cons_Cons: "
  map2 f (x # xs) (y # ys) =
  (f x y) # map2 f xs ys"
by simp

lemma map2_length: "⋀ys. length (map2 f xs ys) = length xs"
by (induct xs, simp+)
corollary map2_empty_conv: "
  (map2 f xs ys = []) = (xs = [])"
by (simp del: length_0_conv add: length_0_conv[symmetric] map2_length)
corollary map2_not_empty_conv: "
  (map2 f xs ys ≠ []) = (xs ≠ [])"
by (simp add: map2_empty_conv)

lemma map2_nth: "⋀n ys.
  ⟦ n < length xs; n < length ys ⟧ ⟹
  (map2 f xs ys ! n) =
  f (xs ! n) (ys ! n)"
by (simp add: map2_map_list_conv map_list_nth)

lemma map2_ys_take: "⋀n ys.
  length xs ≤ n ⟹
  map2 f xs (ys ↓ n) =
  map2 f xs ys"
by (simp add: map2_map_list_conv map_list_xs_take)

lemma map2_take: "⋀n ys.
  (map2 f xs ys) ↓ n =
  (map2 f (xs ↓ n) ys)"
by (simp add: map2_map_list_conv take_map map_list_take)

lemma map2_take_take: "⋀n ys.
  (map2 f xs ys) ↓ n =
  (map2 f (xs ↓ n) (ys ↓ n))"
by (simp add: map2_take map2_ys_take)

lemma map2_drop: "⋀n ys.
  (map2 f xs ys) ↑ n =
  (map2 f (xs ↑ n) (ys ↑ n))"
by (simp add: map2_map_list_conv map_list_drop drop_map)


lemma map2_append_append: "⋀ys1 .
  length xs1 = length ys1 ⟹
  map2 f (xs1 @ xs2) (ys1 @ ys2) =
  map2 f xs1 ys1 @
  map2 f xs2 ys2"
by (simp add: map2_map_list_conv map_list_append_append)

lemma map2_snoc_snoc: "
  length xs = length ys ⟹
  map2 f (xs @ [x]) (ys @ [y]) =
  map2 f xs ys @
  [f x y]"
by (simp add: map2_append_append)

lemma map2_snoc: "⋀ys.
  length xs < length ys ⟹
  map2 f (xs @ [x]) ys =
  map2 f xs ys @
  [f x (ys ! (length xs))]"
by (simp add: map2_map_list_conv map_list_snoc)

lemma map2_Cons_if: "
  map2 f xs (y # ys) =
  (if (xs = []) then [] else (
    (f (hd xs) y) # map2 f (tl xs) ys))"
by (case_tac "xs", simp+)
lemma map2_Cons_not_empty: "
  xs ≠ [] ⟹
  map2 f xs (y # ys) =
  (f (hd xs) y) # map2 f (tl xs) ys"
by (simp add: map2_Cons_if)

lemma map2_append1_take_drop: "
  length xs1 ≤ length ys ⟹
  map2 f (xs1 @ xs2) ys =
  map2 f xs1 (ys ↓ length xs1) @
  map2 f xs2 (ys ↑ length xs1)"
apply (rule_tac
  t = "map2 f (xs1 @ xs2) ys" and
  s = "map2 f (xs1 @ xs2) (ys ↓ length xs1 @ ys ↑ length xs1)"
  in subst)
 apply simp
apply (simp add: map2_append_append del: append_take_drop_id)
done

lemma map2_append2_take_drop: "
  length ys1 ≤ length xs ⟹
  map2 f xs (ys1 @ ys2) =
  map2 f (xs ↓ length ys1) ys1 @
  map2 f (xs ↑ length ys1) ys2"
apply (rule_tac
  t = "map2 f xs (ys1 @ ys2)" and
  s = "map2 f (xs ↓ length ys1 @ xs ↑ length ys1) (ys1 @ ys2)"
  in subst)
 apply simp
apply (simp add: map2_append_append del: append_take_drop_id)
done

lemma map2_cong: "
  ⟦ xs1 = xs2; ys1 = ys2; length xs2 ≤ length ys2;
    ⋀x y. ⟦ x ∈ set xs2; y ∈ set ys2 ⟧ ⟹ f x y = g x y ⟧ ⟹
  map2 f xs1 ys1 = map2 g xs2 ys2"
by (simp (no_asm_simp) add: expand_list_eq map2_length map2_nth)

lemma map2_eq_conv: "
  length xs ≤ length ys ⟹
  (map2 f xs ys = map2 g xs ys) = (∀i<length xs. f (xs ! i) (ys ! i) = g (xs ! i) (ys ! i))"
by (simp add: expand_list_eq map2_length map2_nth)

lemma map2_replicate: "map2 f x⇗n⇖ y⇗n⇖ = (f x y)⇗n⇖"
by (induct n, simp+)

lemma map2_zip_conv: "⋀ys.
  length xs ≤ length ys ⟹
  map2 f xs ys = map (λ(x,y). f x y) (zip xs ys)"
apply (induct xs, simp)
apply (case_tac ys, simp+)
done

lemma map2_rev: "⋀ys.
  length xs = length ys ⟹
  rev (map2 f xs ys) = map2 f (rev xs) (rev ys)"
apply (induct xs, simp)
apply (case_tac ys, simp)
apply (simp add: map2_Cons_Cons map2_snoc_snoc)
done

hide_const (open) map2

end