(* 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet am 2026-11-04)
¤
*© Formatika GbR, Deutschland
