24 lemma [code]: |
24 lemma [code]: |
25 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2" |
25 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2" |
26 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2" |
26 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2" |
27 unfolding prod_le_def prod_less_def by simp_all |
27 unfolding prod_le_def prod_less_def by simp_all |
28 |
28 |
29 instance * :: (preorder, preorder) preorder proof |
29 instance prod :: (preorder, preorder) preorder proof |
30 qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans) |
30 qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans) |
31 |
31 |
32 instance * :: (order, order) order proof |
32 instance prod :: (order, order) order proof |
33 qed (auto simp add: prod_le_def) |
33 qed (auto simp add: prod_le_def) |
34 |
34 |
35 instance * :: (linorder, linorder) linorder proof |
35 instance prod :: (linorder, linorder) linorder proof |
36 qed (auto simp: prod_le_def) |
36 qed (auto simp: prod_le_def) |
37 |
37 |
38 instantiation * :: (linorder, linorder) distrib_lattice |
38 instantiation prod :: (linorder, linorder) distrib_lattice |
39 begin |
39 begin |
40 |
40 |
41 definition |
41 definition |
42 inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min" |
42 inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min" |
43 |
43 |
47 instance proof |
47 instance proof |
48 qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) |
48 qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1) |
49 |
49 |
50 end |
50 end |
51 |
51 |
52 instantiation * :: (bot, bot) bot |
52 instantiation prod :: (bot, bot) bot |
53 begin |
53 begin |
54 |
54 |
55 definition |
55 definition |
56 bot_prod_def: "bot = (bot, bot)" |
56 bot_prod_def: "bot = (bot, bot)" |
57 |
57 |
58 instance proof |
58 instance proof |
59 qed (auto simp add: bot_prod_def prod_le_def) |
59 qed (auto simp add: bot_prod_def prod_le_def) |
60 |
60 |
61 end |
61 end |
62 |
62 |
63 instantiation * :: (top, top) top |
63 instantiation prod :: (top, top) top |
64 begin |
64 begin |
65 |
65 |
66 definition |
66 definition |
67 top_prod_def: "top = (top, top)" |
67 top_prod_def: "top = (top, top)" |
68 |
68 |