# HG changeset patch # User desharna # Date 1671182032 -3600 # Node ID 99d6e9217586d2351bf97aa82b83bb5f13fb60f2 # Parent f8826fc8c4191cafa8cc8100596bddba7bafc62e added predicates sym_on and symp_on and redefined sym and symp to be abbreviations diff -r f8826fc8c419 -r 99d6e9217586 NEWS --- a/NEWS Fri Dec 16 09:55:22 2022 +0100 +++ b/NEWS Fri Dec 16 10:13:52 2022 +0100 @@ -30,6 +30,10 @@ irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are explicitly provided for backward compatibility but their usage is discouraged. Minor INCOMPATIBILITY. + - Added predicates sym_on and symp_on and redefined sym and + symp to be abbreviations. Lemmas sym_def and symp_def are explicitly + provided for backward compatibility but their usage is discouraged. + Minor INCOMPATIBILITY. - Added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are explicitly provided for backward compatibility but their usage is diff -r f8826fc8c419 -r 99d6e9217586 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Fri Dec 16 09:55:22 2022 +0100 +++ b/src/HOL/Relation.thy Fri Dec 16 10:13:52 2022 +0100 @@ -361,11 +361,25 @@ subsubsection \Symmetry\ -definition sym :: "'a rel \ bool" - where "sym r \ (\x y. (x, y) \ r \ (y, x) \ r)" +definition sym_on :: "'a set \ 'a rel \ bool" where + "sym_on A r \ (\x \ A. \y \ A. (x, y) \ r \ (y, x) \ r)" + +abbreviation sym :: "'a rel \ bool" where + "sym \ sym_on UNIV" + +definition symp_on :: "'a set \ ('a \ 'a \ bool) \ bool" where + "symp_on A R \ (\x \ A. \y \ A. R x y \ R y x)" -definition symp :: "('a \ 'a \ bool) \ bool" - where "symp r \ (\x y. r x y \ r y x)" +abbreviation symp :: "('a \ 'a \ bool) \ bool" where + "symp \ symp_on UNIV" + +lemma sym_def[no_atp]: "sym r \ (\x y. (x, y) \ r \ (y, x) \ r)" + by (simp add: sym_on_def) + +lemma symp_def[no_atp]: "symp R \ (\x y. R x y \ R y x)" + by (simp add: symp_on_def) + +text \@{thm [source] sym_def} and @{thm [source] symp_def} are for backward compatibility.\ lemma symp_sym_eq [pred_set_conv]: "symp (\x y. (x, y) \ r) \ sym r" by (simp add: sym_def symp_def) diff -r f8826fc8c419 -r 99d6e9217586 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 16 09:55:22 2022 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 16 10:13:52 2022 +0100 @@ -399,7 +399,7 @@ fun mk_pred name R = Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R; val mk_reflp = mk_pred \<^const_abbrev>\reflp\; -val mk_symp = mk_pred \<^const_name>\symp\; +val mk_symp = mk_pred \<^const_abbrev>\symp\; val mk_transp = mk_pred \<^const_name>\transp\; fun mk_trans thm1 thm2 = trans OF [thm1, thm2];