# HG changeset patch # User desharna # Date 1671445408 -3600 # Node ID 2f8219460ac9f526434877fa0c4450e4ad327442 # Parent 0fbe27cf295a63c2a7af65d819d2cd488cee858d added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp] diff -r 0fbe27cf295a -r 2f8219460ac9 NEWS --- a/NEWS Mon Dec 19 08:44:18 2022 +0100 +++ b/NEWS Mon Dec 19 11:23:28 2022 +0100 @@ -118,6 +118,8 @@ * Theory "HOL.Wellfounded": - Added lemmas. + irrefl_lex_prod[simp] + irrefl_on_lex_prod[simp] wfP_if_convertible_to_nat wfP_if_convertible_to_wfP wf_if_convertible_to_wf diff -r 0fbe27cf295a -r 2f8219460ac9 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Mon Dec 19 08:44:18 2022 +0100 +++ b/src/HOL/Wellfounded.thy Mon Dec 19 11:23:28 2022 +0100 @@ -849,19 +849,27 @@ by (simp add: zeq) qed auto +lemma irrefl_on_lex_prod[simp]: + "irrefl_on A r\<^sub>A \ irrefl_on B r\<^sub>B \ irrefl_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)" + by (auto intro!: irrefl_onI dest: irrefl_onD) + +lemma irrefl_lex_prod[simp]: "irrefl r\<^sub>A \ irrefl r\<^sub>B \ irrefl (r\<^sub>A <*lex*> r\<^sub>B)" + by (rule irrefl_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) + text \\<*lex*>\ preserves transitivity\ lemma trans_lex_prod [simp,intro!]: "trans R1 \ trans R2 \ trans (R1 <*lex*> R2)" unfolding trans_def lex_prod_def by blast -lemma total_on_lex_prod [simp]: "total_on A r \ total_on B s \ total_on (A \ B) (r <*lex*> s)" +lemma total_on_lex_prod[simp]: + "total_on A r\<^sub>A \ total_on B r\<^sub>B \ total_on (A \ B) (r\<^sub>A <*lex*> r\<^sub>B)" by (auto simp: total_on_def) +lemma total_lex_prod[simp]: "total r\<^sub>A \ total r\<^sub>B \ total (r\<^sub>A <*lex*> r\<^sub>B)" + by (rule total_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV]) + lemma asym_lex_prod: "\asym R; asym S\ \ asym (R <*lex*> S)" by (auto simp add: asym_iff lex_prod_def) -lemma total_lex_prod [simp]: "total r \ total s \ total (r <*lex*> s)" - by (auto simp: total_on_def) - text \lexicographic combinations with measure functions\ definition mlex_prod :: "('a \ nat) \ ('a \ 'a) set \ ('a \ 'a) set" (infixr "<*mlex*>" 80)