|
1 theory Datatype_absolute = WF_absolute: |
|
2 |
|
3 (*Epsilon.thy*) |
|
4 lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})" |
|
5 apply (insert arg_subset_eclose [of "{i}"], simp) |
|
6 apply (frule eclose_subset, blast) |
|
7 done |
|
8 |
|
9 lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)" |
|
10 apply (rule equalityI) |
|
11 apply (erule eclose_sing_Ord) |
|
12 apply (rule succ_subset_eclose_sing) |
|
13 done |
|
14 |
|
15 (*Ordinal.thy*) |
|
16 lemma relation_Memrel: "relation(Memrel(A))" |
|
17 by (simp add: relation_def Memrel_def, blast) |
|
18 |
|
19 lemma (in M_axioms) nat_case_closed: |
|
20 "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))" |
|
21 apply (case_tac "k=0", simp) |
|
22 apply (case_tac "\<exists>m. k = succ(m)") |
|
23 apply force |
|
24 apply (simp add: nat_case_def) |
|
25 done |
|
26 |
|
27 |
|
28 subsection{*The lfp of a continuous function can be expressed as a union*} |
|
29 |
|
30 constdefs |
|
31 contin :: "[i=>i]=>o" |
|
32 "contin(h) == (\<forall>A. A\<noteq>0 --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))" |
|
33 |
|
34 lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \<in> nat|] ==> h^n (0) <= D" |
|
35 apply (induct_tac n) |
|
36 apply (simp_all add: bnd_mono_def, blast) |
|
37 done |
|
38 |
|
39 |
|
40 lemma contin_iterates_eq: |
|
41 "contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))" |
|
42 apply (simp add: contin_def) |
|
43 apply (rule trans) |
|
44 apply (rule equalityI) |
|
45 apply (simp_all add: UN_subset_iff) |
|
46 apply safe |
|
47 apply (erule_tac [2] natE) |
|
48 apply (rule_tac a="succ(x)" in UN_I) |
|
49 apply simp_all |
|
50 apply blast |
|
51 done |
|
52 |
|
53 lemma lfp_subset_Union: |
|
54 "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) <= (\<Union>n\<in>nat. h^n(0))" |
|
55 apply (rule lfp_lowerbound) |
|
56 apply (simp add: contin_iterates_eq) |
|
57 apply (simp add: contin_def bnd_mono_iterates_subset UN_subset_iff) |
|
58 done |
|
59 |
|
60 lemma Union_subset_lfp: |
|
61 "bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)" |
|
62 apply (simp add: UN_subset_iff) |
|
63 apply (rule ballI) |
|
64 apply (induct_tac x, simp_all) |
|
65 apply (rule subset_trans [of _ "h(lfp(D,h))"]) |
|
66 apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] ) |
|
67 apply (erule lfp_lemma2) |
|
68 done |
|
69 |
|
70 lemma lfp_eq_Union: |
|
71 "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) = (\<Union>n\<in>nat. h^n(0))" |
|
72 by (blast del: subsetI |
|
73 intro: lfp_subset_Union Union_subset_lfp) |
|
74 |
|
75 |
|
76 subsection {*lists without univ*} |
|
77 |
|
78 lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ |
|
79 Pair_in_univ zero_in_univ |
|
80 |
|
81 lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)" |
|
82 apply (rule bnd_monoI) |
|
83 apply (intro subset_refl zero_subset_univ A_subset_univ |
|
84 sum_subset_univ Sigma_subset_univ) |
|
85 apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI) |
|
86 done |
|
87 |
|
88 lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)" |
|
89 by (simp add: contin_def, blast) |
|
90 |
|
91 text{*Re-expresses lists using sum and product*} |
|
92 lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)" |
|
93 apply (simp add: list_def) |
|
94 apply (rule equalityI) |
|
95 apply (rule lfp_lowerbound) |
|
96 prefer 2 apply (rule lfp_subset) |
|
97 apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono]) |
|
98 apply (simp add: Nil_def Cons_def) |
|
99 apply blast |
|
100 txt{*Opposite inclusion*} |
|
101 apply (rule lfp_lowerbound) |
|
102 prefer 2 apply (rule lfp_subset) |
|
103 apply (clarify, subst lfp_unfold [OF list.bnd_mono]) |
|
104 apply (simp add: Nil_def Cons_def) |
|
105 apply (blast intro: datatype_univs |
|
106 dest: lfp_subset [THEN subsetD]) |
|
107 done |
|
108 |
|
109 text{*Re-expresses lists using "iterates", no univ.*} |
|
110 lemma list_eq_Union: |
|
111 "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))" |
|
112 by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin) |
|
113 |
|
114 |
|
115 subsection {*Absoluteness for "Iterates"*} |
|
116 |
|
117 lemma (in M_trancl) iterates_relativize: |
|
118 "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x)); |
|
119 strong_replacement(M, |
|
120 \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) & |
|
121 is_recfun (Memrel(succ(n)), x, |
|
122 \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) & |
|
123 y = nat_case(v, \<lambda>m. F(g`m), x))|] |
|
124 ==> iterates(F,n,v) = z <-> |
|
125 (\<exists>g[M]. is_recfun(Memrel(succ(n)), n, |
|
126 \<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n), g) & |
|
127 z = nat_case(v, \<lambda>m. F(g`m), n))" |
|
128 by (simp add: iterates_nat_def recursor_def transrec_def |
|
129 eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M |
|
130 wf_Memrel trans_Memrel relation_Memrel nat_case_closed) |
|
131 |
|
132 |
|
133 lemma (in M_wfrank) iterates_closed [intro,simp]: |
|
134 "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x)); |
|
135 strong_replacement(M, |
|
136 \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) & |
|
137 is_recfun (Memrel(succ(n)), x, |
|
138 \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) & |
|
139 y = nat_case(v, \<lambda>m. F(g`m), x))|] |
|
140 ==> M(iterates(F,n,v))" |
|
141 by (simp add: iterates_nat_def recursor_def transrec_def |
|
142 eclose_sing_Ord_eq trans_wfrec_closed nat_into_M |
|
143 wf_Memrel trans_Memrel relation_Memrel nat_case_closed) |
|
144 |
|
145 |
|
146 locale M_datatypes = M_wfrank + |
|
147 (*THEY NEED RELATIVIZATION*) |
|
148 assumes list_replacement1: |
|
149 "[|M(A); n \<in> nat|] ==> |
|
150 strong_replacement(M, |
|
151 \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) & |
|
152 is_recfun (Memrel(succ(n)), x, |
|
153 \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) & |
|
154 y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))" |
|
155 and list_replacement2': |
|
156 "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))" |
|
157 |
|
158 |
|
159 lemma (in M_datatypes) list_replacement1': |
|
160 "[|M(A); n \<in> nat|] |
|
161 ==> strong_replacement |
|
162 (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> & |
|
163 is_recfun (Memrel(succ(n)), x, |
|
164 \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) & |
|
165 z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))" |
|
166 by (insert list_replacement1, simp) |
|
167 |
|
168 |
|
169 lemma (in M_datatypes) list_closed [intro,simp]: |
|
170 "M(A) ==> M(list(A))" |
|
171 by (simp add: list_eq_Union list_replacement1' list_replacement2') |
|
172 |
|
173 end |