# HG changeset patch
# User desharna
# Date 1671455377 -3600
# Node ID 0b5efc6de3858af497e67fe794ce6890338f5f4c
# Parent  8ad17c4669da1ea6a271b6b8ee8b0acd74d083d6# Parent  e65a50f6c2de22030947341855a9e5141b7ec04c
merged

diff -r 8ad17c4669da -r 0b5efc6de385 NEWS
--- a/NEWS	Sun Dec 18 18:30:37 2022 +0100
+++ b/NEWS	Mon Dec 19 14:09:37 2022 +0100
@@ -34,6 +34,8 @@
     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 asym_on and asymp_on and redefined asym and
+    asymp to be abbreviations. 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
@@ -41,22 +43,34 @@
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
       order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
+      preorder.asymp_greater[simp] ~> preorder.asymp_on_greater[simp]
+      preorder.asymp_less[simp] ~> preorder.asymp_on_less[simp]
       preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
       preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
       reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
+      sym_converse[simp] ~> sym_on_converse[simp]
+      antisym_converse[simp] ~> antisym_on_converse[simp]
   - Added lemmas.
-      antisym_if_asymp
       antisym_onD
       antisym_onI
+      antisym_on_if_asymp_on
       antisym_on_subset
-      antisymp_if_asymp
       antisymp_onD
       antisymp_onI
       antisymp_on_antisym_on_eq[pred_set_conv]
+      antisymp_on_conversep[simp]
+      antisymp_on_if_asymp_on
       antisymp_on_subset
-      asym_if_irrefl_and_trans
-      asymp_if_irreflp_and_transp
+      asym_on_iff_irrefl_on_if_trans
+      asym_onD
+      asym_onI
+      asym_on_converse[simp]
+      asymp_on_iff_irreflp_on_if_transp
+      asymp_onD
+      asymp_onI
+      asymp_on_asym_on_eq[pred_set_conv]
+      asymp_on_conversep[simp]
       irreflD
       irrefl_onD
       irrefl_onI
@@ -74,16 +88,19 @@
       linorder.totalp_on_less[simp]
       order.antisymp_ge[simp]
       order.antisymp_le[simp]
-      preorder.antisymp_greater[simp]
-      preorder.antisymp_less[simp]
+      preorder.antisymp_on_greater[simp]
+      preorder.antisymp_on_less[simp]
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
+      reflD
+      reflI
       reflp_on_conversp[simp]
       sym_onD
       sym_onI
       sym_on_subset
       symp_onD
       symp_onI
+      symp_on_conversep[simp]
       symp_on_subset
       symp_on_sym_on_eq[pred_set_conv]
       totalI
@@ -103,6 +120,13 @@
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
+      asym_lex_prod[simp]
+      asym_on_lex_prod[simp]
+      irrefl_lex_prod[simp]
+      irrefl_on_lex_prod[simp]
+      refl_lex_prod[simp]
+      sym_lex_prod[simp]
+      sym_on_lex_prod[simp]
       wfP_if_convertible_to_nat
       wfP_if_convertible_to_wfP
       wf_if_convertible_to_wf
diff -r 8ad17c4669da -r 0b5efc6de385 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Dec 19 14:09:37 2022 +0100
@@ -3403,7 +3403,7 @@
   from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
     *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
   moreover from * [of a] have "a \<notin># K"
-    using \<open>asymp r\<close> by (meson asymp.cases)
+    using \<open>asymp r\<close> by (meson asympD)
   ultimately show thesis by (auto intro: that)
 qed
 
diff -r 8ad17c4669da -r 0b5efc6de385 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Dec 19 14:09:37 2022 +0100
@@ -55,7 +55,7 @@
     using \<open>asymp r\<close> by (auto elim: mult1_lessE)
   from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P"
     using *(4) \<open>asymp r\<close>
