Theory Util

theory Util
imports List_Util Archimedean_Field Relative_Rewriting
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2012-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Util
imports
  List_Util
  "~~/src/HOL/Library/Infinite_Set"
  "~~/src/HOL/Archimedean_Field"
  "$AFP/Abstract-Rewriting/Abstract_Rewriting"
  "$AFP/Abstract-Rewriting/Relative_Rewriting"
begin

lemma trans_O_iff: "trans A ⟷ A O A ⊆ A" unfolding trans_def by auto
lemma refl_O_iff: "refl A ⟷ Id ⊆ A" unfolding refl_on_def by auto

(*TODO: move*)
lemma foldr_append2 [simp]:
  "foldr (op @ ∘ f) xs (ys @ zs) = foldr (op @ ∘ f) xs ys @ zs"
  by (induct xs) simp_all

(*TODO: move*)
lemma foldr_append2_Nil [simp]:
  "foldr (op @ ∘ f) xs [] @ zs = foldr (op @ ∘ f) xs zs"
  unfolding foldr_append2 [symmetric] by simp

(*TODO: move*)
lemma UNION_set_zip:
  "(⋃x ∈ set (zip [0..<length xs] (map f xs)). g x) = (⋃i < length xs. g (i, f (xs ! i)))"
by (auto simp: set_conv_nth)

lemma Id_on_union: "Id_on (A ∪ B) = Id_on A ∪ Id_on B" unfolding Id_on_def by auto

lemma relpow_union_cases: "(a,d) ∈ (A ∪ B)^^n ⟹ (a,d) ∈ B^^n ∨ (∃ b c k m. (a,b) ∈ B^^k ∧ (b,c) ∈ A ∧ (c,d) ∈ (A ∪ B)^^m ∧ n = Suc (k + m))"
proof (induct n arbitrary: a d)
  case (Suc n a e)
  let ?AB = "A ∪ B"
  from Suc(2) obtain b where ab: "(a,b) ∈ ?AB" and be: "(b,e) ∈ ?AB^^n" by (rule relpow_Suc_E2)
  from ab
  show ?case
  proof 
    assume "(a,b) ∈ A"
    show ?thesis
    proof (rule disjI2, intro exI conjI)
      show "Suc n = Suc (0 + n)" by simp
      show "(a,b) ∈ A" by fact
    qed (insert be, auto)
  next
    assume ab: "(a,b) ∈ B"
    from Suc(1)[OF be]
    show ?thesis
    proof 
      assume "(b,e) ∈ B ^^ n"
      with ab show ?thesis
        by (intro disjI1 relpow_Suc_I2)
    next
      assume "∃ c d k m. (b, c) ∈ B ^^ k ∧ (c, d) ∈ A ∧ (d, e) ∈ ?AB ^^ m ∧ n = Suc (k + m)"
      then obtain c d k m where "(b, c) ∈ B ^^ k" and *: "(c, d) ∈ A" "(d, e) ∈ ?AB ^^ m" "n = Suc (k + m)" by blast
      with ab have ac: "(a,c) ∈ B ^^ (Suc k)" by (intro relpow_Suc_I2)
      show ?thesis 
        by (intro disjI2 exI conjI, rule ac, (rule *)+, simp add: *)
    qed
  qed
qed simp


definition replace :: "'a ⇒ 'a set ⇒ 'a set ⇒ 'a set" where
  "replace a bs M ≡ if a ∈ M then M - {a} ∪ bs else M"

definition replace_impl :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
  "replace_impl a bs M ≡ if a ∈ set M then bs @ filter (λ b. b ≠ a) M else M"

lemma replace_impl[simp]: "set (replace_impl a bs M) = replace a (set bs) (set M)"
  unfolding replace_impl_def replace_def by auto

lemma listsum_replicate_mono: assumes "w1 ≤ (w2 :: nat)"
  shows "listsum (replicate n w1) ≤ listsum (replicate n w2)"
proof (induct n)
  case (Suc n)
  thus ?case using ‹w1 ≤ w2› by auto
qed simp

lemma all_gt_0_listsum_map:
  assumes *: "⋀x. f x > (0::nat)"
    and x: "x ∈ set xs" and len: "1 < length xs"
  shows "f x < (∑x←xs. f x)"
  using x len
proof (induct xs)
  case (Cons y xs)
  show ?case
  proof (cases "y = x")
    case True
    with *[of "hd xs"] Cons(3) show ?thesis by (cases xs, auto)
  next
    case False
    with Cons(2) have x: "x ∈ set xs" by auto
    then obtain z zs where xs: "xs = z # zs" by (cases xs, auto)
    show ?thesis
    proof (cases "length zs")
      case 0
      with x xs *[of y] show ?thesis by auto
    next
      case (Suc n)
      with xs have "1 < length xs" by auto
      from Cons(1)[OF x this] show ?thesis by simp
    qed
  qed
qed simp

lemma zip_fst: "p ∈ set (zip as bs) ⟹ fst p ∈ set as"
  by (cases p, rule set_zip_leftD, simp)

lemma zip_snd: "p ∈ set (zip as bs) ⟹ snd p ∈ set bs"
  by (cases p, rule set_zip_rightD, simp)

text ‹functions for removing the i-th element of a list and adjusting an index for this removal›
definition remove_idx :: "nat ⇒ 'a list ⇒ 'a list" where
  "remove_idx i xs ≡ take i xs @ drop (Suc i) xs"

lemma remove_idx_len:
  assumes i: "i < length xs"
  shows "length xs = Suc (length (remove_idx i xs))"
proof -
  show ?thesis unfolding arg_cong[where f = "length", OF id_take_nth_drop[OF i]]
    unfolding remove_idx_def by simp
qed

definition adjust_idx :: "nat ⇒ nat ⇒ nat" where
  "adjust_idx i j ≡ (if j < i then j else (Suc j))"

definition adjust_idx_rev :: "nat ⇒ nat ⇒ nat" where
  "adjust_idx_rev i j ≡ (if j < i then j else j - Suc 0)"

lemma adjust_idx_rev1: "adjust_idx_rev i (adjust_idx i j) = j"
  unfolding adjust_idx_def adjust_idx_rev_def by (cases "i < j", auto)

lemma adjust_idx_rev2:
  assumes "j ≠ i" shows "adjust_idx i (adjust_idx_rev i j) = j"
  unfolding adjust_idx_def adjust_idx_rev_def using assms by (cases "i < j", auto)

lemma adjust_idx_i:
  "adjust_idx i j ≠ i"
  unfolding adjust_idx_def by (cases "j < i", auto)

lemma adjust_idx_nth:
  assumes i: "i < length xs"
  shows "remove_idx i xs ! j = xs ! adjust_idx i j" (is "?l = ?r")
proof -
  let ?j = "adjust_idx i j"
  from i have ltake: "length (take i xs) = i" by simp
  note nth_xs = arg_cong[where f = "λ xs. xs ! ?j", OF id_take_nth_drop[OF i], unfolded nth_append ltake]
  show ?thesis
  proof (cases "j < i")    
    case True
    hence j: "?j = j" unfolding adjust_idx_def by simp
    show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append ltake
      using True by simp
  next
    case False    
    hence j: "?j = Suc j" unfolding adjust_idx_def by simp
    from i have lxs: "min (length xs) i = i" by simp
    show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append
      using False by (simp add: lxs)
  qed
