src/HOL/Library/List_Lexorder.thy

--- a/src/HOL/Library/List_Lexorder.thy	Fri Apr 17 17:32:11 2020 +0200
+++ b/src/HOL/Library/List_Lexorder.thy	Fri Apr 17 20:55:53 2020 +0100
@@ -23,47 +23,33 @@
 
 instance list :: (order) order
 proof
-  fix xs :: "'a list"
-  show "xs \<le> xs" by (simp add: list_le_def)
-next
-  fix xs ys zs :: "'a list"
-  assume "xs \<le> ys" and "ys \<le> zs"
-  then show "xs \<le> zs"
-    apply (auto simp add: list_le_def list_less_def)
-    apply (rule lexord_trans)
-    apply (auto intro: transI)
-    done
-next
-  fix xs ys :: "'a list"
-  assume "xs \<le> ys" and "ys \<le> xs"
-  then show "xs = ys"
-    apply (auto simp add: list_le_def list_less_def)
-    apply (rule lexord_irreflexive [THEN notE])
-    defer
-    apply (rule lexord_trans)
-    apply (auto intro: transI)
-    done
-next
-  fix xs ys :: "'a list"
-  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
-    apply (auto simp add: list_less_def list_le_def)
-    defer
-    apply (rule lexord_irreflexive [THEN notE])
-    apply auto
-    apply (rule lexord_irreflexive [THEN notE])
-    defer
-    apply (rule lexord_trans)
-    apply (auto intro: transI)
-    done
+  let ?r = "{(u, v::'a). u < v}"
+  have tr: "trans ?r"
+    using trans_def by fastforce
+  have \<section>: False
+    if "(xs,ys) \<in> lexord ?r" "(ys,xs) \<in> lexord ?r" for xs ys :: "'a list"
+  proof -
+    have "(xs,xs) \<in> lexord ?r"
+      using that transD [OF lexord_transI [OF tr]] by blast
+    then show False
+      by (meson case_prodD lexord_irreflexive less_irrefl mem_Collect_eq)
+  qed
+  show "xs \<le> xs" for xs :: "'a list" by (simp add: list_le_def)
+  show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" for xs ys zs :: "'a list"
+    using that transD [OF lexord_transI [OF tr]] by (auto simp add: list_le_def list_less_def)
+  show "xs = ys" if "xs \<le> ys" "ys \<le> xs" for xs ys :: "'a list"
+    using \<section> that list_le_def list_less_def by blast
+  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
+    by (auto simp add: list_less_def list_le_def dest: \<section>)
 qed
 
 instance list :: (linorder) linorder
 proof
   fix xs ys :: "'a list"
-  have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
-    by (rule lexord_linear) auto
+  have "total (lexord {(u, v::'a). u < v})"
+    by (rule total_lexord) (auto simp: total_on_def)
   then show "xs \<le> ys \<or> ys \<le> xs"
-    by (auto simp add: list_le_def list_less_def)
+    by (auto simp add: total_on_def list_le_def list_less_def)
 qed
 
 instantiation list :: (linorder) distrib_lattice