# HG changeset patch
# User nipkow
# Date 1028124624 -7200
# Node ID 527811f00c5689cea28be99ca58747ef66e0e091
# Parent  01b3fc0cc1b893948f216b15cc81d9fae3678a46
added mk_left_commute to HOL.thy and used it "everywhere"

diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/HOL.thy
--- 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)
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Hyperreal/HyperDef.ML
--- 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, 
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Hyperreal/HyperNat.ML
--- 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 *)
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Integ/IntDef.ML
--- 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*)
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Library/Ring_and_Field.thy
--- 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
 
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Nat.ML
--- 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]);
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Real/PRat.ML
--- 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*)
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Real/PReal.ML
--- 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 *)
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/Real/RealDef.ML
--- 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 *)
diff -r 01b3fc0cc1b8 -r 527811f00c56 src/HOL/UNITY/Union.ML
--- 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])));