# HG changeset patch # User desharna # Date 1654350214 -7200 # Node ID e5d88927e0177ea5af39b46810319ab0b15a57b9 # Parent 5cd5f9059f81b744f4d5d92a12bcd36da7d28af1 introduced predicate reflp_on and redefined reflp to be an abbreviation diff -r 5cd5f9059f81 -r e5d88927e017 NEWS --- a/NEWS Tue May 31 20:56:09 2022 +0200 +++ b/NEWS Sat Jun 04 15:43:34 2022 +0200 @@ -40,8 +40,12 @@ * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any longer. INCOMPATIBILITY. -* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to - type class preorder. +* Theory "HOL.Relation": + - Added lemmas asymp_less and asymp_greater to type class preorder. + - Added predicate reflp_on and redefined reflp to ab an abbreviation. + Lemma reflp_def is explicitly provided for backward compatibility + but its usage is discouraged. Minor INCOMPATIBILITY. + - Added lemmas reflp_onI and reflp_onD. * Theory "HOL-Library.Multiset": - Consolidated operation and fact names. diff -r 5cd5f9059f81 -r e5d88927e017 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Tue May 31 20:56:09 2022 +0200 +++ b/src/HOL/Relation.thy Sat Jun 04 15:43:34 2022 +0200 @@ -155,8 +155,16 @@ abbreviation refl :: "'a rel \ bool" \ \reflexivity over a type\ where "refl \ refl_on UNIV" -definition reflp :: "('a \ 'a \ bool) \ bool" - where "reflp r \ (\x. r x x)" +definition reflp_on :: "'a set \ ('a \ 'a \ bool) \ bool" + where "reflp_on A R \ (\x\A. R x x)" + +abbreviation reflp :: "('a \ 'a \ bool) \ bool" + where "reflp \ reflp_on UNIV" + +lemma reflp_def[no_atp]: "reflp R \ (\x. R x x)" + by (simp add: reflp_on_def) + +text \@{thm [source] reflp_def} is for backward compatibility.\ lemma reflp_refl_eq [pred_set_conv]: "reflp (\x y. (x, y) \ r) \ refl r" by (simp add: refl_on_def reflp_def) @@ -164,6 +172,13 @@ lemma refl_onI [intro?]: "r \ A \ A \ (\x. x \ A \ (x, x) \ r) \ refl_on A r" unfolding refl_on_def by (iprover intro!: ballI) +lemma reflp_onI: + "(\x y. x \ A \ R x x) \ reflp_on A R" + by (simp add: reflp_on_def) + +lemma reflpI[intro?]: "(\x. R x x) \ reflp R" + by (rule reflp_onI) + lemma refl_onD: "refl_on A r \ a \ A \ (a, a) \ r" unfolding refl_on_def by blast @@ -173,19 +188,18 @@ lemma refl_onD2: "refl_on A r \ (x, y) \ r \ y \ A" unfolding refl_on_def by blast -lemma reflpI [intro?]: "(\x. r x x) \ reflp r" - by (auto intro: refl_onI simp add: reflp_def) +lemma reflp_onD: + "reflp_on A R \ x \ A \ R x x" + by (simp add: reflp_on_def) + +lemma reflpD[dest?]: "reflp R \ R x x" + by (simp add: reflp_onD) lemma reflpE: assumes "reflp r" obtains "r x x" using assms by (auto dest: refl_onD simp add: reflp_def) -lemma reflpD [dest?]: - assumes "reflp r" - shows "r x x" - using assms by (auto elim: reflpE) - lemma refl_on_Int: "refl_on A r \ refl_on B s \ refl_on (A \ B) (r \ s)" unfolding refl_on_def by blast diff -r 5cd5f9059f81 -r e5d88927e017 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Tue May 31 20:56:09 2022 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Sat Jun 04 15:43:34 2022 +0200 @@ -389,7 +389,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_name>\reflp\; +val mk_reflp = mk_pred \<^const_abbrev>\reflp\; val mk_symp = mk_pred \<^const_name>\symp\; val mk_transp = mk_pred \<^const_name>\transp\; diff -r 5cd5f9059f81 -r e5d88927e017 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue May 31 20:56:09 2022 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sat Jun 04 15:43:34 2022 +0200 @@ -758,7 +758,7 @@ handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." in case reflp_tm of - Const (\<^const_name>\reflp\, _) $ _ => () + \<^Const_>\reflp_on _ for \<^Const>\top_class.top _\ _\ => () | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." end