src/HOL/ex/PiSets.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10212 33fe2d701ddd
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/PiSets.thy
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Kammueller, University of Cambridge
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     4
5856
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
     5
The bijection between elements of the Pi set and functional graphs
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
     6
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
     7
Also the nice -> operator for function space
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     8
*)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     9
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 5856
diff changeset
    10
PiSets = Datatype_Universe + Finite +
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    11
5856
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
    12
syntax
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
    13
  "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
5846
paulson
parents: 5250
diff changeset
    14
5856
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
    15
translations
5fb5a626f3b9 moved Pi and -> (renamed funcset) to Fun.thy
paulson
parents: 5846
diff changeset
    16
  "A -> B" == "A funcset B"
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    17
5846
paulson
parents: 5250
diff changeset
    18
constdefs
paulson
parents: 5250
diff changeset
    19
(* bijection between Pi_sig and Pi_=> *)
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    20
  PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
5846
paulson
parents: 5250
diff changeset
    21
    "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    22
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    23
  Graph ::  "['a set, 'a => 'b set] => ('a * 'b) set set"
5846
paulson
parents: 5250
diff changeset
    24
   "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    25
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    26
end