# HG changeset patch
# User paulson
# Date 905864647 -7200
# Node ID 85855f65d0c6229b92fea2873e3cb04c4cb22bbd
# Parent  15c97b95b3e304888af8a9105f001be86c192108
From Compl(A) to -A

diff -r 15c97b95b3e3 -r 85855f65d0c6 NEWS
--- a/NEWS	Tue Sep 15 13:09:23 1998 +0200
+++ b/NEWS	Tue Sep 15 15:04:07 1998 +0200
@@ -20,6 +20,8 @@
   less_imp_add_less  should be replaced by  trans_less_add1
   le_imp_add_le      should be replaced by  trans_le_add1
 
+* HOL: unary - is now overloaded (new type constraints may be required);
+
 * Pure: ML function 'theory_of' replaced by 'theory';
 
 
@@ -209,6 +211,10 @@
 * HOL/recdef can now declare non-recursive functions, with {} supplied as
 the well-founded relation;
 
+* HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
+    Compl A.  The "Compl" syntax remains available as input syntax for this
+    release ONLY.
+
 * HOL/Update: new theory of function updates:
     f(a:=b) == %x. if x=a then b else f x
 may also be iterated as in f(a:=b,c:=d,...);
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -10,7 +10,7 @@
 
 (** The union of two disjoint tilings is a tiling **)
 
-Goal "t: tiling A ==> u: tiling A --> t <= Compl u --> t Un u : tiling A";
+Goal "t: tiling A ==> u: tiling A --> t Int u = {} --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [Un_assoc]) 1);
@@ -59,7 +59,7 @@
 by (induct_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1])));
 by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row]
-                       addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
+                        addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
 qed "dominoes_tile_matrix";
 
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/Set.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -295,19 +295,19 @@
 
 section "Set complement -- Compl";
 
-qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)"
+qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
  (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Compl_iff];
 
-val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
+val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : -A";
 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
 qed "ComplI";
 
 (*This form, with negated conclusion, works well with the Classical prover.
   Negated assumptions behave like formulae on the right side of the notional
   turnstile...*)
-Goalw [Compl_def] "c : Compl(A) ==> c~:A";
+Goalw [Compl_def] "c : -A ==> c~:A";
 by (etac CollectD 1);
 qed "ComplD";
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -79,9 +79,9 @@
                         addIs [common_stable, LeadsTo_weaken_R]) 1);
 val lemma = result();
 
-(*The "ALL m: Compl common" form echoes CMT6.*)
+(*The "ALL m: -common" form echoes CMT6.*)
 Goal "[| ALL m. Constrains prg {m} (maxfg m); \
-\               ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
+\               ALL m: -common. LeadsTo prg {m} (greaterThan m); \
 \               n: common;  id: Acts prg |]  \
 \            ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
 by (rtac lemma 1);
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/Deadlock.ML
--- a/src/HOL/UNITY/Deadlock.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -35,8 +35,8 @@
 
 
 (*Dual of the required property.  Converse inclusion fails.*)
-Goal "(UN i:{i. i < n}. A i) Int Compl (A n) <=  \
-\         (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))";
+Goal "(UN i:{i. i < n}. A i) Int -(A n) <=  \
+\         (UN i:{i. i < n}. (A i) Int -(A(Suc i)))";
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
@@ -45,8 +45,8 @@
 
 
 (*Converse inclusion fails.*)
-Goal "(INT i:{i. i < n}. Compl(A i) Un A (Suc i))  <= \
-\         (INT i:{i. i < n}. Compl(A i)) Un A n";
+Goal "(INT i:{i. i < n}. -A i Un A (Suc i))  <= \
+\         (INT i:{i. i < n}. -A i) Un A n";
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
@@ -55,15 +55,14 @@
 
 
 (*Specialized rewriting*)
