# 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 \ 'a \ bool) \ bool" where + "reflp r \ refl {(x, y). r x y}" + +definition symp :: "('a \ 'a \ bool) \ bool" where + "symp r \ sym {(x, y). r x y}" + +definition transp :: "('a \ 'a \ bool) \ bool" where + "transp r \ trans {(x, y). r x y}" + +lemma reflpI: + "(\x. r x x) \ 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: + "(\x y. r x y \ r y x) \ 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: + "(\x y z. r x y \ r y z \ r x z) \ 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 *}