src/HOL/Old_Datatype.thy

 *)
 
 header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
 
 theory Old_Datatype
-imports Product_Type Sum_Type Nat
+imports Power
 keywords "datatype" :: thy_decl
 begin
 
 subsection {* The datatype universe *}
 

 by blast
 
 lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
 
 
+(*** Domain theorems ***)
+
+lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
+  by auto
+
+lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
+  by auto
+
+
 text {* hides popular names *}
 hide_type (open) node item
 hide_const (open) Push Node Atom Leaf Numb Lim Split Case
 
 ML_file "Tools/Old_Datatype/old_datatype.ML"