author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 47071  2884ee1ffbf0 
child 58871  c399ae4b836f 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26056
diff
changeset

1 
(* Title: ZF/InfDatatype.thy 
13134  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1994 University of Cambridge 

4 
*) 

5 

13356  6 
header{*InfiniteBranching Datatype Definitions*} 
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  9 

46820  10 
lemmas fun_Limit_VfromE = 
13134  11 
Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]] 
12 

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  46 

47 
lemma subset_Vcsucc: 

46820  48 
"[ D \<subseteq> Vfrom(A,csucc(K)); D \<le> K; InfCard(K) ] 
49 
==> \<exists>j. D \<subseteq> Vfrom(A,j) & j < csucc(K)" 

13134  50 
by (simp add: subset_iff_id fun_Vcsucc_lemma) 
51 

52 
(*Version for arbitrary index sets*) 

53 
lemma fun_Vcsucc: 

46820  54 
"[ D \<le> K; InfCard(K); D \<subseteq> Vfrom(A,csucc(K)) ] ==> 
55 
D > Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))" 

13134  56 
apply (safe dest!: fun_Vcsucc_lemma subset_Vcsucc) 
57 
apply (rule Vfrom [THEN ssubst]) 

58 
apply (drule fun_is_rel) 

59 
(*This level includes the function, and is below csucc(K)*) 

46820  60 
apply (rule_tac a1 = "succ (succ (j \<union> ja))" in UN_I [THEN UnI2]) 
13134  61 
apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ 
46820  62 
Un_least_lt) 
13134  63 
apply (erule subset_trans [THEN PowI]) 
64 
apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2) 

65 
done 

66 

67 
lemma fun_in_Vcsucc: 

46820  68 
"[ f: D > Vfrom(A, csucc(K)); D \<le> K; InfCard(K); 
69 
D \<subseteq> Vfrom(A,csucc(K)) ] 

13134  70 
==> f: Vfrom(A,csucc(K))" 
71 
by (blast intro: fun_Vcsucc [THEN subsetD]) 

72 

46820  73 
text{*Remove @{text "\<subseteq>"} from the rule above*} 
13134  74 
lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI] 
75 

76 
(** Version where K itself is the index set **) 

77 

78 
lemma Card_fun_Vcsucc: 

46820  79 
"InfCard(K) ==> K > Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))" 
13134  80 
apply (frule InfCard_is_Card [THEN Card_is_Ord]) 
81 
apply (blast del: subsetI 

46820  82 
intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom 
83 
lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans]) 

13134  84 
done 
85 

86 
lemma Card_fun_in_Vcsucc: 

87 
"[ f: K > Vfrom(A, csucc(K)); InfCard(K) ] ==> f: Vfrom(A,csucc(K))" 

46820  88 
by (blast intro: Card_fun_Vcsucc [THEN subsetD]) 
13134  89 

90 
lemma Limit_csucc: "InfCard(K) ==> Limit(csucc(K))" 

91 
by (erule InfCard_csucc [THEN InfCard_is_Limit]) 

92 

93 
lemmas Pair_in_Vcsucc = Pair_in_VLimit [OF _ _ Limit_csucc] 

94 
lemmas Inl_in_Vcsucc = Inl_in_VLimit [OF _ Limit_csucc] 

95 
lemmas Inr_in_Vcsucc = Inr_in_VLimit [OF _ Limit_csucc] 

96 
lemmas zero_in_Vcsucc = Limit_csucc [THEN zero_in_VLimit] 

97 
lemmas nat_into_Vcsucc = nat_into_VLimit [OF _ Limit_csucc] 

98 

46820  99 
(*For handling Cardinals of the form @{term"nat \<union> X"} *) 
13134  100 

101 
lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal] 

102 

103 
lemmas le_nat_Un_cardinal = 

104 
Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]] 

105 

106 
lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le] 

107 

108 
(*The new version of Data_Arg.intrs, declared in Datatype.ML*) 

109 
lemmas Data_Arg_intros = 

110 
SigmaI InlI InrI 

46820  111 
Pair_in_univ Inl_in_univ Inr_in_univ 
13134  112 
zero_in_univ A_into_univ nat_into_univ UnCI 
113 

114 
(*For most Kbranching datatypes with domain Vfrom(A, csucc(K)) *) 

115 
lemmas inf_datatype_intros = 

116 
InfCard_nat InfCard_nat_Un_cardinal 

46820  117 
Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc 
13134  118 
zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc 
46820  119 
Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I 
13134  120 

121 
end 

122 