qed

lemma adjust_idx_rev_nth:
  assumes i: "i < length xs"
    and ji: "j ≠ i"
  shows "remove_idx i xs ! adjust_idx_rev i j = xs ! j" (is "?l = ?r")
proof -
  let ?j = "adjust_idx_rev i j"
  from i have ltake: "length (take i xs) = i" by simp
  note nth_xs = arg_cong[where f = "λ xs. xs ! j", OF id_take_nth_drop[OF i], unfolded nth_append ltake]
  show ?thesis
  proof (cases "j < i")    
    case True
    hence j: "?j = j" unfolding adjust_idx_rev_def by simp
    show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append ltake
      using True by simp
  next
    case False
    with ji have ji: "j > i" by auto
    hence j: "?j = j - Suc 0" unfolding adjust_idx_rev_def by simp
    show ?thesis unfolding nth_xs unfolding j remove_idx_def nth_append ltake
      using ji by auto
  qed
qed

lemma adjust_idx_length:
  assumes i: "i < length xs"
    and j: "j < length (remove_idx i xs)"
  shows "adjust_idx i j < length xs"
  using j unfolding remove_idx_len[OF i] adjust_idx_def by (cases "j < i", auto)

lemma adjust_idx_rev_length:
  assumes "i < length xs"
    and "j < length xs"
    and "j ≠ i"
  shows "adjust_idx_rev i j < length (remove_idx i xs)"
  using assms by (cases "j < i") (simp_all add: adjust_idx_rev_def remove_idx_len[OF assms(1)])

lemma [code_unfold]:
  "(set xs = set ys) = (set xs ⊆ set ys ∧ set ys ⊆ set xs)"
  by auto

lemma zip_size_aux: "size_list (size o snd) (zip ts ls) ≤ (size_list size ls)"
proof (induct ls arbitrary: ts)
  case (Cons l ls ts)
  thus ?case by (cases ts, auto)
qed auto

lemma option_map_cong[fundef_cong]: "xs = ys ⟹ ⟦⋀ x. ys = Some x ⟹ f x = g x⟧ ⟹ map_option f xs = map_option g ys"
  by (cases ys, auto)

lemma finite_distinct: "finite { xs . distinct xs ∧ set xs = X}" (is "finite (?S X)")
proof (cases "finite X")
  case False
  with finite_set have id: "?S X = {}" by auto
  show ?thesis unfolding id by auto
next
  case True
  show ?thesis
  proof (induct rule: finite_induct[OF True])
    case 1
    show ?case by simp
  next
    case (2 x X)
    let ?L = "{0..< card (insert x X)} × ?S X" 
    from 2(3) 
    have fin: "finite ?L" by auto 
    let ?f = "λ (i,xs). take i xs @ x # drop i xs"
    show ?case
    proof (rule finite_surj[OF fin, of _ ?f], rule)
      fix xs
      assume "xs ∈ ?S (insert x X)"
      hence dis: "distinct xs" and set: "set xs = insert x X" by auto
      from distinct_card[OF dis] have len: "length xs = card (set xs)" by auto
      from set[unfolded set_conv_nth] obtain i where x: "x = xs ! i" and i: "i < length xs" by auto
      from i have min: "min (length xs) i = i" by simp
      let ?ys = "take i xs @ drop (Suc i) xs"
      from id_take_nth_drop[OF i] have xsi: "xs = take i xs @ xs ! i # drop (Suc i) xs" .
      also have "... = ?f (i,?ys)" unfolding split
        by (simp add: min x)
      finally have xs: "xs = ?f (i,?ys)" .
      show "xs ∈ ?f ` ?L"
      proof (rule image_eqI, rule xs, rule SigmaI)
        show "i ∈ {0..<card (insert x X)}" using i[unfolded len] set[symmetric] by simp
      next
        from dis xsi have disxsi: "distinct (take i xs @ xs ! i # drop (Suc i) xs)" by simp
        note disxsi = disxsi[unfolded distinct_append x[symmetric]]
        have xys: "x ∉ set ?ys" using disxsi by auto
        from distinct_take_drop[OF dis i]
        have disys: "distinct ?ys" .
        have "insert x (set ?ys) = set xs" unfolding arg_cong[OF xsi, of set] x by simp        
        hence "insert x (set ?ys) = insert x X" unfolding set by simp
        from this[unfolded insert_eq_iff[OF xys 2(2)]]
        show "?ys ∈ ?S X" using disys by auto
      qed
    qed
  qed
qed

lemma finite_distinct_subset:
  assumes "finite X"
  shows "finite { xs . distinct xs ∧ set xs ⊆ X}" (is "finite (?S X)")
proof -
  let ?X = "{ { xs. distinct xs ∧ set xs = Y} | Y. Y ⊆ X}"
  have id: "?S X = ⋃ ?X" by blast
  show ?thesis unfolding id
  proof (rule finite_Union)
    show "finite ?X" using assms  by auto
  next
    fix M
    assume "M ∈ ?X"
    with finite_distinct show "finite M" by auto
  qed
qed

