src/HOL/Fun.thy
author paulson
Fri Nov 13 13:26:16 1998 +0100 (1998-11-13)
changeset 5852 4d7320490be4
parent 5608 a82a038a3e7a
child 6171 cd237a10cbf8
permissions -rw-r--r--
the function space operator
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
paulson@5852
     9
Fun = Vimage + equalities + 
nipkow@2912
    10
paulson@4059
    11
instance set :: (term) order
paulson@4059
    12
                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
nipkow@2912
    13
consts
nipkow@2912
    14
nipkow@5608
    15
  id          ::  'a => 'a
oheimb@5305
    16
  o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
nipkow@4830
    17
  inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
nipkow@4830
    18
  inj_on      :: ['a => 'b, 'a set] => bool
nipkow@4830
    19
  inv         :: ('a => 'b) => ('b => 'a)
oheimb@5305
    20
  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
oheimb@5305
    21
oheimb@5305
    22
nonterminals
oheimb@5305
    23
  updbinds  updbind
oheimb@5305
    24
oheimb@5305
    25
syntax
oheimb@5305
    26
oheimb@5305
    27
  (* Let expressions *)
oheimb@5305
    28
oheimb@5305
    29
  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
oheimb@5305
    30
  ""               :: updbind => updbinds             ("_")
oheimb@5305
    31
  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
oheimb@5305
    32
  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
oheimb@5305
    33
oheimb@5305
    34
translations
oheimb@5305
    35
  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
oheimb@5305
    36
  "f(x:=y)"                     == "fun_upd f x y"
nipkow@2912
    37
nipkow@2912
    38
defs
nipkow@2912
    39
nipkow@5608
    40
  id_def	"id             == %x. x"
oheimb@5305
    41
  o_def   	"f o g          == %x. f(g(x))"
oheimb@5305
    42
  inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
oheimb@5305
    43
  inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
oheimb@5305
    44
  surj_def	"surj f         == ! y. ? x. y=f(x)"
oheimb@5305
    45
  inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
oheimb@5305
    46
  fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
nipkow@2912
    47
paulson@5852
    48
paulson@5852
    49
(*The Pi-operator, by Florian Kammueller*)
paulson@5852
    50
  
paulson@5852
    51
constdefs
paulson@5852
    52
  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
paulson@5852
    53
    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
paulson@5852
    54
paulson@5852
    55
  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
paulson@5852
    56
    "restrict f A == (%x. if x : A then f x else (@ y. True))"
paulson@5852
    57
paulson@5852
    58
syntax
paulson@5852
    59
  "@Pi"  :: "[idt, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
paulson@5852
    60
  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
paulson@5852
    61
  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
paulson@5852
    62
paulson@5852
    63
  (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
paulson@5852
    64
paulson@5852
    65
translations
paulson@5852
    66
  "PI x:A. B" => "Pi A (%x. B)"
paulson@5852
    67
  "A funcset B"    => "Pi A (_K B)"
paulson@5852
    68
  "lam x:A. f"  == "restrict (%x. f) A"
paulson@5852
    69
paulson@5852
    70
constdefs
paulson@5852
    71
  Applyall :: "[('a => 'b) set, 'a]=> 'b set"
paulson@5852
    72
    "Applyall F a == (%f. f a) `` F"
paulson@5852
    73
paulson@5852
    74
  compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
paulson@5852
    75
    "compose A g f == lam x : A. g(f x)"
paulson@5852
    76
paulson@5852
    77
  Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
paulson@5852
    78
    "Inv A f == (% x. (@ y. y : A & f y = x))"
paulson@5852
    79
paulson@5852
    80
  
nipkow@2912
    81
end
paulson@5852
    82
paulson@5852
    83
ML
paulson@5852
    84
val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];