# HG changeset patch
# User haftmann
# Date 1291029286 -3600
# Node ID f1fc2a1547eb27f15bbab0d374d962c1edb5244c
# Parent  ff16e22e8776b5ba09baa18ef3b68bf242c0cb09
moved generic definitions about relations from Quotient.thy to Predicate;
more natural deduction rules

diff -r ff16e22e8776 -r f1fc2a1547eb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Nov 29 12:14:43 2010 +0100
+++ b/src/HOL/Predicate.thy	Mon Nov 29 12:14:46 2010 +0100
@@ -363,6 +363,44 @@
 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   "single_valuedP r == single_valued {(x, y). r x y}"
 
+(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
+
+definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
+
+definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
+
+definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
+
+lemma reflpI:
+  "(\<And>x. r x x) \<Longrightarrow> reflp r"
+  by (auto intro: refl_onI simp add: reflp_def)
+
+lemma reflpE:
+  assumes "reflp r"
+  obtains "r x x"
+  using assms by (auto dest: refl_onD simp add: reflp_def)
+
+lemma sympI:
+  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
+  by (auto intro: symI simp add: symp_def)
+
+lemma sympE:
+  assumes "symp r" and "r x y"
+  obtains "r y x"
+  using assms by (auto dest: symD simp add: symp_def)
+
+lemma transpI:
+  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
+  by (auto intro: transI simp add: transp_def)
+  
+lemma transpE:
+  assumes "transp r" and "r x y" and "r y z"
+  obtains "r x z"
+  using assms by (auto dest: transD simp add: transp_def)
+
 
 subsection {* Predicates as enumerations *}