# HG changeset patch
# User paulson
# Date 935761330 -7200
# Node ID 2cb340e66d1514d3f267616a1cfd9ab71055bfde
# Parent  dec7b838f5cb6d10871e1abd9772f0a83d8b0763
tidied, allowing pattern-matching in defs of zadd and zmult

diff -r dec7b838f5cb -r 2cb340e66d15 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Fri Aug 27 15:41:11 1999 +0200
+++ b/src/HOL/Integ/Equiv.ML	Fri Aug 27 15:42:10 1999 +0200
@@ -8,10 +8,6 @@
 
 val RSLIST = curry (op MRS);
 
-open Equiv;
-
-Delrules [equalityI];
-
 (*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***)
 
 (** first half: equiv A r ==> r^-1 O r = r **)
@@ -110,23 +106,24 @@
 
 Goalw [equiv_def,refl_def,quotient_def]
     "equiv A r ==> Union(A/r) = A";
-by (blast_tac (claset() addSIs [equalityI]) 1);
+by (Blast_tac 1);
 qed "Union_quotient";
 
 Goalw [quotient_def]
     "[| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y = {})";
-by (safe_tac (claset() addSIs [equiv_class_eq]));
+by (Clarify_tac 1);
+by (rtac equiv_class_eq 1);
 by (assume_tac 1);
 by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
-by (blast_tac (claset() addSIs [equalityI]) 1);
+by (Blast_tac 1);
 qed "quotient_disj";
 
 
 (**** Defining unary operations upon equivalence classes ****)
 
 (* theorem needed to prove UN_equiv_class *)
-goal Set.thy "!!A. [| a:A; ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
-by (fast_tac (claset() addSEs [equalityE] addSIs [equalityI]) 1);
+Goal "[| a:A;  ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
+by Auto_tac;
 qed "UN_constant_eq";
 
 
@@ -139,7 +136,7 @@
 \     ==> (UN x:r^^{a}. b(x)) = b(a)";
 by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1));
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
-by (Blast_tac 1);
+by (blast_tac (claset() delrules [equalityI]) 1);
 qed "UN_equiv_class";
 
 (*type checking of  UN x:r``{a}. b(x) *)
@@ -186,7 +183,7 @@
 by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
                                      congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
-by (Blast_tac 1);
+by (blast_tac (claset() delrules [equalityI]) 1);
 qed "congruent2_implies_congruent_UN";
 
 Goal "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
@@ -209,6 +206,12 @@
                              congruent2_implies_congruent, quotientI]) 1));
 qed "UN_equiv_class_type2";
 
+(*Allows a natural expression of binary operators, without explicit calls
+  to "split"*)
+Goal "(UN (x1,x2):X. UN (y1,y2):Y. A x1 x2 y1 y2) = \
+\     (UN x:X. UN y:Y. split(%x1 x2. split(%y1 y2. A x1 x2 y1 y2) y) x)";
+by Auto_tac;
+qed "UN_UN_split_split_eq";
 
 (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   than the direct proof*)
@@ -253,12 +256,11 @@
 by (Blast_tac 1);
 qed "finite_equiv_class";
 
-Goal "[| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] \
-\              ==> k dvd card(A)";
+Goal "[| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] ==> k dvd card(A)";
 by (rtac (Union_quotient RS subst) 1);
 by (assume_tac 1);
 by (rtac dvd_partition 1);
-by (blast_tac (claset() delrules [equalityI] addEs [quotient_disj RS disjE]) 4);
+by (blast_tac (claset() addEs [quotient_disj RS disjE]) 4);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [Union_quotient, equiv_type, 
 				      finite_quotient])));
diff -r dec7b838f5cb -r 2cb340e66d15 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Fri Aug 27 15:41:11 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Fri Aug 27 15:42:10 1999 +0200
@@ -53,15 +53,12 @@
 qed "intrel_refl";
 
 Goalw [equiv_def, refl_def, sym_def, trans_def]
-    "equiv {x::(nat*nat).True} intrel";
+    "equiv UNIV intrel";
 by (fast_tac (claset() addSIs [intrel_refl] 
-                        addSEs [sym, integ_trans_lemma]) 1);
+                       addSEs [sym, integ_trans_lemma]) 1);
 qed "equiv_intrel";
 
