233 by (auto simp: symp_def fun_eq_iff) |
233 by (auto simp: symp_def fun_eq_iff) |
234 |
234 |
235 lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y" |
235 lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y" |
236 by blast |
236 by blast |
237 |
237 |
|
238 definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
239 where "eq_onp R = (\<lambda>x y. R x \<and> x = y)" |
|
240 |
|
241 lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" |
|
242 unfolding eq_onp_def Grp_def by auto |
|
243 |
|
244 lemma eq_onp_to_eq: "eq_onp P x y \<Longrightarrow> x = y" |
|
245 by (simp add: eq_onp_def) |
|
246 |
|
247 lemma eq_onp_top_eq_eq: "eq_onp top = op =" |
|
248 by (simp add: eq_onp_def) |
|
249 |
|
250 lemma eq_onp_same_args: "eq_onp P x x = P x" |
|
251 using assms by (auto simp add: eq_onp_def) |
|
252 |
|
253 lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x" |
|
254 unfolding eq_onp_def by blast |
|
255 |
|
256 lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))" |
|
257 by auto |
|
258 |
|
259 lemma eq_onp_mono0: "\<forall>x\<in>A. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>x\<in>A. \<forall>y\<in>A. eq_onp P x y \<longrightarrow> eq_onp Q x y" |
|
260 unfolding eq_onp_def by auto |
|
261 |
|
262 lemma eq_onp_True: "eq_onp (\<lambda>_. True) = (op =)" |
|
263 unfolding eq_onp_def by simp |
|
264 |
|
265 lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)" |
|
266 by auto |
|
267 |
238 ML_file "Tools/BNF/bnf_util.ML" |
268 ML_file "Tools/BNF/bnf_util.ML" |
239 ML_file "Tools/BNF/bnf_tactics.ML" |
269 ML_file "Tools/BNF/bnf_tactics.ML" |
240 ML_file "Tools/BNF/bnf_def_tactics.ML" |
270 ML_file "Tools/BNF/bnf_def_tactics.ML" |
241 ML_file "Tools/BNF/bnf_def.ML" |
271 ML_file "Tools/BNF/bnf_def.ML" |
242 |
272 |