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