--- a/src/HOL/Integ/Equiv.ML Wed Jul 19 12:33:19 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML Wed Jul 19 12:33:36 2000 +0200
@@ -6,24 +6,20 @@
Equivalence relations in HOL Set Theory
*)
-val RSLIST = curry (op MRS);
-
(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***)
(** first half: equiv A r ==> r^-1 O r = r **)
Goalw [trans_def,sym_def,converse_def]
- "[| sym(r); trans(r) |] ==> r^-1 O r <= r";
+ "[| sym(r); trans(r) |] ==> r^-1 O r <= r";
by (Blast_tac 1);
qed "sym_trans_comp_subset";
-Goalw [refl_def]
- "refl A r ==> r <= r^-1 O r";
+Goalw [refl_def] "refl A r ==> r <= r^-1 O r";
by (Blast_tac 1);
qed "refl_comp_subset";
-Goalw [equiv_def]
- "equiv A r ==> r^-1 O r = r";
+Goalw [equiv_def] "equiv A r ==> r^-1 O r = r";
by (Clarify_tac 1);
by (rtac equalityI 1);
by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1));
@@ -31,7 +27,7 @@
(*second half*)
Goalw [equiv_def,refl_def,sym_def,trans_def]
- "[| r^-1 O r = r; Domain(r) = A |] ==> equiv A r";
+ "[| r^-1 O r = r; Domain(r) = A |] ==> equiv A r";
by (etac equalityE 1);
by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
by (ALLGOALS Fast_tac);
@@ -41,7 +37,7 @@
(*Lemma for the next result*)
Goalw [equiv_def,trans_def,sym_def]
- "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
+ "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
by (Blast_tac 1);
qed "equiv_class_subset";
@@ -51,8 +47,7 @@
by (Blast_tac 1);
qed "equiv_class_eq";
-Goalw [equiv_def,refl_def]
- "[| equiv A r; a: A |] ==> a: r^^{a}";
+Goalw [equiv_def,refl_def] "[| equiv A r; a: A |] ==> a: r^^{a}";
by (Blast_tac 1);
qed "equiv_class_self";
@@ -68,35 +63,34 @@
(*thus r^^{a} = r^^{b} as well*)
Goalw [equiv_def,trans_def,sym_def]
- "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
+ "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
by (Blast_tac 1);
qed "equiv_class_nondisjoint";
-val [major] = goalw Equiv.thy [equiv_def,refl_def]
- "equiv A r ==> r <= A <*> A";
-by (rtac (major RS conjunct1 RS conjunct1) 1);
+Goalw [equiv_def,refl_def] "equiv A r ==> r <= A <*> A";
+by (Blast_tac 1);
qed "equiv_type";
Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
by (blast_tac (claset() addSIs [equiv_class_eq]
- addDs [eq_equiv_class, equiv_type]) 1);
+ addDs [eq_equiv_class, equiv_type]) 1);
qed "equiv_class_eq_iff";
Goal "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
by (blast_tac (claset() addSIs [equiv_class_eq]
- addDs [eq_equiv_class, equiv_type]) 1);
+ addDs [eq_equiv_class, equiv_type]) 1);
qed "eq_equiv_class_iff";
(*** Quotients ***)
(** Introduction/elimination rules -- needed? **)
-Goalw [quotient_def] "x:A ==> r^^{x}: A/r";
+Goalw [quotient_def] "x:A ==> r^^{x}: A//r";
by (Blast_tac 1);
qed "quotientI";
-val [major,minor] = goalw Equiv.thy [quotient_def]
- "[| X:(A/r); !!x. [| X = r^^{x}; x:A |] ==> P |] \
+val [major,minor] = Goalw [quotient_def]
+ "[| X:(A//r); !!x. [| X = r^^{x}; x:A |] ==> P |] \
\ ==> P";
by (resolve_tac [major RS UN_E] 1);
by (rtac minor 1);
@@ -105,12 +99,12 @@
qed "quotientE";
Goalw [equiv_def,refl_def,quotient_def]
- "equiv A r ==> Union(A/r) = A";
+ "equiv A r ==> Union(A//r) = A";
by (Blast_tac 1);
qed "Union_quotient";
Goalw [quotient_def]
- "[| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y = {})";
+ "[| equiv A r; X: A//r; Y: A//r |] ==> X=Y | (X Int Y = {})";
by (Clarify_tac 1);
by (rtac equiv_class_eq 1);
by (assume_tac 1);
@@ -122,7 +116,7 @@
(**** Defining unary operations upon equivalence classes ****)
(* theorem needed to prove UN_equiv_class *)
-Goal "[| a:A; ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
+Goal "[| a:A; ALL y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
by Auto_tac;
qed "UN_constant_eq";
@@ -140,8 +134,8 @@
qed "UN_equiv_class";
(*type checking of UN x:r``{a}. b(x) *)
-val prems = goalw Equiv.thy [quotient_def]
- "[| equiv A r; congruent r b; X: A/r; \
+val prems = Goalw [quotient_def]
+ "[| equiv A r; congruent r b; X: A//r; \
\ !!x. x : A ==> b(x) : B |] \
\ ==> (UN x:X. b(x)) : B";
by (cut_facts_tac prems 1);
@@ -153,9 +147,9 @@
(*Sufficient conditions for injectiveness. Could weaken premises!
major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
*)
-val prems = goalw Equiv.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv A r; congruent r b; \
-\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
+\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A//r; Y: A//r; \
\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \
\ ==> X=Y";
by (cut_facts_tac prems 1);
@@ -194,9 +188,9 @@
qed "UN_equiv_class2";
(*type checking*)
-val prems = goalw Equiv.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv A r; congruent2 r b; \
-\ X1: A/r; X2: A/r; \
+\ X1: A//r; X2: A//r; \
\ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \
\ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
by (cut_facts_tac prems 1);
@@ -215,7 +209,7 @@
(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
than the direct proof*)
-val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
+val prems = Goalw [congruent2_def,equiv_def,refl_def]
"[| equiv A r; \
\ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \
\ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \
@@ -225,7 +219,7 @@
by (blast_tac (claset() addIs (trans::prems)) 1);
qed "congruent2I";
-val [equivA,commute,congt] = goal Equiv.thy
+val [equivA,commute,congt] = Goal
"[| equiv A r; \
\ !! y z. [| y: A; z: A |] ==> b y z = b z y; \
\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \
@@ -242,7 +236,7 @@
(*** Cardinality results suggested by Florian Kammueller ***)
(*Recall that equiv A r implies r <= A <*> A (equiv_type) *)
-Goal "[| finite A; r <= A <*> A |] ==> finite (A/r)";
+Goal "[| finite A; r <= A <*> A |] ==> finite (A//r)";
by (rtac finite_subset 1);
by (etac (finite_Pow_iff RS iffD2) 2);
by (rewtac quotient_def);
@@ -250,13 +244,14 @@
qed "finite_quotient";
Goalw [quotient_def]
- "[| finite A; r <= A <*> A; X : A/r |] ==> finite X";
+ "[| finite A; r <= A <*> A; X : A//r |] ==> finite X";
by (rtac finite_subset 1);
by (assume_tac 2);
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; ALL 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);
--- a/src/HOL/Integ/Equiv.thy Wed Jul 19 12:33:19 2000 +0200
+++ b/src/HOL/Integ/Equiv.thy Wed Jul 19 12:33:36 2000 +0200
@@ -7,17 +7,17 @@
*)
Equiv = Relation + Finite +
-consts
- equiv :: "['a set, ('a*'a) set] => bool"
- quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/" 90)
- (*set of equiv classes*)
- congruent :: "[('a*'a) set, 'a=>'b] => bool"
- congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool"
+constdefs
+ equiv :: "['a set, ('a*'a) set] => bool"
+ "equiv A r == refl A r & sym(r) & trans(r)"
+
+ quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90)
+ "A//r == UN x:A. {r^^{x}}" (*set of equiv classes*)
-defs
- equiv_def "equiv A r == refl A r & sym(r) & trans(r)"
- quotient_def "A/r == UN x:A. {r^^{x}}"
- congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)"
- congruent2_def "congruent2 r b == ALL y1 z1 y2 z2.
- (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
+ congruent :: "[('a*'a) set, 'a=>'b] => bool"
+ "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)"
+
+ congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool"
+ "congruent2 r b == ALL y1 z1 y2 z2.
+ (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
end
--- a/src/HOL/Integ/IntDef.ML Wed Jul 19 12:33:19 2000 +0200
+++ b/src/HOL/Integ/IntDef.ML Wed Jul 19 12:33:36 2000 +0200
@@ -10,62 +10,25 @@
(*Rewrite the overloaded 0::int to (int 0)*)
Addsimps [Zero_def];
-(*** Proving that intrel is an equivalence relation ***)
-
-val eqa::eqb::prems = goal Arith.thy
- "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
-\ x1 + y3 = x3 + y1";
-by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1);
-by (rtac (add_left_commute RS trans) 1);
-by (stac eqb 1);
-by (rtac (add_left_commute RS trans) 1);
-by (stac eqa 1);
-by (rtac (add_left_commute) 1);
-qed "integ_trans_lemma";
-
-(** Natural deduction for intrel **)
-
-Goalw [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
-by (Fast_tac 1);
-qed "intrelI";
-
-(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
-Goalw [intrel_def]
- "p: intrel --> (EX x1 y1 x2 y2. \
-\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
-by (Fast_tac 1);
-qed "intrelE_lemma";
-
-val [major,minor] = Goal
- "[| p: intrel; \
-\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \
-\ ==> Q";
-by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
-by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
-qed "intrelE";
-
-AddSIs [intrelI];
-AddSEs [intrelE];
-
-Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
-by (Fast_tac 1);
+Goalw [intrel_def] "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
+by (Blast_tac 1);
qed "intrel_iff";
-Goal "(x,x): intrel";
+Goalw [intrel_def] "(x,x): intrel";
by (pair_tac "x" 1);
-by (rtac intrelI 1);
-by (rtac refl 1);
+by (Blast_tac 1);
qed "intrel_refl";
-Goalw [equiv_def, refl_def, sym_def, trans_def]
+Goalw [intrel_def, equiv_def, refl_def, sym_def, trans_def]
"equiv UNIV intrel";
-by (fast_tac (claset() addSIs [intrel_refl]
- addSEs [sym, integ_trans_lemma]) 1);
+by Auto_tac;
qed "equiv_intrel";
-bind_thm ("equiv_intrel_iff", [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
+bind_thm ("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";
+Goalw [Integ_def,intrel_def,quotient_def]
+ "intrel^^{(x,y)}:Integ";
by (Fast_tac 1);
qed "intrel_in_integ";
@@ -93,16 +56,15 @@
by (dtac eq_equiv_class 1);
by (rtac equiv_intrel 1);
by (Fast_tac 1);
-by Safe_tac;
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [intrel_def]) 1);
qed "inj_int";
(**** zminus: unary negation on Integ ****)
-Goalw [congruent_def] "congruent intrel (%(x,y). intrel^^{(y,x)})";
-by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
+Goalw [congruent_def, intrel_def]
+ "congruent intrel (%(x,y). intrel^^{(y,x)})";
+by (auto_tac (claset(), simpset() addsimps add_ac));
qed "zminus_congruent";
Goalw [zminus_def]
@@ -161,7 +123,6 @@
\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
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";
@@ -275,28 +236,23 @@
(**** zmult: multiplication on Integ ****)
-Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
-by (simp_tac (simpset() addsimps add_ac) 1);
-qed "zmult_congruent_lemma";
-
(*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 (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 ([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);
-by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
+by (rename_tac "x1 x2 y1 y2 z1 z2" 1);
+by (rtac ([equiv_intrel, intrel_iff RS iffD2] MRS equiv_class_eq) 1);
+by (asm_full_simp_tac (simpset() addsimps [intrel_def]) 1);
+by (subgoal_tac
+ "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2" 1);
+by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 2);
+by (arith_tac 1);
qed "zmult_congruent2";
Goalw [zmult_def]
--- a/src/HOL/Integ/IntDef.thy Wed Jul 19 12:33:19 2000 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Jul 19 12:33:36 2000 +0200
@@ -9,10 +9,10 @@
IntDef = Equiv + Arith +
constdefs
intrel :: "((nat * nat) * (nat * nat)) set"
- "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Integ)
- int = "UNIV/intrel" (Equiv.quotient_def)
+ int = "UNIV//intrel" (Equiv.quotient_def)
instance
int :: {ord, zero, plus, times, minus}
@@ -33,7 +33,8 @@
iszero :: int => bool
"iszero z == z = int 0"
-defs
+defs (*of overloaded constants*)
+
Zero_def "0 == int 0"
zadd_def