src/ZF/fin.ML
author wenzelm
Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717 20c42415c07d
parent 279 7738aed3f84d
permissions -rw-r--r--
plain ASCII;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ex/fin.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Finite powerset operator
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
could define cardinality?
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
	card(0)=0
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
    12
	[| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
b: Fin(A) ==> inj(b,b)<=surj(b,b)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
Fin(univ(A)) <= univ(A)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
structure Fin = Inductive_Fun
279
7738aed3f84d Improved layout for inductive defs
lcp
parents: 129
diff changeset
    21
 (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
7738aed3f84d Improved layout for inductive defs
lcp
parents: 129
diff changeset
    22
  val rec_doms   = [("Fin","Pow(A)")]
7738aed3f84d Improved layout for inductive defs
lcp
parents: 129
diff changeset
    23
  val sintrs     = ["0 : Fin(A)",
7738aed3f84d Improved layout for inductive defs
lcp
parents: 129
diff changeset
    24
                    "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
7738aed3f84d Improved layout for inductive defs
lcp
parents: 129
diff changeset
    25
  val monos      = []
7738aed3f84d Improved layout for inductive defs
lcp
parents: 129
diff changeset
    26
  val con_defs   = []
70
8a29f8b4aca1 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
lcp
parents: 55
diff changeset
    27
  val type_intrs = [empty_subsetI, cons_subsetI, PowI]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val type_elims = [make_elim PowD]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
124
858ab9a9b047 made pseudo theories for all ML files;
clasohm
parents: 70
diff changeset
    30
store_theory "Fin" Fin.thy;
858ab9a9b047 made pseudo theories for all ML files;
clasohm
parents: 70
diff changeset
    31
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val [Fin_0I, Fin_consI] = Fin.intrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
goalw Fin.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (rtac lfp_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
by (REPEAT (rtac Fin.bnd_mono 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val Fin_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
(* A : Fin(B) ==> A <= B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val FinD = Fin.dom_subset RS subsetD RS PowD;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(** Induction on finite sets **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
    46
(*Discharging x~:y entails extra work*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val major::prems = goal Fin.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    "[| b: Fin(A);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
\       P(0);        \
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
    50
\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
\    |] ==> P(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
by (rtac (major RS Fin.induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
by (res_inst_tac [("Q","a:b")] (excluded_middle RS disjE) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val Fin_induct = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
(** Simplification for Fin **)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    59
val Fin_ss = arith_ss addsimps Fin.intrs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    61
(*The union of two finite sets is finite.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val major::prems = goal Fin.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (rtac (major RS Fin_induct) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    65
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val Fin_UnI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    68
(*The union of a set of finite sets is finite.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
by (rtac (major RS Fin_induct) 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    71
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val Fin_UnionI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    74
(*Every subset of a finite set is finite.*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    75
goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
129
dc50a4b96d7b expandshort and other trivial changes
lcp
parents: 124
diff changeset
    76
by (etac Fin_induct 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    77
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    80
by (ALLGOALS (asm_simp_tac Fin_ss));
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    81
val Fin_subset_lemma = result();
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    82
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    83
goal Fin.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 37
diff changeset
    84
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
val Fin_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val major::prems = goal Fin.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
    "[| c: Fin(A);  b: Fin(A);  				\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
\       P(b);       						\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
\    |] ==> c<=b --> P(b-c)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (rtac (major RS Fin_induct) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
by (rtac (Diff_cons RS ssubst) 2);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    94
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
				Diff_subset RS Fin_subset]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
val Fin_0_induct_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
val prems = goal Fin.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
    "[| b: Fin(A);  						\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
\       P(b);        						\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
\    |] ==> P(0)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
by (rtac (Diff_cancel RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (rtac (Fin_0_induct_lemma RS mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (REPEAT (ares_tac (subset_refl::prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val Fin_0_induct = result();