src/HOL/Relation.thy
changeset 63563 0bcd79da075b
parent 63561 fba08009ff3e
child 63612 7195acc2fe93
     1.1 --- a/src/HOL/Relation.thy	Fri Jul 29 11:42:13 2016 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri Jul 29 12:44:22 2016 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4  lemma refl_on_empty [simp]: "refl_on {} {}"
     1.5    by (simp add: refl_on_def)
     1.6  
     1.7 -lemma refl_on_singleton [iff]: "refl_on {x} {(x, x)}"
     1.8 +lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
     1.9  by (blast intro: refl_onI)
    1.10  
    1.11  lemma refl_on_def' [nitpick_unfold, code]:
    1.12 @@ -338,7 +338,7 @@
    1.13  lemma antisymP_equality [simp]: "antisymP op ="
    1.14    by (auto intro: antisymI)
    1.15  
    1.16 -lemma antisym_singleton [iff]: "antisym {x}"
    1.17 +lemma antisym_singleton [simp]: "antisym {x}"
    1.18  by (blast intro: antisymI)
    1.19  
    1.20  
    1.21 @@ -399,16 +399,16 @@
    1.22  lemma transp_equality [simp]: "transp op ="
    1.23    by (auto intro: transpI)
    1.24  
    1.25 -lemma trans_empty [iff]: "trans {}"
    1.26 +lemma trans_empty [simp]: "trans {}"
    1.27  by (blast intro: transI)
    1.28  
    1.29 -lemma transp_empty [iff]: "transp (\<lambda>x y. False)"
    1.30 +lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
    1.31  using trans_empty[to_pred] by(simp add: bot_fun_def)
    1.32  
    1.33 -lemma trans_singleton [iff]: "trans {(a, a)}"
    1.34 +lemma trans_singleton [simp]: "trans {(a, a)}"
    1.35  by (blast intro: transI)
    1.36  
    1.37 -lemma transp_singleton [iff]: "transp (\<lambda>x y. x = a \<and> y = a)"
    1.38 +lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
    1.39  by(simp add: transp_def)
    1.40  
    1.41  subsubsection \<open>Totality\<close>
    1.42 @@ -425,7 +425,7 @@
    1.43  lemma total_on_empty [simp]: "total_on {} r"
    1.44    by (simp add: total_on_def)
    1.45  
    1.46 -lemma total_on_singleton [iff]: "total_on {x} {(x, x)}"
    1.47 +lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
    1.48  unfolding total_on_def by blast
    1.49  
    1.50  subsubsection \<open>Single valued relations\<close>
    1.51 @@ -931,7 +931,7 @@
    1.52  lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}"
    1.53    by blast
    1.54  
    1.55 -lemma Field_square [iff]: "Field (x \<times> x) = x"
    1.56 +lemma Field_square [simp]: "Field (x \<times> x) = x"
    1.57  unfolding Field_def by blast
    1.58  
    1.59