# HG changeset patch
# User paulson
# Date 910795464 -3600
# Node ID eb183b062eae4f33f85be9ed6ddc3aa1c0361718
# Parent  2886310fb5e94b89e6ac1ce9ca4575b9de262880
Big simplification of proofs.
Deleted lots of unnecessary theorems

diff -r 2886310fb5e9 -r eb183b062eae src/HOL/ex/LocaleGroup.ML
--- a/src/HOL/ex/LocaleGroup.ML	Tue Nov 10 16:28:08 1998 +0100
+++ b/src/HOL/ex/LocaleGroup.ML	Wed Nov 11 15:44:24 1998 +0100
@@ -12,190 +12,134 @@
 Addsimps [simp_G, thm "Group_G"];
 
 
-goal LocaleGroup.thy "e : carrier G";
-by (afs [thm "e_def"] 1);
-val e_closed = result();
+Goal "e : carrier G";
+by (simp_tac (simpset() addsimps [thm "e_def"]) 1);
+qed "e_closed";
 
 (* Mit dieser Def ist es halt schwierig *)
-goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G";
+Goal "op # : carrier G -> carrier G -> carrier G";
 by (res_inst_tac [("t","op #")] ssubst 1);
 by (rtac ext 1);
 by (rtac ext 1);
 by (rtac meta_eq_to_obj_eq 1);
 by (rtac (thm "binop_def") 1);
 by (Asm_full_simp_tac 1);
-val binop_funcset = result();
+qed "binop_funcset";
 
-goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G |] ==> x # y : carrier G";
-by (afs [binop_funcset RS funcset2E1] 1);
-val binop_closed = result();
+Goal "[| x: carrier G; y: carrier G |] ==> x # y : carrier G";
+by (asm_simp_tac
+    (simpset() addsimps [binop_funcset RS funcset_mem RS funcset_mem]) 1);
+qed "binop_closed";
 
-goal LocaleGroup.thy "inv : carrier G -> carrier G";
-by (res_inst_tac [("t","inv")] ssubst 1);
-by (rtac ext 1);
-by (rtac meta_eq_to_obj_eq 1);
-by (rtac (thm "inv_def") 1);
-by (Asm_full_simp_tac 1);
-val inv_funcset = result();
+Addsimps [binop_closed, e_closed];
 
-goal LocaleGroup.thy "!! x . x: carrier G ==> x -| : carrier G";
-by (afs [inv_funcset RS funcsetE1] 1);
-val inv_closed = result(); 
+Goal "INV : carrier G -> carrier G";
+by (asm_simp_tac (simpset() addsimps [thm "inv_def"]) 1);
+qed "inv_funcset";
 
+Goal "x: carrier G ==> x -| : carrier G";
+by (asm_simp_tac (simpset() addsimps [inv_funcset RS funcset_mem]) 1);
+qed "inv_closed"; 
 
-goal LocaleGroup.thy "!! x . x: carrier G ==> e # x = x";
-by (afs [thm "e_def", thm "binop_def"] 1);
-val e_ax1 = result();
+Goal "x: carrier G ==> e # x = x";
+by (asm_simp_tac (simpset() addsimps [thm "e_def", thm "binop_def"]) 1);
+qed "e_ax1";
 
-goal LocaleGroup.thy "!! x. x: carrier G ==> (x -|) # x = e";
-by (afs [thm "binop_def", thm "inv_def", thm "e_def"] 1);
-val inv_ax2 = result();
+Goal "x: carrier G ==> (x -|) # x = e";
+by (asm_simp_tac
+    (simpset() addsimps [thm "binop_def", thm "inv_def", thm "e_def"]) 1);
+qed "inv_ax2";
 
-goal LocaleGroup.thy "!! x y z. [| x: carrier G; y: carrier G; z: carrier G |]\
+Addsimps [inv_closed, e_ax1, inv_ax2];
+
+Goal "[| x: carrier G; y: carrier G; z: carrier G |]\
 \               ==> (x # y) # z = x # (y # z)";
-by (afs [thm "binop_def"] 1);
-val binop_assoc = result();
+by (asm_simp_tac (simpset() addsimps [thm "binop_def"]) 1);
+qed "binop_assoc";
 
-goal LocaleGroup.thy "!! G f i e1. [|f : G -> G -> G; i: G -> G; e1: G;\
-\        ! x: G. (f (i x) x = e1); ! x: G. (f e1 x = x);\
-\        ! x: G. ! y: G. ! z: G.(f (f x y) z = f (x) (f y z)) |] \
-\ ==> (| carrier = G, bin_op = f, inverse = i, unit = e1 |) : Group";
-by (afs [Group_def] 1);
-val GroupI = result();
+Goal "[|f : A -> A -> A; i: A -> A; e1: A;\
+\        ! x: A. (f (i x) x = e1); ! x: A. (f e1 x = x);\
+\        ! x: A. ! y: A. ! z: A.(f (f x y) z = f (x) (f y z)) |] \
+\     ==> (| carrier = A, bin_op = f, inverse = i, unit = e1 |) : Group";
+by (asm_simp_tac (simpset() addsimps [Group_def]) 1);
+qed "GroupI";
 
 (*****)
 (* Now the real derivations *)
 
-goal LocaleGroup.thy "!! x y z. [| x : carrier G ; y : carrier G; z : carrier G;\
-\                  x # y  =  x # z |] ==> y = z";
-(* remarkable: In the following step the use of e_ax1 instead of unit_ax1
-   is better! It doesn't produce G: Group as subgoal and the nice syntax stays *)
+Goal "[| x # y  =  x # z;  \
+\        x : carrier G ; y : carrier G; z : carrier G |] ==> y = z";
 by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
 by (assume_tac 1);
 (* great: we can use the nice syntax even in res_inst_tac *)
-by (res_inst_tac [("P","%r. r # y = z")] subst 1);
-by (res_inst_tac [("x","x")] inv_ax2 1);
-by (assume_tac 1);
-by (stac binop_assoc 1);
-by (rtac inv_closed 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (res_inst_tac [("P","%r. r # y = z")] (inv_ax2 RS subst) 1);
 by (assume_tac 1);
-by (etac ssubst 1);
-by (rtac (binop_assoc RS subst) 1);
-by (rtac inv_closed 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (stac inv_ax2 1);
-by (assume_tac 1);
-by (stac e_ax1 1);
-by (assume_tac 1);
-by (rtac refl 1);
-val left_cancellation = result();
+by (asm_simp_tac (simpset() delsimps [inv_ax2] addsimps [binop_assoc]) 1);
+by (asm_simp_tac (simpset() addsimps [binop_assoc RS sym]) 1);
+qed "left_cancellation";
 
 
-(* here are the other directions of basic lemmas, they needed a cancellation (left) *)
-(* to be able to show the other directions of inverse and unity axiom we need:*)
-goal LocaleGroup.thy "!! x. x: carrier G ==> x # e = x";
-(* here is a problem with res_inst_tac: in Fun there is a 
-   constant inv, and that gets addressed when we type in -|.
-   We have to use the defining term and then fold the def of inv *)
-by (res_inst_tac [("x","inverse G x")] left_cancellation 1);
-by (fold_goals_tac [thm "inv_def"]);
-by (fast_tac (claset() addSEs [inv_closed]) 1);
-by (afs [binop_closed, e_closed] 1);
-by (assume_tac 1);
-by (rtac (binop_assoc RS subst) 1);
-by (fast_tac (claset() addSEs [inv_closed]) 1);
-by (assume_tac 1);
-by (rtac (e_closed) 1);
-by (stac inv_ax2 1);
-by (assume_tac 1);
-by (stac e_ax1 1);
-by (rtac e_closed 1);
-by (rtac refl 1);
-val e_ax2 = result();
+(* Here are the other directions of basic lemmas. 
+   They needed a cancellation (left) to be able to show the other
+   directions of inverse and unity axiom.*)
+Goal "x: carrier G ==> x # e = x";
+by (rtac left_cancellation 1);
+by (etac inv_closed 2);
+by (auto_tac (claset(), simpset() addsimps [binop_assoc RS sym]));
+qed "e_ax2";
+
+Addsimps [e_ax2];
+
+Goal "[| x: carrier G; x # x = x |] ==> x = e";
+by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS ssubst) 1);
+by (etac left_cancellation 2);
+by Auto_tac;
+qed "idempotent_e";
 
-goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e";
-by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1);
-by (assume_tac 1);
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac e_closed 1);
-by (assume_tac 1);
-val idempotent_e = result();
-
-goal LocaleGroup.thy  "!! x. x: carrier G ==> x # (x -|) = e";
+Goal  "x: carrier G ==> x # (x -|) = e";
 by (rtac idempotent_e 1);
