equal
deleted
inserted
replaced
664 by (simp add:override_on_def) |
664 by (simp add:override_on_def) |
665 |
665 |
666 lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a" |
666 lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a" |
667 by (simp add:override_on_def) |
667 by (simp add:override_on_def) |
668 |
668 |
|
669 lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)" |
|
670 unfolding override_on_def by (simp add: fun_eq_iff) |
|
671 |
|
672 lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)" |
|
673 unfolding override_on_def by (simp add: fun_eq_iff) |
|
674 |
669 |
675 |
670 subsection \<open>\<open>swap\<close>\<close> |
676 subsection \<open>\<open>swap\<close>\<close> |
671 |
677 |
672 definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" |
678 definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" |
673 where "swap a b f = f (a := f b, b:= f a)" |
679 where "swap a b f = f (a := f b, b:= f a)" |