src/HOL/Library/List_lexord.thy
changeset 21458 475b321982f7
parent 17200 3a4d03d1a31b
child 22177 515021e98684
     1.1 --- a/src/HOL/Library/List_lexord.thy	Wed Nov 22 10:20:17 2006 +0100
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Wed Nov 22 10:20:18 2006 +0100
     1.3 @@ -9,10 +9,9 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -instance list :: (ord) ord ..
     1.8 -defs (overloaded)
     1.9 +instance list :: (ord) ord
    1.10    list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
    1.11 -  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}"
    1.12 +  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
    1.13  
    1.14  lemmas list_ord_defs = list_less_def list_le_def
    1.15  
    1.16 @@ -28,29 +27,29 @@
    1.17    apply assumption
    1.18    done
    1.19  
    1.20 -instance list::(linorder)linorder
    1.21 +instance list :: (linorder) linorder
    1.22    apply (intro_classes, unfold list_le_def list_less_def, safe)
    1.23    apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    1.24     apply force
    1.25    apply simp
    1.26    done
    1.27  
    1.28 -lemma not_less_Nil[simp]: "~(x < [])"
    1.29 +lemma not_less_Nil [simp, code func]: "~(x < [])"
    1.30    by (unfold list_less_def) simp
    1.31  
    1.32 -lemma Nil_less_Cons[simp]: "[] < a # x"
    1.33 +lemma Nil_less_Cons [simp, code func]: "[] < a # x"
    1.34    by (unfold list_less_def) simp
    1.35  
    1.36 -lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)"
    1.37 +lemma Cons_less_Cons [simp, code func]: "(a # x < b # y) = (a < b | a = b & x < y)"
    1.38    by (unfold list_less_def) simp
    1.39  
    1.40 -lemma le_Nil[simp]: "(x <= []) = (x = [])"
    1.41 +lemma le_Nil [simp, code func]: "(x <= []) = (x = [])"
    1.42    by (unfold list_ord_defs, cases x) auto
    1.43  
    1.44 -lemma Nil_le_Cons [simp]: "([] <= x)"
    1.45 +lemma Nil_le_Cons [simp, code func]: "([] <= x)"
    1.46    by (unfold list_ord_defs, cases x) auto
    1.47  
    1.48 -lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
    1.49 +lemma Cons_le_Cons [simp, code func]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
    1.50    by (unfold list_ord_defs) auto
    1.51  
    1.52  end