lemma finite_card_eq_imp_bij_betw:
  assumes "finite A"
    and "card (f ` A) = card A"
  shows "bij_betw f A (f ` A)"
  using ‹card (f ` A) = card A›
  unfolding inj_on_iff_eq_card [OF ‹finite A›, symmetric]
  by (rule inj_on_imp_bij_betw)

text ‹Every bijective function between two subsets of a set can be turned
into a compatible renaming (with finite domain) on the full set.›
lemma bij_betw_extend:
  assumes *: "bij_betw f A B"
    and "A ⊆ V"
    and "B ⊆ V"
    and "finite A"
  shows "∃g. finite {x. g x ≠ x} ∧
    (∀x∈UNIV - (A ∪ B). g x = x) ∧
    (∀x∈A. g x = f x) ∧
    bij_betw g V V"
proof -
  have "finite B" using assms by (metis bij_betw_finite)
  have [simp]: "card A = card B" by (metis * bij_betw_same_card)
  have "card (A - B) = card (B - A)"
  proof -
    have "card (A - B) = card A - card (A ∩ B)"
      by (metis ‹finite A› card_Diff_subset_Int finite_Int)
    moreover have "card (B - A) = card B - card (A ∩ B)"
      by (metis ‹finite A› card_Diff_subset_Int finite_Int inf_commute)
    ultimately show ?thesis by simp
  qed
  then obtain g where **: "bij_betw g (B - A) (A - B)"
    by (metis ‹finite A› ‹finite B› bij_betw_iff_card finite_Diff)
  def h  "λx. if x ∈ A then f x else if x ∈ B - A then g x else x"
  have "bij_betw h A B"
    by (metis (full_types) * bij_betw_cong h_def)
  moreover have "bij_betw h (V - (A ∪ B)) (V - (A ∪ B))"
    by (auto simp: bij_betw_def h_def inj_on_def)
  moreover have "B ∩ (V - (A ∪ B)) = {}" by blast
  ultimately have "bij_betw h (A ∪ (V - (A ∪ B))) (B ∪ (V - (A ∪ B)))"
    by (rule bij_betw_combine)
  moreover have "A ∪ (V - (A ∪ B)) = V - (B - A)"
    and "B ∪ (V - (A ∪ B)) = V - (A - B)"
    using ‹A ⊆ V› and ‹B ⊆ V› by blast+
  ultimately have "bij_betw h (V - (B - A)) (V - (A - B))" by simp
  moreover have "bij_betw h (B - A) (A - B)"
    using ** by (auto simp: bij_betw_def h_def inj_on_def)
  moreover have "(V - (A - B)) ∩ (A - B) = {}" by blast
  ultimately have "bij_betw h ((V - (B - A)) ∪ (B - A)) ((V - (A - B)) ∪ (A - B))"
    by (rule bij_betw_combine)
  moreover have "(V - (B - A)) ∪ (B - A) = V"
    and "(V - (A - B)) ∪ (A - B) = V"
    using ‹A ⊆ V› and ‹B ⊆ V› by auto
  ultimately have "bij_betw h V V" by simp
  moreover have "∀x∈A. h x = f x" by (auto simp: h_def)
  moreover have "finite {x. h x ≠ x}"
  proof -
    have "finite (A ∪ (B - A))" using ‹finite A› and ‹finite B› by auto
    moreover have "{x. h x ≠ x} ⊆ (A ∪ (B - A))" by (auto simp: h_def)
    ultimately show ?thesis by (metis finite_subset)
  qed
  moreover have "∀x∈UNIV - (A ∪ B). h x = x" by (simp add: h_def)
  ultimately show ?thesis by blast
qed


lemma map_of_filter:
  assumes "P x"
  shows "map_of [(x',y) ← ys. P x'] x = map_of ys x"
proof (induct ys)
  case (Cons xy ys)
  obtain x' y where xy: "xy = (x',y)" by force
  show ?case
    by (cases "x' = x", insert assms xy Cons, auto)
qed simp

lemma infinite_imp_elem: "¬ finite A ⟹ ∃ x. x ∈ A"
  by (cases "A = {}", auto)

lemma infinite_imp_many_elems: 
  "infinite A ⟹ ∃ xs. set xs ⊆ A ∧ length xs = n ∧ distinct xs"
proof (induct n arbitrary: A)
  case (Suc n)
  from infinite_imp_elem[OF Suc(2)] obtain x where x: "x ∈ A" by auto
  from Suc(2) have "infinite (A - {x})" by auto
  from Suc(1)[OF this] obtain xs where "set xs ⊆ A - {x}" and "length xs = n" and "distinct xs" by auto
  with x show ?case by (intro exI[of _ "x # xs"], auto)
qed auto


lemma inf_pigeonhole_principle:
  assumes "∀k::nat. ∃i<n::nat. f k i"
  shows "∃i<n. ∀k. ∃k'≥k. f k' i"
proof -
  have nfin: "~ finite (UNIV :: nat set)" by auto
  have fin: "finite ({i. i < n})" by auto
  from pigeonhole_infinite_rel[OF nfin fin] assms
  obtain i where i: "i < n" and nfin: "¬ finite {a. f a i}" by auto
  show ?thesis 
  proof (intro exI conjI, rule i, intro allI)
    fix k
    have "finite {a. f a i ∧ a < k}" by auto
    with nfin have "¬ finite ({a. f a i} - {a. f a i ∧ a < k})" by auto
    from infinite_imp_elem[OF this]
    obtain a where "f a i" and "a ≥ k" by auto
    thus "∃ k' ≥ k. f k' i" by force
  qed
qed

lemma infinite_inj_on_remove_one:
  fixes f :: "'a ⇒ 'b" 
  assumes inf: "infinite B"
  and inj: "inj_on f A"
  and ran: "range f ⊆ B"
  shows "∃ g. inj_on g A ∧ range g ⊆ B - {b}"
proof -
  from inf have inf: "infinite (B - {b})" by auto
  from infinite_imp_elem[OF inf] obtain b' where b': "b' ∈ B - {b}" by force
  from infinite_countable_subset[OF inf] obtain h :: "nat ⇒ 'b" where inj_h: "inj h" and ran_h: "range h ⊆ B - {b}" by auto
  let ?h = "λ a. h (Suc (the_inv h (f a)))"
  let ?f = "λ a. (if f a ∈ range h then ?h a else f a)"
  let ?g = "λ a. if f a = b then h 0 else if a ∈ A then ?f a else b'"
  show ?thesis
  proof (rule exI[of _ ?g], unfold inj_on_def, intro conjI ballI impI)
    fix a1 a2
    assume a1: "a1 ∈ A" and a2: "a2 ∈ A" and id: "?g a1 = ?g a2"
    show "a1 = a2" 
    proof (cases "f a1 = b")
      case True 
      with id have id: "?g a2 = h 0" and fa1: "f a1 = b" by auto
      show ?thesis
      proof (cases "f a2 = b")
        case True
        with fa1 id a1 a2 inj show ?thesis unfolding inj_on_def by auto
      next
        case False
        with id a2 have id: "?f a2 = h 0" by auto
        with inj_h show ?thesis unfolding inj_on_def by (cases "f a2 ∈ range h", auto)
      qed
    next
      case False
      with id a1 have id: "?f a1 = ?g a2" by auto
      show ?thesis
      proof (cases "f a2 = b")
        case True
        with id have "?f a1 = h 0" by auto
        with inj_h show ?thesis unfolding inj_on_def by (cases "f a1 ∈ range h", auto)
      next
        case False
        with id a2 have id: "?f a1 = ?f a2" by auto
        have "f a1 = f a2"
        proof (cases "f a1 ∈ range h")
          case True note r1 = this
          with id have id: "?f a2 = ?h a1" by simp
          hence r2: "f a2 ∈ range h" by (cases "f a2 ∈ range h", auto)
          with id have id: "?h a1 = ?h a2" by simp
          from r1 r2 obtain i1 i2 where h: "f a1 = h i1" "f a2 = h i2" by auto
          from id[unfolded h the_inv_f_f[OF inj_h]] have "h (Suc i1) = h (Suc i2)" .
          with inj_h have id: "i1 = i2" unfolding inj_on_def by auto
          with h show "f a1 = f a2" by auto
        next
          case False note r1 = this
          {
            assume "f a2 ∈ range h"
            with id have id: "?f a1 = ?h a2" by simp
            hence "f a1 ∈ range h" by (cases "f a1 ∈ range h", auto)
            with r1 have False by auto
          }
          with r1 id show ?thesis by auto
        qed
        with a1 a2 inj show ?thesis unfolding inj_on_def by auto
      qed
    qed
  next
    show "range ?g ⊆ B - {b}" using ran_h ran b' by auto
  qed
qed  

lemma infinite_inj_on_finite_remove_finite:
  fixes f :: "'a ⇒ 'b" and B :: "'b set"
  assumes inf: "infinite B"
    and inj: "inj_on f A"
    and fin: "finite B'"
    and ran: "range f ⊆ B"
  shows "∃ g. inj_on g A ∧ range g ⊆ B - B'"
  using fin
proof (induct B')
  case empty
  show ?case using inj ran by auto
next
  case (insert b B')
  from insert(3) obtain g where inj: "inj_on (g :: 'a ⇒ 'b) A" and ran: "range g ⊆ B - B'" by auto
  from insert(1) inf have "infinite (B - B')" by auto
  from infinite_inj_on_remove_one[OF this inj ran, of b]
  show ?case by auto
qed


subsection ‹Combinators›

definition const :: "'a ⇒ 'b ⇒ 'a" where
  "const ≡ (λx y. x)"

definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ ('b ⇒ 'a ⇒ 'c)" where
  "flip f ≡ (λx y. f y x)"
declare flip_def[simp]

lemma const_apply[simp]: "const x y = x"
  by (simp add: const_def)

lemma foldr_Cons_append_conv [simp]:
  "foldr op # xs ys = xs @ ys"
  by (induct xs) simp_all

lemma foldl_flip_Cons[simp]:
  "foldl (flip op #) xs ys = rev ys @ xs"
  by (induct ys arbitrary: xs) simp_all

(*FIXME: already present as List.foldl_foldr, but
direction seems odd.*)
lemma foldr_flip_rev[simp]:
  "foldr (flip f) (rev xs) a = foldl f a xs"
  by (simp add: foldr_conv_foldl)

(*FIXME: already present as List.foldr_foldr, but
direction seems odd.*)
lemma foldl_flip_rev[simp]:
  "foldl (flip f) a (rev xs) = foldr f xs a"
  by (simp add: foldl_conv_foldr)

(*FIXME: available in HOL library?*)
(*
interpretation o!: semigroup_add "op ∘"
  by (unfold_locales) (simp add: o_assoc)
*)

fun debug :: "string ⇒ string ⇒ 'a ⇒ 'a" where "debug i t x = x"


section ‹Auxiliary Lemmas›

lemma (in order) rtranclp_less_eq [simp]:
  "(op ≤)** = op ≤"
  by (intro ext) (auto elim: rtranclp_induct)

lemma (in order) tranclp_less [simp]:
  "(op <)++ = op <"
  by (intro ext) (auto elim: tranclp_induct)

lemma (in order) rtranclp_greater_eq [simp]:
  "(op ≥)** = op ≥"
  by (intro ext) (auto elim: rtranclp_induct)

lemma (in order) tranclp_greater [simp]:
  "(op >)++ = op >"
  by (intro ext) (auto elim: tranclp_induct)

lemma down_chain_imp_eq:
  fixes f :: "nat seq"
  assumes "∀i. f i ≥ f (Suc i)"
  shows "∃N. ∀i > N. f i = f (Suc i)"
proof -
  let ?F = "{f i | i. True}"
  from wf_less [unfolded wf_eq_minimal, THEN spec, of ?F]
    obtain x where "x ∈ ?F" and *: "∀y. y < x ⟶ y ∉ ?F" by auto
  obtain N where "f N = x" using ‹x ∈ ?F› by auto
  moreover have "∀i > N. f i ∈ ?F" by auto
  ultimately have "∀i > N. ¬ f i < x" using * by auto
  moreover have "∀i > N. f N ≥ f i"
    using chainp_imp_rtranclp [of "op ≥" f, OF assms] by simp
  ultimately have "∀i > N. f i = f (Suc i)"
    using ‹f N = x› by (auto) (metis less_SucI order.not_eq_order_implies_strict)
  then show ?thesis ..
qed

lemma set_subset_insertI: "set xs ⊆ set (List.insert x xs)" by auto
lemma set_removeAll_subset: "set (removeAll x xs) ⊆ set xs" by auto

lemma all_less_two: "(∀ i < Suc (Suc 0). P i) = (P 0 ∧ P (Suc 0))" (is "?l = ?r") 
proof
  assume ?l thus ?r by auto
next
  assume r: ?r
  show ?l
  proof(intro allI impI)
    fix i
    assume "i < Suc (Suc 0)"
    hence "i = 0 ∨ i = Suc 0" by auto
    with r show "P i" by auto
  qed
qed 


subsection ‹Induction Rules›

text ‹Induction over a finite set of natural numbers.›
lemma bound_nat_induct[consumes 1]:
  assumes "n ∈ {l..u}" and "P l" and "⋀n. ⟦P n; n ∈ {l..<u}⟧ ⟹ P (Suc n)"
  shows "P n"
using assms
proof (induct n)
 case (Suc n) thus ?case by (cases "Suc n = l") auto
qed simp

  
fun max_f :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
  "max_f f 0 = 0"
| "max_f f (Suc i) = max (f i) (max_f f i)"

lemma max_f: "i < n ⟹ f i ≤ max_f f n"
proof (induct n)
  case (Suc n)
  thus ?case by (cases "i = n", auto)
qed simp


subsection ‹size estimations›

lemma size_list_pointwise2: assumes "length xs = length ys"
  and "⋀ i. i < length ys ⟹ f (xs ! i) ≤ g (ys ! i)"
  shows "size_list f xs ≤ size_list g ys"
proof -
  have id: "(size_list f xs ≤ size_list g ys) = (listsum (map f xs) ≤ listsum (map g ys))"
    unfolding size_list_conv_listsum assms(1) by auto
  have "map f xs = map f (map (op ! xs) [0..<length xs])" using map_nth[of xs] by simp
  also have "... = map (λ i. f (xs ! i)) [0..<length xs]" (is "_ = ?xs") by simp
  finally have xs: "map f xs = ?xs" .
  have "map g ys = map g (map (op ! ys) [0..<length ys])" using map_nth[of ys] by simp
  also have "... = map (λ i. g (ys ! i)) [0..<length xs]" (is "_ = ?ys") using assms by simp
  finally have ys: "map g ys = ?ys" .
  show ?thesis
    unfolding id unfolding xs ys
    by (rule listsum_mono, insert assms, auto)
qed    

lemma size_list_pointwise3: assumes len: "length xs = length ys"
  and xs: "xs ≠ []"
  and lt: "⋀ i. i < length ys ⟹ f (xs ! i) < g (ys ! i)"
  shows "size_list f xs < size_list g ys"
proof -
  from xs obtain x xs' where xs: "xs = x # xs'" by (cases xs, auto)
  with len obtain y ys' where ys: "ys = y # ys'" by (cases ys, auto)
  have "size_list f xs = f x + 1 + size_list f xs'" by (simp add: xs)
  also have "size_list f xs' ≤ size_list g ys'"
  proof (rule size_list_pointwise2)
    fix i
    assume "i < length ys'"
    hence "Suc i < length ys" unfolding ys by simp
    from lt[OF this]
    show "f (xs' ! i) ≤ g (ys' ! i)" unfolding xs ys by auto
  qed (insert len xs ys, simp)
  also have "f x < g y" using lt[of 0] unfolding xs ys by simp
  also have "g y + 1 + size_list g ys' = size_list g ys" unfolding ys by simp
  finally show ?thesis by arith
qed

subsection ‹assignments from key-value pairs›

fun enum_vectors :: "'c list ⇒ 'v list ⇒ ('v × 'c)list list"
where "enum_vectors C [] = [[]]"
    | "enum_vectors C (x # xs) = (let rec = enum_vectors C xs in concat (map (λ vec. map (λ c. (x,c) # vec) C) rec))" 

definition fun_of :: "('v × 'c) list ⇒ 'v ⇒ 'c" where
  [simp]: "fun_of vec x = the (map_of vec x)"

lemma enum_vectors_complete:
  assumes "C ≠ []"
  shows "∃ vec ∈ set (enum_vectors C xs). ∀ x ∈ set xs. ∀ c ∈ set C. α x = c ⟶ fun_of vec x = c"
proof (induct xs, simp)
  case (Cons x xs)
  from this obtain vec where enum: "vec ∈ set (enum_vectors C xs)" and eq: "∀ x ∈ set xs. ∀ c ∈ set C. α x = c ⟶ fun_of vec x = c" by auto
  from enum have res: "set (map (λ c. (x,c) # vec) C) ⊆ set (enum_vectors C (x # xs)) " (is "_ ⊆ ?res") by auto
  show ?case 
  proof (cases "α x ∈ set C")
    case False
    from assms have "hd C ∈ set C" by auto
    with res have elem: "(x,hd C) # vec ∈ ?res" (is "?vec ∈ _") by auto
    from eq False have "∀ y ∈ set (x # xs). ∀ c ∈ set C. α y = c ⟶ fun_of ?vec y = c" by auto
    with elem show ?thesis by blast
  next
    case True
    with res have elem: "(x, α x) # vec ∈ ?res" (is "?vec ∈ _") by auto
    from eq True have "∀ y ∈ set (x # xs). ∀ c ∈ set C. α y = c ⟶ fun_of ?vec y = c" by auto
    with elem show ?thesis by blast
  qed
qed

lemma enum_vectors_sound:
  assumes "y ∈ set xs" and "vec ∈ set (enum_vectors C xs)"
  shows "fun_of vec y ∈ set C"
  using assms
proof (induct xs arbitrary: vec, simp)
  case (Cons x xs vec)
  from Cons(3) obtain v vecc where vec: "vec = v # vecc" by auto
  note C3 = Cons(3)[unfolded vec enum_vectors.simps Let_def]
  from C3 have vecc: "vecc ∈ set (enum_vectors C xs)" by auto
  from C3 obtain c where v: "v = (x,c)" and c: "c ∈ set C" by auto
  show ?case 
  proof (cases "y = x")
    case True
    show ?thesis unfolding vec v True using c by auto
  next
    case False
    with Cons(2) have y: "y ∈ set xs" by auto
    from False have id: "fun_of vec y = fun_of vecc y"
      unfolding vec v by auto
    show ?thesis unfolding id
      by (rule Cons(1)[OF y vecc])
  qed
qed

declare fun_of_def[simp del]

lemma map_of_nth_zip_Some [simp]:
  assumes "distinct vs" and "length vs ≤ length ts" and "i < length vs"
  shows "map_of (zip vs ts) (vs ! i) = Some (ts ! i)"
using assms proof (induct i arbitrary: vs ts)
  case 0 thus ?case by (induct ts) (induct vs, auto)+
next
  case (Suc i) show ?case
  proof (cases ts)
    case Nil with Suc show ?thesis unfolding Nil by simp
  next
    case (Cons t ts')
    note Cons' = this
    show ?thesis
    proof (cases vs)
      case Nil from Suc show ?thesis unfolding Cons' Nil by simp
    next
      case (Cons v vs') from Suc show ?thesis unfolding Cons Cons' by auto
    qed
  qed
qed

lemma map_of_append_Some:
  "map_of xs y = Some z ⟹ map_of (xs @ ys) y = Some z"
  by (induction xs) auto

lemma map_of_append_None:
  "map_of xs y = None ⟹ map_of (xs @ ys) y = map_of ys y"
  by (induction xs) auto

lemma fun_of_concat:
  assumes mem: "x ∈ set (map fst (τs i))"
    and i: "i < n"
    and ident: "⋀ i j. i < n ⟹ j < n ⟹ x ∈ set (map fst (τs i)) ⟹ x ∈ set (map fst (τs j)) ⟹ fun_of (τs i) x = fun_of (τs j) x"
  shows "fun_of (concat (map τs [0..<n])) x = fun_of (τs i) x"
using assms
proof (induct n arbitrary: i τs)
  case 0
  thus ?case by simp
next
  case (Suc n i τs) note IH = this
  let ?τs = "λi. τs (Suc i)"
  have id: "concat (map τs [0..<Suc n]) = τs 0 @ concat (map ?τs [0..<n])" unfolding map_upt_Suc by simp
  let ?l = "map_of (τs 0) x"
  show ?case
  proof (cases i)
    case 0
    with IH(2) have x: "x ∈ set (map fst (τs 0))" by auto
    then obtain y where xy: "(x,y) ∈ set (τs 0)" by auto
    from map_of_eq_None_iff[of "τs 0" x] xy have "?l ≠ None" by force
    then obtain y where look: "?l = Some y" by (cases "τs 0", auto)
    find_theorems "map_of" "_ ++ _"
    show ?thesis unfolding 0 fun_of_def id look map_of_append_Some[OF look] by simp
  next
    case (Suc j)
    with IH(3)
    have 0: "0 < i" and j: "j < n" by auto
    show ?thesis 
    proof (cases "x ∈ set (map fst (τs 0))")
      case False
      have l: "?l = None"
      proof (cases "?l")
        case (Some y)
        from map_of_SomeD[OF this] and False show ?thesis by force
      qed simp
      show ?thesis unfolding fun_of_def id map_of_append_None[OF l]
        unfolding fun_of_def[symmetric] Suc
      proof (rule IH(1)[OF _ j])
        show "x ∈ set (map fst (τs (Suc j)))" using IH(2) unfolding Suc .
      next
        fix i j
        assume "i < n" and "j < n" and "x ∈ set (map fst (τs (Suc i)))" and "x ∈ set (map fst (τs (Suc j)))"
        thus "fun_of (τs (Suc i)) x = fun_of (τs (Suc j)) x"
          using IH(4)[of "Suc i" "Suc j"] by auto
      qed
    next
      case True
      then obtain y where xy: "(x,y) ∈ set (τs 0)" by auto
      from map_of_eq_None_iff[of "τs 0" x] and xy have "?l ≠ None" by force
      then obtain y where look: "?l = Some y" by (cases "τs 0", auto)
      have "fun_of (concat (map τs [0..<Suc n])) x = fun_of (τs 0) x" 
        unfolding id fun_of_def look
        map_of_append_Some[OF look] by simp
      also have "... = fun_of (τs i) x"
      proof (rule IH(4)[OF _ IH(3)])
        from xy show "x ∈ set (map fst (τs 0))" by force
      next
        from IH(2) show "x ∈ set (map fst (τs i))" by force
      qed simp
      finally show ?thesis .
    qed
  qed
qed

lemma fun_of_concat_part: assumes mem: "x ∈ set (map fst (τs i))"
  and i: "i < n"
  and partition: "is_partition (map (λ i. set (map fst (τs i))) [0..<n])"
  shows "fun_of (concat (map τs [0..<n])) x = fun_of (τs i) x"
proof (rule fun_of_concat, rule mem, rule i)
  fix i j
  assume "i < n" and "j < n" and "x ∈ set (map fst (τs i))" and "x ∈ set (map fst (τs j))"
  hence "i = j" using partition[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto)
  thus "fun_of (τs i) x = fun_of (τs j) x" by simp
qed

lemma fun_of_concat_merge:
  assumes "⋀ i. i < length ts ⟹ x ∈ h (ts ! i) ⟹ fun_of (f i) x = (g ! i) x"
    and "length ts = length g"
    and "⋀ i. i < length ts ⟹ map_of (f i) x ≠ None ⟷ x ∈ h (ts ! i)"
    and "x ∈ h (ts ! i)"
    and "i < length ts"
  shows "fun_of (concat (map f [0..<length ts])) x = fun_merge g (map h ts) x"
  using assms 
  unfolding fun_merge_def fun_of_def
proof (induct ts arbitrary: i f g)
  case Nil
  thus ?case by simp
next
  case (Cons xy ts)
  let ?p' = "λ ts i. i < length (map h ts) ∧ x ∈ map h ts ! i"
  let ?p = "?p' (xy # ts)"
  let ?P = "?p' ts"
  let ?L = "LEAST i. ?p i"
  have id: "the (map_of (concat (map f [0..<length (xy # ts)])) x) = 
    the (map_of (f 0 @ concat (map (λ i. f (Suc i)) [0..<length ts])) x)"
    (is "?l = the (map_of ( _ @ ?l') x)")
    by (simp add: map_upt_Suc del: upt_Suc) 
  show ?case 
  proof (cases "map_of (f 0) x")
    case (Some y)
    from map_of_append_Some[OF Some]
    have ly: "?l = y" unfolding id Some by simp
    have "?p 0" using Cons(4)[of 0] using Some by auto
    hence L0: "?L = 0" 
      by (rule Least_equality, simp)
    from Cons(4)[of 0] Some have x: "x ∈ h xy" by auto
    show ?thesis unfolding ly L0 using Cons(2)[of 0, unfolded Some] x by simp
  next
    case None
    from map_of_append_None[OF None]
    have ll: "?l = the (map_of ?l' x)" unfolding id by simp
    from Cons(4)[of 0] None have x: "x ∉ h xy" by auto
    hence p0: "¬ ?p 0" by simp
    from Cons(5) Cons(6) have pI: "?p i" unfolding nth_map[OF Cons(6)] by simp
    from Least_Suc[of ?p, OF pI p0] have L: "?L = Suc (LEAST m. ?P m)" by simp
    from Cons(3) obtain a g' where g: "g = a # g'" by (cases g, auto)
    from Cons(5) x obtain j where i: "i = Suc j" by (cases i, auto)
    show ?thesis unfolding ll L g nth_Cons_Suc
    proof (rule Cons(1))
      from g Cons(3) show "length ts = length g'" by auto
    next
      from Cons(5) i show "x ∈ h (ts ! j)" by auto
    next
      from Cons(6) i show "j < length ts" by auto
    next
      fix m
      assume "m < length ts"
      thus "map_of (f (Suc m)) x ≠ None ⟷ x ∈ h (ts ! m)"
        using Cons(4)[of "Suc m"] by auto
    next
      fix m
      assume "m < length ts" and "x ∈ h (ts ! m)"
      thus "the (map_of (f (Suc m)) x) = (g' ! m) x"
        using Cons(2)[of "Suc m"] unfolding g by auto
    qed
  qed
qed

context 
  fixes P :: "'a ⇒ 'b ⇒ bool"
  and R :: "'a rel"
  and R' :: "'b rel"
  assumes simulate: "⋀ s t s'. P s t ⟹ (s,s') ∈ R ⟹ ∃ t'. P s' t' ∧ (t,t') ∈ R'"
begin
lemma simulate_conditional_steps_count: assumes steps: "(s,s') ∈ R^^n"
  and P: "P s t"
  shows "∃ t'. P s' t' ∧ (t,t') ∈ R'^^n"
  using steps 
proof (induct n arbitrary: s')
  case 0
  with P show ?case by auto
next
  case (Suc n s'')
  from Suc(2) obtain s' where ss': "(s,s') ∈ R^^n" and ss'': "(s',s'') ∈ R" by auto
  from Suc(1)[OF ss'] obtain t' where tt': "(t, t') ∈ R' ^^ n" and P: "P s' t'" by auto
  from simulate[OF P ss''] tt' show ?case by auto
qed

lemma simulate_conditional_steps: assumes steps: "(s,s') ∈ R*"
  and P: "P s t"
  shows "∃ t'. P s' t' ∧ (t,t') ∈ R'*"
proof -
  from steps obtain n where "(s,s') ∈ R^^n" by auto
  from simulate_conditional_steps_count[OF this P]
  show ?thesis by (blast intro: relpow_imp_rtrancl)
qed
end

context 
  fixes P :: "'a ⇒ 'b ⇒ bool"
  and R S :: "'a rel"
  and R' S' :: "'b rel"
  assumes simulateR: "⋀ s t s'. P s t ⟹ (s,s') ∈ R ⟹ ∃ t'. P s' t' ∧ (t,t') ∈ R'"
  and simulateS: "⋀ s t s'. P s t ⟹ (s,s') ∈ S ⟹ ∃ t'. P s' t' ∧ (t,t') ∈ S'"
begin
lemma simulate_conditional_relative_step: assumes step: "(s,s') ∈ relto R S"
  and P: "P s t"
  shows "∃ t'. P s' t' ∧ (t,t') ∈ relto R' S'"
proof -
  from step obtain u v where su: "(s,u) ∈ S*" and uv: "(u,v) ∈ R" and vs': "(v,s') ∈ S*" by auto
  have "∃ u'. P u u' ∧ (t,u') ∈ S'*"
    by (rule simulate_conditional_steps[of P, OF simulateS su P])
  then obtain u' where P: "P u u'" and tu: "(t,u') ∈ S'*" by blast
  from simulateR[OF P uv] obtain v' where P: "P v v'" and uv: "(u',v') ∈ R'" by auto
  have "∃ t'. P s' t' ∧ (v',t') ∈ S'*"
    by (rule simulate_conditional_steps[of P, OF simulateS vs' P])
  then obtain t' where P: "P s' t'" and vt: "(v',t') ∈ S'*" by blast
  from tu uv vt have "(t,t') ∈ relto R' S'" by auto
  with P show ?thesis by auto
qed

lemma simulate_conditional_relative_steps_count: assumes step: "(s,s') ∈ (relto R S)^^n"
  and P: "P s t"
  shows "∃ t'. P s' t' ∧ (t,t') ∈ (relto R' S')^^n"
  by (rule simulate_conditional_steps_count[of P, OF simulate_conditional_relative_step step P])
end

locale relative_simulation_image = 
  fixes S :: "'a rel" and N :: "'a rel" and B :: "'b rel" and f :: "'a ⇒ 'b"
  assumes S: "(x,y) ∈ S ⟹ (f x, f y) ∈ B^+"
  and N: "(x,y) ∈ N ⟹ (f x, f y) ∈ B*"
begin

lemma many_non_strict: "(x,y) ∈ N* ⟹ (f x, f y) ∈ B*"
proof (induct rule: rtrancl_induct)
  case (step y z)
  from step(3) N[OF step(2)] show ?case by auto
qed auto

lemma single_relative: assumes step: "(x,y) ∈ relto S N" shows "(f x, f y) ∈ B^+"
proof -
  from step obtain u v where xu: "(x,u) ∈ N*" and uv: "(u,v) ∈ S" and vy: "(v,y) ∈ N*" by blast
  from many_non_strict[OF xu] S[OF uv] many_non_strict[OF vy] show ?thesis by auto
qed

lemma count_relative: "(x,y) ∈ (relto S N)^^n ⟹ ∃ m ≥ n. (f x, f y) ∈ B^^m"
proof (induct n arbitrary: x y)
  case (Suc n x y)
  let ?R = "relto S N"
  from Suc(2) obtain u where xu: "(x,u) ∈ ?R ^^ n" and uy: "(u,y) ∈ ?R" by auto
  from single_relative[OF uy] 
  obtain n1 where n1: "n1 > 0" and uy: "(f u, f y) ∈ B ^^ n1" unfolding trancl_power by blast
  from Suc(1)[OF xu] obtain m where m: "m ≥ n" and xu: "(f x, f u) ∈ B^^m" by auto
  from xu uy have xy: "(f x, f y) ∈ B^^(m + n1)" unfolding relpow_add by blast
  from m n1 have n: "m + n1 ≥ Suc n" by auto
  from xy n show ?case by auto
next
  case 0
  thus ?case by (intro exI[of _ 0], auto)
qed 
end

lemma rtrancl_map:
  assumes simu: "⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s"
    and steps: "(x, y) ∈ r*"
  shows "(f x, f y) ∈ s*"
  by (rule relative_simulation_image.many_non_strict[of "{}", OF _ steps], unfold_locales, insert simu, auto)

context
begin

private fun simulate :: "'a rel ⇒ ('a ⇒ bool) ⇒ 'a ⇒ nat ⇒ 'a" where
  "simulate R P s 0 = s"
| "simulate R P s (Suc n) = (SOME u. (simulate R P s n,u) ∈ R ∧ P u)"

lemma conditional_steps_imp_not_SN_on: assumes start: "P s"
  and step: "⋀ t. P t ⟹ ∃ u. (t,u) ∈ R ∧ P u"
  shows "¬ SN_on R {s}"
proof -
  let ?sim = "simulate R P s"
  {
    fix i
    have "P (?sim i) ∧ (i > 0 ⟶ (?sim (i - 1), ?sim i) ∈ R)"
    proof (induct i)
      case 0 show ?case using start by auto
    next
      case (Suc i)
      hence P: "P (?sim i)" by simp
      from someI_ex[OF step[OF P]]
      show ?case by auto
    qed
  } note main = this
  def g  "?sim"
  have "g 0 = s" unfolding g_def by simp  
  {
    fix i
    from main[of "Suc i"]
    have "(g i, g (Suc i)) ∈ R" unfolding g_def by auto
  }
  with ‹g 0 = s› show ?thesis by auto
qed
end

lemma relpow_Suc: "r ^^ Suc n = r O r ^^ n"
  using relpow_add[of 1 n r] by auto

lemma converse_power: fixes r :: "'a rel" shows "(r¯)^^n = (r^^n)¯"
proof (induct n)
  case (Suc n)
  show ?case unfolding relpow.simps(2)[of _ "r¯"] relpow_Suc[of _ r]
    by (simp add: Suc converse_relcomp)
qed simp


lemma finite_imp_eq [simp]:
  "finite {x. P x ⟶ Q x} ⟷ finite {x. ¬ P x} ∧ finite {x. Q x}"
  by (auto simp: Collect_imp_eq Collect_neg_eq)

lemma trans_refl_imp_rtrancl_id:
  assumes "trans r" "refl r"
  shows "r* = r"
proof
  show "r* ⊆ r"
  proof
    fix x y
    assume "(x,y) ∈ r*"
    thus "(x,y) ∈ r"
      by (induct, insert assms, unfold refl_on_def trans_def, blast+)
  qed
qed regexp

lemma image_Pair_Un_imp_eq:
  assumes "a ≠ b"
    and "Pair a ` A ∪ Pair b ` B = Pair a ` C ∪ Pair b ` D"
  shows "A = C ∧ B = D"
proof (rule ccontr)
  presume "A ≠ C ∨ B ≠ D"
  thus False
  proof
    assume "A ≠ C"
    then obtain x where "x ∈ (A - C) ∨ x ∈ (C - A)" by auto
    thus False by (rule disjE) (insert assms, auto)
  next
    assume "B ≠ D"
    then obtain y where "y ∈ (B - D) ∨ y ∈ (D - B)" by auto
    thus False by (rule disjE) (insert assms, auto)
  qed
qed simp

lemma image_Pair_Un_eq[simp]:
  "a ≠ b ⟹ Pair a ` A ∪ Pair b ` B = Pair a ` C ∪ Pair b ` D ⟷ A = C ∧ B = D"
  using image_Pair_Un_imp_eq[of a b A B C D] by blast

lemma inj_Pair1: "inj (Pair a)" unfolding inj_on_def by auto

lemma Pair_image_diff_simps[simp]:
  "a ≠ b ⟹ (Pair a ` A ∪ Pair b ` B) - (Pair a ` C) = (Pair a ` A - Pair a ` C) ∪ Pair b ` B"
  "a ≠ b ⟹ (Pair a ` A ∪ Pair b ` B) - (Pair b ` C) = Pair a ` A ∪ (Pair b ` B - Pair b ` C)"
  "a ≠ b ⟹ (Pair a ` A ∪ (Pair b ` B - Pair b ` C)) - Pair a ` D =
    (Pair a ` A - Pair a ` D) ∪ (Pair b ` B - Pair b ` C)"
  by auto

lemma Collect_Un: "{x ∈ A ∪ B. P x} = {x ∈ A. P x} ∪ {x ∈ B. P x}" by auto
lemma image_snd_Pair: "snd ` {x ∈ Pair a ` A. P x} = {x ∈ A. P (a, x)}" by force
lemma Collect_nested_conj: "{x ∈ {x ∈ A. P x}. Q x} = {x ∈ A. P x ∧ Q x}" by simp
lemma image_snd_Pair_Un[simp]: "snd ` (Pair x ` A ∪ (Pair y ` B)) = A ∪ B" by force

