src/ZF/Constructible/L_axioms.thy
author paulson
Wed Aug 21 15:57:24 2002 +0200 (2002-08-21)
changeset 13513 b9e14471629c
parent 13506 acc18a5d2b1a
child 13563 7d6c9817c432
permissions -rw-r--r--
tweaks
     1 (*  Title:      ZF/Constructible/L_axioms.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2002  University of Cambridge
     5 *)
     6 
     7 header {* The ZF Axioms (Except Separation) in L *}
     8 
     9 theory L_axioms = Formula + Relative + Reflection + MetaExists:
    10 
    11 text {* The class L satisfies the premises of locale @{text M_triv_axioms} *}
    12 
    13 lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
    14 apply (insert Transset_Lset)
    15 apply (simp add: Transset_def L_def, blast)
    16 done
    17 
    18 lemma nonempty: "L(0)"
    19 apply (simp add: L_def)
    20 apply (blast intro: zero_in_Lset)
    21 done
    22 
    23 lemma upair_ax: "upair_ax(L)"
    24 apply (simp add: upair_ax_def upair_def, clarify)
    25 apply (rule_tac x="{x,y}" in rexI)
    26 apply (simp_all add: doubleton_in_L)
    27 done
    28 
    29 lemma Union_ax: "Union_ax(L)"
    30 apply (simp add: Union_ax_def big_union_def, clarify)
    31 apply (rule_tac x="Union(x)" in rexI)
    32 apply (simp_all add: Union_in_L, auto)
    33 apply (blast intro: transL)
    34 done
    35 
    36 lemma power_ax: "power_ax(L)"
    37 apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
    38 apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)
    39 apply (simp_all add: LPow_in_L, auto)
    40 apply (blast intro: transL)
    41 done
    42 
    43 subsection{*For L to satisfy Replacement *}
    44 
    45 (*Can't move these to Formula unless the definition of univalent is moved
    46 there too!*)
    47 
    48 lemma LReplace_in_Lset:
    49      "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|]
    50       ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
    51 apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"
    52        in exI)
    53 apply simp
    54 apply clarify
    55 apply (rule_tac a=x in UN_I)
    56  apply (simp_all add: Replace_iff univalent_def)
    57 apply (blast dest: transL L_I)
    58 done
    59 
    60 lemma LReplace_in_L:
    61      "[|L(X); univalent(L,X,Q)|]
    62       ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
    63 apply (drule L_D, clarify)
    64 apply (drule LReplace_in_Lset, assumption+)
    65 apply (blast intro: L_I Lset_in_Lset_succ)
    66 done
    67 
    68 lemma replacement: "replacement(L,P)"
    69 apply (simp add: replacement_def, clarify)
    70 apply (frule LReplace_in_L, assumption+, clarify)
    71 apply (rule_tac x=Y in rexI)
    72 apply (simp_all add: Replace_iff univalent_def, blast)
    73 done
    74 
    75 subsection{*Instantiating the locale @{text M_triv_axioms}*}
    76 text{*No instances of Separation yet.*}
    77 
    78 lemma Lset_mono_le: "mono_le_subset(Lset)"
    79 by (simp add: mono_le_subset_def le_imp_subset Lset_mono)
    80 
    81 lemma Lset_cont: "cont_Ord(Lset)"
    82 by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)
    83 
    84 lemmas Pair_in_Lset = Formula.Pair_in_LLimit
    85 
    86 lemmas L_nat = Ord_in_L [OF Ord_nat]
    87 
    88 theorem M_triv_axioms_L: "PROP M_triv_axioms(L)"
    89   apply (rule M_triv_axioms.intro)
    90         apply (erule (1) transL)
    91        apply (rule nonempty)
    92       apply (rule upair_ax)
    93      apply (rule Union_ax)
    94     apply (rule power_ax)
    95    apply (rule replacement)
    96   apply (rule L_nat)
    97   done
    98 
    99 lemmas rall_abs = M_triv_axioms.rall_abs [OF M_triv_axioms_L]
   100   and rex_abs = M_triv_axioms.rex_abs [OF M_triv_axioms_L]
   101   and ball_iff_equiv = M_triv_axioms.ball_iff_equiv [OF M_triv_axioms_L]
   102   and M_equalityI = M_triv_axioms.M_equalityI [OF M_triv_axioms_L]
   103   and empty_abs = M_triv_axioms.empty_abs [OF M_triv_axioms_L]
   104   and subset_abs = M_triv_axioms.subset_abs [OF M_triv_axioms_L]
   105   and upair_abs = M_triv_axioms.upair_abs [OF M_triv_axioms_L]
   106   and upair_in_M_iff = M_triv_axioms.upair_in_M_iff [OF M_triv_axioms_L]
   107   and singleton_in_M_iff = M_triv_axioms.singleton_in_M_iff [OF M_triv_axioms_L]
   108   and pair_abs = M_triv_axioms.pair_abs [OF M_triv_axioms_L]
   109   and pair_in_M_iff = M_triv_axioms.pair_in_M_iff [OF M_triv_axioms_L]
   110   and pair_components_in_M = M_triv_axioms.pair_components_in_M [OF M_triv_axioms_L]
   111   and cartprod_abs = M_triv_axioms.cartprod_abs [OF M_triv_axioms_L]
   112   and union_abs = M_triv_axioms.union_abs [OF M_triv_axioms_L]
   113   and inter_abs = M_triv_axioms.inter_abs [OF M_triv_axioms_L]
   114   and setdiff_abs = M_triv_axioms.setdiff_abs [OF M_triv_axioms_L]
   115   and Union_abs = M_triv_axioms.Union_abs [OF M_triv_axioms_L]
   116   and Union_closed = M_triv_axioms.Union_closed [OF M_triv_axioms_L]
   117   and Un_closed = M_triv_axioms.Un_closed [OF M_triv_axioms_L]
   118   and cons_closed = M_triv_axioms.cons_closed [OF M_triv_axioms_L]
   119   and successor_abs = M_triv_axioms.successor_abs [OF M_triv_axioms_L]
   120   and succ_in_M_iff = M_triv_axioms.succ_in_M_iff [OF M_triv_axioms_L]
   121   and separation_closed = M_triv_axioms.separation_closed [OF M_triv_axioms_L]
   122   and strong_replacementI = M_triv_axioms.strong_replacementI [OF M_triv_axioms_L]
   123   and strong_replacement_closed = M_triv_axioms.strong_replacement_closed [OF M_triv_axioms_L]
   124   and RepFun_closed = M_triv_axioms.RepFun_closed [OF M_triv_axioms_L]
   125   and lam_closed = M_triv_axioms.lam_closed [OF M_triv_axioms_L]
   126   and image_abs = M_triv_axioms.image_abs [OF M_triv_axioms_L]
   127   and powerset_Pow = M_triv_axioms.powerset_Pow [OF M_triv_axioms_L]
   128   and powerset_imp_subset_Pow = M_triv_axioms.powerset_imp_subset_Pow [OF M_triv_axioms_L]
   129   and nat_into_M = M_triv_axioms.nat_into_M [OF M_triv_axioms_L]
   130   and nat_case_closed = M_triv_axioms.nat_case_closed [OF M_triv_axioms_L]
   131   and Inl_in_M_iff = M_triv_axioms.Inl_in_M_iff [OF M_triv_axioms_L]
   132   and Inr_in_M_iff = M_triv_axioms.Inr_in_M_iff [OF M_triv_axioms_L]
   133   and lt_closed = M_triv_axioms.lt_closed [OF M_triv_axioms_L]
   134   and transitive_set_abs = M_triv_axioms.transitive_set_abs [OF M_triv_axioms_L]
   135   and ordinal_abs = M_triv_axioms.ordinal_abs [OF M_triv_axioms_L]
   136   and limit_ordinal_abs = M_triv_axioms.limit_ordinal_abs [OF M_triv_axioms_L]
   137   and successor_ordinal_abs = M_triv_axioms.successor_ordinal_abs [OF M_triv_axioms_L]
   138   and finite_ordinal_abs = M_triv_axioms.finite_ordinal_abs [OF M_triv_axioms_L]
   139   and omega_abs = M_triv_axioms.omega_abs [OF M_triv_axioms_L]
   140   and number1_abs = M_triv_axioms.number1_abs [OF M_triv_axioms_L]
   141   and number2_abs = M_triv_axioms.number2_abs [OF M_triv_axioms_L]
   142   and number3_abs = M_triv_axioms.number3_abs [OF M_triv_axioms_L]
   143 
   144 declare rall_abs [simp]
   145 declare rex_abs [simp]
   146 declare empty_abs [simp]
   147 declare subset_abs [simp]
   148 declare upair_abs [simp]
   149 declare upair_in_M_iff [iff]
   150 declare singleton_in_M_iff [iff]
   151 declare pair_abs [simp]
   152 declare pair_in_M_iff [iff]
   153 declare cartprod_abs [simp]
   154 declare union_abs [simp]
   155 declare inter_abs [simp]
   156 declare setdiff_abs [simp]
   157 declare Union_abs [simp]
   158 declare Union_closed [intro, simp]
   159 declare Un_closed [intro, simp]
   160 declare cons_closed [intro, simp]
   161 declare successor_abs [simp]
   162 declare succ_in_M_iff [iff]
   163 declare separation_closed [intro, simp]
   164 declare strong_replacementI
   165 declare strong_replacement_closed [intro, simp]
   166 declare RepFun_closed [intro, simp]
   167 declare lam_closed [intro, simp]
   168 declare image_abs [simp]
   169 declare nat_into_M [intro]
   170 declare Inl_in_M_iff [iff]
   171 declare Inr_in_M_iff [iff]
   172 declare transitive_set_abs [simp]
   173 declare ordinal_abs [simp]
   174 declare limit_ordinal_abs [simp]
   175 declare successor_ordinal_abs [simp]
   176 declare finite_ordinal_abs [simp]
   177 declare omega_abs [simp]
   178 declare number1_abs [simp]
   179 declare number2_abs [simp]
   180 declare number3_abs [simp]
   181 
   182 
   183 subsection{*Instantiation of the locale @{text reflection}*}
   184 
   185 text{*instances of locale constants*}
   186 constdefs
   187   L_F0 :: "[i=>o,i] => i"
   188     "L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
   189 
   190   L_FF :: "[i=>o,i] => i"
   191     "L_FF(P)   == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
   192 
   193   L_ClEx :: "[i=>o,i] => o"
   194     "L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a"
   195 
   196 
   197 text{*We must use the meta-existential quantifier; otherwise the reflection
   198       terms become enormous!*}
   199 constdefs
   200   L_Reflects :: "[i=>o,[i,i]=>o] => prop"      ("(3REFLECTS/ [_,/ _])")
   201     "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
   202                            (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x))))"
   203 
   204 
   205 theorem Triv_reflection:
   206      "REFLECTS[P, \<lambda>a x. P(x)]"
   207 apply (simp add: L_Reflects_def)
   208 apply (rule meta_exI)
   209 apply (rule Closed_Unbounded_Ord)
   210 done
   211 
   212 theorem Not_reflection:
   213      "REFLECTS[P,Q] ==> REFLECTS[\<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x)]"
   214 apply (unfold L_Reflects_def)
   215 apply (erule meta_exE)
   216 apply (rule_tac x=Cl in meta_exI, simp)
   217 done
   218 
   219 theorem And_reflection:
   220      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
   221       ==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"
   222 apply (unfold L_Reflects_def)
   223 apply (elim meta_exE)
   224 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
   225 apply (simp add: Closed_Unbounded_Int, blast)
   226 done
   227 
   228 theorem Or_reflection:
   229      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
   230       ==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"
   231 apply (unfold L_Reflects_def)
   232 apply (elim meta_exE)
   233 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
   234 apply (simp add: Closed_Unbounded_Int, blast)
   235 done
   236 
   237 theorem Imp_reflection:
   238      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
   239       ==> REFLECTS[\<lambda>x. P(x) --> P'(x), \<lambda>a x. Q(a,x) --> Q'(a,x)]"
   240 apply (unfold L_Reflects_def)
   241 apply (elim meta_exE)
   242 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
   243 apply (simp add: Closed_Unbounded_Int, blast)
   244 done
   245 
   246 theorem Iff_reflection:
   247      "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |]
   248       ==> REFLECTS[\<lambda>x. P(x) <-> P'(x), \<lambda>a x. Q(a,x) <-> Q'(a,x)]"
   249 apply (unfold L_Reflects_def)
   250 apply (elim meta_exE)
   251 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
   252 apply (simp add: Closed_Unbounded_Int, blast)
   253 done
   254 
   255 
   256 lemma reflection_Lset: "reflection(Lset)"
   257 apply (blast intro: reflection.intro Lset_mono_le Lset_cont Pair_in_Lset) +
   258 done
   259 
   260 theorem Ex_reflection:
   261      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   262       ==> REFLECTS[\<lambda>x. \<exists>z. L(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
   263 apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
   264 apply (elim meta_exE)
   265 apply (rule meta_exI)
   266 apply (erule reflection.Ex_reflection [OF reflection_Lset])
   267 done
   268 
   269 theorem All_reflection:
   270      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   271       ==> REFLECTS[\<lambda>x. \<forall>z. L(z) --> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
   272 apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
   273 apply (elim meta_exE)
   274 apply (rule meta_exI)
   275 apply (erule reflection.All_reflection [OF reflection_Lset])
   276 done
   277 
   278 theorem Rex_reflection:
   279      "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   280       ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
   281 apply (unfold rex_def)
   282 apply (intro And_reflection Ex_reflection, assumption)
   283 done
   284 
   285 theorem Rall_reflection:
   286      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   287       ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
   288 apply (unfold rall_def)
   289 apply (intro Imp_reflection All_reflection, assumption)
   290 done
   291 
   292 text{*This version handles an alternative form of the bounded quantifier
   293       in the second argument of @{text REFLECTS}.*}
   294 theorem Rex_reflection':
   295      "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   296       ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]"
   297 apply (unfold setclass_def rex_def)
   298 apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
   299 done
   300 
   301 text{*As above.*}
   302 theorem Rall_reflection':
   303      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
   304       ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]"
   305 apply (unfold setclass_def rall_def)
   306 apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
   307 done
   308 
   309 lemmas FOL_reflections =
   310         Triv_reflection Not_reflection And_reflection Or_reflection
   311         Imp_reflection Iff_reflection Ex_reflection All_reflection
   312         Rex_reflection Rall_reflection Rex_reflection' Rall_reflection'
   313 
   314 lemma ReflectsD:
   315      "[|REFLECTS[P,Q]; Ord(i)|]
   316       ==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <-> Q(j,x))"
   317 apply (unfold L_Reflects_def Closed_Unbounded_def)
   318 apply (elim meta_exE, clarify)
   319 apply (blast dest!: UnboundedD)
   320 done
   321 
   322 lemma ReflectsE:
   323      "[| REFLECTS[P,Q]; Ord(i);
   324          !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
   325       ==> R"
   326 apply (drule ReflectsD, assumption, blast)
   327 done
   328 
   329 lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B"
   330 by blast
   331 
   332 
   333 subsection{*Internalized Formulas for some Set-Theoretic Concepts*}
   334 
   335 lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex
   336 
   337 subsubsection{*Some numbers to help write de Bruijn indices*}
   338 
   339 syntax
   340     "3" :: i   ("3")
   341     "4" :: i   ("4")
   342     "5" :: i   ("5")
   343     "6" :: i   ("6")
   344     "7" :: i   ("7")
   345     "8" :: i   ("8")
   346     "9" :: i   ("9")
   347 
   348 translations
   349    "3"  == "succ(2)"
   350    "4"  == "succ(3)"
   351    "5"  == "succ(4)"
   352    "6"  == "succ(5)"
   353    "7"  == "succ(6)"
   354    "8"  == "succ(7)"
   355    "9"  == "succ(8)"
   356 
   357 
   358 subsubsection{*The Empty Set, Internalized*}
   359 
   360 constdefs empty_fm :: "i=>i"
   361     "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
   362 
   363 lemma empty_type [TC]:
   364      "x \<in> nat ==> empty_fm(x) \<in> formula"
   365 by (simp add: empty_fm_def)
   366 
   367 lemma arity_empty_fm [simp]:
   368      "x \<in> nat ==> arity(empty_fm(x)) = succ(x)"
   369 by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac)
   370 
   371 lemma sats_empty_fm [simp]:
   372    "[| x \<in> nat; env \<in> list(A)|]
   373     ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))"
   374 by (simp add: empty_fm_def empty_def)
   375 
   376 lemma empty_iff_sats:
   377       "[| nth(i,env) = x; nth(j,env) = y;
   378           i \<in> nat; env \<in> list(A)|]
   379        ==> empty(**A, x) <-> sats(A, empty_fm(i), env)"
   380 by simp
   381 
   382 theorem empty_reflection:
   383      "REFLECTS[\<lambda>x. empty(L,f(x)),
   384                \<lambda>i x. empty(**Lset(i),f(x))]"
   385 apply (simp only: empty_def setclass_simps)
   386 apply (intro FOL_reflections)
   387 done
   388 
   389 text{*Not used.  But maybe useful?*}
   390 lemma Transset_sats_empty_fm_eq_0:
   391    "[| n \<in> nat; env \<in> list(A); Transset(A)|]
   392     ==> sats(A, empty_fm(n), env) <-> nth(n,env) = 0"
   393 apply (simp add: empty_fm_def empty_def Transset_def, auto)
   394 apply (case_tac "n < length(env)")
   395 apply (frule nth_type, assumption+, blast)
   396 apply (simp_all add: not_lt_iff_le nth_eq_0)
   397 done
   398 
   399 
   400 subsubsection{*Unordered Pairs, Internalized*}
   401 
   402 constdefs upair_fm :: "[i,i,i]=>i"
   403     "upair_fm(x,y,z) ==
   404        And(Member(x,z),
   405            And(Member(y,z),
   406                Forall(Implies(Member(0,succ(z)),
   407                               Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"
   408 
   409 lemma upair_type [TC]:
   410      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> upair_fm(x,y,z) \<in> formula"
   411 by (simp add: upair_fm_def)
   412 
   413 lemma arity_upair_fm [simp]:
   414      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   415       ==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   416 by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)
   417 
   418 lemma sats_upair_fm [simp]:
   419    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   420     ==> sats(A, upair_fm(x,y,z), env) <->
   421             upair(**A, nth(x,env), nth(y,env), nth(z,env))"
   422 by (simp add: upair_fm_def upair_def)
   423 
   424 lemma upair_iff_sats:
   425       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   426           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   427        ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)"
   428 by (simp add: sats_upair_fm)
   429 
   430 text{*Useful? At least it refers to "real" unordered pairs*}
   431 lemma sats_upair_fm2 [simp]:
   432    "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|]
   433     ==> sats(A, upair_fm(x,y,z), env) <->
   434         nth(z,env) = {nth(x,env), nth(y,env)}"
   435 apply (frule lt_length_in_nat, assumption)
   436 apply (simp add: upair_fm_def Transset_def, auto)
   437 apply (blast intro: nth_type)
   438 done
   439 
   440 theorem upair_reflection:
   441      "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),
   442                \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"
   443 apply (simp add: upair_def)
   444 apply (intro FOL_reflections)
   445 done
   446 
   447 subsubsection{*Ordered pairs, Internalized*}
   448 
   449 constdefs pair_fm :: "[i,i,i]=>i"
   450     "pair_fm(x,y,z) ==
   451        Exists(And(upair_fm(succ(x),succ(x),0),
   452               Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
   453                          upair_fm(1,0,succ(succ(z)))))))"
   454 
   455 lemma pair_type [TC]:
   456      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pair_fm(x,y,z) \<in> formula"
   457 by (simp add: pair_fm_def)
   458 
   459 lemma arity_pair_fm [simp]:
   460      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   461       ==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   462 by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)
   463 
   464 lemma sats_pair_fm [simp]:
   465    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   466     ==> sats(A, pair_fm(x,y,z), env) <->
   467         pair(**A, nth(x,env), nth(y,env), nth(z,env))"
   468 by (simp add: pair_fm_def pair_def)
   469 
   470 lemma pair_iff_sats:
   471       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   472           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   473        ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)"
   474 by (simp add: sats_pair_fm)
   475 
   476 theorem pair_reflection:
   477      "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
   478                \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"
   479 apply (simp only: pair_def setclass_simps)
   480 apply (intro FOL_reflections upair_reflection)
   481 done
   482 
   483 
   484 subsubsection{*Binary Unions, Internalized*}
   485 
   486 constdefs union_fm :: "[i,i,i]=>i"
   487     "union_fm(x,y,z) ==
   488        Forall(Iff(Member(0,succ(z)),
   489                   Or(Member(0,succ(x)),Member(0,succ(y)))))"
   490 
   491 lemma union_type [TC]:
   492      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> union_fm(x,y,z) \<in> formula"
   493 by (simp add: union_fm_def)
   494 
   495 lemma arity_union_fm [simp]:
   496      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   497       ==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   498 by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)
   499 
   500 lemma sats_union_fm [simp]:
   501    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   502     ==> sats(A, union_fm(x,y,z), env) <->
   503         union(**A, nth(x,env), nth(y,env), nth(z,env))"
   504 by (simp add: union_fm_def union_def)
   505 
   506 lemma union_iff_sats:
   507       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   508           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   509        ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)"
   510 by (simp add: sats_union_fm)
   511 
   512 theorem union_reflection:
   513      "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
   514                \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"
   515 apply (simp only: union_def setclass_simps)
   516 apply (intro FOL_reflections)
   517 done
   518 
   519 
   520 subsubsection{*Set ``Cons,'' Internalized*}
   521 
   522 constdefs cons_fm :: "[i,i,i]=>i"
   523     "cons_fm(x,y,z) ==
   524        Exists(And(upair_fm(succ(x),succ(x),0),
   525                   union_fm(0,succ(y),succ(z))))"
   526 
   527 
   528 lemma cons_type [TC]:
   529      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cons_fm(x,y,z) \<in> formula"
   530 by (simp add: cons_fm_def)
   531 
   532 lemma arity_cons_fm [simp]:
   533      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   534       ==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   535 by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)
   536 
   537 lemma sats_cons_fm [simp]:
   538    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   539     ==> sats(A, cons_fm(x,y,z), env) <->
   540         is_cons(**A, nth(x,env), nth(y,env), nth(z,env))"
   541 by (simp add: cons_fm_def is_cons_def)
   542 
   543 lemma cons_iff_sats:
   544       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   545           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   546        ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)"
   547 by simp
   548 
   549 theorem cons_reflection:
   550      "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),
   551                \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"
   552 apply (simp only: is_cons_def setclass_simps)
   553 apply (intro FOL_reflections upair_reflection union_reflection)
   554 done
   555 
   556 
   557 subsubsection{*Successor Function, Internalized*}
   558 
   559 constdefs succ_fm :: "[i,i]=>i"
   560     "succ_fm(x,y) == cons_fm(x,x,y)"
   561 
   562 lemma succ_type [TC]:
   563      "[| x \<in> nat; y \<in> nat |] ==> succ_fm(x,y) \<in> formula"
   564 by (simp add: succ_fm_def)
   565 
   566 lemma arity_succ_fm [simp]:
   567      "[| x \<in> nat; y \<in> nat |]
   568       ==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)"
   569 by (simp add: succ_fm_def)
   570 
   571 lemma sats_succ_fm [simp]:
   572    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   573     ==> sats(A, succ_fm(x,y), env) <->
   574         successor(**A, nth(x,env), nth(y,env))"
   575 by (simp add: succ_fm_def successor_def)
   576 
   577 lemma successor_iff_sats:
   578       "[| nth(i,env) = x; nth(j,env) = y;
   579           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   580        ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)"
   581 by simp
   582 
   583 theorem successor_reflection:
   584      "REFLECTS[\<lambda>x. successor(L,f(x),g(x)),
   585                \<lambda>i x. successor(**Lset(i),f(x),g(x))]"
   586 apply (simp only: successor_def setclass_simps)
   587 apply (intro cons_reflection)
   588 done
   589 
   590 
   591 subsubsection{*The Number 1, Internalized*}
   592 
   593 (* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
   594 constdefs number1_fm :: "i=>i"
   595     "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
   596 
   597 lemma number1_type [TC]:
   598      "x \<in> nat ==> number1_fm(x) \<in> formula"
   599 by (simp add: number1_fm_def)
   600 
   601 lemma arity_number1_fm [simp]:
   602      "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
   603 by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
   604 
   605 lemma sats_number1_fm [simp]:
   606    "[| x \<in> nat; env \<in> list(A)|]
   607     ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
   608 by (simp add: number1_fm_def number1_def)
   609 
   610 lemma number1_iff_sats:
   611       "[| nth(i,env) = x; nth(j,env) = y;
   612           i \<in> nat; env \<in> list(A)|]
   613        ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
   614 by simp
   615 
   616 theorem number1_reflection:
   617      "REFLECTS[\<lambda>x. number1(L,f(x)),
   618                \<lambda>i x. number1(**Lset(i),f(x))]"
   619 apply (simp only: number1_def setclass_simps)
   620 apply (intro FOL_reflections empty_reflection successor_reflection)
   621 done
   622 
   623 
   624 subsubsection{*Big Union, Internalized*}
   625 
   626 (*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
   627 constdefs big_union_fm :: "[i,i]=>i"
   628     "big_union_fm(A,z) ==
   629        Forall(Iff(Member(0,succ(z)),
   630                   Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
   631 
   632 lemma big_union_type [TC]:
   633      "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
   634 by (simp add: big_union_fm_def)
   635 
   636 lemma arity_big_union_fm [simp]:
   637      "[| x \<in> nat; y \<in> nat |]
   638       ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
   639 by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
   640 
   641 lemma sats_big_union_fm [simp]:
   642    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   643     ==> sats(A, big_union_fm(x,y), env) <->
   644         big_union(**A, nth(x,env), nth(y,env))"
   645 by (simp add: big_union_fm_def big_union_def)
   646 
   647 lemma big_union_iff_sats:
   648       "[| nth(i,env) = x; nth(j,env) = y;
   649           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   650        ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
   651 by simp
   652 
   653 theorem big_union_reflection:
   654      "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
   655                \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
   656 apply (simp only: big_union_def setclass_simps)
   657 apply (intro FOL_reflections)
   658 done
   659 
   660 
   661 subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*}
   662 
   663 text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*}
   664 
   665 
   666 lemma sats_subset_fm':
   667    "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
   668     ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))"
   669 by (simp add: subset_fm_def Relative.subset_def)
   670 
   671 theorem subset_reflection:
   672      "REFLECTS[\<lambda>x. subset(L,f(x),g(x)),
   673                \<lambda>i x. subset(**Lset(i),f(x),g(x))]"
   674 apply (simp only: Relative.subset_def setclass_simps)
   675 apply (intro FOL_reflections)
   676 done
   677 
   678 lemma sats_transset_fm':
   679    "[|x \<in> nat; env \<in> list(A)|]
   680     ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))"
   681 by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)
   682 
   683 theorem transitive_set_reflection:
   684      "REFLECTS[\<lambda>x. transitive_set(L,f(x)),
   685                \<lambda>i x. transitive_set(**Lset(i),f(x))]"
   686 apply (simp only: transitive_set_def setclass_simps)
   687 apply (intro FOL_reflections subset_reflection)
   688 done
   689 
   690 lemma sats_ordinal_fm':
   691    "[|x \<in> nat; env \<in> list(A)|]
   692     ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))"
   693 by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def)
   694 
   695 lemma ordinal_iff_sats:
   696       "[| nth(i,env) = x;  i \<in> nat; env \<in> list(A)|]
   697        ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)"
   698 by (simp add: sats_ordinal_fm')
   699 
   700 theorem ordinal_reflection:
   701      "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"
   702 apply (simp only: ordinal_def setclass_simps)
   703 apply (intro FOL_reflections transitive_set_reflection)
   704 done
   705 
   706 
   707 subsubsection{*Membership Relation, Internalized*}
   708 
   709 constdefs Memrel_fm :: "[i,i]=>i"
   710     "Memrel_fm(A,r) ==
   711        Forall(Iff(Member(0,succ(r)),
   712                   Exists(And(Member(0,succ(succ(A))),
   713                              Exists(And(Member(0,succ(succ(succ(A)))),
   714                                         And(Member(1,0),
   715                                             pair_fm(1,0,2))))))))"
   716 
   717 lemma Memrel_type [TC]:
   718      "[| x \<in> nat; y \<in> nat |] ==> Memrel_fm(x,y) \<in> formula"
   719 by (simp add: Memrel_fm_def)
   720 
   721 lemma arity_Memrel_fm [simp]:
   722      "[| x \<in> nat; y \<in> nat |]
   723       ==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)"
   724 by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)
   725 
   726 lemma sats_Memrel_fm [simp]:
   727    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   728     ==> sats(A, Memrel_fm(x,y), env) <->
   729         membership(**A, nth(x,env), nth(y,env))"
   730 by (simp add: Memrel_fm_def membership_def)
   731 
   732 lemma Memrel_iff_sats:
   733       "[| nth(i,env) = x; nth(j,env) = y;
   734           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   735        ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)"
   736 by simp
   737 
   738 theorem membership_reflection:
   739      "REFLECTS[\<lambda>x. membership(L,f(x),g(x)),
   740                \<lambda>i x. membership(**Lset(i),f(x),g(x))]"
   741 apply (simp only: membership_def setclass_simps)
   742 apply (intro FOL_reflections pair_reflection)
   743 done
   744 
   745 subsubsection{*Predecessor Set, Internalized*}
   746 
   747 constdefs pred_set_fm :: "[i,i,i,i]=>i"
   748     "pred_set_fm(A,x,r,B) ==
   749        Forall(Iff(Member(0,succ(B)),
   750                   Exists(And(Member(0,succ(succ(r))),
   751                              And(Member(1,succ(succ(A))),
   752                                  pair_fm(1,succ(succ(x)),0))))))"
   753 
   754 
   755 lemma pred_set_type [TC]:
   756      "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
   757       ==> pred_set_fm(A,x,r,B) \<in> formula"
   758 by (simp add: pred_set_fm_def)
   759 
   760 lemma arity_pred_set_fm [simp]:
   761    "[| A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat |]
   762     ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)"
   763 by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)
   764 
   765 lemma sats_pred_set_fm [simp]:
   766    "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|]
   767     ==> sats(A, pred_set_fm(U,x,r,B), env) <->
   768         pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"
   769 by (simp add: pred_set_fm_def pred_set_def)
   770 
   771 lemma pred_set_iff_sats:
   772       "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
   773           i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
   774        ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)"
   775 by (simp add: sats_pred_set_fm)
   776 
   777 theorem pred_set_reflection:
   778      "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
   779                \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"
   780 apply (simp only: pred_set_def setclass_simps)
   781 apply (intro FOL_reflections pair_reflection)
   782 done
   783 
   784 
   785 
   786 subsubsection{*Domain of a Relation, Internalized*}
   787 
   788 (* "is_domain(M,r,z) ==
   789         \<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
   790 constdefs domain_fm :: "[i,i]=>i"
   791     "domain_fm(r,z) ==
   792        Forall(Iff(Member(0,succ(z)),
   793                   Exists(And(Member(0,succ(succ(r))),
   794                              Exists(pair_fm(2,0,1))))))"
   795 
   796 lemma domain_type [TC]:
   797      "[| x \<in> nat; y \<in> nat |] ==> domain_fm(x,y) \<in> formula"
   798 by (simp add: domain_fm_def)
   799 
   800 lemma arity_domain_fm [simp]:
   801      "[| x \<in> nat; y \<in> nat |]
   802       ==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)"
   803 by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)
   804 
   805 lemma sats_domain_fm [simp]:
   806    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   807     ==> sats(A, domain_fm(x,y), env) <->
   808         is_domain(**A, nth(x,env), nth(y,env))"
   809 by (simp add: domain_fm_def is_domain_def)
   810 
   811 lemma domain_iff_sats:
   812       "[| nth(i,env) = x; nth(j,env) = y;
   813           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   814        ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)"
   815 by simp
   816 
   817 theorem domain_reflection:
   818      "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),
   819                \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"
   820 apply (simp only: is_domain_def setclass_simps)
   821 apply (intro FOL_reflections pair_reflection)
   822 done
   823 
   824 
   825 subsubsection{*Range of a Relation, Internalized*}
   826 
   827 (* "is_range(M,r,z) ==
   828         \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
   829 constdefs range_fm :: "[i,i]=>i"
   830     "range_fm(r,z) ==
   831        Forall(Iff(Member(0,succ(z)),
   832                   Exists(And(Member(0,succ(succ(r))),
   833                              Exists(pair_fm(0,2,1))))))"
   834 
   835 lemma range_type [TC]:
   836      "[| x \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
   837 by (simp add: range_fm_def)
   838 
   839 lemma arity_range_fm [simp]:
   840      "[| x \<in> nat; y \<in> nat |]
   841       ==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)"
   842 by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)
   843 
   844 lemma sats_range_fm [simp]:
   845    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   846     ==> sats(A, range_fm(x,y), env) <->
   847         is_range(**A, nth(x,env), nth(y,env))"
   848 by (simp add: range_fm_def is_range_def)
   849 
   850 lemma range_iff_sats:
   851       "[| nth(i,env) = x; nth(j,env) = y;
   852           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   853        ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)"
   854 by simp
   855 
   856 theorem range_reflection:
   857      "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),
   858                \<lambda>i x. is_range(**Lset(i),f(x),g(x))]"
   859 apply (simp only: is_range_def setclass_simps)
   860 apply (intro FOL_reflections pair_reflection)
   861 done
   862 
   863 
   864 subsubsection{*Field of a Relation, Internalized*}
   865 
   866 (* "is_field(M,r,z) ==
   867         \<exists>dr[M]. is_domain(M,r,dr) &
   868             (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
   869 constdefs field_fm :: "[i,i]=>i"
   870     "field_fm(r,z) ==
   871        Exists(And(domain_fm(succ(r),0),
   872               Exists(And(range_fm(succ(succ(r)),0),
   873                          union_fm(1,0,succ(succ(z)))))))"
   874 
   875 lemma field_type [TC]:
   876      "[| x \<in> nat; y \<in> nat |] ==> field_fm(x,y) \<in> formula"
   877 by (simp add: field_fm_def)
   878 
   879 lemma arity_field_fm [simp]:
   880      "[| x \<in> nat; y \<in> nat |]
   881       ==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)"
   882 by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac)
   883 
   884 lemma sats_field_fm [simp]:
   885    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   886     ==> sats(A, field_fm(x,y), env) <->
   887         is_field(**A, nth(x,env), nth(y,env))"
   888 by (simp add: field_fm_def is_field_def)
   889 
   890 lemma field_iff_sats:
   891       "[| nth(i,env) = x; nth(j,env) = y;
   892           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   893        ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)"
   894 by simp
   895 
   896 theorem field_reflection:
   897      "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)),
   898                \<lambda>i x. is_field(**Lset(i),f(x),g(x))]"
   899 apply (simp only: is_field_def setclass_simps)
   900 apply (intro FOL_reflections domain_reflection range_reflection
   901              union_reflection)
   902 done
   903 
   904 
   905 subsubsection{*Image under a Relation, Internalized*}
   906 
   907 (* "image(M,r,A,z) ==
   908         \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
   909 constdefs image_fm :: "[i,i,i]=>i"
   910     "image_fm(r,A,z) ==
   911        Forall(Iff(Member(0,succ(z)),
   912                   Exists(And(Member(0,succ(succ(r))),
   913                              Exists(And(Member(0,succ(succ(succ(A)))),
   914                                         pair_fm(0,2,1)))))))"
   915 
   916 lemma image_type [TC]:
   917      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> image_fm(x,y,z) \<in> formula"
   918 by (simp add: image_fm_def)
   919 
   920 lemma arity_image_fm [simp]:
   921      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   922       ==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   923 by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)
   924 
   925 lemma sats_image_fm [simp]:
   926    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   927     ==> sats(A, image_fm(x,y,z), env) <->
   928         image(**A, nth(x,env), nth(y,env), nth(z,env))"
   929 by (simp add: image_fm_def Relative.image_def)
   930 
   931 lemma image_iff_sats:
   932       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   933           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   934        ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)"
   935 by (simp add: sats_image_fm)
   936 
   937 theorem image_reflection:
   938      "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
   939                \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"
   940 apply (simp only: Relative.image_def setclass_simps)
   941 apply (intro FOL_reflections pair_reflection)
   942 done
   943 
   944 
   945 subsubsection{*Pre-Image under a Relation, Internalized*}
   946 
   947 (* "pre_image(M,r,A,z) ==
   948         \<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
   949 constdefs pre_image_fm :: "[i,i,i]=>i"
   950     "pre_image_fm(r,A,z) ==
   951        Forall(Iff(Member(0,succ(z)),
   952                   Exists(And(Member(0,succ(succ(r))),
   953                              Exists(And(Member(0,succ(succ(succ(A)))),
   954                                         pair_fm(2,0,1)))))))"
   955 
   956 lemma pre_image_type [TC]:
   957      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> pre_image_fm(x,y,z) \<in> formula"
   958 by (simp add: pre_image_fm_def)
   959 
   960 lemma arity_pre_image_fm [simp]:
   961      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
   962       ==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
   963 by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac)
   964 
   965 lemma sats_pre_image_fm [simp]:
   966    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   967     ==> sats(A, pre_image_fm(x,y,z), env) <->
   968         pre_image(**A, nth(x,env), nth(y,env), nth(z,env))"
   969 by (simp add: pre_image_fm_def Relative.pre_image_def)
   970 
   971 lemma pre_image_iff_sats:
   972       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   973           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   974        ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)"
   975 by (simp add: sats_pre_image_fm)
   976 
   977 theorem pre_image_reflection:
   978      "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
   979                \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]"
   980 apply (simp only: Relative.pre_image_def setclass_simps)
   981 apply (intro FOL_reflections pair_reflection)
   982 done
   983 
   984 
   985 subsubsection{*Function Application, Internalized*}
   986 
   987 (* "fun_apply(M,f,x,y) ==
   988         (\<exists>xs[M]. \<exists>fxs[M].
   989          upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
   990 constdefs fun_apply_fm :: "[i,i,i]=>i"
   991     "fun_apply_fm(f,x,y) ==
   992        Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
   993                          And(image_fm(succ(succ(f)), 1, 0),
   994                              big_union_fm(0,succ(succ(y)))))))"
   995 
   996 lemma fun_apply_type [TC]:
   997      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
   998 by (simp add: fun_apply_fm_def)
   999 
  1000 lemma arity_fun_apply_fm [simp]:
  1001      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1002       ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1003 by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
  1004 
  1005 lemma sats_fun_apply_fm [simp]:
  1006    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1007     ==> sats(A, fun_apply_fm(x,y,z), env) <->
  1008         fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
  1009 by (simp add: fun_apply_fm_def fun_apply_def)
  1010 
  1011 lemma fun_apply_iff_sats:
  1012       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1013           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1014        ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
  1015 by simp
  1016 
  1017 theorem fun_apply_reflection:
  1018      "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
  1019                \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
  1020 apply (simp only: fun_apply_def setclass_simps)
  1021 apply (intro FOL_reflections upair_reflection image_reflection
  1022              big_union_reflection)
  1023 done
  1024 
  1025 
  1026 subsubsection{*The Concept of Relation, Internalized*}
  1027 
  1028 (* "is_relation(M,r) ==
  1029         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
  1030 constdefs relation_fm :: "i=>i"
  1031     "relation_fm(r) ==
  1032        Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"
  1033 
  1034 lemma relation_type [TC]:
  1035      "[| x \<in> nat |] ==> relation_fm(x) \<in> formula"
  1036 by (simp add: relation_fm_def)
  1037 
  1038 lemma arity_relation_fm [simp]:
  1039      "x \<in> nat ==> arity(relation_fm(x)) = succ(x)"
  1040 by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)
  1041 
  1042 lemma sats_relation_fm [simp]:
  1043    "[| x \<in> nat; env \<in> list(A)|]
  1044     ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))"
  1045 by (simp add: relation_fm_def is_relation_def)
  1046 
  1047 lemma relation_iff_sats:
  1048       "[| nth(i,env) = x; nth(j,env) = y;
  1049           i \<in> nat; env \<in> list(A)|]
  1050        ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)"
  1051 by simp
  1052 
  1053 theorem is_relation_reflection:
  1054      "REFLECTS[\<lambda>x. is_relation(L,f(x)),
  1055                \<lambda>i x. is_relation(**Lset(i),f(x))]"
  1056 apply (simp only: is_relation_def setclass_simps)
  1057 apply (intro FOL_reflections pair_reflection)
  1058 done
  1059 
  1060 
  1061 subsubsection{*The Concept of Function, Internalized*}
  1062 
  1063 (* "is_function(M,r) ==
  1064         \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
  1065            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'" *)
  1066 constdefs function_fm :: "i=>i"
  1067     "function_fm(r) ==
  1068        Forall(Forall(Forall(Forall(Forall(
  1069          Implies(pair_fm(4,3,1),
  1070                  Implies(pair_fm(4,2,0),
  1071                          Implies(Member(1,r#+5),
  1072                                  Implies(Member(0,r#+5), Equal(3,2))))))))))"
  1073 
  1074 lemma function_type [TC]:
  1075      "[| x \<in> nat |] ==> function_fm(x) \<in> formula"
  1076 by (simp add: function_fm_def)
  1077 
  1078 lemma arity_function_fm [simp]:
  1079      "x \<in> nat ==> arity(function_fm(x)) = succ(x)"
  1080 by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)
  1081 
  1082 lemma sats_function_fm [simp]:
  1083    "[| x \<in> nat; env \<in> list(A)|]
  1084     ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
  1085 by (simp add: function_fm_def is_function_def)
  1086 
  1087 lemma is_function_iff_sats:
  1088       "[| nth(i,env) = x; nth(j,env) = y;
  1089           i \<in> nat; env \<in> list(A)|]
  1090        ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
  1091 by simp
  1092 
  1093 theorem is_function_reflection:
  1094      "REFLECTS[\<lambda>x. is_function(L,f(x)),
  1095                \<lambda>i x. is_function(**Lset(i),f(x))]"
  1096 apply (simp only: is_function_def setclass_simps)
  1097 apply (intro FOL_reflections pair_reflection)
  1098 done
  1099 
  1100 
  1101 subsubsection{*Typed Functions, Internalized*}
  1102 
  1103 (* "typed_function(M,A,B,r) ==
  1104         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
  1105         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))" *)
  1106 
  1107 constdefs typed_function_fm :: "[i,i,i]=>i"
  1108     "typed_function_fm(A,B,r) ==
  1109        And(function_fm(r),
  1110          And(relation_fm(r),
  1111            And(domain_fm(r,A),
  1112              Forall(Implies(Member(0,succ(r)),
  1113                   Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))"
  1114 
  1115 lemma typed_function_type [TC]:
  1116      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> typed_function_fm(x,y,z) \<in> formula"
  1117 by (simp add: typed_function_fm_def)
  1118 
  1119 lemma arity_typed_function_fm [simp]:
  1120      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1121       ==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1122 by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)
  1123 
  1124 lemma sats_typed_function_fm [simp]:
  1125    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1126     ==> sats(A, typed_function_fm(x,y,z), env) <->
  1127         typed_function(**A, nth(x,env), nth(y,env), nth(z,env))"
  1128 by (simp add: typed_function_fm_def typed_function_def)
  1129 
  1130 lemma typed_function_iff_sats:
  1131   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1132       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1133    ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
  1134 by simp
  1135 
  1136 lemmas function_reflections =
  1137         empty_reflection number1_reflection
  1138         upair_reflection pair_reflection union_reflection
  1139         big_union_reflection cons_reflection successor_reflection
  1140         fun_apply_reflection subset_reflection
  1141         transitive_set_reflection membership_reflection
  1142         pred_set_reflection domain_reflection range_reflection field_reflection
  1143         image_reflection pre_image_reflection
  1144         is_relation_reflection is_function_reflection
  1145 
  1146 lemmas function_iff_sats =
  1147         empty_iff_sats number1_iff_sats
  1148         upair_iff_sats pair_iff_sats union_iff_sats
  1149         big_union_iff_sats cons_iff_sats successor_iff_sats
  1150         fun_apply_iff_sats  Memrel_iff_sats
  1151         pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
  1152         image_iff_sats pre_image_iff_sats
  1153         relation_iff_sats is_function_iff_sats
  1154 
  1155 
  1156 theorem typed_function_reflection:
  1157      "REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),
  1158                \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"
  1159 apply (simp only: typed_function_def setclass_simps)
  1160 apply (intro FOL_reflections function_reflections)
  1161 done
  1162 
  1163 
  1164 subsubsection{*Composition of Relations, Internalized*}
  1165 
  1166 (* "composition(M,r,s,t) ==
  1167         \<forall>p[M]. p \<in> t <->
  1168                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
  1169                 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
  1170                 xy \<in> s & yz \<in> r)" *)
  1171 constdefs composition_fm :: "[i,i,i]=>i"
  1172   "composition_fm(r,s,t) ==
  1173      Forall(Iff(Member(0,succ(t)),
  1174              Exists(Exists(Exists(Exists(Exists(
  1175               And(pair_fm(4,2,5),
  1176                And(pair_fm(4,3,1),
  1177                 And(pair_fm(3,2,0),
  1178                  And(Member(1,s#+6), Member(0,r#+6))))))))))))"
  1179 
  1180 lemma composition_type [TC]:
  1181      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> composition_fm(x,y,z) \<in> formula"
  1182 by (simp add: composition_fm_def)
  1183 
  1184 lemma arity_composition_fm [simp]:
  1185      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1186       ==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1187 by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac)
  1188 
  1189 lemma sats_composition_fm [simp]:
  1190    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1191     ==> sats(A, composition_fm(x,y,z), env) <->
  1192         composition(**A, nth(x,env), nth(y,env), nth(z,env))"
  1193 by (simp add: composition_fm_def composition_def)
  1194 
  1195 lemma composition_iff_sats:
  1196       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1197           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1198        ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)"
  1199 by simp
  1200 
  1201 theorem composition_reflection:
  1202      "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)),
  1203                \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]"
  1204 apply (simp only: composition_def setclass_simps)
  1205 apply (intro FOL_reflections pair_reflection)
  1206 done
  1207 
  1208 
  1209 subsubsection{*Injections, Internalized*}
  1210 
  1211 (* "injection(M,A,B,f) ==
  1212         typed_function(M,A,B,f) &
  1213         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
  1214           pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')" *)
  1215 constdefs injection_fm :: "[i,i,i]=>i"
  1216  "injection_fm(A,B,f) ==
  1217     And(typed_function_fm(A,B,f),
  1218        Forall(Forall(Forall(Forall(Forall(
  1219          Implies(pair_fm(4,2,1),
  1220                  Implies(pair_fm(3,2,0),
  1221                          Implies(Member(1,f#+5),
  1222                                  Implies(Member(0,f#+5), Equal(4,3)))))))))))"
  1223 
  1224 
  1225 lemma injection_type [TC]:
  1226      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> injection_fm(x,y,z) \<in> formula"
  1227 by (simp add: injection_fm_def)
  1228 
  1229 lemma arity_injection_fm [simp]:
  1230      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1231       ==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1232 by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)
  1233 
  1234 lemma sats_injection_fm [simp]:
  1235    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1236     ==> sats(A, injection_fm(x,y,z), env) <->
  1237         injection(**A, nth(x,env), nth(y,env), nth(z,env))"
  1238 by (simp add: injection_fm_def injection_def)
  1239 
  1240 lemma injection_iff_sats:
  1241   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1242       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1243    ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
  1244 by simp
  1245 
  1246 theorem injection_reflection:
  1247      "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),
  1248                \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"
  1249 apply (simp only: injection_def setclass_simps)
  1250 apply (intro FOL_reflections function_reflections typed_function_reflection)
  1251 done
  1252 
  1253 
  1254 subsubsection{*Surjections, Internalized*}
  1255 
  1256 (*  surjection :: "[i=>o,i,i,i] => o"
  1257     "surjection(M,A,B,f) ==
  1258         typed_function(M,A,B,f) &
  1259         (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)
  1260 constdefs surjection_fm :: "[i,i,i]=>i"
  1261  "surjection_fm(A,B,f) ==
  1262     And(typed_function_fm(A,B,f),
  1263        Forall(Implies(Member(0,succ(B)),
  1264                       Exists(And(Member(0,succ(succ(A))),
  1265                                  fun_apply_fm(succ(succ(f)),0,1))))))"
  1266 
  1267 lemma surjection_type [TC]:
  1268      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> surjection_fm(x,y,z) \<in> formula"
  1269 by (simp add: surjection_fm_def)
  1270 
  1271 lemma arity_surjection_fm [simp]:
  1272      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1273       ==> arity(surjection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1274 by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)
  1275 
  1276 lemma sats_surjection_fm [simp]:
  1277    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1278     ==> sats(A, surjection_fm(x,y,z), env) <->
  1279         surjection(**A, nth(x,env), nth(y,env), nth(z,env))"
  1280 by (simp add: surjection_fm_def surjection_def)
  1281 
  1282 lemma surjection_iff_sats:
  1283   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1284       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1285    ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
  1286 by simp
  1287 
  1288 theorem surjection_reflection:
  1289      "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),
  1290                \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"
  1291 apply (simp only: surjection_def setclass_simps)
  1292 apply (intro FOL_reflections function_reflections typed_function_reflection)
  1293 done
  1294 
  1295 
  1296 
  1297 subsubsection{*Bijections, Internalized*}
  1298 
  1299 (*   bijection :: "[i=>o,i,i,i] => o"
  1300     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
  1301 constdefs bijection_fm :: "[i,i,i]=>i"
  1302  "bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"
  1303 
  1304 lemma bijection_type [TC]:
  1305      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> bijection_fm(x,y,z) \<in> formula"
  1306 by (simp add: bijection_fm_def)
  1307 
  1308 lemma arity_bijection_fm [simp]:
  1309      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1310       ==> arity(bijection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1311 by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)
  1312 
  1313 lemma sats_bijection_fm [simp]:
  1314    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1315     ==> sats(A, bijection_fm(x,y,z), env) <->
  1316         bijection(**A, nth(x,env), nth(y,env), nth(z,env))"
  1317 by (simp add: bijection_fm_def bijection_def)
  1318 
  1319 lemma bijection_iff_sats:
  1320   "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1321       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1322    ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
  1323 by simp
  1324 
  1325 theorem bijection_reflection:
  1326      "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),
  1327                \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"
  1328 apply (simp only: bijection_def setclass_simps)
  1329 apply (intro And_reflection injection_reflection surjection_reflection)
  1330 done
  1331 
  1332 
  1333 subsubsection{*Restriction of a Relation, Internalized*}
  1334 
  1335 
  1336 (* "restriction(M,r,A,z) ==
  1337         \<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
  1338 constdefs restriction_fm :: "[i,i,i]=>i"
  1339     "restriction_fm(r,A,z) ==
  1340        Forall(Iff(Member(0,succ(z)),
  1341                   And(Member(0,succ(r)),
  1342                       Exists(And(Member(0,succ(succ(A))),
  1343                                  Exists(pair_fm(1,0,2)))))))"
  1344 
  1345 lemma restriction_type [TC]:
  1346      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> restriction_fm(x,y,z) \<in> formula"
  1347 by (simp add: restriction_fm_def)
  1348 
  1349 lemma arity_restriction_fm [simp]:
  1350      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
  1351       ==> arity(restriction_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
  1352 by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac)
  1353 
  1354 lemma sats_restriction_fm [simp]:
  1355    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
  1356     ==> sats(A, restriction_fm(x,y,z), env) <->
  1357         restriction(**A, nth(x,env), nth(y,env), nth(z,env))"
  1358 by (simp add: restriction_fm_def restriction_def)
  1359 
  1360 lemma restriction_iff_sats:
  1361       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
  1362           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
  1363        ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)"
  1364 by simp
  1365 
  1366 theorem restriction_reflection:
  1367      "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)),
  1368                \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]"
  1369 apply (simp only: restriction_def setclass_simps)
  1370 apply (intro FOL_reflections pair_reflection)
  1371 done
  1372 
  1373 subsubsection{*Order-Isomorphisms, Internalized*}
  1374 
  1375 (*  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
  1376    "order_isomorphism(M,A,r,B,s,f) ==
  1377         bijection(M,A,B,f) &
  1378         (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
  1379           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
  1380             pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
  1381             pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
  1382   *)
  1383 
  1384 constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"
  1385  "order_isomorphism_fm(A,r,B,s,f) ==
  1386    And(bijection_fm(A,B,f),
  1387      Forall(Implies(Member(0,succ(A)),
  1388        Forall(Implies(Member(0,succ(succ(A))),
  1389          Forall(Forall(Forall(Forall(
  1390            Implies(pair_fm(5,4,3),
  1391              Implies(fun_apply_fm(f#+6,5,2),
  1392                Implies(fun_apply_fm(f#+6,4,1),
  1393                  Implies(pair_fm(2,1,0),
  1394                    Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))"
  1395 
  1396 lemma order_isomorphism_type [TC]:
  1397      "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
  1398       ==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"
  1399 by (simp add: order_isomorphism_fm_def)
  1400 
  1401 lemma arity_order_isomorphism_fm [simp]:
  1402      "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
  1403       ==> arity(order_isomorphism_fm(A,r,B,s,f)) =
  1404           succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"
  1405 by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)
  1406 
  1407 lemma sats_order_isomorphism_fm [simp]:
  1408    "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
  1409     ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
  1410         order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),
  1411                                nth(s,env), nth(f,env))"
  1412 by (simp add: order_isomorphism_fm_def order_isomorphism_def)
  1413 
  1414 lemma order_isomorphism_iff_sats:
  1415   "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;
  1416       nth(k',env) = f;
  1417       i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|]
  1418    ==> order_isomorphism(**A,U,r,B,s,f) <->
  1419        sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
  1420 by simp
  1421 
  1422 theorem order_isomorphism_reflection:
  1423      "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
  1424                \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
  1425 apply (simp only: order_isomorphism_def setclass_simps)
  1426 apply (intro FOL_reflections function_reflections bijection_reflection)
  1427 done
  1428 
  1429 subsubsection{*Limit Ordinals, Internalized*}
  1430 
  1431 text{*A limit ordinal is a non-empty, successor-closed ordinal*}
  1432 
  1433 (* "limit_ordinal(M,a) ==
  1434         ordinal(M,a) & ~ empty(M,a) &
  1435         (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
  1436 
  1437 constdefs limit_ordinal_fm :: "i=>i"
  1438     "limit_ordinal_fm(x) ==
  1439         And(ordinal_fm(x),
  1440             And(Neg(empty_fm(x)),
  1441                 Forall(Implies(Member(0,succ(x)),
  1442                                Exists(And(Member(0,succ(succ(x))),
  1443                                           succ_fm(1,0)))))))"
  1444 
  1445 lemma limit_ordinal_type [TC]:
  1446      "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula"
  1447 by (simp add: limit_ordinal_fm_def)
  1448 
  1449 lemma arity_limit_ordinal_fm [simp]:
  1450      "x \<in> nat ==> arity(limit_ordinal_fm(x)) = succ(x)"
  1451 by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac)
  1452 
  1453 lemma sats_limit_ordinal_fm [simp]:
  1454    "[| x \<in> nat; env \<in> list(A)|]
  1455     ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))"
  1456 by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm')
  1457 
  1458 lemma limit_ordinal_iff_sats:
  1459       "[| nth(i,env) = x; nth(j,env) = y;
  1460           i \<in> nat; env \<in> list(A)|]
  1461        ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)"
  1462 by simp
  1463 
  1464 theorem limit_ordinal_reflection:
  1465      "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)),
  1466                \<lambda>i x. limit_ordinal(**Lset(i),f(x))]"
  1467 apply (simp only: limit_ordinal_def setclass_simps)
  1468 apply (intro FOL_reflections ordinal_reflection
  1469              empty_reflection successor_reflection)
  1470 done
  1471 
  1472 subsubsection{*Finite Ordinals: The Predicate ``Is A Natural Number''*}
  1473 
  1474 (*     "finite_ordinal(M,a) == 
  1475 	ordinal(M,a) & ~ limit_ordinal(M,a) & 
  1476         (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
  1477 constdefs finite_ordinal_fm :: "i=>i"
  1478     "finite_ordinal_fm(x) ==
  1479        And(ordinal_fm(x),
  1480           And(Neg(limit_ordinal_fm(x)),
  1481            Forall(Implies(Member(0,succ(x)),
  1482                           Neg(limit_ordinal_fm(0))))))"
  1483 
  1484 lemma finite_ordinal_type [TC]:
  1485      "x \<in> nat ==> finite_ordinal_fm(x) \<in> formula"
  1486 by (simp add: finite_ordinal_fm_def)
  1487 
  1488 lemma sats_finite_ordinal_fm [simp]:
  1489    "[| x \<in> nat; env \<in> list(A)|]
  1490     ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(**A, nth(x,env))"
  1491 by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def)
  1492 
  1493 lemma finite_ordinal_iff_sats:
  1494       "[| nth(i,env) = x; nth(j,env) = y;
  1495           i \<in> nat; env \<in> list(A)|]
  1496        ==> finite_ordinal(**A, x) <-> sats(A, finite_ordinal_fm(i), env)"
  1497 by simp
  1498 
  1499 theorem finite_ordinal_reflection:
  1500      "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)),
  1501                \<lambda>i x. finite_ordinal(**Lset(i),f(x))]"
  1502 apply (simp only: finite_ordinal_def setclass_simps)
  1503 apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection)
  1504 done
  1505 
  1506 
  1507 subsubsection{*Omega: The Set of Natural Numbers*}
  1508 
  1509 (* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
  1510 constdefs omega_fm :: "i=>i"
  1511     "omega_fm(x) ==
  1512        And(limit_ordinal_fm(x),
  1513            Forall(Implies(Member(0,succ(x)),
  1514                           Neg(limit_ordinal_fm(0)))))"
  1515 
  1516 lemma omega_type [TC]:
  1517      "x \<in> nat ==> omega_fm(x) \<in> formula"
  1518 by (simp add: omega_fm_def)
  1519 
  1520 lemma arity_omega_fm [simp]:
  1521      "x \<in> nat ==> arity(omega_fm(x)) = succ(x)"
  1522 by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac)
  1523 
  1524 lemma sats_omega_fm [simp]:
  1525    "[| x \<in> nat; env \<in> list(A)|]
  1526     ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))"
  1527 by (simp add: omega_fm_def omega_def)
  1528 
  1529 lemma omega_iff_sats:
  1530       "[| nth(i,env) = x; nth(j,env) = y;
  1531           i \<in> nat; env \<in> list(A)|]
  1532        ==> omega(**A, x) <-> sats(A, omega_fm(i), env)"
  1533 by simp
  1534 
  1535 theorem omega_reflection:
  1536      "REFLECTS[\<lambda>x. omega(L,f(x)),
  1537                \<lambda>i x. omega(**Lset(i),f(x))]"
  1538 apply (simp only: omega_def setclass_simps)
  1539 apply (intro FOL_reflections limit_ordinal_reflection)
  1540 done
  1541 
  1542 
  1543 lemmas fun_plus_reflections =
  1544         typed_function_reflection composition_reflection
  1545         injection_reflection surjection_reflection
  1546         bijection_reflection restriction_reflection
  1547         order_isomorphism_reflection finite_ordinal_reflection 
  1548         ordinal_reflection limit_ordinal_reflection omega_reflection
  1549 
  1550 lemmas fun_plus_iff_sats =
  1551         typed_function_iff_sats composition_iff_sats
  1552         injection_iff_sats surjection_iff_sats
  1553         bijection_iff_sats restriction_iff_sats
  1554         order_isomorphism_iff_sats finite_ordinal_iff_sats
  1555         ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats
  1556 
  1557 end