src/HOL/Library/FuncSet.thy
changeset 19536 1a3a3cf8b4fa
parent 17781 32bb237158a5
child 19656 09be06943252
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue May 02 20:42:30 2006 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue May 02 20:42:32 2006 +0200
     1.3 @@ -19,14 +19,20 @@
     1.4    "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
     1.5    "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
     1.6  
     1.7 +abbreviation
     1.8 +  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
     1.9 +  "A -> B == Pi A (%_. B)"
    1.10 +
    1.11 +abbreviation (xsymbols)
    1.12 +  funcset1  (infixr "\<rightarrow>" 60)
    1.13 +  "funcset1 == funcset"
    1.14 +
    1.15  syntax
    1.16    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    1.17 -  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
    1.18    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    1.19  
    1.20  syntax (xsymbols)
    1.21    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.22 -  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60)
    1.23    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.24  
    1.25  syntax (HTML output)
    1.26 @@ -34,16 +40,13 @@
    1.27    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.28  
    1.29  translations
    1.30 -  "PI x:A. B" => "Pi A (%x. B)"
    1.31 -  "A -> B" => "Pi A (%_. B)"
    1.32 +  "PI x:A. B" == "Pi A (%x. B)"
    1.33    "%x:A. f" == "restrict (%x. f) A"
    1.34  
    1.35  constdefs
    1.36    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    1.37    "compose A g f == \<lambda>x\<in>A. g (f x)"
    1.38  
    1.39 -print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
    1.40 -
    1.41  
    1.42  subsection{*Basic Properties of @{term Pi}*}
    1.43