-by (afs [binop_closed,inv_closed] 1);
-by (stac binop_assoc 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (afs [binop_closed,inv_closed] 1);
-by (res_inst_tac [("t","x -| # x # x -|")] subst 1);
-by (rtac binop_assoc 1);
-by (afs [inv_closed] 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (stac inv_ax2 1);
-by (assume_tac 1);
-by (stac e_ax1 1);
-by (afs [inv_closed] 1);
-by (rtac refl 1);
-val inv_ax1 = result();
+by (Asm_simp_tac 1);
+by (subgoal_tac "(x # x -|) # x # x -| = x # (x -| # x) # x -|" 1);
+by (asm_simp_tac (simpset() delsimps [inv_ax2]
+			    addsimps [binop_assoc]) 2);
+by Auto_tac;
+qed "inv_ax1";
+
+Addsimps [inv_ax1];
+
+Goal "[| x # y = e; x: carrier G; y: carrier G |] ==> y = x -|";
+by (res_inst_tac [("x","x")] left_cancellation 1);
+by Auto_tac;
+qed "inv_unique";
+
+Goal "x : carrier G ==> x -| -| = x";
+by (res_inst_tac [("x","x -|")] left_cancellation 1);
+by Auto_tac;
+qed "inv_inv";
+
+Addsimps [inv_inv];
+
+Goal "[| x : carrier G; y : carrier G |] ==> (x # y) -| = y -| # x -|";
+by (rtac (inv_unique RS sym) 1);
+by (subgoal_tac "(x # y) # y -| # x -| = x # (y # y -|) # x -|" 1);
+by (asm_simp_tac (simpset() delsimps [inv_ax1, inv_ax2]
+			    addsimps [binop_assoc]) 2);
+by Auto_tac;
+qed "inv_prod";
 
 
-goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \
-\                     x # y = e |] ==> y = x -|";
-by (res_inst_tac [("x","x")] left_cancellation 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (stac inv_ax1 1);
-by (assume_tac 1);
-by (assume_tac 1);
-val inv_unique = result();
-
-goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x";
-by (res_inst_tac [("x","inverse G x")] left_cancellation 1);
-by (fold_goals_tac [thm "inv_def"]);
-by (afs [inv_closed] 1);
-by (afs [inv_closed] 1);
-by (assume_tac 1);
-by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
-val inv_inv = result();
-
-goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\
-\           ==> (x # y) -| = y -| # x -|";
-by (rtac sym 1);
-by (rtac inv_unique 1);
-by (afs [binop_closed] 1);
-by (afs [inv_closed,binop_closed] 1);
-by (afs [binop_assoc,inv_closed,binop_closed] 1);
-by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (afs [inv_closed] 1);
-by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
-val inv_prod = result();
-
-
-goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\
-\ z : carrier G; y # x =  z # x|] ==> y = z";
+Goal "[| y # x = z # x;  x : carrier G; y : carrier G; \
+\        z : carrier G |] ==> y = z";
 by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
 by (assume_tac 1);
-by (res_inst_tac [("P","%r. y # r = z")] subst 1);
-by (rtac inv_ax1 1);
-by (assume_tac 1);
-by (rtac (binop_assoc RS subst) 1);
+by (res_inst_tac [("P","%r. y # r = z")] (inv_ax1 RS subst) 1);
 by (assume_tac 1);
-by (assume_tac 1);
-by (afs [inv_closed] 1);
-by (etac ssubst 1);
-by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1);
-val right_cancellation = result();
+by (asm_simp_tac (simpset() delsimps [inv_ax1] 
+		  addsimps [binop_assoc RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
+qed "right_cancellation";
+
+Close_locale();
 
 (* example what happens if export *)
 val Left_cancellation = export left_cancellation;
diff -r 2886310fb5e9 -r eb183b062eae src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Tue Nov 10 16:28:08 1998 +0100
+++ b/src/HOL/ex/PiSets.ML	Wed Nov 11 15:44:24 1998 +0100
@@ -5,762 +5,247 @@
 Pi sets and their application.
 *)
 
-(* One abbreviation for my major simp application *)
-fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
-(* strip outer quantifiers and lift implication *)
-fun strip i = (REPEAT ((rtac ballI i) 
-                       ORELSE (rtac allI i)
-                       ORELSE (rtac impI i)));
-(* eresolve but leave the eliminated assumptions (improves unification) *)
-goal HOL.thy "!! P. [| P |] ==> P & P";
-by (Fast_tac 1);
-val double = result();
-
-fun re_tac rule r i = ((rotate_tac (r - 1) i)
-                 THEN (dtac double i)
-                 THEN (rotate_tac ~1 i)
-                 THEN (etac conjE i)
-                 THEN (rotate_tac ~1 i)
-                 THEN (etac rule i));
-
-(* individual theorems for convenient use *)
-val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q";
-by (fold_goals_tac [p1]);
-by (rtac p2 1);
-val apply_def = result();
-
-goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)";
-by (etac ssubst 1);
-by (rtac refl 1);
-val extend = result();
-
-val [p1] = goal HOL.thy "P ==> ~~P";
-by (rtac notI 1);
-by (rtac (p1 RSN(2, notE)) 1);
-by (assume_tac 1);
-val notnotI = result();
-
-val [p1] = goal Set.thy "? x. x: S ==> S ~= {}";
-by (rtac contrapos 1);
-by (rtac (p1 RS notnotI) 1);
-by (etac ssubst 1);
-by (rtac notI 1);
-by (etac exE 1);
-by (etac emptyE 1);
-val ExEl_NotEmpty = result();
-
-
-val [p1] = goal HOL.thy "~x ==> x = False";
-val l1 = (p1 RS (not_def RS apply_def)) RS mp;
-val l2 = read_instantiate [("P","x")] FalseE;
-by (rtac iffI 1);
-by (rtac l1 1);
-by (rtac l2 2);
-by (assume_tac 1);
-by (assume_tac 1);
-val NoteqFalseEq = result();
-
-val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)";
-by (rtac exCI 1);
-(*  1. ! x. ~ P x ==> P ?a *)
-val l1 = p1 RS NoteqFalseEq;
-(* l1 = (! x. ~ P x) = False *)
-val l2 = l1 RS iffD1;
-val l3 = l1 RS iffD2;
-val l4 = read_instantiate [("P", "P ?a")] FalseE;
-by (rtac (l2 RS l4) 1);
-by (assume_tac 1);
-val NotAllNot_Ex = result();
-
-val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)";
-by (rtac notnotD 1);
-by (rtac (p1 RS contrapos) 1);
-by (rtac NotAllNot_Ex 1);
-by (assume_tac 1);
-val NotEx_AllNot = result();
-
-goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}";
-by (Fast_tac 1);
-val NoEl_Empty = result();
-
-goal Set.thy "!!S. S ~= {} ==> ? x. x : S";
-by (Fast_tac 1);
-val NotEmpty_ExEl = result();
-
-goal PiSets.thy "!!S. S = {} ==> ! x. x ~: S";
-by (Fast_tac 1);
-val Empty_NoElem = result();
-
-
-val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)";
-by (stac q1 1);
-by (rtac q2 1);
-val forw_subst = result();
-
-val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)";
-by (rtac (q1 RS subst) 1);
-by (rtac q2 1);
-val forw_ssubst = result();
-
-goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A";
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac refl 1);
-val blow4 = result();
-
-goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)";
-by (Step_tac 1);
-by (afs [fst_conv,snd_conv] 1);
-val apply_pair = result();
-
-goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \
-\ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))";
-by (dtac (blow4 RS forw_subst) 1);
-by (afs [split_def] 1);
-val apply_quadr = result();
-
-goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)";
-by (rtac (surjective_pairing RS subst) 1);
-by (rtac refl 1);
-val surj_pair_forw = result();
-
-goal Prod.thy "!! A B x. x: A Times B ==> fst x: A";
-by (forward_tac [surj_pair_forw] 1);
-by (dtac forw_ssubst 1);
-by (assume_tac 1);
-by (etac SigmaD1 1);
-val TimesE1 = result();
-
-goal Prod.thy "!! A B x. x: A Times B ==> snd x: B";
-by (forward_tac [surj_pair_forw] 1);
-by (dtac forw_ssubst 1);
-by (assume_tac 1);
-by (etac SigmaD2 1);
-val TimesE2 = result();
-
-(* -> and Pi *)
-
-goal PiSets.thy "!! A B. A -> B == {f. ! x. if x: A then f(x) : B else f(x) = (@ y. True)}";
-by (simp_tac (simpset() addsimps [Pi_def]) 1);
-val funcset_def = result();
+(*** -> and Pi ***)
 
 
-val [q1,q2] = goal PiSets.thy 
-"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: Pi A B";
-by (rewtac Pi_def);
-by (rtac CollectI 1);
-by (rtac allI 1);
-by (case_tac "x : A" 1);
-by (stac if_P 1);
-by (assume_tac 1);
-by (etac q1 1);
-by (stac if_not_P 1);
-by (assume_tac 1);
-by (etac q2 1);
-val Pi_I = result();
+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";
 
