src/ZF/Constructible/AC_in_L.thy
changeset 21404 eb85850d3eb7
parent 21233 5a5c8ea5f66a
child 32960 69916a850301
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -223,18 +223,20 @@
     1.4  "DPow(A)"}, we take the minimum such ordinal.*}
     1.5  
     1.6  definition
     1.7 -  env_form_r :: "[i,i,i]=>i"
     1.8 +  env_form_r :: "[i,i,i]=>i" where
     1.9      --{*wellordering on (environment, formula) pairs*}
    1.10     "env_form_r(f,r,A) ==
    1.11        rmult(list(A), rlist(A, r),
    1.12  	    formula, measure(formula, enum(f)))"
    1.13  
    1.14 -  env_form_map :: "[i,i,i,i]=>i"
    1.15 +definition
    1.16 +  env_form_map :: "[i,i,i,i]=>i" where
    1.17      --{*map from (environment, formula) pairs to ordinals*}
    1.18     "env_form_map(f,r,A,z)
    1.19        == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
    1.20  
    1.21 -  DPow_ord :: "[i,i,i,i,i]=>o"
    1.22 +definition
    1.23 +  DPow_ord :: "[i,i,i,i,i]=>o" where
    1.24      --{*predicate that holds if @{term k} is a valid index for @{term X}*}
    1.25     "DPow_ord(f,r,A,X,k) ==
    1.26             \<exists>env \<in> list(A). \<exists>p \<in> formula.
    1.27 @@ -242,11 +244,13 @@
    1.28               X = {x\<in>A. sats(A, p, Cons(x,env))} &
    1.29               env_form_map(f,r,A,<env,p>) = k"
    1.30  
    1.31 -  DPow_least :: "[i,i,i,i]=>i"
    1.32 +definition
    1.33 +  DPow_least :: "[i,i,i,i]=>i" where
    1.34      --{*function yielding the smallest index for @{term X}*}
    1.35     "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
    1.36  
    1.37 -  DPow_r :: "[i,i,i]=>i"
    1.38 +definition
    1.39 +  DPow_r :: "[i,i,i]=>i" where
    1.40      --{*a wellordering on @{term "DPow(A)"}*}
    1.41     "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))"
    1.42  
    1.43 @@ -318,7 +322,7 @@
    1.44  of wellorderings for smaller ordinals.*}
    1.45  
    1.46  definition
    1.47 -  rlimit :: "[i,i=>i]=>i"
    1.48 +  rlimit :: "[i,i=>i]=>i" where
    1.49    --{*Expresses the wellordering at limit ordinals.  The conditional
    1.50        lets us remove the premise @{term "Limit(i)"} from some theorems.*}
    1.51      "rlimit(i,r) ==
    1.52 @@ -329,7 +333,8 @@
    1.53  		  (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
    1.54         else 0"
    1.55  
    1.56 -  Lset_new :: "i=>i"
    1.57 +definition
    1.58 +  Lset_new :: "i=>i" where
    1.59    --{*This constant denotes the set of elements introduced at level
    1.60        @{term "succ(i)"}*}
    1.61      "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
    1.62 @@ -401,7 +406,7 @@
    1.63  subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
    1.64  
    1.65  definition
    1.66 - L_r :: "[i, i] => i"
    1.67 +  L_r :: "[i, i] => i" where
    1.68    "L_r(f) == %i.
    1.69        transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), 
    1.70                  \<lambda>x r. rlimit(x, \<lambda>y. r`y))"