author nipkow Wed, 06 Mar 1996 10:05:00 +0100 changeset 1548 afe750876848 parent 1547 9ee49b349bb4 child 1549 ac9b58304d62
 src/HOL/Finite.ML file | annotate | diff | comparison | revisions src/HOL/Set.ML file | annotate | diff | comparison | revisions src/HOL/equalities.ML file | annotate | diff | comparison | revisions src/HOL/simpdata.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/Finite.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -8,7 +8,7 @@

open Finite;

-(*** Fin ***)
+section "The finite powerset operator -- Fin";

goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
by (rtac lfp_mono 1);
@@ -98,7 +98,7 @@
qed "Fin_empty_induct";

-(*** finite ***)
+section "The predicate 'finite'";

val major::prems = goalw Finite.thy [finite_def]
"[| finite F;  P({}); \
@@ -163,7 +163,7 @@
qed "finite_empty_induct";

-(*** Cardinality ***)
+section "Finite cardinality -- 'card'";

goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
by(fast_tac eq_cs 1);
@@ -175,8 +175,6 @@
qed "card_empty";

-
val [major] = goal Finite.thy
"finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
br (major RS finite_induct) 1;
@@ -188,7 +186,7 @@
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);
qed "finite_has_card";

goal Finite.thy
@@ -265,7 +263,7 @@
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
be subst 1;
br refl 1;
br notI 1;```
```--- a/src/HOL/Set.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/Set.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -8,7 +8,9 @@

open Set;

-val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
+section "Relating predicates and sets";
+
+val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}";
by (rtac (mem_Collect_eq RS ssubst) 1);
by (rtac prem 1);
qed "CollectI";
@@ -29,7 +31,7 @@

val CollectE = make_elim CollectD;

-(*** Bounded quantifiers ***)
+section "Bounded quantifiers";

val prems = goalw Set.thy [Ball_def]
"[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
@@ -91,7 +93,7 @@
ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
qed "bex_cong";

-(*** Subsets ***)
+section "Subsets";

val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
by (REPEAT (ares_tac (prems @ [ballI]) 1));
@@ -126,7 +128,7 @@
qed "subset_trans";

-(*** Equality ***)
+section "Equality";

(*Anti-symmetry of the subset relation*)
val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
@@ -168,7 +170,7 @@
qed "setup_induction";

-(*** Set complement -- Compl ***)
+section "Set complement -- Compl";

val prems = goalw Set.thy [Compl_def]
"[| c:A ==> False |] ==> c : Compl(A)";
@@ -186,7 +188,7 @@
val ComplE = make_elim ComplD;

-(*** Binary union -- Un ***)
+section "Binary union -- Un";

val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
@@ -210,7 +212,7 @@
qed "UnE";

-(*** Binary intersection -- Int ***)
+section "Binary intersection -- Int";

val prems = goalw Set.thy [Int_def]
"[| c:A;  c:B |] ==> c : A Int B";
@@ -233,7 +235,7 @@
qed "IntE";

-(*** Set difference ***)
+section "Set difference";

qed_goalw "DiffI" Set.thy [set_diff_def]
"[| c : A;  c ~: B |] ==> c : A - B"
@@ -257,7 +259,7 @@
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 -- {} ***)
+section "The empty set -- {}";

qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
(fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]);
@@ -275,7 +277,7 @@
[ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);

-(*** Augmenting a set -- insert ***)
+section "Augmenting a set -- insert";

qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B"
(fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]);
@@ -298,7 +300,7 @@
[ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
(etac prem 1) ]);

-(*** Singletons, using insert ***)
+section "Singletons, using insert";

qed_goal "singletonI" Set.thy "a : {a}"
(fn _=> [ (rtac insertI1 1) ]);
@@ -320,13 +322,13 @@
qed "singleton_inject";

-(*** UNIV - The universal set ***)
+section "The universal set -- UNIV";

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)  ***)
+section "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*)
val prems = goalw Set.thy [UNION_def]
@@ -349,7 +351,7 @@
qed "UN_cong";

-(*** Intersections of families -- INTER x:A. B(x) is Inter(B``A) *)
+section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";

val prems = goalw Set.thy [INTER_def]
"(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
@@ -378,7 +380,7 @@
qed "INT_cong";

