src/HOL/Fun.thy
 changeset 44744 bdf8eb8f126b parent 44277 bcb696533579 child 44860 56101fa00193
equal 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)"`