src/HOL/Library/List_lexord.thy
author wenzelm
Wed Aug 31 15:46:37 2005 +0200 (2005-08-31)
changeset 17200 3a4d03d1a31b
parent 15737 c7e522520910
child 21458 475b321982f7
permissions -rw-r--r--
tuned presentation;
     1 (*  Title:      HOL/Library/List_lexord.thy
     2     ID:         $Id$
     3     Author:     Norbert Voelker
     4 *)
     5 
     6 header {* Lexicographic order on lists *}
     7 
     8 theory List_lexord
     9 imports Main
    10 begin
    11 
    12 instance list :: (ord) ord ..
    13 defs (overloaded)
    14   list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
    15   list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}"
    16 
    17 lemmas list_ord_defs = list_less_def list_le_def
    18 
    19 instance list :: (order) order
    20   apply (intro_classes, unfold list_ord_defs)
    21      apply (rule disjI2, safe)
    22     apply (blast intro: lexord_trans transI order_less_trans)
    23    apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    24     apply simp
    25    apply (blast intro: lexord_trans transI order_less_trans)
    26   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    27   apply simp
    28   apply assumption
    29   done
    30 
    31 instance list::(linorder)linorder
    32   apply (intro_classes, unfold list_le_def list_less_def, safe)
    33   apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    34    apply force
    35   apply simp
    36   done
    37 
    38 lemma not_less_Nil[simp]: "~(x < [])"
    39   by (unfold list_less_def) simp
    40 
    41 lemma Nil_less_Cons[simp]: "[] < a # x"
    42   by (unfold list_less_def) simp
    43 
    44 lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)"
    45   by (unfold list_less_def) simp
    46 
    47 lemma le_Nil[simp]: "(x <= []) = (x = [])"
    48   by (unfold list_ord_defs, cases x) auto
    49 
    50 lemma Nil_le_Cons [simp]: "([] <= x)"
    51   by (unfold list_ord_defs, cases x) auto
    52 
    53 lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
    54   by (unfold list_ord_defs) auto
    55 
    56 end