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.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
```