Theory ListInf

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

section ‹Additional definitions and results for lists›

theory ListInf
imports List2 "../CommonSet/InfiniteSet2"
begin

subsection ‹Infinite lists›

text ‹
  We define infinite lists as functions over natural numbers, i. e.,
  we use functions @{typ "nat ⇒ 'a"}
  as infinite lists over elements of @{typ "'a"}.
  Mapping functions to intervals lists ‹[m..<n]›
  yiels common finite lists.›


subsubsection ‹Appending a functions to a list›

type_synonym 'a ilist = "nat ⇒ 'a"

definition i_append :: "'a list ⇒ 'a ilist ⇒ 'a ilist" (infixr "⌢" 65)
  where "xs ⌢ f ≡ λn. if n < length xs then xs ! n else f (n - length xs)"

text ‹
  Synonym for the lemma ‹fun_eq_iff›
  from the HOL library to unify lemma names for finite and infinite lists,
  providing ‹list_eq_iff› for finite and
  ‹ilist_eq_iff› for infinite lists.›
lemmas expand_ilist_eq = fun_eq_iff
lemmas ilist_eq_iff = expand_ilist_eq

lemma i_append_nth: "(xs ⌢ f) n = (if n < length xs then xs ! n else f (n - length xs))"
by (simp add: i_append_def)
lemma i_append_nth1[simp]: "n < length xs ⟹ (xs ⌢ f) n = xs ! n"
by (simp add: i_append_def)
lemma i_append_nth2[simp]: "length xs ≤ n ⟹ (xs ⌢ f) n = f (n - length xs)"
by (simp add: i_append_def)
lemma i_append_Nil[simp]: "[] ⌢ f = f"
by (simp add: i_append_def)

lemma i_append_assoc[simp]: "xs ⌢ (ys ⌢ f) = (xs @ ys) ⌢ f"
apply (case_tac "ys = []", simp)
apply (fastforce simp: expand_ilist_eq i_append_def nth_append)
done

lemma i_append_Cons: "(x # xs) ⌢ f = [x] ⌢ (xs ⌢ f)"
by simp

lemma i_append_eq_i_append_conv[simp]: "
  length xs = length ys ⟹
  (xs ⌢ f = ys ⌢ g) = (xs = ys ∧ f = g)"
apply (rule iffI)
 prefer 2
 apply simp
apply (simp add: expand_ilist_eq expand_list_eq i_append_nth)
apply (intro conjI impI allI)
 apply (rename_tac x)
 apply (drule_tac x=x in spec)
 apply simp
apply (rename_tac x)
apply (drule_tac x="x + length ys" in spec)
apply simp
done

lemma i_append_eq_i_append_conv2_aux: "
  ⟦ xs ⌢ f = ys ⌢ g; length xs ≤ length ys ⟧ ⟹
  ∃zs. xs @ zs = ys ∧ f = zs ⌢ g"
apply (simp add: expand_ilist_eq expand_list_eq nth_append)
apply (rule_tac x="drop (length xs) ys" in exI)
apply simp
apply (rule conjI)
 apply (clarify, rename_tac i)
 apply (drule_tac x=i in spec)
 apply simp
apply (clarify, rename_tac i)
apply (drule_tac x="length xs + i" in spec)
apply (simp add: i_append_nth)
apply (case_tac "length xs + i < length ys")
 apply fastforce
apply (fastforce simp: add.commute[of _ "length xs"])
done

lemma i_append_eq_i_append_conv2: "
  (xs ⌢ f = ys ⌢ g) =
  (∃zs. xs = ys @ zs ∧ zs ⌢ f = g ∨ xs @ zs = ys ∧ f = zs ⌢ g)"
apply (rule iffI)
 apply (case_tac "length xs ≤ length ys")
  apply (frule i_append_eq_i_append_conv2_aux, assumption)
  apply blast
 apply (simp add: linorder_not_le eq_commute[of "xs ⌢ f"], drule less_imp_le)
 apply (frule i_append_eq_i_append_conv2_aux, assumption)
 apply blast
apply fastforce
done

lemma same_i_append_eq[iff]: "(xs ⌢ f = xs ⌢ g) = (f = g)"
apply (rule iffI)
 apply (clarsimp simp: expand_ilist_eq, rename_tac i)
 apply (erule_tac x="length xs + i" in allE)
 apply simp
apply simp
done


lemma NOT_i_append_same_eq: "
  ¬(∀xs ys f. (xs ⌢ (f::(nat ⇒ nat)) = ys ⌢ f) = (xs = ys))"
apply simp
apply (rule_tac x="[]" in exI)
apply (rule_tac x="[0]" in exI)
apply (rule_tac x="λn. 0" in exI)
apply (simp add: expand_ilist_eq i_append_nth)
done

lemma i_append_hd: "(xs ⌢ f) 0 = (if xs = [] then f 0 else hd xs)"
by (simp add: hd_eq_first)

lemma i_append_hd2[simp]: "xs ≠ [] ⟹ (xs ⌢ f) 0 = hd xs"
by (simp add: i_append_hd)

lemma eq_Nil_i_appendI: "f = g ⟹ f = [] ⌢ g"
by simp

lemma i_append_eq_i_appendI: "
  ⟦ xs @ xs' = ys; f = xs' ⌢ g ⟧ ⟹ xs ⌢ f = ys ⌢ g"
by simp


lemma o_ext: "
  (∀x. (x ∈ range h ⟶ f x = g x)) ⟹ f ∘ h = g ∘ h"
by (simp add: expand_ilist_eq)

lemma i_append_o[simp]: "g ∘ (xs ⌢ f) = (map g xs) ⌢ (g ∘ f)"
by (simp add: expand_ilist_eq i_append_nth)

lemma o_eq_conv: "(f ∘ h = g ∘ h) = (∀x∈range h. f x = g x)"
by (simp add: expand_ilist_eq)

lemma o_cong: "
  ⟦ h = i; ⋀x. x ∈ range i ⟹ f x = g x ⟧ ⟹ f ∘ h = f ∘ i"
