# HG changeset patch
# User paulson
# Date 886858737 -3600
# Node ID b435c5a320b0ea944d4282559e9c0d4e495821d0
# Parent  cdf16a9fb2ce114d3fa0d86c30a92d7c9e0e134b
AC and other rewrite rules for Un and Int

diff -r cdf16a9fb2ce -r b435c5a320b0 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Sat Feb 07 14:38:15 1998 +0100
+++ b/src/HOL/equalities.ML	Sat Feb 07 14:38:57 1998 +0100
@@ -133,14 +133,25 @@
 qed "Int_absorb";
 Addsimps[Int_absorb];
 
+goal thy " A Int (A Int B) = A Int B";
+by (Blast_tac 1);
+qed "Int_left_absorb";
+
 goal thy "A Int B  =  B Int A";
 by (Blast_tac 1);
 qed "Int_commute";
 
+goal thy "A Int (B Int C) = B Int (A Int C)";
+by (Blast_tac 1);
+qed "Int_left_commute";
+
 goal thy "(A Int B) Int C  =  A Int (B Int C)";
 by (Blast_tac 1);
 qed "Int_assoc";
 
+(*Intersection is an AC-operator*)
+val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
+
 goal thy "{} Int B = {}";
 by (Blast_tac 1);
 qed "Int_empty_left";
@@ -197,7 +208,7 @@
 by (Blast_tac 1);
 qed "Un_commute";
 
-goal thy " A Un (B Un C) = B Un (A Un C)";
+goal thy "A Un (B Un C) = B Un (A Un C)";
 by (Blast_tac 1);
 qed "Un_left_commute";
 
@@ -205,6 +216,9 @@
 by (Blast_tac 1);
 qed "Un_assoc";
 
+(*Union is an AC-operator*)
+val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
+
 goal thy "{} Un B = B";
 by (Blast_tac 1);
 qed "Un_empty_left";
@@ -247,10 +261,14 @@
 by (Blast_tac 1);
 qed "Int_insert_right";
 
-goal thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
+goal thy "A Un (B Int C)  =  (A Un B) Int (A Un C)";
 by (Blast_tac 1);
 qed "Un_Int_distrib";
 
+goal thy "(B Int C) Un A =  (B Un A) Int (C Un A)";
+by (Blast_tac 1);
+qed "Un_Int_distrib2";
+
 goal thy
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
 by (Blast_tac 1);
@@ -507,6 +525,10 @@
 
 section "-";
 
+goal thy "A-B = A Int Compl B";
+by (Blast_tac 1);
+qed "Diff_eq_Int_Compl";
+
 goal thy "A-A = {}";
 by (Blast_tac 1);
 qed "Diff_cancel";