-val equiv_intrel_iff =
-    [TrueI, TrueI] MRS 
-    ([CollectI, CollectI] MRS 
-    (equiv_intrel RS eq_equiv_class_iff));
+val equiv_intrel_iff = [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
 
 Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
 by (Fast_tac 1);
@@ -98,24 +95,18 @@
 
 (**** zminus: unary negation on Integ ****)
 
-Goalw [congruent_def]
-  "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
-by Safe_tac;
+Goalw [congruent_def] "congruent intrel (%(x,y). intrel^^{(y,x)})";
+by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps add_ac) 1);
 qed "zminus_congruent";
 
-
-(*Resolve th against the corresponding facts for zminus*)
-val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
-
 Goalw [zminus_def]
       "- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
-by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
-   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
+	      [equiv_intrel RS UN_equiv_class, zminus_congruent]) 1);
 qed "zminus";
 
-(*by lcp*)
+(*Every integer can be written in the form Abs_Integ(...) *)
 val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
@@ -160,24 +151,13 @@
 
 (**** zadd: addition on Integ ****)
 
-(** Congruence property for addition **)
-
-Goalw [congruent2_def]
-    "congruent2 intrel (%p1 p2.                  \
-\         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
-(*Proof via congruent2_commuteI seems longer*)
-by Safe_tac;
-by (Asm_simp_tac 1);
-qed "zadd_congruent2";
-
-(*Resolve th against the corresponding facts for zadd*)
-val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
-
 Goalw [zadd_def]
   "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
 \  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
-by (asm_simp_tac
-    (simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
+by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1);
+by (stac (equiv_intrel RS UN_equiv_class2) 1);
+(*Congruence property for addition*)
+by (auto_tac (claset(), simpset() addsimps [congruent2_def]));
 qed "zadd";
 
 Goal "- (z + w) = (- z) + (- w::int)";
@@ -285,24 +265,22 @@
 
 (**** zmult: multiplication on Integ ****)
 
-(** Congruence property for multiplication **)
-
 Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
 by (simp_tac (simpset() addsimps add_ac) 1);
 qed "zmult_congruent_lemma";
 
-Goal "congruent2 intrel (%p1 p2.                 \
-\               split (%x1 y1. split (%x2 y2.   \
+(*Congruence property for multiplication*)
+Goal "congruent2 intrel \
+\       (%p1 p2. (%(x1,y1). (%(x2,y2).   \
 \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
 by (pair_tac "w" 2);
 by (rename_tac "z1 z2" 2);
-by Safe_tac;
-by (rewtac split_def);
+by (ALLGOALS Clarify_tac);
 by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
 by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
-                           addsimps add_ac@mult_ac) 1);
-by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
+                            addsimps add_ac@mult_ac) 1);
+by (rtac ([equiv_intrel, intrelI] MRS equiv_class_eq) 1);
 by (rtac (zmult_congruent_lemma RS trans) 1);
 by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
 by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
@@ -311,13 +289,12 @@
 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
 qed "zmult_congruent2";
 
-(*Resolve th against the corresponding facts for zmult*)
-val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
-
 Goalw [zmult_def]
    "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) =   \
 \   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
-by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2,
+			 equiv_intrel RS UN_equiv_class2]) 1);
 qed "zmult";
 
 Goal "(- z) * w = - (z * (w::int))";
diff -r dec7b838f5cb -r 2cb340e66d15 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Aug 27 15:41:11 1999 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Aug 27 15:42:10 1999 +0200
@@ -12,14 +12,14 @@
   "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Integ)
-  int = "{x::(nat*nat).True}/intrel"            (Equiv.quotient_def)
+  int = "UNIV/intrel"            (Equiv.quotient_def)
 
 instance
   int :: {ord, plus, times, minus}
 
 defs
   zminus_def
-    "- Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
+    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel^^{(y,x)})"
 
 constdefs
 
@@ -36,8 +36,8 @@
 defs
   zadd_def
    "z + w == 
-       Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w).   
-           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
+       Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
+		 intrel^^{(x1+x2, y1+y2)})"
 
   zdiff_def "z - (w::int) == z + (-w)"
 
@@ -47,7 +47,7 @@
 
   zmult_def
    "z * w == 
-       Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w). split (%x1 y1.   
-           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
+       Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
+		 intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
 
 end