-(*** Unions over a type; UNION1(B) = Union(range(B)) ***)
+section "Unions over a type; UNION1(B) = Union(range(B))";

(*The order of the premises presupposes that A is rigid; b may be flexible*)
val prems = goalw Set.thy [UNION1_def]
@@ -393,7 +395,7 @@
qed "UN1_E";

-(*** Intersections over a type; INTER1(B) = Inter(range(B)) *)
+section "Intersections over a type; INTER1(B) = Inter(range(B))";

val prems = goalw Set.thy [INTER1_def]
"(!!x. b: B(x)) ==> b : (INT x. B(x))";
@@ -405,7 +407,7 @@
by (rtac (TrueI RS (CollectI RS (major RS INT_D))) 1);
qed "INT1_D";

-(*** Unions ***)
+section "Union";

(*The order of the premises presupposes that C is rigid; A may be flexible*)
val prems = goalw Set.thy [Union_def]
@@ -419,7 +421,7 @@
by (REPEAT (ares_tac prems 1));
qed "UnionE";

-(*** Inter ***)
+section "Inter";

val prems = goalw Set.thy [Inter_def]
"[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
@@ -441,7 +443,7 @@
by (REPEAT (eresolve_tac prems 1));
qed "InterE";

-(*** Powerset ***)
+section "The Powerset operator -- Pow";

qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
(fn _ => [ (etac CollectI 1) ]);```
```--- a/src/HOL/equalities.ML	Tue Mar 05 17:37:28 1996 +0100
+++ b/src/HOL/equalities.ML	Wed Mar 06 10:05:00 1996 +0100
@@ -10,6 +10,8 @@

val eq_cs = set_cs addSIs [equalityI];

+section "{}";
+
goal Set.thy "{x.False} = {}";
by(fast_tac eq_cs 1);
qed "Collect_False_empty";
@@ -20,7 +22,7 @@
qed "subset_empty";

-(** The membership relation, : **)
+section ":";

goal Set.thy "x ~: {}";
by(fast_tac set_cs 1);
@@ -32,7 +34,7 @@
qed "in_insert";

-(** insert **)
+section "insert";

(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
goal Set.thy "insert a A = {a} Un A";
@@ -67,7 +69,7 @@
by(fast_tac eq_cs 1);
qed "mk_disjoint_insert";

-(** Image **)
+section "''";

goal Set.thy "f``{} = {}";
by (fast_tac eq_cs 1);
@@ -79,7 +81,7 @@
qed "image_insert";

-(** Binary Intersection **)
+section "Int";

goal Set.thy "A Int A = A";
by (fast_tac eq_cs 1);
@@ -127,7 +129,7 @@
qed "Int_UNIV";

-(** Binary Union **)
+section "Un";

goal Set.thy "A Un A = A";
by (fast_tac eq_cs 1);
@@ -188,7 +190,7 @@
qed "Un_empty";

-(** Simple properties of Compl -- complement of a set **)
+section "Compl";

goal Set.thy "A Int Compl(A) = {}";
by (fast_tac eq_cs 1);
@@ -227,7 +229,7 @@
qed "Un_Int_assoc_eq";

-(** Big Union and Intersection **)
+section "Union";

goal Set.thy "Union({}) = {}";
by (fast_tac eq_cs 1);
@@ -258,6 +260,8 @@
by (fast_tac (eq_cs addSEs [equalityE]) 1);
qed "Union_disjoint";

+section "Inter";
+
goal Set.thy "Inter({}) = UNIV";
by (fast_tac eq_cs 1);
qed "Inter_empty";
@@ -284,7 +288,7 @@
by (best_tac eq_cs 1);
qed "Inter_Un_distrib";

-(** Unions and Intersections of Families **)
+section "UN and INT";

(*Basic identities*)

@@ -410,7 +414,7 @@
by (fast_tac eq_cs 1);
qed "Un_INT_distrib2";

-(** Simple properties of Diff -- set difference **)
+section "-";

goal Set.thy "A-A = {}";
by (fast_tac eq_cs 1);
@@ -482,20 +486,4 @@
by (fast_tac eq_cs 1);
qed "Diff_Int";

-(* 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}";
-br set_ext 1;
-br iffI 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);
-qed "Collect_cong1";
-
```--- a/src/HOL/simpdata.ML	Tue Mar 05 17:37:28 1996 +0100