Changed some definitions and proofs to use pattern-matching.

--- a/src/ZF/ex/Integ.ML	Thu May 04 02:02:18 1995 +0200
+++ b/src/ZF/ex/Integ.ML	Thu May 04 02:02:54 1995 +0200
@@ -203,11 +203,12 @@
 (** Congruence property for addition **)
 
 goalw Integ.thy [congruent2_def]
-    "congruent2(intrel, %p1 p2.                  \
-\         split(%x1 y1. split(%x2 y2. intrel `` {<x1#+x2, y1#+y2>}, p2), p1))";
+    "congruent2(intrel, %z1 z2.     	             \
+\         let <x1,y1>=z1; <x2,y2>=z2                 \
+\                           in intrel``{<x1#+x2, y1#+y2>})";
 (*Proof via congruent2_commuteI seems longer*)
 by (safe_tac intrel_cs);
-by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1);
+by (asm_simp_tac (intrel_ss addsimps [add_assoc, Let_def]) 1);
 (*The rest should be trivial, but rearranging terms is hard;
   add_ac does not help rewriting with the assumptions.*)
 by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
@@ -216,14 +217,14 @@
 by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
 qed "zadd_congruent2";
 
-
 (*Resolve th against the corresponding facts for zadd*)
 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
 
 goalw Integ.thy [integ_def,zadd_def]
     "!!z w. [| z: integ;  w: integ |] ==> z $+ w : integ";
-by (REPEAT (ares_tac [zadd_ize UN_equiv_class_type2,
-		      split_type, add_type, quotientI, SigmaI] 1));
+by (rtac (zadd_ize UN_equiv_class_type2) 1);
+by (simp_tac (ZF_ss addsimps [Let_def]) 3);
+by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
 qed "zadd_type";
 
 goalw Integ.thy [zadd_def]
@@ -231,6 +232,7 @@
 \           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =	\
 \	    intrel `` {<x1#+x2, y1#+y2>}";
 by (asm_simp_tac (ZF_ss addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
+by (simp_tac (ZF_ss addsimps [Let_def]) 1);
 qed "zadd";
 
 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";

--- a/src/ZF/ex/Integ.thy	Thu May 04 02:02:18 1995 +0200
+++ b/src/ZF/ex/Integ.thy	Thu May 04 02:02:54 1995 +0200
@@ -30,25 +30,29 @@
     
     znat_def	"$# m == intrel `` {<m,0>}"
     
-    zminus_def	"$~ Z == UN p:Z. split(%x y. intrel``{<y,x>}, p)"
+    zminus_def	"$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
     
     znegative_def
 	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
     
     zmagnitude_def
-	"zmagnitude(Z) == UN p:Z. split(%x y. (y#-x) #+ (x#-y), p)"
+	"zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
     
+    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
+      Perhaps a "curried" or even polymorphic congruent predicate would be
+      better.*)
     zadd_def
      "Z1 $+ Z2 == \
-\       UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. 		\
-\                                         intrel``{<x1#+x2, y1#+y2>}, p2), p1)"
+\       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 \
+\                           in intrel``{<x1#+x2, y1#+y2>}"
     
     zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
     zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
     
+    (*This illustrates the primitive form of definitions (no patterns)*)
     zmult_def
      "Z1 $* Z2 == \
-\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2. 	\
+\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        \
 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
     
  end

--- a/src/ZF/ex/misc.ML	Thu May 04 02:02:18 1995 +0200
+++ b/src/ZF/ex/misc.ML	Thu May 04 02:02:54 1995 +0200
@@ -145,7 +145,7 @@
 goal (merge_theories(Sum.thy,Perm.thy))
     "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
 \    : bij(Pow(A+B), Pow(A)*Pow(B))";
-by (res_inst_tac [("d", "split(%X Y.{Inl(x).x:X} Un {Inr(y).y:Y})")] 
+by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
     lam_bijective 1);
 by (TRYALL (etac SigmaE));
 by (ALLGOALS (asm_simp_tac ZF_ss));