src/HOL/Predicate.thy
 changeset 40813 f1fc2a1547eb parent 40674 54dbe6a1c349 child 41075 4bed56dc95fb
```     1.1 --- a/src/HOL/Predicate.thy	Mon Nov 29 12:14:43 2010 +0100
1.2 +++ b/src/HOL/Predicate.thy	Mon Nov 29 12:14:46 2010 +0100
1.3 @@ -363,6 +363,44 @@
1.4  abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
1.5    "single_valuedP r == single_valued {(x, y). r x y}"
1.6
1.7 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
1.8 +
1.9 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.10 +  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
1.11 +
1.12 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.13 +  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
1.14 +
1.15 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
1.16 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
1.17 +
1.18 +lemma reflpI:
1.19 +  "(\<And>x. r x x) \<Longrightarrow> reflp r"
1.20 +  by (auto intro: refl_onI simp add: reflp_def)
1.21 +
1.22 +lemma reflpE:
1.23 +  assumes "reflp r"
1.24 +  obtains "r x x"
1.25 +  using assms by (auto dest: refl_onD simp add: reflp_def)
1.26 +
1.27 +lemma sympI:
1.28 +  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
1.29 +  by (auto intro: symI simp add: symp_def)
1.30 +
1.31 +lemma sympE:
1.32 +  assumes "symp r" and "r x y"
1.33 +  obtains "r y x"
1.34 +  using assms by (auto dest: symD simp add: symp_def)
1.35 +
1.36 +lemma transpI:
1.37 +  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
1.38 +  by (auto intro: transI simp add: transp_def)
1.39 +
1.40 +lemma transpE:
1.41 +  assumes "transp r" and "r x y" and "r y z"
1.42 +  obtains "r x z"
1.43 +  using assms by (auto dest: transD simp add: transp_def)
1.44 +
1.45
1.46  subsection {* Predicates as enumerations *}
1.47
```