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