Theory ListPre

(*  Title:      ListPre.thy
    Author:     Ludovic Henrio and Florian Kammuller, 2006

List lemmata and other general stuff as preparation for ASP.
*)

section ‹List features›

theory ListPre
imports Main
begin

lemma drop_lem[rule_format]: 
  fixes n :: nat and l :: "'a list" and g :: "'a list"
  assumes "drop n l = drop n g" and "length l = length g" and "n < length g"
  shows "l!n = g!n"
proof -
  from assms(2-3) have "n < length l" by simp
  from Cons_nth_drop_Suc[OF this] Cons_nth_drop_Suc[OF assms(3)] assms(1) 
  have "l!n # drop (Suc n) l = g!n # drop (Suc n) g" by simp
  thus ?thesis by simp
qed

lemma mem_append_lem': "x ∈ set (l @ [y]) ⟹ x ∈ set l ∨ x = y"
  by auto

lemma nth_last: "length l = n ⟹ (l @ [x])!n = x"
  by auto

lemma take_n:
  fixes n :: nat and l :: "'a list" and g :: "'a list"
  assumes "take n l = take n g" and "Suc n ≤ length g" and "length l = length g"
  shows "take (Suc n) (l[n := g!n]) = take (Suc n) g"
proof -
  from assms(2) have ng: "n < length g" by simp
  with assms(3) have nlupd: "n < length (l[n := g!n])" by simp
  hence nl: "n < length l" by simp
  from 
    sym[OF assms(1)] id_take_nth_drop[OF ng] take_Suc_conv_app_nth[OF nlupd]
    nth_list_update_eq[OF nl] take_Suc_conv_app_nth[OF ng]
    upd_conv_take_nth_drop[OF nl] assms(2-3)
  show ?thesis by simp
qed

lemma drop_n_lem:
  fixes n :: nat and l :: "'a list"
  assumes "Suc n ≤ length l"
  shows "drop (Suc n) (l[n := x]) = drop (Suc n) l"
  using assms by simp

lemma drop_n: 
  fixes n :: nat and l :: "'a list" and g :: "'a list"
  assumes "drop n l = drop n g" and "Suc n ≤ length g" and "length l = length g"
  shows "drop (Suc n) (l[n := g!n]) = drop (Suc n) g"
proof -
  from assms(2-3) have "Suc n ≤ length l" by simp
  from drop_n_lem[OF this] assms(1) show ?thesis
    by (simp, (subst drop_Suc)+, (subst drop_tl)+, simp)
qed

lemma nth_fst[rule_format]: "length l = n + 1 ⟶ (l @ [x])!0 = l!0" 
  by (induct l, simp_all)

lemma nth_zero_app: 
  fixes l :: "'a list" and x :: 'a and y :: 'a
  assumes "l ≠ []" and "l!0 = x"
  shows"(l @ [y])!0 = x"
proof -
  have "l ≠ [] ∧ l!0 = x ⟶ (l @ [y])!0 = x"
    by (induct l, simp_all)
  with assms show ?thesis by simp
qed

lemma rev_induct2[consumes 1]:
  fixes xs :: "'a list" and ys :: "'a list" and P :: "'a list ⇒ 'a list ⇒ bool"
  assumes 
  "length xs = length ys" and "P [] []" and
  "⋀x xs y ys. ⟦ length xs = length ys; P xs ys ⟧ ⟹ P (xs @ [x]) (ys @ [y])"
  shows "P xs ys"
proof (simplesubst rev_rev_ident[symmetric])
  from assms(1) have lrev: "length (rev xs) = length (rev ys)" by simp
  from assms have "P (rev (rev xs))(rev (rev ys))" 
    by (induct rule: list_induct2[OF lrev], simp_all)
  thus "P xs (rev (rev ys))" by simp
qed

