Ring Theory.
authornipkow
Fri Nov 29 15:11:37 1996 +0100 (1996-11-29)
changeset 2281e00c13a29eda
parent 2280 eb2ba30c2981
child 2282 90fb68d597f8
Ring Theory.
src/HOL/Integ/Group.ML
src/HOL/Integ/Group.thy
src/HOL/Integ/IntRing.ML
src/HOL/Integ/IntRing.thy
src/HOL/Integ/IntRingDefs.ML
src/HOL/Integ/IntRingDefs.thy
src/HOL/Integ/Lagrange.ML
src/HOL/Integ/Lagrange.thy
src/HOL/Integ/Ring.ML
src/HOL/Integ/Ring.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/Group.ML	Fri Nov 29 15:11:37 1996 +0100
     1.3 @@ -0,0 +1,127 @@
     1.4 +(*  Title:      HOL/Integ/Group.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1996 TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +open Group;
    1.11 +
    1.12 +Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
    1.13 +
    1.14 +goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
    1.15 +br trans 1;
    1.16 +br (plus_assoc RS sym) 1;
    1.17 +by(stac left_inv 1);
    1.18 +br zeroL 1;
    1.19 +qed "left_inv2";
    1.20 +
    1.21 +goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
    1.22 +br trans 1;
    1.23 +by(res_inst_tac [("x","zero-x")] left_inv2 2);
    1.24 +by(stac left_inv 1);
    1.25 +br (zeroR RS sym) 1;
    1.26 +qed "inv_inv";
    1.27 +
    1.28 +goal Group.thy "zero-zero = (zero::'a::add_group)";
    1.29 +br trans 1;
    1.30 +br (zeroR RS sym) 1;
    1.31 +br trans 1;
    1.32 +by(res_inst_tac [("x","zero")] left_inv2 2);
    1.33 +by(Simp_tac 1);
    1.34 +qed "inv_zero";
    1.35 +
    1.36 +goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
    1.37 +br trans 1;
    1.38 +by(res_inst_tac [("x","zero-x")] left_inv 2);
    1.39 +by(stac inv_inv 1);
    1.40 +br refl 1;
    1.41 +qed "right_inv";
    1.42 +
    1.43 +goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
    1.44 +br trans 1;
    1.45 +by(res_inst_tac [("x","zero-x")] left_inv2 2);
    1.46 +by(stac inv_inv 1);
    1.47 +br refl 1;
    1.48 +qed "right_inv2";
    1.49 +
    1.50 +goal Group.thy "!!x::'a::add_group. x-x = zero";
    1.51 +by(stac minus_inv 1);
    1.52 +br right_inv 1;
    1.53 +qed "minus_self_zero";
    1.54 +Addsimps [minus_self_zero];
    1.55 +
    1.56 +goal Group.thy "!!x::'a::add_group. x-zero = x";
    1.57 +by(stac minus_inv 1);
    1.58 +by(stac inv_zero 1);
    1.59 +br zeroR 1;
    1.60 +qed "minus_zero";
    1.61 +Addsimps [minus_zero];
    1.62 +
    1.63 +val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
    1.64 +
    1.65 +goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
    1.66 +br trans 1;
    1.67 + br zeroR 2;
    1.68 +br trans 1;
    1.69 + br plus_cong 2;
    1.70 +  br refl 2;
    1.71 + by(res_inst_tac [("x","x+y")] right_inv 2);
    1.72 +br trans 1;
    1.73 + br plus_assoc 2;
    1.74 +br trans 1;
    1.75 + br plus_cong 2;
    1.76 +  by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
    1.77 + br refl 2;
    1.78 +br (zeroL RS sym) 1;
    1.79 +qed "inv_plus";
    1.80 +
    1.81 +goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
    1.82 +br trans 1;
    1.83 +br plus_commute 1;
    1.84 +br trans 1;
    1.85 +br plus_assoc 1;
    1.86 +by(Simp_tac 1);
    1.87 +qed "plus_commuteL";
    1.88 +Addsimps [plus_commuteL];
    1.89 +
    1.90 +Addsimps [inv_inv,inv_plus];
    1.91 +
    1.92 +(* Phase 1 *)
    1.93 +
    1.94 +goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
    1.95 +by(Simp_tac 1);
    1.96 +val lemma = result();
    1.97 +bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
    1.98 +
    1.99 +goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
   1.100 +by(Simp_tac 1);
   1.101 +val lemma = result();
   1.102 +bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.103 +
   1.104 +goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
   1.105 +by(Simp_tac 1);
   1.106 +val lemma = result();
   1.107 +bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.108 +
   1.109 +goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
   1.110 +by(Simp_tac 1);
   1.111 +val lemma = result();
   1.112 +bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.113 +
   1.114 +(* Phase 2 *)
   1.115 +
   1.116 +goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
   1.117 +by(Simp_tac 1);
   1.118 +val lemma = result();
   1.119 +bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.120 +
   1.121 +goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
   1.122 +br (plus_assoc RS trans) 1;
   1.123 +br trans 1;
   1.124 + br plus_cong 1;
   1.125 +  br refl 1;
   1.126 + br right_inv2 2;
   1.127 +br plus_commute 1;
   1.128 +val lemma = result();
   1.129 +bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   1.130 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Integ/Group.thy	Fri Nov 29 15:11:37 1996 +0100
     2.3 @@ -0,0 +1,38 @@
     2.4 +(*  Title:      HOL/Integ/Group.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1996 TU Muenchen
     2.8 +
     2.9 +A little bit of group theory leading up to rings. Hence groups are additive.
    2.10 +*)
    2.11 +
    2.12 +Group = Set +
    2.13 +
    2.14 +(* 0 already used in Nat *)
    2.15 +axclass  zero < term
    2.16 +consts   zero :: "'a::zero"
    2.17 +
    2.18 +(* additive semigroups *)
    2.19 +
    2.20 +axclass  add_semigroup < plus
    2.21 +  plus_assoc   "(x + y) + z = x + (y + z)"
    2.22 +
    2.23 +
    2.24 +(* additive monoids *)
    2.25 +
    2.26 +axclass  add_monoid < add_semigroup, zero
    2.27 +  zeroL    "zero + x = x"
    2.28 +  zeroR    "x + zero = x"
    2.29 +
    2.30 +(* additive groups *)
    2.31 +
    2.32 +axclass  add_group < add_monoid, minus
    2.33 +  left_inv  "(zero-x)+x = zero"
    2.34 +  minus_inv "x-y = x + (zero-y)"
    2.35 +
    2.36 +(* additive abelian groups *)
    2.37 +
    2.38 +axclass  add_agroup < add_group
    2.39 +  plus_commute  "x + y = y + x"
    2.40 +
    2.41 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Integ/IntRing.ML	Fri Nov 29 15:11:37 1996 +0100
     3.3 @@ -0,0 +1,18 @@
     3.4 +(*  Title:      HOL/Integ/IntRing.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow and Markus Wenzel
     3.7 +    Copyright   1996 TU Muenchen
     3.8 +
     3.9 +The instantiation of Lagrange's lemma for int.
    3.10 +*)
    3.11 +
    3.12 +open IntRing;
    3.13 +
    3.14 +goal thy "!!i1::int. \
    3.15 +\  (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
    3.16 +\  sq(i1*j1 - i2*j2 - i3*j3 - i4*j4)  + \
    3.17 +\  sq(i1*j2 + i2*j1 + i3*j4 - i4*j3)  + \
    3.18 +\  sq(i1*j3 - i2*j4 + i3*j1 + i4*j2)  + \
    3.19 +\  sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
    3.20 +br Lagrange_lemma 1;
    3.21 +qed "Lagrange_lemma_int";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Integ/IntRing.thy	Fri Nov 29 15:11:37 1996 +0100
     4.3 @@ -0,0 +1,19 @@
     4.4 +(*  Title:      HOL/Integ/IntRing.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow and Markus Wenzel
     4.7 +    Copyright   1996 TU Muenchen
     4.8 +
     4.9 +The integers form a commutative ring.
    4.10 +With an application of Lagrange's lemma.
    4.11 +*)
    4.12 +
    4.13 +IntRing = IntRingDefs + Lagrange +
    4.14 +
    4.15 +instance int :: add_semigroup (zadd_assoc)
    4.16 +instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right)
    4.17 +instance int :: add_group (left_inv_int,minus_inv_int)
    4.18 +instance int :: add_agroup (zadd_commute)
    4.19 +instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
    4.20 +instance int :: cring (zmult_commute)
    4.21 +
    4.22 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Integ/IntRingDefs.ML	Fri Nov 29 15:11:37 1996 +0100
     5.3 @@ -0,0 +1,16 @@
     5.4 +(*  Title:      HOL/Integ/IntRingDefs.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tobias Nipkow and Markus Wenzel
     5.7 +    Copyright   1996 TU Muenchen
     5.8 +
     5.9 +*)
    5.10 +
    5.11 +open IntRingDefs;
    5.12 +
    5.13 +goalw thy [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
    5.14 +by(Simp_tac 1);
    5.15 +qed "left_inv_int";
    5.16 +
    5.17 +goalw thy [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
    5.18 +by(Simp_tac 1);
    5.19 +qed "minus_inv_int";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Integ/IntRingDefs.thy	Fri Nov 29 15:11:37 1996 +0100
     6.3 @@ -0,0 +1,15 @@
     6.4 +(*  Title:      HOL/Integ/IntRingDefs.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Tobias Nipkow and Markus Wenzel
     6.7 +    Copyright   1996 TU Muenchen
     6.8 +
     6.9 +Provides the basic defs and thms for showing that int is a commutative ring.
    6.10 +Most of it has been defined and shown already.
    6.11 +*)
    6.12 +
    6.13 +IntRingDefs = Integ + Ring +
    6.14 +
    6.15 +instance int :: zero
    6.16 +defs zero_int_def "zero::int == $# 0"
    6.17 +
    6.18 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Integ/Lagrange.ML	Fri Nov 29 15:11:37 1996 +0100
     7.3 @@ -0,0 +1,19 @@
     7.4 +(*  Title:      HOL/Integ/Lagrange.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Tobias Nipkow
     7.7 +    Copyright   1996 TU Muenchen
     7.8 +
     7.9 +
    7.10 +The following lemma essentially shows that all composite natural numbers are
    7.11 +sums of fours squares, provided all prime numbers are. However, this is an
    7.12 +abstract thm about commutative rings and has a priori nothing to do with nat.
    7.13 +*)
    7.14 +
    7.15 +goalw Lagrange.thy [Lagrange.sq_def] "!!x1::'a::cring. \
    7.16 +\  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
    7.17 +\  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  + \
    7.18 +\  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  + \
    7.19 +\  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
    7.20 +\  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
    7.21 +by(cring_simp 1);
    7.22 +qed "Lagrange_lemma";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Integ/Lagrange.thy	Fri Nov 29 15:11:37 1996 +0100
     8.3 @@ -0,0 +1,18 @@
     8.4 +(*  Title:      HOL/Integ/Lagrange.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Tobias Nipkow
     8.7 +    Copyright   1996 TU Muenchen
     8.8 +
     8.9 +
    8.10 +This theory only contains a single thm, which is a lemma in Lagrange's proof
    8.11 +that every natural number is the sum of 4 squares.  It's sole purpose is to
    8.12 +demonstrate ordered rewriting for commutative rings.
    8.13 +
    8.14 +The enterprising reader might consider proving all of Lagrange's thm.
    8.15 +*)
    8.16 +Lagrange = Ring +
    8.17 +
    8.18 +constdefs sq :: 'a::times => 'a
    8.19 +         "sq x == x*x"
    8.20 +
    8.21 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Integ/Ring.ML	Fri Nov 29 15:11:37 1996 +0100
     9.3 @@ -0,0 +1,148 @@
     9.4 +(*  Title:      HOL/Integ/Ring.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Tobias Nipkow
     9.7 +    Copyright   1996 TU Muenchen
     9.8 +
     9.9 +Derives a few equational consequences about rings
    9.10 +and defines cring_simpl, a simplification tactic for commutative rings.
    9.11 +*)
    9.12 +
    9.13 +open Ring;
    9.14 +
    9.15 +(***
    9.16 +It is not clear if all thsese rules, esp. distributivity, should be part
    9.17 +of the default simpset. At the moment they are because they are used in the
    9.18 +decision procedure.
    9.19 +***)   
    9.20 +Addsimps [times_assoc,times_commute,distribL,distribR];
    9.21 +
    9.22 +goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
    9.23 +br trans 1;
    9.24 +br times_commute 1;
    9.25 +br trans 1;
    9.26 +br times_assoc 1;
    9.27 +by(Simp_tac 1);
    9.28 +qed "times_commuteL";
    9.29 +Addsimps [times_commuteL];
    9.30 +
    9.31 +val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
    9.32 +
    9.33 +goal Ring.thy "!!x::'a::ring. zero*x = zero";
    9.34 +br trans 1;
    9.35 + br right_inv 2;
    9.36 +br trans 1;
    9.37 + br plus_cong 2;
    9.38 +  br refl 3;
    9.39 + br trans 2;
    9.40 +  br times_cong 3;
    9.41 +   br zeroL 3;
    9.42 +  br refl 3;
    9.43 + br (distribR RS sym) 2;
    9.44 +br trans 1;
    9.45 + br(plus_assoc RS sym) 2;
    9.46 +br trans 1;
    9.47 + br plus_cong 2;
    9.48 +  br refl 2;
    9.49 + br (right_inv RS sym) 2;
    9.50 +br (zeroR RS sym) 1;
    9.51 +qed "mult_zeroL";
    9.52 +
    9.53 +goal Ring.thy "!!x::'a::ring. x*zero = zero";
    9.54 +br trans 1;
    9.55 + br right_inv 2;
    9.56 +br trans 1;
    9.57 + br plus_cong 2;
    9.58 +  br refl 3;
    9.59 + br trans 2;
    9.60 +  br times_cong 3;
    9.61 +   br zeroL 4;
    9.62 +  br refl 3;
    9.63 + br (distribL RS sym) 2;
    9.64 +br trans 1;
    9.65 + br(plus_assoc RS sym) 2;
    9.66 +br trans 1;
    9.67 + br plus_cong 2;
    9.68 +  br refl 2;
    9.69 + br (right_inv RS sym) 2;
    9.70 +br (zeroR RS sym) 1;
    9.71 +qed "mult_zeroR";
    9.72 +
    9.73 +goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
    9.74 +br trans 1;
    9.75 + br zeroL 2;
    9.76 +br trans 1;
    9.77 + br plus_cong 2;
    9.78 +  br refl 3;
    9.79 + br mult_zeroL 2;
    9.80 +br trans 1;
    9.81 + br plus_cong 2;
    9.82 +  br refl 3;
    9.83 + br times_cong 2;
    9.84 +  br left_inv 2;
    9.85 + br refl 2;
    9.86 +br trans 1;
    9.87 + br plus_cong 2;
    9.88 +  br refl 3;
    9.89 + br (distribR RS sym) 2;
    9.90 +br trans 1;
    9.91 + br(plus_assoc RS sym) 2;
    9.92 +br trans 1;
    9.93 + br plus_cong 2;
    9.94 +  br refl 2;
    9.95 + br (right_inv RS sym) 2;
    9.96 +br (zeroR RS sym) 1;
    9.97 +qed "mult_invL";
    9.98 +
    9.99 +goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
   9.100 +br trans 1;
   9.101 + br zeroL 2;
   9.102 +br trans 1;
   9.103 + br plus_cong 2;
   9.104 +  br refl 3;
   9.105 + br mult_zeroR 2;
   9.106 +br trans 1;
   9.107 + br plus_cong 2;
   9.108 +  br refl 3;
   9.109 + br times_cong 2;
   9.110 +  br refl 2;
   9.111 + br left_inv 2;
   9.112 +br trans 1;
   9.113 + br plus_cong 2;
   9.114 +  br refl 3;
   9.115 + br (distribL RS sym) 2;
   9.116 +br trans 1;
   9.117 + br(plus_assoc RS sym) 2;
   9.118 +br trans 1;
   9.119 + br plus_cong 2;
   9.120 +  br refl 2;
   9.121 + br (right_inv RS sym) 2;
   9.122 +br (zeroR RS sym) 1;
   9.123 +qed "mult_invR";
   9.124 +
   9.125 +Addsimps[mult_invL,mult_invR];
   9.126 +
   9.127 +
   9.128 +goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
   9.129 +by(stac minus_inv 1);
   9.130 +br sym 1;
   9.131 +by(stac minus_inv 1);
   9.132 +by(Simp_tac 1);
   9.133 +qed "minus_distribL";
   9.134 +
   9.135 +goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
   9.136 +by(stac minus_inv 1);
   9.137 +br sym 1;
   9.138 +by(stac minus_inv 1);
   9.139 +by(Simp_tac 1);
   9.140 +qed "minus_distribR";
   9.141 +
   9.142 +Addsimps [minus_distribL,minus_distribR];
   9.143 +
   9.144 +(*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
   9.145 +     MUST be tried first ***)
   9.146 +val cring_simp =
   9.147 +  let val phase1 = !simpset addsimps
   9.148 +                   [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
   9.149 +      val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
   9.150 +                                    zeroL,zeroR,mult_zeroL,mult_zeroR]
   9.151 +  in simp_tac phase1 THEN' simp_tac phase2 end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Integ/Ring.thy	Fri Nov 29 15:11:37 1996 +0100
    10.3 @@ -0,0 +1,24 @@
    10.4 +(*  Title:      HOL/Integ/Ring.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Tobias Nipkow
    10.7 +    Copyright   1996 TU Muenchen
    10.8 +
    10.9 +Bits of rings.
   10.10 +Main output: a simplification tactic for commutative rings.
   10.11 +*)
   10.12 +
   10.13 +Ring = Group +
   10.14 +
   10.15 +(* Ring *)
   10.16 +
   10.17 +axclass  ring < add_agroup, times
   10.18 +  times_assoc "(x*y)*z = x*(y*z)"
   10.19 +  distribL    "x*(y+z) = x*y + x*z"
   10.20 +  distribR    "(x+y)*z = x*z + y*z"
   10.21 +
   10.22 +(* Commutative ring *)
   10.23 +
   10.24 +axclass cring < ring
   10.25 +  times_commute "x*y = y*x"
   10.26 +
   10.27 +end