src/ZF/Finite.ML
author paulson
Wed Feb 02 11:42:17 2000 +0100 (2000-02-02)
changeset 8181 ee74d3843214
parent 6070 032babd0120b
child 8183 344888de76c4
permissions -rw-r--r--
new theorems by Sidi O. Ehmety
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@534
    13
(*** Finite powerset operator ***)
lcp@534
    14
paulson@5137
    15
Goalw Fin.defs "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));
clasohm@760
    19
qed "Fin_mono";
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*)
paulson@5268
    27
val major::prems = Goal
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);
clasohm@1461
    34
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);      (*backtracking!*)
lcp@516
    35
by (REPEAT (ares_tac prems 1));
clasohm@760
    36
qed "Fin_induct";
lcp@516
    37
lcp@516
    38
(** Simplification for Fin **)
paulson@2469
    39
Addsimps Fin.intrs;
lcp@516
    40
lcp@516
    41
(*The union of two finite sets is finite.*)
paulson@5268
    42
Goal "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
paulson@2469
    43
by (etac Fin_induct 1);
wenzelm@4091
    44
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
clasohm@760
    45
qed "Fin_UnI";
lcp@516
    46
paulson@2469
    47
Addsimps [Fin_UnI];
paulson@2469
    48
paulson@5412
    49
lcp@516
    50
(*The union of a set of finite sets is finite.*)
lcp@516
    51
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
lcp@516
    52
by (rtac (major RS Fin_induct) 1);
paulson@2469
    53
by (ALLGOALS Asm_simp_tac);
clasohm@760
    54
qed "Fin_UnionI";
lcp@516
    55
lcp@516
    56
(*Every subset of a finite set is finite.*)
paulson@5137
    57
Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
lcp@516
    58
by (etac Fin_induct 1);
wenzelm@4091
    59
by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
wenzelm@4091
    60
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
paulson@4152
    61
by Safe_tac;
lcp@534
    62
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
paulson@2469
    63
by (Asm_simp_tac 1);
clasohm@760
    64
qed "Fin_subset_lemma";
lcp@516
    65
paulson@5137
    66
Goal "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
lcp@516
    67
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
clasohm@760
    68
qed "Fin_subset";
lcp@516
    69
paulson@5412
    70
Goal "b: Fin(A) ==> b Int c : Fin(A)";
paulson@5412
    71
by (blast_tac (claset() addIs [Fin_subset]) 1);
paulson@5412
    72
qed "Fin_IntI1";
paulson@5412
    73
paulson@5412
    74
Goal "c: Fin(A) ==> b Int c : Fin(A)";
paulson@5412
    75
by (blast_tac (claset() addIs [Fin_subset]) 1);
paulson@5412
    76
qed "Fin_IntI2";
paulson@5412
    77
paulson@5412
    78
Addsimps[Fin_IntI1, Fin_IntI2];
paulson@5412
    79
AddIs[Fin_IntI1, Fin_IntI2];
paulson@5412
    80
paulson@5412
    81
paulson@5268
    82
val major::prems = Goal
clasohm@1461
    83
    "[| c: Fin(A);  b: Fin(A);                                  \
clasohm@1461
    84
\       P(b);                                                   \
lcp@516
    85
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
lcp@516
    86
\    |] ==> c<=b --> P(b-c)";
lcp@516
    87
by (rtac (major RS Fin_induct) 1);
paulson@2033
    88
by (stac Diff_cons 2);
wenzelm@4091
    89
by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff, 
clasohm@1461
    90
                                Diff_subset RS Fin_subset]))));
clasohm@760
    91
qed "Fin_0_induct_lemma";
lcp@516
    92
paulson@5268
    93
val prems = Goal
clasohm@1461
    94
    "[| b: Fin(A);                                              \
clasohm@1461
    95
\       P(b);                                                   \
lcp@516
    96
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
lcp@516
    97
\    |] ==> P(0)";
lcp@516
    98
by (rtac (Diff_cancel RS subst) 1);
lcp@516
    99
by (rtac (Fin_0_induct_lemma RS mp) 1);
lcp@516
   100
by (REPEAT (ares_tac (subset_refl::prems) 1));
clasohm@760
   101
qed "Fin_0_induct";
lcp@516
   102
lcp@516
   103
(*Functions from a finite ordinal*)
paulson@5268
   104
Goal "n: nat ==> n->A <= Fin(nat*A)";
paulson@6070
   105
by (induct_tac "n" 1);
wenzelm@4091
   106
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
paulson@5268
   107
