--- a/src/HOL/List.thy Thu Jun 11 14:18:34 2020 +0200
+++ b/src/HOL/List.thy Thu Jun 11 16:13:53 2020 +0100
@@ -6326,7 +6326,6 @@
by (metis DomainE Int_emptyI RangeE lexn_length)
qed
-
lemma lexn_conv:
"lexn r n =
{(xs,ys). length xs = n \<and> length ys = n \<and>
@@ -6516,7 +6515,6 @@
by (meson irrefl_def lex_take_index)
-
subsubsection \<open>Lexicographic Ordering\<close>
text \<open>Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
@@ -6618,11 +6616,11 @@
qed
lemma lexord_trans:
- "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
-by(auto simp: trans_def intro:lexord_partial_trans)
+ "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
+ by(auto simp: trans_def intro:lexord_partial_trans)
lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
-by (rule transI, drule lexord_trans, blast)
+ by (meson lexord_trans transI)
lemma total_lexord: "total r \<Longrightarrow> total (lexord r)"
unfolding total_on_def
@@ -6653,10 +6651,7 @@
lemma lexord_asym:
assumes "asym R"
shows "asym (lexord R)"
-proof
- from assms obtain "irrefl R" by (blast elim: asym.cases)
- then show "irrefl (lexord R)" by (rule lexord_irrefl)
-next
+proof
fix xs ys
assume "(xs, ys) \<in> lexord R"
then show "(ys, xs) \<notin> lexord R"
@@ -6679,6 +6674,38 @@
then show ?thesis by (rule asym.cases) (auto simp add: hyp)
qed
+lemma asym_lex: "asym R \<Longrightarrow> asym (lex R)"
+ by (meson asym.simps 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)
+
+lemma lenlex_append1:
+ assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys"
+ shows "(us @ vs, xs @ ys) \<in> lenlex R"
+ using len
+proof (induction us)
+ case Nil
+ then show ?case
+ by (simp add: lenlex_def eq)
+next
+ case (Cons u us)
+ with lex_append_rightI show ?case
+ by (fastforce simp add: lenlex_def eq)
+qed
+
+lemma lenlex_append2 [simp]:
+ assumes "irrefl R"
+ shows "(us @ xs, us @ ys) \<in> lenlex R \<longleftrightarrow> (xs, ys) \<in> lenlex R"
+proof (induction us)
+ case Nil
+ then show ?case
+ by (simp add: lenlex_def)
+next
+ case (Cons u us)
+ with assms show ?case
+ by (auto simp: lenlex_def irrefl_def)
+qed
text \<open>
Predicate version of lexicographic order integrated with Isabelle's order type classes.
--- a/src/HOL/Relation.thy Thu Jun 11 14:18:34 2020 +0200
+++ b/src/HOL/Relation.thy Thu Jun 11 16:13:53 2020 +0100
@@ -245,14 +245,19 @@
subsubsection \<open>Asymmetry\<close>
inductive asym :: "'a rel \<Rightarrow> bool"
- where asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
+ where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
+ where asympI: "(\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
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 asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
+ by (simp add: asym.simps)
+
+lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
+ by (blast intro: asymI dest: asymD)
subsubsection \<open>Symmetry\<close>
@@ -1136,6 +1141,9 @@
lemma total_inv_image: "\<lbrakk>inj f; total r\<rbrakk> \<Longrightarrow> total (inv_image r f)"
unfolding inv_image_def total_on_def by (auto simp: inj_eq)
+lemma asym_inv_image: "asym R \<Longrightarrow> asym (inv_image R f)"
+ by (simp add: inv_image_def asym_iff)
+
lemma in_inv_image[simp]: "(x, y) \<in> inv_image r f \<longleftrightarrow> (f x, f y) \<in> r"
by (auto simp: inv_image_def)
--- a/src/HOL/Wellfounded.thy Thu Jun 11 14:18:34 2020 +0200
+++ b/src/HOL/Wellfounded.thy Thu Jun 11 16:13:53 2020 +0100
@@ -583,6 +583,9 @@
lemma irrefl_less_than: "irrefl less_than"
using irrefl_def by blast
+lemma asym_less_than: "asym less_than"
+ by (simp add: asym.simps irrefl_less_than)
+
lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
using total_on_def by force+
@@ -798,6 +801,9 @@
lemma total_on_lex_prod [simp]: "total_on A r \<Longrightarrow> total_on B s \<Longrightarrow> total_on (A \<times> B) (r <*lex*> s)"
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)