src/HOL/Library/List_lexord.thy
author nipkow
Fri Apr 15 14:14:24 2005 +0200 (2005-04-15)
changeset 15737 c7e522520910
child 17200 3a4d03d1a31b
permissions -rw-r--r--
New
     1 (*  Title:      HOL/Library/List_lexord.thy
     2     ID:         $Id$
     3     Author:     Norbert Voelker
     4 *)
     5 
     6 header {* Instantiation of order classes for lexord 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   by assumption
    29 
    30 instance list::(linorder)linorder
    31   apply (intro_classes, unfold list_le_def list_less_def, safe)
    32   apply (cut_tac x="x" and y="y" and  r = "{(a,b). a < b}"  in lexord_linear)
    33   by (force, simp)
    34 
    35 lemma not_less_Nil[simp]: "~(x < [])";
    36   by (unfold list_less_def, simp);
    37 
    38 lemma Nil_less_Cons[simp]: "[] < a # x";
    39   by (unfold list_less_def, simp);
    40 
    41 lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)";
    42   by (unfold list_less_def, simp);
    43 
    44 lemma le_Nil[simp]: "(x <= [])   = (x = [])";
    45   by (unfold list_ord_defs, case_tac x, auto);
    46 
    47 lemma Nil_le_Cons[simp]: "([] <= x)";
    48   by (unfold list_ord_defs, case_tac x, auto);
    49 
    50 lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)";
    51   by (unfold list_ord_defs, auto);
    52 
    53 end