src/ZF/Finite.ML
author lcp
Fri Aug 12 12:51:34 1994 +0200 (1994-08-12)
changeset 516 1957113f0d7d
child 534 cd8bec47e175
permissions -rw-r--r--
installation of new inductive/datatype sections
lcp@516
     1
(*  Title: 	ZF/Finite.ML
lcp@516
     2
    ID:         $Id$
lcp@516
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
lcp@516
     5
lcp@516
     6
Finite powerset operator
lcp@516
     7
lcp@516
     8
prove X:Fin(A) ==> |X| < nat
lcp@516
     9
lcp@516
    10
prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
lcp@516
    11
*)
lcp@516
    12
lcp@516
    13
open Finite;
lcp@516
    14
lcp@516
    15
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
lcp@516
    16
by (rtac lfp_mono 1);
lcp@516
    17
by (REPEAT (rtac Fin.bnd_mono 1));
lcp@516
    18
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
lcp@516
    19
val Fin_mono = result();
lcp@516
    20
lcp@516
    21
(* A : Fin(B) ==> A <= B *)
lcp@516
    22
val FinD = Fin.dom_subset RS subsetD RS PowD;
lcp@516
    23
lcp@516
    24
(** Induction on finite sets **)
lcp@516
    25
lcp@516
    26
(*Discharging x~:y entails extra work*)
lcp@516
    27
val major::prems = goal Finite.thy 
lcp@516
    28
    "[| b: Fin(A);  \
lcp@516
    29
\       P(0);        \
lcp@516
    30
\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
lcp@516
    31
\    |] ==> P(b)";
lcp@516
    32
by (rtac (major RS Fin.induct) 1);
lcp@516
    33
by (excluded_middle_tac "a:b" 2);
lcp@516
    34
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
lcp@516
    35
by (REPEAT (ares_tac prems 1));
lcp@516
    36
val Fin_induct = result();
lcp@516
    37
lcp@516
    38
(** Simplification for Fin **)
lcp@516
    39
val Fin_ss = arith_ss addsimps Fin.intrs;
lcp@516
    40
lcp@516
    41
(*The union of two finite sets is finite.*)
lcp@516
    42
val major::prems = goal Finite.thy
lcp@516
    43
    "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
lcp@516
    44
by (rtac (major RS Fin_induct) 1);
lcp@516
    45
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
lcp@516
    46
val Fin_UnI = result();
lcp@516
    47
lcp@516
    48
(*The union of a set of finite sets is finite.*)
lcp@516
    49
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
lcp@516
    50
by (rtac (major RS Fin_induct) 1);
lcp@516
    51
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
lcp@516
    52
val Fin_UnionI = result();
lcp@516
    53
lcp@516
    54
(*Every subset of a finite set is finite.*)
lcp@516
    55
goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
lcp@516
    56
by (etac Fin_induct 1);
lcp@516
    57
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
lcp@516
    58
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
lcp@516
    59
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
lcp@516
    60
by (ALLGOALS (asm_simp_tac Fin_ss));
lcp@516
    61
val Fin_subset_lemma = result();
lcp@516
    62
lcp@516
    63
goal Finite.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
lcp@516
    64
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
lcp@516
    65
val Fin_subset = result();
lcp@516
    66
lcp@516
    67
val major::prems = goal Finite.thy 
lcp@516
    68
    "[| c: Fin(A);  b: Fin(A);  				\
lcp@516
    69
\       P(b);       						\
lcp@516
    70
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
lcp@516
    71
\    |] ==> c<=b --> P(b-c)";
lcp@516
    72
by (rtac (major RS Fin_induct) 1);
lcp@516
    73
by (rtac (Diff_cons RS ssubst) 2);
lcp@516
    74
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
lcp@516
    75
				Diff_subset RS Fin_subset]))));
lcp@516
    76
val Fin_0_induct_lemma = result();
lcp@516
    77
lcp@516
    78
val prems = goal Finite.thy 
lcp@516
    79
    "[| b: Fin(A);  						\
lcp@516
    80
\       P(b);        						\
lcp@516
    81
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
lcp@516
    82
\    |] ==> P(0)";
lcp@516
    83
by (rtac (Diff_cancel RS subst) 1);
lcp@516
    84
by (rtac (Fin_0_induct_lemma RS mp) 1);
lcp@516
    85
by (REPEAT (ares_tac (subset_refl::prems) 1));
lcp@516
    86
val Fin_0_induct = result();
lcp@516
    87
lcp@516
    88
(*Functions from a finite ordinal*)
lcp@516
    89
val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
lcp@516
    90
by (nat_ind_tac "n" prems 1);
lcp@516
    91
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1);
lcp@516
    92
by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
lcp@516
    93
by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
lcp@516
    94
val nat_fun_subset_Fin = result();