-goal PiSets.thy 
-"!! A f. [| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A -> B";
-by (afs [Pi_I] 1);
-val funcsetI = result();
+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";
 
-val [q1,q2,q3] = goal PiSets.thy 
-"[| !! x y. [| x: A; y: B |] ==> f x y: C; \
-\   !! x. [| x ~: A |] ==> f x = (@ y. True);\
-\   !! x y. [| x : A; y ~: B |] ==> f x y = (@ y. True)  |] ==> f: A -> B -> C";
-by (simp_tac (simpset() addsimps [q1,q2,q3,funcsetI]) 1);
-val funcsetI2 = result();
+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());
 
-goal PiSets.thy "!! f A B. [|f: A -> B; x: A|] ==> f x: B";
-by (afs [funcset_def] 1);
-val funcsetE1 = 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 PiSets.thy "!! f A B. [|f: Pi A B; x: A|] ==> f x: B x";
-by (afs [Pi_def] 1);
-val PiE1 = result();
-
-goal PiSets.thy "!! f A B. [|f: A -> B; x~: A|] ==> f x = (@ y. True)";
-by (afs [funcset_def] 1);
-val funcsetE2 = result();
+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 PiSets.thy "!! f A B. [|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
-by (afs [Pi_def] 1);
-val PiE2 = result();
+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 PiSets.thy "!! f A B. [|f: A -> B -> C; x : A; y ~: B|] ==> f x y = (@ y. True)";
-by (afs [funcset_def] 1);
-val funcset2E2 = result();
+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 PiSets.thy "!! f A B C. [| f: A -> B -> C; x: A; y: B |] ==> f x y: C";
-by (afs [funcset_def] 1);
-val funcset2E1 = result();
-
-goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\
-\                  ==> f = g";
-by (rtac ext 1);
-by (case_tac "x : A" 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1);
-val function_extensionality = result();
-
-goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\
-\                  ==> f = g";
-by (rtac ext 1);
-by (case_tac "x : A" 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1);
-val Pi_extensionality = result();
-
-(* compose *)
-goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C";
-by (rtac funcsetI 1);
-by (rewrite_goals_tac [compose_def,restrict_def]);  
-by (afs [funcsetE1] 1);
-by (stac if_not_P 1);
-by (assume_tac 1);
-by (rtac refl 1);
-val funcset_compose = result();
-
-goal PiSets.thy "!! A B C f g h. [| 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")] function_extensionality 1);
-by (rtac funcset_compose 1);
-by (rtac funcset_compose 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac funcset_compose 1);
-by (assume_tac 1);
-by (rtac funcset_compose 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac ballI 1);
-by (rewrite_goals_tac [compose_def,restrict_def]);  
-by (afs [funcsetE1,if_P RS ssubst] 1);
-val compose_assoc = result();
-
-goal PiSets.thy "!! A B C f g x. [| f: A -> B; g: B -> C; x: A |]==> compose A g f x = g(f(x))";
-by (afs [compose_def, restrict_def, if_P RS ssubst] 1);
-val composeE1 = result();
-
-goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\
-\                          ==> compose A g f `` A = C";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (rotate_tac 4 1);
-by (etac ssubst 1);
-by (rtac (funcset_compose RS funcsetE1) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac subsetI 1);
-by (hyp_subst_tac 1);
-by (etac imageE 1);
-by (rotate_tac 3 1);
-by (etac ssubst 1);
-by (etac imageE 1);
-by (rotate_tac 3 1);
-by (etac ssubst 1);
-by (etac (composeE1 RS subst) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rtac imageI 1);
-by (assume_tac 1);
-val surj_compose = result();
+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";
 
 
-goal PiSets.thy "!! A B C g f.[| 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 (rtac inj_onI 1);
-by (forward_tac [composeE1] 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (forward_tac [composeE1] 1);
-by (assume_tac 1);
-by (rotate_tac 7 1);
-by (assume_tac 1);
-by (step_tac (claset() addSEs [inj_onD]) 1);
-by (rotate_tac 5 1);
-by (etac subst 1);
-by (etac subst 1);
-by (assume_tac 1);
-by (etac imageI 1);
-by (etac imageI 1);
-val inj_on_compose = result();
+(*** 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";
 
 
-(* restrict / lam *)
-goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B";
-by (rewtac restrict_def);
-by (rtac funcsetI 1);
-by (afs [if_P RS ssubst] 1);
-by (etac subsetD 1);
-by (etac imageI 1);
-by (afs [if_not_P RS ssubst] 1);
-val restrict_in_funcset = result();
-
-goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B";
-by (rtac restrict_in_funcset 1);
-by (afs [image_def] 1);
-by (Step_tac 1);
-by (Fast_tac 1);
-val restrictI = result();
-
-goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B";
-by (rewtac restrict_def);
-by (rtac Pi_I 1);
-by (afs [if_P RS ssubst] 1);
-by (Asm_full_simp_tac 1);
-val restrictI_Pi = result();
+Goal "x: A ==> (lam y: A. f y) x = f x";
+by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
+qed "restrict_apply1";
 
-(* The following proof has to be redone *)
-goal PiSets.thy "!! f A B C.[| f `` A  <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
-by (rtac restrict_in_funcset 1);
-by (afs [image_def] 1);
-by (afs [Pi_def,subset_def] 1);
-by (afs [restrict_def] 1);
-by (Step_tac 1);
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","f xa")] spec 1);
-by (dtac mp 1);
-by (rtac bexI 1);
-by (rtac refl 1);
-by (assume_tac 1);
-by (dres_inst_tac [("x","xb")] spec 1);
-by (Asm_full_simp_tac 1);
-(* fini 1 *)
-by (Asm_full_simp_tac 1);
-val restrict_in_funcset2 = result();
+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 PiSets.thy "!! f A B C.[| !x: A. ! y: B. f x y: C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
-by (rtac restrict_in_funcset 1);
-by (afs [image_def] 1);
-by (afs [Pi_def,subset_def] 1);
-by (afs [restrict_def] 1);
-by (Step_tac 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-val restrictI2 = result();
+Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
+by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
+qed "restrict_apply2";
 
 
-(* goal PiSets.thy "!! f A B. [| f `` A <= UNION A B |] ==> (lam x: A. f x) : Pi A B"; *)
-
-goal PiSets.thy "!! f A B. [| x: A |] ==> (lam y: A. f y) x = f x";
-by (afs [restrict_def] 1);
-val restrictE1 = result();
-
-goal PiSets.thy "!! f A B. [| x: A; f : A -> B |] ==> (lam y: A. f y) x : B";
-by (afs [restrictE1,funcsetE1] 1);
-val restrictE1a = result();
-
-goal PiSets.thy "!! f A B. [| x ~: A |] ==> (lam y: A. f y) x =  (@ y. True)";
-by (afs [restrict_def] 1);
-val restrictE2 = result();
-
-(* It would be nice to have this, but this doesn't work unfortunately
-   see PiSets.ML: Pi_subset1 
-goal PiSets.thy "!! A B. [| A <= B ; ! x: A. f x : C|] ==> (lam x: B. f(x)): A -> C"; *)
-
-goal PiSets.thy "!! f A B x y. [| x: A; y: B |] ==> \
-\               (lam a: A. lam b: B. f a b) x y = f x y";
-by (afs [restrictE1] 1);
-val restrict2E1 = result();
-
-(* New restrict2E1:  *)
-goal PiSets.thy "!! A B. [| x : A; y : B x|] ==> (lam a:A. lam b: (B a). f a b) x y = f x y" ;
-by (afs [restrictE1] 1);
-val restrict2E1a = result();
-
-goal PiSets.thy "!! f A B x y. [| x: A; y: B; z: C |] ==> \
-\     (lam a: A. lam b: B. lam c: C. f a b c) x y z = f x y z";
-by (afs [restrictE1] 1);
-val restrict3E1 = result();
-
-goal PiSets.thy "!! f A B x y. [| x: A; y ~: B |] ==> \
-\           (lam a: A. lam b: B. f a b) x y = (@ y. True)";
-by (afs [restrictE1,restrictE2] 1);
-val restrict2E2 = result();
+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";
 
 
-goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\
-\                             ==> (lam x: A. f x) = (lam x: A. g x)";
-by (rtac ext 1);
-by (case_tac "x: A" 1);
-by (afs [restrictE1] 1);
-by (afs [restrictE2] 1);
-val restrict_ext = result();
-
-(* Invers *)
+(*** Inverse ***)
 
-goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x";
-by (rewtac image_def);
-by (dtac equalityD2 1);
-by (dtac subsetD 1);
-by (assume_tac 1);
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (dtac sym 1);
-by (etac bexI 1);
-by (assume_tac 1);
-val surj_image = result();
+Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
+by (Blast_tac 1);
+qed "surj_image";
 
-val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \
-\             ==> (lam x: B. (Inv A f) x) : B -> A";
-by (rtac restrict_in_funcset 1);
-by (rewtac image_def);
-by (rtac subsetI 1); 
-by (dtac CollectD 1);
-by (etac bexE 1);
-by (etac ssubst 1);
-by (dtac (q1 RS surj_image) 1);
-by (etac bexE 1);
-by (etac subst 1);
-by (rewtac Inv_def);
-by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1);
-by (rtac (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
-by (etac (q2 RS funcsetE1) 1);
-val Inv_funcset = result();
+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";
 
 
-val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
-\                ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x";
-by (rtac ballI 1);
-by (stac restrictE1 1);
-by (etac (q1 RS funcsetE1) 1);
-by (rewtac Inv_def); 
-by (rtac (q2 RS inj_onD) 1);
-by (assume_tac 3);
-by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1);
-by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
-by (etac (q1 RS funcsetE1) 1);
-by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1);
-by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
-by (etac (q1 RS funcsetE1) 1);
-val Inv_f_f = result();
+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";
 
-val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\
-\                ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x";
-by (rtac ballI 1);
-by (stac restrictE1 1);
-by (assume_tac 1);
-by (rewtac Inv_def); 
-by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1);
-by (rtac (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
-by (assume_tac 1);
-val f_Inv_f = result();
+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";
 
-val [q1,q2,q3] = goal PiSets.thy "[| 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 function_extensionality 1);
-by (rtac funcset_compose 1);
-by (rtac q1 1);
-by (rtac (q1 RS (q3 RS Inv_funcset)) 1);
-by (rtac restrict_in_funcset 1);
-by (Fast_tac 1);
-by (rtac ballI 1);
-by (afs [compose_def] 1);
-by (stac restrictE1 1);
-by (assume_tac 1);
-by (stac restrictE1 1);
-by (assume_tac 1);
-by (etac (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1);
-val comp_Inv_id = result();
+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 @@ *)
+(*** Pi and its application @@ ***)
 
-goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}";
-by (dtac NotEmpty_ExEl 1);
-by (etac exE 1);
-by (rewtac Pi_def);
-by (dtac CollectD 1);
-by (rtac ballI 1);
-by (rtac ExEl_NotEmpty 1);
-by (res_inst_tac [("x","x xa")] exI 1);
-by (afs [if_P RS subst] 1);
-val Pi_total1 = result();
-
-goal Set.thy "!! M P. ? x: M . P x ==> (~ (! x: M. ~ P x))";
-by (Fast_tac 1);
-val SetEx_NotNotAll = result();
-
-goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}";
-by (rtac notnotD 1);
-by (rtac (Pi_total1 RSN(2,contrapos)) 1);
-by (assume_tac 2); 
-by (etac SetEx_NotNotAll 1);
-val Pi_total2 = result();
+Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
+by Auto_tac;
+qed "Pi_eq_empty";
 
-val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)";
-by (rewtac Fset_apply_def);
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (etac ssubst 1);
-by (rewtac Pi_def);
-by (dtac CollectD 1);
-by (dtac spec 1);
-by (rtac (q1 RS if_P RS subst) 1);  
-by (assume_tac 1);
-by (rtac subsetI 1);
-by (rewtac image_def);
-by (rtac CollectI 1);
-by (rtac exE 1);
-by (rtac (q2 RS NotEmpty_ExEl) 1);
-by (res_inst_tac [("x","%y. if  (y = a) then  x else xa y")] bexI 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (rtac allI 1);
-by (case_tac "xb: A" 1);
-by (afs [if_P RS ssubst] 1);
-by (case_tac "xb = a" 1);
-by (afs [if_P RS ssubst] 1);
-by (afs [if_not_P RS ssubst] 1);
-by (rewtac Pi_def);
-by (afs [if_P RS ssubst] 1);
-by (afs [if_not_P RS ssubst] 1);
-by (case_tac "xb = a" 1);
-by (afs [if_P RS ssubst] 1);
-by (hyp_subst_tac 1);
-by (afs [q1] 1);
-by (afs [if_not_P RS ssubst] 1);
-val Pi_app_def = result();
+Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
+by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
+qed "Pi_total1";
 
-goal PiSets.thy "!! a A B C. [| a: A; (PI x: A. PI y: B x. C x y) ~= {} |] ==>  (PI y: B a. C a y) ~= {}";
-by (dtac NotEmpty_ExEl 1);
-by (etac exE 1);
-by (rewtac Pi_def);
-by (dtac CollectD 1);
-by (dtac spec 1);
-by (rtac ExEl_NotEmpty 1);
-by (rtac exI 1);
-by (etac (if_P RS eq_reflection RS apply_def) 1);
-by (assume_tac 1);
-val NotEmptyPiStep = result();
+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";
+
 
-val [q1,q2,q3] = goal PiSets.thy 
-"[|a : A; b: B a; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI x: A. PI y: B x. C x y) @@ a @@ b = C a b";
-by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]);
-by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]);
-by (rtac refl 1);
-val Pi_app2_def = result();
+(*** 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(),
+	      simpset() addsimps [PiBij_def,Pi_def,restrict_apply1]));
+qed "PiBij_subset_Sigma";
 
