author haftmann Wed Nov 22 10:20:18 2006 +0100 (2006-11-22) changeset 21458 475b321982f7 parent 21457 84a21cf15923 child 21459 20c2ddee8bc5
 src/HOL/Library/List_lexord.thy file | annotate | diff | revisions src/HOL/Library/Product_ord.thy file | annotate | diff | revisions
```     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
```
```     2.1 --- a/src/HOL/Library/Product_ord.thy	Wed Nov 22 10:20:17 2006 +0100
2.2 +++ b/src/HOL/Library/Product_ord.thy	Wed Nov 22 10:20:18 2006 +0100
2.3 @@ -9,15 +9,17 @@
2.4  imports Main
2.5  begin
2.6
2.7 -instance "*" :: (ord, ord) ord ..
2.8 -
2.10 +instance "*" :: (ord, ord) ord
2.11    prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
2.12 -  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
2.13 -
2.14 +  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" ..
2.15
2.16  lemmas prod_ord_defs = prod_less_def prod_le_def
2.17
2.18 +lemma [code]:
2.19 +  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
2.20 +  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
2.21 +  unfolding prod_ord_defs by simp_all
2.22 +
2.23  instance * :: (order, order) order
2.24    by default (auto simp: prod_ord_defs intro: order_less_trans)
2.25
```