equal
deleted
inserted
replaced
7 |
7 |
8 theory Product_ord |
8 theory Product_ord |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 instance "*" :: (ord,ord) ord .. |
12 instance "*" :: (ord, ord) ord .. |
13 |
13 |
14 defs (overloaded) |
14 defs (overloaded) |
15 prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)" |
15 prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)" |
16 prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" |
16 prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" |
17 |
17 |
18 |
18 |
19 lemmas prod_ord_defs = prod_less_def prod_le_def |
19 lemmas prod_ord_defs = prod_less_def prod_le_def |
20 |
20 |
21 instance "*" :: (order,order) order |
21 instance * :: (order, order) order |
22 apply (intro_classes, unfold prod_ord_defs) |
22 by default (auto simp: prod_ord_defs intro: order_less_trans) |
23 by (auto intro: order_less_trans) |
|
24 |
23 |
25 instance "*":: (linorder,linorder)linorder |
24 instance * :: (linorder, linorder) linorder |
26 by (intro_classes, unfold prod_le_def, auto) |
25 by default (auto simp: prod_le_def) |
27 |
26 |
28 end |
27 end |