-(* Sigma does a better job ( the following is from PiSig.ML) *)
-goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\
-\ ==>  Sigma A B ^^ {a} = Pi A B @@ a";
-by (stac Pi_app_def 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1);
-by (rewtac Bex_def);
-by (Fast_tac 1);
-val PiSig_image_eq = result();
-
-goal PiSets.thy "!! A b a. [| a: A |]\
-\ ==>  Sigma A B ^^ {a} = B a";
-by (Fast_tac 1);
-val Sigma_app_def = result();
-
-(* Bijection between Pi in terms of => and Pi in terms of Sigma *)
-goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B";
-by (afs [PiBij_def,Pi_def,restrictE1] 1);
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (dtac CollectD 1);
-by (Asm_full_simp_tac 1);
-val PiBij_subset_Sigma = result();
+Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
+by (auto_tac (claset(),
+	      simpset() addsimps [PiBij_def,restrict_apply1]));
+qed "PiBij_unique";
 
-goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
-by (afs [PiBij_def,restrictE1] 1);
-by (rtac ballI 1);
-by (rtac ex1I 1);
-by (assume_tac 2);
-by (rtac refl 1);
-val PiBij_unique = result();
-
-goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))";
-by (afs [PiBij_def,restrictE1] 1);
-by (rtac ballI 1);
-by (rtac ex1I 1);
-by (etac conjunct2 2);
-by (afs [PiE1] 1);
-val PiBij_unique2 = result();
-
-goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f : Graph A B";
-by (afs [Graph_def,PiBij_unique,PiBij_subset_Sigma] 1);
-val PiBij_in_Graph = result();
+Goal "f: Pi A B ==> PiBij A B f : Graph A B";
+by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
+				      PiBij_subset_Sigma]) 1);
+qed "PiBij_in_Graph";
 
