src/HOL/Fun.thy
changeset 5852 4d7320490be4
parent 5608 a82a038a3e7a
child 6171 cd237a10cbf8
     1.1 --- a/src/HOL/Fun.thy	Thu Nov 12 16:45:40 1998 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Nov 13 13:26:16 1998 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Notions about functions.
     1.5  *)
     1.6  
     1.7 -Fun = Vimage +
     1.8 +Fun = Vimage + equalities + 
     1.9  
    1.10  instance set :: (term) order
    1.11                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
    1.12 @@ -45,4 +45,40 @@
    1.13    inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.14    fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    1.15  
    1.16 +
    1.17 +(*The Pi-operator, by Florian Kammueller*)
    1.18 +  
    1.19 +constdefs
    1.20 +  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
    1.21 +    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
    1.22 +
    1.23 +  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
    1.24 +    "restrict f A == (%x. if x : A then f x else (@ y. True))"
    1.25 +
    1.26 +syntax
    1.27 +  "@Pi"  :: "[idt, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    1.28 +  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
    1.29 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
    1.30 +
    1.31 +  (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
    1.32 +
    1.33 +translations
    1.34 +  "PI x:A. B" => "Pi A (%x. B)"
    1.35 +  "A funcset B"    => "Pi A (_K B)"
    1.36 +  "lam x:A. f"  == "restrict (%x. f) A"
    1.37 +
    1.38 +constdefs
    1.39 +  Applyall :: "[('a => 'b) set, 'a]=> 'b set"
    1.40 +    "Applyall F a == (%f. f a) `` F"
    1.41 +
    1.42 +  compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
    1.43 +    "compose A g f == lam x : A. g(f x)"
    1.44 +
    1.45 +  Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
    1.46 +    "Inv A f == (% x. (@ y. y : A & f y = x))"
    1.47 +
    1.48 +  
    1.49  end
    1.50 +
    1.51 +ML
    1.52 +val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];