1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory LexordList imports
8  Main
9  Eisbach_Methods (* for tests *)
10begin
11
12text \<open>
13  Wrapper for lexicographic string comparisons.
14  We need this to define search trees with string keys, etc.
15
16  This is mostly copied from HOL/Library/List_lexord, but we add
17  the wrapper type lexord_list to avoid clashing with the existing
18  prefix ordering on lists (HOL/Library/Prefix_Order).
19\<close>
20
21datatype 'a lexord_list = lexord_list "'a list"
22primrec dest_lexord_list where
23  "dest_lexord_list (lexord_list xs) = xs"
24
25instantiation lexord_list :: (ord) ord
26begin
27
28definition
29  lexord_list_less_def: "xs < ys \<longleftrightarrow> (dest_lexord_list xs, dest_lexord_list ys) \<in> lexord {(u, v). u < v}"
30
31definition
32  lexord_list_le_def: "(xs :: _ lexord_list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
33
34instance ..
35
36end
37
38instance lexord_list :: (order) order
39proof
40  fix xs :: "'a lexord_list"
41  show "xs \<le> xs" by (simp add: lexord_list_le_def)
42next
43  fix xs ys zs :: "'a lexord_list"
44  assume "xs \<le> ys" and "ys \<le> zs"
45  then show "xs \<le> zs"
46    apply (auto simp add: lexord_list_le_def lexord_list_less_def)
47    apply (rule lexord_trans)
48    apply (auto intro: transI)
49    done
50next
51  fix xs ys :: "'a lexord_list"
52  assume "xs \<le> ys" and "ys \<le> xs"
53  then show "xs = ys"
54    apply (auto simp add: lexord_list_le_def lexord_list_less_def)
55    apply (rule lexord_irreflexive [THEN notE])
56    defer
57    apply (rule lexord_trans)
58    apply (auto intro: transI)
59    done
60next
61  fix xs ys :: "'a lexord_list"
62  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
63    apply (auto simp add: lexord_list_less_def lexord_list_le_def)
64    defer
65    apply (rule lexord_irreflexive [THEN notE])
66    apply auto
67    apply (rule lexord_irreflexive [THEN notE])
68    defer
69    apply (rule lexord_trans)
70    apply (auto intro: transI)
71    done
72qed
73
74instance lexord_list :: (linorder) linorder
75proof
76  fix xs ys :: "'a lexord_list"
77  have "(dest_lexord_list xs, dest_lexord_list ys) \<in> lexord {(u, v). u < v} \<or>
78        dest_lexord_list xs = dest_lexord_list ys \<or>
79        (dest_lexord_list ys, dest_lexord_list xs) \<in> lexord {(u, v). u < v}"
80    by (rule lexord_linear) auto
81  then show "xs \<le> ys \<or> ys \<le> xs"
82    apply (case_tac xs)
83    apply (case_tac ys)
84    apply (auto simp add: lexord_list_le_def lexord_list_less_def)
85    done
86qed
87
88instantiation lexord_list :: (linorder) distrib_lattice
89begin
90
91definition inf_lexord_list_def: "(inf :: 'a lexord_list \<Rightarrow> _) = min"
92
93definition sup_lexord_list_def: "(sup :: 'a lexord_list \<Rightarrow> _) = max"
94
95instance
96  by standard (auto simp add: inf_lexord_list_def sup_lexord_list_def max_min_distrib2)
97
98end
99
100lemma lexord_not_less_Nil [simp]: "\<not> x < lexord_list []"
101  by (simp add: lexord_list_less_def)
102
103lemma lexord_Nil_less_Cons [simp]: "lexord_list [] < lexord_list (a # x)"
104  by (simp add: lexord_list_less_def)
105
106lemma lexord_Cons_less_Cons [simp]: "lexord_list (a # x) < lexord_list (b # y) \<longleftrightarrow> a < b \<or> a = b \<and> lexord_list x < lexord_list y"
107  by (simp add: lexord_list_less_def)
108
109lemma lexord_le_Nil [simp]: "x \<le> lexord_list [] \<longleftrightarrow> x = lexord_list []"
110  unfolding lexord_list_le_def by (cases x) auto
111
112lemma lexord_Nil_le_Cons [simp]: "lexord_list [] \<le> x"
113  unfolding lexord_list_le_def
114  apply (cases x, rename_tac x', case_tac x')
115  by auto
116
117lemma lexord_Cons_le_Cons [simp]: "lexord_list (a # x) \<le> lexord_list (b # y) \<longleftrightarrow> a < b \<or> a = b \<and> lexord_list x \<le> lexord_list y"
118  unfolding lexord_list_le_def by auto
119
120instantiation lexord_list :: (order) order_bot
121begin
122
123definition bot_lexord_list_def: "bot = lexord_list []"
124
125instance
126  by standard (simp add: bot_lexord_list_def)
127
128end
129
130lemma lexord_less_list_code [code]:
131  "xs < lexord_list ([]::'a::{equal, order} list) \<longleftrightarrow> False"
132  "lexord_list [] < lexord_list ((x::'a::{equal, order}) # xs') \<longleftrightarrow> True"
133  "lexord_list ((x::'a::{equal, order}) # xs') < lexord_list (y # ys') \<longleftrightarrow> x < y \<or> x = y \<and> lexord_list xs' < lexord_list ys'"
134  by simp_all
135
136lemma lexord_less_eq_list_code [code]:
137  "lexord_list (x # xs') \<le> lexord_list ([]::'a::{equal, order} list) \<longleftrightarrow> False"
138  "lexord_list [] \<le> (xs::'a::{equal, order} lexord_list) \<longleftrightarrow> True"
139  "lexord_list ((x::'a::{equal, order}) # xs') \<le> lexord_list (y # ys') \<longleftrightarrow> x < y \<or> x = y \<and> lexord_list xs' \<le> lexord_list ys'"
140  by simp_all
141
142text \<open>
143  Some basic tests.
144\<close>
145experiment begin
146  value "lexord_list [1, 2, 3, 4] < lexord_list [1, 2, 3, 5 :: int]"
147
148  lemma "lexord_list [1, 2, 3, 4] < lexord_list [1, 2, 3, 5 :: int]"
149    by simp
150  lemma "\<not> (lexord_list [1, 2, 3, 5] < lexord_list [1, 2, 3, 4, 5 :: int])"
151    by simp
152  lemma "lexord_list [1, 2, 3, 4] \<le> lexord_list [1, 2, 3, 5 :: int]"
153    by simp
154end
155
156text \<open>
157  Minimal simpset for efficient lexord_list evaluation.
158\<close>
159
160lemmas lexord_list_simps =
161  simp_thms
162  lexord_list.inject list.distinct list.inject \<comment> \<open>eq\<close>
163  lexord_not_less_Nil lexord_Nil_less_Cons lexord_Cons_less_Cons \<comment> \<open>less\<close>
164  lexord_le_Nil lexord_Nil_le_Cons lexord_Cons_le_Cons \<comment> \<open>le\<close>
165
166experiment begin
167  lemma "lexord_list [1, 2, 3] < lexord_list [1, 3 :: nat]"
168    apply (fails \<open>solves \<open>simp only: lexord_list_simps\<close>\<close>)
169    apply (fails \<open>solves \<open>simp only: rel_simps\<close>\<close>)
170    by (simp only: lexord_list_simps rel_simps)
171
172  lemma "lexord_list [1, 2, 3] \<le> lexord_list [1, 3 :: nat]"
173    apply (fails \<open>solves \<open>simp only: lexord_list_simps\<close>\<close>)
174    apply (fails \<open>solves \<open>simp only: rel_simps\<close>\<close>)
175    by (simp only: lexord_list_simps rel_simps)
176
177  lemma "lexord_list [1, 2, 3] \<le> lexord_list [1, 2, 3 :: nat]"
178    by (simp only: lexord_list_simps)
179
180  lemma "\<not> (lexord_list [1, 2, 3] < lexord_list [1, 2, 3 :: nat])"
181    by (simp only: lexord_list_simps rel_simps)
182end
183
184
185end
186