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