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