src/ZF/Finite.ML
author paulson
Tue Sep 01 10:11:06 1998 +0200 (1998-09-01)
changeset 5412 0c2472c74c24
parent 5268 59ef39008514
child 6070 032babd0120b
permissions -rw-r--r--
New lemmas involving Int
clasohm@1461
     1
(*  Title:      ZF/Finite.ML
lcp@516
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
lcp@516
     5
lcp@534
     6
Finite powerset operator; finite function space
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@534
    15
(*** Finite powerset operator ***)
lcp@534
    16
paulson@5137
    17
Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
lcp@516
    18
by (rtac lfp_mono 1);
lcp@516
    19
by (REPEAT (rtac Fin.bnd_mono 1));
lcp@516
    20
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
clasohm@760
    21
qed "Fin_mono";
lcp@516
    22
lcp@516
    23
(* A : Fin(B) ==> A <= B *)
lcp@516
    24
val FinD = Fin.dom_subset RS subsetD RS PowD;
lcp@516
    25
lcp@516
    26
(** Induction on finite sets **)
lcp@516
    27
lcp@516
    28
(*Discharging x~:y entails extra work*)
paulson@5268
    29
val major::prems = Goal
lcp@516
    30
    "[| b: Fin(A);  \
lcp@516
    31
\       P(0);        \
lcp@516
    32
\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
lcp@516
    33
\    |] ==> P(b)";
lcp@516
    34
by (rtac (major RS Fin.induct) 1);
lcp@516
    35
by (excluded_middle_tac "a:b" 2);
clasohm@1461
    36
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);      (*backtracking!*)
lcp@516
    37
by (REPEAT (ares_tac prems 1));
clasohm@760
    38
qed "Fin_induct";
lcp@516
    39
lcp@516
    40
(** Simplification for Fin **)
paulson@2469
    41
Addsimps Fin.intrs;
lcp@516
    42
lcp@516
    43
(*The union of two finite sets is finite.*)
paulson@5268
    44
Goal "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
paulson@2469
    45
by (etac Fin_induct 1);
wenzelm@4091
    46
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
clasohm@760
    47
qed "Fin_UnI";
lcp@516
    48
paulson@2469
    49
Addsimps [Fin_UnI];
paulson@2469
    50
paulson@5412
    51
lcp@516
    52
(*The union of a set of finite sets is finite.*)
lcp@516
    53
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
lcp@516
    54
by (rtac (major RS Fin_induct) 1);
paulson@2469
    55
by (ALLGOALS Asm_simp_tac);
clasohm@760
    56
qed "Fin_UnionI";
lcp@516
    57
lcp@516
    58
(*Every subset of a finite set is finite.*)
paulson@5137
    59
Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
lcp@516
    60
by (etac Fin_induct 1);
wenzelm@4091
    61
by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
wenzelm@4091
    62
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
paulson@4152
    63
by Safe_tac;
lcp@534
    64
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
paulson@2469
    65
by (Asm_simp_tac 1);
clasohm@760
    66
qed "Fin_subset_lemma";
lcp@516
    67
paulson@5137
    68
Goal "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
lcp@516
    69
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
clasohm@760
    70
qed "Fin_subset";
lcp@516
    71
paulson@5412
    72
Goal "b: Fin(A) ==> b Int c : Fin(A)";
paulson@5412
    73
by (blast_tac (claset() addIs [Fin_subset]) 1);
paulson@5412
    74
qed "Fin_IntI1";
paulson@5412
    75
paulson@5412
    76
Goal "c: Fin(A) ==> b Int c : Fin(A)";
paulson@5412
    77
by (blast_tac (claset() addIs [Fin_subset]) 1);
paulson@5412
    78
qed "Fin_IntI2";
paulson@5412
    79
paulson@5412
    80
Addsimps[Fin_IntI1, Fin_IntI2];
paulson@5412
    81
AddIs[Fin_IntI1, Fin_IntI2];
paulson@5412
    82
paulson@5412
    83
paulson@5268
    84
val major::prems = Goal
clasohm@1461
    85
    "[| c: Fin(A);  b: Fin(A);                                  \
clasohm@1461
    86
