Theory Term_Utils

theory Term_Utils
imports
  "HOL-Library.Finite_Map"
  "HOL-Library.Monad_Syntax"
  "HOL-Library.State_Monad"
begin

fun map2 where
"map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
"map2 _ _ _ = []"

lemma map2_elemE:
  assumes "z  set (map2 f xs ys)"
  obtains x y where "x  set xs" "y  set ys" "z = f x y"
using assms by (induct f xs ys rule: map2.induct) auto

lemma map2_elemE1:
  assumes "length xs = length ys" "x  set xs"
  obtains y where "y  set ys" "f x y  set (map2 f xs ys)"
using assms by (induct xs ys rule: list_induct2) auto

lemma map2_elemE2:
  assumes "length xs = length ys" "y  set ys"
  obtains x where "x  set xs" "f x y  set (map2 f xs ys)"
using assms by (induct xs ys rule: list_induct2) auto

lemma map2_cong[fundef_cong]:
  assumes "xs1 = xs2" "ys1 = ys2"
  assumes fg: "x y. x  set xs1  y  set ys1  f x y = g x y"
  shows "map2 f xs1 ys1 = map2 g xs2 ys2"
proof -
  have "map2 f xs1 ys1 = map2 g xs1 ys1"
    using fg
    by (induction f xs1 ys1 rule: map2.induct) auto
  with assms show ?thesis
    by simp
qed

lemma option_bindE:
  assumes "x  f = Some a"
  obtains x' where "x = Some x'"  "f x' = Some a"
using assms
by (cases x) auto

lemma rel_option_bind[intro]:
  assumes "rel_option R x y" "a b. R a b  rel_option R (f a) (g b)"
  shows "rel_option R (x  f) (y  g)"
using assms(1) proof (cases rule: option.rel_cases)
  case None
  thus ?thesis
    by simp
next
  case (Some a b)
  thus ?thesis
    using assms(2) by simp
qed

lemma list_split:
  assumes "n < length xs"
  obtains xs1 xs2 where "xs = xs1 @ xs2" "n = length xs2" "0 < length xs1"
proof
  let ?xs1 = "take (length xs - n) xs"
  let ?xs2 = "drop (length xs - n) xs"

  show "xs = ?xs1 @ ?xs2"
    by simp
  show "n = length ?xs2" "0 < length ?xs1"
    using assms by auto
qed

context
  includes fset.lifting
begin

lemma ffUnion_alt_def: "x |∈| ffUnion A  fBex A (λX. x |∈| X)"
by transfer blast

lemma funion_image_bind_eq: "ffUnion (f |`| M) = fbind M f"
by transfer auto

lemma fbind_funion: "fbind (M |∪| N) f = fbind M f |∪| fbind N f"
by transfer' auto

lemma ffUnion_least: "fBall A (λX. X |⊆| C)  ffUnion A |⊆| C"
by transfer blast

lemma fbind_iff: "x |∈| fbind S f  (s. x |∈| f s  s |∈| S)"
  by transfer' auto

lemma fBall_pred_weaken: "(x. x |∈| M  P x  Q x)  fBall M P  fBall M Q"
by auto

end

lemma fmmap_fmupd[simp]:
  "fmmap f (fmupd k v m) = fmupd k (f v) (fmmap f m)"
apply (rule fmap_ext)
by auto

definition fmlookup_default :: "('a, 'b) fmap  ('a  'b)  'a  'b" where
"fmlookup_default m f x = (case fmlookup m x of None  f x | Some b  b)"

end