src/ZF/Finite.ML
 author paulson Fri Jun 30 12:51:30 2000 +0200 (2000-06-30) changeset 9211 6236c5285bd8 parent 9173 422968aeed49 child 9907 473a6604da94 permissions -rw-r--r--
removal of batch-style proofs
```     1 (*  Title:      ZF/Finite.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 Finite powerset operator; finite function space
```
```     7
```
```     8 prove X:Fin(A) ==> |X| < nat
```
```     9
```
```    10 prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
```
```    11 *)
```
```    12
```
```    13 (*** Finite powerset operator ***)
```
```    14
```
```    15 Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
```
```    16 by (rtac lfp_mono 1);
```
```    17 by (REPEAT (rtac Fin.bnd_mono 1));
```
```    18 by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
```
```    19 qed "Fin_mono";
```
```    20
```
```    21 (* A : Fin(B) ==> A <= B *)
```
```    22 val FinD = Fin.dom_subset RS subsetD RS PowD;
```
```    23
```
```    24 (** Induction on finite sets **)
```
```    25
```
```    26 (*Discharging x~:y entails extra work*)
```
```    27 val major::prems = Goal
```
```    28     "[| b: Fin(A);  \
```
```    29 \       P(0);        \
```
```    30 \       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
```
```    31 \    |] ==> P(b)";
```
```    32 by (rtac (major RS Fin.induct) 1);
```
```    33 by (excluded_middle_tac "a:b" 2);
```
```    34 by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);      (*backtracking!*)
```
```    35 by (REPEAT (ares_tac prems 1));
```
```    36 qed "Fin_induct";
```
```    37
```
```    38 (** Simplification for Fin **)
```
```    39 Addsimps Fin.intrs;
```
```    40
```
```    41 (*The union of two finite sets is finite.*)
```
```    42 Goal "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
```
```    43 by (etac Fin_induct 1);
```
```    44 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
```
```    45 qed "Fin_UnI";
```
```    46
```
```    47 Addsimps [Fin_UnI];
```
```    48
```
```    49
```
```    50 (*The union of a set of finite sets is finite.*)
```
```    51 Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
```
```    52 by (etac Fin_induct 1);
```
```    53 by (ALLGOALS Asm_simp_tac);
```
```    54 qed "Fin_UnionI";
```
```    55
```
```    56 (*Every subset of a finite set is finite.*)
```
```    57 Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
```
```    58 by (etac Fin_induct 1);
```
```    59 by (simp_tac (simpset() addsimps [subset_empty_iff]) 1);
```
```    60 by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
```
```    61 by Safe_tac;
```
```    62 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
```
```    63 by (Asm_simp_tac 1);
```
```    64 qed "Fin_subset_lemma";
```
```    65
```
```    66 Goal "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
```
```    67 by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
```
```    68 qed "Fin_subset";
```
```    69
```
```    70 Goal "b: Fin(A) ==> b Int c : Fin(A)";
```
```    71 by (blast_tac (claset() addIs [Fin_subset]) 1);
```
```    72 qed "Fin_IntI1";
```
```    73
```
```    74 Goal "c: Fin(A) ==> b Int c : Fin(A)";
```
```    75 by (blast_tac (claset() addIs [Fin_subset]) 1);
```
```    76 qed "Fin_IntI2";
```
```    77
```
```    78 Addsimps[Fin_IntI1, Fin_IntI2];
```
```    79 AddIs[Fin_IntI1, Fin_IntI2];
```
```    80
```
```    81
```
```    82 val major::prems = Goal
```
```    83     "[| c: Fin(A);  b: Fin(A);                                  \
```
```    84 \       P(b);                                                   \
```
```    85 \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
```
```    86 \    |] ==> c<=b --> P(b-c)";
```
```    87 by (rtac (major RS Fin_induct) 1);
```
```    88 by (stac Diff_cons 2);
```
```    89 by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff,
```
```    90                                 Diff_subset RS Fin_subset]))));
```
```    91 qed "Fin_0_induct_lemma";
```
```    92
```
```    93 val prems = Goal
```
```    94     "[| b: Fin(A);                                              \
```
```    95 \       P(b);                                                   \
```
```    96 \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
```
```    97 \    |] ==> P(0)";
```
```    98 by (rtac (Diff_cancel RS subst) 1);
```
```    99 by (rtac (Fin_0_induct_lemma RS mp) 1);
```
```   100 by (REPEAT (ares_tac (subset_refl::prems) 1));
```
```   101 qed "Fin_0_induct";
```
```   102
```
```   103 (*Functions from a finite ordinal*)
```
```   104 Goal "n: nat ==> n->A <= Fin(nat*A)";
```
```   105 by (induct_tac "n" 1);
```
```   106 by (simp_tac (simpset() addsimps [subset_iff]) 1);
```
```   107 by (asm_simp_tac
```
```   108     (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
```
```   109 by (fast_tac (claset() addSIs [Fin.consI]) 1);
```
```   110 qed "nat_fun_subset_Fin";
```
```   111
```
```   112
```
```   113 (*** Finite function space ***)
```
```   114
```
```   115 Goalw FiniteFun.defs
```
```   116     "[| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
```
```   117 by (rtac lfp_mono 1);
```
```   118 by (REPEAT (rtac FiniteFun.bnd_mono 1));
```
```   119 by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
```
```   120 qed "FiniteFun_mono";
```
```   121
```
```   122 Goal "A<=B ==> A -||> A  <=  B -||> B";
```
```   123 by (REPEAT (ares_tac [FiniteFun_mono] 1));
```
```   124 qed "FiniteFun_mono1";
```
```   125
```
```   126 Goal "h: A -||>B ==> h: domain(h) -> B";
```
```   127 by (etac FiniteFun.induct 1);
```
```   128 by (Simp_tac 1);
```
```   129 by (asm_simp_tac (simpset() addsimps [fun_extend3]) 1);
```
```   130 qed "FiniteFun_is_fun";
```
```   131
```
```   132 Goal "h: A -||>B ==> domain(h) : Fin(A)";
```
```   133 by (etac FiniteFun.induct 1);
```
```   134 by (Simp_tac 1);
```
```   135 by (Asm_simp_tac 1);
```
```   136 qed "FiniteFun_domain_Fin";
```
```   137
```
```   138 bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
```
```   139
```
```   140 (*Every subset of a finite function is a finite function.*)
```
```   141 Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
```
```   142 by (etac FiniteFun.induct 1);
```
```   143 by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1);
```
```   144 by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1);
```
```   145 by Safe_tac;
```
```   146 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
```
```   147 by (dtac (spec RS mp) 1 THEN assume_tac 1);
```
```   148 by (fast_tac (claset() addSIs FiniteFun.intrs) 1);
```
```   149 qed "FiniteFun_subset_lemma";
```
```   150
```
```   151 Goal "[| c<=b;  b: A-||>B |] ==> c: A-||>B";
```
```   152 by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
```
```   153 qed "FiniteFun_subset";
```
```   154
```
```   155 (** Some further results by Sidi O. Ehmety **)
```
```   156
```
```   157 Goal "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B";
```
```   158 by (etac Fin.induct 1);
```
```   159 by (simp_tac (simpset() addsimps FiniteFun.intrs) 1);
```
```   160 by (Clarify_tac 1);
```
```   161 by (case_tac "a:b" 1);
```
```   162 by (rotate_tac ~1 1);
```
```   163 by (asm_full_simp_tac (simpset() addsimps [cons_absorb]) 1);
```
```   164 by (subgoal_tac "restrict(f,b) : b -||> B" 1);
```
```   165 by (blast_tac (claset() addIs [restrict_type2]) 2);
```
```   166 by (stac fun_cons_restrict_eq 1 THEN assume_tac 1);
```
```   167 by (full_simp_tac (simpset() addsimps [restrict_def, lam_def]) 1);
```
```   168 by (blast_tac (claset() addIs [apply_funtype, impOfSubs FiniteFun_mono]
```
```   169                               @FiniteFun.intrs) 1);
```
```   170 qed_spec_mp "fun_FiniteFunI";
```
```   171
```
```   172 Goal "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}";
```
```   173 by (blast_tac (claset() addIs [fun_FiniteFunI, lam_funtype]) 1);
```
```   174 qed "lam_FiniteFun";
```
```   175
```
```   176 Goal "f : FiniteFun(A, {y:B. P(y)})  \
```
```   177 \     <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))";
```
```   178 by Auto_tac;
```
```   179 by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1);
```
```   180 by (blast_tac (claset() addDs [Pair_mem_PiD, FiniteFun_is_fun]) 1);
```
```   181 by (res_inst_tac [("A1", "domain(f)")]
```
```   182     (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
```
```   183 by (fast_tac (claset() addDs
```
```   184 		[FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1);
```
```   185 by (rtac fun_FiniteFunI 1);
```
```   186 by (etac FiniteFun_domain_Fin 1);
```
```   187 by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1);
```
```   188 by (ALLGOALS
```
```   189     (blast_tac (claset() addDs
```
```   190 		[FiniteFun_is_fun, range_of_fun, range_type,
```
```   191 		 apply_equality])));
```
```   192 qed "FiniteFun_Collect_iff";
```