Theory Utils

(* Author: Alexander Maletzky *)

section ‹Utilities›

theory Utils
  imports Main Well_Quasi_Orders.Almost_Full_Relations
begin

lemma subset_imageE_inj:
  assumes "B ⊆ f ` A"
  obtains C where "C ⊆ A" and "B = f ` C" and "inj_on f C"
proof -
  define g where "g = (λx. SOME a. a ∈ A ∧ f a = x)"
  have "g b ∈ A ∧ f (g b) = b" if "b ∈ B" for b
  proof -
    from that assms have "b ∈ f ` A" ..
    then obtain a where "a ∈ A" and "b = f a" ..
    hence "a ∈ A ∧ f a = b" by simp
    thus ?thesis unfolding g_def by (rule someI)
  qed
  hence 1: "⋀b. b ∈ B ⟹ g b ∈ A" and 2: "⋀b. b ∈ B ⟹ f (g b) = b" by simp_all
  let ?C = "g ` B"
  show ?thesis
  proof
    show "?C ⊆ A" by (auto intro: 1)
  next
    show "B = f ` ?C"
    proof (rule set_eqI)
      fix b
      show "b ∈ B ⟷ b ∈ f ` ?C"
      proof
        assume "b ∈ B"
        moreover from this have "f (g b) = b" by (rule 2)
        ultimately show "b ∈ f ` ?C" by force
      next
        assume "b ∈ f ` ?C"
        then obtain b' where "b' ∈ B" and "b = f (g b')" unfolding image_image ..
        moreover from this(1) have "f (g b') = b'" by (rule 2)
        ultimately show "b ∈ B" by simp
      qed
    qed
  next
    show "inj_on f ?C"
    proof
      fix x y
      assume "x ∈ ?C"
      then obtain bx where "bx ∈ B" and x: "x = g bx" ..
      moreover from this(1) have "f (g bx) = bx" by (rule 2)
      ultimately have *: "f x = bx" by simp
      assume "y ∈ ?C"
      then obtain "by" where "by ∈ B" and y: "y = g by" ..
      moreover from this(1) have "f (g by) = by" by (rule 2)
      ultimately have "f y = by" by simp
      moreover assume "f x = f y"
      ultimately have "bx = by" using * by simp
      thus "x = y" by (simp only: x y)
    qed
  qed
qed

lemma wfP_chain:
  assumes "¬(∃f. ∀i. r (f (Suc i)) (f i))"
  shows "wfP r"
proof -
  from assms wf_iff_no_infinite_down_chain[of "{(x, y). r x y}"] have "wf {(x, y). r x y}" by auto
  thus "wfP r" unfolding wfp_def .
qed

lemma transp_sequence:
  assumes "transp r" and "⋀i. r (seq (Suc i)) (seq i)" and "i < j"
  shows "r (seq j) (seq i)"
proof -
  have "⋀k. r (seq (i + Suc k)) (seq i)"
  proof -
    fix k::nat
    show "r (seq (i + Suc k)) (seq i)"
    proof (induct k)
      case 0
      from assms(2) have "r (seq (Suc i)) (seq i)" .
      thus ?case by simp
    next
      case (Suc k)
      note assms(1)
      moreover from assms(2) have "r (seq (Suc (Suc i + k))) (seq (Suc (i + k)))" by simp
      moreover have "r (seq (Suc (i + k))) (seq i)" using Suc.hyps by simp
      ultimately have "r (seq (Suc (Suc i + k))) (seq i)" by (rule transpD)
      thus ?case by simp
    qed
  qed
  hence "r (seq (i + Suc(j - i - 1))) (seq i)" .
  thus "r (seq j) (seq i)" using ‹i < j› by simp
qed

lemma almost_full_on_finite_subsetE:
  assumes "reflp P" and "almost_full_on P S"
  obtains T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. P t s)"
