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  (tT. P t s)"
proof -
  define crit where "crit = (λU s. s  S  (uU. ¬ P u s))"
  have critD: "s  U" if "crit U s" for U s
  proof
    assume "s  U"
    from crit U s have "uU. ¬ 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 "useq 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 "tseq i. P t s"
    proof (rule ccontr, simp)
      assume "tseq 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 *: "yset 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 "zset 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 "zset 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) = (xset 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)) = (xset 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) = (aA. 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) = (aA. 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)) = (xxs. 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) = (aA. 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 *)