src/ZF/InfDatatype.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 47071 2884ee1ffbf0
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26056
diff changeset
     1
(*  Title:      ZF/InfDatatype.thy
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
     3
    Copyright   1994  University of Cambridge
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
     4
*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
     5
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     6
header{*Infinite-Branching Datatype Definitions*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     7
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 16417
diff changeset
     8
theory InfDatatype imports Datatype_ZF Univ Finite Cardinal_AC begin
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
     9
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    10
lemmas fun_Limit_VfromE =
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    11
    Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    12
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    13
lemma fun_Vcsucc_lemma:
47071
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    14
  assumes f: "f \<in> D -> Vfrom(A,csucc(K))" and DK: "|D| \<le> K" and ICK: "InfCard(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    15
  shows "\<exists>j. f \<in> D -> Vfrom(A,j) & j < csucc(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    16
proof (rule exI, rule conjI)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    17
  show "f \<in> D \<rightarrow> Vfrom(A, \<Union>z\<in>D. \<mu> i. f`z \<in> Vfrom (A,i))"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    18
    proof (rule Pi_type [OF f])
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    19
      fix d
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    20
      assume d: "d \<in> D"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    21
      show "f ` d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    22
        proof (rule fun_Limit_VfromE [OF f d ICK]) 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    23
          fix x
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    24
          assume "x < csucc(K)"  "f ` d \<in> Vfrom(A, x)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    25
          hence "f`d \<in> Vfrom(A, \<mu> i. f`d \<in> Vfrom (A,i))" using d
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    26
            by (fast elim: LeastI ltE)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    27
          also have "... \<subseteq> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    28
            by (rule Vfrom_mono) (auto intro: d) 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    29
          finally show "f`d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" .
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    30
        qed
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    31
    qed
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    32
next
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    33
  show "(\<Union>d\<in>D. \<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    34
    proof (rule le_UN_Ord_lt_csucc [OF ICK DK])
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    35
      fix d
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    36
      assume d: "d \<in> D"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    37
      show "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    38
        proof (rule fun_Limit_VfromE [OF f d ICK]) 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    39
          fix x
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    40
          assume "x < csucc(K)"  "f ` d \<in> Vfrom(A, x)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    41
          thus "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    42
            by (blast intro: Least_le lt_trans1 lt_Ord) 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    43
        qed
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    44
    qed
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 46820
diff changeset
    45
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    46
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    47
lemma subset_Vcsucc:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    48
     "[| D \<subseteq> Vfrom(A,csucc(K));  |D| \<le> K;  InfCard(K) |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    49
      ==> \<exists>j. D \<subseteq> Vfrom(A,j) & j < csucc(K)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    50
by (simp add: subset_iff_id fun_Vcsucc_lemma)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    51
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    52
(*Version for arbitrary index sets*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    53
lemma fun_Vcsucc:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    54
     "[| |D| \<le> K;  InfCard(K);  D \<subseteq> Vfrom(A,csucc(K)) |] ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    55
          D -> Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    56
apply (safe dest!: fun_Vcsucc_lemma subset_Vcsucc)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    57
apply (rule Vfrom [THEN ssubst])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    58
apply (drule fun_is_rel)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    59
(*This level includes the function, and is below csucc(K)*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    60
apply (rule_tac a1 = "succ (succ (j \<union> ja))" in UN_I [THEN UnI2])
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    61
apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    62
                    Un_least_lt)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    63
apply (erule subset_trans [THEN PowI])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    64
apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    65
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    66
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    67
lemma fun_in_Vcsucc:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    68
     "[| f: D -> Vfrom(A, csucc(K));  |D| \<le> K;  InfCard(K);
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    69
         D \<subseteq> Vfrom(A,csucc(K)) |]
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    70
       ==> f: Vfrom(A,csucc(K))"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    71
by (blast intro: fun_Vcsucc [THEN subsetD])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    72
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    73
text{*Remove @{text "\<subseteq>"} from the rule above*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    74
lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    75
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    76
(** Version where K itself is the index set **)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    77
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    78
lemma Card_fun_Vcsucc:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    79
     "InfCard(K) ==> K -> Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    80
apply (frule InfCard_is_Card [THEN Card_is_Ord])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    81
apply (blast del: subsetI
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    82
             intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    83
                   lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans])
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    84
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    85
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    86
lemma Card_fun_in_Vcsucc:
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    87
     "[| f: K -> Vfrom(A, csucc(K));  InfCard(K) |] ==> f: Vfrom(A,csucc(K))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    88
by (blast intro: Card_fun_Vcsucc [THEN subsetD])
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    89
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    90
lemma Limit_csucc: "InfCard(K) ==> Limit(csucc(K))"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    91
by (erule InfCard_csucc [THEN InfCard_is_Limit])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    92
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    93
lemmas Pair_in_Vcsucc = Pair_in_VLimit [OF _ _ Limit_csucc]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    94
lemmas Inl_in_Vcsucc = Inl_in_VLimit [OF _ Limit_csucc]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    95
lemmas Inr_in_Vcsucc = Inr_in_VLimit [OF _ Limit_csucc]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    96
lemmas zero_in_Vcsucc = Limit_csucc [THEN zero_in_VLimit]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    97
lemmas nat_into_Vcsucc = nat_into_VLimit [OF _ Limit_csucc]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
    98
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
    99
(*For handling Cardinals of the form  @{term"nat \<union> |X|"} *)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   100
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   101
lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   102
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   103
lemmas le_nat_Un_cardinal =
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   104
     Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   105
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   106
lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   107
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   108
(*The new version of Data_Arg.intrs, declared in Datatype.ML*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   109
lemmas Data_Arg_intros =
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   110
       SigmaI InlI InrI
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
   111
       Pair_in_univ Inl_in_univ Inr_in_univ
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   112
       zero_in_univ A_into_univ nat_into_univ UnCI
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   113
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   114
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   115
lemmas inf_datatype_intros =
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   116
     InfCard_nat InfCard_nat_Un_cardinal
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
   117
     Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   118
     zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 32960
diff changeset
   119
     Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   120
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   121
end
bf37a3049251 converted the AC branch to Isar
paulson
parents: 516
diff changeset
   122