src/ZF/Finite.ML
author lcp
Fri, 12 Aug 1994 12:51:34 +0200
changeset 516 1957113f0d7d
child 534 cd8bec47e175
permissions -rw-r--r--
installation of new inductive/datatype sections
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Finite.ML
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     2
    ID:         $Id$
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     5
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     6
Finite powerset operator
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     7
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     8
prove X:Fin(A) ==> |X| < nat
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     9
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    10
prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    11
*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    12
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    13
open Finite;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    14
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    15
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    16
by (rtac lfp_mono 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    17
by (REPEAT (rtac Fin.bnd_mono 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    18
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    19
val Fin_mono = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    20
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    21
(* A : Fin(B) ==> A <= B *)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    22
val FinD = Fin.dom_subset RS subsetD RS PowD;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    23
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    24
(** Induction on finite sets **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    25
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    26
(*Discharging x~:y entails extra work*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    27
val major::prems = goal Finite.thy 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    28
    "[| b: Fin(A);  \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    29
\       P(0);        \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    30
\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    31
\    |] ==> P(b)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    32
by (rtac (major RS Fin.induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    33
by (excluded_middle_tac "a:b" 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    34
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    35
by (REPEAT (ares_tac prems 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    36
val Fin_induct = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    37
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    38
(** Simplification for Fin **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    39
val Fin_ss = arith_ss addsimps Fin.intrs;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    40
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    41
(*The union of two finite sets is finite.*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    42
val major::prems = goal Finite.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    43
    "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    44
by (rtac (major RS Fin_induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    45
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    46
val Fin_UnI = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    47
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    48
(*The union of a set of finite sets is finite.*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    49
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    50
by (rtac (major RS Fin_induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    51
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    52
val Fin_UnionI = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    53
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    54
(*Every subset of a finite set is finite.*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    55
goal Finite.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    56
by (etac Fin_induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    57
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    58
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    59
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    60
by (ALLGOALS (asm_simp_tac Fin_ss));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    61
val Fin_subset_lemma = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    62
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    63
goal Finite.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    64
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    65
val Fin_subset = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    66
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    67
val major::prems = goal Finite.thy 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    68
    "[| c: Fin(A);  b: Fin(A);  				\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    69
\       P(b);       						\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    70
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    71
\    |] ==> c<=b --> P(b-c)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    72
by (rtac (major RS Fin_induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    73
by (rtac (Diff_cons RS ssubst) 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    74
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    75
				Diff_subset RS Fin_subset]))));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    76
val Fin_0_induct_lemma = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    77
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    78
val prems = goal Finite.thy 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    79
    "[| b: Fin(A);  						\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    80
\       P(b);        						\
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    81
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    82
\    |] ==> P(0)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    83
by (rtac (Diff_cancel RS subst) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    84
by (rtac (Fin_0_induct_lemma RS mp) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    85
by (REPEAT (ares_tac (subset_refl::prems) 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    86
val Fin_0_induct = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    87
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    88
(*Functions from a finite ordinal*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    89
val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    90
by (nat_ind_tac "n" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    91
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin.emptyI, subset_iff, cons_iff]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    92
by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    93
by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    94
val nat_fun_subset_Fin = result();