src/ZF/Fin.ML
author clasohm
Fri Jul 01 11:03:42 1994 +0200 (1994-07-01 ago)
changeset 444 3ca9d49fd662
parent 437 435875e4b21d
child 477 53fc8ad84b33
permissions -rw-r--r--
replaced extend_theory by new add_* functions;
changed syntax of datatype declaration
     1 (*  Title: 	ZF/ex/Fin.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Finite powerset operator
     7 
     8 prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)
     9 	card(0)=0
    10 	[| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
    11 
    12 b: Fin(A) ==> inj(b,b)<=surj(b,b)
    13 
    14 Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j))
    15 Fin(univ(A)) <= univ(A)
    16 *)
    17 
    18 structure Fin = Inductive_Fun
    19  (val thy        = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
    20   val rec_doms   = [("Fin","Pow(A)")]
    21   val sintrs     = ["0 : Fin(A)",
    22                     "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
    23   val monos      = []
    24   val con_defs   = []
    25   val type_intrs = [empty_subsetI, cons_subsetI, PowI]
    26   val type_elims = [make_elim PowD]);
    27 
    28 store_theory "Fin" Fin.thy;
    29 
    30 val [Fin_0I, Fin_consI] = Fin.intrs;
    31 
    32 
    33 goalw Fin.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    34 by (rtac lfp_mono 1);
    35 by (REPEAT (rtac Fin.bnd_mono 1));
    36 by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
    37 val Fin_mono = result();
    38 
    39 (* A : Fin(B) ==> A <= B *)
    40 val FinD = Fin.dom_subset RS subsetD RS PowD;
    41 
    42 (** Induction on finite sets **)
    43 
    44 (*Discharging x~:y entails extra work*)
    45 val major::prems = goal Fin.thy 
    46     "[| b: Fin(A);  \
    47 \       P(0);        \
    48 \       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
    49 \    |] ==> P(b)";
    50 by (rtac (major RS Fin.induct) 1);
    51 by (excluded_middle_tac "a:b" 2);
    52 by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
    53 by (REPEAT (ares_tac prems 1));
    54 val Fin_induct = result();
    55 
    56 (** Simplification for Fin **)
    57 val Fin_ss = arith_ss addsimps Fin.intrs;
    58 
    59 (*The union of two finite sets is finite.*)
    60 val major::prems = goal Fin.thy
    61     "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
    62 by (rtac (major RS Fin_induct) 1);
    63 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
    64 val Fin_UnI = result();
    65 
    66 (*The union of a set of finite sets is finite.*)
    67 val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
    68 by (rtac (major RS Fin_induct) 1);
    69 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
    70 val Fin_UnionI = result();
    71 
    72 (*Every subset of a finite set is finite.*)
    73 goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
    74 by (etac Fin_induct 1);
    75 by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
    76 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
    77 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
    78 by (ALLGOALS (asm_simp_tac Fin_ss));
    79 val Fin_subset_lemma = result();
    80 
    81 goal Fin.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
    82 by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
    83 val Fin_subset = result();
    84 
    85 val major::prems = goal Fin.thy 
    86     "[| c: Fin(A);  b: Fin(A);  				\
    87 \       P(b);       						\
    88 \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    89 \    |] ==> c<=b --> P(b-c)";
    90 by (rtac (major RS Fin_induct) 1);
    91 by (rtac (Diff_cons RS ssubst) 2);
    92 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
    93 				Diff_subset RS Fin_subset]))));
    94 val Fin_0_induct_lemma = result();
    95 
    96 val prems = goal Fin.thy 
    97     "[| b: Fin(A);  						\
    98 \       P(b);        						\
    99 \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
   100 \    |] ==> P(0)";
   101 by (rtac (Diff_cancel RS subst) 1);
   102 by (rtac (Fin_0_induct_lemma RS mp) 1);
   103 by (REPEAT (ares_tac (subset_refl::prems) 1));
   104 val Fin_0_induct = result();