by blast

lemma ex_o_conv: "(∃h. g = f ∘ h) = (∀y∈range g. ∃x. y = f x)"
apply (rule iffI)
 apply fastforce
apply (simp add: expand_ilist_eq)
apply (rule_tac x="λx. (SOME y. g x = f y)" in exI)
apply (fastforce intro: someI_ex)
done

lemma o_inj_on: "
  ⟦ f ∘ g = f ∘ h; inj_on f (range g ∪ range h) ⟧ ⟹ g = h"
apply (rule expand_ilist_eq[THEN iffD2], clarify, rename_tac x)
apply (drule_tac x=x in fun_cong)
apply (rule inj_onD)
apply simp+
done

lemma inj_on_o_eq_o: "
  inj_on f (range g ∪ range h) ⟹
  (f ∘ g = f ∘ h) = (g = h)"
apply (rule iffI)
 apply (rule o_inj_on, assumption+)
apply simp
done

lemma o_injective: "⟦ f ∘ g = f ∘ h; inj f ⟧ ⟹ g = h"
by (simp add: expand_ilist_eq inj_on_def)

lemma inj_o_eq_o: "inj f ⟹ (f ∘ g = f ∘ h) = (g = h)"
apply (rule iffI)
 apply (rule o_injective, assumption+)
apply simp
done

lemma inj_oI: "inj f ⟹ inj (λg. f ∘ g)"
apply (simp add: inj_on_def)
apply (blast intro: o_inj_on[unfolded inj_on_def])
done

lemma inj_oD: "inj (λg. f ∘ g) ⟹ inj f"
apply (clarsimp simp add: inj_on_def, rename_tac g h)
apply (erule_tac x="λn. g" in allE)
apply (erule_tac x="λn. h" in allE)
apply (simp add: expand_ilist_eq)
done

lemma inj_o[iff]: "inj (λg. f ∘ g) = inj f"
apply (rule iffI)
 apply (rule inj_oD, assumption)
apply (rule inj_oI, assumption)
done

