1.1 --- a/src/HOL/Library/Product_ord.thy Wed May 23 13:33:35 2012 +0200
1.2 +++ b/src/HOL/Library/Product_ord.thy Wed May 23 14:17:32 2012 +0200
1.3 @@ -22,30 +22,30 @@
1.4 end
1.5
1.6 lemma [code]:
1.7 - "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
1.8 - "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
1.9 + "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
1.10 + "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
1.11 unfolding prod_le_def prod_less_def by simp_all
1.12
1.13 -instance prod :: (preorder, preorder) preorder proof
1.14 -qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
1.15 +instance prod :: (preorder, preorder) preorder
1.16 + by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
1.17
1.18 -instance prod :: (order, order) order proof
1.19 -qed (auto simp add: prod_le_def)
1.20 +instance prod :: (order, order) order
1.21 + by default (auto simp add: prod_le_def)
1.22
1.23 -instance prod :: (linorder, linorder) linorder proof
1.24 -qed (auto simp: prod_le_def)
1.25 +instance prod :: (linorder, linorder) linorder
1.26 + by default (auto simp: prod_le_def)
1.27
1.28 instantiation prod :: (linorder, linorder) distrib_lattice
1.29 begin
1.30
1.31 definition
1.32 - inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
1.33 + inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
1.34
1.35 definition
1.36 - sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
1.37 + sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
1.38
1.39 -instance proof
1.40 -qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
1.41 +instance
1.42 + by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
1.43
1.44 end
1.45
1.46 @@ -55,8 +55,8 @@
1.47 definition
1.48 bot_prod_def: "bot = (bot, bot)"
1.49
1.50 -instance proof
1.51 -qed (auto simp add: bot_prod_def prod_le_def)
1.52 +instance
1.53 + by default (auto simp add: bot_prod_def prod_le_def)
1.54
1.55 end
1.56
1.57 @@ -66,8 +66,8 @@
1.58 definition
1.59 top_prod_def: "top = (top, top)"
1.60
1.61 -instance proof
1.62 -qed (auto simp add: top_prod_def prod_le_def)
1.63 +instance
1.64 + by default (auto simp add: top_prod_def prod_le_def)
1.65
1.66 end
1.67
1.68 @@ -86,11 +86,29 @@
1.69 proof (induct z)
1.70 case (Pair a b)
1.71 show "P (a, b)"
1.72 - apply (induct a arbitrary: b rule: less_induct)
1.73 - apply (rule less_induct [where 'a='b])
1.74 - apply (rule P)
1.75 - apply (auto simp add: prod_less_eq)
1.76 - done
1.77 + proof (induct a arbitrary: b rule: less_induct)
1.78 + case (less a\<^isub>1) note a\<^isub>1 = this
1.79 + show "P (a\<^isub>1, b)"
1.80 + proof (induct b rule: less_induct)
1.81 + case (less b\<^isub>1) note b\<^isub>1 = this
1.82 + show "P (a\<^isub>1, b\<^isub>1)"
1.83 + proof (rule P)
1.84 + fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
1.85 + show "P p"
1.86 + proof (cases "fst p < a\<^isub>1")
1.87 + case True
1.88 + then have "P (fst p, snd p)" by (rule a\<^isub>1)
1.89 + then show ?thesis by simp
1.90 + next
1.91 + case False
1.92 + with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
1.93 + by (simp_all add: prod_less_eq)
1.94 + from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
1.95 + with 1 show ?thesis by simp
1.96 + qed
1.97 + qed
1.98 + qed
1.99 + qed
1.100 qed
1.101 qed
1.102