src/HOL/Library/List_lexord.thy
author haftmann
Mon Mar 23 08:14:24 2009 +0100 (2009-03-23)
changeset 30663 0b6aff7451b2
parent 28562 4e74209f113e
child 37474 ce943f9edf5e
permissions -rw-r--r--
Main is (Complex_Main) base entry point in library theories
     1 (*  Title:      HOL/Library/List_lexord.thy
     2     Author:     Norbert Voelker
     3 *)
     4 
     5 header {* Lexicographic order on lists *}
     6 
     7 theory List_lexord
     8 imports List Main
     9 begin
    10 
    11 instantiation list :: (ord) ord
    12 begin
    13 
    14 definition
    15   list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
    16 
    17 definition
    18   list_le_def [code del]: "(xs::('a::ord) 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" by (auto simp add: list_le_def list_less_def)
    32     (rule lexord_trans, auto intro: transI)
    33 next
    34   fix xs ys :: "'a list"
    35   assume "xs \<le> ys" and "ys \<le> xs"
    36   then show "xs = ys" apply (auto simp add: list_le_def list_less_def)
    37   apply (rule lexord_irreflexive [THEN notE])
    38   defer
    39   apply (rule lexord_trans) apply (auto intro: transI) done
    40 next
    41   fix xs ys :: "'a list"
    42   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
    43   apply (auto simp add: list_less_def list_le_def)
    44   defer
    45   apply (rule lexord_irreflexive [THEN notE])
    46   apply auto
    47   apply (rule lexord_irreflexive [THEN notE])
    48   defer
    49   apply (rule lexord_trans) apply (auto intro: transI) done
    50 qed
    51 
    52 instance list :: (linorder) linorder
    53 proof
    54   fix xs ys :: "'a list"
    55   have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
    56     by (rule lexord_linear) auto
    57   then show "xs \<le> ys \<or> ys \<le> xs" 
    58     by (auto simp add: list_le_def list_less_def)
    59 qed
    60 
    61 instantiation list :: (linorder) distrib_lattice
    62 begin
    63 
    64 definition
    65   [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    66 
    67 definition
    68   [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    69 
    70 instance
    71   by intro_classes
    72     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
    73 
    74 end
    75 
    76 lemma not_less_Nil [simp]: "\<not> (x < [])"
    77   by (unfold list_less_def) simp
    78 
    79 lemma Nil_less_Cons [simp]: "[] < a # x"
    80   by (unfold list_less_def) simp
    81 
    82 lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
    83   by (unfold list_less_def) simp
    84 
    85 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
    86   by (unfold list_le_def, cases x) auto
    87 
    88 lemma Nil_le_Cons [simp]: "[] \<le> x"
    89   by (unfold list_le_def, cases x) auto
    90 
    91 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    92   by (unfold list_le_def) auto
    93 
    94 lemma less_code [code]:
    95   "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    96   "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
    97   "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
    98   by simp_all
    99 
   100 lemma less_eq_code [code]:
   101   "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   102   "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
   103   "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   104   by simp_all
   105 
   106 end