(*FIXME: move to Map.thy*)
lemma ran_map_upd_Some:
  assumes "m a = Some b"
  shows "ran (m(a ↦ c)) ⊆ insert c (ran m)"
proof
  fix x assume "x ∈ ran (m(a ↦ c))"
  then obtain k where upd: "(m(a ↦ c)) k = Some x" by (auto simp: ran_def)
  show "x ∈ insert c (ran m)"
  proof (cases "a = k")
    case True
    from assms and upd have x: "x = c" by (simp add: True)
    thus ?thesis by simp
  next
    case False
    hence m_upd: "(m(a ↦ c)) k = m k" by simp
    from upd[unfolded m_upd] have "x ∈ ran m" by (auto simp: ran_def)
    thus ?thesis by simp
  qed
qed

(*FIXME: move to Map.thy?*)
lemma subset_UNION_ran:
  assumes "m a = Some b"
    and "set b ⊆ set c"
  shows "UNION (ran (m(a ↦ c))) set = UNION (insert c (ran m)) set"
proof
  show "UNION (ran (m(a ↦ c))) set ⊆ UNION (insert c (ran m)) set"
  proof
    fix x assume "x ∈ UNION (ran (m(a ↦ c))) set"
    then obtain rs where rs: "rs ∈ ran (m(a ↦ c))" and x: "x ∈ set rs" by auto
    from ran_map_upd_Some[of m a b c, OF assms(1)] and rs
      have "rs ∈ insert c (ran m)" by blast
    with x show "x ∈ UNION (insert c (ran m)) set" by auto
  qed
