# HG changeset patch
# User wenzelm
# Date 981148690 -3600
# Node ID 83f723e86dace0fd7b6c62b0d7e9b705381b8d9e
# Parent  99c4bed16b9b7b8e5be7ee181f871f68bb723233
added hidden internal_split constant;
tuned;

diff -r 99c4bed16b9b -r 83f723e86dac src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Feb 02 22:17:31 2001 +0100
+++ b/src/HOL/Product_Type.thy	Fri Feb 02 22:18:10 2001 +0100
@@ -8,10 +8,7 @@
 *)
 
 theory Product_Type = Fun
-files 
-  ("Tools/split_rule.ML")
-  ("Product_Type_lemmas.ML")
-:
+files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"):
 
 
 (** products **)
@@ -20,13 +17,13 @@
 
 constdefs
   Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
- "Pair_Rep == (%a b. %x y. x=a & y=b)"
+  "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)}"
+    = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
 proof
   fix a b show "Pair_Rep a b : ?Prod"
     by blast
@@ -80,7 +77,7 @@
   "@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"))]; *}
+print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
 
 
 (* definitions *)
@@ -89,8 +86,8 @@
 
 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)"
+  fst_def:      "fst p == SOME a. EX b. p = (a, b)"
+  snd_def:      "snd p == SOME b. EX 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)}"
@@ -101,7 +98,7 @@
 
 global
 
-typedef  unit = "{True}" 
+typedef unit = "{True}"
 proof
   show "True : ?unit"
     by blast
@@ -115,9 +112,22 @@
 defs
   Unity_def:    "() == Abs_unit True"
 
+
+
+(** lemmas and tool setup **)
+
 use "Product_Type_lemmas.ML"
 
+constdefs
+  internal_split :: "('a \<Rightarrow> 'b => 'c) => 'a * 'b => 'c"
+  "internal_split == split"
+
+lemma internal_split_conv: "internal_split c (a, b) = c a b"
+  by (simp only: internal_split_def split_conv)
+
+hide const internal_split
+
 use "Tools/split_rule.ML"
-setup split_attributes
+setup SplitRule.setup
 
 end