equal
deleted
inserted
replaced
1 (* Title: HOL/Library/List_Lenlexorder.thy |
1 (* Title: HOL/Library/List_Lenlexorder.thy |
2 *) |
2 *) |
3 |
3 |
4 section \<open>Lexicographic order on lists\<close> |
4 section \<open>Lexicographic order on lists\<close> |
|
5 |
|
6 text \<open>This version prioritises length and can yield wellorderings\<close> |
5 |
7 |
6 theory List_Lenlexorder |
8 theory List_Lenlexorder |
7 imports Main |
9 imports Main |
8 begin |
10 begin |
9 |
11 |
49 by (rule total_lenlex) (auto simp: total_on_def) |
51 by (rule total_lenlex) (auto simp: total_on_def) |
50 then show "xs \<le> ys \<or> ys \<le> xs" |
52 then show "xs \<le> ys \<or> ys \<le> xs" |
51 by (auto simp add: total_on_def list_le_def list_less_def) |
53 by (auto simp add: total_on_def list_le_def list_less_def) |
52 qed |
54 qed |
53 |
55 |
|
56 instance list :: (wellorder) wellorder |
|
57 proof |
|
58 fix P :: "'a list \<Rightarrow> bool" and a |
|
59 assume "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" |
|
60 then show "P a" |
|
61 unfolding list_less_def by (metis wf_lenlex wf_induct wf_lenlex wf) |
|
62 qed |
|
63 |
54 instantiation list :: (linorder) distrib_lattice |
64 instantiation list :: (linorder) distrib_lattice |
55 begin |
65 begin |
56 |
66 |
57 definition "(inf :: 'a list \<Rightarrow> _) = min" |
67 definition "(inf :: 'a list \<Rightarrow> _) = min" |
58 |
68 |