# 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) \ ys \ (xs < ys \ xs = ys)" - list_less_def: "(xs::('a::ord) list) < ys \ (xs, ys) \ lexord {(u,v). u < v}" + list_less_def: "(xs::('a::ord) list) < ys \ (xs, ys) \ 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 \ y) \ (fst x < fst y) | (fst x = fst y & snd x \ snd y)" - prod_less_def: "(x < y) \ (fst x < fst y) | (fst x = fst y & snd x < snd y)" - + prod_less_def: "(x < y) \ (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) \ (x2, y2) \ x1 < x2 \ x1 = x2 \ y1 \ y2" + "(x1, y1) < (x2, y2) \ x1 < x2 \ x1 = x2 \ y1 < y2" + unfolding prod_ord_defs by simp_all + instance * :: (order, order) order by default (auto simp: prod_ord_defs intro: order_less_trans)