Ring Theory.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Group.ML Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,127 @@
+(* Title: HOL/Integ/Group.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1996 TU Muenchen
+*)
+
+open Group;
+
+Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
+
+goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
+br trans 1;
+br (plus_assoc RS sym) 1;
+by(stac left_inv 1);
+br zeroL 1;
+qed "left_inv2";
+
+goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
+br trans 1;
+by(res_inst_tac [("x","zero-x")] left_inv2 2);
+by(stac left_inv 1);
+br (zeroR RS sym) 1;
+qed "inv_inv";
+
+goal Group.thy "zero-zero = (zero::'a::add_group)";
+br trans 1;
+br (zeroR RS sym) 1;
+br trans 1;
+by(res_inst_tac [("x","zero")] left_inv2 2);
+by(Simp_tac 1);
+qed "inv_zero";
+
+goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
+br trans 1;
+by(res_inst_tac [("x","zero-x")] left_inv 2);
+by(stac inv_inv 1);
+br refl 1;
+qed "right_inv";
+
+goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
+br trans 1;
+by(res_inst_tac [("x","zero-x")] left_inv2 2);
+by(stac inv_inv 1);
+br refl 1;
+qed "right_inv2";
+
+goal Group.thy "!!x::'a::add_group. x-x = zero";
+by(stac minus_inv 1);
+br right_inv 1;
+qed "minus_self_zero";
+Addsimps [minus_self_zero];
+
+goal Group.thy "!!x::'a::add_group. x-zero = x";
+by(stac minus_inv 1);
+by(stac inv_zero 1);
+br zeroR 1;
+qed "minus_zero";
+Addsimps [minus_zero];
+
+val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
+
+goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
+br trans 1;
+ br zeroR 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 2;
+ by(res_inst_tac [("x","x+y")] right_inv 2);
+br trans 1;
+ br plus_assoc 2;
+br trans 1;
+ br plus_cong 2;
+ by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
+ br refl 2;
+br (zeroL RS sym) 1;
+qed "inv_plus";
+
+goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
+br trans 1;
+br plus_commute 1;
+br trans 1;
+br plus_assoc 1;
+by(Simp_tac 1);
+qed "plus_commuteL";
+Addsimps [plus_commuteL];
+
+Addsimps [inv_inv,inv_plus];
+
+(* Phase 1 *)
+
+goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+(* Phase 2 *)
+
+goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
+by(Simp_tac 1);
+val lemma = result();
+bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
+goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
+br (plus_assoc RS trans) 1;
+br trans 1;
+ br plus_cong 1;
+ br refl 1;
+ br right_inv2 2;
+br plus_commute 1;
+val lemma = result();
+bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Group.thy Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,38 @@
+(* Title: HOL/Integ/Group.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1996 TU Muenchen
+
+A little bit of group theory leading up to rings. Hence groups are additive.
+*)
+
+Group = Set +
+
+(* 0 already used in Nat *)
+axclass zero < term
+consts zero :: "'a::zero"
+
+(* additive semigroups *)
+
+axclass add_semigroup < plus
+ plus_assoc "(x + y) + z = x + (y + z)"
+
+
+(* additive monoids *)
+
+axclass add_monoid < add_semigroup, zero
+ zeroL "zero + x = x"
+ zeroR "x + zero = x"
+
+(* additive groups *)
+
+axclass add_group < add_monoid, minus
+ left_inv "(zero-x)+x = zero"
+ minus_inv "x-y = x + (zero-y)"
+
+(* additive abelian groups *)
+
+axclass add_agroup < add_group
+ plus_commute "x + y = y + x"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntRing.ML Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,18 @@
+(* Title: HOL/Integ/IntRing.ML
+ ID: $Id$
+ Author: Tobias Nipkow and Markus Wenzel
+ Copyright 1996 TU Muenchen
+
+The instantiation of Lagrange's lemma for int.
+*)
+
+open IntRing;
+
+goal thy "!!i1::int. \
+\ (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
+\ sq(i1*j1 - i2*j2 - i3*j3 - i4*j4) + \
+\ sq(i1*j2 + i2*j1 + i3*j4 - i4*j3) + \
+\ sq(i1*j3 - i2*j4 + i3*j1 + i4*j2) + \
+\ sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
+br Lagrange_lemma 1;
+qed "Lagrange_lemma_int";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntRing.thy Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,19 @@
+(* Title: HOL/Integ/IntRing.thy
+ ID: $Id$
+ Author: Tobias Nipkow and Markus Wenzel
+ Copyright 1996 TU Muenchen
+
+The integers form a commutative ring.
+With an application of Lagrange's lemma.
+*)
+
+IntRing = IntRingDefs + Lagrange +
+
+instance int :: add_semigroup (zadd_assoc)
+instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right)
+instance int :: add_group (left_inv_int,minus_inv_int)
+instance int :: add_agroup (zadd_commute)
+instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
+instance int :: cring (zmult_commute)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntRingDefs.ML Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,16 @@
+(* Title: HOL/Integ/IntRingDefs.thy
+ ID: $Id$
+ Author: Tobias Nipkow and Markus Wenzel
+ Copyright 1996 TU Muenchen
+
+*)
+
+open IntRingDefs;
+
+goalw thy [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
+by(Simp_tac 1);
+qed "left_inv_int";
+
+goalw thy [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
+by(Simp_tac 1);
+qed "minus_inv_int";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntRingDefs.thy Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,15 @@
+(* Title: HOL/Integ/IntRingDefs.thy
+ ID: $Id$
+ Author: Tobias Nipkow and Markus Wenzel
+ Copyright 1996 TU Muenchen
+
+Provides the basic defs and thms for showing that int is a commutative ring.
+Most of it has been defined and shown already.
+*)
+
+IntRingDefs = Integ + Ring +
+
+instance int :: zero
+defs zero_int_def "zero::int == $# 0"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Lagrange.ML Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,19 @@
+(* Title: HOL/Integ/Lagrange.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1996 TU Muenchen
+
+
+The following lemma essentially shows that all composite natural numbers are
+sums of fours squares, provided all prime numbers are. However, this is an
+abstract thm about commutative rings and has a priori nothing to do with nat.
+*)
+
+goalw Lagrange.thy [Lagrange.sq_def] "!!x1::'a::cring. \
+\ (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
+\ sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + \
+\ sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + \
+\ sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + \
+\ sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
+by(cring_simp 1);
+qed "Lagrange_lemma";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Lagrange.thy Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,18 @@
+(* Title: HOL/Integ/Lagrange.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1996 TU Muenchen
+
+
+This theory only contains a single thm, which is a lemma in Lagrange's proof
+that every natural number is the sum of 4 squares. It's sole purpose is to
+demonstrate ordered rewriting for commutative rings.
+
+The enterprising reader might consider proving all of Lagrange's thm.
+*)
+Lagrange = Ring +
+
+constdefs sq :: 'a::times => 'a
+ "sq x == x*x"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Ring.ML Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,148 @@
+(* Title: HOL/Integ/Ring.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1996 TU Muenchen
+
+Derives a few equational consequences about rings
+and defines cring_simpl, a simplification tactic for commutative rings.
+*)
+
+open Ring;
+
+(***
+It is not clear if all thsese rules, esp. distributivity, should be part
+of the default simpset. At the moment they are because they are used in the
+decision procedure.
+***)
+Addsimps [times_assoc,times_commute,distribL,distribR];
+
+goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
+br trans 1;
+br times_commute 1;
+br trans 1;
+br times_assoc 1;
+by(Simp_tac 1);
+qed "times_commuteL";
+Addsimps [times_commuteL];
+
+val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
+
+goal Ring.thy "!!x::'a::ring. zero*x = zero";
+br trans 1;
+ br right_inv 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br trans 2;
+ br times_cong 3;
+ br zeroL 3;
+ br refl 3;
+ br (distribR RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_zeroL";
+
+goal Ring.thy "!!x::'a::ring. x*zero = zero";
+br trans 1;
+ br right_inv 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br trans 2;
+ br times_cong 3;
+ br zeroL 4;
+ br refl 3;
+ br (distribL RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_zeroR";
+
+goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
+br trans 1;
+ br zeroL 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br mult_zeroL 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br times_cong 2;
+ br left_inv 2;
+ br refl 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br (distribR RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_invL";
+
+goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
+br trans 1;
+ br zeroL 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br mult_zeroR 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br times_cong 2;
+ br refl 2;
+ br left_inv 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 3;
+ br (distribL RS sym) 2;
+br trans 1;
+ br(plus_assoc RS sym) 2;
+br trans 1;
+ br plus_cong 2;
+ br refl 2;
+ br (right_inv RS sym) 2;
+br (zeroR RS sym) 1;
+qed "mult_invR";
+
+Addsimps[mult_invL,mult_invR];
+
+
+goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
+by(stac minus_inv 1);
+br sym 1;
+by(stac minus_inv 1);
+by(Simp_tac 1);
+qed "minus_distribL";
+
+goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
+by(stac minus_inv 1);
+br sym 1;
+by(stac minus_inv 1);
+by(Simp_tac 1);
+qed "minus_distribR";
+
+Addsimps [minus_distribL,minus_distribR];
+
+(*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
+ MUST be tried first ***)
+val cring_simp =
+ let val phase1 = !simpset addsimps
+ [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
+ val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
+ zeroL,zeroR,mult_zeroL,mult_zeroR]
+ in simp_tac phase1 THEN' simp_tac phase2 end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Ring.thy Fri Nov 29 15:11:37 1996 +0100
@@ -0,0 +1,24 @@
+(* Title: HOL/Integ/Ring.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1996 TU Muenchen
+
+Bits of rings.
+Main output: a simplification tactic for commutative rings.
+*)
+
+Ring = Group +
+
+(* Ring *)
+
+axclass ring < add_agroup, times
+ times_assoc "(x*y)*z = x*(y*z)"
+ distribL "x*(y+z) = x*y + x*z"
+ distribR "(x+y)*z = x*z + y*z"
+
+(* Commutative ring *)
+
+axclass cring < ring
+ times_commute "x*y = y*x"
+
+end