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