--- 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(),
--- 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", "@->"))];