lemma list_induct3: (* Similar to induction for 2: see ML "thm \"list_induct2\""; *)
  "⋀ys zs. ⟦ length xs = length ys; length zs = length xs; P [] [] [];
              ⋀x xs y ys z zs. ⟦ length xs = length ys; 
                                    length zs = length xs; P xs ys zs ⟧
                                 ⟹ P (x # xs)(y # ys)(z # zs) 
  ⟧ ⟹ P xs ys zs"
proof (induct xs, simp)
  case (Cons a xs ys zs) 
  from ‹length (a#xs) = length ys› ‹length zs = length (a#xs)› 
  have "ys ≠ [] ∧ zs ≠ []" by auto
  then obtain b ly c lz where "ys = b#ly" and "zs = c#lz"
    by (auto simp: neq_Nil_conv)
  with ‹length (a#xs) = length ys› ‹length zs = length (a#xs)› 
  obtain "length xs = length ly" and "length lz = length xs" 
    by auto
  from 
    Cons(5)[OF this Cons(1)[OF this ‹P [] [] []›]] 
    Cons(5) ‹ys = b#ly› ‹zs = c#lz› 
  show ?case by simp
qed

primrec list_insert :: "'a list ⇒ nat ⇒ 'a ⇒ 'a list" where
  "list_insert (ah#as) i a = 
  (case i of 
        0      ⇒ a#ah#as
       |Suc j  ⇒ ah#(list_insert as j a))" |

  "list_insert [] i a = [a]"

lemma insert_eq[simp]: "∀i≤length l. (list_insert l i a)!i = a"
  by (induct l, simp, intro strip, simp split: nat.split)

lemma insert_gt[simp]: "∀i≤length l. ∀j<i. (list_insert  l i a)!j = l!j"
proof (induct l, simp)
  case (Cons x l) thus ?case
  proof (auto split: nat.split)
    fix n j assume "n ≤ length l" and "j < Suc n"
    with Cons(1) show "(x#(list_insert l n a))!j = (x#l)!j"
      by (cases j) simp_all
  qed
qed

lemma insert_lt[simp]: "∀j≤length l. ∀i≤j. (list_insert l i a)!Suc j = l!j"
proof (induct l, simp)
  case (Cons x l) thus ?case
  proof (auto split: nat.split)
    fix n j assume "j ≤ Suc (length l)" and "Suc n ≤ j" 
    with Cons(1) show "(list_insert l n a)!j = l!(j - Suc 0)"
      by (cases j) simp_all
  qed
qed

lemma insert_first[simp]: "list_insert l 0 b = b#l"
  by (induct l, simp_all)

lemma insert_prepend[simp]: 
  "i = Suc j ⟹ list_insert (a#l) i b = a # list_insert l j b"
  by auto

lemma insert_lt2[simp]: "∀j. ∀i≤j. (list_insert  l i a)!Suc j = l!j"
proof (induct l, simp)
  case (Cons x l) thus ?case
  proof (auto split: nat.split)
    fix n j assume "Suc n ≤ j" 
    with Cons(1) show "(list_insert l n a)!j = l!(j - Suc 0)"
      by (cases j) simp_all
  qed
qed

lemma insert_commute[simp]: 
  "∀i≤length l. (list_insert (list_insert l i b) 0 a) =
                 (list_insert (list_insert l 0 a ) (Suc i) b)"
  by (induct l, auto split: nat.split)

lemma insert_length': "⋀i x. length (list_insert l i x) = length (x#l)"
  by (induct l, auto split: nat.split)

lemma insert_length[simp]: "length (list_insert l i b) = length (list_insert l j c)"
  by (simp add: insert_length')

lemma insert_select[simp]: "the ((f(l ↦ t)) l) = t"
  by auto

lemma dom_insert[simp]: "l ∈ dom f ⟹ dom (f(l ↦ t)) = dom f"
  by auto

lemma insert_select2[simp]: "l1 ≠ l2 ⟹ ((f(l1 ↦ t)) l2) = (f l2)"
  by auto

lemma the_insert_select[simp]: 
  "⟦ l2 ∈ dom f; l1 ≠ l2 ⟧ ⟹  the ((f(l1 ↦ t)) l2) =  the (f l2)"
  by auto

lemma insert_dom_eq: "dom f = dom f' ⟹ dom (f(l ↦ x)) = dom (f'(l ↦ x'))"
  by auto

lemma insert_dom_less_eq: 
  "⟦ x ∉ dom f; x ∉ dom f'; dom (f(x ↦ y)) = dom (f'(x ↦ y')) ⟧ 
  ⟹ dom f = dom f'"
  by auto

lemma one_more_dom[rule_format]: 
  "∀l∈dom f . ∃f'. f = f'(l ↦ the(f l)) ∧ l ∉ dom f'"
proof
  fix l assume "l ∈ dom f"
  hence "⋀la. f la = ((λla. if la = l then None else f la)(l ↦ the (f l))) la"
    by auto
  hence "f = (λla. if la = l then None else f la)(l ↦ the (f l))"
    by (rule ext)
  thus "∃f'. f = f'(l ↦ the(f l) ) ∧ l ∉ dom f'" by auto
qed
 
end