# HG changeset patch
# User paulson
# Date 935660057 -7200
# Node ID 7d3136b9af080bc9e1f8c53f7179449b41871b6b
# Parent  98a2afab3f86d018d632036441a1e896a17a6c30
more Join rules including AC-rules

diff -r 98a2afab3f86 -r 7d3136b9af08 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Thu Aug 26 11:33:24 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Thu Aug 26 11:34:17 1999 +0200
@@ -99,6 +99,10 @@
 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]) 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]) 1);
 qed "Join_assoc";
@@ -122,6 +126,13 @@
 
 Addsimps [Join_absorb];
 
+Goalw [Join_def] "A Join (A Join B) = A Join B";
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "Join_left_absorb";
+
+(*Join is an AC-operator*)
+val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute];
 
 
 (*** JN laws ***)