equal
deleted
inserted
replaced
69 instance proof |
69 instance proof |
70 qed (auto simp add: top_prod_def prod_le_def) |
70 qed (auto simp add: top_prod_def prod_le_def) |
71 |
71 |
72 end |
72 end |
73 |
73 |
|
74 text {* A stronger version of the definition holds for partial orders. *} |
|
75 |
|
76 lemma prod_less_eq: |
|
77 fixes x y :: "'a::order \<times> 'b::ord" |
|
78 shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)" |
|
79 unfolding prod_less_def fst_conv snd_conv le_less by auto |
|
80 |
|
81 instance prod :: (wellorder, wellorder) wellorder |
|
82 proof |
|
83 fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b" |
|
84 assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" |
|
85 show "P z" |
|
86 proof (induct z) |
|
87 case (Pair a b) |
|
88 show "P (a, b)" |
|
89 apply (induct a arbitrary: b rule: less_induct) |
|
90 apply (rule less_induct [where 'a='b]) |
|
91 apply (rule P) |
|
92 apply (auto simp add: prod_less_eq) |
|
93 done |
|
94 qed |
|
95 qed |
|
96 |
74 end |
97 end |