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