proof -
  define crit where "crit = (λU s. s ∈ S ∧ (∀u∈U. ¬ P u s))"
  have critD: "s ∉ U" if "crit U s" for U s
  proof
    assume "s ∈ U"
    from ‹crit U s› have "∀u∈U. ¬ P u s" unfolding crit_def ..
    from this ‹s ∈ U› have "¬ P s s" ..
    moreover from assms(1) have "P s s" by (rule reflpD)
    ultimately show False ..
  qed
  define "fun"
    where "fun = (λU. (if (∃s. crit U s) then
                        insert (SOME s. crit U s) U
                      else
                        U
                      ))"
  define seq where "seq = rec_nat {} (λ_. fun)"
  have seq_Suc: "seq (Suc i) = fun (seq i)" for i by (simp add: seq_def)
  
  have seq_incr_Suc: "seq i ⊆ seq (Suc i)" for i by (auto simp add: seq_Suc fun_def)
  have seq_incr: "i ≤ j ⟹ seq i ⊆ seq j" for i j
  proof -
    assume "i ≤ j"
    hence "i = j ∨ i < j" by auto
    thus "seq i ⊆ seq j"
    proof
      assume "i = j"
      thus ?thesis by simp
    next
      assume "i < j"
      with _ seq_incr_Suc show ?thesis by (rule transp_sequence, simp add: transp_def)
    qed
  qed
  have sub: "seq i ⊆ S" for i
  proof (induct i, simp add: seq_def, simp add: seq_Suc fun_def, rule)
    fix i
    assume "Ex (crit (seq i))"
    hence "crit (seq i) (Eps (crit (seq i)))" by (rule someI_ex)
    thus "Eps (crit (seq i)) ∈ S" by (simp add: crit_def)
  qed
  have "∃i. seq (Suc i) = seq i"
  proof (rule ccontr, simp)
    assume "∀i. seq (Suc i) ≠ seq i"
    with seq_incr_Suc have "seq i ⊂ seq (Suc i)" for i by blast
    define seq1 where "seq1 = (λn. (SOME s. s ∈ seq (Suc n) ∧ s ∉ seq n))"
    have seq1: "seq1 n ∈ seq (Suc n) ∧ seq1 n ∉ seq n" for n unfolding seq1_def
    proof (rule someI_ex)
      from ‹seq n ⊂ seq (Suc n)› show "∃x. x ∈ seq (Suc n) ∧ x ∉ seq n" by blast
    qed
    have "seq1 i ∈ S" for i
    proof
      from seq1[of i] show "seq1 i ∈ seq (Suc i)" ..
    qed (fact sub)
    with assms(2) obtain a b where "a < b" and "P (seq1 a) (seq1 b)" by (rule almost_full_onD)
    from ‹a < b› have "Suc a ≤ b" by simp
    from seq1 have "seq1 a ∈ seq (Suc a)" ..
    also from ‹Suc a ≤ b› have "... ⊆ seq b" by (rule seq_incr)
    finally have "seq1 a ∈ seq b" .
    from seq1 have "seq1 b ∈ seq (Suc b)" and "seq1 b ∉ seq b" by blast+
    hence "crit (seq b) (seq1 b)" by (simp add: seq_Suc fun_def someI split: if_splits)
    hence "∀u∈seq b. ¬ P u (seq1 b)" by (simp add: crit_def)
    from this ‹seq1 a ∈ seq b› have "¬ P (seq1 a) (seq1 b)" ..
    from this ‹P (seq1 a) (seq1 b)› show False ..
  qed
  then obtain i where "seq (Suc i) = seq i" ..
  show ?thesis
  proof
    show "finite (seq i)" by (induct i, simp_all add: seq_def fun_def)
  next
    fix s
    assume "s ∈ S"
    let ?s = "Eps (crit (seq i))"
    show "∃t∈seq i. P t s"
    proof (rule ccontr, simp)
      assume "∀t∈seq i. ¬ P t s"
      with ‹s ∈ S› have "crit (seq i) s" by (simp only: crit_def)
      hence "crit (seq i) ?s" and eq: "seq (Suc i) = insert ?s (seq i)"
        by (auto simp add: seq_Suc fun_def intro: someI)
      from this(1) have "?s ∉ seq i" by (rule critD)
      hence "seq (Suc i) ≠ seq i" unfolding eq by blast
      from this ‹seq (Suc i) = seq i› show False ..
    qed
  qed (fact sub)
qed

subsection ‹Lists›

lemma map_upt: "map (λi. f (xs ! i)) [0..<length xs] = map f xs"
  by (auto intro: nth_equalityI)

