# HG changeset patch # User oheimb # Date 997345065 -7200 # Node ID f3ff2549cdc8af0956fedb29e245f3f2fe5a57a6 # Parent 6659e1ddd4ca7929dfbf81b3ca7d5a195ec48657 added pair_imageI (also as intro rule) diff -r 6659e1ddd4ca -r f3ff2549cdc8 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Aug 09 10:16:23 2001 +0200 +++ b/src/HOL/Product_Type.thy Thu Aug 09 10:17:45 2001 +0200 @@ -30,9 +30,9 @@ qed syntax (symbols) - "*" :: "[type, type] => type" ("(_ \\/ _)" [21, 20] 20) + "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) syntax (HTML output) - "*" :: "[type, type] => type" ("(_ \\/ _)" [21, 20] 20) + "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) (* abstract constants and syntax *) @@ -74,8 +74,8 @@ "A <*> B" => "Sigma A (_K B)" syntax (symbols) - "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\ _\\_./ _)" 10) - "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\ _" [81, 80] 80) + "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\ _\_./ _)" 10) + "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \ _" [81, 80] 80) print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} @@ -118,6 +118,11 @@ use "Product_Type_lemmas.ML" +lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" +apply (rule_tac x = "(a,b)" in image_eqI) +apply auto +done + constdefs internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c" "internal_split == split"