# HG changeset patch # User nipkow # Date 849276486 -3600 # Node ID eb2ba30c298146f26e646a581334ba112b6dada2 # Parent 2f337bf8108539af6b36d6b8db0606eb22be1488 Moved the Rings stuff from ex to Integ and showed that int::cring. diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/Integ/ROOT.ML --- a/src/HOL/Integ/ROOT.ML Fri Nov 29 15:07:27 1996 +0100 +++ b/src/HOL/Integ/ROOT.ML Fri Nov 29 15:08:06 1996 +0100 @@ -9,3 +9,4 @@ HOL_build_completed; (*Cause examples to fail if HOL did*) time_use_thy "Bin"; +time_use_thy "IntRing"; diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Group.ML --- a/src/HOL/ex/Group.ML Fri Nov 29 15:07:27 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,127 +0,0 @@ -(* Title: HOL/ex/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); - diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Group.thy --- a/src/HOL/ex/Group.thy Fri Nov 29 15:07:27 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -(* Title: HOL/ex/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 diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Lagrange.ML --- a/src/HOL/ex/Lagrange.ML Fri Nov 29 15:07:27 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/ex/Lagrange.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1996 TU Muenchen - - -The following lemma schows that all composite natural numbers are sums of -fours squares, provided all prime numbers are. -*) - -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"; diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Lagrange.thy --- a/src/HOL/ex/Lagrange.thy Fri Nov 29 15:07:27 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/ex/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 diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Nov 29 15:07:27 1996 +0100 +++ b/src/HOL/ex/ROOT.ML Fri Nov 29 15:08:06 1996 +0100 @@ -21,7 +21,6 @@ time_use_thy "InSort"; time_use_thy "Qsort"; time_use_thy "LexProd"; -time_use_thy "Lagrange"; time_use_thy "Puzzle"; time_use_thy "Mutil"; time_use_thy "Primes"; diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Ring.ML --- a/src/HOL/ex/Ring.ML Fri Nov 29 15:07:27 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,148 +0,0 @@ -(* Title: HOL/ex/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; diff -r 2f337bf81085 -r eb2ba30c2981 src/HOL/ex/Ring.thy --- a/src/HOL/ex/Ring.thy Fri Nov 29 15:07:27 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: HOL/ex/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