--- a/src/HOL/Library/Product_ord.thy Wed May 23 13:33:35 2012 +0200
+++ b/src/HOL/Library/Product_ord.thy Wed May 23 14:17:32 2012 +0200
@@ -22,30 +22,30 @@
end
lemma [code]:
- "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
- "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+ "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+ "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
unfolding prod_le_def prod_less_def by simp_all
-instance prod :: (preorder, preorder) preorder proof
-qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
+instance prod :: (preorder, preorder) preorder
+ by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
-instance prod :: (order, order) order proof
-qed (auto simp add: prod_le_def)
+instance prod :: (order, order) order
+ by default (auto simp add: prod_le_def)
-instance prod :: (linorder, linorder) linorder proof
-qed (auto simp: prod_le_def)
+instance prod :: (linorder, linorder) linorder
+ by default (auto simp: prod_le_def)
instantiation prod :: (linorder, linorder) distrib_lattice
begin
definition
- inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+ inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
definition
- sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
+ sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
-instance proof
-qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+instance
+ by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
end
@@ -55,8 +55,8 @@
definition
bot_prod_def: "bot = (bot, bot)"
-instance proof
-qed (auto simp add: bot_prod_def prod_le_def)
+instance
+ by default (auto simp add: bot_prod_def prod_le_def)
end
@@ -66,8 +66,8 @@
definition
top_prod_def: "top = (top, top)"
-instance proof
-qed (auto simp add: top_prod_def prod_le_def)
+instance
+ by default (auto simp add: top_prod_def prod_le_def)
end
@@ -86,11 +86,29 @@
proof (induct z)
case (Pair a b)
show "P (a, b)"
- apply (induct a arbitrary: b rule: less_induct)
- apply (rule less_induct [where 'a='b])
- apply (rule P)
- apply (auto simp add: prod_less_eq)
- done
+ proof (induct a arbitrary: b rule: less_induct)
+ case (less a\<^isub>1) note a\<^isub>1 = this
+ show "P (a\<^isub>1, b)"
+ proof (induct b rule: less_induct)
+ case (less b\<^isub>1) note b\<^isub>1 = this
+ show "P (a\<^isub>1, b\<^isub>1)"
+ proof (rule P)
+ fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
+ show "P p"
+ proof (cases "fst p < a\<^isub>1")
+ case True
+ then have "P (fst p, snd p)" by (rule a\<^isub>1)
+ then show ?thesis by simp
+ next
+ case False
+ with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
+ by (simp_all add: prod_less_eq)
+ from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
+ with 1 show ?thesis by simp
+ qed
+ qed
+ qed
+ qed
qed
qed