equal
deleted
inserted
replaced
83 apply (simp add:rel_defs fun_upd_apply) |
83 apply (simp add:rel_defs fun_upd_apply) |
84 done |
84 done |
85 |
85 |
86 definition |
86 definition |
87 \<comment> \<open>Restriction of a relation\<close> |
87 \<comment> \<open>Restriction of a relation\<close> |
88 restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set" (\<open>(_/ | _)\<close> [50, 51] 50) |
88 restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set" |
|
89 (\<open>(\<open>notation=\<open>mixfix relation restriction\<close>\<close>_/ | _)\<close> [50, 51] 50) |
89 where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}" |
90 where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}" |
90 |
91 |
91 text \<open>Rewrite rules for the restriction of a relation\<close> |
92 text \<open>Rewrite rules for the restriction of a relation\<close> |
92 |
93 |
93 lemma restr_identity[simp]: |
94 lemma restr_identity[simp]: |