\       P(b);                                                   \
lcp@516
    87
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
lcp@516
    88
\    |] ==> c<=b --> P(b-c)";
lcp@516
    89
by (rtac (major RS Fin_induct) 1);
paulson@2033
    90
by (stac Diff_cons 2);
wenzelm@4091
    91
by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff, 
clasohm@1461
    92
                                Diff_subset RS Fin_subset]))));
clasohm@760
    93
qed "Fin_0_induct_lemma";
lcp@516
    94
paulson@5268
    95
val prems = Goal
clasohm@1461
    96
    "[| b: Fin(A);                                              \
clasohm@1461
    97
\       P(b);                                                   \
lcp@516
    98
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
lcp@516
    99
\    |] ==> P(0)";
lcp@516
   100
by (rtac (Diff_cancel RS subst) 1);
lcp@516
   101
by (rtac (Fin_0_induct_lemma RS mp) 1);
lcp@516
   102
by (REPEAT (ares_tac (subset_refl::prems) 1));
clasohm@760
   103
qed "Fin_0_induct";
lcp@516
   104
lcp@516
   105
(*Functions from a finite ordinal*)
paulson@5268
   106
Goal "n: nat ==> n->A <= Fin(nat*A)";
paulson@5268
   107
by (nat_ind_tac "n" [] 1);
wenzelm@4091
   108
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
paulson@5268
   109
by (asm_simp_tac 
paulson@5268
   110
    (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
wenzelm@4091
   111
by (fast_tac (claset() addSIs [Fin.consI]) 1);
clasohm@760
   112
qed "nat_fun_subset_Fin";
lcp@534
   113
lcp@534
   114
lcp@534
   115
(*** Finite function space ***)
lcp@534
   116
wenzelm@5067
   117
Goalw FiniteFun.defs
lcp@534
   118
    "!!A B C D. [| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
lcp@534
   119
by (rtac lfp_mono 1);
lcp@534
   120
by (REPEAT (rtac FiniteFun.bnd_mono 1));
lcp@534
   121
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
clasohm@760
   122
qed "FiniteFun_mono";
lcp@534
   123
paulson@5137
   124
Goal "A<=B ==> A -||> A  <=  B -||> B";
lcp@534
   125
by (REPEAT (ares_tac [FiniteFun_mono] 1));
clasohm@760
   126
qed "FiniteFun_mono1";
lcp@534
   127
paulson@5137
   128
Goal "h: A -||>B ==> h: domain(h) -> B";
lcp@534
   129
by (etac FiniteFun.induct 1);
wenzelm@4091
   130
by (simp_tac (simpset() addsimps [empty_fun, domain_0]) 1);
wenzelm@4091
   131
by (asm_simp_tac (simpset() addsimps [fun_extend3, domain_cons]) 1);
clasohm@760
   132
qed "FiniteFun_is_fun";
lcp@534
   133
paulson@5137
   134
Goal "h: A -||>B ==> domain(h) : Fin(A)";
lcp@534
   135
by (etac FiniteFun.induct 1);
wenzelm@4091
   136
by (simp_tac (simpset() addsimps [domain_0]) 1);
wenzelm@4091
   137
by (asm_simp_tac (simpset() addsimps [domain_cons]) 1);
clasohm@760
   138
qed "FiniteFun_domain_Fin";
lcp@534
   139
lcp@803
   140
bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
lcp@534
   141
lcp@534
   142
(*Every subset of a finite function is a finite function.*)
paulson@5137
   143
Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
lcp@534
   144
by (etac FiniteFun.induct 1);
wenzelm@4091
   145
by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
wenzelm@4091
   146
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
paulson@4152
   147
by Safe_tac;
lcp@534
   148
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
lcp@534
   149
by (dtac (spec RS mp) 1 THEN assume_tac 1);
wenzelm@4091
   150
by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
clasohm@760
   151
qed "FiniteFun_subset_lemma";
lcp@534
   152
paulson@5137
   153
Goal "[| c<=b;  b: A-||>B |] ==> c: A-||>B";
lcp@534
   154
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
clasohm@760
   155
qed "FiniteFun_subset";
lcp@534
   156