-    by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
+    by (metis asympD add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
         count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
   moreover
   { assume "count P a \<le> count M a"
@@ -65,7 +65,7 @@
         by blast
       with * have "count N z \<le> count P z"
         using \<open>asymp r\<close>
-        by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
+        by (metis add_diff_cancel_left' add_mset_add_single asympD diff_diff_add_mset
             diff_single_trivial in_diff_count not_le_imp_less)
       with z have "\<exists>z. r a z \<and> count M z < count P z" by auto
   } note count_a = this
diff -r 8ad17c4669da -r 0b5efc6de385 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/HOL/List.thy	Mon Dec 19 14:09:37 2022 +0100
@@ -6986,7 +6986,7 @@
   next
     case (Cons x xs)
     then obtain z zs where ys: "ys = z # zs" by (cases ys) auto
-    with assms Cons show ?case by (auto elim: asym.cases)
+    with assms Cons show ?case by (auto dest: asymD)
   qed
 qed
 
@@ -6996,11 +6996,11 @@
   shows "(b, a) \<notin> lexord R"
 proof -
   from \<open>asym R\<close> have "asym (lexord R)" by (rule lexord_asym)
-  then show ?thesis by (rule asym.cases) (auto simp add: hyp)
+  then show ?thesis by (auto simp: hyp dest: asymD)
 qed
 
 lemma asym_lex: "asym R \<Longrightarrow> asym (lex R)"
-  by (meson asym.simps irrefl_lex lexord_asym lexord_lex)
+  by (meson asymI asymD irrefl_lex lexord_asym lexord_lex)
 
 lemma asym_lenlex: "asym R \<Longrightarrow> asym (lenlex R)"
   by (simp add: lenlex_def asym_inv_image asym_less_than asym_lex asym_lex_prod)
diff -r 8ad17c4669da -r 0b5efc6de385 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 14:09:37 2022 +0100
@@ -173,6 +173,9 @@
 lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
   unfolding refl_on_def by (iprover intro!: ballI)
 
+lemma reflI: "(\<And>x. (x, x) \<in> r) \<Longrightarrow> refl r"
+  by (auto intro: refl_onI)
+
 lemma reflp_onI:
   "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
   by (simp add: reflp_on_def)
@@ -189,6 +192,9 @@
 lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
   unfolding refl_on_def by blast
 
+lemma reflD: "refl r \<Longrightarrow> (a, a) \<in> r"
+  unfolding refl_on_def by blast
+
 lemma reflp_onD:
   "reflp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> R x x"
   by (simp add: reflp_on_def)
@@ -332,31 +338,66 @@
 lemma (in preorder) irreflp_on_greater[simp]: "irreflp_on A (>)"
   by (simp add: irreflp_onI)
 
+
 subsubsection \<open>Asymmetry\<close>
 
-inductive asym :: "'a rel \<Rightarrow> bool"
-  where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
+definition asym_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "asym_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. (x, y) \<in> r \<longrightarrow> (y, x) \<notin> r)"
+
+abbreviation asym :: "'a rel \<Rightarrow> bool" where
+  "asym \<equiv> asym_on UNIV"
 
-inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where asympI: "(\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
+definition asymp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "asymp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. R x y \<longrightarrow> \<not> R y x)"
+
+abbreviation asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "asymp \<equiv> asymp_on UNIV"
+
+lemma asymp_on_asym_on_eq[pred_set_conv]: "asymp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> asym_on A r"
+  by (simp add: asymp_on_def asym_on_def)
+
+lemmas asymp_asym_eq = asymp_on_asym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
-lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R"
-  by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
+lemma asym_onI[intro]:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r) \<Longrightarrow> asym_on A r"
+  by (simp add: asym_on_def)
+
+lemma asymI[intro]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r) \<Longrightarrow> asym r"
+  by (simp add: asym_onI)
+
+lemma asymp_onI[intro]:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x) \<Longrightarrow> asymp_on A R"
+  by (rule asym_onI[to_pred])
 
-lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
-  by (simp add: asym.simps)
+lemma asympI[intro]: "(\<And>x y. R x y \<Longrightarrow> \<not> R y x) \<Longrightarrow> asymp R"
+  by (rule asymI[to_pred])
+
+lemma asym_onD: "asym_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r"
+  by (simp add: asym_on_def)
+
+lemma asymD: "asym r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r"
+  by (simp add: asym_onD)
+
+lemma asymp_onD: "asymp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
+  by (rule asym_onD[to_pred])
 
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
 
-lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
-  by (blast intro: asymI dest: asymD)
+lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
+  by (blast dest: asymD)
+
+lemma asym_on_subset: "asym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asym_on B r"
+  by (auto simp: asym_on_def)
 
-lemma (in preorder) asymp_less[simp]: "asymp (<)"
-  by (auto intro: asympI dual_order.asym)
+lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
+  by (auto simp: asymp_on_def)
 
-lemma (in preorder) asymp_greater[simp]: "asymp (>)"
-  by (auto intro: asympI dual_order.asym)
+lemma (in preorder) asymp_on_less[simp]: "asymp_on A (<)"
+  by (auto intro: dual_order.asym)
+
+lemma (in preorder) asymp_on_greater[simp]: "asymp_on A (>)"
+  by (auto intro: dual_order.asym)
 
 
 subsubsection \<open>Symmetry\<close>
@@ -541,17 +582,17 @@
   "antisym {x}"
   by (blast intro: antisymI)
 
-lemma antisym_if_asym: "asym r \<Longrightarrow> antisym r"
-  by (auto intro: antisymI elim: asym.cases)
+lemma antisym_on_if_asym_on: "asym_on A r \<Longrightarrow> antisym_on A r"
+  by (auto intro: antisym_onI dest: asym_onD)
 
-lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
-  by (rule antisym_if_asym[to_pred])
+lemma antisymp_on_if_asymp_on: "asymp_on A R \<Longrightarrow> antisymp_on A R"
+  by (rule antisym_on_if_asym_on[to_pred])
 
-lemma (in preorder) antisymp_less[simp]: "antisymp (<)"
-  by (rule antisymp_if_asymp[OF asymp_less])
+lemma (in preorder) antisymp_on_less[simp]: "antisymp_on A (<)"
+  by (rule antisymp_on_if_asymp_on[OF asymp_on_less])
 
-lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
-  by (rule antisymp_if_asymp[OF asymp_greater])
+lemma (in preorder) antisymp_on_greater[simp]: "antisymp_on A (>)"
+  by (rule antisymp_on_if_asymp_on[OF asymp_on_greater])
 
 lemma (in order) antisymp_on_le[simp]: "antisymp_on A (\<le>)"
   by (simp add: antisymp_onI)
@@ -630,11 +671,11 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
-lemma asym_if_irrefl_and_trans: "irrefl R \<Longrightarrow> trans R \<Longrightarrow> asym R"
-  by (auto intro: asymI dest: transD irreflD)
+lemma asym_on_iff_irrefl_on_if_trans: "trans r \<Longrightarrow> asym_on A r \<longleftrightarrow> irrefl_on A r"
+  by (auto intro: irrefl_onI dest: transD asym_onD irrefl_onD)
 
-lemma asymp_if_irreflp_and_transp: "irreflp R \<Longrightarrow> transp R \<Longrightarrow> asymp R"
-  by (rule asym_if_irrefl_and_trans[to_pred])
+lemma asymp_on_iff_irreflp_on_if_transp: "transp R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
+  by (rule asym_on_iff_irrefl_on_if_trans[to_pred])
 
 context preorder
 begin
@@ -1075,11 +1116,23 @@
 lemma irreflp_on_converse [simp]: "irreflp_on A (r\<inverse>\<inverse>) = irreflp_on A r"
   by (rule irrefl_on_converse[to_pred])
 
