src/HOL/Library/List_lexord.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 61076 bdc1e2f0a86a
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/List_lexord.thy
     2     Author:     Norbert Voelker
     3 *)
     4 
     5 section \<open>Lexicographic order on lists\<close>
     6 
     7 theory List_lexord
     8 imports Main
     9 begin
    10 
    11 instantiation list :: (ord) ord
    12 begin
    13 
    14 definition
    15   list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
    16 
    17 definition
    18   list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
    19 
    20 instance ..
    21 
    22 end
    23 
    24 instance list :: (order) order
    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"
    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
    36 next
    37   fix xs ys :: "'a list"
    38   assume "xs \<le> ys" and "ys \<le> xs"
    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
    46 next
    47   fix xs ys :: "'a list"
    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
    58 qed
    59 
    60 instance list :: (linorder) linorder
    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
    65   then show "xs \<le> ys \<or> ys \<le> xs"
    66     by (auto simp add: list_le_def list_less_def)
    67 qed
    68 
    69 instantiation list :: (linorder) distrib_lattice
    70 begin
    71 
    72 definition "(inf :: 'a list \<Rightarrow> _) = min"
    73 
    74 definition "(sup :: 'a list \<Rightarrow> _) = max"
    75 
    76 instance
    77   by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
    78 
    79 end
    80 
    81 lemma not_less_Nil [simp]: "\<not> x < []"
    82   by (simp add: list_less_def)
    83 
    84 lemma Nil_less_Cons [simp]: "[] < a # x"
    85   by (simp add: list_less_def)
    86 
    87 lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
    88   by (simp add: list_less_def)
    89 
    90 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
    91   unfolding list_le_def by (cases x) auto
    92 
    93 lemma Nil_le_Cons [simp]: "[] \<le> x"
    94   unfolding list_le_def by (cases x) auto
    95 
    96 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    97   unfolding list_le_def by auto
    98 
    99 instantiation list :: (order) order_bot
   100 begin
   101 
   102 definition "bot = []"
   103 
   104 instance
   105   by standard (simp add: bot_list_def)
   106 
   107 end
   108 
   109 lemma less_list_code [code]:
   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"
   113   by simp_all
   114 
   115 lemma less_eq_list_code [code]:
   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"
   119   by simp_all
   120 
   121 end