# HG changeset patch
# User paulson
# Date 910959976 -3600
# Node ID 4d7320490be4f17ddbaf4a973aef084ca255f9ab
# Parent  15ce4c1c83134e3a77dbf2df67a9cc3b5012f096
the function space operator

diff -r 15ce4c1c8313 -r 4d7320490be4 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Thu Nov 12 16:45:40 1998 +0100
+++ b/src/HOL/Fun.ML	Fri Nov 13 13:26:16 1998 +0100
@@ -58,6 +58,10 @@
 by (Blast_tac 1);
 qed "image_compose";
 
+Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
+by (Blast_tac 1);
+qed "UNION_o";
+
 
 section "inj";
 
@@ -219,3 +223,156 @@
 by (rtac ext 1);
 by (Auto_tac);
 qed "fun_upd_twist";
+
+
+(*** -> and Pi, by Florian Kammueller and LCP ***)
+
+val prems = Goalw [Pi_def]
+"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
+\    ==> f: Pi A B";
+by (auto_tac (claset(), simpset() addsimps prems));
+qed "Pi_I";
+
+val prems = Goal 
+"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
+by (blast_tac (claset() addIs Pi_I::prems) 1);
+qed "funcsetI";
+
+Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
+by Auto_tac;
+qed "Pi_mem";
+
+Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
+by Auto_tac;
+qed "funcset_mem";
+
+Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
+by Auto_tac;
+qed "apply_arb";
+
+Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
+by (rtac ext 1);
+by Auto_tac;
+val Pi_extensionality = ballI RSN (3, result());
+
+(*** compose ***)
+
+Goalw [Pi_def, compose_def, restrict_def]
+     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
+by Auto_tac;
+qed "funcset_compose";
+
+Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
+\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
+by (res_inst_tac [("A","A")] Pi_extensionality 1);
+by (blast_tac (claset() addIs [funcset_compose]) 1);
+by (blast_tac (claset() addIs [funcset_compose]) 1);
+by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
+by Auto_tac;
+qed "compose_assoc";
+
+Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
+by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
+qed "compose_eq";
+
+Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
+\     ==> compose A g f `` A = C";
+by (auto_tac (claset(),
+	      simpset() addsimps [image_def, compose_eq]));
+qed "surj_compose";
+
+
+Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
+\     ==> inj_on (compose A g f) A";
+by (auto_tac (claset(),
+	      simpset() addsimps [inj_on_def, compose_eq]));
+qed "inj_on_compose";
+
+
+(*** restrict / lam ***)
+Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
+by (auto_tac (claset(),
+	      simpset() addsimps [restrict_def, Pi_def]));
+qed "restrict_in_funcset";
+
+val prems = Goalw [restrict_def, Pi_def]
+     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
+by (asm_simp_tac (simpset() addsimps prems) 1);
+qed "restrictI";
+
+
+Goal "x: A ==> (lam y: A. f y) x = f x";
+by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
+qed "restrict_apply1";
+
+Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
+by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
+qed "restrict_apply1_mem";
+
+Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
+by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
+qed "restrict_apply2";
+
+
+val prems = Goal
+    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
+by (rtac ext 1);
+by (auto_tac (claset(),
+	      simpset() addsimps prems@[restrict_def, Pi_def]));
+qed "restrict_ext";
+
+
+(*** Inverse ***)
+
+Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
+by (Blast_tac 1);
+qed "surj_image";
+
+Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
+\                ==> (lam x: B. (Inv A f) x) : B funcset A";
+by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
+qed "Inv_funcset";
+
+
+Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
+\     ==> (lam y: B. (Inv A f) y) (f x) = x";
+by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
+by (rtac selectI2 1);
+by Auto_tac;
+qed "Inv_f_f";
+
+Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
+\     ==> f ((lam y: B. (Inv A f y)) x) = x";
+by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
+by (fast_tac (claset() addIs [selectI2]) 1);
+qed "f_Inv_f";
+
+Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
+\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
+by (rtac Pi_extensionality 1);
+by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
+by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
+qed "compose_Inv_id";
+
+
+(*** Pi and Applyall ***)
+
+Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
+by Auto_tac;
+qed "Pi_eq_empty";
+
+Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
+by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
+qed "Pi_total1";
+
+Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
+by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
+by (rename_tac "g z" 1);
+by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
+by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
+qed "Applyall_beta";
+
+
diff -r 15ce4c1c8313 -r 4d7320490be4 src/HOL/Fun.thy
--- 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"))];