next
  show "UNION (insert c (ran m)) set ⊆ UNION (ran (m(a ↦ c))) set"
  proof
    fix x assume "x ∈ UNION (insert c (ran m)) set"
    then obtain rs where "rs ∈ insert c (ran m)" and x: "x ∈ set rs" by auto
    hence "c = rs ∨ rs ∈ ran m" by auto
    thus "x ∈ UNION (ran (m(a ↦ c))) set"
    proof
      assume c: "c = rs"
      show ?thesis unfolding c using x by (auto simp: ran_def)
    next
      assume "rs ∈ ran m"
      then obtain k where mk: "m k = Some rs" by (auto simp: ran_def)
      show  ?thesis
      proof (cases "a = k")
        case True
        from assms(1) and mk have rs: "rs = b" by (simp add: True)
        with assms(2) and x show ?thesis by (auto simp: ran_def)
      next
        case False
        with mk have "rs ∈ ran (m(a ↦ c))" by (auto simp: ran_def)
        with x show ?thesis by blast
      qed
    qed
  qed
qed

locale abstract_closure =
  fixes A B C :: "'a rel" and S :: "'a set" and P :: "'a ⇒ bool"
  assumes S: "⋀ a b. a ∈ S ⟹ (a,b) ∈ C* ⟹ P b"
  and AC: "A ⊆ C*"
  and PAB: "⋀ a b. P a ⟹ P b ⟹ (a,b) ∈ A ⟹ (a,b) ∈ B"