-goal PiSets.thy "!! A B. PiBij A B:  Pi A B -> Graph A B";
-by (afs [PiBij_def] 1);
+Goalw [PiBij_def, Graph_def] "PiBij A B:  Pi A B -> Graph A B";
 by (rtac restrictI 1);
-by (strip 1);
-by (afs [Graph_def] 1);
-by (rtac conjI 1);
-by (rtac subsetI 1);
-by (strip 2);
-by (rtac ex1I 2);
-by (rtac refl 2);
-by (assume_tac 2);
-by (split_all_tac 1);
-by (afs [Pi_def] 1);
-val PiBij_func = result();
+by (auto_tac (claset(), simpset() addsimps [Pi_def]));
+qed "PiBij_func";
 
-goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B;  \
-\       {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\
-\                ==> f x = g x";
-by (etac equalityE 1);
-by (rewtac subset_def);
-by (Auto_tac);
-val set_eq_lemma = result();
-
-goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
+Goal "inj_on (PiBij A B) (Pi A B)";
 by (rtac inj_onI 1);
 by (rtac Pi_extensionality 1);			
 by (assume_tac 1);
 by (assume_tac 1);
-by (strip 1);
-by (afs [PiBij_def,restrictE1] 1);
-by (re_tac set_eq_lemma 2 1);
-by (assume_tac 1);
-by (assume_tac 2);
-by (afs [restrictE1] 1);
-by (etac subst 1);
-by (afs [restrictE1] 1);
-val inj_PiBij = result();
+by (rotate_tac 1 1);
+by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1);
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "inj_PiBij";
 
