Moved ring stuff from ex into Ring_and_Field.
authornipkow
Fri Apr 16 20:33:16 2004 +0200 (2004-04-16)
changeset 14603985eb6708207
parent 14602 e06ded775eca
child 14604 1946097f7068
Moved ring stuff from ex into Ring_and_Field.
src/HOL/IsaMakefile
src/HOL/Ring_and_Field.thy
src/HOL/ex/Group.ML
src/HOL/ex/Group.thy
src/HOL/ex/IntRing.ML
src/HOL/ex/IntRing.thy
src/HOL/ex/Lagrange.ML
src/HOL/ex/Lagrange.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Ring.ML
src/HOL/ex/Ring.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 16 19:04:17 2004 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 16 20:33:16 2004 +0200
     1.3 @@ -584,16 +584,16 @@
     1.4  
     1.5  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
     1.6    ex/BT.thy ex/BinEx.thy ex/Exceptions.thy \
     1.7 -  ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
     1.8 -  ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
     1.9 +  ex/Higher_Order_Logic.thy \
    1.10 +  ex/Hilbert_Classical.thy ex/InSort.thy \
    1.11    ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
    1.12 -  ex/IntRing.thy ex/Intuitionistic.thy \
    1.13 -  ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
    1.14 +  ex/Intuitionistic.thy \
    1.15 +  ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
    1.16    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
    1.17    ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
    1.18    ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
    1.19    ex/Refute_Examples.thy \
    1.20 -  ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.21 +  ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.22    ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
    1.23    ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
    1.24    ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
     2.1 --- a/src/HOL/Ring_and_Field.thy	Fri Apr 16 19:04:17 2004 +0200
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Apr 16 20:33:16 2004 +0200
     2.3 @@ -19,10 +19,7 @@
     2.4    zero [simp]: "0 + x = x"
     2.5  
     2.6  lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
     2.7 -apply (rule plus_ac0.commute [THEN trans])
     2.8 -apply (rule plus_ac0.assoc [THEN trans])
     2.9 -apply (rule plus_ac0.commute [THEN arg_cong])
    2.10 -done
    2.11 +by(rule mk_left_commute[of "op +",OF plus_ac0.assoc plus_ac0.commute])
    2.12  
    2.13  lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
    2.14  apply (rule plus_ac0.commute [THEN trans])
    2.15 @@ -39,15 +36,7 @@
    2.16  
    2.17  theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
    2.18    y * (x * z)"
    2.19 -proof -
    2.20 -  have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
    2.21 -    by (rule times_ac1.assoc [THEN sym])
    2.22 -  also have "x * y = y * x"
    2.23 -    by (rule times_ac1.commute)
    2.24 -  also have "(y * x) * z = y * (x * z)"
    2.25 -    by (rule times_ac1.assoc)
    2.26 -  finally show ?thesis .
    2.27 -qed
    2.28 +by(rule mk_left_commute[of "op *",OF times_ac1.assoc times_ac1.commute])
    2.29  
    2.30  theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"
    2.31  proof -
    2.32 @@ -525,6 +514,13 @@
    2.33         diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    2.34         diff_eq_eq eq_diff_eq
    2.35  
    2.36 +text{*This list of rewrites decides ring equalities by ordered rewriting.*}
    2.37 +lemmas ring_eq_simps =
    2.38 +  times_ac1.assoc times_ac1.commute times_ac1_left_commute
    2.39 +  left_distrib right_distrib left_diff_distrib right_diff_distrib
    2.40 +  plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
    2.41 +  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    2.42 +  diff_eq_eq eq_diff_eq
    2.43  
    2.44  subsection{*Lemmas for the @{text cancel_numerals} simproc*}
    2.45  
     3.1 --- a/src/HOL/ex/Group.ML	Fri Apr 16 19:04:17 2004 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,222 +0,0 @@
     3.4 -(*  Title:      HOL/Integ/Group.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -    Copyright   1997 TU Muenchen
     3.8 -*)
     3.9 -
    3.10 -(*** Groups ***)
    3.11 -
    3.12 -(* Derives the well-known convergent set of equations for groups
    3.13 -   based on the unary inverse 0-x.
    3.14 -*)
    3.15 -
    3.16 -Goal "!!x::'a::add_group. (0 - x) + (x + y) = y";
    3.17 -by (rtac trans 1);
    3.18 -by (rtac (plus_assoc RS sym) 1);
    3.19 -by (stac left_inv 1);
    3.20 -by (rtac zeroL 1);
    3.21 -qed "left_inv2";
    3.22 -
    3.23 -Goal "!!x::'a::add_group. (0 - (0 - x)) = x";
    3.24 -by (rtac trans 1);
    3.25 -by (res_inst_tac [("x","0 - x")] left_inv2 2);
    3.26 -by (stac left_inv 1);
    3.27 -by (rtac (zeroR RS sym) 1);
    3.28 -qed "inv_inv";
    3.29 -
    3.30 -Goal "0 - 0 = (0::'a::add_group)";
    3.31 -by (rtac trans 1);
    3.32 -by (rtac (zeroR RS sym) 1);
    3.33 -by (rtac trans 1);
    3.34 -by (res_inst_tac [("x","0")] left_inv2 2);
    3.35 -by (simp_tac (simpset() addsimps [zeroR]) 1);
    3.36 -qed "inv_zero";
    3.37 -
    3.38 -Goal "!!x::'a::add_group. x + (0 - x) = 0";
    3.39 -by (rtac trans 1);
    3.40 -by (res_inst_tac [("x","0-x")] left_inv 2);
    3.41 -by (stac inv_inv 1);
    3.42 -by (rtac refl 1);
    3.43 -qed "right_inv";
    3.44 -
    3.45 -Goal "!!x::'a::add_group. x + ((0 - x) + y) = y";
    3.46 -by (rtac trans 1);
    3.47 -by (res_inst_tac [("x","0 - x")] left_inv2 2);
    3.48 -by (stac inv_inv 1);
    3.49 -by (rtac refl 1);
    3.50 -qed "right_inv2";
    3.51 -
    3.52 -val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
    3.53 -
    3.54 -Goal "!!x::'a::add_group. 0 - (x + y) = (0 - y) + (0 - x)";
    3.55 -by (rtac trans 1);
    3.56 - by (rtac zeroR 2);
    3.57 -by (rtac trans 1);
    3.58 - by (rtac plus_cong 2);
    3.59 -  by (rtac refl 2);
    3.60 - by (res_inst_tac [("x","x+y")] right_inv 2);
    3.61 -by (rtac trans 1);
    3.62 - by (rtac plus_assoc 2);
    3.63 -by (rtac trans 1);
    3.64 - by (rtac plus_cong 2);
    3.65 -  by (simp_tac (simpset() addsimps
    3.66 -        [plus_assoc,left_inv,left_inv2,right_inv,right_inv2]) 2);
    3.67 - by (rtac refl 2);
    3.68 -by (rtac (zeroL RS sym) 1);
    3.69 -qed "inv_plus";
    3.70 -
    3.71 -(*** convergent TRS for groups with unary inverse 0 - x ***)
    3.72 -val group1_simps =
    3.73 -  [zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv,
    3.74 -   inv_zero,inv_plus];
    3.75 -
    3.76 -val group1_tac =
    3.77 -  let val ss = HOL_basic_ss addsimps group1_simps
    3.78 -  in simp_tac ss end;
    3.79 -
    3.80 -(* I believe there is no convergent TRS for groups with binary `-',
    3.81 -   unless you have an extra unary `-' and simply define x - y = x + (-y).
    3.82 -   This does not work with only a binary `-' because x - y = x + (0 - y) does
    3.83 -   not terminate. Hence we have a special tactic for converting all
    3.84 -   occurrences of x - y into x + (0 - y):
    3.85 -*)
    3.86 -
    3.87 -local
    3.88 -fun find(Const("op -",Type("fun",[T,_]))$s$t) = [(T,s,t)] @ find s @ find t
    3.89 -  | find(s$t) = find s @ find t
    3.90 -  | find _ = [];
    3.91 -
    3.92 -fun subst_tac sg (tacf,(T,s,t)) = 
    3.93 -  let val typinst = [(("'a",0),ctyp_of sg T)];
    3.94 -      val terminst = [(cterm_of sg (Var(("x",0),T)),cterm_of sg s),
    3.95 -                      (cterm_of sg (Var(("y",0),T)),cterm_of sg t)];
    3.96 -  in tacf THEN' rtac ((instantiate(typinst,terminst) minus_inv) RS ssubst) end;
    3.97 -
    3.98 -in
    3.99 -val mk_group1_tac = SUBGOAL(fn (t,i) => fn st =>
   3.100 -      let val sg = #sign(rep_thm st)
   3.101 -      in foldl (subst_tac sg) (K all_tac,find t) i st
   3.102 -      end)
   3.103 -end;
   3.104 -
   3.105 -(* The following two equations are not used in any of the decision procedures,
   3.106 -   but are still very useful. They also demonstrate mk_group1_tac.
   3.107 -*)
   3.108 -Goal "x - x = (0::'a::add_group)";
   3.109 -by (mk_group1_tac 1);
   3.110 -by (group1_tac 1);
   3.111 -qed "minus_self_zero";
   3.112 -
   3.113 -Goal "x - 0 = (x::'a::add_group)";
   3.114 -by (mk_group1_tac 1);
   3.115 -by (group1_tac 1);
   3.116 -qed "minus_zero";
   3.117 -
   3.118 -(*** Abelian Groups ***)
   3.119 -
   3.120 -Goal "x+(y+z)=y+(x+z::'a::add_agroup)";
   3.121 -by (rtac trans 1);
   3.122 -by (rtac plus_commute 1);
   3.123 -by (rtac trans 1);
   3.124 -by (rtac plus_assoc 1);
   3.125 -by (simp_tac (simpset() addsimps [plus_commute]) 1);
   3.126 -qed "plus_commuteL";
   3.127 -
   3.128 -(* Convergent TRS for Abelian groups with unary inverse 0 - x.
   3.129 -   Requires ordered rewriting
   3.130 -*)
   3.131 -
   3.132 -val agroup1_simps = plus_commute::plus_commuteL::group1_simps;
   3.133 -
   3.134 -val agroup1_tac =
   3.135 -  let val ss = HOL_basic_ss addsimps agroup1_simps
   3.136 -  in simp_tac ss end;
   3.137 -
   3.138 -(* Again, I do not believe there is a convergent TRS for Abelian Groups with
   3.139 -   binary `-'. However, we can still decide the word problem using additional
   3.140 -   rules for 
   3.141 -   1. floating `-' to the top:
   3.142 -      "x + (y - z) = (x + y) - (z::'a::add_group)"
   3.143 -      "(x - y) + z = (x + z) - (y::'a::add_agroup)"
   3.144 -      "(x - y) - z = x - (y + (z::'a::add_agroup))"
   3.145 -      "x - (y - z) = (x + z) - (y::'a::add_agroup)"
   3.146 -   2. and for moving `-' over to the other side:
   3.147 -      (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
   3.148 -*)
   3.149 -Goal "x + (y - z) = (x + y) - (z::'a::add_group)";
   3.150 -by (mk_group1_tac 1);
   3.151 -by (group1_tac 1);
   3.152 -qed "plus_minusR";
   3.153 -
   3.154 -Goal "(x - y) + z = (x + z) - (y::'a::add_agroup)";
   3.155 -by (mk_group1_tac 1);
   3.156 -by (agroup1_tac 1);
   3.157 -qed "plus_minusL";
   3.158 -
   3.159 -Goal "(x - y) - z = x - (y + (z::'a::add_agroup))";
   3.160 -by (mk_group1_tac 1);
   3.161 -by (agroup1_tac 1);
   3.162 -qed "minus_minusL";
   3.163 -
   3.164 -Goal "x - (y - z) = (x + z) - (y::'a::add_agroup)";
   3.165 -by (mk_group1_tac 1);
   3.166 -by (agroup1_tac 1);
   3.167 -qed "minus_minusR";
   3.168 -
   3.169 -Goal "!!x::'a::add_group. (x-y = z) = (x = z+y)";
   3.170 -by (stac minus_inv 1);
   3.171 -by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
   3.172 -qed "minusL_iff";
   3.173 -
   3.174 -Goal "!!x::'a::add_group. (x = y-z) = (x+z = y)";
   3.175 -by (stac minus_inv 1);
   3.176 -by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
   3.177 -qed "minusR_iff";
   3.178 -
   3.179 -val agroup2_simps =
   3.180 -  [zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL,
   3.181 -   plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff];
   3.182 -
   3.183 -(* This two-phase ordered rewriting tactic works, but agroup_simps are
   3.184 -   simpler. However, agroup_simps is not confluent for arbitrary terms,
   3.185 -   it merely decides equality.
   3.186 -(* Phase 1 *)
   3.187 -
   3.188 -Goal "!!x::'a::add_agroup. (x+(0-y))+z = (x+z)+(0-y)";
   3.189 -by (Simp_tac 1);
   3.190 -val lemma = result();
   3.191 -bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   3.192 -
   3.193 -Goal "!!x::'a::add_agroup. x+(0-(y+z)) = (x+(0-y))+(0-z)";
   3.194 -by (Simp_tac 1);
   3.195 -val lemma = result();
   3.196 -bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   3.197 -
   3.198 -Goal "!!x::'a::add_agroup. x+(0-(y+(0-z))) = (x+z)+(0-y)";
   3.199 -by (Simp_tac 1);
   3.200 -val lemma = result();
   3.201 -bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   3.202 -
   3.203 -Goal "!!x::'a::add_agroup. x+(y+(0-z)) = (x+y)+(0-z)";
   3.204 -by (Simp_tac 1);
   3.205 -val lemma = result();
   3.206 -bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   3.207 -
   3.208 -(* Phase 2 *)
   3.209 -
   3.210 -Goal "!!x::'a::add_agroup. (x+y)+(0-z) = x+(y+(0-z))";
   3.211 -by (Simp_tac 1);
   3.212 -val lemma = result();
   3.213 -bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   3.214 -
   3.215 -Goal "!!x::'a::add_agroup. (x+y)+(0-x) = y";
   3.216 -by (rtac (plus_assoc RS trans) 1);
   3.217 -by (rtac trans 1);
   3.218 - by (rtac plus_cong 1);
   3.219 -  by (rtac refl 1);
   3.220 - by (rtac right_inv2 2);
   3.221 -by (rtac plus_commute 1);
   3.222 -val lemma = result();
   3.223 -bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   3.224 -
   3.225 -*)
     4.1 --- a/src/HOL/ex/Group.thy	Fri Apr 16 19:04:17 2004 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,40 +0,0 @@
     4.4 -(*  Title:      HOL/Integ/Group.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow
     4.7 -    Copyright   1996 TU Muenchen
     4.8 -
     4.9 -A little bit of group theory leading up to rings. Hence groups are additive.
    4.10 -*)
    4.11 -
    4.12 -Group = Main +
    4.13 -
    4.14 -(* additive semigroups *)
    4.15 -
    4.16 -axclass  add_semigroup < plus
    4.17 -  plus_assoc   "(x + y) + z = x + (y + z)"
    4.18 -
    4.19 -
    4.20 -(* additive monoids *)
    4.21 -
    4.22 -axclass  add_monoid < add_semigroup, zero
    4.23 -  zeroL    "0 + x = x"
    4.24 -  zeroR    "x + 0 = x"
    4.25 -
    4.26 -(* additive groups *)
    4.27 -(*
    4.28 -The inverse is the binary `-'. Groups with unary and binary inverse are
    4.29 -interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is
    4.30 -simply the translation of (-x)+x = 0. This characterizes groups already,
    4.31 -provided we only allow (0-x). Law minus_inv `defines' the general x-y in
    4.32 -terms of the specific 0-y.
    4.33 -*)
    4.34 -axclass  add_group < add_monoid, minus
    4.35 -  left_inv  "(0-x)+x = 0"
    4.36 -  minus_inv "x-y = x + (0-y)"
    4.37 -
    4.38 -(* additive abelian groups *)
    4.39 -
    4.40 -axclass  add_agroup < add_group
    4.41 -  plus_commute  "x + y = y + x"
    4.42 -
    4.43 -end
     5.1 --- a/src/HOL/ex/IntRing.ML	Fri Apr 16 19:04:17 2004 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,16 +0,0 @@
     5.4 -(*  Title:      HOL/Integ/IntRing.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Nipkow and Markus Wenzel
     5.7 -    Copyright   1996 TU Muenchen
     5.8 -
     5.9 -The instantiation of Lagrange's lemma for int.
    5.10 -*)
    5.11 -
    5.12 -Goal "!!i1::int. \
    5.13 -\  (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
    5.14 -\  sq(i1*j1 - i2*j2 - i3*j3 - i4*j4)  + \
    5.15 -\  sq(i1*j2 + i2*j1 + i3*j4 - i4*j3)  + \
    5.16 -\  sq(i1*j3 - i2*j4 + i3*j1 + i4*j2)  + \
    5.17 -\  sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
    5.18 -by (rtac Lagrange_lemma 1);
    5.19 -qed "Lagrange_lemma_int";
     6.1 --- a/src/HOL/ex/IntRing.thy	Fri Apr 16 19:04:17 2004 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,19 +0,0 @@
     6.4 -(*  Title:      HOL/Integ/IntRing.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Tobias Nipkow and Markus Wenzel
     6.7 -    Copyright   1996 TU Muenchen
     6.8 -
     6.9 -The integers form a commutative ring.
    6.10 -With an application of Lagrange's lemma.
    6.11 -*)
    6.12 -
    6.13 -IntRing = Ring + Lagrange +
    6.14 -
    6.15 -instance int :: add_semigroup (zadd_assoc)
    6.16 -instance int :: add_monoid (zadd_0,zadd_0_right)
    6.17 -instance int :: add_group {|Auto_tac|}
    6.18 -instance int :: add_agroup (zadd_commute)
    6.19 -instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
    6.20 -instance int :: cring (zmult_commute)
    6.21 -
    6.22 -end
     7.1 --- a/src/HOL/ex/Lagrange.ML	Fri Apr 16 19:04:17 2004 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,37 +0,0 @@
     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 every natural number is the sum of
    7.11 -four squares, provided all prime numbers are.  However, this is an abstract
    7.12 -theorem about commutative rings.  It has, a priori, nothing to do with nat.*)
    7.13 -
    7.14 -Goalw [Lagrange.sq_def]
    7.15 - "!!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_tac 1);  (*once a slow step, but now (2001) just three seconds!*)
    7.22 -qed "Lagrange_lemma";
    7.23 -
    7.24 -
    7.25 -(* A challenge by John Harrison.
    7.26 -   Takes forever because of the naive bottom-up strategy of the rewriter.
    7.27 -
    7.28 -Goalw [Lagrange.sq_def] "!!p1::'a::cring.\
    7.29 -\ (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * \
    7.30 -\ (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) \
    7.31 -\  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + \
    7.32 -\    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +\
    7.33 -\    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +\
    7.34 -\    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +\
    7.35 -\    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +\
    7.36 -\    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +\
    7.37 -\    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +\
    7.38 -\    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)";
    7.39 -by (cring_tac 1);
    7.40 -*)
     8.1 --- a/src/HOL/ex/Lagrange.thy	Fri Apr 16 19:04:17 2004 +0200
     8.2 +++ b/src/HOL/ex/Lagrange.thy	Fri Apr 16 20:33:16 2004 +0200
     8.3 @@ -10,9 +10,42 @@
     8.4  
     8.5  The enterprising reader might consider proving all of Lagrange's theorem.
     8.6  *)
     8.7 -Lagrange = Ring +
     8.8  
     8.9 -constdefs sq :: 'a::times => 'a
    8.10 +theory Lagrange = Main:
    8.11 +
    8.12 +constdefs sq :: "'a::times => 'a"
    8.13           "sq x == x*x"
    8.14  
    8.15 +(* The following lemma essentially shows that every natural number is the sum
    8.16 +of four squares, provided all prime numbers are.  However, this is an
    8.17 +abstract theorem about commutative rings.  It has, a priori, nothing to do
    8.18 +with nat.*)
    8.19 +
    8.20 +(*once a slow step, but now (2001) just three seconds!*)
    8.21 +lemma Lagrange_lemma:
    8.22 + "!!x1::'a::ring.
    8.23 +  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    8.24 +  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    8.25 +  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    8.26 +  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    8.27 +  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    8.28 +by(simp add: sq_def ring_eq_simps)
    8.29 +
    8.30 +
    8.31 +(* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.
    8.32 +
    8.33 +lemma "!!p1::'a::ring.
    8.34 + (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    8.35 + (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    8.36 +  = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    8.37 +    sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    8.38 +    sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    8.39 +    sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    8.40 +    sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    8.41 +    sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    8.42 +    sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    8.43 +    sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    8.44 +by(simp add: sq_def ring_eq_simps)
    8.45 +*)
    8.46 +
    8.47  end
     9.1 --- a/src/HOL/ex/ROOT.ML	Fri Apr 16 19:04:17 2004 +0200
     9.2 +++ b/src/HOL/ex/ROOT.ML	Fri Apr 16 20:33:16 2004 +0200
     9.3 @@ -33,7 +33,7 @@
     9.4  no_document use_thy "List_Prefix";
     9.5  time_use_thy "Exceptions";
     9.6  
     9.7 -time_use_thy "IntRing";
     9.8 +time_use_thy "Lagrange";
     9.9  
    9.10  time_use_thy "set";
    9.11  time_use_thy "MT";
    10.1 --- a/src/HOL/ex/Ring.ML	Fri Apr 16 19:04:17 2004 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,139 +0,0 @@
    10.4 -(*  Title:      HOL/Integ/Ring.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Tobias Nipkow
    10.7 -    Copyright   1996 TU Muenchen
    10.8 -
    10.9 -Derives a few equational consequences about rings
   10.10 -and defines cring_simpl, a simplification tactic for commutative rings.
   10.11 -*)
   10.12 -
   10.13 -Goal "!!x::'a::cring. x*(y*z)=y*(x*z)";
   10.14 -by (rtac trans 1);
   10.15 -by (rtac times_commute 1);
   10.16 -by (rtac trans 1);
   10.17 -by (rtac times_assoc 1);
   10.18 -by (simp_tac (HOL_basic_ss addsimps [times_commute]) 1);
   10.19 -qed "times_commuteL";
   10.20 -
   10.21 -val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
   10.22 -
   10.23 -Goal "!!x::'a::ring. 0*x = 0";
   10.24 -by (rtac trans 1);
   10.25 - by (rtac right_inv 2);
   10.26 -by (rtac trans 1);
   10.27 - by (rtac plus_cong 2);
   10.28 -  by (rtac refl 3);
   10.29 - by (rtac trans 2);
   10.30 -  by (rtac times_cong 3);
   10.31 -   by (rtac zeroL 3);
   10.32 -  by (rtac refl 3);
   10.33 - by (rtac (distribR RS sym) 2);
   10.34 -by (rtac trans 1);
   10.35 - by (rtac (plus_assoc RS sym) 2);
   10.36 -by (rtac trans 1);
   10.37 - by (rtac plus_cong 2);
   10.38 -  by (rtac refl 2);
   10.39 - by (rtac (right_inv RS sym) 2);
   10.40 -by (rtac (zeroR RS sym) 1);
   10.41 -qed "mult_zeroL";
   10.42 -
   10.43 -Goal "!!x::'a::ring. x*0 = 0";
   10.44 -by (rtac trans 1);
   10.45 - by (rtac right_inv 2);
   10.46 -by (rtac trans 1);
   10.47 - by (rtac plus_cong 2);
   10.48 -  by (rtac refl 3);
   10.49 - by (rtac trans 2);
   10.50 -  by (rtac times_cong 3);
   10.51 -   by (rtac zeroL 4);
   10.52 -  by (rtac refl 3);
   10.53 - by (rtac (distribL RS sym) 2);
   10.54 -by (rtac trans 1);
   10.55 - by (rtac (plus_assoc RS sym) 2);
   10.56 -by (rtac trans 1);
   10.57 - by (rtac plus_cong 2);
   10.58 -  by (rtac refl 2);
   10.59 - by (rtac (right_inv RS sym) 2);
   10.60 -by (rtac (zeroR RS sym) 1);
   10.61 -qed "mult_zeroR";
   10.62 -
   10.63 -Goal "!!x::'a::ring. (0-x)*y = 0-(x*y)";
   10.64 -by (rtac trans 1);
   10.65 - by (rtac zeroL 2);
   10.66 -by (rtac trans 1);
   10.67 - by (rtac plus_cong 2);
   10.68 -  by (rtac refl 3);
   10.69 - by (rtac mult_zeroL 2);
   10.70 -by (rtac trans 1);
   10.71 - by (rtac plus_cong 2);
   10.72 -  by (rtac refl 3);
   10.73 - by (rtac times_cong 2);
   10.74 -  by (rtac left_inv 2);
   10.75 - by (rtac refl 2);
   10.76 -by (rtac trans 1);
   10.77 - by (rtac plus_cong 2);
   10.78 -  by (rtac refl 3);
   10.79 - by (rtac (distribR RS sym) 2);
   10.80 -by (rtac trans 1);
   10.81 - by (rtac (plus_assoc RS sym) 2);
   10.82 -by (rtac trans 1);
   10.83 - by (rtac plus_cong 2);
   10.84 -  by (rtac refl 2);
   10.85 - by (rtac (right_inv RS sym) 2);
   10.86 -by (rtac (zeroR RS sym) 1);
   10.87 -qed "mult_invL";
   10.88 -
   10.89 -Goal "!!x::'a::ring. x*(0-y) = 0-(x*y)";
   10.90 -by (rtac trans 1);
   10.91 - by (rtac zeroL 2);
   10.92 -by (rtac trans 1);
   10.93 - by (rtac plus_cong 2);
   10.94 -  by (rtac refl 3);
   10.95 - by (rtac mult_zeroR 2);
   10.96 -by (rtac trans 1);
   10.97 - by (rtac plus_cong 2);
   10.98 -  by (rtac refl 3);
   10.99 - by (rtac times_cong 2);
  10.100 -  by (rtac refl 2);
  10.101 - by (rtac left_inv 2);
  10.102 -by (rtac trans 1);
  10.103 - by (rtac plus_cong 2);
  10.104 -  by (rtac refl 3);
  10.105 - by (rtac (distribL RS sym) 2);
  10.106 -by (rtac trans 1);
  10.107 - by (rtac (plus_assoc RS sym) 2);
  10.108 -by (rtac trans 1);
  10.109 - by (rtac plus_cong 2);
  10.110 -  by (rtac refl 2);
  10.111 - by (rtac (right_inv RS sym) 2);
  10.112 -by (rtac (zeroR RS sym) 1);
  10.113 -qed "mult_invR";
  10.114 -
  10.115 -Goal "x*(y-z) = (x*y - x*z::'a::ring)";
  10.116 -by (mk_group1_tac 1);
  10.117 -by (simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
  10.118 -qed "minus_distribL";
  10.119 -
  10.120 -Goal "(x-y)*z = (x*z - y*z::'a::ring)";
  10.121 -by (mk_group1_tac 1);
  10.122 -by (simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
  10.123 -qed "minus_distribR";
  10.124 -
  10.125 -val cring_simps = [times_assoc,times_commute,times_commuteL,
  10.126 -                   distribL,distribR,minus_distribL,minus_distribR]
  10.127 -                  @ agroup2_simps;
  10.128 -
  10.129 -val cring_tac =
  10.130 -  let val ss = HOL_basic_ss addsimps cring_simps
  10.131 -  in simp_tac ss end;
  10.132 -
  10.133 -
  10.134 -(*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
  10.135 -     MUST be tried first
  10.136 -val cring_simp =
  10.137 -  let val phase1 = simpset() addsimps
  10.138 -                   [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
  10.139 -      val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
  10.140 -                                    zeroL,zeroR,mult_zeroL,mult_zeroR]
  10.141 -  in simp_tac phase1 THEN' simp_tac phase2 end;
  10.142 -***)
    11.1 --- a/src/HOL/ex/Ring.thy	Fri Apr 16 19:04:17 2004 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,24 +0,0 @@
    11.4 -(*  Title:      HOL/Integ/Ring.thy
    11.5 -    ID:         $Id$
    11.6 -    Author:     Tobias Nipkow
    11.7 -    Copyright   1996 TU Muenchen
    11.8 -
    11.9 -Bits of rings.
   11.10 -Main output: a simplification tactic for commutative rings.
   11.11 -*)
   11.12 -
   11.13 -Ring = Group +
   11.14 -
   11.15 -(* Ring *)
   11.16 -
   11.17 -axclass  ring < add_agroup, times
   11.18 -  times_assoc "(x*y)*z = x*(y*z)"
   11.19 -  distribL    "x*(y+z) = x*y + x*z"
   11.20 -  distribR    "(x+y)*z = x*z + y*z"
   11.21 -
   11.22 -(* Commutative ring *)
   11.23 -
   11.24 -axclass cring < ring
   11.25 -  times_commute "x*y = y*x"
   11.26 -
   11.27 -end