Theory Higher_Order_Terms.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 xs⇩1 xs⇩2 where "xs = xs⇩1 @ xs⇩2" "n = length xs⇩2" "0 < length xs⇩1"
proof
  let ?xs⇩1 = "take (length xs - n) xs"
  let ?xs⇩2 = "drop (length xs - n) xs"

  show "xs = ?xs⇩1 @ ?xs⇩2"
    by simp
  show "n = length ?xs⇩2" "0 < length ?xs⇩1"
    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