Theory List_local

(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory List_local
imports Extra "HOL-Library.While_Combinator"
begin


text‹Partition a list with respect to an equivalence relation.›

text‹First up: split a list according to a relation.›

abbreviation "rel_ext r ≡ { x . r x }"

definition
  partition_split_body :: "('a × 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a list × 'a list ⇒ 'a list × 'a list"
where
  [code]: "partition_split_body r x ≡ λy (X', xc).
            if r (x, y) then (X', List.insert y xc) else (List.insert y X', xc)"

definition
  partition_split :: "('a × 'a ⇒ bool) ⇒ 'a ⇒ 'a list ⇒ 'a list × 'a list"
where
  [code]: "partition_split r x xs ≡ foldr (partition_split_body r x) xs ([], [])"

lemma partition_split:
  shows "set (fst (partition_split r x xs)) = set xs - (rel_ext r `` {x})"
    and "set (snd (partition_split r x xs)) = set xs ∩ (rel_ext r `` {x})"
proof(induct xs)
  case Nil
  { case 1 with Nil show ?case
      unfolding partition_split_def by simp }
  { case 2 with Nil show ?case
      unfolding partition_split_def by simp }
next
  case (Cons x xs)
  { case 1 with Cons show ?case
      unfolding partition_split_def
      apply simp
      apply (subst partition_split_body_def)
      apply (split prod.split)
      apply clarsimp
      apply rule
       apply clarsimp
      apply clarsimp
      unfolding Image_def
      apply auto
      done }
  { case 2 with Cons show ?case
      unfolding partition_split_def
      apply simp
      apply (subst partition_split_body_def)
      apply (split prod.split)
      apply clarsimp
      apply rule
       apply clarsimp
      apply clarsimp
      done }
qed

lemma partition_split':
  assumes "partition_split r x xs = (xxs', xec)"
  shows "set xxs' = set xs - (rel_ext r `` {x})"
    and "set xec = set xs ∩ (rel_ext r `` {x})"
  using assms partition_split[where r=r and x=x and xs=xs]
  by simp_all

text‹Next, split an list on each of its members. For this to be
unambiguous @{term "r"} must be an equivalence relation.›

definition
  partition_aux_body :: "('a × 'a ⇒ bool) ⇒ 'a list × 'a list list ⇒ 'a list × 'a list list"
where
  "partition_aux_body ≡ λr (xxs, ecs). case xxs of [] ⇒ ([], []) | x # xs ⇒
                           let (xxs', xec) = partition_split r x xs
                            in (xxs', (x # xec) # ecs)"

definition
  partition_aux :: "('a × 'a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list list"
where
  [code]: "partition_aux r xs ≡
             while (Not ∘ List.null ∘ fst) (partition_aux_body r) (xs, [])"

(* FIXME move these. *)

lemma equiv_subseteq_in_sym:
  "⟦ r `` X ⊆ X;  (x, y) ∈ r; y ∈ X; equiv Y r; X ⊆ Y ⟧ ⟹ x ∈ X"
  unfolding equiv_def by (auto dest: symD)

lemma FIXME_refl_on_insert_absorb[simp]:
  "⟦ refl_on A r; x ∈ A ⟧ ⟹ insert x (r `` {x}) = r `` {x}"
  by (auto dest: refl_onD)

lemma equiv_subset[intro]:
  "⟦ equiv A r; B ⊆ A ⟧ ⟹ equiv B (r ∩ B × B)"
  unfolding equiv_def by (auto intro: refl_onI symI transI dest: refl_onD symD transD)

lemma FIXME_fiddle1: "⟦ x ∈ Y; X ⊆ Y; refl_on Y r ⟧ ⟹ insert x (X ∩ r `` {x}) = (insert x X) ∩ r `` {x}"
  by (auto dest: refl_onD)

lemma FIXME_second_fiddle:
  "⟦ (r ∩ Y × Y) `` X ⊆ X; refl_on Z r; x ∈ X; X ⊆ Y; Y ⊆ Z ⟧
     ⟹ (r ∩ (Y - (X - r `` {x})) × (Y - (X - r `` {x}))) `` {x}
       = (r ∩ X × X) `` {x}"
  by (blast dest: refl_onD)

lemma FIXME_third_fiddle:
  "⟦ (r ∩ Y × Y) `` X ⊆ X; X ⊆ Y; x ∈ X; y ∈ Y - X    ;    r `` {y} ∩ X = {} ⟧
     ⟹ (r ∩ (Y - (X - r `` {x})) × (Y - (X - r `` {x}))) `` {y}
       = (r ∩ (Y - X) × (Y - X)) `` {y}"
  by auto

lemma partition_aux:
  assumes equiv: "equiv X (rel_ext r)"
      and XZ: "set xs ⊆ X"
  shows "fst (partition_aux r xs) = []
       ∧ set ` set (snd (partition_aux r xs))
       = (set xs // (rel_ext r ∩ set xs × set xs))"
proof -
  let ?b = "Not ∘ List.null ∘ fst"
  let ?c = "partition_aux_body r"
  let ?r' = "λA. rel_ext r ∩ A × A"
  let ?P1 = "λ(A, B). set A ⊆ set xs"
  let ?P2 = "λ(A, B). ?r' (set xs) `` set A ⊆ set A"
  let ?P3 = "λ(A, B). set ` set B = ((set xs - set A) // ?r' (set xs - set A))"
  let ?P = "λAB. ?P1 AB ∧ ?P2 AB ∧ ?P3 AB"
  let ?wfr = "inv_image finite_psubset (set ∘ fst)"
  show ?thesis
  unfolding partition_aux_def
  proof(rule while_rule[where P="?P" and r="?wfr"])
    from equiv XZ show "?P (xs, [])" by auto
  next
    fix s assume P: "?P s" and b: "?b s"

    obtain A B where s: "s = (A, B)" by (cases s) blast

    moreover
    from XZ P s have "?P1 (?c (A, B))"
      unfolding partition_aux_body_def
      by (auto simp add: partition_split' split: list.split prod.split)

    moreover
    from equiv XZ P s have "?P2 (?c s)"
      apply (cases A)
      unfolding partition_aux_body_def
      apply simp_all
      subgoal for a as
        apply (cases "partition_split r a as")
        apply (simp add: partition_split')
        unfolding equiv_def
        apply (auto dest: symD transD elim: quotientE)
        done
      done

    moreover
    have "?P3 (?c s)"
    proof -
      from b s obtain x where x: "x ∈ set A" by (cases A) (auto iff: null_def)
      with XZ equiv P b s x
      show ?thesis
      
        unfolding partition_aux_body_def
        apply clarsimp
        apply (erule equivE)
        apply (cases A)
         apply simp
        apply simp
        apply (case_tac "partition_split r a list")
        apply clarsimp
        apply (simp add: partition_split')

        apply (subst FIXME_fiddle1[where Y=X])
           apply blast
          apply auto[1]
         apply blast

        apply rule
         apply clarsimp
         apply rule
          apply (rule_tac x=a in quotientI2)
           apply (blast dest: refl_onD)
          using XZ
          apply (auto dest: refl_onD)[1]
         apply clarsimp
         apply (erule quotientE)
         apply clarsimp
         apply (rule_tac x=xa in quotientI2)
          apply (blast dest: refl_onD)
         apply rule
          apply clarsimp
         apply clarsimp
         apply rule
          apply rule
          apply clarsimp
          apply (cut_tac X="insert a (set list)" and Y="set xs" and x=xa and y=a and r="rel_ext r ∩ set xs × set xs" in equiv_subseteq_in_sym)
          apply simp_all
          using equiv
          apply blast
         apply clarsimp
         apply (cut_tac X="insert a (set list)" and Y="set xs" and x=xa and y=xb and r="rel_ext r ∩ set xs × set xs" in equiv_subseteq_in_sym)
         apply simp_all
         using equiv
         apply blast

        apply (rule subsetI)
        apply (erule quotientE)
        apply (case_tac "xaa = a")
         apply auto[1]
        apply clarsimp

        apply (case_tac "xa ∈ set list")
         apply clarsimp
         apply rule
          apply (auto dest: transD)[1]
         apply (auto dest: symD transD)[1]

        unfolding quotient_def
        apply clarsimp
        apply (erule_tac x=xa in ballE)
         unfolding Image_def
         apply clarsimp
        apply (auto dest: symD transD)  (* SLOW *)
        done
    qed

    ultimately show "?P (?c s)" by auto
  next
    fix s assume P: "?P s" and b: "¬ (?b s)"
    from b have F: "fst s = []"
      apply (cases s)
      apply simp
      apply (case_tac a)
      apply (simp_all add: List.null_def)
      done
    from equiv P F have S: "set ` set (snd s) = (set xs // ?r' (set xs))"
      apply (cases s)
      unfolding Image_def
      apply simp
      done
    from F S show "fst s = [] ∧ set ` set (snd s) = (set xs // ?r' (set xs))"
      by (simp add: prod_eqI)
  next
    show "wf ?wfr" by (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
  next
    fix s assume P: "?P s" and b: "?b s"
    from equiv XZ P b have "set (fst (?c s)) ⊂ set (fst s)"
      apply -
      apply (cases s)
      apply (simp add: Let_def)
      unfolding partition_aux_body_def
      apply clarsimp
      apply (case_tac a)
       apply (simp add: List.null_def)
      apply simp
      apply (case_tac "partition_split r aa list")
      apply (simp add: partition_split')

      unfolding equiv_def
      apply (auto dest: refl_onD)
      done
    thus "(?c s, s) ∈ ?wfr" by auto
  qed
qed

definition
  partition :: "('a × 'a ⇒ bool) ⇒ 'a list ⇒ 'a list list"
where
  [code]: "partition r xs ≡ snd (partition_aux r xs)"

lemma partition:
  assumes equiv: "equiv X (rel_ext r)"
      and xs: "set xs ⊆ X"
  shows "set ` set (partition r xs) = set xs // ((rel_ext r) ∩ set xs × set xs)"
  unfolding partition_def
  using partition_aux[OF equiv xs] by simp

(* **************************************** *)

fun
  odlist_equal :: "'a list ⇒ 'a list ⇒ bool"
where
  "odlist_equal [] [] = True"
| "odlist_equal [] ys = False"
| "odlist_equal xs [] = False"
| "odlist_equal (x # xs) (y # ys) = (x = y ∧ odlist_equal xs ys)"

declare odlist_equal.simps [code]

lemma equal_odlist_equal[simp]:
  "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧
     ⟹ odlist_equal xs ys ⟷ (xs = ys)"
  by (induct xs ys rule: odlist_equal.induct) (auto)

fun
  difference :: "('a :: linorder) list ⇒ 'a list ⇒ 'a list"
where
  "difference [] ys = []"
| "difference xs [] = xs"
| "difference (x # xs) (y # ys) =
     (if x = y then difference xs ys
               else if x < y then x # difference xs (y # ys)
                             else difference (x # xs) ys)"

declare difference.simps [code]

lemma set_difference[simp]:
  "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧
     ⟹ set (difference xs ys) = set xs - set ys"
  by (induct xs ys rule: difference.induct) (auto)

lemma distinct_sorted_difference[simp]:
  "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧
     ⟹ distinct (difference xs ys) ∧ sorted (difference xs ys)"
  by (induct xs ys rule: difference.induct) (auto)

fun
  intersection :: "('a :: linorder) list ⇒ 'a list ⇒ 'a list"
where
  "intersection [] ys = []"
| "intersection xs [] = []"
| "intersection (x # xs) (y # ys) =
     (if x = y then x # intersection xs ys
               else if x < y then intersection xs (y # ys)
                             else intersection (x # xs) ys)"

declare intersection.simps [code]

lemma set_intersection[simp]:
  "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧
     ⟹ set (intersection xs ys) = set xs ∩ set ys"
  by (induct xs ys rule: intersection.induct) (auto)

lemma distinct_sorted_intersection[simp]:
  "⟦ distinct xs; distinct ys; sorted xs; sorted ys ⟧
     ⟹ distinct (intersection xs ys) ∧ sorted (intersection xs ys)"
  by (induct xs ys rule: intersection.induct) (auto)

(* This is a variant of zipWith *)
fun
  image :: "('a :: linorder × 'b :: linorder) list ⇒ 'a list ⇒ 'b list"
where
  "image [] xs = []"
| "image R []  = []"
| "image ((x, y) # rs) (z # zs) =
     (if x = z then y # image rs (z # zs)
               else if x < z then image rs (z # zs)
                             else image ((x, y) # rs) zs)"

declare image.simps [code]

lemma set_image[simp]:
  "⟦ distinct R; distinct xs; sorted R; sorted xs ⟧
     ⟹ set (image R xs) = set R `` set xs"
  by (induct R xs rule: image.induct) (auto iff: less_eq_prod_def)

(* Extra lemmas that really belong in List.thy *)

lemma sorted_filter[simp]:
  "sorted xs ⟹ sorted (filter P xs)"
  by (induct xs) (auto)

lemma map_prod_eq:
  assumes f: "map fst xs = map fst ys"
      and s: "map snd xs = map snd ys"
  shows "xs = ys"
  using assms by (fact pair_list_eqI)

lemma list_choose_hd:
  assumes "∀x ∈ set xs. P x"
      and "x ∈ set xs"
  shows "P (List.hd xs)"
  using assms by (induct xs arbitrary: x) auto

end