begin

lemma A_steps_imp_P: assumes a: "a ∈ S"
  and rel: "(a,b) ∈ A^^n" shows "P b"
proof -
  from relpow_imp_rtrancl[OF rel] rtrancl_mono[OF AC] have "(a,b) ∈ C*" by auto
  from S[OF a this] show ?thesis .
qed
  
lemma A_steps_imp_B_steps_count: assumes a: "a ∈ S" 
  shows "(a,b) ∈ A^^n ⟹ (a,b) ∈ B^^n"
proof (induct n arbitrary: b)
  case (Suc n c)
  from Suc(2) obtain b where ab: "(a,b) ∈ A^^n" and bc: "(b,c) ∈ A" by auto
  from Suc(1)[OF ab] have abB: "(a,b) ∈ B^^n" .
  with PAB[OF A_steps_imp_P[OF a ab] A_steps_imp_P[OF a Suc(2)] bc]
  show ?case by auto
qed auto

lemma A_steps_imp_B_steps: assumes a: "a ∈ S" 
  shows "(a,b) ∈ A* ⟹ (a,b) ∈ B*"
using A_steps_imp_B_steps_count[OF a, of b] unfolding rtrancl_is_UN_relpow by auto
end

locale abstract_closure_twice = abstract_closure +
  fixes A' B' :: "'a rel"
  assumes AC': "A' ⊆ C*"
  and PAB': "⋀ a b. P a ⟹ P b ⟹ (a,b) ∈ A' ⟹ (a,b) ∈ B'"
