src/HOL/Relation.thy
changeset 56545 8f1e7596deb7
parent 56218 1c3f1f2431f9
child 56742 678a52e676b6
     1.1 --- a/src/HOL/Relation.thy	Sat Apr 12 17:26:27 2014 +0200
     1.2 +++ b/src/HOL/Relation.thy	Sat Apr 12 11:27:36 2014 +0200
     1.3 @@ -211,13 +211,44 @@
     1.4  
     1.5  definition irrefl :: "'a rel \<Rightarrow> bool"
     1.6  where
     1.7 -  "irrefl r \<longleftrightarrow> (\<forall>x. (x, x) \<notin> r)"
     1.8 +  "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)"
     1.9 +
    1.10 +definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    1.11 +where
    1.12 +  "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)"
    1.13 +
    1.14 +lemma irreflp_irrefl_eq [pred_set_conv]:
    1.15 +  "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" 
    1.16 +  by (simp add: irrefl_def irreflp_def)
    1.17 +
    1.18 +lemma irreflI:
    1.19 +  "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R"
    1.20 +  by (simp add: irrefl_def)
    1.21 +
    1.22 +lemma irreflpI:
    1.23 +  "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
    1.24 +  by (fact irreflI [to_pred])
    1.25  
    1.26  lemma irrefl_distinct [code]:
    1.27 -  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
    1.28 +  "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
    1.29    by (auto simp add: irrefl_def)
    1.30  
    1.31  
    1.32 +subsubsection {* Asymmetry *}
    1.33 +
    1.34 +inductive asym :: "'a rel \<Rightarrow> bool"
    1.35 +where
    1.36 +  asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
    1.37 +
    1.38 +inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    1.39 +where
    1.40 +  asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
    1.41 +
    1.42 +lemma asymp_asym_eq [pred_set_conv]:
    1.43 +  "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" 
    1.44 +  by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
    1.45 +
    1.46 +
    1.47  subsubsection {* Symmetry *}
    1.48  
    1.49  definition sym :: "'a rel \<Rightarrow> bool"