# HG changeset patch
# User paulson
# Date 910960144 -3600
# Node ID 5fb5a626f3b942980e8e0f41bad39a96f7a41f8b
# Parent  9be441c17f6d941ad42a375d3822897545b40739
moved Pi and -> (renamed funcset) to Fun.thy

diff -r 9be441c17f6d -r 5fb5a626f3b9 src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Fri Nov 13 13:28:23 1998 +0100
+++ b/src/HOL/ex/PiSets.ML	Fri Nov 13 13:29:04 1998 +0100
@@ -5,158 +5,6 @@
 Pi sets and their application.
 *)
 
-(*** -> and Pi ***)
-
-
-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 -> 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 -> 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 -> B; g: B -> C |]==> compose A g f: A -> C";
-by Auto_tac;
-qed "funcset_compose";
-
-Goal "[| f: A -> B; g: B -> C; h: C -> 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 -> B; g: B -> 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 -> B; f `` A = B; g: B -> 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 -> B; g: B -> 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 -> 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 -> 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 -> B |] \
-\                ==> (lam x: B. (Inv A f) x) : B -> A";
-by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
-qed "Inv_funcset";
-
-
-Goal "[| f: A -> 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 -> 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 -> 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 its application @@ ***)
-
-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 ~= {} |] ==> (Pi A B) @@ a = B(a)";
-by (auto_tac (claset(), simpset() addsimps [Fset_apply_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 "Fset_beta";
-
-
 (*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
 Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";
 by (auto_tac (claset(),
diff -r 9be441c17f6d -r 5fb5a626f3b9 src/HOL/ex/PiSets.thy
--- a/src/HOL/ex/PiSets.thy	Fri Nov 13 13:28:23 1998 +0100
+++ b/src/HOL/ex/PiSets.thy	Fri Nov 13 13:29:04 1998 +0100
@@ -2,41 +2,20 @@
     ID:         $Id$
     Author:     Florian Kammueller, University of Cambridge
 
-Theory for Pi type in terms of sets.
+The bijection between elements of the Pi set and functional graphs
+
+Also the nice -> operator for function space
 *)
 
 PiSets = Univ + Finite +
 
+syntax
+  "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
 
+translations
+  "A -> B" == "A funcset B"
 
 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)
-  "@->"  :: "['a set, 'b set] => ('a => 'b) set"       ("_ -> _" [91,90]90) 
-(* or "->" ... (infixr 60) and at the end print_translation (... op ->) *)
-  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"    ("(3lam _:_./ _)" 10)
-
-translations
-  "PI x:A. B" => "Pi A (%x. B)"
-  "A -> B"    => "Pi A (_K B)"
-  "lam x:A. f"  == "restrict (%x. f) A"
-
-constdefs
-  Fset_apply :: "[('a => 'b) set, 'a]=> 'b set"   ("_ @@ _" [90,91]90)
-    "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))"
-
 (* bijection between Pi_sig and Pi_=> *)
   PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
     "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
@@ -45,6 +24,3 @@
    "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
 
 end
-
-ML
-val print_translation = [("Pi", dependent_tr' ("@Pi", "@->"))];