--- 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,...);
--- 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";
--- 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";
--- 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);
--- 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
--- 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";
--- 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);
--- 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";
--- 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;
--- 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])));
--- 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";
--- 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";
--- 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";
--- 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));
--- 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";