src/ZF/InfDatatype.ML
author clasohm
Tue, 30 Jan 1996 13:42:57 +0100
changeset 1461 6bcb44e4d6e5
parent 801 316121afb5b5
child 2469 b50b8c0eec01
permissions -rw-r--r--
expanded tabs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
     1
(*  Title:      ZF/InfDatatype.ML
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
488
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
801
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
     6
Infinite-branching datatype definitions
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     7
*)
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     8
801
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
     9
val fun_Limit_VfromE =
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    10
   [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE 
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    11
   |> standard;
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    12
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    13
goal InfDatatype.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    14
    "!!K. [| f: W -> Vfrom(A,csucc(K));  |W| le K;  InfCard(K)  \
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    15
\         |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    16
by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    17
by (rtac conjI 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    18
by (rtac le_UN_Ord_lt_csucc 2);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    19
by (rtac ballI 4  THEN
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    20
    etac fun_Limit_VfromE 4 THEN REPEAT_SOME assume_tac);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    21
by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    22
by (rtac Pi_type 1);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    23
by (rename_tac "w" 2);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    24
by (etac fun_Limit_VfromE 2 THEN REPEAT_SOME assume_tac);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    25
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
    26
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    27
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
    28
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 692
diff changeset
    29
qed "fun_Vcsucc_lemma";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    30
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    31
goal InfDatatype.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    32
    "!!K. [| W <= Vfrom(A,csucc(K));  |W| le K;  InfCard(K)     \
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    33
\         |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    34
by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 692
diff changeset
    35
qed "subset_Vcsucc";
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    36
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    37
(*Version for arbitrary index sets*)
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    38
goal InfDatatype.thy
534
cd8bec47e175 ZF/Finite: added the finite function space, A-||>B
lcp
parents: 524
diff changeset
    39
    "!!K. [| |W| le K;  InfCard(K);  W <= Vfrom(A,csucc(K)) |] ==> \
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    40
\         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    41
by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    42
by (resolve_tac [Vfrom RS ssubst] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    43
by (dtac fun_is_rel 1);
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    44
(*This level includes the function, and is below csucc(K)*)
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    45
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
    46
by (eresolve_tac [subset_trans RS PowI] 2);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    47
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
    48
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    49
                      Limit_has_succ, Un_least_lt] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 692
diff changeset
    50
qed "fun_Vcsucc";
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    51
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    52
goal InfDatatype.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    53
    "!!K. [| f: W -> Vfrom(A, csucc(K));  |W| le K;  InfCard(K);        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    54
\            W <= Vfrom(A,csucc(K))                                     \
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    55
\         |] ==> f: Vfrom(A,csucc(K))";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    56
by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 692
diff changeset
    57
qed "fun_in_Vcsucc";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    58
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    59
(*Remove <= from the rule above*)
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    60
val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    61
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    62
(** Version where K itself is the index set **)
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    63
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    64
goal InfDatatype.thy
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    65
    "!!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
    66
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    67
by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    68
                      i_subset_Vfrom,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    69
                      lt_csucc RS leI RS le_imp_subset RS subset_trans] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 692
diff changeset
    70
qed "Card_fun_Vcsucc";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    71
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    72
goal InfDatatype.thy
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    73
    "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    74
\         |] ==> f: Vfrom(A,csucc(K))";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
    75
by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 692
diff changeset
    76
qed "Card_fun_in_Vcsucc";
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    77
801
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    78
(*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*)
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    79
qed_goal "Limit_csucc" InfDatatype.thy
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    80
    "!!K. InfCard(K) ==> Limit(csucc(K))"
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    81
  (fn _ => [etac (InfCard_csucc RS InfCard_is_Limit) 1]);
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    82
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    83
bind_thm ("Pair_in_Vcsucc",  Limit_csucc RSN (3, Pair_in_VLimit));
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    84
bind_thm ("Inl_in_Vcsucc",   Limit_csucc RSN (2, Inl_in_VLimit));
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    85
bind_thm ("Inr_in_Vcsucc",   Limit_csucc RSN (2, Inr_in_VLimit));
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    86
bind_thm ("zero_in_Vcsucc",  Limit_csucc RS zero_in_VLimit);
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    87
bind_thm ("nat_into_Vcsucc", Limit_csucc RSN (2, nat_into_VLimit));
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
    88
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    89
(*For handling Cardinals of the form  (nat Un |X|) *)
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    90
801
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    91
bind_thm ("InfCard_nat_Un_cardinal",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    92
          [InfCard_nat, Card_cardinal] MRS InfCard_Un);
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    93
801
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    94
bind_thm ("le_nat_Un_cardinal",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    95
          [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le);
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    96
801
316121afb5b5 Added Limit_csucc from CardinalArith
lcp
parents: 768
diff changeset
    97
bind_thm ("UN_upper_cardinal",
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 801
diff changeset
    98
          UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le);
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
    99
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   100
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
   101
val inf_datatype_intrs =  
524
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   102
    [InfCard_nat, InfCard_nat_Un_cardinal,
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   103
     Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   104
     zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
b1bf18e83302 ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents: 517
diff changeset
   105
     Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs;