# HG changeset patch # User paulson # Date 964002816 -7200 # Node ID c8e6529cc082e10ad63c0736c32995354c145c51 # Parent a6ab3a442da614873627a4d2a4efcf544a5a8eaa changed / to // for quotienting diff -r a6ab3a442da6 -r c8e6529cc082 src/HOL/Integ/Equiv.ML --- 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); diff -r a6ab3a442da6 -r c8e6529cc082 src/HOL/Integ/Equiv.thy --- 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 diff -r a6ab3a442da6 -r c8e6529cc082 src/HOL/Integ/IntDef.ML --- 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] diff -r a6ab3a442da6 -r c8e6529cc082 src/HOL/Integ/IntDef.thy --- 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