equal
deleted
inserted
replaced
20 instance .. |
20 instance .. |
21 |
21 |
22 end |
22 end |
23 |
23 |
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, equal}, 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, equal}, 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 prod :: (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 |