-Goal "A 0 Int (Compl (A n) Int \
-\                  (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}";
+Goal "A 0 Int (-(A n) Int (INT i:{i. i < n}. -A i Un A (Suc i))) = {}";
 by (blast_tac (claset() addIs [gr0I]
 		        addDs [impOfSubs INT_Un_Compl_subset]) 1);
 val lemma = result();
 
 (*Reverse direction makes it harder to invoke the ind hyp*)
 Goal "(INT i:{i. i <= n}. A i) = \
-\         A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))";
+\         A 0 Int (INT i:{i. i < n}. -A i Un A(Suc i))";
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac
@@ -73,7 +72,7 @@
 qed "INT_le_equals_Int";
 
 Goal "(INT i:{i. i <= Suc n}. A i) = \
-\         A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))";
+\         A 0 Int (INT i:{i. i <= n}. -A i Un A(Suc i))";
 by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, 
 				  INT_le_equals_Int]) 1);
 qed "INT_le_Suc_equals_Int";
@@ -83,7 +82,7 @@
 val [zeroprem, allprem] = goalw thy [stable_def]
     "[| constrains Acts (A 0 Int A (Suc n)) (A 0);  \
 \       ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \
-\                                         (Compl(A i) Un A(Suc i)) |] \
+\                                         (-A i Un A(Suc i)) |] \
 \    ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
 
 by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/FP.ML
--- a/src/HOL/UNITY/FP.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/FP.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -50,7 +50,7 @@
 qed "FP_weakest";
 
 Goalw [FP_def, stable_def, constrains_def]
-    "Compl (FP Acts) = (UN act:Acts. Compl{s. act^^{s} <= {s}})";
+    "-(FP Acts) = (UN act:Acts. -{s. act^^{s} <= {s}})";
 by (Blast_tac 1);
 qed "Compl_FP";
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -32,7 +32,7 @@
 qed "UN_lessThan_UNIV";
 
 Goalw [lessThan_def, atLeast_def, le_def]
-    "Compl(lessThan k) = atLeast k";
+    "-lessThan k = atLeast k";
 by (Blast_tac 1);
 qed "Compl_lessThan";
 
@@ -58,12 +58,12 @@
 qed "INT_greaterThan_UNIV";
 
 Goalw [greaterThan_def, atMost_def, le_def]
-    "Compl(greaterThan k) = atMost k";
+    "-greaterThan k = atMost k";
 by (Blast_tac 1);
 qed "Compl_greaterThan";
 
 Goalw [greaterThan_def, atMost_def, le_def]
-    "Compl(atMost k) = greaterThan k";
+    "-atMost k = greaterThan k";
 by (Blast_tac 1);
 qed "Compl_atMost";
 
@@ -96,7 +96,7 @@
 qed "UN_atLeast_UNIV";
 
 Goalw [lessThan_def, atLeast_def, le_def]
-    "Compl(atLeast k) = lessThan k";
+    "-atLeast k = lessThan k";
 by (Blast_tac 1);
 qed "Compl_atLeast";
 
@@ -128,7 +128,7 @@
 qed "UN_atMost_UNIV";
 
 Goalw [atMost_def, le_def]
-    "Compl(atMost k) = greaterThan k";
+    "-atMost k = greaterThan k";
 by (Blast_tac 1);
 qed "Compl_atMost";
 Addsimps [Compl_atMost];
@@ -148,31 +148,40 @@
 
 context Set.thy;
 
