src/HOL/Fun.thy
author wenzelm
Tue, 11 Dec 2001 13:43:00 +0100
changeset 12460 624a8cd51b4e
parent 12459 6978ab7cac64
child 13585 db4005b40cc6
permissions -rw-r--r--
oops;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 923
diff changeset
     1
(*  Title:      HOL/Fun.thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 923
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
     6
Notions about functions.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
12258
5da24e7e9aba got rid of theory Inverse_Image;
wenzelm
parents: 12114
diff changeset
     9
Fun = Typedef +
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
    10
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12258
diff changeset
    11
instance set :: (type) order
4059
59c1422c9da5 New Blast_tac (and minor tidying...)
paulson
parents: 2912
diff changeset
    12
                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    13
consts
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    14
  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    15
9141
wenzelm
parents: 8960
diff changeset
    16
nonterminals
wenzelm
parents: 8960
diff changeset
    17
  updbinds updbind
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    18
syntax
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    19
  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    20
  ""               :: updbind => updbinds             ("_")
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    21
  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
8258
666d3a4f3b9d changed precedence of function update
oheimb
parents: 7374
diff changeset
    22
  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
5305
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    23
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    24
translations
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    25
  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
513925de8962 cleanup for Fun.thy:
oheimb
parents: 4830
diff changeset
    26
  "f(x:=y)"                     == "fun_upd f x y"
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
    27
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
    28
defs
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    29
  fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
    30
9340
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    31
(* Hint: to define the sum of two functions (or maps), use sum_case.
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    32
         A nice infix syntax could be defined (in Datatype.thy or below) by
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    33
consts
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    34
  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    35
translations
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    36
 "fun_sum" == "sum_case"
9666f78ecfab added hint on fun_sum
oheimb
parents: 9309
diff changeset
    37
*)
12258
5da24e7e9aba got rid of theory Inverse_Image;
wenzelm
parents: 12114
diff changeset
    38
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    39
constdefs
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    40
  id ::  'a => 'a
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    41
    "id == %x. x"
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    42
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    43
  o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    44
    "f o g == %x. f(g(x))"
11123
15ffc08f905e removed whitespace
oheimb
parents: 10826
diff changeset
    45
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    46
  inj_on :: ['a => 'b, 'a set] => bool
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    47
    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
    48
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 11609
diff changeset
    49
syntax (xsymbols)
9352
416b2ecd97a1 syntax (symbols) "op o" moved from HOL to Fun;
wenzelm
parents: 9340
diff changeset
    50
  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
416b2ecd97a1 syntax (symbols) "op o" moved from HOL to Fun;
wenzelm
parents: 9340
diff changeset
    51
6171
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    52
syntax
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    53
  inj   :: ('a => 'b) => bool                   (*injective*)
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    54
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    55
translations
cd237a10cbf8 inj is now a translation of inj_on
paulson
parents: 5852
diff changeset
    56
  "inj f" == "inj_on f UNIV"
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    57
7374
dec7b838f5cb the bij predicate (at last)
paulson
parents: 6171
diff changeset
    58
constdefs
dec7b838f5cb the bij predicate (at last)
paulson
parents: 6171
diff changeset
    59
  surj :: ('a => 'b) => bool                   (*surjective*)
dec7b838f5cb the bij predicate (at last)
paulson
parents: 6171
diff changeset
    60
    "surj f == ! y. ? x. y=f(x)"
12258
5da24e7e9aba got rid of theory Inverse_Image;
wenzelm
parents: 12114
diff changeset
    61
7374
dec7b838f5cb the bij predicate (at last)
paulson
parents: 6171
diff changeset
    62
  bij :: ('a => 'b) => bool                    (*bijective*)
dec7b838f5cb the bij predicate (at last)
paulson
parents: 6171
diff changeset
    63
    "bij f == inj f & surj f"
12258
5da24e7e9aba got rid of theory Inverse_Image;
wenzelm
parents: 12114
diff changeset
    64
7374
dec7b838f5cb the bij predicate (at last)
paulson
parents: 6171
diff changeset
    65
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    66
(*The Pi-operator, by Florian Kammueller*)
12258
5da24e7e9aba got rid of theory Inverse_Image;
wenzelm
parents: 12114
diff changeset
    67
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    68
constdefs
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    69
  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11123
diff changeset
    70
    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}"
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    71
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    72
  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11123
diff changeset
    73
    "restrict f A == (%x. if x : A then f x else arbitrary)"
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    74
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    75
syntax
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11123
diff changeset
    76
  "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
12258
5da24e7e9aba got rid of theory Inverse_Image;
wenzelm
parents: 12114
diff changeset
    77
  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)
12459
6978ab7cac64 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents: 12338
diff changeset
    78
  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
6978ab7cac64 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents: 12338
diff changeset
    79
syntax (xsymbols)
12460
wenzelm
parents: 12459
diff changeset
    80
  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3)
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    81
12459
6978ab7cac64 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents: 12338
diff changeset
    82
  (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11123
diff changeset
    83
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 11609
diff changeset
    84
syntax (xsymbols)
11451
8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice
paulson
parents: 11123
diff changeset
    85
  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    86
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    87
translations
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    88
  "PI x:A. B" => "Pi A (%x. B)"
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    89
  "A funcset B"    => "Pi A (_K B)"
12459
6978ab7cac64 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents: 12338
diff changeset
    90
  "%x:A. f"  == "restrict (%x. f) A"
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    91
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    92
constdefs
9309
4078d5e8b293 fixed compose decl;
wenzelm
parents: 9141
diff changeset
    93
  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
12459
6978ab7cac64 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents: 12338
diff changeset
    94
  "compose A g f == %x:A. g (f x)"
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    95
2912
3fac3e8d5d3e moved inj and surj from Set to Fun and Inv -> inv.
nipkow
parents: 1475
diff changeset
    96
end
5852
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    97
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    98
ML
4d7320490be4 the function space operator
paulson
parents: 5608
diff changeset
    99
val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];