lemma inj_on_oI: "
  inj_on f (⋃ ((λf. range f) ` A)) ⟹ inj_on (λg. f ∘ g) A"
apply (rule inj_onI)
apply (rule o_inj_on, assumption)
apply (unfold inj_on_def)
apply force
done

lemma o_idI: "∀x. x ∈ range g ⟶ f x = x ⟹ f ∘ g = g"
by (simp add: expand_ilist_eq)

lemma o_fun_upd[simp]: "y ∉ range g ⟹ f (y := x) ∘ g = f ∘ g"
by (fastforce simp: expand_ilist_eq)

lemma range_i_append[simp]: "range (xs ⌢ f) = set xs ∪ range f"
by (fastforce simp: in_set_conv_nth i_append_nth)

lemma set_subset_i_append: "set xs ⊆ range (xs ⌢ f)"
by simp

lemma range_subset_i_append: "range f ⊆ range (xs ⌢ f)"
by simp

lemma range_ConsD: "y ∈ range ([x] ⌢ f) ⟹ y = x ∨ y ∈ range f"
by simp

lemma range_o [simp]: "range (f ∘ g) = f ` range g"
by (simp add: image_comp)

lemma in_range_conv_decomp: "
  (x ∈ range f) = (∃xs g. f = xs ⌢ ([x] ⌢ g))"
apply (simp add: image_iff)
apply (rule iffI)
 apply (clarify, rename_tac n)
 apply (rule_tac x="map f [0..<n]" in exI)
 apply (rule_tac x="λi. f (i + Suc n)" in exI)
 apply (simp add: expand_ilist_eq i_append_nth nth_append linorder_not_less less_Suc_eq_le)
apply (clarify, rename_tac xs g)
apply (rule_tac x="length xs" in exI)
apply simp
done


text ‹‹nth››

lemma i_append_nth_Cons_0[simp]: "((x # xs) ⌢ f) 0 = x"
by simp

lemma i_append_nth_Cons_Suc[simp]:
  "((x # xs) ⌢ f) (Suc n) = (xs ⌢ f) n"
by (simp add: i_append_nth)

lemma i_append_nth_Cons: "
  ([x] ⌢ f) n = (case n of 0 ⇒ x | Suc k ⇒ f k)"
by (case_tac n, simp_all add: i_append_nth)

lemma i_append_nth_Cons': "
  ([x] ⌢ f) n = (if n = 0 then x else f (n - Suc 0))"
by (case_tac n, simp_all add: i_append_nth)

lemma i_append_nth_length[simp]: "(xs ⌢ f) (length xs) = f 0"
by simp

lemma i_append_nth_length_plus[simp]: "(xs ⌢ f) (length xs + n) = f n"
by simp

lemma range_iff: "(y ∈ range f) = (∃x. y = f x)"
by blast

lemma range_ball_nth: "∀y∈range f. P y ⟹ P (f x)"
by blast

lemma all_nth_imp_all_range: "⟦ ∀x. P (f x);y ∈ range f ⟧ ⟹ P y"
by blast

lemma all_range_conv_all_nth: "(∀y∈range f. P y) = (∀x. P (f x))"
by blast

lemma i_append_update1: "
  n < length xs ⟹ (xs ⌢ f) (n := x) = xs[n := x] ⌢ f"
by (simp add: expand_ilist_eq i_append_nth)

lemma i_append_update2: "
  length xs ≤ n ⟹ (xs ⌢ f) (n := x) = xs ⌢ (f(n - length xs := x))"
by (fastforce simp: expand_ilist_eq i_append_nth)

lemma i_append_update: "
  (xs ⌢ f) (n := x) =
  (if n < length xs then xs[n := x] ⌢ f
   else xs ⌢ (f(n - length xs := x)))"
by (simp add: i_append_update1 i_append_update2)

lemma i_append_update_length[simp]: "
  (xs ⌢ f) (length xs := y) = xs ⌢ (f(0 := y))"
by (simp add: i_append_update2)

lemma range_update_subset_insert: "
  range (f(n := x)) ⊆ insert x (range f)"
by fastforce

lemma range_update_subsetI: "
  ⟦ range f ⊆ A; x ∈ A ⟧ ⟹ range (f(n := x)) ⊆ A"
by fastforce

lemma range_update_memI: "x ∈ range (f(n := x))"
by fastforce


subsubsection ‹@{term take} and @{term drop} for infinite lists›

text ‹
  The @{term i_take} operator takes the first @{term n} elements of an infinite list,
  i.e. ‹i_take f n = [f 0, f 1, …, f (n-1)]›.
  The @{term i_drop} operator drops the first @{term n} elements of an infinite list,
  i.e. ‹(i_take f n) 0 = f n, (i_take f n) 1 = f (n + 1), …›.›

definition i_take  :: "nat ⇒ 'a ilist ⇒ 'a list"
  where "i_take n f ≡ map f [0..<n]"
definition i_drop  :: "nat ⇒ 'a ilist ⇒ 'a ilist"
  where "i_drop n f ≡ (λx. f (n + x))"

abbreviation i_take' :: "'a ilist ⇒ nat ⇒ 'a list"  (infixl "⇓" 100)
  where "f ⇓ n ≡ i_take n f"
abbreviation i_drop' :: "'a ilist ⇒ nat ⇒ 'a ilist"  (infixl "⇑" 100)
  where "f ⇑ n ≡ i_drop n f"

lemma "f ⇓ n = map f [0..<n]"
by (simp add: i_take_def)
lemma "f ⇑ n = (λx. f (n + x))"
by (simp add: i_drop_def)


text ‹Basic results for @{term i_take} and @{term i_drop}›

lemma i_take_first: "f ⇓ Suc 0 = [f 0]"
by (simp add: i_take_def)

lemma i_drop_i_take_1: "f ⇑ n ⇓ Suc 0 = [f n]"
by (simp add: i_drop_def i_take_def)

lemma i_take_take_eq1: "m ≤ n ⟹ (f ⇓ n) ↓ m = f ⇓ m"
by (simp add: i_take_def take_map)

lemma i_take_take_eq2: "n ≤ m ⟹ (f ⇓ n) ↓ m = f ⇓ n"
by (simp add: i_take_def take_map)

lemma i_take_take[simp]: "(f ⇓ n) ↓ m = f ⇓ min n m"
by (simp add: min_def i_take_take_eq1 i_take_take_eq2)

lemma i_drop_nth[simp]: "(s ⇑ n) x = s (n + x)"
by (simp add: i_drop_def)

lemma i_drop_nth_sub: "n ≤ x ⟹ (s ⇑ n) (x - n) = s x"
by (simp add: i_drop_def)

theorem i_take_nth[simp]: "i < n ⟹ (f ⇓ n) ! i = f i"
by (simp add: i_take_def)

lemma i_take_length[simp]: "length (f ⇓ n) = n"
by (simp add: i_take_def)

lemma i_take_0[simp]: "f ⇓ 0 = []"
by (simp add: i_take_def)

lemma i_drop_0[simp]: "f ⇑ 0 = f"
by (simp add: i_drop_def)

lemma i_take_eq_Nil[simp]: "(f ⇓ n = []) = (n = 0)"
by (simp add: length_0_conv[symmetric] del: length_0_conv)

lemma i_take_not_empty_conv: "(f ⇓ n ≠ []) = (0 < n)"
by simp

lemma last_i_take: "last (f ⇓ Suc n) = f n"
by (simp add: last_nth)

lemma last_i_take2: "0 < n ⟹ last (f ⇓ n) = f (n - Suc 0)"
by (simp add: last_i_take[of _ f, symmetric])

lemma nth_0_i_drop: "(f ⇑ n) 0 = f n"
by simp

lemma i_take_const[simp]: "(λn. x) ⇓ i = replicate i x"
by (simp add: expand_list_eq)

lemma i_drop_const[simp]: "(λn. x) ⇑ i = (λn. x)"
by (simp add: expand_ilist_eq)

lemma i_append_i_take_eq1: "
  n ≤ length xs ⟹ (xs ⌢ f) ⇓ n = xs ↓ n"
by (simp add: expand_list_eq)

lemma i_append_i_take_eq2: "
  length xs ≤ n ⟹ (xs ⌢ f) ⇓ n = xs @ (f ⇓ (n - length xs))"
by (simp add: expand_list_eq nth_append)

lemma i_append_i_take_if: "
  (xs ⌢ f) ⇓ n = (if n ≤ length xs then xs ↓ n else xs @ (f ⇓ (n - length xs)))"
by (simp add: i_append_i_take_eq1 i_append_i_take_eq2)

lemma i_append_i_take[simp]: "
  (xs ⌢ f) ⇓ n = (xs ↓ n) @ (f ⇓ (n - length xs))"
by (simp add: i_append_i_take_if)

lemma i_append_i_drop_eq1: "
  n ≤ length xs ⟹ (xs ⌢ f) ⇑ n = (xs ↑ n) ⌢ f"
by (simp add: expand_ilist_eq i_append_nth less_diff_conv add.commute[of _ n])

lemma i_append_i_drop_eq2: "
  length xs ≤ n ⟹ (xs ⌢ f) ⇑ n = f ⇑ (n - length xs)"
by (simp add: expand_ilist_eq i_append_nth)

lemma i_append_i_drop_if: "
  (xs ⌢ f) ⇑ n = (if n < length xs then (xs ↑ n) ⌢ f else f ⇑ (n - length xs))"
by (simp add: i_append_i_drop_eq1 i_append_i_drop_eq2)

lemma i_append_i_drop[simp]: "(xs ⌢ f) ⇑ n = (xs ↑ n) ⌢ (f ⇑ (n - length xs))"
by (simp add: i_append_i_drop_if)

lemma i_append_i_take_i_drop_id[simp]: "(f ⇓ n) ⌢ (f ⇑ n) = f"
by (simp add: expand_ilist_eq i_append_nth)

lemma ilist_i_take_i_drop_imp_eq: "
  ⟦ f ⇓ n  = g ⇓ n; f ⇑ n = g ⇑ n ⟧ ⟹ f = g"
apply (subst i_append_i_take_i_drop_id[of n f, symmetric])
apply (subst i_append_i_take_i_drop_id[of n g, symmetric])
apply simp
done

lemma ilist_i_take_i_drop_eq_conv: "
  (f = g) = (∃n. (f ⇓ n = g ⇓ n ∧ f ⇑ n = g ⇑ n))"
apply (rule iffI, simp)
apply (blast intro: ilist_i_take_i_drop_imp_eq)
done

lemma ilist_i_take_eq_conv: "(f = g) = (∀n. f ⇓ n = g ⇓ n)"
apply (rule iffI, simp)
apply (clarsimp simp: expand_ilist_eq, rename_tac i)
apply (drule_tac x="Suc i" in spec)
apply (drule_tac f="λxs. xs ! i" in arg_cong)
apply simp
done

lemma ilist_i_drop_eq_conv: "(f = g) = (∀n. f ⇑ n = g ⇑ n)"
apply (rule iffI, simp)
apply (drule_tac x=0 in spec)
apply simp
done

lemma i_take_the_conv: "
  f ⇓ k = (THE xs. length xs = k ∧ (∃g. xs ⌢ g = f))"
apply (rule the1I2)
 apply (rule_tac a="f ⇓ k" in ex1I)
 apply (fastforce intro: i_append_i_take_i_drop_id)+
done

lemma i_drop_the_conv: "
  f ⇑ k = (THE g. (∃xs. length xs = k ∧ xs ⌢ g = f))"
apply (rule sym, rule the1_equality)
 apply (rule_tac a="f ⇑ k" in ex1I)
  apply (rule_tac x="f ⇓ k" in exI, simp)
 apply clarsimp
apply (rule_tac x="f ⇓ k" in exI, simp)
done

lemma i_take_Suc_append[simp]: "
  ((x # xs) ⌢ f) ⇓ Suc n = x # ((xs ⌢ f) ⇓ n)"
by (simp add: expand_list_eq)

corollary i_take_Suc_Cons: "([x] ⌢ f) ⇓ Suc n = x # (f ⇓ n)"
by simp

lemma i_drop_Suc_append[simp]: "((x # xs) ⌢ f) ⇑ Suc n = ((xs ⌢ f) ⇑ n)"
by (simp add: expand_list_eq)

corollary i_drop_Suc_Cons: "([x] ⌢ f) ⇑ Suc n = f ⇑ n"
by simp

lemma i_take_Suc: "f ⇓ Suc n = f 0 # (f ⇑ Suc 0 ⇓ n)"
by (simp add: expand_list_eq nth_Cons')

lemma i_take_Suc_conv_app_nth: "f ⇓ Suc n = (f ⇓ n) @ [f n]"
by (simp add: i_take_def)

lemma i_drop_i_drop[simp]: "s ⇑ a ⇑ b = s ⇑ (a + b)"
by (simp add: i_drop_def add.assoc)

corollary i_drop_Suc: "f ⇑ Suc 0 ⇑ n = f ⇑ Suc n"
by simp

lemma i_take_commute: "s ⇓ a ↓ b = s ⇓ b ↓ a"
by (simp add: ac_simps)

lemma i_drop_commute: "s ⇑ a ⇑ b = s ⇑ b ⇑ a"
by (simp add: add.commute[of a])

corollary i_drop_tl: "f ⇑ Suc 0 ⇑ n = f ⇑ n ⇑ Suc 0"
by simp

lemma nth_via_i_drop: "(f ⇑ n) 0 = x ⟹ f n = x"
by simp

lemma i_drop_Suc_conv_tl: "[f n] ⌢ (f ⇑ Suc n) = f ⇑ n"
by (simp add: expand_ilist_eq i_append_nth)

lemma i_drop_Suc_conv_tl': "([f n] ⌢ f) ⇑ Suc n = f ⇑ n"
by (simp add: i_drop_Suc_Cons)

lemma i_take_i_drop: "f ⇑ m ⇓ n = f ⇓ (n + m) ↑ m"
by (simp add: expand_list_eq)


text ‹Appending an interval of a function›
lemma i_take_int_append: "
  m ≤ n ⟹ (f ⇓ m) @ map f [m..<n] = f ⇓ n"
by (simp add: expand_list_eq nth_append)

lemma i_take_drop_map_empty_iff: "(f ⇓ n ↑ m = []) = (n ≤ m)"
by simp

lemma i_take_drop_map: "f ⇓ n ↑ m = map f [m..<n]"
by (simp add: expand_list_eq)

corollary i_take_drop_append[simp]: "
  m ≤ n ⟹ (f ⇓ m) @ (f ⇓ n ↑ m) = f ⇓ n"
by (simp add: i_take_drop_map i_take_int_append)

lemma i_take_drop: "f ⇓ n ↑ m = f ⇑ m ⇓ (n - m)"
by (simp add: expand_list_eq)

lemma i_take_o[simp]: "(f ∘ g) ⇓ n = map f (g ⇓ n)"
by (simp add: expand_list_eq)

lemma i_drop_o[simp]: "(f ∘ g) ⇑ n = f ∘ (g ⇑ n)"
by (simp add: expand_ilist_eq)

lemma set_i_take_subset: "set (f ⇓ n) ⊆ range f"
by (fastforce simp: in_set_conv_nth)

lemma range_i_drop_subset: "range (f ⇑ n) ⊆ range f"
by fastforce

lemma in_set_i_takeD: "x ∈ set (f ⇓ n) ⟹ x ∈ range f"
by (rule subsetD[OF set_i_take_subset])

lemma in_range_i_takeD: "x ∈ range (f ⇑ n) ⟹ x ∈ range f"
by (rule subsetD[OF range_i_drop_subset])

lemma i_append_eq_conv_conj: "
  ((xs ⌢ f) = g) = (xs = g ⇓ length xs ∧ f = g ⇑ length xs)"
apply (simp add: expand_ilist_eq expand_list_eq i_append_nth)
apply (rule iffI)
 apply (clarsimp, rename_tac x)
 apply (drule_tac x="length xs + x" in spec)
 apply simp
apply simp
done

lemma i_take_add: "f ⇓ (i + j) = (f ⇓ i) @ (f ⇑ i ⇓ j)"
by (simp add: expand_list_eq nth_append)

lemma i_append_eq_i_append_conv_if_aux: "
  length xs ≤ length ys ⟹
  (xs ⌢ f = ys ⌢ g) = (xs = ys ↓ length xs ∧ f = (ys ↑ length xs) ⌢ g)"
apply (simp add: expand_list_eq expand_ilist_eq i_append_nth min_eqR)
apply (rule iffI)
 apply simp
 apply (clarify, rename_tac x)
 apply (drule_tac x="length xs + x" in spec)
 apply (simp add: less_diff_conv add.commute[of _ "length xs"])
apply simp
done

lemma i_append_eq_i_append_conv_if: "
  (xs ⌢ f = ys ⌢ g) =
  (if length xs ≤ length ys
   then xs = ys ↓ length xs ∧ f = (ys ↑ length xs) ⌢ g
   else xs ↓ length ys = ys ∧ (xs ↑ length ys) ⌢ f = g)"
apply (split if_split, intro conjI impI)
 apply (simp add: i_append_eq_i_append_conv_if_aux)
apply (force simp: eq_commute[of "xs ⌢ f"] i_append_eq_i_append_conv_if_aux)
done

lemma i_take_hd_i_drop: "(f ⇓ n) @ [(f ⇑ n) 0] = f ⇓ Suc n"
by (simp add: i_take_Suc_conv_app_nth)

lemma id_i_take_nth_i_drop: "f = (f ⇓ n) ⌢ (([f n] ⌢ f) ⇑ Suc n)"
by (simp add: i_drop_Suc_Cons)

lemma upd_conv_i_take_nth_i_drop: "
  f (n := x) = (f ⇓ n) ⌢ ([x] ⌢ (f ⇑ Suc n))"
by (simp add: expand_ilist_eq nth_append i_append_nth)

theorem i_take_induct: "
  ⟦ P (f ⇓ 0); ⋀n. P (f ⇓ n) ⟹ P ( f ⇓ Suc n) ⟧ ⟹ P ( f ⇓ n)"
by (rule nat.induct)

theorem take_induct[rule_format]: "
  ⟦ P (s ↓ 0);
    ⋀n.  ⟦ Suc n < length s; P (s ↓ n) ⟧ ⟹ P ( s ↓ Suc n);
    i < length s⟧
  ⟹ P (s ↓ i)"
by (induct i, simp+)

theorem i_drop_induct: "
  ⟦ P (f ⇑ 0); ⋀n. P (f ⇑ n) ⟹ P ( f ⇑ Suc n) ⟧ ⟹ P ( f ⇑ n)"
by (rule nat.induct)

theorem f_drop_induct[rule_format]: "
  ⟦ P (s ↑ 0);
    ⋀n.  ⟦ Suc n < length s; P (s ↑ n) ⟧ ⟹ P ( s ↑ Suc n);
    i < length s⟧
  ⟹ P (s ↑ i)"
by (induct i, simp+)


lemma i_take_drop_eq_map: "f ⇑ m ⇓ n = map f [m..<m+n]"
by (simp add: expand_list_eq)

lemma o_eq_i_append_imp: "
  f ∘ g = ys ⌢ i ⟹
  ∃xs h. g = xs ⌢ h ∧ map f xs = ys ∧ f ∘ h = i"
apply (rule_tac x="g ⇓ (length ys)" in exI)
apply (rule_tac x="g ⇑ (length ys)" in exI)
apply (frule arg_cong[where f="λx. x ⇓ length ys"])
apply (drule arg_cong[where f="λx. x ⇑ length ys"])
apply simp
done

corollary o_eq_i_append_conv: "
  (f ∘ g = ys ⌢ i) =
  (∃xs h. g = xs ⌢ h ∧ map f xs = ys ∧ f ∘ h = i)"
by (fastforce simp: o_eq_i_append_imp)
corollary i_append_eq_o_conv: "
  (ys ⌢ i = f ∘ g) =
  (∃xs h. g = xs ⌢ h ∧ map f xs = ys ∧ f ∘ h = i)"
by (fastforce simp: o_eq_i_append_imp)


subsubsection ‹@{term zip} for infinite lists›

definition i_zip :: "'a ilist ⇒ 'b ilist ⇒ ('a × 'b) ilist"
  where "i_zip f g ≡ λn. (f n, g n)"

lemma i_zip_nth: "(i_zip f g) n = (f n, g n)"
by (simp add: i_zip_def)

lemma i_zip_swap: "(λ(y, x). (x, y)) ∘ i_zip g f = i_zip f g"
by (simp add: expand_ilist_eq i_zip_nth)

lemma i_zip_i_take: "(i_zip f g) ⇓ n = zip (f ⇓ n) (g ⇓ n)"
by (simp add: expand_list_eq i_zip_nth)

lemma i_zip_i_drop: "(i_zip f g) ⇑ n = i_zip (f ⇑ n) (g ⇑ n)"
by (simp add: expand_ilist_eq i_zip_nth)

lemma fst_o_izip: "fst ∘ (i_zip f g) = f"
by (simp add: expand_ilist_eq i_zip_nth)

lemma snd_o_i_zip: "snd ∘ (i_zip f g) = g"
by (simp add: expand_ilist_eq i_zip_nth)

lemma update_i_zip: "
  (i_zip f g)(n := xy) = i_zip (f(n := fst xy)) (g(n := snd xy))"
by (simp add: expand_ilist_eq i_zip_nth)

lemma i_zip_Cons_Cons: "
  i_zip ([x] ⌢ f) ([y] ⌢ g) = [(x, y)] ⌢ (i_zip f g)"
by (simp add: expand_ilist_eq i_zip_nth i_append_nth)

lemma i_zip_i_append1: "
  i_zip (xs ⌢ f) g = zip xs (g ⇓ length xs) ⌢ (i_zip f (g ⇑ length xs))"
by (simp add: expand_ilist_eq i_zip_nth i_append_nth)

lemma i_zip_i_append2: "
  i_zip f (ys ⌢ g) = zip (f ⇓ length ys) ys ⌢ (i_zip (f ⇑ length ys) g)"
by (simp add: expand_ilist_eq i_zip_nth i_append_nth)

lemma i_zip_append: "
  length xs = length ys ⟹
  i_zip (xs ⌢ f) (ys ⌢ g) = zip xs ys ⌢ (i_zip f g)"
by (simp add: expand_ilist_eq i_zip_nth i_append_nth)

lemma i_zip_range: "range (i_zip f g) = { (f n, g n)| n. True }"
by (fastforce simp: i_zip_nth)

lemma i_zip_update: "
  i_zip (f(n := x)) (g(n := y)) = (i_zip f g)( n := (x, y))"
by (simp add: update_i_zip)

lemma i_zip_const: "i_zip (λn. x) (λn. y) = (λn. (x, y))"
by (simp add: expand_ilist_eq i_zip_nth)


subsubsection ‹Mapping functions with two arguments to infinite lists›

definition i_map2 :: "
  ― ‹Function taking two parameters›
  ('a ⇒ 'b ⇒ 'c) ⇒
  ― ‹Lists of parameters›
  'a ilist ⇒ 'b ilist ⇒
  'c ilist"
where
  "i_map2 f xs ys ≡ λn. f (xs n) (ys n)"

lemma i_map2_nth: "(i_map2 f xs ys) n = f (xs n) (ys n)"
by (simp add: i_map2_def)

lemma i_map2_Cons_Cons: "
  i_map2 f ([x] ⌢ xs) ([y] ⌢ ys) =
  [f x y] ⌢ (i_map2 f xs ys)"
by (simp add: fun_eq_iff i_map2_nth i_append_nth_Cons')

lemma i_map2_take_ge: "
  n ≤ n1 ⟹
  i_map2 f xs ys ⇓ n =
  map2 f (xs ⇓ n) (ys ⇓ n1)"
by (simp add: expand_list_eq map2_length i_map2_nth map2_nth)
lemma i_map2_take_take: "
  i_map2 f xs ys ⇓ n =
  map2 f (xs ⇓ n) (ys ⇓ n)"
by (rule i_map2_take_ge[OF le_refl])

lemma i_map2_drop: "
  (i_map2 f xs ys) ⇑ n =
  (i_map2 f (xs ⇑ n) (ys ⇑ n))"
by (simp add: fun_eq_iff i_map2_nth)

lemma i_map2_append_append: "
  length xs1 = length ys1 ⟹
  i_map2 f (xs1 ⌢ xs) (ys1 ⌢ ys) =
  map2 f xs1 ys1 ⌢ i_map2 f xs ys"
by (simp add: fun_eq_iff i_map2_nth i_append_nth map2_length map2_nth)

lemma i_map2_Cons_left: "
  i_map2 f ([x] ⌢ xs) ys =
  [f x (ys 0)] ⌢ i_map2 f xs (ys ⇑ Suc 0)"
by (simp add: fun_eq_iff i_map2_nth i_append_nth_Cons')
lemma i_map2_Cons_right: "
  i_map2 f xs ([y] ⌢ ys) =
  [f (xs 0) y] ⌢ i_map2 f (xs ⇑ Suc 0) ys"
by (simp add: fun_eq_iff i_map2_nth i_append_nth_Cons')


lemma i_map2_append_take_drop_left: "
  i_map2 f (xs1 ⌢ xs) ys =
  map2 f xs1 (ys ⇓ length xs1) ⌢
  i_map2 f xs (ys ⇑ length xs1)"
by (simp add: fun_eq_iff map2_nth i_map2_nth i_append_nth map2_length)
lemma i_map2_append_take_drop_right: "
  i_map2 f xs (ys1 ⌢ ys) =
  map2 f (xs ⇓ length ys1) ys1 ⌢
  i_map2 f (xs ⇑ length ys1) ys"
by (simp add: fun_eq_iff map2_nth i_map2_nth i_append_nth map2_length)

lemma i_map2_cong: "
  ⟦ xs1 = xs2; ys1 = ys2;
    ⋀x y. ⟦ x ∈ range xs2; y ∈ range ys2 ⟧ ⟹ f x y = g x y ⟧ ⟹
  i_map2 f xs1 ys1 = i_map2 g xs2 ys2"
by (simp add: fun_eq_iff i_map2_nth)

lemma i_map2_eq_conv: "
  (i_map2 f xs ys = i_map2 g xs ys) = (∀i. f (xs i) (ys i) = g (xs i) (ys i))"
by (simp add: fun_eq_iff i_map2_nth)

lemma i_map2_replicate: "i_map2 f (λn. x) (λn. y)  = (λn. f x y)"
by (simp add: fun_eq_iff i_map2_nth)

lemma i_map2_i_zip_conv: "
  i_map2 f xs ys = (λ(x,y). f x y) ∘ (i_zip xs ys)"
by (simp add: fun_eq_iff i_map2_nth i_zip_nth)


subsection ‹Generalised lists as combination of finite and infinite lists›

subsubsection ‹Basic definitions›

datatype (gset: 'a) glist = FL "'a list" | IL "'a ilist" for map: gmap

definition glength :: "'a glist ⇒ enat"
where
  "glength a ≡ case a of
    FL xs ⇒ enat (length xs) |
    IL f  ⇒ ∞"

definition gCons :: "'a ⇒ 'a glist ⇒ 'a glist"  (infixr "#⇩g" 65)
where
  "x #⇩g a ≡ case a of
    FL xs ⇒ FL (x # xs) |
    IL g  ⇒ IL ([x] ⌢ g)"

definition gappend :: "'a glist ⇒ 'a glist ⇒ 'a glist"  (infixr "@⇩g" 65)
where
  "gappend a b ≡ case a of
    FL xs ⇒ (case b of FL ys ⇒ FL (xs @ ys) | IL f ⇒ IL (xs ⌢ f)) |
    IL f  ⇒ IL f"

definition gtake :: "enat ⇒ 'a glist ⇒ 'a glist"
where
  "gtake n a ≡ case n of
    enat m ⇒ FL (case a of
      FL xs ⇒ xs ↓ m |
      IL f  ⇒ f ⇓ m) |
    ∞ ⇒ a"

definition gdrop :: "enat ⇒ 'a glist ⇒ 'a glist"
where
  "gdrop n a ≡ case n of
    enat m ⇒ (case a of
      FL xs ⇒ FL (xs ↑ m) |
      IL f  ⇒ IL (f ⇑ m)) |
    ∞ ⇒ FL []"

definition gnth :: "'a glist ⇒ nat ⇒ 'a"  (infixl "!⇩g" 100)
where
  "a !⇩g n ≡ case a of
    FL xs ⇒ xs ! n |
    IL f  ⇒ f n"

abbreviation g_take' :: "'a glist ⇒ enat ⇒ 'a glist"  (infixl "↓⇩g" 100)
  where "a ↓⇩g n ≡ gtake n a"

abbreviation g_drop' :: "'a glist ⇒ enat ⇒ 'a glist"  (infixl "↑⇩g" 100)
  where "a ↑⇩g n ≡ gdrop n a"


subsubsection ‹‹glength››

lemma glength_fin[simp]: "glength (FL xs) = enat (length xs)"
by (simp add: glength_def)

lemma glength_infin[simp]: "glength (IL f) = ∞"
by (simp add: glength_def)

lemma gappend_glength[simp]: "glength (a @⇩g b) = glength a + glength b"
by (unfold gappend_def, case_tac a, case_tac b, simp+)

lemma gmap_glength[simp]: "glength (gmap f a) = glength a"
by (case_tac a, simp+)

lemma glength_0_conv[simp]: "(glength a = 0) = (a = FL [])"
by (unfold glength_def, case_tac a, simp+)

lemma glength_greater_0_conv[simp]: "(0 < glength a) = (a ≠ FL [])"
by (simp add: glength_0_conv[symmetric])

lemma glength_gSuc_conv: "
  (glength a = eSuc n) =
  (∃x b. a = x #⇩g b ∧ glength b = n)"
apply (unfold glength_def gCons_def, rule iffI)
 apply (case_tac a, rename_tac a')
  apply (case_tac n, rename_tac n')
   apply (rule_tac x="hd a'" in exI)
   apply (rule_tac x="FL (tl a')" in exI)
   apply (simp add: eSuc_enat)
   apply (subgoal_tac "a' ≠ []")
    prefer 2
    apply (rule ccontr, simp)
   apply simp
  apply simp
 apply (rename_tac f)
 apply (case_tac n, simp add: eSuc_enat)
 apply (rule_tac x="f 0" in exI)
 apply (rule_tac x="IL (f ⇑ Suc 0)" in exI)
 apply (simp add: i_take_first[symmetric])
apply (clarsimp, rename_tac x b)
apply (case_tac a)
 apply (case_tac b)
  apply (simp add: eSuc_enat)+
apply (case_tac b)
apply (simp add: eSuc_enat)+
done

lemma gSuc_glength_conv: "
  (eSuc n = glength a) =
  (∃x b. a = x #⇩g b ∧ glength b = n)"
by (simp add: eq_commute[of _ "glength a"] glength_gSuc_conv)



subsubsection ‹‹@›\ensuremath{{}_g} -- gappend›

lemma gappend_Nil[simp]: "(FL []) @⇩g a = a"
by (unfold gappend_def, case_tac a, simp+)

lemma gappend_Nil2[simp]: "a @⇩g (FL [])= a"
by (unfold gappend_def, case_tac a, simp+)

lemma gappend_is_Nil_conv[simp]: "(a @⇩g b = FL []) = (a = FL [] ∧ b = FL [])"
by (unfold gappend_def, case_tac a, case_tac b, simp+)

lemma Nil_is_gappend_conv[simp]: "(FL [] = a @⇩g b) = (a = FL [] ∧ b = FL [])"
by (simp add: eq_commute[of "FL []"])

lemma gappend_assoc[simp]: "(a @⇩g b) @⇩g c = a @⇩g b @⇩g c"
by (unfold gappend_def, case_tac a, case_tac b, case_tac c, simp+)

lemma gappend_infin[simp]: "IL f @⇩g b = IL f"
by (simp add: gappend_def)

lemma same_gappend_eq_disj[simp]: "(a @⇩g b = a @⇩g c) = (glength a = ∞ ∨ b = c)"
apply (case_tac a)
 apply simp
 apply (case_tac b, case_tac c)
 apply (simp add: gappend_def)+
 apply (case_tac c)
 apply simp+
done
lemma same_gappend_eq: "
  glength a < ∞ ⟹ (a @⇩g b = a @⇩g c) = (b = c)"
by fastforce


subsubsection ‹‹gmap››

lemma gmap_gappend[simp]: "gmap f (a @⇩g b) = gmap f a @⇩g gmap f b"
by (unfold gappend_def, induct a, induct b, simp+)

lemmas gmap_gmap[simp] = glist.map_comp

lemma gmap_eq_conv[simp]: "(gmap f a = gmap g a) = (∀x∈gset a. f x = g x)"
apply (case_tac a)
apply (simp add: o_eq_conv)+
done

lemmas gmap_cong = glist.map_cong

lemma gmap_is_Nil_conv: "(gmap f a = FL []) = (a = FL [])"
by (simp add: glength_0_conv[symmetric])

lemma gmap_eq_imp_glength_eq: "
  gmap f a = gmap f b ⟹ glength a = glength b"
by (drule arg_cong[where f=glength], simp)


subsubsection ‹‹gset››

lemma gset_gappend[simp]: "
  gset (a @⇩g b) =
  (case a of FL a' ⇒ set a' ∪ gset b | IL a'  ⇒ range a')"
by (unfold gappend_def, case_tac a, case_tac b, simp+)

lemma gset_gappend_if: "
  gset (a @⇩g b) =
  (if glength a < ∞ then gset a ∪ gset b else gset a)"
by (unfold gappend_def, case_tac a, case_tac b, simp+)

lemma gset_empty[simp]: "(gset a = {}) = (a = FL [])"
by (case_tac a, simp+)

lemmas gset_gmap[simp] = glist.set_map

lemma icard_glength: "icard (gset a) ≤ glength a"
apply (unfold icard_def glength_def)
apply (case_tac a)
apply (simp add: card_length)+
done


subsubsection ‹‹!›\ensuremath{{}_g} -- gnth›

lemma gnth_gCons_0[simp]: "(x #⇩g a) !⇩g 0 = x"
by (unfold gCons_def gnth_def, case_tac a, simp+)

lemma gnth_gCons_Suc[simp]: "(x #⇩g a) !⇩g Suc n = a !⇩g n"
by (unfold gCons_def gnth_def, case_tac a, simp+)

lemma gnth_gappend: "
  (a @⇩g b) !⇩g n =
  (if enat n < glength a then a !⇩g n
  else b !⇩g (n - the_enat (glength a)))"
apply (unfold glength_def gappend_def gCons_def gnth_def)
apply (case_tac a, case_tac b)
apply (simp add: nth_append)+
done

lemma gnth_gappend_length_plus[simp]: "(FL xs @⇩g b) !⇩g (length xs + n) = b !⇩g n"
by (simp add: gnth_gappend)

lemma gmap_gnth[simp]: "enat n < glength a ⟹ gmap f a !⇩g n = f (a !⇩g n)"
by (unfold gnth_def, case_tac a, simp+)

lemma in_gset_cong_gnth: "(x ∈ gset a) = (∃i. enat i < glength a ∧ a !⇩g i = x)"
apply (unfold gnth_def, case_tac a)
apply (fastforce simp: in_set_conv_nth)+
done


subsubsection ‹‹gtake› and ‹gdrop››

lemma gtake_0[simp]: "a ↓⇩g 0 = FL []"
by (unfold gtake_def, case_tac a, simp+)

lemma gdrop_0[simp]: "a ↑⇩g 0 = a"
by (unfold gdrop_def, case_tac a, simp+)

lemma gtake_Infty[simp]: "a ↓⇩g ∞ = a"
by (unfold gtake_def, case_tac a, simp+)

lemma gdrop_Infty[simp]: "a ↑⇩g ∞ = FL []"
by (unfold gdrop_def, case_tac a, simp+)

lemma gtake_all[simp]: "glength a ≤ n ⟹ a ↓⇩g n = a"
by (unfold gtake_def, case_tac a, case_tac n, simp+)

lemma gdrop_all[simp]: "glength a ≤ n ⟹ a ↑⇩g n = FL []"
by (unfold gdrop_def, case_tac a, case_tac n, simp+)

lemma gtake_eSuc_gCons[simp]: "(x #⇩g a) ↓⇩g (eSuc n) = x #⇩g a ↓⇩g n"
by (unfold gtake_def gCons_def, case_tac n, case_tac a, simp_all add: eSuc_enat)

lemma gdrop_eSuc_gCons[simp]: "(x #⇩g a) ↑⇩g (eSuc n) = a ↑⇩g n"
by (unfold gdrop_def gCons_def, case_tac n, case_tac a, simp_all add: eSuc_enat)

lemma gtake_eSuc: "a ≠ FL [] ⟹ a ↓⇩g (eSuc n) = a !⇩g 0 #⇩g (a ↑⇩g (eSuc 0) ↓⇩g n)"
apply (unfold gtake_def gdrop_def gnth_def gCons_def)
apply (case_tac n)
 apply (case_tac a)
 apply (simp add: eSuc_enat take_Suc hd_eq_first take_drop i_take_Suc)+
apply (case_tac a)
apply (simp add: hd_eq_first drop_eq_tl i_drop_Suc_conv_tl)+
done

lemma gdrop_eSuc: "a ↑⇩g (eSuc n) = a ↑⇩g (eSuc 0) ↑⇩g n"
by (unfold gtake_def gdrop_def gnth_def gCons_def, case_tac n, case_tac a, simp_all add: eSuc_enat)

lemma gnth_via_grop: "a ↑⇩g (enat n) = x #⇩g b ⟹ a !⇩g n = x"
apply (unfold gdrop_def gnth_def gCons_def)
apply (case_tac a, case_tac b)
apply (simp add: nth_via_drop)+
apply (case_tac b)
apply (fastforce intro: nth_via_i_drop)+
done

lemma gtake_eSuc_conv_gapp_gnth: "
  enat n < glength a ⟹ a ↓⇩g enat (Suc n) = a ↓⇩g (enat n) @⇩g FL [a !⇩g n]"
apply (unfold glength_def gtake_def gappend_def gnth_def)
apply (case_tac a)
apply (simp add: take_Suc_conv_app_nth i_take_Suc_conv_app_nth)+
done

lemma gdrop_eSuc_conv_tl: "
  enat n < glength a ⟹ a !⇩g n #⇩g a ↑⇩g enat (Suc n) = a ↑⇩g enat n"
apply (unfold glength_def gdrop_def gappend_def gnth_def gCons_def)
apply (case_tac a)
apply (simp add: Cons_nth_drop_Suc i_drop_Suc_conv_tl)+
done

lemma glength_gtake[simp]: "glength (a ↓⇩g n) = min (glength a) n"
by (unfold glength_def gtake_def, case_tac n, case_tac a, simp+)

lemma glength_drop[simp]: "glength (a ↑⇩g (enat n)) = glength a - (enat n)"
by (unfold glength_def gdrop_def, case_tac a, case_tac n, simp+)

end