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