added mk_left_commute to HOL.thy and used it "everywhere"
authornipkow
Wed Jul 31 16:10:24 2002 +0200 (2002-07-31)
changeset 13438527811f00c56
parent 13437 01b3fc0cc1b8
child 13439 2f98365f57a8
added mk_left_commute to HOL.thy and used it "everywhere"
src/HOL/HOL.thy
src/HOL/Hyperreal/HyperDef.ML
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Integ/IntDef.ML
src/HOL/Library/Ring_and_Field.thy
src/HOL/Nat.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RealDef.ML
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Jul 31 14:40:40 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Jul 31 16:10:24 2002 +0200
     1.3 @@ -507,6 +507,13 @@
     1.4  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
     1.5  setup Splitter.setup setup Clasimp.setup
     1.6  
     1.7 +text{*Needs only HOL-lemmas:*}
     1.8 +lemma mk_left_commute:
     1.9 +  assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and
    1.10 +          c: "\<And>x y. f x y = f y x"
    1.11 +  shows "f x (f y z) = f y (f x z)"
    1.12 +by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]])
    1.13 +
    1.14  
    1.15  subsubsection {* Generic cases and induction *}
    1.16  
    1.17 @@ -852,6 +859,49 @@
    1.18    apply (blast intro: order_less_trans)
    1.19    done
    1.20  
    1.21 +declare order_less_irrefl [iff]
    1.22 +
    1.23 +lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
    1.24 +apply(simp add:max_def)
    1.25 +apply(rule conjI)
    1.26 +apply(blast intro:order_trans)
    1.27 +apply(simp add:linorder_not_le)
    1.28 +apply(blast dest: order_less_trans order_le_less_trans)
    1.29 +done
    1.30 +
    1.31 +lemma max_commute: "!!x::'a::linorder. max x y = max y x"
    1.32 +apply(simp add:max_def)
    1.33 +apply(rule conjI)
    1.34 +apply(blast intro:order_antisym)
    1.35 +apply(simp add:linorder_not_le)
    1.36 +apply(blast dest: order_less_trans)
    1.37 +done
    1.38 +
    1.39 +lemmas max_ac = max_assoc max_commute
    1.40 +                mk_left_commute[of max,OF max_assoc max_commute]
    1.41 +
    1.42 +lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
    1.43 +apply(simp add:min_def)
    1.44 +apply(rule conjI)
    1.45 +apply(blast intro:order_trans)
    1.46 +apply(simp add:linorder_not_le)
    1.47 +apply(blast dest: order_less_trans order_le_less_trans)
    1.48 +done
    1.49 +
    1.50 +lemma min_commute: "!!x::'a::linorder. min x y = min y x"
    1.51 +apply(simp add:min_def)
    1.52 +apply(rule conjI)
    1.53 +apply(blast intro:order_antisym)
    1.54 +apply(simp add:linorder_not_le)
    1.55 +apply(blast dest: order_less_trans)
    1.56 +done
    1.57 +
    1.58 +lemmas min_ac = min_assoc min_commute
    1.59 +                mk_left_commute[of min,OF min_assoc min_commute]
    1.60 +
    1.61 +declare order_less_irrefl [iff del]
    1.62 +declare order_less_irrefl [simp]
    1.63 +
    1.64  lemma split_min:
    1.65      "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
    1.66    by (simp add: min_def)
     2.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Wed Jul 31 14:40:40 2002 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperDef.ML	Wed Jul 31 16:10:24 2002 +0200
     2.3 @@ -352,9 +352,8 @@
     2.4  
     2.5  (*For AC rewriting*)
     2.6  Goal "(x::hypreal)+(y+z)=y+(x+z)";
     2.7 -by (rtac (hypreal_add_commute RS trans) 1);
     2.8 -by (rtac (hypreal_add_assoc RS trans) 1);
     2.9 -by (rtac (hypreal_add_commute RS arg_cong) 1);
    2.10 +by(rtac ([hypreal_add_assoc,hypreal_add_commute] MRS
    2.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    2.12  qed "hypreal_add_left_commute";
    2.13  
    2.14  (* hypreal addition is an AC operator *)
    2.15 @@ -476,11 +475,10 @@
    2.16  by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
    2.17  qed "hypreal_mult_assoc";
    2.18  
    2.19 -qed_goal "hypreal_mult_left_commute" (the_context ())
    2.20 -    "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
    2.21 - (fn _ => [rtac (hypreal_mult_commute RS trans) 1, 
    2.22 -           rtac (hypreal_mult_assoc RS trans) 1,
    2.23 -           rtac (hypreal_mult_commute RS arg_cong) 1]);
    2.24 +Goal "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)";
    2.25 +by(rtac ([hypreal_mult_assoc,hypreal_mult_commute] MRS
    2.26 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    2.27 +qed "hypreal_mult_left_commute";
    2.28  
    2.29  (* hypreal multiplication is an AC operator *)
    2.30  bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, 
     3.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Wed Jul 31 14:40:40 2002 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Wed Jul 31 16:10:24 2002 +0200
     3.3 @@ -161,9 +161,8 @@
     3.4  
     3.5  (*For AC rewriting*)
     3.6  Goal "(x::hypnat)+(y+z)=y+(x+z)";
     3.7 -by (rtac (hypnat_add_commute RS trans) 1);
     3.8 -by (rtac (hypnat_add_assoc RS trans) 1);
     3.9 -by (rtac (hypnat_add_commute RS arg_cong) 1);
    3.10 +by(rtac ([hypnat_add_assoc,hypnat_add_commute] MRS
    3.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    3.12  qed "hypnat_add_left_commute";
    3.13  
    3.14  (* hypnat addition is an AC operator *)
    3.15 @@ -301,9 +300,8 @@
    3.16  
    3.17  
    3.18  Goal "(z1::hypnat) * (z2 * z3) = z2 * (z1 * z3)";
    3.19 -by (rtac (hypnat_mult_commute RS trans) 1);
    3.20 -by (rtac (hypnat_mult_assoc RS trans) 1);
    3.21 -by (rtac (hypnat_mult_commute RS arg_cong) 1);
    3.22 +by(rtac ([hypnat_mult_assoc,hypnat_mult_commute] MRS
    3.23 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    3.24  qed "hypnat_mult_left_commute";
    3.25  
    3.26  (* hypnat multiplication is an AC operator *)
     4.1 --- a/src/HOL/Integ/IntDef.ML	Wed Jul 31 14:40:40 2002 +0200
     4.2 +++ b/src/HOL/Integ/IntDef.ML	Wed Jul 31 16:10:24 2002 +0200
     4.3 @@ -139,9 +139,8 @@
     4.4  
     4.5  (*For AC rewriting*)
     4.6  Goal "(x::int)+(y+z)=y+(x+z)";
     4.7 -by (rtac (zadd_commute RS trans) 1);
     4.8 -by (rtac (zadd_assoc RS trans) 1);
     4.9 -by (rtac (zadd_commute RS arg_cong) 1);
    4.10 +by(rtac ([zadd_assoc,zadd_commute] MRS
    4.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    4.12  qed "zadd_left_commute";
    4.13  
    4.14  (*Integer addition is an AC operator*)
    4.15 @@ -270,9 +269,8 @@
    4.16  
    4.17  (*For AC rewriting*)
    4.18  Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
    4.19 -by (rtac (zmult_commute RS trans) 1);
    4.20 -by (rtac (zmult_assoc RS trans) 1);
    4.21 -by (rtac (zmult_commute RS arg_cong) 1);
    4.22 +by(rtac ([zmult_assoc,zmult_commute] MRS
    4.23 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    4.24  qed "zmult_left_commute";
    4.25  
    4.26  (*Integer multiplication is an AC operator*)
     5.1 --- a/src/HOL/Library/Ring_and_Field.thy	Wed Jul 31 14:40:40 2002 +0200
     5.2 +++ b/src/HOL/Library/Ring_and_Field.thy	Wed Jul 31 16:10:24 2002 +0200
     5.3 @@ -55,11 +55,7 @@
     5.4  qed
     5.5  
     5.6  lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))"
     5.7 -proof -
     5.8 -  have "a + (b + c) = (a + b) + c" by (simp only: add_assoc)
     5.9 -  also have "... = (b + a) + c" by (simp only: add_commute)
    5.10 -  finally show ?thesis by (simp only: add_assoc) 
    5.11 -qed
    5.12 +by(rule mk_left_commute[OF add_assoc add_commute])
    5.13  
    5.14  theorems ring_add_ac = add_assoc add_commute add_left_commute
    5.15  
    5.16 @@ -94,11 +90,7 @@
    5.17  qed
    5.18  
    5.19  lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))"
    5.20 -proof -
    5.21 -  have "a * (b * c) = (a * b) * c" by (simp only: mult_assoc)
    5.22 -  also have "... = (b * a) * c" by (simp only: mult_commute)
    5.23 -  finally show ?thesis by (simp only: mult_assoc)
    5.24 -qed
    5.25 +by(rule mk_left_commute[OF mult_assoc mult_commute])
    5.26  
    5.27  theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
    5.28  
     6.1 --- a/src/HOL/Nat.ML	Wed Jul 31 14:40:40 2002 +0200
     6.2 +++ b/src/HOL/Nat.ML	Wed Jul 31 16:10:24 2002 +0200
     6.3 @@ -195,9 +195,8 @@
     6.4  qed "add_commute";
     6.5  
     6.6  Goal "x+(y+z)=y+((x+z)::nat)";
     6.7 -by (rtac (add_commute RS trans) 1);
     6.8 -by (rtac (add_assoc RS trans) 1);
     6.9 -by (rtac (add_commute RS arg_cong) 1);
    6.10 +by(rtac ([add_assoc,add_commute] MRS
    6.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    6.12  qed "add_left_commute";
    6.13  
    6.14  (*Addition is an AC-operator*)
    6.15 @@ -426,11 +425,8 @@
    6.16  qed "mult_assoc";
    6.17  
    6.18  Goal "x*(y*z) = y*((x*z)::nat)";
    6.19 -by (rtac trans 1);
    6.20 -by (rtac mult_commute 1);
    6.21 -by (rtac trans 1);
    6.22 -by (rtac mult_assoc 1);
    6.23 -by (rtac (mult_commute RS arg_cong) 1);
    6.24 +by(rtac ([mult_assoc,mult_commute] MRS
    6.25 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    6.26  qed "mult_left_commute";
    6.27  
    6.28  bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
     7.1 --- a/src/HOL/Real/PRat.ML	Wed Jul 31 14:40:40 2002 +0200
     7.2 +++ b/src/HOL/Real/PRat.ML	Wed Jul 31 16:10:24 2002 +0200
     7.3 @@ -176,9 +176,8 @@
     7.4  
     7.5  (*For AC rewriting*)
     7.6  Goal "(z1::prat) + (z2 + z3) = z2 + (z1 + z3)";
     7.7 -by (rtac (prat_add_commute RS trans) 1);
     7.8 -by (rtac (prat_add_assoc RS trans) 1);
     7.9 -by (rtac (prat_add_commute RS arg_cong) 1);
    7.10 +by(rtac ([prat_add_assoc,prat_add_commute] MRS
    7.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    7.12  qed "prat_add_left_commute";
    7.13  
    7.14  (* Positive Rational addition is an AC operator *)
    7.15 @@ -222,9 +221,8 @@
    7.16  
    7.17  (*For AC rewriting*)
    7.18  Goal "(x::prat)*(y*z)=y*(x*z)";
    7.19 -by (rtac (prat_mult_commute RS trans) 1);
    7.20 -by (rtac (prat_mult_assoc RS trans) 1);
    7.21 -by (rtac (prat_mult_commute RS arg_cong) 1);
    7.22 +by(rtac ([prat_mult_assoc,prat_mult_commute] MRS
    7.23 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    7.24  qed "prat_mult_left_commute";
    7.25  
    7.26  (*Positive Rational multiplication is an AC operator*)
     8.1 --- a/src/HOL/Real/PReal.ML	Wed Jul 31 14:40:40 2002 +0200
     8.2 +++ b/src/HOL/Real/PReal.ML	Wed Jul 31 16:10:24 2002 +0200
     8.3 @@ -266,9 +266,8 @@
     8.4  qed "preal_add_assoc";
     8.5  
     8.6  Goal "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)";
     8.7 -by (rtac (preal_add_commute RS trans) 1);
     8.8 -by (rtac (preal_add_assoc RS trans) 1);
     8.9 -by (rtac (preal_add_commute RS arg_cong) 1);
    8.10 +by(rtac ([preal_add_assoc,preal_add_commute] MRS
    8.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    8.12  qed "preal_add_left_commute";
    8.13  
    8.14  (* Positive Reals addition is an AC operator *)
    8.15 @@ -347,9 +346,8 @@
    8.16  qed "preal_mult_assoc";
    8.17  
    8.18  Goal "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)";
    8.19 -by (rtac (preal_mult_commute RS trans) 1);
    8.20 -by (rtac (preal_mult_assoc RS trans) 1);
    8.21 -by (rtac (preal_mult_commute RS arg_cong) 1);
    8.22 +by(rtac ([preal_mult_assoc,preal_mult_commute] MRS
    8.23 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    8.24  qed "preal_mult_left_commute";
    8.25  
    8.26  (* Positive Reals multiplication is an AC operator *)
     9.1 --- a/src/HOL/Real/RealDef.ML	Wed Jul 31 14:40:40 2002 +0200
     9.2 +++ b/src/HOL/Real/RealDef.ML	Wed Jul 31 16:10:24 2002 +0200
     9.3 @@ -177,9 +177,8 @@
     9.4  
     9.5  (*For AC rewriting*)
     9.6  Goal "(x::real)+(y+z)=y+(x+z)";
     9.7 -by (rtac (real_add_commute RS trans) 1);
     9.8 -by (rtac (real_add_assoc RS trans) 1);
     9.9 -by (rtac (real_add_commute RS arg_cong) 1);
    9.10 +by(rtac ([real_add_assoc,real_add_commute] MRS
    9.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    9.12  qed "real_add_left_commute";
    9.13  
    9.14  (* real addition is an AC operator *)
    9.15 @@ -329,9 +328,8 @@
    9.16  qed "real_mult_assoc";
    9.17  
    9.18  Goal "(z1::real) * (z2 * z3) = z2 * (z1 * z3)";
    9.19 -by (rtac (real_mult_commute RS trans) 1);
    9.20 -by (rtac (real_mult_assoc RS trans) 1);
    9.21 -by (rtac (real_mult_commute RS arg_cong) 1);
    9.22 +by(rtac ([real_mult_assoc,real_mult_commute] MRS
    9.23 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    9.24  qed "real_mult_left_commute";
    9.25  
    9.26  (* real multiplication is an AC operator *)
    10.1 --- a/src/HOL/UNITY/Union.ML	Wed Jul 31 14:40:40 2002 +0200
    10.2 +++ b/src/HOL/UNITY/Union.ML	Wed Jul 31 16:10:24 2002 +0200
    10.3 @@ -109,16 +109,16 @@
    10.4  by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
    10.5  qed "Join_commute";
    10.6  
    10.7 -
    10.8 -Goal "A Join (B Join C) = B Join (A Join C)";
    10.9 -by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def, insert_absorb]) 1);
   10.10 -qed "Join_left_commute";
   10.11 -
   10.12 -
   10.13  Goal "(F Join G) Join H = F Join (G Join H)";
   10.14  by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
   10.15  qed "Join_assoc";
   10.16   
   10.17 +Goal "A Join (B Join C) = B Join (A Join C)";
   10.18 +by(rtac ([Join_assoc,Join_commute] MRS
   10.19 +         read_instantiate[("f","op Join")](thm"mk_left_commute")) 1);
   10.20 +qed "Join_left_commute";
   10.21 +
   10.22 +
   10.23  Goalw [Join_def, SKIP_def] "SKIP Join F = F";
   10.24  by (rtac program_equalityI 1);
   10.25  by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));