-(** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
+(** Rewrite rules to eliminate A.  Conditions can be satisfied by letting B
     be any set including A Int C and contained in A Un C, such as B=A or B=C.
 **)
 
 Goal "[| A Int C <= B; B <= A Un C |] \
-\     ==> (A Int B) Un (Compl A Int C) = B Un C";
+\     ==> (A Int B) Un (-A Int C) = B Un C";
 by (Blast_tac 1);
+qed "set_cancel1";
 
 Goal "[| A Int C <= B; B <= A Un C |] \
-\     ==> (A Un B) Int (Compl A Un C) = B Int C";
+\     ==> (A Un B) Int (-A Un C) = B Int C";
 by (Blast_tac 1);
+qed "set_cancel2";
 
 (*The base B=A*)
-Goal "A Un (Compl A Int C) = A Un C";
+Goal "A Un (-A Int C) = A Un C";
 by (Blast_tac 1);
+qed "set_cancel3";
 
-Goal "A Int (Compl A Un C) = A Int C";
+Goal "A Int (-A Un C) = A Int C";
 by (Blast_tac 1);
+qed "set_cancel4";
 
 (*The base B=C*)
-Goal "(A Int C) Un (Compl A Int C) = C";
+Goal "(A Int C) Un (-A Int C) = C";
 by (Blast_tac 1);
+qed "set_cancel5";
 
-Goal "(A Un C) Int (Compl A Un C) = C";
+Goal "(A Un C) Int (-A Un C) = C";
 by (Blast_tac 1);
+qed "set_cancel6";
+
+Addsimps [set_cancel1, set_cancel2, set_cancel3,
+	  set_cancel4, set_cancel5, set_cancel6];
 
 
 (** More ad-hoc rules **)
@@ -180,6 +189,7 @@
 Goal "A Un B - (A - B) = B";
 by (Blast_tac 1);
 qed "Un_Diff_Diff";
+Addsimps [Un_Diff_Diff];
 
 Goal "A Int (B - C) Un C = A Int B Un C";
 by (Blast_tac 1);
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -259,10 +259,10 @@
 by (etac (leI RS le_anti_sym RS sym) 1);
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (ALLGOALS metric_simp_tac);
-by (asm_simp_tac (simpset() addsimps [less_diff_conv, trans_le_add1]) 1);
 by (auto_tac
-    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)],
-	      simpset()));
+    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
+              addIs [diff_le_Suc_diff, diff_less_Suc_diff],
+	      simpset() addsimps [trans_le_add1]));
 qed "E_thm12b";
 
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -73,7 +73,7 @@
   a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
   *)
 
-Goal "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
+Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
 by (simp_tac (simpset() addsimps
 	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym])) 1);
 by Auto_tac;
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/Token.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -34,7 +34,7 @@
 
 AddIffs [thm "N_positive", thm"skip"];
 
-Goalw [stable_def] "stable acts (Compl(E i) Un (HasTok i))";
+Goalw [stable_def] "stable acts (-(E i) Un (HasTok i))";
 by (rtac constrains_weaken 1);
 by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
 by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
@@ -96,7 +96,7 @@
 (*Misra's TR9: the token reaches an arbitrary node*)
 Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)";
 by (rtac leadsTo_weaken_R 1);
-by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")]
+by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
      (wf_nodeOrder RS bounded_induct) 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
 						HasTok_def])));
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -32,8 +32,7 @@
 qed "transient_strengthen";
 
 Goalw [transient_def]
-    "[| act:acts;  A <= Domain act;  act^^A <= Compl A |] \
-\         ==> transient acts A";
+    "[| act:acts;  A <= Domain act;  act^^A <= -A |] ==> transient acts A";
 by (Blast_tac 1);
 qed "transient_mem";
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/Vimage.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -53,7 +53,7 @@
 by (Blast_tac 1);
 qed "vimage_empty";
 
-Goal "f-``(Compl A) = Compl (f-``A)";
+Goal "f-``(-A) = -(f-``A)";
 by (Blast_tac 1);
 qed "vimage_Compl";
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/equalities.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -186,7 +186,7 @@
 qed "Int_empty_right";
 Addsimps[Int_empty_right];
 
-Goal "(A Int B = {}) = (A <= Compl B)";
+Goal "(A Int B = {}) = (A <= -B)";
 by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "disjoint_eq_subset_Compl";
 
@@ -338,33 +338,33 @@
 
 section "Compl";
 
-Goal "A Int Compl(A) = {}";
+Goal "A Int -A = {}";
 by (Blast_tac 1);
 qed "Compl_disjoint";
 Addsimps[Compl_disjoint];
 
-Goal "A Un Compl(A) = UNIV";
+Goal "A Un -A = UNIV";
 by (Blast_tac 1);
 qed "Compl_partition";
 
