author nipkow Mon Mar 04 14:37:33 1996 +0100 (1996-03-04 ago) changeset 1531 e5eb247ad13c parent 1530 63fed88fe8e6 child 1532 769a4517ad7b
Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
 src/HOL/Finite.ML file | annotate | diff | revisions src/HOL/Finite.thy file | annotate | diff | revisions src/HOL/Nat.ML file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions src/HOL/Set.ML file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions src/HOL/Univ.ML file | annotate | diff | revisions src/HOL/Univ.thy file | annotate | diff | revisions src/HOL/equalities.ML file | annotate | diff | revisions src/HOL/subset.ML file | annotate | diff | revisions
```     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.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.37 +                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
1.38 +qed "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.45 +qed "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.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.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.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.115 +                          setloop split_tac[expand_if]) 1);
1.116 +qed "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.146 +
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.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.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.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.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.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.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.11 +
9.12 +goal Set.thy "(A <= {}) = (A = {})";
9.13 +by(fast_tac eq_cs 1);
9.14 +qed "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.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.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.40
9.41  bind_thm("empty_not_insert",insert_not_empty RS not_sym);
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.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.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.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.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.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.90
9.91  goal Set.thy "A Int {} = {}";
9.92  by (fast_tac eq_cs 1);
9.93  qed "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.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.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.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.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.131
9.132  goal Set.thy "A Un {} = A";
9.133  by(fast_tac eq_cs 1);
9.134  qed "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.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.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.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.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.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.179 +
9.180 +goal Set.thy "Union(UNIV) = UNIV";
9.181 +by (fast_tac eq_cs 1);
9.182 +qed "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.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.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.205 +
9.206 +goal Set.thy "Inter(UNIV) = {}";
9.207 +by (fast_tac eq_cs 1);
9.208 +qed "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.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.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.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.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.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.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.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.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.264
9.265  goal Set.thy "(INT x.B) = B";
9.266  by (fast_tac eq_cs 1);
9.267  qed "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.277
9.278  goal Set.thy "{}-A = {}";
9.279  by (fast_tac eq_cs 1);
9.280  qed "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.287 +
9.288 +goal Set.thy "A-UNIV = {}";
9.289 +by (fast_tac eq_cs 1);
9.290 +qed "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.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.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.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.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.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 +
```
```    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
```