231 (environment, formula) pairs into the ordinals. For each member of @{term |
231 (environment, formula) pairs into the ordinals. For each member of @{term |
232 "DPow(A)"}, we take the minimum such ordinal.\<close> |
232 "DPow(A)"}, we take the minimum such ordinal.\<close> |
233 |
233 |
234 definition |
234 definition |
235 env_form_r :: "[i,i,i]=>i" where |
235 env_form_r :: "[i,i,i]=>i" where |
236 \<comment>\<open>wellordering on (environment, formula) pairs\<close> |
236 \<comment> \<open>wellordering on (environment, formula) pairs\<close> |
237 "env_form_r(f,r,A) == |
237 "env_form_r(f,r,A) == |
238 rmult(list(A), rlist(A, r), |
238 rmult(list(A), rlist(A, r), |
239 formula, measure(formula, enum(f)))" |
239 formula, measure(formula, enum(f)))" |
240 |
240 |
241 definition |
241 definition |
242 env_form_map :: "[i,i,i,i]=>i" where |
242 env_form_map :: "[i,i,i,i]=>i" where |
243 \<comment>\<open>map from (environment, formula) pairs to ordinals\<close> |
243 \<comment> \<open>map from (environment, formula) pairs to ordinals\<close> |
244 "env_form_map(f,r,A,z) |
244 "env_form_map(f,r,A,z) |
245 == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" |
245 == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" |
246 |
246 |
247 definition |
247 definition |
248 DPow_ord :: "[i,i,i,i,i]=>o" where |
248 DPow_ord :: "[i,i,i,i,i]=>o" where |
249 \<comment>\<open>predicate that holds if @{term k} is a valid index for @{term X}\<close> |
249 \<comment> \<open>predicate that holds if @{term k} is a valid index for @{term X}\<close> |
250 "DPow_ord(f,r,A,X,k) == |
250 "DPow_ord(f,r,A,X,k) == |
251 \<exists>env \<in> list(A). \<exists>p \<in> formula. |
251 \<exists>env \<in> list(A). \<exists>p \<in> formula. |
252 arity(p) \<le> succ(length(env)) & |
252 arity(p) \<le> succ(length(env)) & |
253 X = {x\<in>A. sats(A, p, Cons(x,env))} & |
253 X = {x\<in>A. sats(A, p, Cons(x,env))} & |
254 env_form_map(f,r,A,<env,p>) = k" |
254 env_form_map(f,r,A,<env,p>) = k" |
255 |
255 |
256 definition |
256 definition |
257 DPow_least :: "[i,i,i,i]=>i" where |
257 DPow_least :: "[i,i,i,i]=>i" where |
258 \<comment>\<open>function yielding the smallest index for @{term X}\<close> |
258 \<comment> \<open>function yielding the smallest index for @{term X}\<close> |
259 "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" |
259 "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" |
260 |
260 |
261 definition |
261 definition |
262 DPow_r :: "[i,i,i]=>i" where |
262 DPow_r :: "[i,i,i]=>i" where |
263 \<comment>\<open>a wellordering on @{term "DPow(A)"}\<close> |
263 \<comment> \<open>a wellordering on @{term "DPow(A)"}\<close> |
264 "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" |
264 "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" |
265 |
265 |
266 |
266 |
267 lemma (in Nat_Times_Nat) well_ord_env_form_r: |
267 lemma (in Nat_Times_Nat) well_ord_env_form_r: |
268 "well_ord(A,r) |
268 "well_ord(A,r) |