author lcp Mon, 27 Feb 1995 17:06:19 +0100 changeset 904 5240dcd12adb parent 903 26138063bb88 child 905 80b581036036
 src/ZF/ex/Integ.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/ex/Integ.ML	Mon Feb 27 16:58:59 1995 +0100
+++ b/src/ZF/ex/Integ.ML	Mon Feb 27 17:06:19 1995 +0100
@@ -12,18 +12,10 @@
\$+ and \$* are monotonic wrt \$<
*)

-    read_instantiate_sg (sign_of Arith.thy) [("t","op #+")] subst_context2;
-
-
open Integ;

(*** Proving that intrel is an equivalence relation ***)

-
-
(*By luck, requires no typing premises for y1, y2,y3*)
val eqa::eqb::prems = goal Arith.thy
"[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
@@ -263,6 +255,15 @@

+(*For AC rewriting*)
+    "!!z1 z2 z3. [| z1:integ;  z2:integ;  z3: integ |] ==> \
+\                z1\$+(z2\$+z3) = z2\$+(z1\$+z3)"
+
+(*Integer addition is an AC operator*)
+
goalw Integ.thy [znat_def]
"!!m n. [| m: nat;  n: nat |] ==> \$# (m #+ n) = (\$#m) \$+ (\$#n)";
@@ -364,6 +365,16 @@
qed "zmult_assoc";

+(*For AC rewriting*)
+qed_goal "zmult_left_commute" Integ.thy
+    "!!z1 z2 z3. [| z1:integ;  z2:integ;  z3: integ |] ==> \
+\                z1\$*(z2\$*z3) = z2\$*(z1\$*z3)"
+ (fn _ => [asm_simp_tac (ZF_ss addsimps [zmult_assoc RS sym,
+					 zmult_commute]) 1]);
+
+(*Integer multiplication is an AC operator*)
+val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
+
goalw Integ.thy [integ_def]
"!!z1 z2 z3. [| z1: integ;  z2: integ;  w: integ |] ==> \
\                (z1 \$+ z2) \$* w = (z1 \$* w) \$+ (z2 \$* w)";
@@ -376,6 +387,14 @@
val integ_typechecks =