src/HOL/Product_Type.thy
changeset 11025 a70b796d9af8
parent 10289 475ea668c67d
child 11032 83f723e86dac
--- a/src/HOL/Product_Type.thy	Thu Feb 01 20:51:13 2001 +0100
+++ b/src/HOL/Product_Type.thy	Thu Feb 01 20:51:48 2001 +0100
@@ -7,7 +7,11 @@
 The unit type.
 *)
 
-Product_Type = Fun +
+theory Product_Type = Fun
+files 
+  ("Tools/split_rule.ML")
+  ("Product_Type_lemmas.ML")
+:
 
 
 (** products **)
@@ -15,31 +19,34 @@
 (* type definition *)
 
 constdefs
-  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
-  "Pair_Rep == (%a b. %x y. x=a & y=b)"
+  Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
+ "Pair_Rep == (%a b. %x y. x=a & y=b)"
 
 global
 
 typedef (Prod)
   ('a, 'b) "*"          (infixr 20)
     = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
+proof
+  fix a b show "Pair_Rep a b : ?Prod"
+    by blast
+qed
 
 syntax (symbols)
-  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
-
+  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 syntax (HTML output)
-  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
+  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 
 
 (* abstract constants and syntax *)
 
 consts
-  fst           :: "'a * 'b => 'a"
-  snd           :: "'a * 'b => 'b"
-  split         :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
-  prod_fun      :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
-  Pair          :: "['a, 'b] => 'a * 'b"
-  Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
+  fst      :: "'a * 'b => 'a"
+  snd      :: "'a * 'b => 'b"
+  split    :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
+  prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
+  Pair     :: "['a, 'b] => 'a * 'b"
+  Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
 
 
 (* patterns -- extends pre-defined type "pttrn" used in abstractions *)
@@ -51,11 +58,11 @@
   "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
   "_tuple_arg"  :: "'a => tuple_args"                   ("_")
   "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
-  "_pattern"    :: [pttrn, patterns] => pttrn           ("'(_,/ _')")
-  ""            :: pttrn => patterns                    ("_")
-  "_patterns"   :: [pttrn, patterns] => patterns        ("_,/ _")
-  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
-  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
+  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("'(_,/ _')")
+  ""            :: "pttrn => patterns"                  ("_")
+  "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
+  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
+  "@Times" ::"['a set,  'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
 
 translations
   "(x, y)"       == "Pair x y"
@@ -70,8 +77,10 @@
   "A <*> B"      => "Sigma A (_K B)"
 
 syntax (symbols)
-  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
-  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
+  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
+  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
+
+print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; *}
 
 
 (* definitions *)
@@ -79,12 +88,12 @@
 local
 
 defs
-  Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
-  fst_def       "fst p == @a. ? b. p = (a, b)"
-  snd_def       "snd p == @b. ? a. p = (a, b)"
-  split_def     "split == (%c p. c (fst p) (snd p))"
-  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
-  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
+  Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
+  fst_def:      "fst p == @a. ? b. p = (a, b)"
+  snd_def:      "snd p == @b. ? a. p = (a, b)"
+  split_def:    "split == (%c p. c (fst p) (snd p))"
+  prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
+  Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
 
 
@@ -92,7 +101,11 @@
 
 global
 
-typedef  unit = "{True}"
+typedef  unit = "{True}" 
+proof
+  show "True : ?unit"
+    by blast
+qed
 
 consts
   "()"          :: unit                           ("'(')")
@@ -100,10 +113,11 @@
 local
 
 defs
-  Unity_def     "() == Abs_unit True"
+  Unity_def:    "() == Abs_unit True"
+
+use "Product_Type_lemmas.ML"
+
+use "Tools/split_rule.ML"
+setup split_attributes
 
 end
-
-ML
-
-val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];