by (asm_simp_tac 
paulson@5268
   108
    (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
wenzelm@4091
   109
by (fast_tac (claset() addSIs [Fin.consI]) 1);
clasohm@760
   110
qed "nat_fun_subset_Fin";
lcp@534
   111
lcp@534
   112
lcp@534
   113
(*** Finite function space ***)
lcp@534
   114
wenzelm@5067
   115
Goalw FiniteFun.defs
paulson@8181
   116
    "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
lcp@534
   117
by (rtac lfp_mono 1);
lcp@534
   118
by (REPEAT (rtac FiniteFun.bnd_mono 1));
lcp@534
   119
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
clasohm@760
   120
qed "FiniteFun_mono";
lcp@534
   121
paulson@5137
   122
Goal "A<=B ==> A -||> A  <=  B -||> B";
lcp@534
   123
by (REPEAT (ares_tac [FiniteFun_mono] 1));
clasohm@760
   124
qed "FiniteFun_mono1";
lcp@534
   125
paulson@5137
   126
Goal "h: A -||>B ==> h: domain(h) -> B";
lcp@534
   127
by (etac FiniteFun.induct 1);
wenzelm@4091
   128
by (simp_tac (simpset() addsimps [empty_fun, domain_0]) 1);
wenzelm@4091
   129
by (asm_simp_tac (simpset() addsimps [fun_extend3, domain_cons]) 1);
clasohm@760
   130
qed "FiniteFun_is_fun";
lcp@534
   131
paulson@5137
   132
Goal "h: A -||>B ==> domain(h) : Fin(A)";
lcp@534
   133
by (etac FiniteFun.induct 1);
wenzelm@4091
   134
by (simp_tac (simpset() addsimps [domain_0]) 1);
wenzelm@4091
   135
by (asm_simp_tac (simpset() addsimps [domain_cons]) 1);
clasohm@760
   136
qed "FiniteFun_domain_Fin";
lcp@534
   137
lcp@803
   138
bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
lcp@534
   139
lcp@534
   140
(*Every subset of a finite function is a finite function.*)
paulson@5137
   141
Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
lcp@534
   142
by (etac FiniteFun.induct 1);
wenzelm@4091
   143
by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
wenzelm@4091
   144
by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
paulson@4152
   145
by Safe_tac;
lcp@534
   146
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
lcp@534
   147
by (dtac (spec RS mp) 1 THEN assume_tac 1);
wenzelm@4091
   148
by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
clasohm@760
   149
qed "FiniteFun_subset_lemma";
lcp@534
   150
paulson@5137
   151
Goal "[| c<=b;  b: A-||>B |] ==> c: A-||>B";
lcp@534
   152
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
clasohm@760
   153
qed "FiniteFun_subset";
lcp@534
   154
paulson@8181
   155
(** Some further results by Sidi O. Ehmety **)
paulson@8181
   156
paulson@8181
   157
Goal "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B";
paulson@8181
   158
by (etac Fin.induct 1);
paulson@8181
   159
by (simp_tac (simpset() addsimps FiniteFun.intrs) 1);
paulson@8181
   160
by (Clarify_tac 1);
paulson@8181
   161
by (case_tac "a:b" 1);
paulson@8181
   162
by (rotate_tac ~1 1);
paulson@8181
   163
by (asm_full_simp_tac (simpset() addsimps [cons_absorb]) 1);
paulson@8181
   164
by (subgoal_tac "restrict(f,b) : b -||> B" 1);
paulson@8181
   165
by (blast_tac (claset() addIs [restrict_type2]) 2);
paulson@8181
   166
by (stac fun_cons_restrict_eq 1 THEN assume_tac 1);
paulson@8181
   167
by (full_simp_tac (simpset() addsimps [restrict_def, lam_def]) 1);
paulson@8181
   168
by (blast_tac (claset() addIs [apply_funtype, impOfSubs FiniteFun_mono]
paulson@8181
   169
                              @FiniteFun.intrs) 1);
paulson@8181
   170
qed_spec_mp "fun_FiniteFunI";
paulson@8181
   171
paulson@8181
   172
Goal "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}";
paulson@8181
   173
by (blast_tac (claset() addIs [fun_FiniteFunI, lam_funtype]) 1);
paulson@8181
   174
qed "lam_FiniteFun";
paulson@8181
   175
paulson@8181
   176
Goal "f : FiniteFun(A, {y:B. P(y)})  \
paulson@8181
   177
\     <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))";
paulson@8181
   178
by Auto_tac;
paulson@8181
   179
by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1);
paulson@8181
   180
by (blast_tac (claset() addDs [FiniteFun_is_fun]
paulson@8181
   181
                        addEs [Pair_mem_PiE]) 1);
paulson@8181
   182
by (res_inst_tac [("A1", "domain(f)")]
paulson@8181
   183
    (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
paulson@8181
   184
by (fast_tac (claset() addDs
paulson@8181
   185
		[FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1);
paulson@8181
   186
by (resolve_tac [fun_FiniteFunI] 1);
paulson@8181
   187
be FiniteFun_domain_Fin 1;
paulson@8181
   188
by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1);
paulson@8181
   189
by (ALLGOALS
paulson@8181
   190
    (blast_tac (claset() addDs
paulson@8181
   191
		[FiniteFun_is_fun, range_of_fun, range_type,
paulson@8181
   192
		 apply_equality])));
paulson@8181
   193
qed "FiniteFun_Collect_iff";