src/HOL/Relation.thy
 changeset 52749 ed416f4ac34e parent 52730 6bf02eb4ddf7 child 53680 c5096c22892b
```     1.1 --- a/src/HOL/Relation.thy	Sat Jul 27 22:44:04 2013 +0200
1.2 +++ b/src/HOL/Relation.thy	Sun Jul 28 12:59:59 2013 +0200
1.3 @@ -705,11 +705,23 @@
1.4  lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
1.5    by blast
1.6
1.7 -lemma converse_mono: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
1.8 +lemma converse_mono[simp]: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
1.9 +  by auto
1.10 +
1.11 +lemma conversep_mono[simp]: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
1.12 +  by (fact converse_mono[to_pred])
1.13 +
1.14 +lemma converse_inject[simp]: "r^-1 = s ^-1 \<longleftrightarrow> r = s"
1.15    by auto
1.16
1.17 -lemma conversep_mono: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
1.18 -  by (fact converse_mono[to_pred])
1.19 +lemma conversep_inject[simp]: "r^--1 = s ^--1 \<longleftrightarrow> r = s"
1.20 +  by (fact converse_inject[to_pred])
1.21 +
1.22 +lemma converse_subset_swap: "r \<subseteq> s ^-1 = (r ^-1 \<subseteq> s)"
1.23 +  by auto
1.24 +
1.25 +lemma conversep_le_swap: "r \<le> s ^--1 = (r ^--1 \<le> s)"
1.26 +  by (fact converse_subset_swap[to_pred])
1.27
1.28  lemma converse_Id [simp]: "Id^-1 = Id"
1.29    by blast
1.30 @@ -741,18 +753,8 @@
1.31  lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r"
1.32    by (auto simp: total_on_def)
1.33
1.34 -lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.35 -  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
1.36 -   apply simp
1.37 -   apply (rule iffI)
1.38 -    apply (erule finite_imageD [unfolded inj_on_def])
1.39 -    apply (simp split add: split_split)
1.40 -   apply (erule finite_imageI)
1.41 -  apply (simp add: set_eq_iff image_def, auto)
1.42 -  apply (rule bexI)
1.43 -   prefer 2 apply assumption
1.44 -  apply simp
1.45 -  done
1.46 +lemma finite_converse [iff]: "finite (r^-1) = finite r"
1.47 +  unfolding converse_def conversep_iff by (auto elim: finite_imageD simp: inj_on_def)
1.48
1.49  lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
1.50    by (auto simp add: fun_eq_iff)
1.51 @@ -1075,7 +1077,7 @@
1.52    interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
1.53      by (rule comp_fun_commute_Image_fold)
1.54    have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))"
1.55 -    by (auto intro: rev_ImageI)
1.56 +    by (force intro: rev_ImageI)
1.57    show ?thesis using assms by (induct R) (auto simp: *)
1.58  qed
1.59
1.60 @@ -1119,11 +1121,9 @@
1.61    assumes "finite S"
1.62    shows "R O S = Finite_Set.fold
1.63      (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
1.64 -proof -
1.65 -  show ?thesis using assms by (induct R)
1.66 -    (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
1.67 +  using assms by (induct R)
1.68 +    (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
1.69        cong: if_cong)
1.70 -qed
1.71
1.72
1.73
```