src/ZF/Finite.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 1956 589af052bcd4
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:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
     1
(*  Title:      ZF/Finite.ML
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
516
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
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
     6
Finite powerset operator; finite function space
516
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
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    15
(*** Finite powerset operator ***)
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    16
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    17
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    18
by (rtac lfp_mono 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    19
by (REPEAT (rtac Fin.bnd_mono 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    20
by (REPEAT (ares_tac (Pow_mono::basic_monos) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    21
qed "Fin_mono";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    22
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    23
(* A : Fin(B) ==> A <= B *)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    24
val FinD = Fin.dom_subset RS subsetD RS PowD;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    25
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    26
(** Induction on finite sets **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    27
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    28
(*Discharging x~:y entails extra work*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    29
val major::prems = goal Finite.thy 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    30
    "[| b: Fin(A);  \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    31
\       P(0);        \
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    32
\       !!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
    33
\    |] ==> P(b)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    34
by (rtac (major RS Fin.induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    35
by (excluded_middle_tac "a:b" 2);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
    36
by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3);      (*backtracking!*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    37
by (REPEAT (ares_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    38
qed "Fin_induct";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    39
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    40
(** Simplification for Fin **)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    41
val Fin_ss = arith_ss addsimps Fin.intrs;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    42
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    43
(*The union of two finite sets is finite.*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    44
val major::prems = goal Finite.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    45
    "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    46
by (rtac (major RS Fin_induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    47
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    48
qed "Fin_UnI";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    49
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    50
(*The union of a set of finite sets is finite.*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    51
val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    52
by (rtac (major RS Fin_induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    53
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    54
qed "Fin_UnionI";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    55
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    56
(*Every subset of a finite set is finite.*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    57
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
    58
by (etac Fin_induct 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    59
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    60
by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    61
by (safe_tac ZF_cs);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    62
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    63
by (asm_simp_tac Fin_ss 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    64
qed "Fin_subset_lemma";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    65
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    66
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
    67
by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    68
qed "Fin_subset";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    69
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    70
val major::prems = goal Finite.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
    71
    "[| c: Fin(A);  b: Fin(A);                                  \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
    72
\       P(b);                                                   \
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    73
\       !!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
    74
\    |] ==> c<=b --> P(b-c)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    75
by (rtac (major RS Fin_induct) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    76
by (rtac (Diff_cons RS ssubst) 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    77
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
    78
                                Diff_subset RS Fin_subset]))));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    79
qed "Fin_0_induct_lemma";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    80
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    81
val prems = goal Finite.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
    82
    "[| b: Fin(A);                                              \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 803
diff changeset
    83
\       P(b);                                                   \
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    84
\       !!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
    85
\    |] ==> P(0)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    86
by (rtac (Diff_cancel RS subst) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    87
by (rtac (Fin_0_induct_lemma RS mp) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    88
by (REPEAT (ares_tac (subset_refl::prems) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    89
qed "Fin_0_induct";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    90
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    91
(*Functions from a finite ordinal*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    92
val prems = goal Finite.thy "n: nat ==> n->A <= Fin(nat*A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    93
by (nat_ind_tac "n" prems 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents:
diff changeset
    94
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
    95
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
    96
by (fast_tac (ZF_cs addSIs [Fin.consI]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
    97
qed "nat_fun_subset_Fin";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    98
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
    99
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   100
(*** Finite function space ***)
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   101
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   102
goalw Finite.thy FiniteFun.defs
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   103
    "!!A B C D. [| A<=C;  B<=D |] ==> A -||> B  <=  C -||> D";
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   104
by (rtac lfp_mono 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   105
by (REPEAT (rtac FiniteFun.bnd_mono 1));
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   106
by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
   107
qed "FiniteFun_mono";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   108
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   109
goal Finite.thy "!!A B. A<=B ==> A -||> A  <=  B -||> B";
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   110
by (REPEAT (ares_tac [FiniteFun_mono] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
   111
qed "FiniteFun_mono1";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   112
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   113
goal Finite.thy "!!h. h: A -||>B ==> h: domain(h) -> B";
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   114
by (etac FiniteFun.induct 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   115
by (simp_tac (ZF_ss addsimps [empty_fun, domain_0]) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   116
by (asm_simp_tac (ZF_ss addsimps [fun_extend3, domain_cons]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
   117
qed "FiniteFun_is_fun";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   118
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   119
goal Finite.thy "!!h. h: A -||>B ==> domain(h) : Fin(A)";
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   120
by (etac FiniteFun.induct 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   121
by (simp_tac (Fin_ss addsimps [domain_0]) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   122
by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
   123
qed "FiniteFun_domain_Fin";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   124
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 760
diff changeset
   125
bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type);
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   126
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   127
(*Every subset of a finite function is a finite function.*)
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   128
goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B";
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   129
by (etac FiniteFun.induct 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   130
by (simp_tac (ZF_ss addsimps subset_empty_iff::FiniteFun.intrs) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   131
by (asm_simp_tac (ZF_ss addsimps subset_cons_iff::distrib_rews) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   132
by (safe_tac ZF_cs);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   133
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   134
by (dtac (spec RS mp) 1 THEN assume_tac 1);
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   135
by (fast_tac (ZF_cs addSIs FiniteFun.intrs) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
   136
qed "FiniteFun_subset_lemma";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   137
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   138
goal Finite.thy "!!c b A. [| c<=b;  b: A-||>B |] ==> c: A-||>B";
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   139
by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 534
diff changeset
   140
qed "FiniteFun_subset";
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 516
diff changeset
   141