author  nipkow 
Tue, 29 May 2018 14:05:59 +0200  
changeset 68312  e9b5f25f6712 
parent 61076  src/HOL/Library/List_lexord.thy@bdc1e2f0a86a 
child 71766  1249b998e377 
permissions  rwrr 
68312  1 
(* Title: HOL/Library/List_Lexorder.thy 
15737  2 
Author: Norbert Voelker 
3 
*) 

4 

60500  5 
section \<open>Lexicographic order on lists\<close> 
15737  6 

68312  7 
theory List_Lexorder 
53214  8 
imports Main 
15737  9 
begin 
10 

25764  11 
instantiation list :: (ord) ord 
12 
begin 

13 

14 
definition 

37474  15 
list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}" 
25764  16 

17 
definition 

37474  18 
list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys" 
25764  19 

20 
instance .. 

21 

22 
end 

15737  23 

17200  24 
instance list :: (order) order 
27682  25 
proof 
26 
fix xs :: "'a list" 

27 
show "xs \<le> xs" by (simp add: list_le_def) 

28 
next 

29 
fix xs ys zs :: "'a list" 

30 
assume "xs \<le> ys" and "ys \<le> zs" 

53214  31 
then show "xs \<le> zs" 
32 
apply (auto simp add: list_le_def list_less_def) 

33 
apply (rule lexord_trans) 

34 
apply (auto intro: transI) 

35 
done 

27682  36 
next 
37 
fix xs ys :: "'a list" 

38 
assume "xs \<le> ys" and "ys \<le> xs" 

53214  39 
then show "xs = ys" 
40 
apply (auto simp add: list_le_def list_less_def) 

41 
apply (rule lexord_irreflexive [THEN notE]) 

42 
defer 

43 
apply (rule lexord_trans) 

44 
apply (auto intro: transI) 

45 
done 

27682  46 
next 
47 
fix xs ys :: "'a list" 

53214  48 
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
49 
apply (auto simp add: list_less_def list_le_def) 

50 
defer 

51 
apply (rule lexord_irreflexive [THEN notE]) 

52 
apply auto 

53 
apply (rule lexord_irreflexive [THEN notE]) 

54 
defer 

55 
apply (rule lexord_trans) 

56 
apply (auto intro: transI) 

57 
done 

27682  58 
qed 
15737  59 

21458  60 
instance list :: (linorder) linorder 
27682  61 
proof 
62 
fix xs ys :: "'a list" 

63 
have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}" 

64 
by (rule lexord_linear) auto 

53214  65 
then show "xs \<le> ys \<or> ys \<le> xs" 
27682  66 
by (auto simp add: list_le_def list_less_def) 
67 
qed 

15737  68 

25764  69 
instantiation list :: (linorder) distrib_lattice 
70 
begin 

71 

61076  72 
definition "(inf :: 'a list \<Rightarrow> _) = min" 
25764  73 

61076  74 
definition "(sup :: 'a list \<Rightarrow> _) = max" 
25764  75 

76 
instance 

60679  77 
by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2) 
22483  78 

25764  79 
end 
80 

53214  81 
lemma not_less_Nil [simp]: "\<not> x < []" 
82 
by (simp add: list_less_def) 

15737  83 

22177  84 
lemma Nil_less_Cons [simp]: "[] < a # x" 
53214  85 
by (simp add: list_less_def) 
15737  86 

22177  87 
lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y" 
53214  88 
by (simp add: list_less_def) 
15737  89 

22177  90 
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []" 
53214  91 
unfolding list_le_def by (cases x) auto 
22177  92 

93 
lemma Nil_le_Cons [simp]: "[] \<le> x" 

53214  94 
unfolding list_le_def by (cases x) auto 
15737  95 

22177  96 
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y" 
53214  97 
unfolding list_le_def by auto 
15737  98 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
38857
diff
changeset

99 
instantiation list :: (order) order_bot 
37474  100 
begin 
101 

53214  102 
definition "bot = []" 
37474  103 

53214  104 
instance 
60679  105 
by standard (simp add: bot_list_def) 
37474  106 

107 
end 

108 

109 
lemma less_list_code [code]: 

61076  110 
"xs < ([]::'a::{equal, order} list) \<longleftrightarrow> False" 
111 
"[] < (x::'a::{equal, order}) # xs \<longleftrightarrow> True" 

112 
"(x::'a::{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys" 

22177  113 
by simp_all 
114 

37474  115 
lemma less_eq_list_code [code]: 
61076  116 
"x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False" 
117 
"[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True" 

118 
"(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys" 

22177  119 
by simp_all 
120 

17200  121 
end 