begin
lemma AA_steps_imp_P: assumes a: "a ∈ S"
  and steps: "(a,b) ∈ (A ∪ A')*" shows "P b"
proof -
  from AC AC' have "A ∪ A' ⊆ C*" by auto
  from rtrancl_mono[OF this] steps have "(a,b) ∈ C*" by auto
  from S[OF a this] show ?thesis .
qed

lemma shift_closure: assumes a: "a ∈ S"
  and ab: "(a,b) ∈ (A ∪ A')*"
  shows "abstract_closure_twice A B C {b} P A' B'"
proof -
  {
    fix c
    assume bc: "(b,c) ∈ C*"
    from AC AC' have "(A ∪ A') ⊆ C*" by auto
    from ab rtrancl_mono[OF this] have ab: "(a,b) ∈ C*" by auto
    with bc have "(a,c) ∈ C* O C*" by auto
    also have "… ⊆ C*" by regexp
    finally have "P c" by (rule S[OF a])
  } note P = this
  show ?thesis
    by (unfold_locales, insert P AC' PAB' AC PAB, auto)
qed

lemma AA_step_imp_BB_step: assumes a: "a ∈ S"
  and steps: "(a,b) ∈ relto A A'" shows "(a,b) ∈ relto B B'"
proof -
  interpret alt: abstract_closure_twice A' B' C S P A B
    by (unfold_locales, insert S AC' PAB' AC PAB, auto)
  from steps obtain c d where ac: "(a,c) ∈ A'*" and cd: "(c,d) ∈ A" and db: "(d,b) ∈ A'*" by blast
  from alt.A_steps_imp_B_steps[OF a ac] have ac': "(a,c) ∈ B'*" by auto
  from AA_steps_imp_P[OF a] have P: "⋀ b. (a,b) ∈ (A ∪ A')* ⟹ P b" .
  have ac: "(a,c) ∈ (A ∪ A')*" using ac by regexp
  have "(a,d) ∈ (A ∪ A')* O A" using ac cd by auto
  also have "… ⊆ (A ∪ A')*" by regexp
  finally have ad: "(a,d) ∈ (A ∪ A')*" .
  from PAB[OF P[OF ac] P[OF ad] cd] have cd': "(c,d) ∈ B" .
  interpret alt2: abstract_closure_twice A' B' C "{d}" P A B 
    by (rule alt.shift_closure[OF a], insert ad, simp add: ac_simps)
  from alt2.A_steps_imp_B_steps[OF _ db] have db': "(d,b) ∈ B'*" by simp
  from ac' cd' db' show ?thesis by blast
qed

lemma AA_steps_imp_BB_steps: assumes a: "a ∈ S"
  and steps: "(a,b) ∈ (relto A A')^^n" shows "(a,b) ∈ (relto B B')^^n"
  using steps
proof (induct n arbitrary: b)
  case (Suc n c)
  from Suc(2) obtain b where ab: "(a,b) ∈ (relto A A')^^n" and bc: "(b,c) ∈ relto A A'" by auto
  from Suc(1)[OF ab] have ab': "(a,b) ∈ (relto B B')^^n" by auto
  from relpow_imp_rtrancl[OF ab] have ab: "(a,b) ∈ (A ∪ A')*" by regexp
  interpret alt: abstract_closure_twice A B C "{b}" P A' B'
    by (rule shift_closure[OF a ab])
  from alt.AA_step_imp_BB_step[OF _ bc] have bc: "(b,c) ∈ relto B B'" by simp
  from ab' bc show ?case by auto
qed simp
end

end