lemma map_upt_zip:
  assumes "length xs = length ys"
  shows "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] = map (λ(x, y). f x y) (zip xs ys)" (is "?l = ?r")
proof -
  have len_l: "length ?l = length ys" by simp
  from assms have len_r: "length ?r = length ys" by simp
  show ?thesis
  proof (simp only: list_eq_iff_nth_eq len_l len_r, rule, rule, intro allI impI)
    fix i
    assume "i < length ys"
    hence "i < length ?l" and "i < length ?r" by (simp_all only: len_l len_r)
    thus "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] ! i = map (λ(x, y). f x y) (zip xs ys) ! i"
      by simp
  qed
qed

lemma distinct_sorted_wrt_irrefl:
  assumes "irreflp rel" and "transp rel" and "sorted_wrt rel xs"
  shows "distinct xs"
  using assms(3)
proof (induct xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  from Cons(2) have "sorted_wrt rel xs" and *: "∀y∈set xs. rel x y"
    by (simp_all)
  from this(1) have "distinct xs" by (rule Cons(1))
  show ?case
  proof (simp add: ‹distinct xs›, rule)
    assume "x ∈ set xs"
    with * have "rel x x" ..
    with assms(1) show False by (simp add: irreflp_def)
  qed
qed

lemma distinct_sorted_wrt_imp_sorted_wrt_strict:
  assumes "distinct xs" and "sorted_wrt rel xs"
  shows "sorted_wrt (λx y. rel x y ∧ ¬ x = y) xs"
  using assms
proof (induct xs)
  case Nil
  show ?case by simp
next
  case step: (Cons x xs)
  show ?case
  proof (cases "xs")
    case Nil
    thus ?thesis by simp
  next
    case (Cons y zs)
    from step(2) have "x ≠ y" and 1: "distinct (y # zs)" by (simp_all add: Cons)
    from step(3) have "rel x y" and 2: "sorted_wrt rel (y # zs)" by (simp_all add: Cons)
    from 1 2 have "sorted_wrt (λx y. rel x y ∧ x ≠ y) (y # zs)" by (rule step(1)[simplified Cons])
    with ‹x ≠ y› ‹rel x y› show ?thesis using step.prems by (auto simp: Cons)
  qed
qed

lemma sorted_wrt_distinct_set_unique:
  assumes "antisymp rel"
  assumes "sorted_wrt rel xs" "distinct xs" "sorted_wrt rel ys" "distinct ys" "set xs = set ys"
  shows "xs = ys"
proof -
  from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  from assms(2-6) show ?thesis
  proof(induct rule:list_induct2[OF 1])
    case 1
    show ?case by simp
  next
    case (2 x xs y ys)
    from 2(4) have "x ∉ set xs" and "distinct xs" by simp_all
    from 2(6) have "y ∉ set ys" and "distinct ys" by simp_all
    have "x = y"
    proof (rule ccontr)
      assume "x ≠ y"
      from 2(3) have "∀z∈set xs. rel x z" by (simp)
      moreover from ‹x ≠ y› have "y ∈ set xs" using 2(7) by auto
      ultimately have *: "rel x y" ..
      from 2(5) have "∀z∈set ys. rel y z" by (simp)
      moreover from ‹x ≠ y› have "x ∈ set ys" using 2(7) by auto
      ultimately have "rel y x" ..
      with assms(1) * have "x = y" by (rule antisympD)
      with ‹x ≠ y› show False ..
    qed
    from 2(3) have "sorted_wrt rel xs" by (simp)
    moreover note ‹distinct xs›
    moreover from 2(5) have "sorted_wrt rel ys" by (simp)
    moreover note ‹distinct ys›
    moreover from 2(7) ‹x ∉ set xs› ‹y ∉ set ys› have "set xs = set ys" by (auto simp add: ‹x = y›)
    ultimately have "xs = ys" by (rule 2(2))
    with ‹x = y› show ?case by simp
  qed
qed

lemma sorted_wrt_refl_nth_mono:
  assumes "reflp P" and "sorted_wrt P xs" and "i ≤ j" and "j < length xs"
  shows "P (xs ! i) (xs ! j)"
proof (cases "i < j")
  case True
  from assms(2) this assms(4) show ?thesis by (rule sorted_wrt_nth_less)
next
  case False
  with assms(3) have "i = j" by simp
  from assms(1) show ?thesis unfolding ‹i = j› by (rule reflpD)
qed

fun merge_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
  "merge_wrt _ xs [] = xs"|
  "merge_wrt rel [] ys = ys"|
  "merge_wrt rel (x # xs) (y # ys) =
    (if x = y then
      y # (merge_wrt rel xs ys)
    else if rel x y then
      x # (merge_wrt rel xs (y # ys))
    else
      y # (merge_wrt rel (x # xs) ys)
    )"

lemma set_merge_wrt: "set (merge_wrt rel xs ys) = set xs ∪ set ys"
proof (induct rel xs ys rule: merge_wrt.induct)
  case (1 rel xs)
  show ?case by simp
next
  case (2 rel y ys)
  show ?case by simp
next
  case (3 rel x xs y ys)
  show ?case
  proof (cases "x = y")
    case True
    thus ?thesis by (simp add: 3(1))
  next
    case False
    show ?thesis
    proof (cases "rel x y")
      case True
      with ‹x ≠ y› show ?thesis by (simp add: 3(2) insert_commute)
    next
      case False
      with ‹x ≠ y› show ?thesis by (simp add: 3(3))
    qed
  qed
qed

lemma sorted_merge_wrt:
  assumes "transp rel" and "⋀x y. x ≠ y ⟹ rel x y ∨ rel y x"
    and "sorted_wrt rel xs" and "sorted_wrt rel ys"
  shows "sorted_wrt rel (merge_wrt rel xs ys)"
  using assms
proof (induct rel xs ys rule: merge_wrt.induct)
  case (1 rel xs)
  from 1(3) show ?case by simp
next
  case (2 rel y ys)
  from 2(4) show ?case by simp
next
  case (3 rel x xs y ys)
  show ?case
  proof (cases "x = y")
    case True
    show ?thesis
    proof (auto simp add: True)
      fix z
      assume "z ∈ set (merge_wrt rel xs ys)"
      hence "z ∈ set xs ∪ set ys" by (simp only: set_merge_wrt)
      thus "rel y z"
      proof
        assume "z ∈ set xs"
        with 3(6) show ?thesis by (simp add: True)
      next
        assume "z ∈ set ys"
        with 3(7) show ?thesis by (simp)
      qed
    next
      note True 3(4, 5)
      moreover from 3(6) have "sorted_wrt rel xs" by (simp)
      moreover from 3(7) have "sorted_wrt rel ys" by (simp)
      ultimately show "sorted_wrt rel (merge_wrt rel xs ys)" by (rule 3(1))
    qed
  next
    case False
    show ?thesis
    proof (cases "rel x y")
      case True
      show ?thesis
      proof (auto simp add: False True)
        fix z
        assume "z ∈ set (merge_wrt rel xs (y # ys))"
        hence "z ∈ insert y (set xs ∪ set ys)" by (simp add: set_merge_wrt)
        thus "rel x z"
        proof
          assume "z = y"
          with True show ?thesis by simp
        next
          assume "z ∈ set xs ∪ set ys"
          thus ?thesis
          proof
            assume "z ∈ set xs"
            with 3(6) show ?thesis by (simp)
          next
            assume "z ∈ set ys"
            with 3(7) have "rel y z" by (simp)
            with 3(4) True show ?thesis by (rule transpD)
          qed
        qed
      next
        note False True 3(4, 5)
        moreover from 3(6) have "sorted_wrt rel xs" by (simp)
        ultimately show "sorted_wrt rel (merge_wrt rel xs (y # ys))" using 3(7) by (rule 3(2))
      qed
    next
      assume "¬ rel x y"
      from ‹x ≠ y› have "rel x y ∨ rel y x" by (rule 3(5))
      with ‹¬ rel x y› have *: "rel y x" by simp
      show ?thesis
      proof (auto simp add: False ‹¬ rel x y›)
        fix z
        assume "z ∈ set (merge_wrt rel (x # xs) ys)"
        hence "z ∈ insert x (set xs ∪ set ys)" by (simp add: set_merge_wrt)
        thus "rel y z"
        proof
          assume "z = x"
          with * show ?thesis by simp
        next
          assume "z ∈ set xs ∪ set ys"
          thus ?thesis
          proof
            assume "z ∈ set xs"
            with 3(6) have "rel x z" by (simp)
            with 3(4) * show ?thesis by (rule transpD)
          next
            assume "z ∈ set ys"
            with 3(7) show ?thesis by (simp)
          qed
        qed
      next
        note False ‹¬ rel x y› 3(4, 5, 6)
        moreover from 3(7) have "sorted_wrt rel ys" by (simp)
        ultimately show "sorted_wrt rel (merge_wrt rel (x # xs) ys)" by (rule 3(3))
      qed
    qed
  qed
qed

lemma set_fold:
  assumes "⋀x ys. set (f (g x) ys) = set (g x) ∪ set ys"
  shows "set (fold (λx. f (g x)) xs ys) = (⋃x∈set xs. set (g x)) ∪ set ys"
proof (induct xs arbitrary: ys)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  have eq: "set (fold (λx. f (g x)) xs (f (g x) ys)) = (⋃x∈set xs. set (g x)) ∪ set (f (g x) ys)"
    by (rule Cons)
  show ?case by (simp add: o_def assms set_merge_wrt eq ac_simps)
qed

subsection ‹Sums and Products›

lemma additive_implies_homogenous:
  assumes "⋀x y. f (x + y) = f x + ((f (y::'a::monoid_add))::'b::cancel_comm_monoid_add)"
  shows "f 0 = 0"
proof -
  have "f (0 + 0) = f 0 + f 0" by (rule assms)
  hence "f 0 = f 0 + f 0" by simp
  thus "f 0 = 0" by simp
qed

lemma fun_sum_commute:
  assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
  shows "f (sum g A) = (∑a∈A. f (g a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    thus ?case by (simp add: assms(1))
  next
    case step: (insert a A)
    show ?case by (simp add: sum.insert[OF step(1) step(2)] assms(2) step(3))
  qed
next
  case False
  thus ?thesis by (simp add: assms(1))
qed

lemma fun_sum_commute_canc:
  assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)"
  shows "f (sum g A) = (∑a∈A. f (g a))"
  by (rule fun_sum_commute, rule additive_implies_homogenous, fact+)

