src/HOL/Fun.thy
changeset 44744 bdf8eb8f126b
parent 44277 bcb696533579
child 44860 56101fa00193
equal deleted inserted replaced
44743:804dfa6d35b6 44744:bdf8eb8f126b
   610 by auto
   610 by auto
   611 
   611 
   612 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   612 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   613 by (auto intro: ext)
   613 by (auto intro: ext)
   614 
   614 
       
   615 lemma UNION_fun_upd:
       
   616   "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
       
   617 by (auto split: if_splits)
       
   618 
   615 
   619 
   616 subsection {* @{text override_on} *}
   620 subsection {* @{text override_on} *}
   617 
   621 
   618 definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
   622 definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
   619   "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
   623   "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"