--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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>