# HG changeset patch
# User nipkow
# Date 825946653 -3600
# Node ID e5eb247ad13c06159ce2462aac7ab0890ec37ccd
# Parent  63fed88fe8e6e2ce6cb68bcd558fb72f65bea632
Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
Added cardinality to Finite.

diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Finite.ML	Mon Mar 04 14:37:33 1996 +0100
@@ -1,13 +1,15 @@
 (*  Title:      HOL/Finite.thy
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
+    Author:     Lawrence C Paulson & Tobias Nipkow
+    Copyright   1995  University of Cambridge & TU Muenchen
 
-Finite powerset operator
+Finite sets and their cardinality
 *)
 
 open Finite;
 
+(*** Fin ***)
+
 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
@@ -31,8 +33,6 @@
 by (REPEAT (ares_tac prems 1));
 qed "Fin_induct";
 
-(** Simplification for Fin **)
-
 Addsimps Fin.intrs;
 
 (*The union of two finite sets is finite*)
@@ -54,6 +54,19 @@
 by (ALLGOALS Asm_simp_tac);
 qed "Fin_subset";
 
+goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
+by(fast_tac (set_cs addIs [Fin_UnI] addDs
+                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
+qed "subset_Fin";
+Addsimps[subset_Fin];
+
+goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
+by(stac insert_is_Un 1);
+by(Simp_tac 1);
+by(fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
+qed "insert_Fin";
+Addsimps[insert_Fin];
+
 (*The image of a finite set is finite*)
 val major::_ = goal Finite.thy
     "F: Fin(A) ==> h``F : Fin(h``A)";
@@ -72,7 +85,7 @@
 by (rtac (Diff_insert RS ssubst) 2);
 by (ALLGOALS (asm_simp_tac
                 (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
-qed "Fin_empty_induct_lemma";
+val lemma = result();
 
 val prems = goal Finite.thy 
     "[| b: Fin(A);                                              \
@@ -80,6 +93,227 @@
 \       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
 \    |] ==> P({})";
 by (rtac (Diff_cancel RS subst) 1);
-by (rtac (Fin_empty_induct_lemma RS mp) 1);
+by (rtac (lemma RS mp) 1);
 by (REPEAT (ares_tac (subset_refl::prems) 1));
 qed "Fin_empty_induct";
+
+
+(*** finite ***)
+
+val major::prems = goalw Finite.thy [finite_def]
+    "[| finite F;  P({}); \
+\       !!F x. [| finite F;  x~:F;  P(F) |] ==> P(insert x F) \
+\    |] ==> P(F)";
+by (rtac (major RS Fin_induct) 1);
+by (REPEAT (ares_tac prems 1));
+qed "finite_induct";
+
+
+goalw Finite.thy [finite_def] "finite {}";
+by(Simp_tac 1);
+qed "finite_emptyI";
+Addsimps [finite_emptyI];
+
+goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
+by(Asm_simp_tac 1);
+qed "finite_insertI";
+
+(*The union of two finite sets is finite*)
+goalw Finite.thy [finite_def]
+    "!!F. [| finite F;  finite G |] ==> finite(F Un G)";
+by(Asm_simp_tac 1);
+qed "finite_UnI";
+
+goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
+be Fin_subset 1;
+ba 1;
+qed "finite_subset";
+
+goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
+by(Simp_tac 1);
+qed "subset_finite";
+Addsimps[subset_finite];
+
+goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
+by(Simp_tac 1);
+qed "insert_finite";
+Addsimps[insert_finite];
+
+goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
+be finite_induct 1;
+by(Simp_tac 1);
+by(asm_simp_tac (!simpset addsimps [insert_Diff_if]
+                          setloop split_tac[expand_if]) 1);
+qed "finite_Diff";
+Addsimps [finite_Diff];
+
+(*The image of a finite set is finite*)
+goal Finite.thy "!!F. finite F ==> finite(h``F)";
+be finite_induct 1;
+by(ALLGOALS Asm_simp_tac);
+qed "finite_imageI";
+
+val major::prems = goalw Finite.thy [finite_def]
+    "[| finite A;                                       \
+\       P(A);                                           \
+\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
+\    |] ==> P({})";
+by (rtac (major RS Fin_empty_induct) 1);
+by (REPEAT (ares_tac (subset_refl::prems) 1));
+qed "finite_empty_induct";
+
+
+(*** Cardinality ***)
+
+goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
+by(fast_tac eq_cs 1);
+val Collect_conv_insert = result();
+
+goalw Finite.thy [card_def] "card {} = 0";
+br Least_equality 1;
+by(ALLGOALS Asm_full_simp_tac);
+qed "card_empty";
+Addsimps [card_empty];
+
+(*Addsimps [Collect_conv_insert];*)
+
+val [major] = goal Finite.thy
+  "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
+br (major RS finite_induct) 1;
+ by(res_inst_tac [("x","0")] exI 1);
+ by(Simp_tac 1);
+be exE 1;
+be exE 1;
+by(hyp_subst_tac 1);
+by(res_inst_tac [("x","Suc n")] exI 1);
+by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
+by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]
+                          addcongs [Collect_cong1]) 1);
+qed "finite_has_card";
+
+goal Finite.thy
+  "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
+\  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
+by(res_inst_tac [("n","n")] natE 1);
+ by(hyp_subst_tac 1);
+ by(Asm_full_simp_tac 1);
+by(rename_tac "m" 1);
+by(hyp_subst_tac 1);
+by(case_tac "? a. a:A" 1);
+ by(res_inst_tac [("x","0")] exI 2);
+ by(Simp_tac 2);
+ by(fast_tac eq_cs 2);
+be exE 1;
+by(Simp_tac 1);
+br exI 1;
+br conjI 1;
+ br disjI2 1;
+ br refl 1;
+be equalityE 1;
+by(asm_full_simp_tac
+     (!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
+by(SELECT_GOAL(safe_tac eq_cs)1);
+  by(Asm_full_simp_tac 1);
+  by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
+  by(SELECT_GOAL(safe_tac eq_cs)1);
+   by(subgoal_tac "x ~= f m" 1);
+    by(fast_tac set_cs 2);
+   by(subgoal_tac "? k. f k = x & k<m" 1);
+    by(best_tac set_cs 2);
+   by(SELECT_GOAL(safe_tac HOL_cs)1);
+   by(res_inst_tac [("x","k")] exI 1);
+   by(Asm_simp_tac 1);
+  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+  by(best_tac set_cs 1);
+ bd sym 1;
+ by(rotate_tac ~1 1);
+ by(Asm_full_simp_tac 1);
+ by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
+ by(SELECT_GOAL(safe_tac eq_cs)1);
+  by(subgoal_tac "x ~= f m" 1);
+   by(fast_tac set_cs 2);
+  by(subgoal_tac "? k. f k = x & k<m" 1);
+   by(best_tac set_cs 2);
+  by(SELECT_GOAL(safe_tac HOL_cs)1);
+  by(res_inst_tac [("x","k")] exI 1);
+  by(Asm_simp_tac 1);
+ by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by(best_tac set_cs 1);
+by(res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
+by(SELECT_GOAL(safe_tac eq_cs)1);
+ by(subgoal_tac "x ~= f i" 1);
+  by(fast_tac set_cs 2);
+ by(case_tac "x = f m" 1);
+  by(res_inst_tac [("x","i")] exI 1);
+  by(Asm_simp_tac 1);
+ by(subgoal_tac "? k. f k = x & k<m" 1);
+  by(best_tac set_cs 2);
+ by(SELECT_GOAL(safe_tac HOL_cs)1);
+ by(res_inst_tac [("x","k")] exI 1);
+ by(Asm_simp_tac 1);
+by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by(best_tac set_cs 1);
+val lemma = result();
+
+goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
+\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
+br Least_equality 1;
+ bd finite_has_card 1;
+ be exE 1;
+ by(dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
+ be exE 1;
+ by(res_inst_tac
+   [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
+ by(simp_tac
+    (!simpset addsimps [Collect_conv_insert] addcongs [Collect_cong1]) 1);
+ be subst 1;
+ br refl 1;
+br notI 1;
+be exE 1;
+bd lemma 1;
+ ba 1;
+be exE 1;
+be conjE 1;
+by(dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
+by(dtac le_less_trans 1 THEN atac 1);
+by(Asm_full_simp_tac 1);
+be disjE 1;
+by(etac less_asym 1 THEN atac 1);
+by(hyp_subst_tac 1);
+by(Asm_full_simp_tac 1);
+val lemma = result();
+
+goalw Finite.thy [card_def]
+  "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
+be lemma 1;
+ba 1;
+qed "card_insert_disjoint";
+
+val [major] = goal Finite.thy
+  "finite A ==> card(insert x A) = Suc(card(A-{x}))";
+by(case_tac "x:A" 1);
+by(asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
+bd mk_disjoint_insert 1;
+be exE 1;
+by(Asm_simp_tac 1);
+br card_insert_disjoint 1;
+br (major RSN (2,finite_subset)) 1;
+by(fast_tac set_cs 1);
+by(fast_tac HOL_cs 1);
+by(asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
+qed "card_insert";
+Addsimps [card_insert];
+
+
+goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
+be finite_induct 1;
+by(Simp_tac 1);
+by(strip_tac 1);
+by(case_tac "x:B" 1);
+ bd mk_disjoint_insert 1;
+ by(SELECT_GOAL(safe_tac HOL_cs)1);
+ by(rotate_tac ~1 1);
+ by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
+by(rotate_tac ~1 1);
+by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
+qed_spec_mp "card_mono";
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Finite.thy	Mon Mar 04 14:37:33 1996 +0100
@@ -1,12 +1,13 @@
 (*  Title:      HOL/Finite.thy
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
+    Author:     Lawrence C Paulson & Tobias Nipkow
+    Copyright   1995  University of Cambridge & TU Muenchen
 
-Finite powerset operator
+Finite sets and their cardinality
 *)
 
-Finite = Lfp +
+Finite = Arith +
+
 consts Fin :: 'a set => 'a set set
 
 inductive "Fin(A)"
@@ -14,4 +15,10 @@
     emptyI  "{} : Fin(A)"
     insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
 
+consts finite :: 'a set => bool
+defs finite_def "finite A == A : Fin(UNIV)"
+
+consts card :: 'a set => nat
+defs card_def "card A == LEAST n. ? f. A = {f i |i. i<n}"
+
 end
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Nat.ML	Mon Mar 04 14:37:33 1996 +0100
@@ -475,3 +475,43 @@
 qed "Suc_le_mono";
 
 Addsimps [le_refl,Suc_le_mono];
+
+
+(** LEAST -- the least number operator **)
+
+val [prem1,prem2] = goalw Nat.thy [Least_def]
+    "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
+by (rtac select_equality 1);
+by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
+by (cut_facts_tac [less_linear] 1);
+by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
+qed "Least_equality";
+
+val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))";
+by (rtac (prem RS rev_mp) 1);
+by (res_inst_tac [("n","k")] less_induct 1);
+by (rtac impI 1);
+by (rtac classical 1);
+by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
+by (assume_tac 1);
+by (assume_tac 2);
+by (fast_tac HOL_cs 1);
+qed "LeastI";
+
+(*Proof is almost identical to the one above!*)
+val [prem] = goal Nat.thy "P(k) ==> (LEAST x.P(x)) <= k";
+by (rtac (prem RS rev_mp) 1);
+by (res_inst_tac [("n","k")] less_induct 1);
+by (rtac impI 1);
+by (rtac classical 1);
+by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
+by (assume_tac 1);
+by (rtac le_refl 2);
+by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
+qed "Least_le";
+
+val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)";
+by (rtac notI 1);
+by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
+by (rtac prem 1);
+qed "not_less_Least";
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 04 14:37:33 1996 +0100
@@ -43,11 +43,13 @@
 (* abstract constants and syntax *)
 
 consts
-  "0"           :: nat                ("0")
-  Suc           :: nat => nat
-  nat_case      :: ['a, nat => 'a, nat] => 'a
-  pred_nat      :: "(nat * nat) set"
-  nat_rec       :: [nat, 'a, [nat, 'a] => 'a] => 'a
+  "0"       :: nat                ("0")
+  Suc       :: nat => nat
+  nat_case  :: ['a, nat => 'a, nat] => 'a
+  pred_nat  :: "(nat * nat) set"
+  nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
+
+  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
 
 translations
   "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
@@ -61,9 +63,13 @@
                                         & (!x. n=Suc(x) --> z=f(x))"
   pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
 
-  less_def "m<n == (m,n):trancl(pred_nat)"
+  less_def      "m<n == (m,n):trancl(pred_nat)"
+
+  le_def        "m<=(n::nat) == ~(n<m)"
 
-  le_def   "m<=(n::nat) == ~(n<m)"
+  nat_rec_def   "nat_rec n c d ==
+		 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
+  (*least number operator*)
+  Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
 
-nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
 end
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Set.ML	Mon Mar 04 14:37:33 1996 +0100
@@ -257,7 +257,6 @@
 qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
  (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
 
-
 (*** The empty set -- {} ***)
 
 qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
@@ -320,6 +319,13 @@
 by (rtac singletonI 1);
 qed "singleton_inject";
 
+
+(*** UNIV - The universal set ***)
+
+qed_goal "subset_UNIV" Set.thy "A <= UNIV"
+  (fn _ => [rtac subsetI 1, rtac ComplI 1, etac emptyE 1]);
+
+
 (*** Unions of families -- UNION x:A. B(x) is Union(B``A)  ***)
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Set.thy	Mon Mar 04 14:37:33 1996 +0100
@@ -37,6 +37,8 @@
 
 syntax
 
+  UNIV         :: 'a set
+
   "~:"          :: ['a, 'a set] => bool             (infixl 50)
 
   "@Finset"     :: args => 'a set                   ("{(_)}")
@@ -57,6 +59,7 @@
   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
 
 translations
+  "UNIV"        == "Compl {}"
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Univ.ML	Mon Mar 04 14:37:33 1996 +0100
@@ -8,47 +8,6 @@
 
 open Univ;
 
-(** LEAST -- the least number operator **)
-
-
-val [prem1,prem2] = goalw Univ.thy [Least_def]
-    "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
-by (rtac select_equality 1);
-by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
-by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
-qed "Least_equality";
-
-val [prem] = goal Univ.thy "P(k) ==> P(LEAST x.P(x))";
-by (rtac (prem RS rev_mp) 1);
-by (res_inst_tac [("n","k")] less_induct 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
-by (assume_tac 1);
-by (assume_tac 2);
-by (fast_tac HOL_cs 1);
-qed "LeastI";
-
-(*Proof is almost identical to the one above!*)
-val [prem] = goal Univ.thy "P(k) ==> (LEAST x.P(x)) <= k";
-by (rtac (prem RS rev_mp) 1);
-by (res_inst_tac [("n","k")] less_induct 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
-by (assume_tac 1);
-by (rtac le_refl 2);
-by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
-qed "Least_le";
-
-val [prem] = goal Univ.thy "k < (LEAST x.P(x)) ==> ~P(k)";
-by (rtac notI 1);
-by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
-by (rtac prem 1);
-qed "not_less_Least";
-
-
 (** apfst -- can be used in similar type definitions **)
 
 goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Univ.thy	Mon Mar 04 14:37:33 1996 +0100
@@ -22,8 +22,6 @@
   'a item = 'a node set
 
 consts
-  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
-
   apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
   Push      :: [nat, nat=>nat] => (nat=>nat)
 
@@ -52,9 +50,6 @@
 
 defs
 
-  (*least number operator*)
-  Least_def      "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
-
   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
   (*crude "lists" of nats -- needed for the constructions*)
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/equalities.ML	Mon Mar 04 14:37:33 1996 +0100
@@ -10,47 +10,81 @@
 
 val eq_cs = set_cs addSIs [equalityI];
 
+goal Set.thy "{x.False} = {}";
+by(fast_tac eq_cs 1);
+qed "Collect_False_empty";
+Addsimps [Collect_False_empty];
+
+goal Set.thy "(A <= {}) = (A = {})";
+by(fast_tac eq_cs 1);
+qed "subset_empty";
+Addsimps [subset_empty];
+
 (** The membership relation, : **)
 
 goal Set.thy "x ~: {}";
 by(fast_tac set_cs 1);
 qed "in_empty";
+Addsimps[in_empty];
 
 goal Set.thy "x : insert y A = (x=y | x:A)";
 by(fast_tac set_cs 1);
 qed "in_insert";
+Addsimps[in_insert];
 
 (** insert **)
 
+(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
+goal Set.thy "insert a A = {a} Un A";
+by(fast_tac eq_cs 1);
+qed "insert_is_Un";
+
 goal Set.thy "insert a A ~= {}";
 by (fast_tac (set_cs addEs [equalityCE]) 1);
 qed"insert_not_empty";
+Addsimps[insert_not_empty];
 
 bind_thm("empty_not_insert",insert_not_empty RS not_sym);
+Addsimps[empty_not_insert];
 
 goal Set.thy "!!a. a:A ==> insert a A = A";
 by (fast_tac eq_cs 1);
 qed "insert_absorb";
 
+goal Set.thy "insert x (insert x A) = insert x A";
+by(fast_tac eq_cs 1);
+qed "insert_absorb2";
+Addsimps [insert_absorb2];
+
 goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
 by (fast_tac set_cs 1);
 qed "insert_subset";
+Addsimps[insert_subset];
+
+(* use new B rather than (A-{a}) to avoid infinite unfolding *)
+goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
+by(res_inst_tac [("x","A-{a}")] exI 1);
+by(fast_tac eq_cs 1);
+qed "mk_disjoint_insert";
 
 (** Image **)
 
 goal Set.thy "f``{} = {}";
 by (fast_tac eq_cs 1);
 qed "image_empty";
+Addsimps[image_empty];
 
 goal Set.thy "f``insert a B = insert (f a) (f``B)";
 by (fast_tac eq_cs 1);
 qed "image_insert";
+Addsimps[image_insert];
 
 (** Binary Intersection **)
 
 goal Set.thy "A Int A = A";
 by (fast_tac eq_cs 1);
 qed "Int_absorb";
+Addsimps[Int_absorb];
 
 goal Set.thy "A Int B  =  B Int A";
 by (fast_tac eq_cs 1);
@@ -63,10 +97,22 @@
 goal Set.thy "{} Int B = {}";
 by (fast_tac eq_cs 1);
 qed "Int_empty_left";
+Addsimps[Int_empty_left];
 
 goal Set.thy "A Int {} = {}";
 by (fast_tac eq_cs 1);
 qed "Int_empty_right";
+Addsimps[Int_empty_right];
+
+goal Set.thy "UNIV Int B = B";
+by (fast_tac eq_cs 1);
+qed "Int_UNIV_left";
+Addsimps[Int_UNIV_left];
+
+goal Set.thy "A Int UNIV = A";
+by (fast_tac eq_cs 1);
+qed "Int_UNIV_right";
+Addsimps[Int_UNIV_right];
 
 goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
 by (fast_tac eq_cs 1);
@@ -76,11 +122,17 @@
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "subset_Int_eq";
 
+goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
+by (fast_tac (eq_cs addEs [equalityCE]) 1);
+qed "Int_UNIV";
+Addsimps[Int_UNIV];
+
 (** Binary Union **)
 
 goal Set.thy "A Un A = A";
 by (fast_tac eq_cs 1);
 qed "Un_absorb";
+Addsimps[Un_absorb];
 
 goal Set.thy "A Un B  =  B Un A";
 by (fast_tac eq_cs 1);
@@ -93,10 +145,22 @@
 goal Set.thy "{} Un B = B";
 by(fast_tac eq_cs 1);
 qed "Un_empty_left";
+Addsimps[Un_empty_left];
 
 goal Set.thy "A Un {} = A";
 by(fast_tac eq_cs 1);
 qed "Un_empty_right";
+Addsimps[Un_empty_right];
+
+goal Set.thy "UNIV Un B = UNIV";
+by(fast_tac eq_cs 1);
+qed "Un_UNIV_left";
+Addsimps[Un_UNIV_left];
+
+goal Set.thy "A Un UNIV = UNIV";
+by(fast_tac eq_cs 1);
+qed "Un_UNIV_right";
+Addsimps[Un_UNIV_right];
 
 goal Set.thy "insert a B Un C = insert a (B Un C)";
 by(fast_tac eq_cs 1);
@@ -122,20 +186,23 @@
 goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
 by (fast_tac (eq_cs addEs [equalityCE]) 1);
 qed "Un_empty";
+Addsimps[Un_empty];
 
 (** Simple properties of Compl -- complement of a set **)
 
 goal Set.thy "A Int Compl(A) = {}";
 by (fast_tac eq_cs 1);
 qed "Compl_disjoint";
+Addsimps[Compl_disjoint];
 
-goal Set.thy "A Un Compl(A) = {x.True}";
+goal Set.thy "A Un Compl(A) = UNIV";
 by (fast_tac eq_cs 1);
 qed "Compl_partition";
 
 goal Set.thy "Compl(Compl(A)) = A";
 by (fast_tac eq_cs 1);
 qed "double_complement";
+Addsimps[double_complement];
 
 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
 by (fast_tac eq_cs 1);
@@ -165,14 +232,22 @@
 goal Set.thy "Union({}) = {}";
 by (fast_tac eq_cs 1);
 qed "Union_empty";
+Addsimps[Union_empty];
+
+goal Set.thy "Union(UNIV) = UNIV";
+by (fast_tac eq_cs 1);
+qed "Union_UNIV";
+Addsimps[Union_UNIV];
 
 goal Set.thy "Union(insert a B) = a Un Union(B)";
 by (fast_tac eq_cs 1);
 qed "Union_insert";
+Addsimps[Union_insert];
 
 goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
 by (fast_tac eq_cs 1);
 qed "Union_Un_distrib";
+Addsimps[Union_Un_distrib];
 
 goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
 by (fast_tac set_cs 1);
@@ -183,6 +258,28 @@
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
+goal Set.thy "Inter({}) = UNIV";
+by (fast_tac eq_cs 1);
+qed "Inter_empty";
+Addsimps[Inter_empty];
+
+goal Set.thy "Inter(UNIV) = {}";
+by (fast_tac eq_cs 1);
+qed "Inter_UNIV";
+Addsimps[Inter_UNIV];
+
+goal Set.thy "Inter(insert a B) = a Int Inter(B)";
+by (fast_tac eq_cs 1);
+qed "Inter_insert";
+Addsimps[Inter_insert];
+
+(* Why does fast_tac fail???
+goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)";
+by (fast_tac eq_cs 1);
+qed "Inter_Int_distrib";
+Addsimps[Inter_Int_distrib];
+*)
+
 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
 by (best_tac eq_cs 1);
 qed "Inter_Un_distrib";
@@ -194,10 +291,32 @@
 goal Set.thy "(UN x:{}. B x) = {}";
 by (fast_tac eq_cs 1);
 qed "UN_empty";
+Addsimps[UN_empty];
+
+goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
+by (fast_tac eq_cs 1);
+qed "UN_UNIV";
+Addsimps[UN_UNIV];
+
+goal Set.thy "(INT x:{}. B x) = UNIV";
+by (fast_tac eq_cs 1);
+qed "INT_empty";
+Addsimps[INT_empty];
+
+goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
+by (fast_tac eq_cs 1);
+qed "INT_UNIV";
+Addsimps[INT_UNIV];
 
 goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
 by (fast_tac eq_cs 1);
 qed "UN_insert";
+Addsimps[UN_insert];
+
+goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
+by (fast_tac eq_cs 1);
+qed "INT_insert";
+Addsimps[INT_insert];
 
 goal Set.thy "Union(range(f)) = (UN x.f(x))";
 by (fast_tac eq_cs 1);
@@ -226,10 +345,12 @@
 goal Set.thy "(UN x.B) = B";
 by (fast_tac eq_cs 1);
 qed "UN1_constant";
+Addsimps[UN1_constant];
 
 goal Set.thy "(INT x.B) = B";
 by (fast_tac eq_cs 1);
 qed "INT1_constant";
+Addsimps[INT1_constant];
 
 goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
 by (fast_tac eq_cs 1);
@@ -294,14 +415,27 @@
 goal Set.thy "A-A = {}";
 by (fast_tac eq_cs 1);
 qed "Diff_cancel";
+Addsimps[Diff_cancel];
 
 goal Set.thy "{}-A = {}";
 by (fast_tac eq_cs 1);
 qed "empty_Diff";
+Addsimps[empty_Diff];
 
 goal Set.thy "A-{} = A";
 by (fast_tac eq_cs 1);
 qed "Diff_empty";
+Addsimps[Diff_empty];
+
+goal Set.thy "A-UNIV = {}";
+by (fast_tac eq_cs 1);
+qed "Diff_UNIV";
+Addsimps[Diff_UNIV];
+
+goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
+by(fast_tac eq_cs 1);
+qed "Diff_insert0";
+Addsimps [Diff_insert0];
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
 goal Set.thy "A - insert a B = A - B - {a}";
@@ -313,6 +447,16 @@
 by (fast_tac eq_cs 1);
 qed "Diff_insert2";
 
+goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
+by(simp_tac (!simpset setloop split_tac[expand_if]) 1);
+by(fast_tac eq_cs 1);
+qed "insert_Diff_if";
+
+goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
+by(fast_tac eq_cs 1);
+qed "insert_Diff1";
+Addsimps [insert_Diff1];
+
 val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
 by (fast_tac (eq_cs addSIs prems) 1);
 qed "insert_Diff";
@@ -320,6 +464,7 @@
 goal Set.thy "A Int (B-A) = {}";
 by (fast_tac eq_cs 1);
 qed "Diff_disjoint";
+Addsimps[Diff_disjoint];
 
 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
 by (fast_tac eq_cs 1);
@@ -337,13 +482,20 @@
 by (fast_tac eq_cs 1);
 qed "Diff_Int";
 
-Addsimps
-  [in_empty,in_insert,insert_subset,
-   insert_not_empty,empty_not_insert,
-   Int_absorb,Int_empty_left,Int_empty_right,
-   Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
-   UN_empty, UN_insert,
-   UN1_constant,image_empty,
-   Compl_disjoint,double_complement,
-   Union_empty,Union_insert,empty_subsetI,subset_refl,
-   Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint];
+(* Congruence rule for set comprehension *)
+val prems = goal Set.thy
+  "[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \
+\  {f x |x. P x} = {g x|x. Q x}";
+by(simp_tac (!simpset addsimps prems) 1);
+br set_ext 1;
+br iffI 1;
+by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1);
+be CollectE 1;
+be exE 1;
+by(Asm_simp_tac 1);
+be conjE 1;
+by(rtac exI 1 THEN rtac conjI 1 THEN atac 2);
+by(asm_simp_tac (!simpset addsimps prems) 1);
+qed "Collect_cong1";
+
+Addsimps[subset_UNIV, empty_subsetI, subset_refl];
diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/subset.ML
--- a/src/HOL/subset.ML	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/subset.ML	Mon Mar 04 14:37:33 1996 +0100
@@ -12,6 +12,10 @@
 qed_goal "subset_insertI" Set.thy "B <= insert a B"
  (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
 
+goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
+by(fast_tac set_cs 1);
+qed "subset_insert";
+
 (*** Big Union -- least upper bound of a set  ***)
 
 val prems = goal Set.thy