src/HOL/Fun.thy
author oheimb
Fri Feb 18 20:24:16 2000 +0100 (2000-02-18)
changeset 8258 666d3a4f3b9d
parent 7374 dec7b838f5cb
child 8924 c434283b4cfa
permissions -rw-r--r--
changed precedence of function update
     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 = Vimage + equalities + 
    10 
    11 instance set :: (term) order
    12                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
    13 nonterminals
    14   updbinds  updbind
    15 
    16 consts
    17   fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    18 
    19 syntax
    20 
    21   (* Let expressions *)
    22 
    23   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    24   ""               :: updbind => updbinds             ("_")
    25   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    26   "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
    27 
    28 translations
    29   "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    30   "f(x:=y)"                     == "fun_upd f x y"
    31 
    32 defs
    33   fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    34 
    35   
    36 constdefs
    37   id ::  'a => 'a
    38     "id == %x. x"
    39 
    40   o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    41     "f o g == %x. f(g(x))"
    42   
    43   inv :: ('a => 'b) => ('b => 'a)
    44     "inv(f::'a=>'b) == % y. @x. f(x)=y"
    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
    50   inj   :: ('a => 'b) => bool                   (*injective*)
    51 
    52 translations
    53   "inj f" == "inj_on f UNIV"
    54 
    55 constdefs
    56   surj :: ('a => 'b) => bool                   (*surjective*)
    57     "surj f == ! y. ? x. y=f(x)"
    58   
    59   bij :: ('a => 'b) => bool                    (*bijective*)
    60     "bij f == inj f & surj f"
    61   
    62 
    63 (*The Pi-operator, by Florian Kammueller*)
    64   
    65 constdefs
    66   Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
    67     "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
    68 
    69   restrict :: "['a => 'b, 'a set] => ('a => 'b)"
    70     "restrict f A == (%x. if x : A then f x else (@ y. True))"
    71 
    72 syntax
    73   "@Pi"  :: "[idt, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    74   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
    75   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
    76 
    77   (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
    78 
    79 translations
    80   "PI x:A. B" => "Pi A (%x. B)"
    81   "A funcset B"    => "Pi A (_K B)"
    82   "lam x:A. f"  == "restrict (%x. f) A"
    83 
    84 constdefs
    85   Applyall :: "[('a => 'b) set, 'a]=> 'b set"
    86     "Applyall F a == (%f. f a) `` F"
    87 
    88   compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
    89     "compose A g f == lam x : A. g(f x)"
    90 
    91   Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
    92     "Inv A f == (% x. (@ y. y : A & f y = x))"
    93 
    94   
    95 end
    96 
    97 ML
    98 val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];