--- a/src/HOL/HOL.thy Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/HOL.thy Wed Jul 31 16:10:24 2002 +0200
@@ -507,6 +507,13 @@
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
setup Splitter.setup setup Clasimp.setup
+text{*Needs only HOL-lemmas:*}
+lemma mk_left_commute:
+ assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and
+ c: "\<And>x y. f x y = f y x"
+ shows "f x (f y z) = f y (f x z)"
+by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]])
+
subsubsection {* Generic cases and induction *}
@@ -852,6 +859,49 @@
apply (blast intro: order_less_trans)
done
+declare order_less_irrefl [iff]
+
+lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
+apply(simp add:max_def)
+apply(rule conjI)
+apply(blast intro:order_trans)
+apply(simp add:linorder_not_le)
+apply(blast dest: order_less_trans order_le_less_trans)
+done
+
+lemma max_commute: "!!x::'a::linorder. max x y = max y x"
+apply(simp add:max_def)
+apply(rule conjI)
+apply(blast intro:order_antisym)
+apply(simp add:linorder_not_le)
+apply(blast dest: order_less_trans)
+done
+
+lemmas max_ac = max_assoc max_commute
+ mk_left_commute[of max,OF max_assoc max_commute]
+
+lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
+apply(simp add:min_def)
+apply(rule conjI)
+apply(blast intro:order_trans)
+apply(simp add:linorder_not_le)
+apply(blast dest: order_less_trans order_le_less_trans)
+done
+
+lemma min_commute: "!!x::'a::linorder. min x y = min y x"
+apply(simp add:min_def)
+apply(rule conjI)
+apply(blast intro:order_antisym)
+apply(simp add:linorder_not_le)
+apply(blast dest: order_less_trans)
+done
+
+lemmas min_ac = min_assoc min_commute
+ mk_left_commute[of min,OF min_assoc min_commute]
+
+declare order_less_irrefl [iff del]
+declare order_less_irrefl [simp]
+
lemma split_min:
"P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
by (simp add: min_def)
--- a/src/HOL/Hyperreal/HyperDef.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Hyperreal/HyperDef.ML Wed Jul 31 16:10:24 2002 +0200
@@ -352,9 +352,8 @@
(*For AC rewriting*)
Goal "(x::hypreal)+(y+z)=y+(x+z)";
-by (rtac (hypreal_add_commute RS trans) 1);
-by (rtac (hypreal_add_assoc RS trans) 1);
-by (rtac (hypreal_add_commute RS arg_cong) 1);
+by(rtac ([hypreal_add_assoc,hypreal_add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "hypreal_add_left_commute";
(* hypreal addition is an AC operator *)
@@ -476,11 +475,10 @@
by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
qed "hypreal_mult_assoc";
-qed_goal "hypreal_mult_left_commute" (the_context ())
- "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
- (fn _ => [rtac (hypreal_mult_commute RS trans) 1,
- rtac (hypreal_mult_assoc RS trans) 1,
- rtac (hypreal_mult_commute RS arg_cong) 1]);
+Goal "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)";
+by(rtac ([hypreal_mult_assoc,hypreal_mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
+qed "hypreal_mult_left_commute";
(* hypreal multiplication is an AC operator *)
bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute,
--- a/src/HOL/Hyperreal/HyperNat.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Hyperreal/HyperNat.ML Wed Jul 31 16:10:24 2002 +0200
@@ -161,9 +161,8 @@
(*For AC rewriting*)
Goal "(x::hypnat)+(y+z)=y+(x+z)";
-by (rtac (hypnat_add_commute RS trans) 1);
-by (rtac (hypnat_add_assoc RS trans) 1);
-by (rtac (hypnat_add_commute RS arg_cong) 1);
+by(rtac ([hypnat_add_assoc,hypnat_add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "hypnat_add_left_commute";
(* hypnat addition is an AC operator *)
@@ -301,9 +300,8 @@
Goal "(z1::hypnat) * (z2 * z3) = z2 * (z1 * z3)";
-by (rtac (hypnat_mult_commute RS trans) 1);
-by (rtac (hypnat_mult_assoc RS trans) 1);
-by (rtac (hypnat_mult_commute RS arg_cong) 1);
+by(rtac ([hypnat_mult_assoc,hypnat_mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "hypnat_mult_left_commute";
(* hypnat multiplication is an AC operator *)
--- a/src/HOL/Integ/IntDef.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Integ/IntDef.ML Wed Jul 31 16:10:24 2002 +0200
@@ -139,9 +139,8 @@
(*For AC rewriting*)
Goal "(x::int)+(y+z)=y+(x+z)";
-by (rtac (zadd_commute RS trans) 1);
-by (rtac (zadd_assoc RS trans) 1);
-by (rtac (zadd_commute RS arg_cong) 1);
+by(rtac ([zadd_assoc,zadd_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "zadd_left_commute";
(*Integer addition is an AC operator*)
@@ -270,9 +269,8 @@
(*For AC rewriting*)
Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
-by (rtac (zmult_commute RS trans) 1);
-by (rtac (zmult_assoc RS trans) 1);
-by (rtac (zmult_commute RS arg_cong) 1);
+by(rtac ([zmult_assoc,zmult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "zmult_left_commute";
(*Integer multiplication is an AC operator*)
--- a/src/HOL/Library/Ring_and_Field.thy Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Library/Ring_and_Field.thy Wed Jul 31 16:10:24 2002 +0200
@@ -55,11 +55,7 @@
qed
lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))"
-proof -
- have "a + (b + c) = (a + b) + c" by (simp only: add_assoc)
- also have "... = (b + a) + c" by (simp only: add_commute)
- finally show ?thesis by (simp only: add_assoc)
-qed
+by(rule mk_left_commute[OF add_assoc add_commute])
theorems ring_add_ac = add_assoc add_commute add_left_commute
@@ -94,11 +90,7 @@
qed
lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))"
-proof -
- have "a * (b * c) = (a * b) * c" by (simp only: mult_assoc)
- also have "... = (b * a) * c" by (simp only: mult_commute)
- finally show ?thesis by (simp only: mult_assoc)
-qed
+by(rule mk_left_commute[OF mult_assoc mult_commute])
theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
--- a/src/HOL/Nat.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Nat.ML Wed Jul 31 16:10:24 2002 +0200
@@ -195,9 +195,8 @@
qed "add_commute";
Goal "x+(y+z)=y+((x+z)::nat)";
-by (rtac (add_commute RS trans) 1);
-by (rtac (add_assoc RS trans) 1);
-by (rtac (add_commute RS arg_cong) 1);
+by(rtac ([add_assoc,add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "add_left_commute";
(*Addition is an AC-operator*)
@@ -426,11 +425,8 @@
qed "mult_assoc";
Goal "x*(y*z) = y*((x*z)::nat)";
-by (rtac trans 1);
-by (rtac mult_commute 1);
-by (rtac trans 1);
-by (rtac mult_assoc 1);
-by (rtac (mult_commute RS arg_cong) 1);
+by(rtac ([mult_assoc,mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "mult_left_commute";
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
--- a/src/HOL/Real/PRat.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Real/PRat.ML Wed Jul 31 16:10:24 2002 +0200
@@ -176,9 +176,8 @@
(*For AC rewriting*)
Goal "(z1::prat) + (z2 + z3) = z2 + (z1 + z3)";
-by (rtac (prat_add_commute RS trans) 1);
-by (rtac (prat_add_assoc RS trans) 1);
-by (rtac (prat_add_commute RS arg_cong) 1);
+by(rtac ([prat_add_assoc,prat_add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "prat_add_left_commute";
(* Positive Rational addition is an AC operator *)
@@ -222,9 +221,8 @@
(*For AC rewriting*)
Goal "(x::prat)*(y*z)=y*(x*z)";
-by (rtac (prat_mult_commute RS trans) 1);
-by (rtac (prat_mult_assoc RS trans) 1);
-by (rtac (prat_mult_commute RS arg_cong) 1);
+by(rtac ([prat_mult_assoc,prat_mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "prat_mult_left_commute";
(*Positive Rational multiplication is an AC operator*)
--- a/src/HOL/Real/PReal.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Real/PReal.ML Wed Jul 31 16:10:24 2002 +0200
@@ -266,9 +266,8 @@
qed "preal_add_assoc";
Goal "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)";
-by (rtac (preal_add_commute RS trans) 1);
-by (rtac (preal_add_assoc RS trans) 1);
-by (rtac (preal_add_commute RS arg_cong) 1);
+by(rtac ([preal_add_assoc,preal_add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "preal_add_left_commute";
(* Positive Reals addition is an AC operator *)
@@ -347,9 +346,8 @@
qed "preal_mult_assoc";
Goal "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)";
-by (rtac (preal_mult_commute RS trans) 1);
-by (rtac (preal_mult_assoc RS trans) 1);
-by (rtac (preal_mult_commute RS arg_cong) 1);
+by(rtac ([preal_mult_assoc,preal_mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "preal_mult_left_commute";
(* Positive Reals multiplication is an AC operator *)
--- a/src/HOL/Real/RealDef.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Real/RealDef.ML Wed Jul 31 16:10:24 2002 +0200
@@ -177,9 +177,8 @@
(*For AC rewriting*)
Goal "(x::real)+(y+z)=y+(x+z)";
-by (rtac (real_add_commute RS trans) 1);
-by (rtac (real_add_assoc RS trans) 1);
-by (rtac (real_add_commute RS arg_cong) 1);
+by(rtac ([real_add_assoc,real_add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "real_add_left_commute";
(* real addition is an AC operator *)
@@ -329,9 +328,8 @@
qed "real_mult_assoc";
Goal "(z1::real) * (z2 * z3) = z2 * (z1 * z3)";
-by (rtac (real_mult_commute RS trans) 1);
-by (rtac (real_mult_assoc RS trans) 1);
-by (rtac (real_mult_commute RS arg_cong) 1);
+by(rtac ([real_mult_assoc,real_mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "real_mult_left_commute";
(* real multiplication is an AC operator *)
--- a/src/HOL/UNITY/Union.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/UNITY/Union.ML Wed Jul 31 16:10:24 2002 +0200
@@ -109,16 +109,16 @@
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
qed "Join_commute";
-
-Goal "A Join (B Join C) = B Join (A Join C)";
-by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def, insert_absorb]) 1);
-qed "Join_left_commute";
-
-
Goal "(F Join G) Join H = F Join (G Join H)";
by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
qed "Join_assoc";
+Goal "A Join (B Join C) = B Join (A Join C)";
+by(rtac ([Join_assoc,Join_commute] MRS
+ read_instantiate[("f","op Join")](thm"mk_left_commute")) 1);
+qed "Join_left_commute";
+
+
Goalw [Join_def, SKIP_def] "SKIP Join F = F";
by (rtac program_equalityI 1);
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));