src/ZF/Constructible/AC_in_L.thy
changeset 67443 3abf6a722518
parent 61798 27f3c10b0b50
child 69593 3dda49e08b9d
equal deleted inserted replaced
67442:f075640b8868 67443:3abf6a722518
   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)
   330 @{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
   330 @{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
   331 of wellorderings for smaller ordinals.\<close>
   331 of wellorderings for smaller ordinals.\<close>
   332 
   332 
   333 definition
   333 definition
   334   rlimit :: "[i,i=>i]=>i" where
   334   rlimit :: "[i,i=>i]=>i" where
   335   \<comment>\<open>Expresses the wellordering at limit ordinals.  The conditional
   335   \<comment> \<open>Expresses the wellordering at limit ordinals.  The conditional
   336       lets us remove the premise @{term "Limit(i)"} from some theorems.\<close>
   336       lets us remove the premise @{term "Limit(i)"} from some theorems.\<close>
   337     "rlimit(i,r) ==
   337     "rlimit(i,r) ==
   338        if Limit(i) then 
   338        if Limit(i) then 
   339          {z: Lset(i) * Lset(i).
   339          {z: Lset(i) * Lset(i).
   340           \<exists>x' x. z = <x',x> &
   340           \<exists>x' x. z = <x',x> &
   342                   (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
   342                   (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
   343        else 0"
   343        else 0"
   344 
   344 
   345 definition
   345 definition
   346   Lset_new :: "i=>i" where
   346   Lset_new :: "i=>i" where
   347   \<comment>\<open>This constant denotes the set of elements introduced at level
   347   \<comment> \<open>This constant denotes the set of elements introduced at level
   348       @{term "succ(i)"}\<close>
   348       @{term "succ(i)"}\<close>
   349     "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
   349     "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
   350 
   350 
   351 lemma Limit_Lset_eq2:
   351 lemma Limit_Lset_eq2:
   352     "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))"
   352     "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))"