# HG changeset patch
# User haftmann
# Date 1164187218 -3600
# Node ID 475b321982f772d8a4b7b8883378dc3ee0e42cde
# Parent  84a21cf15923dc2bdb40caecb0642cb3a229061f
added code lemmas

diff -r 84a21cf15923 -r 475b321982f7 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Wed Nov 22 10:20:17 2006 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Nov 22 10:20:18 2006 +0100
@@ -9,10 +9,9 @@
 imports Main
 begin
 
-instance list :: (ord) ord ..
-defs (overloaded)
+instance list :: (ord) ord
   list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
-  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}"
+  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
 
 lemmas list_ord_defs = list_less_def list_le_def
 
@@ -28,29 +27,29 @@
   apply assumption
   done
 
-instance list::(linorder)linorder
+instance list :: (linorder) linorder
   apply (intro_classes, unfold list_le_def list_less_def, safe)
   apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    apply force
   apply simp
   done
 
-lemma not_less_Nil[simp]: "~(x < [])"
+lemma not_less_Nil [simp, code func]: "~(x < [])"
   by (unfold list_less_def) simp
 
-lemma Nil_less_Cons[simp]: "[] < a # x"
+lemma Nil_less_Cons [simp, code func]: "[] < a # x"
   by (unfold list_less_def) simp
 
-lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)"
+lemma Cons_less_Cons [simp, code func]: "(a # x < b # y) = (a < b | a = b & x < y)"
   by (unfold list_less_def) simp
 
-lemma le_Nil[simp]: "(x <= []) = (x = [])"
+lemma le_Nil [simp, code func]: "(x <= []) = (x = [])"
   by (unfold list_ord_defs, cases x) auto
 
-lemma Nil_le_Cons [simp]: "([] <= x)"
+lemma Nil_le_Cons [simp, code func]: "([] <= x)"
   by (unfold list_ord_defs, cases x) auto
 
-lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
+lemma Cons_le_Cons [simp, code func]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
   by (unfold list_ord_defs) auto
 
 end
diff -r 84a21cf15923 -r 475b321982f7 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Wed Nov 22 10:20:17 2006 +0100
+++ b/src/HOL/Library/Product_ord.thy	Wed Nov 22 10:20:18 2006 +0100
@@ -9,15 +9,17 @@
 imports Main
 begin
 
-instance "*" :: (ord, ord) ord ..
-
-defs (overloaded)
+instance "*" :: (ord, ord) ord
   prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
-  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
-
+  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" ..
 
 lemmas prod_ord_defs = prod_less_def prod_le_def
 
+lemma [code]:
+  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
+  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+  unfolding prod_ord_defs by simp_all
+
 instance * :: (order, order) order
   by default (auto simp: prod_ord_defs intro: order_less_trans)