-goal HOL.thy "!! P . ?! x. P x ==> ? x. P x";
-by (Blast_tac 1);
-val Ex1_Ex = result();
+
 
-goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
+Goal "PiBij A B `` (Pi A B) = Graph A B";
 by (rtac equalityI 1);
 by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
 by (rtac subsetI 1);
-by (afs [image_def] 1);
+by (asm_full_simp_tac (simpset() addsimps [image_def]) 1);
 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
- by (rtac restrictI_Pi 2);
- by (strip 2);
- by (rtac ex1E 2);
-  by (afs [Graph_def] 2);
-  by (etac conjE 2);
-  by (dtac bspec 2);
-   by (assume_tac 2);
-  by (assume_tac 2);
- by (stac select_equality 2);
+ by (rtac restrictI 2);
+ by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);
+  by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);
+ by (full_simp_tac (simpset() addsimps [Graph_def]) 2);
+  by (stac select_equality 2);
    by (assume_tac 2);
   by (Blast_tac 2);
-(* gets hung up on by (afs [Graph_def] 2); *)
- by (SELECT_GOAL (rewtac Graph_def) 2);
  by (Blast_tac 2);
 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
-by (afs [PiBij_def,Graph_def] 1);
-by (stac restrictE1 1);
- by (rtac restrictI_Pi 1);
-(* again like the old 2. subgoal *)
- by (strip 1);
- by (rtac ex1E 1);
-  by (etac conjE 1);
-  by (dtac bspec 1);
-   by (assume_tac 1);
-  by (assume_tac 1);
- by (stac select_equality 1);
-   by (assume_tac 1);
-  by (Blast_tac 1);
- by (Blast_tac 1);
-(* *)
+by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);
+by (stac restrict_apply1 1);
+ by (rtac restrictI 1);
+ by (blast_tac (claset() addSDs [[select_eq_Ex, ex1_implies_ex] MRS iffD2]) 1);
+(** LEVEL 17 **)
 by (rtac equalityI 1);
 by (rtac subsetI 1);
- by (rtac CollectI 1);
- by (split_all_tac 1);
- by (Simp_tac 1);
- by (rtac conjI 1);
-  by (Blast_tac 1);
- by (etac conjE 1);
- by (dtac subsetD 1);
-  by (assume_tac 1);
- by (dtac SigmaD1 1);
- by (dtac bspec 1);
-  by (assume_tac 1);
- by (stac restrictE1 1);
-  by (assume_tac 1);
- by (rtac sym 1);
- by (rtac select_equality 1);
-  by (assume_tac 1);
- by (Blast_tac 1);
+by (split_all_tac 1);
+by (subgoal_tac "a: A" 1);
+by (Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
+(*Blast_tac: PROOF FAILED for depth 5*)
+by (fast_tac (claset() addSIs [select1_equality RS sym]) 1);
 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
-by (rtac subsetI 1);
-by (Asm_full_simp_tac 1);
-by (split_all_tac 1);
-by (Asm_full_simp_tac 1);
-by (etac conjE 1);
-by (etac conjE 1);
-by (afs [restrictE1] 1);
-by (dtac bspec 1);
- by (assume_tac 1);
-by (dtac Ex1_Ex 1);
-by (rewtac Ex_def);
-by (assume_tac 1);
-val surj_PiBij = result();
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
+by (fast_tac (claset() addIs [selectI2]) 1);
+qed "surj_PiBij";
 
+Goal "f: Pi A B ==> \
+\     (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
+by (asm_simp_tac
+    (simpset() addsimps [Inv_f_f, PiBij_func, inj_PiBij, surj_PiBij]) 1);
+qed "PiBij_bij1";
 
-goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \
-\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
-by (rtac (Inv_f_f  RS bspec) 1);
-by (assume_tac 4);
-by (afs [PiBij_func] 1);
-by (afs [inj_PiBij] 1);
-by (afs [surj_PiBij] 1);
-val PiBij_bij1 = result();
-
-goal PiSets.thy "!! A B. [| f: Graph A B  |] ==> \
+Goal "[| f: Graph A B  |] ==> \
 \    (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
-by (rtac (PiBij_func RS (f_Inv_f RS bspec)) 1);
-by (afs [surj_PiBij] 1);
+by (rtac (PiBij_func RS f_Inv_f) 1);
+by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
 by (assume_tac 1);
-val PiBij_bij2 = result();
+qed "PiBij_bij2";
 
-goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f";
-by (rtac injI 1);
-by (dres_inst_tac [("f","g")] arg_cong 1);
-by (forw_inst_tac [("x","x")] spec 1);
-by (rotate_tac 2 1);
-by (etac subst 1);
-by (forw_inst_tac [("x","y")] spec 1);
-by (rotate_tac 2 1);
-by (etac subst 1);
-by (assume_tac 1);
-val inj_lemma = result();
+Goal "Pi {} B = {f. !x. f x = (@ y. True)}";
+by (asm_full_simp_tac (simpset() addsimps [Pi_def]) 1);
+qed "empty_Pi";
 
-goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g";
-by (afs [surj_def] 1);
-by (rtac allI 1);
-by (res_inst_tac [("x","f y")] exI 1);
-by (dtac spec 1);
-by (etac sym 1);
-val surj_lemma = result();
-
-goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}";
-by (afs [Pi_def] 1);
-val empty_Pi = result();
+Goal "(% x. (@ y. True)) : Pi {} B";
+by (simp_tac (simpset() addsimps [empty_Pi]) 1);
+qed "empty_Pi_func";
 
-goal PiSets.thy "(% x. (@ y. True)) : Pi {} B";
-by (afs [empty_Pi] 1);
-val empty_Pi_func = result();
-
-goal Set.thy "!! A B. [| A <= B; x ~: B |] ==> x ~: A";
-by (Blast_tac 1);
-val subsetND = result();
-
-
-goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C";
-by (rtac subsetI 1);
-by (rtac Pi_I 1);
-by (afs [Pi_def] 2);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (etac subsetD 1);
-by (afs [PiE1] 1);
-val Pi_subset1 = result();
+val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
+by (auto_tac (claset(),
+	      simpset() addsimps [impOfSubs major]));
+qed "Pi_mono";