equal
deleted
inserted
replaced
11 |
11 |
12 instance "*" :: (ord, ord) ord |
12 instance "*" :: (ord, ord) ord |
13 prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)" |
13 prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)" |
14 prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" .. |
14 prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" .. |
15 |
15 |
16 lemmas prod_ord_defs [code nofunc] = prod_less_def prod_le_def |
16 lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def |
17 |
17 |
18 lemma [code func]: |
18 lemma [code func]: |
19 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" |
19 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2" |
20 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2" |
20 "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2" |
21 unfolding prod_ord_defs by simp_all |
21 unfolding prod_ord_defs by simp_all |