equal
deleted
inserted
replaced
986 by blast |
986 by blast |
987 |
987 |
988 lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A" |
988 lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A" |
989 by blast |
989 by blast |
990 |
990 |
991 lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" |
991 lemma refl_on_converse [simp]: "refl_on A (r\<inverse>) = refl_on A r" |
992 by (auto simp: refl_on_def) |
992 by (auto simp: refl_on_def) |
993 |
993 |
994 lemma reflp_on_conversp [simp]: "reflp_on A R\<inverse>\<inverse> \<longleftrightarrow> reflp_on A R" |
994 lemma reflp_on_conversp [simp]: "reflp_on A R\<inverse>\<inverse> \<longleftrightarrow> reflp_on A R" |
995 by (auto simp: reflp_on_def) |
995 by (auto simp: reflp_on_def) |
|
996 |
|
997 lemma irrefl_on_converse [simp]: "irrefl_on A (r\<inverse>) = irrefl_on A r" |
|
998 by (simp add: irrefl_on_def) |
|
999 |
|
1000 lemma irreflp_on_converse [simp]: "irreflp_on A (r\<inverse>\<inverse>) = irreflp_on A r" |
|
1001 by (rule irrefl_on_converse[to_pred]) |
996 |
1002 |
997 lemma sym_converse [simp]: "sym (converse r) = sym r" |
1003 lemma sym_converse [simp]: "sym (converse r) = sym r" |
998 unfolding sym_def by blast |
1004 unfolding sym_def by blast |
999 |
1005 |
1000 lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |
1006 lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |