src/ZF/Fin.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 484 70b789956bd3
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 363
diff changeset
     1
(*  Title: 	ZF/ex/Fin.ML
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     2
    ID:         $Id$
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
     4
    Copyright   1994  University of Cambridge
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     5
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     6
Finite powerset operator
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     7
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
     8
prove X:Fin(A) ==> |X| < nat
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
     9
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
    10
prove:  b: Fin(A) ==> inj(b,b)<=surj(b,b)
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    11
*)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    12
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    13
structure Fin = Inductive_Fun
444
3ca9d49fd662 replaced extend_theory by new add_* functions;
clasohm
parents: 437
diff changeset
    14
 (val thy        = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
477
53fc8ad84b33 added thy_name to Datatype_Fun's parameter
clasohm
parents: 444
diff changeset
    15
  val thy_name   = "Fin"
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    16
  val rec_doms   = [("Fin","Pow(A)")]
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    17
  val sintrs     = ["0 : Fin(A)",
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    18
                    "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    19
  val monos      = []
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    20
  val con_defs   = []
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    21
  val type_intrs = [empty_subsetI, cons_subsetI, PowI]
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    22
  val type_elims = [make_elim PowD]);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    23
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    24
val [Fin_0I, Fin_consI] = Fin.intrs;
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    25
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    26
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    27
goalw Fin.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    28
by (rtac lfp_mono 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    29
by (REPEAT (rtac Fin.bnd_mono 1));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    30
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    31
val Fin_mono = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    32
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    33
(* A : Fin(B) ==> A <= B *)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    34
val FinD = Fin.dom_subset RS subsetD RS PowD;
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    35
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    36
(** Induction on finite sets **)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    37
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    38
(*Discharging x~:y entails extra work*)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    39
val major::prems = goal Fin.thy 
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    40
    "[| b: Fin(A);  \
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    41
\       P(0);        \
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    42
\       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y)) \
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    43
\    |] ==> P(b)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    44
by (rtac (major RS Fin.induct) 1);
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
    45
by (excluded_middle_tac "a:b" 2);
363
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    46
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);	    (*backtracking!*)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    47
by (REPEAT (ares_tac prems 1));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    48
val Fin_induct = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    49
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    50
(** Simplification for Fin **)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    51
val Fin_ss = arith_ss addsimps Fin.intrs;
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    52
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    53
(*The union of two finite sets is finite.*)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    54
val major::prems = goal Fin.thy
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    55
    "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    56
by (rtac (major RS Fin_induct) 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    57
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    58
val Fin_UnI = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    59
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    60
(*The union of a set of finite sets is finite.*)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    61
val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    62
by (rtac (major RS Fin_induct) 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    63
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    64
val Fin_UnionI = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    65
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    66
(*Every subset of a finite set is finite.*)
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    67
goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    68
by (etac Fin_induct 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    69
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    70
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    71
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    72
by (ALLGOALS (asm_simp_tac Fin_ss));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    73
val Fin_subset_lemma = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    74
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    75
goal Fin.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    76
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    77
val Fin_subset = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    78
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    79
val major::prems = goal Fin.thy 
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    80
    "[| c: Fin(A);  b: Fin(A);  				\
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    81
\       P(b);       						\
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    82
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    83
\    |] ==> c<=b --> P(b-c)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    84
by (rtac (major RS Fin_induct) 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    85
by (rtac (Diff_cons RS ssubst) 2);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    86
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    87
				Diff_subset RS Fin_subset]))));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    88
val Fin_0_induct_lemma = result();
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    89
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    90
val prems = goal Fin.thy 
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    91
    "[| b: Fin(A);  						\
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    92
\       P(b);        						\
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    93
\       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    94
\    |] ==> P(0)";
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    95
by (rtac (Diff_cancel RS subst) 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    96
by (rtac (Fin_0_induct_lemma RS mp) 1);
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    97
by (REPEAT (ares_tac (subset_refl::prems) 1));
1180a3c5479e renaming/removal of filenames to correct case
lcp
parents:
diff changeset
    98
val Fin_0_induct = result();
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
    99
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   100
(*Functions from a finite ordinal*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   101
val prems = goal Fin.thy "n: nat ==> n->A <= Fin(nat*A)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   102
by (nat_ind_tac "n" prems 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   103
by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin_0I, subset_iff, cons_iff]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   104
by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   105
by (fast_tac (ZF_cs addSIs [Fin_consI]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 477
diff changeset
   106
val nat_fun_subset_Fin = result();