Theory Closure_Set

(*  Title:      Containers/Closure_set.thy
    Author:     Andreas Lochbihler, KIT *)

theory Closure_Set imports Equal begin

section ‹Sets implemented as Closures›

context equal_base begin

definition fun_upd :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ 'a ⇒ 'b"
where fun_upd_apply: "fun_upd f a b a' = (if equal a a' then b else f a')"

end

lemmas [code] = equal_base.fun_upd_apply
lemmas [simp] = equal_base.fun_upd_apply

lemma fun_upd_conv_fun_upd: "equal_base.fun_upd (=) = fun_upd"
by(simp add: fun_eq_iff)

end