prefer [simp] over [iff] as [iff] break HOL-UNITY
authorAndreas Lochbihler
Fri Jul 29 12:44:22 2016 +0200 (2016-07-29)
changeset 635630bcd79da075b
parent 63562 6f7a9d48a828
child 63564 eca71be9c948
prefer [simp] over [iff] as [iff] break HOL-UNITY
src/HOL/Order_Relation.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Order_Relation.thy	Fri Jul 29 11:42:13 2016 +0200
     1.2 +++ b/src/HOL/Order_Relation.thy	Fri Jul 29 12:44:22 2016 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
     1.5  by(simp add: order_on_defs trans_diff_Id)
     1.6  
     1.7 -lemma linear_order_on_singleton [iff]: "linear_order_on {x} {(x, x)}"
     1.8 +lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
     1.9  unfolding order_on_defs by simp
    1.10  
    1.11  lemma linear_order_on_acyclic:
     2.1 --- a/src/HOL/Relation.thy	Fri Jul 29 11:42:13 2016 +0200
     2.2 +++ b/src/HOL/Relation.thy	Fri Jul 29 12:44:22 2016 +0200
     2.3 @@ -206,7 +206,7 @@
     2.4  lemma refl_on_empty [simp]: "refl_on {} {}"
     2.5    by (simp add: refl_on_def)
     2.6  
     2.7 -lemma refl_on_singleton [iff]: "refl_on {x} {(x, x)}"
     2.8 +lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
     2.9  by (blast intro: refl_onI)
    2.10  
    2.11  lemma refl_on_def' [nitpick_unfold, code]:
    2.12 @@ -338,7 +338,7 @@
    2.13  lemma antisymP_equality [simp]: "antisymP op ="
    2.14    by (auto intro: antisymI)
    2.15  
    2.16 -lemma antisym_singleton [iff]: "antisym {x}"
    2.17 +lemma antisym_singleton [simp]: "antisym {x}"
    2.18  by (blast intro: antisymI)
    2.19  
    2.20  
    2.21 @@ -399,16 +399,16 @@
    2.22  lemma transp_equality [simp]: "transp op ="
    2.23    by (auto intro: transpI)
    2.24  
    2.25 -lemma trans_empty [iff]: "trans {}"
    2.26 +lemma trans_empty [simp]: "trans {}"
    2.27  by (blast intro: transI)
    2.28  
    2.29 -lemma transp_empty [iff]: "transp (\<lambda>x y. False)"
    2.30 +lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
    2.31  using trans_empty[to_pred] by(simp add: bot_fun_def)
    2.32  
    2.33 -lemma trans_singleton [iff]: "trans {(a, a)}"
    2.34 +lemma trans_singleton [simp]: "trans {(a, a)}"
    2.35  by (blast intro: transI)
    2.36  
    2.37 -lemma transp_singleton [iff]: "transp (\<lambda>x y. x = a \<and> y = a)"
    2.38 +lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
    2.39  by(simp add: transp_def)
    2.40  
    2.41  subsubsection \<open>Totality\<close>
    2.42 @@ -425,7 +425,7 @@
    2.43  lemma total_on_empty [simp]: "total_on {} r"
    2.44    by (simp add: total_on_def)
    2.45  
    2.46 -lemma total_on_singleton [iff]: "total_on {x} {(x, x)}"
    2.47 +lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
    2.48  unfolding total_on_def by blast
    2.49  
    2.50  subsubsection \<open>Single valued relations\<close>
    2.51 @@ -931,7 +931,7 @@
    2.52  lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}"
    2.53    by blast
    2.54  
    2.55 -lemma Field_square [iff]: "Field (x \<times> x) = x"
    2.56 +lemma Field_square [simp]: "Field (x \<times> x) = x"
    2.57  unfolding Field_def by blast
    2.58  
    2.59