src/ZF/InfDatatype.ML
author lcp
Mon, 15 Aug 1994 18:15:09 +0200
changeset 524 b1bf18e83302
parent 517 a9f93400f307
child 534 cd8bec47e175
permissions -rw-r--r--
ZF/InfDatatype: simplified, extended results for infinite branching
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/InfDatatype.ML
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     2
    ID:         $Id$
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     5
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
     6
Datatype Definitions involving ->
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
     7
	Even infinite-branching!
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     8
*)
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     9
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    10
(*** Closure under finite powerset ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    11
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    12
val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    13
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    14
goal Fin_Univ_thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    15
   "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    16
by (eresolve_tac [Fin_induct] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    17
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    18
by (safe_tac ZF_cs);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    19
by (eresolve_tac [Limit_VfromE] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    20
by (assume_tac 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    21
by (res_inst_tac [("x", "xa Un j")] exI 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    22
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    23
			   Un_least_lt]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    24
val Fin_Vfrom_lemma = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    25
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    26
goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    27
by (rtac subsetI 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    28
by (dresolve_tac [Fin_Vfrom_lemma] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    29
by (safe_tac ZF_cs);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    30
by (resolve_tac [Vfrom RS ssubst] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    31
by (fast_tac (ZF_cs addSDs [ltD]) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    32
val Fin_VLimit = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    33
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    34
val Fin_subset_VLimit = 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    35
    [Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    36
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    37
goal Fin_Univ_thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    38
    "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    39
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    40
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    41
		      nat_subset_VLimit, subset_refl] 1));
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    42
val nat_fun_VLimit = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    43
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    44
val nat_fun_subset_VLimit = 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    45
    [Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    46
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    47
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    48
goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    49
by (rtac (Limit_nat RS Fin_VLimit) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    50
val Fin_univ = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    51
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    52
val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    53
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    54
goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    55
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    56
val nat_fun_univ = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    57
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    58
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    59
(*** Infinite branching ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    60
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    61
val fun_Limit_VfromE = 
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    62
    [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    63
	|> standard;
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    64
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    65
goal InfDatatype.thy
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    66
    "!!K. [| f: W -> Vfrom(A,csucc(K));  |W| le K;  InfCard(K)	\
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    67
\         |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    68
by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    69
by (resolve_tac [conjI] 1);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    70
by (resolve_tac [le_UN_Ord_lt_csucc] 2);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    71
by (rtac ballI 4  THEN
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    72
    eresolve_tac [fun_Limit_VfromE] 4 THEN REPEAT_SOME assume_tac);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    73
by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    74
by (resolve_tac [Pi_type] 1);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    75
by (rename_tac "w" 2);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    76
by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    77
by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    78
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    79
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    80
by (assume_tac 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    81
val fun_Vcsucc_lemma = result();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    82
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    83
goal InfDatatype.thy
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    84
    "!!K. [| W <= Vfrom(A,csucc(K));  |W| le K;  InfCard(K)	\
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    85
\         |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    86
by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    87
val subset_Vcsucc = result();
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    88
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    89
(*Version for arbitrary index sets*)
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    90
goal InfDatatype.thy
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    91
    "!!K. [| |W| le K;  W <= Vfrom(A,csucc(K));  InfCard(K) |] ==> \
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    92
\         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    93
by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    94
by (resolve_tac [Vfrom RS ssubst] 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    95
by (eresolve_tac [PiE] 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    96
(*This level includes the function, and is below csucc(K)*)
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    97
by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1);
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    98
by (eresolve_tac [subset_trans RS PowI] 2);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    99
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2);
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   100
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   101
		      Limit_has_succ, Un_least_lt] 1));
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   102
val fun_Vcsucc = result();
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   103
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   104
goal InfDatatype.thy
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   105
    "!!K. [| f: W -> Vfrom(A, csucc(K));  |W| le K;  InfCard(K);	\
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   106
\            W <= Vfrom(A,csucc(K)) 					\
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   107
\         |] ==> f: Vfrom(A,csucc(K))";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   108
by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   109
val fun_in_Vcsucc = result();
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   110
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   111
(*Remove <= from the rule above*)
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   112
val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   113
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   114
(** Version where K itself is the index set **)
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   115
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   116
goal InfDatatype.thy
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   117
    "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   118
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   119
by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   120
		      i_subset_Vfrom,
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   121
		      lt_csucc RS leI RS le_imp_subset RS subset_trans] 1));
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   122
val Card_fun_Vcsucc = result();
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   123
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   124
goal InfDatatype.thy
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   125
    "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   126
\         |] ==> f: Vfrom(A,csucc(K))";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   127
by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   128
val Card_fun_in_Vcsucc = result();
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   129
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   130
val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   131
val Inl_in_Vcsucc  = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   132
val Inr_in_Vcsucc  = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   133
val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   134
val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   135
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   136
(*For handling Cardinals of the form  (nat Un |X|) *)
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   137
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   138
val InfCard_nat_Un_cardinal = [InfCard_nat, Card_cardinal] MRS InfCard_Un
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   139
                              |> standard;
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   140
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   141
val le_nat_Un_cardinal = 
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   142
    [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   143
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   144
val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le 
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   145
                        |> standard;
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   146
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   147
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   148
val inf_datatype_intrs =  
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   149
    [InfCard_nat, InfCard_nat_Un_cardinal,
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   150
     Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   151
     zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   152
     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs;