1.1 --- a/src/ZF/ex/Integ.ML	Thu May 04 02:02:18 1995 +0200
     1.2 +++ b/src/ZF/ex/Integ.ML	Thu May 04 02:02:54 1995 +0200
     1.3 @@ -203,11 +203,12 @@
     1.4  (** Congruence property for addition **)
     1.5  
     1.6  goalw Integ.thy [congruent2_def]
     1.7 -    "congruent2(intrel, %p1 p2.                  \
     1.8 -\         split(%x1 y1. split(%x2 y2. intrel `` {<x1#+x2, y1#+y2>}, p2), p1))";
     1.9 +    "congruent2(intrel, %z1 z2.     	             \
    1.10 +\         let <x1,y1>=z1; <x2,y2>=z2                 \
    1.11 +\                           in intrel``{<x1#+x2, y1#+y2>})";
    1.12  (*Proof via congruent2_commuteI seems longer*)
    1.13  by (safe_tac intrel_cs);
    1.14 -by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1);
    1.15 +by (asm_simp_tac (intrel_ss addsimps [add_assoc, Let_def]) 1);
    1.16  (*The rest should be trivial, but rearranging terms is hard;
    1.17    add_ac does not help rewriting with the assumptions.*)
    1.18  by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
    1.19 @@ -216,14 +217,14 @@
    1.20  by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
    1.21  qed "zadd_congruent2";
    1.22  
    1.23 -
    1.24  (*Resolve th against the corresponding facts for zadd*)
    1.25  val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
    1.26  
    1.27  goalw Integ.thy [integ_def,zadd_def]
    1.28      "!!z w. [| z: integ;  w: integ |] ==> z $+ w : integ";
    1.29 -by (REPEAT (ares_tac [zadd_ize UN_equiv_class_type2,
    1.30 -		      split_type, add_type, quotientI, SigmaI] 1));
    1.31 +by (rtac (zadd_ize UN_equiv_class_type2) 1);
    1.32 +by (simp_tac (ZF_ss addsimps [Let_def]) 3);
    1.33 +by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
    1.34  qed "zadd_type";
    1.35  
    1.36  goalw Integ.thy [zadd_def]
    1.37 @@ -231,6 +232,7 @@
    1.38  \           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =	\
    1.39  \	    intrel `` {<x1#+x2, y1#+y2>}";
    1.40  by (asm_simp_tac (ZF_ss addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
    1.41 +by (simp_tac (ZF_ss addsimps [Let_def]) 1);
    1.42  qed "zadd";
    1.43  
    1.44  goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";

     2.1 --- a/src/ZF/ex/Integ.thy	Thu May 04 02:02:18 1995 +0200
     2.2 +++ b/src/ZF/ex/Integ.thy	Thu May 04 02:02:54 1995 +0200
     2.3 @@ -30,25 +30,29 @@
     2.4      
     2.5      znat_def	"$# m == intrel `` {<m,0>}"
     2.6      
     2.7 -    zminus_def	"$~ Z == UN p:Z. split(%x y. intrel``{<y,x>}, p)"
     2.8 +    zminus_def	"$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
     2.9      
    2.10      znegative_def
    2.11  	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    2.12      
    2.13      zmagnitude_def
    2.14 -	"zmagnitude(Z) == UN p:Z. split(%x y. (y#-x) #+ (x#-y), p)"
    2.15 +	"zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
    2.16      
    2.17 +    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    2.18 +      Perhaps a "curried" or even polymorphic congruent predicate would be
    2.19 +      better.*)
    2.20      zadd_def
    2.21       "Z1 $+ Z2 == \
    2.22 -\       UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2. 		\
    2.23 -\                                         intrel``{<x1#+x2, y1#+y2>}, p2), p1)"
    2.24 +\       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 \
    2.25 +\                           in intrel``{<x1#+x2, y1#+y2>}"
    2.26      
    2.27      zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    2.28      zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
    2.29      
    2.30 +    (*This illustrates the primitive form of definitions (no patterns)*)
    2.31      zmult_def
    2.32       "Z1 $* Z2 == \
    2.33 -\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2. 	\
    2.34 +\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        \
    2.35  \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    2.36      
    2.37   end

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