src/HOL/Fun.thy
author wenzelm
Tue Dec 11 13:43:00 2001 +0100 (2001-12-11)
changeset 12460 624a8cd51b4e
parent 12459 6978ab7cac64
child 13585 db4005b40cc6
permissions -rw-r--r--
oops;
     1 (*  Title:      HOL/Fun.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Notions about functions.
     7 *)
     8 
     9 Fun = Typedef +
    10 
    11 instance set :: (type) order
    12                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
    13 consts
    14   fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    15 
    16 nonterminals
    17   updbinds updbind
    18 syntax
    19   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    20   ""               :: updbind => updbinds             ("_")
    21   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    22   "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
    23 
    24 translations
    25   "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    26   "f(x:=y)"                     == "fun_upd f x y"
    27 
    28 defs
    29   fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    30 
    31 (* Hint: to define the sum of two functions (or maps), use sum_case.
    32          A nice infix syntax could be defined (in Datatype.thy or below) by
    33 consts
    34   fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    35 translations
    36  "fun_sum" == "sum_case"
    37 *)
    38 
    39 constdefs
    40   id ::  'a => 'a
    41     "id == %x. x"
    42 
    43   o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    44     "f o g == %x. f(g(x))"
    45 
    46   inj_on :: ['a => 'b, 'a set] => bool
    47     "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    48 
    49 syntax (xsymbols)
    50   "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
    51 
    52 syntax
    53   inj   :: ('a => 'b) => bool                   (*injective*)
    54 
    55 translations
    56   "inj f" == "inj_on f UNIV"
    57 
    58 constdefs
    59   surj :: ('a => 'b) => bool                   (*surjective*)
    60     "surj f == ! y. ? x. y=f(x)"
    61 
    62   bij :: ('a => 'b) => bool                    (*bijective*)
    63     "bij f == inj f & surj f"
    64 
    65 
    66 (*The Pi-operator, by Florian Kammueller*)
    67 
    68 constdefs
    69   Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
    70     "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}"
    71 
    72   restrict :: "['a => 'b, 'a set] => ('a => 'b)"
    73     "restrict f A == (%x. if x : A then f x else arbitrary)"
    74 
    75 syntax
    76   "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    77   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)
    78   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
    79 syntax (xsymbols)
    80   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3)
    81 
    82   (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
    83 
    84 syntax (xsymbols)
    85   "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
    86 
    87 translations
    88   "PI x:A. B" => "Pi A (%x. B)"
    89   "A funcset B"    => "Pi A (_K B)"
    90   "%x:A. f"  == "restrict (%x. f) A"
    91 
    92 constdefs
    93   compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    94   "compose A g f == %x:A. g (f x)"
    95 
    96 end
    97 
    98 ML
    99 val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];