src/HOL/Library/List_lexord.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 38857 97775f3e8722
child 52729 412c9e0381a1
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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: "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" 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   "(inf \<Colon> 'a list \<Rightarrow> _) = min"
    66 
    67 definition
    68   "(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 instantiation list :: (order) bot
    95 begin
    96 
    97 definition
    98   "bot = []"
    99 
   100 instance proof
   101 qed (simp add: bot_list_def)
   102 
   103 end
   104 
   105 lemma less_list_code [code]:
   106   "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
   107   "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
   108   "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   109   by simp_all
   110 
   111 lemma less_eq_list_code [code]:
   112   "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
   113   "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
   114   "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   115   by simp_all
   116 
   117 end