added pair_imageI (also as intro rule)
authoroheimb
Thu Aug 09 10:17:45 2001 +0200 (2001-08-09)
changeset 11493f3ff2549cdc8
parent 11492 6659e1ddd4ca
child 11494 23a118849801
added pair_imageI (also as intro rule)
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Thu Aug 09 10:16:23 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Aug 09 10:17:45 2001 +0200
     1.3 @@ -30,9 +30,9 @@
     1.4  qed
     1.5  
     1.6  syntax (symbols)
     1.7 -  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
     1.8 +  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
     1.9  syntax (HTML output)
    1.10 -  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    1.11 +  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    1.12  
    1.13  
    1.14  (* abstract constants and syntax *)
    1.15 @@ -74,8 +74,8 @@
    1.16    "A <*> B"      => "Sigma A (_K B)"
    1.17  
    1.18  syntax (symbols)
    1.19 -  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\\<Sigma> _\\<in>_./ _)"   10)
    1.20 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
    1.21 +  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    1.22 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    1.23  
    1.24  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    1.25  
    1.26 @@ -118,6 +118,11 @@
    1.27  
    1.28  use "Product_Type_lemmas.ML"
    1.29  
    1.30 +lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
    1.31 +apply (rule_tac x = "(a,b)" in image_eqI)
    1.32 +apply  auto
    1.33 +done
    1.34 +
    1.35  constdefs
    1.36    internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
    1.37    "internal_split == split"