--- a/src/HOL/Fun.thy Thu Nov 12 16:45:40 1998 +0100
+++ b/src/HOL/Fun.thy Fri Nov 13 13:26:16 1998 +0100
@@ -6,7 +6,7 @@
Notions about functions.
*)
-Fun = Vimage +
+Fun = Vimage + equalities +
instance set :: (term) order
(subset_refl,subset_trans,subset_antisym,psubset_eq)
@@ -45,4 +45,40 @@
inv_def "inv(f::'a=>'b) == % y. @x. f(x)=y"
fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
+
+(*The Pi-operator, by Florian Kammueller*)
+
+constdefs
+ Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
+ "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
+
+ restrict :: "['a => 'b, 'a set] => ('a => 'b)"
+ "restrict f A == (%x. if x : A then f x else (@ y. True))"
+
+syntax
+ "@Pi" :: "[idt, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
+ funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr 60)
+ "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10)
+
+ (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
+
+translations
+ "PI x:A. B" => "Pi A (%x. B)"
+ "A funcset B" => "Pi A (_K B)"
+ "lam x:A. f" == "restrict (%x. f) A"
+
+constdefs
+ Applyall :: "[('a => 'b) set, 'a]=> 'b set"
+ "Applyall F a == (%f. f a) `` F"
+
+ compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
+ "compose A g f == lam x : A. g(f x)"
+
+ Inv :: "['a set, 'a => 'b] => ('b => 'a)"
+ "Inv A f == (% x. (@ y. y : A & f y = x))"
+
+
end
+
+ML
+val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];