lemma fun_sum_list_commute:
  assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
  shows "f (sum_list xs) = sum_list (map f xs)"
proof (induct xs)
  case Nil
  thus ?case by (simp add: assms(1))
next
  case (Cons x xs)
  thus ?case by (simp add: assms(2))
qed

lemma fun_sum_list_commute_canc:
  assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)"
  shows "f (sum_list xs) = sum_list (map f xs)"
  by (rule fun_sum_list_commute, rule additive_implies_homogenous, fact+)

lemma sum_set_upt_eq_sum_list: "(∑i = m..<n. f i) = (∑i←[m..<n]. f i)"
  using sum_set_upt_conv_sum_list_nat by auto

lemma sum_list_upt: "(∑i←[0..<(length xs)]. f (xs ! i)) = (∑x←xs. f x)"
  by (simp only: map_upt)

lemma sum_list_upt_zip:
  assumes "length xs = length ys"
  shows "(∑i←[0..<(length ys)]. f (xs ! i) (ys ! i)) = (∑(x, y)←(zip xs ys). f x y)"
  by (simp only: map_upt_zip[OF assms])

lemma sum_list_zeroI:
  assumes "set xs ⊆ {0}"
  shows "sum_list xs = 0"
  using assms by (induct xs, auto)

lemma fun_prod_commute:
  assumes "f 1 = 1" and "⋀x y. f (x * y) = f x * f y"
  shows "f (prod g A) = (∏a∈A. f (g a))"
proof (cases "finite A")
  case True
  thus ?thesis
  proof (induct A)
    case empty
    thus ?case by (simp add: assms(1))
  next
    case step: (insert a A)
    show ?case by (simp add: prod.insert[OF step(1) step(2)] assms(2) step(3))
  qed
next
  case False
  thus ?thesis by (simp add: assms(1))
qed

end (* theory *)