Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Moved the Rings stuff from ex to Integ and showed that int::cring.
authornipkow
Fri, 29 Nov 1996 15:08:06 +0100
changeset 2280 eb2ba30c2981
parent 2279 2f337bf81085
child 2281 e00c13a29eda
Moved the Rings stuff from ex to Integ and showed that int::cring.
src/HOL/Integ/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/ex/Group.ML file | annotate | diff | comparison | revisions
src/HOL/ex/Group.thy file | annotate | diff | comparison | revisions
src/HOL/ex/Lagrange.ML file | annotate | diff | comparison | revisions
src/HOL/ex/Lagrange.thy file | annotate | diff | comparison | revisions
src/HOL/ex/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/ex/Ring.ML file | annotate | diff | comparison | revisions
src/HOL/ex/Ring.thy file | annotate | diff | comparison | revisions 
--- 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";
--- 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);
-
--- 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
--- 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";
--- 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
--- 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";
--- 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;
--- 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
isabelle