# HG changeset patch
# User haftmann
# Date 1402555739 -7200
# Node ID 8fcbfce2a2a9cffb95ca0c50fc53383d8b57dc4c
# Parent  8cecd655eef4fd0554c35d9b7fd6feb3b28fa5a9
uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor

diff -r 8cecd655eef4 -r 8fcbfce2a2a9 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Product_Type.thy	Thu Jun 12 08:48:59 2014 +0200
@@ -130,39 +130,66 @@
 
 end
 
-instantiation unit :: linorder
+instantiation unit :: "{complete_boolean_algebra, complete_linorder, wellorder}"
 begin
 
-definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
-"less_eq_unit _ _ = True"
+definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool"
+where
+  "(_::unit) \<le> _ \<longleftrightarrow> True"
+
+lemma less_eq_unit [iff]:
+  "(u::unit) \<le> v"
+  by (simp add: less_eq_unit_def)
+
+definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool"
+where
+  "(_::unit) < _ \<longleftrightarrow> False"
+
+lemma less_unit [iff]:
+  "\<not> (u::unit) < v"
+  by (simp_all add: less_eq_unit_def less_unit_def)
+
+definition bot_unit :: unit
+where
+  [code_unfold]: "\<bottom> = ()"
+
+definition top_unit :: unit
+where
+  [code_unfold]: "\<top> = ()"
 
-definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
-"less_unit _ _ = False"
+definition inf_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit"
+where
+  [simp]: "_ \<sqinter> _ = ()"
+
+definition sup_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit"
+where
+  [simp]: "_ \<squnion> _ = ()"
+
+definition Inf_unit :: "unit set \<Rightarrow> unit"
+where
+  [simp]: "\<Sqinter>_ = ()"
 
-declare less_eq_unit_def [simp, abs_def, code_unfold] less_unit_def [simp, abs_def, code_unfold]
+definition Sup_unit :: "unit set \<Rightarrow> unit"
+where
+  [simp]: "\<Squnion>_ = ()"
+
+definition uminus_unit :: "unit \<Rightarrow> unit"
+where
+  [simp]: "- _ = ()"
+
+declare less_eq_unit_def [abs_def, code_unfold]
+  less_unit_def [abs_def, code_unfold]
+  inf_unit_def [abs_def, code_unfold]
+  sup_unit_def [abs_def, code_unfold]
+  Inf_unit_def [abs_def, code_unfold]
+  Sup_unit_def [abs_def, code_unfold]
+  uminus_unit_def [abs_def, code_unfold]
 
 instance
-proof qed auto
+  by intro_classes auto
 
 end
 
-instantiation unit :: complete_boolean_algebra begin
-
-definition "top = ()"
-definition "bot = ()"
-definition [code_unfold]: "sup _ _ = ()"
-definition [code_unfold]: "inf _ _ = ()"
-definition "Sup _ = ()"
-definition "Inf _ = ()"
-definition [simp, code_unfold]: "uminus = (\<lambda>_ :: unit. ())"
-
-instance by intro_classes auto
-
-end
-
-instance unit :: "{complete_linorder, wellorder}"
-  by intro_classes auto
-
 lemma [code]:
   "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+