-lemma sym_converse [simp]: "sym (converse r) = sym r"
-  unfolding sym_def by blast
+lemma sym_on_converse [simp]: "sym_on A (r\<inverse>) = sym_on A r"
+  by (auto intro: sym_onI dest: sym_onD)
+
+lemma symp_on_conversep [simp]: "symp_on A R\<inverse>\<inverse> = symp_on A R"
+  by (rule sym_on_converse[to_pred])
+
+lemma asym_on_converse [simp]: "asym_on A (r\<inverse>) = asym_on A r"
+  by (auto dest: asym_onD)
 
-lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
-  unfolding antisym_def by blast
+lemma asymp_on_conversep [simp]: "asymp_on A R\<inverse>\<inverse> = asymp_on A R"
+  by (rule asym_on_converse[to_pred])
+
+lemma antisym_on_converse [simp]: "antisym_on A (r\<inverse>) = antisym_on A r"
+  by (auto intro: antisym_onI dest: antisym_onD)
+
+lemma antisymp_on_conversep [simp]: "antisymp_on A R\<inverse>\<inverse> = antisymp_on A R"
+  by (rule antisym_on_converse[to_pred])
 
 lemma trans_converse [simp]: "trans (converse r) = trans r"
   unfolding trans_def by blast
diff -r 8ad17c4669da -r 0b5efc6de385 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 19 14:09:37 2022 +0100
@@ -604,7 +604,7 @@
   using irrefl_def by blast
 
 lemma asym_less_than: "asym less_than"
-  by (simp add: asym.simps irrefl_less_than)
+  by (rule asymI) simp
 
 lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
   using total_on_def by force+
@@ -849,18 +849,42 @@
     by (simp add: zeq)
 qed auto
 
+lemma refl_lex_prod[simp]: "refl r\<^sub>B \<Longrightarrow> refl (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: reflI dest: refl_onD)
+
+lemma irrefl_on_lex_prod[simp]:
+  "irrefl_on A r\<^sub>A \<Longrightarrow> irrefl_on B r\<^sub>B \<Longrightarrow> irrefl_on (A \<times> 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 \<Longrightarrow> irrefl r\<^sub>B \<Longrightarrow> irrefl (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule irrefl_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
+
+lemma sym_on_lex_prod[simp]:
+  "sym_on A r\<^sub>A \<Longrightarrow> sym_on B r\<^sub>B \<Longrightarrow> sym_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: sym_onI dest: sym_onD)
+
+lemma sym_lex_prod[simp]:
+  "sym r\<^sub>A \<Longrightarrow> sym r\<^sub>B \<Longrightarrow> sym (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule sym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
+
+lemma asym_on_lex_prod[simp]:
+  "asym_on A r\<^sub>A \<Longrightarrow> asym_on B r\<^sub>B \<Longrightarrow> asym_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (auto intro!: asym_onI dest: asym_onD)
+
+lemma asym_lex_prod[simp]:
+  "asym r\<^sub>A \<Longrightarrow> asym r\<^sub>B \<Longrightarrow> asym (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule asym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
+
 text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
 lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
   unfolding trans_def lex_prod_def by blast
 
-lemma total_on_lex_prod [simp]: "total_on A r \<Longrightarrow> total_on B s \<Longrightarrow> total_on (A \<times> B) (r <*lex*> s)"
+lemma total_on_lex_prod[simp]:
+  "total_on A r\<^sub>A \<Longrightarrow> total_on B r\<^sub>B \<Longrightarrow> total_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
   by (auto simp: total_on_def)
 
-lemma asym_lex_prod: "\<lbrakk>asym R; asym S\<rbrakk> \<Longrightarrow> asym (R <*lex*> S)"
-  by (auto simp add: asym_iff lex_prod_def)
-
-lemma total_lex_prod [simp]: "total r \<Longrightarrow> total s \<Longrightarrow> total (r <*lex*> s)"
-  by (auto simp: total_on_def)
+lemma total_lex_prod[simp]: "total r\<^sub>A \<Longrightarrow> total r\<^sub>B \<Longrightarrow> total (r\<^sub>A <*lex*> r\<^sub>B)"
+  by (rule total_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
 
 text \<open>lexicographic combinations with measure functions\<close>