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