Added a constant UNIV == {x.True}
authornipkow
Mon Mar 04 14:37:33 1996 +0100 (1996-03-04)
changeset 1531e5eb247ad13c
parent 1530 63fed88fe8e6
child 1532 769a4517ad7b
Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
Added cardinality to Finite.
src/HOL/Finite.ML
src/HOL/Finite.thy
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/Univ.ML
src/HOL/Univ.thy
src/HOL/equalities.ML
src/HOL/subset.ML
     1.1 --- a/src/HOL/Finite.ML	Mon Mar 04 12:28:48 1996 +0100
     1.2 +++ b/src/HOL/Finite.ML	Mon Mar 04 14:37:33 1996 +0100
     1.3 @@ -1,13 +1,15 @@
     1.4  (*  Title:      HOL/Finite.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1994  University of Cambridge
     1.8 +    Author:     Lawrence C Paulson & Tobias Nipkow
     1.9 +    Copyright   1995  University of Cambridge & TU Muenchen
    1.10  
    1.11 -Finite powerset operator
    1.12 +Finite sets and their cardinality
    1.13  *)
    1.14  
    1.15  open Finite;
    1.16  
    1.17 +(*** Fin ***)
    1.18 +
    1.19  goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    1.20  by (rtac lfp_mono 1);
    1.21  by (REPEAT (ares_tac basic_monos 1));
    1.22 @@ -31,8 +33,6 @@
    1.23  by (REPEAT (ares_tac prems 1));
    1.24  qed "Fin_induct";
    1.25  
    1.26 -(** Simplification for Fin **)
    1.27 -
    1.28  Addsimps Fin.intrs;
    1.29  
    1.30  (*The union of two finite sets is finite*)
    1.31 @@ -54,6 +54,19 @@
    1.32  by (ALLGOALS Asm_simp_tac);
    1.33  qed "Fin_subset";
    1.34  
    1.35 +goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
    1.36 +by(fast_tac (set_cs addIs [Fin_UnI] addDs
    1.37 +                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    1.38 +qed "subset_Fin";
    1.39 +Addsimps[subset_Fin];
    1.40 +
    1.41 +goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
    1.42 +by(stac insert_is_Un 1);
    1.43 +by(Simp_tac 1);
    1.44 +by(fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
    1.45 +qed "insert_Fin";
    1.46 +Addsimps[insert_Fin];
    1.47 +
    1.48  (*The image of a finite set is finite*)
    1.49  val major::_ = goal Finite.thy
    1.50      "F: Fin(A) ==> h``F : Fin(h``A)";
    1.51 @@ -72,7 +85,7 @@
    1.52  by (rtac (Diff_insert RS ssubst) 2);
    1.53  by (ALLGOALS (asm_simp_tac
    1.54                  (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
    1.55 -qed "Fin_empty_induct_lemma";
    1.56 +val lemma = result();
    1.57  
    1.58  val prems = goal Finite.thy 
    1.59      "[| b: Fin(A);                                              \
    1.60 @@ -80,6 +93,227 @@
    1.61  \       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    1.62  \    |] ==> P({})";
    1.63  by (rtac (Diff_cancel RS subst) 1);
    1.64 -by (rtac (Fin_empty_induct_lemma RS mp) 1);
    1.65 +by (rtac (lemma RS mp) 1);
    1.66  by (REPEAT (ares_tac (subset_refl::prems) 1));
    1.67  qed "Fin_empty_induct";
    1.68 +
    1.69 +
    1.70 +(*** finite ***)
    1.71 +
    1.72 +val major::prems = goalw Finite.thy [finite_def]
    1.73 +    "[| finite F;  P({}); \
    1.74 +\       !!F x. [| finite F;  x~:F;  P(F) |] ==> P(insert x F) \
    1.75 +\    |] ==> P(F)";
    1.76 +by (rtac (major RS Fin_induct) 1);
    1.77 +by (REPEAT (ares_tac prems 1));
    1.78 +qed "finite_induct";
    1.79 +
    1.80 +
    1.81 +goalw Finite.thy [finite_def] "finite {}";
    1.82 +by(Simp_tac 1);
    1.83 +qed "finite_emptyI";
    1.84 +Addsimps [finite_emptyI];
    1.85 +
    1.86 +goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
    1.87 +by(Asm_simp_tac 1);
    1.88 +qed "finite_insertI";
    1.89 +
    1.90 +(*The union of two finite sets is finite*)
    1.91 +goalw Finite.thy [finite_def]
    1.92 +    "!!F. [| finite F;  finite G |] ==> finite(F Un G)";
    1.93 +by(Asm_simp_tac 1);
    1.94 +qed "finite_UnI";
    1.95 +
    1.96 +goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
    1.97 +be Fin_subset 1;
    1.98 +ba 1;
    1.99 +qed "finite_subset";
   1.100 +
   1.101 +goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
   1.102 +by(Simp_tac 1);
   1.103 +qed "subset_finite";
   1.104 +Addsimps[subset_finite];
   1.105 +
   1.106 +goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
   1.107 +by(Simp_tac 1);
   1.108 +qed "insert_finite";
   1.109 +Addsimps[insert_finite];
   1.110 +
   1.111 +goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
   1.112 +be finite_induct 1;
   1.113 +by(Simp_tac 1);
   1.114 +by(asm_simp_tac (!simpset addsimps [insert_Diff_if]
   1.115 +                          setloop split_tac[expand_if]) 1);
   1.116 +qed "finite_Diff";
   1.117 +Addsimps [finite_Diff];
   1.118 +
   1.119 +(*The image of a finite set is finite*)
   1.120 +goal Finite.thy "!!F. finite F ==> finite(h``F)";
   1.121 +be finite_induct 1;
   1.122 +by(ALLGOALS Asm_simp_tac);
   1.123 +qed "finite_imageI";
   1.124 +
   1.125 +val major::prems = goalw Finite.thy [finite_def]
   1.126 +    "[| finite A;                                       \
   1.127 +\       P(A);                                           \
   1.128 +\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
   1.129 +\    |] ==> P({})";
   1.130 +by (rtac (major RS Fin_empty_induct) 1);
   1.131 +by (REPEAT (ares_tac (subset_refl::prems) 1));
   1.132 +qed "finite_empty_induct";
   1.133 +
   1.134 +
   1.135 +(*** Cardinality ***)
   1.136 +
   1.137 +goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
   1.138 +by(fast_tac eq_cs 1);
   1.139 +val Collect_conv_insert = result();
   1.140 +
   1.141 +goalw Finite.thy [card_def] "card {} = 0";
   1.142 +br Least_equality 1;
   1.143 +by(ALLGOALS Asm_full_simp_tac);
   1.144 +qed "card_empty";
   1.145 +Addsimps [card_empty];
   1.146 +
   1.147 +(*Addsimps [Collect_conv_insert];*)
   1.148 +
   1.149 +val [major] = goal Finite.thy
   1.150 +  "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
   1.151 +br (major RS finite_induct) 1;
   1.152 + by(res_inst_tac [("x","0")] exI 1);
   1.153 + by(Simp_tac 1);
   1.154 +be exE 1;
   1.155 +be exE 1;
   1.156 +by(hyp_subst_tac 1);
   1.157 +by(res_inst_tac [("x","Suc n")] exI 1);
   1.158 +by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
   1.159 +by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]
   1.160 +                          addcongs [Collect_cong1]) 1);
   1.161 +qed "finite_has_card";
   1.162 +
   1.163 +goal Finite.thy
   1.164 +  "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
   1.165 +\  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
   1.166 +by(res_inst_tac [("n","n")] natE 1);
   1.167 + by(hyp_subst_tac 1);
   1.168 + by(Asm_full_simp_tac 1);
   1.169 +by(rename_tac "m" 1);
   1.170 +by(hyp_subst_tac 1);
   1.171 +by(case_tac "? a. a:A" 1);
   1.172 + by(res_inst_tac [("x","0")] exI 2);
   1.173 + by(Simp_tac 2);
   1.174 + by(fast_tac eq_cs 2);
   1.175 +be exE 1;
   1.176 +by(Simp_tac 1);
   1.177 +br exI 1;
   1.178 +br conjI 1;
   1.179 + br disjI2 1;
   1.180 + br refl 1;
   1.181 +be equalityE 1;
   1.182 +by(asm_full_simp_tac
   1.183 +     (!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
   1.184 +by(SELECT_GOAL(safe_tac eq_cs)1);
   1.185 +  by(Asm_full_simp_tac 1);
   1.186 +  by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   1.187 +  by(SELECT_GOAL(safe_tac eq_cs)1);
   1.188 +   by(subgoal_tac "x ~= f m" 1);
   1.189 +    by(fast_tac set_cs 2);
   1.190 +   by(subgoal_tac "? k. f k = x & k<m" 1);
   1.191 +    by(best_tac set_cs 2);
   1.192 +   by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.193 +   by(res_inst_tac [("x","k")] exI 1);
   1.194 +   by(Asm_simp_tac 1);
   1.195 +  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.196 +  by(best_tac set_cs 1);
   1.197 + bd sym 1;
   1.198 + by(rotate_tac ~1 1);
   1.199 + by(Asm_full_simp_tac 1);
   1.200 + by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   1.201 + by(SELECT_GOAL(safe_tac eq_cs)1);
   1.202 +  by(subgoal_tac "x ~= f m" 1);
   1.203 +   by(fast_tac set_cs 2);
   1.204 +  by(subgoal_tac "? k. f k = x & k<m" 1);
   1.205 +   by(best_tac set_cs 2);
   1.206 +  by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.207 +  by(res_inst_tac [("x","k")] exI 1);
   1.208 +  by(Asm_simp_tac 1);
   1.209 + by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.210 + by(best_tac set_cs 1);
   1.211 +by(res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   1.212 +by(SELECT_GOAL(safe_tac eq_cs)1);
   1.213 + by(subgoal_tac "x ~= f i" 1);
   1.214 +  by(fast_tac set_cs 2);
   1.215 + by(case_tac "x = f m" 1);
   1.216 +  by(res_inst_tac [("x","i")] exI 1);
   1.217 +  by(Asm_simp_tac 1);
   1.218 + by(subgoal_tac "? k. f k = x & k<m" 1);
   1.219 +  by(best_tac set_cs 2);
   1.220 + by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.221 + by(res_inst_tac [("x","k")] exI 1);
   1.222 + by(Asm_simp_tac 1);
   1.223 +by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.224 +by(best_tac set_cs 1);
   1.225 +val lemma = result();
   1.226 +
   1.227 +goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
   1.228 +\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
   1.229 +br Least_equality 1;
   1.230 + bd finite_has_card 1;
   1.231 + be exE 1;
   1.232 + by(dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
   1.233 + be exE 1;
   1.234 + by(res_inst_tac
   1.235 +   [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
   1.236 + by(simp_tac
   1.237 +    (!simpset addsimps [Collect_conv_insert] addcongs [Collect_cong1]) 1);
   1.238 + be subst 1;
   1.239 + br refl 1;
   1.240 +br notI 1;
   1.241 +be exE 1;
   1.242 +bd lemma 1;
   1.243 + ba 1;
   1.244 +be exE 1;
   1.245 +be conjE 1;
   1.246 +by(dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
   1.247 +by(dtac le_less_trans 1 THEN atac 1);
   1.248 +by(Asm_full_simp_tac 1);
   1.249 +be disjE 1;
   1.250 +by(etac less_asym 1 THEN atac 1);
   1.251 +by(hyp_subst_tac 1);
   1.252 +by(Asm_full_simp_tac 1);
   1.253 +val lemma = result();
   1.254 +
   1.255 +goalw Finite.thy [card_def]
   1.256 +  "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
   1.257 +be lemma 1;
   1.258 +ba 1;
   1.259 +qed "card_insert_disjoint";
   1.260 +
   1.261 +val [major] = goal Finite.thy
   1.262 +  "finite A ==> card(insert x A) = Suc(card(A-{x}))";
   1.263 +by(case_tac "x:A" 1);
   1.264 +by(asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
   1.265 +bd mk_disjoint_insert 1;
   1.266 +be exE 1;
   1.267 +by(Asm_simp_tac 1);
   1.268 +br card_insert_disjoint 1;
   1.269 +br (major RSN (2,finite_subset)) 1;
   1.270 +by(fast_tac set_cs 1);
   1.271 +by(fast_tac HOL_cs 1);
   1.272 +by(asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
   1.273 +qed "card_insert";
   1.274 +Addsimps [card_insert];
   1.275 +
   1.276 +
   1.277 +goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
   1.278 +be finite_induct 1;
   1.279 +by(Simp_tac 1);
   1.280 +by(strip_tac 1);
   1.281 +by(case_tac "x:B" 1);
   1.282 + bd mk_disjoint_insert 1;
   1.283 + by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.284 + by(rotate_tac ~1 1);
   1.285 + by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.286 +by(rotate_tac ~1 1);
   1.287 +by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.288 +qed_spec_mp "card_mono";
     2.1 --- a/src/HOL/Finite.thy	Mon Mar 04 12:28:48 1996 +0100
     2.2 +++ b/src/HOL/Finite.thy	Mon Mar 04 14:37:33 1996 +0100
     2.3 @@ -1,12 +1,13 @@
     2.4  (*  Title:      HOL/Finite.thy
     2.5      ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1994  University of Cambridge
     2.8 +    Author:     Lawrence C Paulson & Tobias Nipkow
     2.9 +    Copyright   1995  University of Cambridge & TU Muenchen
    2.10  
    2.11 -Finite powerset operator
    2.12 +Finite sets and their cardinality
    2.13  *)
    2.14  
    2.15 -Finite = Lfp +
    2.16 +Finite = Arith +
    2.17 +
    2.18  consts Fin :: 'a set => 'a set set
    2.19  
    2.20  inductive "Fin(A)"
    2.21 @@ -14,4 +15,10 @@
    2.22      emptyI  "{} : Fin(A)"
    2.23      insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
    2.24  
    2.25 +consts finite :: 'a set => bool
    2.26 +defs finite_def "finite A == A : Fin(UNIV)"
    2.27 +
    2.28 +consts card :: 'a set => nat
    2.29 +defs card_def "card A == LEAST n. ? f. A = {f i |i. i<n}"
    2.30 +
    2.31  end
     3.1 --- a/src/HOL/Nat.ML	Mon Mar 04 12:28:48 1996 +0100
     3.2 +++ b/src/HOL/Nat.ML	Mon Mar 04 14:37:33 1996 +0100
     3.3 @@ -475,3 +475,43 @@
     3.4  qed "Suc_le_mono";
     3.5  
     3.6  Addsimps [le_refl,Suc_le_mono];
     3.7 +
     3.8 +
     3.9 +(** LEAST -- the least number operator **)
    3.10 +
    3.11 +val [prem1,prem2] = goalw Nat.thy [Least_def]
    3.12 +    "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
    3.13 +by (rtac select_equality 1);
    3.14 +by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
    3.15 +by (cut_facts_tac [less_linear] 1);
    3.16 +by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
    3.17 +qed "Least_equality";
    3.18 +
    3.19 +val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))";
    3.20 +by (rtac (prem RS rev_mp) 1);
    3.21 +by (res_inst_tac [("n","k")] less_induct 1);
    3.22 +by (rtac impI 1);
    3.23 +by (rtac classical 1);
    3.24 +by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
    3.25 +by (assume_tac 1);
    3.26 +by (assume_tac 2);
    3.27 +by (fast_tac HOL_cs 1);
    3.28 +qed "LeastI";
    3.29 +
    3.30 +(*Proof is almost identical to the one above!*)
    3.31 +val [prem] = goal Nat.thy "P(k) ==> (LEAST x.P(x)) <= k";
    3.32 +by (rtac (prem RS rev_mp) 1);
    3.33 +by (res_inst_tac [("n","k")] less_induct 1);
    3.34 +by (rtac impI 1);
    3.35 +by (rtac classical 1);
    3.36 +by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
    3.37 +by (assume_tac 1);
    3.38 +by (rtac le_refl 2);
    3.39 +by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
    3.40 +qed "Least_le";
    3.41 +
    3.42 +val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)";
    3.43 +by (rtac notI 1);
    3.44 +by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
    3.45 +by (rtac prem 1);
    3.46 +qed "not_less_Least";
     4.1 --- a/src/HOL/Nat.thy	Mon Mar 04 12:28:48 1996 +0100
     4.2 +++ b/src/HOL/Nat.thy	Mon Mar 04 14:37:33 1996 +0100
     4.3 @@ -43,11 +43,13 @@
     4.4  (* abstract constants and syntax *)
     4.5  
     4.6  consts
     4.7 -  "0"           :: nat                ("0")
     4.8 -  Suc           :: nat => nat
     4.9 -  nat_case      :: ['a, nat => 'a, nat] => 'a
    4.10 -  pred_nat      :: "(nat * nat) set"
    4.11 -  nat_rec       :: [nat, 'a, [nat, 'a] => 'a] => 'a
    4.12 +  "0"       :: nat                ("0")
    4.13 +  Suc       :: nat => nat
    4.14 +  nat_case  :: ['a, nat => 'a, nat] => 'a
    4.15 +  pred_nat  :: "(nat * nat) set"
    4.16 +  nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
    4.17 +
    4.18 +  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    4.19  
    4.20  translations
    4.21    "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    4.22 @@ -61,9 +63,13 @@
    4.23                                          & (!x. n=Suc(x) --> z=f(x))"
    4.24    pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    4.25  
    4.26 -  less_def "m<n == (m,n):trancl(pred_nat)"
    4.27 +  less_def      "m<n == (m,n):trancl(pred_nat)"
    4.28 +
    4.29 +  le_def        "m<=(n::nat) == ~(n<m)"
    4.30  
    4.31 -  le_def   "m<=(n::nat) == ~(n<m)"
    4.32 +  nat_rec_def   "nat_rec n c d ==
    4.33 +		 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    4.34 +  (*least number operator*)
    4.35 +  Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    4.36  
    4.37 -nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    4.38  end
     5.1 --- a/src/HOL/Set.ML	Mon Mar 04 12:28:48 1996 +0100
     5.2 +++ b/src/HOL/Set.ML	Mon Mar 04 14:37:33 1996 +0100
     5.3 @@ -257,7 +257,6 @@
     5.4  qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
     5.5   (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
     5.6  
     5.7 -
     5.8  (*** The empty set -- {} ***)
     5.9  
    5.10  qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
    5.11 @@ -320,6 +319,13 @@
    5.12  by (rtac singletonI 1);
    5.13  qed "singleton_inject";
    5.14  
    5.15 +
    5.16 +(*** UNIV - The universal set ***)
    5.17 +
    5.18 +qed_goal "subset_UNIV" Set.thy "A <= UNIV"
    5.19 +  (fn _ => [rtac subsetI 1, rtac ComplI 1, etac emptyE 1]);
    5.20 +
    5.21 +
    5.22  (*** Unions of families -- UNION x:A. B(x) is Union(B``A)  ***)
    5.23  
    5.24  (*The order of the premises presupposes that A is rigid; b may be flexible*)
     6.1 --- a/src/HOL/Set.thy	Mon Mar 04 12:28:48 1996 +0100
     6.2 +++ b/src/HOL/Set.thy	Mon Mar 04 14:37:33 1996 +0100
     6.3 @@ -37,6 +37,8 @@
     6.4  
     6.5  syntax
     6.6  
     6.7 +  UNIV         :: 'a set
     6.8 +
     6.9    "~:"          :: ['a, 'a set] => bool             (infixl 50)
    6.10  
    6.11    "@Finset"     :: args => 'a set                   ("{(_)}")
    6.12 @@ -57,6 +59,7 @@
    6.13    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
    6.14  
    6.15  translations
    6.16 +  "UNIV"        == "Compl {}"
    6.17    "x ~: y"      == "~ (x : y)"
    6.18    "{x, xs}"     == "insert x {xs}"
    6.19    "{x}"         == "insert x {}"
     7.1 --- a/src/HOL/Univ.ML	Mon Mar 04 12:28:48 1996 +0100
     7.2 +++ b/src/HOL/Univ.ML	Mon Mar 04 14:37:33 1996 +0100
     7.3 @@ -8,47 +8,6 @@
     7.4  
     7.5  open Univ;
     7.6  
     7.7 -(** LEAST -- the least number operator **)
     7.8 -
     7.9 -
    7.10 -val [prem1,prem2] = goalw Univ.thy [Least_def]
    7.11 -    "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
    7.12 -by (rtac select_equality 1);
    7.13 -by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
    7.14 -by (cut_facts_tac [less_linear] 1);
    7.15 -by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
    7.16 -qed "Least_equality";
    7.17 -
    7.18 -val [prem] = goal Univ.thy "P(k) ==> P(LEAST x.P(x))";
    7.19 -by (rtac (prem RS rev_mp) 1);
    7.20 -by (res_inst_tac [("n","k")] less_induct 1);
    7.21 -by (rtac impI 1);
    7.22 -by (rtac classical 1);
    7.23 -by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
    7.24 -by (assume_tac 1);
    7.25 -by (assume_tac 2);
    7.26 -by (fast_tac HOL_cs 1);
    7.27 -qed "LeastI";
    7.28 -
    7.29 -(*Proof is almost identical to the one above!*)
    7.30 -val [prem] = goal Univ.thy "P(k) ==> (LEAST x.P(x)) <= k";
    7.31 -by (rtac (prem RS rev_mp) 1);
    7.32 -by (res_inst_tac [("n","k")] less_induct 1);
    7.33 -by (rtac impI 1);
    7.34 -by (rtac classical 1);
    7.35 -by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
    7.36 -by (assume_tac 1);
    7.37 -by (rtac le_refl 2);
    7.38 -by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
    7.39 -qed "Least_le";
    7.40 -
    7.41 -val [prem] = goal Univ.thy "k < (LEAST x.P(x)) ==> ~P(k)";
    7.42 -by (rtac notI 1);
    7.43 -by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
    7.44 -by (rtac prem 1);
    7.45 -qed "not_less_Least";
    7.46 -
    7.47 -
    7.48  (** apfst -- can be used in similar type definitions **)
    7.49  
    7.50  goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";
     8.1 --- a/src/HOL/Univ.thy	Mon Mar 04 12:28:48 1996 +0100
     8.2 +++ b/src/HOL/Univ.thy	Mon Mar 04 14:37:33 1996 +0100
     8.3 @@ -22,8 +22,6 @@
     8.4    'a item = 'a node set
     8.5  
     8.6  consts
     8.7 -  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
     8.8 -
     8.9    apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    8.10    Push      :: [nat, nat=>nat] => (nat=>nat)
    8.11  
    8.12 @@ -52,9 +50,6 @@
    8.13  
    8.14  defs
    8.15  
    8.16 -  (*least number operator*)
    8.17 -  Least_def      "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    8.18 -
    8.19    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    8.20  
    8.21    (*crude "lists" of nats -- needed for the constructions*)
     9.1 --- a/src/HOL/equalities.ML	Mon Mar 04 12:28:48 1996 +0100
     9.2 +++ b/src/HOL/equalities.ML	Mon Mar 04 14:37:33 1996 +0100
     9.3 @@ -10,47 +10,81 @@
     9.4  
     9.5  val eq_cs = set_cs addSIs [equalityI];
     9.6  
     9.7 +goal Set.thy "{x.False} = {}";
     9.8 +by(fast_tac eq_cs 1);
     9.9 +qed "Collect_False_empty";
    9.10 +Addsimps [Collect_False_empty];
    9.11 +
    9.12 +goal Set.thy "(A <= {}) = (A = {})";
    9.13 +by(fast_tac eq_cs 1);
    9.14 +qed "subset_empty";
    9.15 +Addsimps [subset_empty];
    9.16 +
    9.17  (** The membership relation, : **)
    9.18  
    9.19  goal Set.thy "x ~: {}";
    9.20  by(fast_tac set_cs 1);
    9.21  qed "in_empty";
    9.22 +Addsimps[in_empty];
    9.23  
    9.24  goal Set.thy "x : insert y A = (x=y | x:A)";
    9.25  by(fast_tac set_cs 1);
    9.26  qed "in_insert";
    9.27 +Addsimps[in_insert];
    9.28  
    9.29  (** insert **)
    9.30  
    9.31 +(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    9.32 +goal Set.thy "insert a A = {a} Un A";
    9.33 +by(fast_tac eq_cs 1);
    9.34 +qed "insert_is_Un";
    9.35 +
    9.36  goal Set.thy "insert a A ~= {}";
    9.37  by (fast_tac (set_cs addEs [equalityCE]) 1);
    9.38  qed"insert_not_empty";
    9.39 +Addsimps[insert_not_empty];
    9.40  
    9.41  bind_thm("empty_not_insert",insert_not_empty RS not_sym);
    9.42 +Addsimps[empty_not_insert];
    9.43  
    9.44  goal Set.thy "!!a. a:A ==> insert a A = A";
    9.45  by (fast_tac eq_cs 1);
    9.46  qed "insert_absorb";
    9.47  
    9.48 +goal Set.thy "insert x (insert x A) = insert x A";
    9.49 +by(fast_tac eq_cs 1);
    9.50 +qed "insert_absorb2";
    9.51 +Addsimps [insert_absorb2];
    9.52 +
    9.53  goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
    9.54  by (fast_tac set_cs 1);
    9.55  qed "insert_subset";
    9.56 +Addsimps[insert_subset];
    9.57 +
    9.58 +(* use new B rather than (A-{a}) to avoid infinite unfolding *)
    9.59 +goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
    9.60 +by(res_inst_tac [("x","A-{a}")] exI 1);
    9.61 +by(fast_tac eq_cs 1);
    9.62 +qed "mk_disjoint_insert";
    9.63  
    9.64  (** Image **)
    9.65  
    9.66  goal Set.thy "f``{} = {}";
    9.67  by (fast_tac eq_cs 1);
    9.68  qed "image_empty";
    9.69 +Addsimps[image_empty];
    9.70  
    9.71  goal Set.thy "f``insert a B = insert (f a) (f``B)";
    9.72  by (fast_tac eq_cs 1);
    9.73  qed "image_insert";
    9.74 +Addsimps[image_insert];
    9.75  
    9.76  (** Binary Intersection **)
    9.77  
    9.78  goal Set.thy "A Int A = A";
    9.79  by (fast_tac eq_cs 1);
    9.80  qed "Int_absorb";
    9.81 +Addsimps[Int_absorb];
    9.82  
    9.83  goal Set.thy "A Int B  =  B Int A";
    9.84  by (fast_tac eq_cs 1);
    9.85 @@ -63,10 +97,22 @@
    9.86  goal Set.thy "{} Int B = {}";
    9.87  by (fast_tac eq_cs 1);
    9.88  qed "Int_empty_left";
    9.89 +Addsimps[Int_empty_left];
    9.90  
    9.91  goal Set.thy "A Int {} = {}";
    9.92  by (fast_tac eq_cs 1);
    9.93  qed "Int_empty_right";
    9.94 +Addsimps[Int_empty_right];
    9.95 +
    9.96 +goal Set.thy "UNIV Int B = B";
    9.97 +by (fast_tac eq_cs 1);
    9.98 +qed "Int_UNIV_left";
    9.99 +Addsimps[Int_UNIV_left];
   9.100 +
   9.101 +goal Set.thy "A Int UNIV = A";
   9.102 +by (fast_tac eq_cs 1);
   9.103 +qed "Int_UNIV_right";
   9.104 +Addsimps[Int_UNIV_right];
   9.105  
   9.106  goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
   9.107  by (fast_tac eq_cs 1);
   9.108 @@ -76,11 +122,17 @@
   9.109  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   9.110  qed "subset_Int_eq";
   9.111  
   9.112 +goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
   9.113 +by (fast_tac (eq_cs addEs [equalityCE]) 1);
   9.114 +qed "Int_UNIV";
   9.115 +Addsimps[Int_UNIV];
   9.116 +
   9.117  (** Binary Union **)
   9.118  
   9.119  goal Set.thy "A Un A = A";
   9.120  by (fast_tac eq_cs 1);
   9.121  qed "Un_absorb";
   9.122 +Addsimps[Un_absorb];
   9.123  
   9.124  goal Set.thy "A Un B  =  B Un A";
   9.125  by (fast_tac eq_cs 1);
   9.126 @@ -93,10 +145,22 @@
   9.127  goal Set.thy "{} Un B = B";
   9.128  by(fast_tac eq_cs 1);
   9.129  qed "Un_empty_left";
   9.130 +Addsimps[Un_empty_left];
   9.131  
   9.132  goal Set.thy "A Un {} = A";
   9.133  by(fast_tac eq_cs 1);
   9.134  qed "Un_empty_right";
   9.135 +Addsimps[Un_empty_right];
   9.136 +
   9.137 +goal Set.thy "UNIV Un B = UNIV";
   9.138 +by(fast_tac eq_cs 1);
   9.139 +qed "Un_UNIV_left";
   9.140 +Addsimps[Un_UNIV_left];
   9.141 +
   9.142 +goal Set.thy "A Un UNIV = UNIV";
   9.143 +by(fast_tac eq_cs 1);
   9.144 +qed "Un_UNIV_right";
   9.145 +Addsimps[Un_UNIV_right];
   9.146  
   9.147  goal Set.thy "insert a B Un C = insert a (B Un C)";
   9.148  by(fast_tac eq_cs 1);
   9.149 @@ -122,20 +186,23 @@
   9.150  goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
   9.151  by (fast_tac (eq_cs addEs [equalityCE]) 1);
   9.152  qed "Un_empty";
   9.153 +Addsimps[Un_empty];
   9.154  
   9.155  (** Simple properties of Compl -- complement of a set **)
   9.156  
   9.157  goal Set.thy "A Int Compl(A) = {}";
   9.158  by (fast_tac eq_cs 1);
   9.159  qed "Compl_disjoint";
   9.160 +Addsimps[Compl_disjoint];
   9.161  
   9.162 -goal Set.thy "A Un Compl(A) = {x.True}";
   9.163 +goal Set.thy "A Un Compl(A) = UNIV";
   9.164  by (fast_tac eq_cs 1);
   9.165  qed "Compl_partition";
   9.166  
   9.167  goal Set.thy "Compl(Compl(A)) = A";
   9.168  by (fast_tac eq_cs 1);
   9.169  qed "double_complement";
   9.170 +Addsimps[double_complement];
   9.171  
   9.172  goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
   9.173  by (fast_tac eq_cs 1);
   9.174 @@ -165,14 +232,22 @@
   9.175  goal Set.thy "Union({}) = {}";
   9.176  by (fast_tac eq_cs 1);
   9.177  qed "Union_empty";
   9.178 +Addsimps[Union_empty];
   9.179 +
   9.180 +goal Set.thy "Union(UNIV) = UNIV";
   9.181 +by (fast_tac eq_cs 1);
   9.182 +qed "Union_UNIV";
   9.183 +Addsimps[Union_UNIV];
   9.184  
   9.185  goal Set.thy "Union(insert a B) = a Un Union(B)";
   9.186  by (fast_tac eq_cs 1);
   9.187  qed "Union_insert";
   9.188 +Addsimps[Union_insert];
   9.189  
   9.190  goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
   9.191  by (fast_tac eq_cs 1);
   9.192  qed "Union_Un_distrib";
   9.193 +Addsimps[Union_Un_distrib];
   9.194  
   9.195  goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
   9.196  by (fast_tac set_cs 1);
   9.197 @@ -183,6 +258,28 @@
   9.198  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   9.199  qed "Union_disjoint";
   9.200  
   9.201 +goal Set.thy "Inter({}) = UNIV";
   9.202 +by (fast_tac eq_cs 1);
   9.203 +qed "Inter_empty";
   9.204 +Addsimps[Inter_empty];
   9.205 +
   9.206 +goal Set.thy "Inter(UNIV) = {}";
   9.207 +by (fast_tac eq_cs 1);
   9.208 +qed "Inter_UNIV";
   9.209 +Addsimps[Inter_UNIV];
   9.210 +
   9.211 +goal Set.thy "Inter(insert a B) = a Int Inter(B)";
   9.212 +by (fast_tac eq_cs 1);
   9.213 +qed "Inter_insert";
   9.214 +Addsimps[Inter_insert];
   9.215 +
   9.216 +(* Why does fast_tac fail???
   9.217 +goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)";
   9.218 +by (fast_tac eq_cs 1);
   9.219 +qed "Inter_Int_distrib";
   9.220 +Addsimps[Inter_Int_distrib];
   9.221 +*)
   9.222 +
   9.223  goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   9.224  by (best_tac eq_cs 1);
   9.225  qed "Inter_Un_distrib";
   9.226 @@ -194,10 +291,32 @@
   9.227  goal Set.thy "(UN x:{}. B x) = {}";
   9.228  by (fast_tac eq_cs 1);
   9.229  qed "UN_empty";
   9.230 +Addsimps[UN_empty];
   9.231 +
   9.232 +goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
   9.233 +by (fast_tac eq_cs 1);
   9.234 +qed "UN_UNIV";
   9.235 +Addsimps[UN_UNIV];
   9.236 +
   9.237 +goal Set.thy "(INT x:{}. B x) = UNIV";
   9.238 +by (fast_tac eq_cs 1);
   9.239 +qed "INT_empty";
   9.240 +Addsimps[INT_empty];
   9.241 +
   9.242 +goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
   9.243 +by (fast_tac eq_cs 1);
   9.244 +qed "INT_UNIV";
   9.245 +Addsimps[INT_UNIV];
   9.246  
   9.247  goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
   9.248  by (fast_tac eq_cs 1);
   9.249  qed "UN_insert";
   9.250 +Addsimps[UN_insert];
   9.251 +
   9.252 +goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
   9.253 +by (fast_tac eq_cs 1);
   9.254 +qed "INT_insert";
   9.255 +Addsimps[INT_insert];
   9.256  
   9.257  goal Set.thy "Union(range(f)) = (UN x.f(x))";
   9.258  by (fast_tac eq_cs 1);
   9.259 @@ -226,10 +345,12 @@
   9.260  goal Set.thy "(UN x.B) = B";
   9.261  by (fast_tac eq_cs 1);
   9.262  qed "UN1_constant";
   9.263 +Addsimps[UN1_constant];
   9.264  
   9.265  goal Set.thy "(INT x.B) = B";
   9.266  by (fast_tac eq_cs 1);
   9.267  qed "INT1_constant";
   9.268 +Addsimps[INT1_constant];
   9.269  
   9.270  goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
   9.271  by (fast_tac eq_cs 1);
   9.272 @@ -294,14 +415,27 @@
   9.273  goal Set.thy "A-A = {}";
   9.274  by (fast_tac eq_cs 1);
   9.275  qed "Diff_cancel";
   9.276 +Addsimps[Diff_cancel];
   9.277  
   9.278  goal Set.thy "{}-A = {}";
   9.279  by (fast_tac eq_cs 1);
   9.280  qed "empty_Diff";
   9.281 +Addsimps[empty_Diff];
   9.282  
   9.283  goal Set.thy "A-{} = A";
   9.284  by (fast_tac eq_cs 1);
   9.285  qed "Diff_empty";
   9.286 +Addsimps[Diff_empty];
   9.287 +
   9.288 +goal Set.thy "A-UNIV = {}";
   9.289 +by (fast_tac eq_cs 1);
   9.290 +qed "Diff_UNIV";
   9.291 +Addsimps[Diff_UNIV];
   9.292 +
   9.293 +goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
   9.294 +by(fast_tac eq_cs 1);
   9.295 +qed "Diff_insert0";
   9.296 +Addsimps [Diff_insert0];
   9.297  
   9.298  (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   9.299  goal Set.thy "A - insert a B = A - B - {a}";
   9.300 @@ -313,6 +447,16 @@
   9.301  by (fast_tac eq_cs 1);
   9.302  qed "Diff_insert2";
   9.303  
   9.304 +goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   9.305 +by(simp_tac (!simpset setloop split_tac[expand_if]) 1);
   9.306 +by(fast_tac eq_cs 1);
   9.307 +qed "insert_Diff_if";
   9.308 +
   9.309 +goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
   9.310 +by(fast_tac eq_cs 1);
   9.311 +qed "insert_Diff1";
   9.312 +Addsimps [insert_Diff1];
   9.313 +
   9.314  val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
   9.315  by (fast_tac (eq_cs addSIs prems) 1);
   9.316  qed "insert_Diff";
   9.317 @@ -320,6 +464,7 @@
   9.318  goal Set.thy "A Int (B-A) = {}";
   9.319  by (fast_tac eq_cs 1);
   9.320  qed "Diff_disjoint";
   9.321 +Addsimps[Diff_disjoint];
   9.322  
   9.323  goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
   9.324  by (fast_tac eq_cs 1);
   9.325 @@ -337,13 +482,20 @@
   9.326  by (fast_tac eq_cs 1);
   9.327  qed "Diff_Int";
   9.328  
   9.329 -Addsimps
   9.330 -  [in_empty,in_insert,insert_subset,
   9.331 -   insert_not_empty,empty_not_insert,
   9.332 -   Int_absorb,Int_empty_left,Int_empty_right,
   9.333 -   Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
   9.334 -   UN_empty, UN_insert,
   9.335 -   UN1_constant,image_empty,
   9.336 -   Compl_disjoint,double_complement,
   9.337 -   Union_empty,Union_insert,empty_subsetI,subset_refl,
   9.338 -   Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint];
   9.339 +(* Congruence rule for set comprehension *)
   9.340 +val prems = goal Set.thy
   9.341 +  "[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \
   9.342 +\  {f x |x. P x} = {g x|x. Q x}";
   9.343 +by(simp_tac (!simpset addsimps prems) 1);
   9.344 +br set_ext 1;
   9.345 +br iffI 1;
   9.346 +by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1);
   9.347 +be CollectE 1;
   9.348 +be exE 1;
   9.349 +by(Asm_simp_tac 1);
   9.350 +be conjE 1;
   9.351 +by(rtac exI 1 THEN rtac conjI 1 THEN atac 2);
   9.352 +by(asm_simp_tac (!simpset addsimps prems) 1);
   9.353 +qed "Collect_cong1";
   9.354 +
   9.355 +Addsimps[subset_UNIV, empty_subsetI, subset_refl];
    10.1 --- a/src/HOL/subset.ML	Mon Mar 04 12:28:48 1996 +0100
    10.2 +++ b/src/HOL/subset.ML	Mon Mar 04 14:37:33 1996 +0100
    10.3 @@ -12,6 +12,10 @@
    10.4  qed_goal "subset_insertI" Set.thy "B <= insert a B"
    10.5   (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
    10.6  
    10.7 +goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
    10.8 +by(fast_tac set_cs 1);
    10.9 +qed "subset_insert";
   10.10 +
   10.11  (*** Big Union -- least upper bound of a set  ***)
   10.12  
   10.13  val prems = goal Set.thy