Theory Auxx.Map_Choice

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2013, 2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2012-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Map_Choice
imports
  Collections.RBTMapImpl
  Collections.RBTSetImpl
  Deriving.RBT_Compare_Order_Impl
begin 

definition ceta_map_of :: "('a × 'b) list ⇒ 'a :: compare_order ⇒ 'b option" where 
  "ceta_map_of ps = rm.α (rm.to_map ps)"

lemma ceta_map_of[simp]: "ceta_map_of ps = map_of ps"
  unfolding ceta_map_of_def rm.correct by simp

fun fun_of_map :: "('a ⇒ 'b option) ⇒ 'b ⇒ ('a ⇒ 'b)" where 
  "fun_of_map m d a = (case m a of Some b ⇒ b | None ⇒ d)"

fun fun_of_map_fun :: "('a ⇒ 'b option) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)" where 
  "fun_of_map_fun m d a = (case m a of Some b ⇒ b | None ⇒ d a)"

definition precompute_fun :: "('a :: compare_order ⇒ 'b) ⇒ 'a list ⇒ 'a ⇒ 'b" where
  "precompute_fun f as = fun_of_map_fun (ceta_map_of (map (λ a. (a,f a)) as)) f"

lemma precompute_fun[simp]: "precompute_fun f as = f"
proof (intro ext)
  fix a
  show "precompute_fun f as a = f a" unfolding precompute_fun_def
    using map_of_SomeD by (force split: option.splits)
qed

fun fun_of_map_fun' :: "('a ⇒ 'b option) ⇒ ('a ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ ('a ⇒ 'c)" where 
  "fun_of_map_fun' m d f a = (case m a of Some b ⇒ f b | None ⇒ d a)"

definition ceta_set_of :: "('a :: compare_order) list ⇒ 'a ⇒ bool" where 
  "ceta_set_of ps ≡ let tree = rs.from_list ps in (λ a. rs.memb a tree)"

lemma ceta_set_of[simp]: "ceta_set_of xs = (λ y. y ∈ set xs)"
  unfolding ceta_set_of_def Let_def
  by (rule ext, simp add: rs.correct)

definition ceta_list_diff :: "('a :: compare_order) list ⇒ 'a list ⇒ 'a list" where 
  "ceta_list_diff xs ys ≡ rs.to_list (foldl (λ a b. rs.delete b a) (rs.from_list xs) ys)"

lemma ceta_list_diff[simp]: "set (ceta_list_diff xs ys) = set xs - set ys" 
proof -
  {
    fix xs
    have "rs.α (foldl (λ a b. rs.delete b a) xs ys) = rs.α xs - set ys"
    proof (induct ys arbitrary: xs)
      case (Cons y ys)
      show ?case unfolding foldl.simps o_def
        unfolding Cons by (auto simp: rs.correct)
    qed simp
  } note main = this
  have id: "⋀ xs. set (rs.to_list xs) = rs.α xs" by (simp add: rs.correct)
  show ?thesis
    unfolding ceta_list_diff_def
    unfolding id
    unfolding main
    by (simp add: rs.correct)
qed

end