Lots of new results concerning recursive datatypes, towards absoluteness of
authorpaulson
Mon Aug 12 18:01:44 2002 +0200 (2002-08-12)
changeset 134935aa68c051725
parent 13492 6aae8eb39a18
child 13494 1c44289716ae
Lots of new results concerning recursive datatypes, towards absoluteness of
"satisfies"
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Mon Aug 12 17:59:57 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Mon Aug 12 18:01:44 2002 +0200
     1.3 @@ -346,18 +346,109 @@
     1.4    is_list :: "[i=>o,i,i] => o"
     1.5      "is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
     1.6  
     1.7 +subsubsection{*Towards Absoluteness of @{term formula_rec}*}
     1.8 +
     1.9 +consts   depth :: "i=>i"
    1.10 +primrec
    1.11 +  "depth(Member(x,y)) = 0"
    1.12 +  "depth(Equal(x,y))  = 0"
    1.13 +  "depth(Nand(p,q)) = succ(depth(p) \<union> depth(q))"
    1.14 +  "depth(Forall(p)) = succ(depth(p))"
    1.15 +
    1.16 +lemma depth_type [TC]: "p \<in> formula ==> depth(p) \<in> nat"
    1.17 +by (induct_tac p, simp_all) 
    1.18 +
    1.19 +
    1.20  constdefs
    1.21 -  is_formula_n :: "[i=>o,i,i] => o"
    1.22 -    "is_formula_n(M,n,Z) == 
    1.23 +  formula_N :: "i => i"
    1.24 +    "formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
    1.25 +
    1.26 +lemma Member_in_formula_N [simp]:
    1.27 +     "Member(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"
    1.28 +by (simp add: formula_N_def Member_def) 
    1.29 +
    1.30 +lemma Equal_in_formula_N [simp]:
    1.31 +     "Equal(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"
    1.32 +by (simp add: formula_N_def Equal_def) 
    1.33 +
    1.34 +lemma Nand_in_formula_N [simp]:
    1.35 +     "Nand(x,y) \<in> formula_N(succ(n)) <-> x \<in> formula_N(n) & y \<in> formula_N(n)"
    1.36 +by (simp add: formula_N_def Nand_def) 
    1.37 +
    1.38 +lemma Forall_in_formula_N [simp]:
    1.39 +     "Forall(x) \<in> formula_N(succ(n)) <-> x \<in> formula_N(n)"
    1.40 +by (simp add: formula_N_def Forall_def) 
    1.41 +
    1.42 +text{*These two aren't simprules because they reveal the underlying
    1.43 +formula representation.*}
    1.44 +lemma formula_N_0: "formula_N(0) = 0"
    1.45 +by (simp add: formula_N_def)
    1.46 +
    1.47 +lemma formula_N_succ:
    1.48 +     "formula_N(succ(n)) = 
    1.49 +      ((nat*nat) + (nat*nat)) + (formula_N(n) * formula_N(n) + formula_N(n))"
    1.50 +by (simp add: formula_N_def)
    1.51 +
    1.52 +lemma formula_N_imp_formula:
    1.53 +  "[| p \<in> formula_N(n); n \<in> nat |] ==> p \<in> formula"
    1.54 +by (force simp add: formula_eq_Union formula_N_def)
    1.55 +
    1.56 +lemma formula_N_imp_depth_lt [rule_format]:
    1.57 +     "n \<in> nat ==> \<forall>p \<in> formula_N(n). depth(p) < n"
    1.58 +apply (induct_tac n)  
    1.59 +apply (auto simp add: formula_N_0 formula_N_succ 
    1.60 +                      depth_type formula_N_imp_formula Un_least_lt_iff
    1.61 +                      Member_def [symmetric] Equal_def [symmetric]
    1.62 +                      Nand_def [symmetric] Forall_def [symmetric]) 
    1.63 +done
    1.64 +
    1.65 +lemma formula_imp_formula_N [rule_format]:
    1.66 +     "p \<in> formula ==> \<forall>n\<in>nat. depth(p) < n --> p \<in> formula_N(n)"
    1.67 +apply (induct_tac p)
    1.68 +apply (simp_all add: succ_Un_distrib Un_least_lt_iff) 
    1.69 +apply (force elim: natE)+
    1.70 +done
    1.71 +
    1.72 +lemma formula_N_imp_eq_depth:
    1.73 +      "[|n \<in> nat; p \<notin> formula_N(n); p \<in> formula_N(succ(n))|] 
    1.74 +       ==> n = depth(p)"
    1.75 +apply (rule le_anti_sym) 
    1.76 + prefer 2 apply (simp add: formula_N_imp_depth_lt) 
    1.77 +apply (frule formula_N_imp_formula, simp)
    1.78 +apply (simp add: not_lt_iff_le [symmetric]) 
    1.79 +apply (blast intro: formula_imp_formula_N) 
    1.80 +done
    1.81 +
    1.82 +
    1.83 +
    1.84 +lemma formula_N_mono [rule_format]:
    1.85 +  "[| m \<in> nat; n \<in> nat |] ==> m\<le>n --> formula_N(m) \<subseteq> formula_N(n)"
    1.86 +apply (rule_tac m = m and n = n in diff_induct)
    1.87 +apply (simp_all add: formula_N_0 formula_N_succ, blast) 
    1.88 +done
    1.89 +
    1.90 +lemma formula_N_distrib:
    1.91 +  "[| m \<in> nat; n \<in> nat |] ==> formula_N(m \<union> n) = formula_N(m) \<union> formula_N(n)"
    1.92 +apply (rule_tac i = m and j = n in Ord_linear_le, auto) 
    1.93 +apply (simp_all add: subset_Un_iff [THEN iffD1] subset_Un_iff2 [THEN iffD1] 
    1.94 +                     le_imp_subset formula_N_mono)
    1.95 +done
    1.96 +
    1.97 +constdefs
    1.98 +  is_formula_N :: "[i=>o,i,i] => o"
    1.99 +    "is_formula_N(M,n,Z) == 
   1.100        \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
   1.101         empty(M,zero) & 
   1.102         successor(M,n,sn) & membership(M,sn,msn) &
   1.103         is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
   1.104    
   1.105 +
   1.106 +constdefs
   1.107 +  
   1.108    mem_formula :: "[i=>o,i] => o"
   1.109      "mem_formula(M,p) == 
   1.110        \<exists>n[M]. \<exists>formn[M]. 
   1.111 -       finite_ordinal(M,n) & is_formula_n(M,n,formn) & p \<in> formn"
   1.112 +       finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn"
   1.113  
   1.114    is_formula :: "[i=>o,i] => o"
   1.115      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
   1.116 @@ -451,20 +542,26 @@
   1.117  
   1.118  lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]
   1.119  
   1.120 -lemma (in M_datatypes) is_formula_n_abs [simp]:
   1.121 +lemma (in M_datatypes) formula_N_abs [simp]:
   1.122       "[|n\<in>nat; M(Z)|] 
   1.123 -      ==> is_formula_n(M,n,Z) <-> 
   1.124 -          Z = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0)"
   1.125 +      ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
   1.126  apply (insert formula_replacement1)
   1.127 -apply (simp add: is_formula_n_def relativize1_def nat_into_M
   1.128 +apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.129                   iterates_abs [of "is_formula_functor(M)" _ 
   1.130 -                        "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.131 +                                  "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.132 +done
   1.133 +
   1.134 +lemma (in M_datatypes) formula_N_closed [intro,simp]:
   1.135 +     "n\<in>nat ==> M(formula_N(n))"
   1.136 +apply (insert formula_replacement1)
   1.137 +apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.138 +                 iterates_closed [of "is_formula_functor(M)"])
   1.139  done
   1.140  
   1.141  lemma (in M_datatypes) mem_formula_abs [simp]:
   1.142       "mem_formula(M,l) <-> l \<in> formula"
   1.143  apply (insert formula_replacement1)
   1.144 -apply (simp add: mem_formula_def relativize1_def formula_eq_Union
   1.145 +apply (simp add: mem_formula_def relativize1_def formula_eq_Union formula_N_def
   1.146                   iterates_closed [of "is_formula_functor(M)"]) 
   1.147  done
   1.148  
   1.149 @@ -739,11 +836,13 @@
   1.150      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   1.151    --{*no constraint on non-formulas*}
   1.152    "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
   1.153 -      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,p) --> is_a(x,y,z)) &
   1.154 -      (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,p) --> is_b(x,y,z)) &
   1.155 -      (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> 
   1.156 +      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> 
   1.157 +                      is_Member(M,x,y,p) --> is_a(x,y,z)) &
   1.158 +      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> 
   1.159 +                      is_Equal(M,x,y,p) --> is_b(x,y,z)) &
   1.160 +      (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) --> 
   1.161                       is_Nand(M,x,y,p) --> is_c(x,y,z)) &
   1.162 -      (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,p) --> is_d(x,z))"
   1.163 +      (\<forall>x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))"
   1.164  
   1.165  lemma (in M_datatypes) formula_case_abs [simp]: 
   1.166       "[| Relativize2(M,nat,nat,is_a,a); Relativize2(M,nat,nat,is_b,b); 
   1.167 @@ -872,94 +971,6 @@
   1.168  done
   1.169  
   1.170  
   1.171 -subsubsection{*Towards Absoluteness of @{term formula_rec}*}
   1.172 -
   1.173 -consts   depth :: "i=>i"
   1.174 -primrec
   1.175 -  "depth(Member(x,y)) = 0"
   1.176 -  "depth(Equal(x,y))  = 0"
   1.177 -  "depth(Nand(p,q)) = succ(depth(p) \<union> depth(q))"
   1.178 -  "depth(Forall(p)) = succ(depth(p))"
   1.179 -
   1.180 -lemma depth_type [TC]: "p \<in> formula ==> depth(p) \<in> nat"
   1.181 -by (induct_tac p, simp_all) 
   1.182 -
   1.183 -
   1.184 -constdefs
   1.185 -  formula_N :: "i => i"
   1.186 -    "formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
   1.187 -
   1.188 -lemma Member_in_formula_N [simp]:
   1.189 -     "Member(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"
   1.190 -by (simp add: formula_N_def Member_def) 
   1.191 -
   1.192 -lemma Equal_in_formula_N [simp]:
   1.193 -     "Equal(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"
   1.194 -by (simp add: formula_N_def Equal_def) 
   1.195 -
   1.196 -lemma Nand_in_formula_N [simp]:
   1.197 -     "Nand(x,y) \<in> formula_N(succ(n)) <-> x \<in> formula_N(n) & y \<in> formula_N(n)"
   1.198 -by (simp add: formula_N_def Nand_def) 
   1.199 -
   1.200 -lemma Forall_in_formula_N [simp]:
   1.201 -     "Forall(x) \<in> formula_N(succ(n)) <-> x \<in> formula_N(n)"
   1.202 -by (simp add: formula_N_def Forall_def) 
   1.203 -
   1.204 -text{*These two aren't simprules because they reveal the underlying
   1.205 -formula representation.*}
   1.206 -lemma formula_N_0: "formula_N(0) = 0"
   1.207 -by (simp add: formula_N_def)
   1.208 -
   1.209 -lemma formula_N_succ:
   1.210 -     "formula_N(succ(n)) = 
   1.211 -      ((nat*nat) + (nat*nat)) + (formula_N(n) * formula_N(n) + formula_N(n))"
   1.212 -by (simp add: formula_N_def)
   1.213 -
   1.214 -lemma formula_N_imp_formula:
   1.215 -  "[| p \<in> formula_N(n); n \<in> nat |] ==> p \<in> formula"
   1.216 -by (force simp add: formula_eq_Union formula_N_def)
   1.217 -
   1.218 -lemma formula_N_imp_depth_lt [rule_format]:
   1.219 -     "n \<in> nat ==> \<forall>p \<in> formula_N(n). depth(p) < n"
   1.220 -apply (induct_tac n)  
   1.221 -apply (auto simp add: formula_N_0 formula_N_succ 
   1.222 -                      depth_type formula_N_imp_formula Un_least_lt_iff
   1.223 -                      Member_def [symmetric] Equal_def [symmetric]
   1.224 -                      Nand_def [symmetric] Forall_def [symmetric]) 
   1.225 -done
   1.226 -
   1.227 -lemma formula_imp_formula_N [rule_format]:
   1.228 -     "p \<in> formula ==> \<forall>n\<in>nat. depth(p) < n --> p \<in> formula_N(n)"
   1.229 -apply (induct_tac p)
   1.230 -apply (simp_all add: succ_Un_distrib Un_least_lt_iff) 
   1.231 -apply (force elim: natE)+
   1.232 -done
   1.233 -
   1.234 -lemma formula_N_imp_eq_depth:
   1.235 -      "[|n \<in> nat; p \<notin> formula_N(n); p \<in> formula_N(succ(n))|] 
   1.236 -       ==> n = depth(p)"
   1.237 -apply (rule le_anti_sym) 
   1.238 - prefer 2 apply (simp add: formula_N_imp_depth_lt) 
   1.239 -apply (frule formula_N_imp_formula, simp)
   1.240 -apply (simp add: not_lt_iff_le [symmetric]) 
   1.241 -apply (blast intro: formula_imp_formula_N) 
   1.242 -done
   1.243 -
   1.244 -
   1.245 -
   1.246 -lemma formula_N_mono [rule_format]:
   1.247 -  "[| m \<in> nat; n \<in> nat |] ==> m\<le>n --> formula_N(m) \<subseteq> formula_N(n)"
   1.248 -apply (rule_tac m = m and n = n in diff_induct)
   1.249 -apply (simp_all add: formula_N_0 formula_N_succ, blast) 
   1.250 -done
   1.251 -
   1.252 -lemma formula_N_distrib:
   1.253 -  "[| m \<in> nat; n \<in> nat |] ==> formula_N(m \<union> n) = formula_N(m) \<union> formula_N(n)"
   1.254 -apply (rule_tac i = m and j = n in Ord_linear_le, auto) 
   1.255 -apply (simp_all add: subset_Un_iff [THEN iffD1] subset_Un_iff2 [THEN iffD1] 
   1.256 -                     le_imp_subset formula_N_mono)
   1.257 -done
   1.258 -
   1.259  text{*Express @{term formula_rec} without using @{term rank} or @{term Vset},
   1.260  neither of which is absolute.*}
   1.261  lemma (in M_triv_axioms) formula_rec_eq:
   1.262 @@ -986,31 +997,6 @@
   1.263  done
   1.264  
   1.265  
   1.266 -constdefs
   1.267 -  is_formula_N :: "[i=>o,i,i] => o"
   1.268 -    "is_formula_N(M,n,Z) == 
   1.269 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
   1.270 -       empty(M,zero) & 
   1.271 -       successor(M,n,sn) & membership(M,sn,msn) &
   1.272 -       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
   1.273 -  
   1.274 -
   1.275 -lemma (in M_datatypes) formula_N_abs [simp]:
   1.276 -     "[|n\<in>nat; M(Z)|] 
   1.277 -      ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
   1.278 -apply (insert formula_replacement1)
   1.279 -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.280 -                 iterates_abs [of "is_formula_functor(M)" _ 
   1.281 -                                  "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.282 -done
   1.283 -
   1.284 -lemma (in M_datatypes) formula_N_closed [intro,simp]:
   1.285 -     "n\<in>nat ==> M(formula_N(n))"
   1.286 -apply (insert formula_replacement1)
   1.287 -apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.288 -                 iterates_closed [of "is_formula_functor(M)"])
   1.289 -done
   1.290 -
   1.291  subsection{*Absoluteness for the Formula Operator @{term depth}*}
   1.292  constdefs
   1.293  
   1.294 @@ -1035,4 +1021,5 @@
   1.295       "p \<in> formula ==> M(depth(p))"
   1.296  by (simp add: nat_into_M) 
   1.297  
   1.298 +
   1.299  end
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Aug 12 17:59:57 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Aug 12 18:01:44 2002 +0200
     2.3 @@ -1464,6 +1464,41 @@
     2.4               empty_reflection successor_reflection)
     2.5  done
     2.6  
     2.7 +subsubsection{*Finite Ordinals: The Predicate ``Is A Natural Number''*}
     2.8 +
     2.9 +(*     "finite_ordinal(M,a) == 
    2.10 +	ordinal(M,a) & ~ limit_ordinal(M,a) & 
    2.11 +        (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
    2.12 +constdefs finite_ordinal_fm :: "i=>i"
    2.13 +    "finite_ordinal_fm(x) ==
    2.14 +       And(ordinal_fm(x),
    2.15 +          And(Neg(limit_ordinal_fm(x)),
    2.16 +           Forall(Implies(Member(0,succ(x)),
    2.17 +                          Neg(limit_ordinal_fm(0))))))"
    2.18 +
    2.19 +lemma finite_ordinal_type [TC]:
    2.20 +     "x \<in> nat ==> finite_ordinal_fm(x) \<in> formula"
    2.21 +by (simp add: finite_ordinal_fm_def)
    2.22 +
    2.23 +lemma sats_finite_ordinal_fm [simp]:
    2.24 +   "[| x \<in> nat; env \<in> list(A)|]
    2.25 +    ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(**A, nth(x,env))"
    2.26 +by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def)
    2.27 +
    2.28 +lemma finite_ordinal_iff_sats:
    2.29 +      "[| nth(i,env) = x; nth(j,env) = y;
    2.30 +          i \<in> nat; env \<in> list(A)|]
    2.31 +       ==> finite_ordinal(**A, x) <-> sats(A, finite_ordinal_fm(i), env)"
    2.32 +by simp
    2.33 +
    2.34 +theorem finite_ordinal_reflection:
    2.35 +     "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
    2.36 +               \<lambda>i x. finite_ordinal(**Lset(i),f(x))]"
    2.37 +apply (simp only: finite_ordinal_def setclass_simps)
    2.38 +apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
    2.39 +done
    2.40 +
    2.41 +
    2.42  subsubsection{*Omega: The Set of Natural Numbers*}
    2.43  
    2.44  (* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Aug 12 17:59:57 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Aug 12 18:01:44 2002 +0200
     3.3 @@ -16,6 +16,7 @@
     3.4  lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
     3.5  by simp
     3.6  
     3.7 +
     3.8  subsection{*The Locale @{text "M_trancl"}*}
     3.9  
    3.10  subsubsection{*Separation for Reflexive/Transitive Closure*}
    3.11 @@ -1264,14 +1265,31 @@
    3.12         2       1       0
    3.13         successor(M,n,sn) & membership(M,sn,msn) &
    3.14         is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
    3.15 -       is_hd(M,X,Z)"
    3.16 +       is_hd(M,X,Z)" *)
    3.17  constdefs nth_fm :: "[i,i,i]=>i"
    3.18      "nth_fm(n,l,Z) == 
    3.19         Exists(Exists(Exists(
    3.20 -         And(successor_fm(n#+3,1),
    3.21 -          And(membership_fm(1,0),
    3.22 -           And(
    3.23 - *)
    3.24 +         And(succ_fm(n#+3,1),
    3.25 +          And(Memrel_fm(1,0),
    3.26 +           And(is_wfrec_fm(iterates_MH_fm(tl_fm(1,0),l#+8,2,1,0), 0, n#+3, 2), hd_fm(2,Z#+3)))))))"
    3.27 +
    3.28 +lemma nth_fm_type [TC]:
    3.29 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> nth_fm(x,y,z) \<in> formula"
    3.30 +by (simp add: nth_fm_def)
    3.31 +
    3.32 +lemma sats_nth_fm [simp]:
    3.33 +   "[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
    3.34 +    ==> sats(A, nth_fm(x,y,z), env) <->
    3.35 +        is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
    3.36 +apply (frule lt_length_in_nat, assumption)  
    3.37 +apply (simp add: nth_fm_def is_nth_def sats_is_wfrec_fm sats_iterates_MH_fm) 
    3.38 +done
    3.39 +
    3.40 +lemma nth_iff_sats:
    3.41 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
    3.42 +          i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
    3.43 +       ==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
    3.44 +by (simp add: sats_nth_fm)
    3.45  
    3.46  theorem nth_reflection:
    3.47       "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),