-Goal "Compl(Compl(A)) = A";
+Goal "- -A = (A:: 'a set)";
 by (Blast_tac 1);
 qed "double_complement";
 Addsimps[double_complement];
 
-Goal "Compl(A Un B) = Compl(A) Int Compl(B)";
+Goal "-(A Un B) = -A Int -B";
 by (Blast_tac 1);
 qed "Compl_Un";
 
-Goal "Compl(A Int B) = Compl(A) Un Compl(B)";
+Goal "-(A Int B) = -A Un -B";
 by (Blast_tac 1);
 qed "Compl_Int";
 
-Goal "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
+Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))";
 by (Blast_tac 1);
 qed "Compl_UN";
 
-Goal "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
+Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))";
 by (Blast_tac 1);
 qed "Compl_INT";
 
@@ -602,7 +602,7 @@
 
 section "-";
 
-Goal "A-B = A Int Compl B";
+Goal "A-B = A Int -B";
 by (Blast_tac 1);
 qed "Diff_eq";
 
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/ex/set.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -72,41 +72,37 @@
 by (Blast_tac 1);
 qed "contra_imageI";
 
-Goal "(a ~: Compl(X)) = (a:X)";
+Goal "(a ~: -(X)) = (a:X)";
 by (Blast_tac 1);
 qed "not_Compl";
 
 (*Lots of backtracking in this proof...*)
 val [compl,fg,Xa] = goal Lfp.thy
-    "[| Compl(f``X) = g``Compl(X);  f(a)=g(b);  a:X |] ==> b:X";
+    "[| -(f``X) = g``(-X);  f(a)=g(b);  a:X |] ==> b:X";
 by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI,
             rtac (compl RS subst), rtac (fg RS subst), stac not_Compl,
             rtac imageI, rtac Xa]);
 qed "disj_lemma";
 
 Goalw [image_def]
-     "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
+     "range(%z. if z:X then f(z) else g(z)) = f``X Un g``(-X)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "range_if_then_else";
 
-Goal "a : X Un Compl(X)";
-by (Blast_tac 1);
-qed "X_Un_Compl";
-
 Goalw [surj_def] "surj(f) = (!a. a : range(f))";
 by (fast_tac (claset() addEs [ssubst]) 1);
 qed "surj_iff_full_range";
 
-Goal "Compl(f``X) = g``Compl(X) ==> surj(%z. if z:X then f(z) else g(z))";
+Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))";
 by (EVERY1[stac surj_iff_full_range, stac range_if_then_else,
            etac subst]);
-by (rtac (X_Un_Compl RS allI) 1);
+by (Blast_tac 1);
 qed "surj_if_then_else";
 
 val [injf,injg,compl,bij] = 
 goal Lfp.thy
-    "[| inj_on f X;  inj_on g (Compl X);  Compl(f``X) = g``Compl(X); \
+    "[| inj_on f X;  inj_on g (-X);  -(f``X) = g``(-X); \
 \       bij = (%z. if z:X then f(z) else g(z)) |] ==> \
 \       inj(bij) & surj(bij)";
 val f_eq_gE = make_elim (compl RS disj_lemma);
@@ -121,7 +117,7 @@
 by (fast_tac (claset() addEs  [inj_onD, f_eq_gE]) 1);
 qed "bij_if_then_else";
 
-Goal "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";
+Goal "!!f:: 'a=>'b.  ? X. X = - (g``(- f``X))";
 by (rtac exI 1);
 by (rtac lfp_Tarski 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
diff -r 15c97b95b3e3 -r 85855f65d0c6 src/HOL/mono.ML
--- a/src/HOL/mono.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/mono.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -51,7 +51,7 @@
 by (Blast_tac 1);
 qed "Diff_mono";
 
-Goal "A<=B ==> Compl(B) <= Compl(A)";
+Goal "!!A::'a set. A <= B ==> -B <= -A";
 by (Blast_tac 1);
 qed "Compl_anti_mono";