# HG changeset patch
# User paulson
# Date 1659439166 -3600
# Node ID b93ed38cef8517027de0645aaabe9d094bf6b4eb
# Parent  a480964ea704891c5675d8789e0f91a6055c867b# Parent  f6695e7aff321c0c2b2bab47ca02b75288b5e381
merged

diff -r a480964ea704 -r b93ed38cef85 src/HOL/Library/List_Lenlexorder.thy
--- a/src/HOL/Library/List_Lenlexorder.thy	Tue Aug 02 13:15:59 2022 +0200
+++ b/src/HOL/Library/List_Lenlexorder.thy	Tue Aug 02 12:19:26 2022 +0100
@@ -3,6 +3,8 @@
 
 section \<open>Lexicographic order on lists\<close>
 
+text \<open>This version prioritises length and can yield wellorderings\<close>
+
 theory List_Lenlexorder
 imports Main
 begin
@@ -51,6 +53,14 @@
     by (auto simp add: total_on_def list_le_def list_less_def)
 qed
 
+instance list :: (wellorder) wellorder
+proof
+  fix P :: "'a list \<Rightarrow> bool" and a
+  assume "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" 
+  then show "P a"
+    unfolding list_less_def by (metis wf_lenlex wf_induct wf_lenlex wf)
+qed
+
 instantiation list :: (linorder) distrib_lattice
 begin