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