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