more Join rules including AC-rules
authorpaulson
Thu Aug 26 11:34:17 1999 +0200 (1999-08-26)
changeset 73607d3136b9af08
parent 7359 98a2afab3f86
child 7361 477e1bdf230f
more Join rules including AC-rules
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Union.ML	Thu Aug 26 11:33:24 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Union.ML	Thu Aug 26 11:34:17 1999 +0200
     1.3 @@ -99,6 +99,10 @@
     1.4  by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
     1.5  qed "Join_commute";
     1.6  
     1.7 +Goal "A Join (B Join C) = B Join (A Join C)";
     1.8 +by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def]) 1);
     1.9 +qed "Join_left_commute";
    1.10 +
    1.11  Goal "(F Join G) Join H = F Join (G Join H)";
    1.12  by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
    1.13  qed "Join_assoc";
    1.14 @@ -122,6 +126,13 @@
    1.15  
    1.16  Addsimps [Join_absorb];
    1.17  
    1.18 +Goalw [Join_def] "A Join (A Join B) = A Join B";
    1.19 +by (rtac program_equalityI 1);
    1.20 +by Auto_tac;
    1.21 +qed "Join_left_absorb";
    1.22 +
    1.23 +(*Join is an AC-operator*)
    1.24 +val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute];
    1.25  
    1.26  
    1.27  (*** JN laws ***)