nipkow@15737: (* Title: HOL/Library/Product_ord.thy nipkow@15737: ID: $Id$ nipkow@15737: Author: Norbert Voelker nipkow@15737: *) nipkow@15737: nipkow@15737: header {* Instantiation of order classes for product types *} nipkow@15737: nipkow@15737: theory Product_ord nipkow@15737: imports Main nipkow@15737: begin nipkow@15737: nipkow@15737: instance "*" :: (ord,ord) ord .. nipkow@15737: nipkow@15737: defs (overloaded) nipkow@15737: prod_le_def: "(x \ y) \ (fst x < fst y) | (fst x = fst y & snd x \ snd y)" nipkow@15737: prod_less_def: "(x < y) \ (fst x < fst y) | (fst x = fst y & snd x < snd y)" nipkow@15737: nipkow@15737: nipkow@15737: lemmas prod_ord_defs = prod_less_def prod_le_def nipkow@15737: nipkow@15737: instance "*" :: (order,order) order nipkow@15737: apply (intro_classes, unfold prod_ord_defs) nipkow@15737: by (auto intro: order_less_trans) nipkow@15737: nipkow@15737: instance "*":: (linorder,linorder)linorder nipkow@15737: by (intro_classes, unfold prod_le_def, auto) nipkow@15737: nipkow@15737: end