src/ZF/Constructible/Separation.thy
author paulson
Wed Jul 31 18:30:25 2002 +0200 (2002-07-31)
changeset 13440 cdde97e1db1c
parent 13437 01b3fc0cc1b8
child 13505 52a16cb7fefb
permissions -rw-r--r--
some progress towards "satisfies"
paulson@13437
     1
(*  Title:      ZF/Constructible/Separation.thy
paulson@13437
     2
    ID:         $Id$
paulson@13437
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13437
     4
    Copyright   2002  University of Cambridge
paulson@13437
     5
*)
paulson@13437
     6
paulson@13339
     7
header{*Early Instances of Separation and Strong Replacement*}
paulson@13323
     8
paulson@13324
     9
theory Separation = L_axioms + WF_absolute:
paulson@13306
    10
paulson@13339
    11
text{*This theory proves all instances needed for locale @{text "M_axioms"}*}
paulson@13339
    12
paulson@13306
    13
text{*Helps us solve for de Bruijn indices!*}
paulson@13306
    14
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
paulson@13306
    15
by simp
paulson@13306
    16
paulson@13316
    17
lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI
wenzelm@13428
    18
lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats
paulson@13323
    19
                   fun_plus_iff_sats
paulson@13306
    20
paulson@13306
    21
lemma Collect_conj_in_DPow:
wenzelm@13428
    22
     "[| {x\<in>A. P(x)} \<in> DPow(A);  {x\<in>A. Q(x)} \<in> DPow(A) |]
paulson@13306
    23
      ==> {x\<in>A. P(x) & Q(x)} \<in> DPow(A)"
wenzelm@13428
    24
by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric])
paulson@13306
    25
paulson@13306
    26
lemma Collect_conj_in_DPow_Lset:
paulson@13306
    27
     "[|z \<in> Lset(j); {x \<in> Lset(j). P(x)} \<in> DPow(Lset(j))|]
paulson@13306
    28
      ==> {x \<in> Lset(j). x \<in> z & P(x)} \<in> DPow(Lset(j))"
paulson@13306
    29
apply (frule mem_Lset_imp_subset_Lset)
wenzelm@13428
    30
apply (simp add: Collect_conj_in_DPow Collect_mem_eq
paulson@13306
    31
                 subset_Int_iff2 elem_subset_in_DPow)
paulson@13306
    32
done
paulson@13306
    33
paulson@13306
    34
lemma separation_CollectI:
paulson@13306
    35
     "(\<And>z. L(z) ==> L({x \<in> z . P(x)})) ==> separation(L, \<lambda>x. P(x))"
wenzelm@13428
    36
apply (unfold separation_def, clarify)
wenzelm@13428
    37
apply (rule_tac x="{x\<in>z. P(x)}" in rexI)
paulson@13306
    38
apply simp_all
paulson@13306
    39
done
paulson@13306
    40
paulson@13306
    41
text{*Reduces the original comprehension to the reflected one*}
paulson@13306
    42
lemma reflection_imp_L_separation:
paulson@13306
    43
      "[| \<forall>x\<in>Lset(j). P(x) <-> Q(x);
wenzelm@13428
    44
          {x \<in> Lset(j) . Q(x)} \<in> DPow(Lset(j));
paulson@13306
    45
          Ord(j);  z \<in> Lset(j)|] ==> L({x \<in> z . P(x)})"
paulson@13306
    46
apply (rule_tac i = "succ(j)" in L_I)
paulson@13306
    47
 prefer 2 apply simp
paulson@13306
    48
apply (subgoal_tac "{x \<in> z. P(x)} = {x \<in> Lset(j). x \<in> z & (Q(x))}")
paulson@13306
    49
 prefer 2
wenzelm@13428
    50
 apply (blast dest: mem_Lset_imp_subset_Lset)
paulson@13306
    51
apply (simp add: Lset_succ Collect_conj_in_DPow_Lset)
paulson@13306
    52
done
paulson@13306
    53
paulson@13306
    54
paulson@13316
    55
subsection{*Separation for Intersection*}
paulson@13306
    56
paulson@13306
    57
lemma Inter_Reflects:
wenzelm@13428
    58
     "REFLECTS[\<lambda>x. \<forall>y[L]. y\<in>A --> x \<in> y,
paulson@13314
    59
               \<lambda>i x. \<forall>y\<in>Lset(i). y\<in>A --> x \<in> y]"
wenzelm@13428
    60
by (intro FOL_reflections)
paulson@13306
    61
paulson@13306
    62
lemma Inter_separation:
paulson@13306
    63
     "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
wenzelm@13428
    64
apply (rule separation_CollectI)
wenzelm@13428
    65
apply (rule_tac A="{A,z}" in subset_LsetE, blast )
paulson@13306
    66
apply (rule ReflectsE [OF Inter_Reflects], assumption)
wenzelm@13428
    67
apply (drule subset_Lset_ltD, assumption)
paulson@13306
    68
apply (erule reflection_imp_L_separation)
paulson@13306
    69
  apply (simp_all add: lt_Ord2, clarify)
wenzelm@13428
    70
apply (rule DPow_LsetI)
wenzelm@13428
    71
apply (rule ball_iff_sats)
paulson@13306
    72
apply (rule imp_iff_sats)
paulson@13306
    73
apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
paulson@13306
    74
apply (rule_tac i=0 and j=2 in mem_iff_sats)
paulson@13306
    75
apply (simp_all add: succ_Un_distrib [symmetric])
paulson@13306
    76
done
paulson@13306
    77
paulson@13437
    78
subsection{*Separation for Set Difference*}
paulson@13437
    79
paulson@13437
    80
lemma Diff_Reflects:
paulson@13437
    81
     "REFLECTS[\<lambda>x. x \<notin> B, \<lambda>i x. x \<notin> B]"
paulson@13437
    82
by (intro FOL_reflections)  
paulson@13437
    83
paulson@13437
    84
lemma Diff_separation:
paulson@13437
    85
     "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
paulson@13437
    86
apply (rule separation_CollectI) 
paulson@13437
    87
apply (rule_tac A="{B,z}" in subset_LsetE, blast ) 
paulson@13437
    88
apply (rule ReflectsE [OF Diff_Reflects], assumption)
paulson@13437
    89
apply (drule subset_Lset_ltD, assumption) 
paulson@13437
    90
apply (erule reflection_imp_L_separation)
paulson@13437
    91
  apply (simp_all add: lt_Ord2, clarify)
paulson@13437
    92
apply (rule DPow_LsetI) 
paulson@13437
    93
apply (rule not_iff_sats) 
paulson@13437
    94
apply (rule_tac env="[x,B]" in mem_iff_sats)
paulson@13437
    95
apply (rule sep_rules | simp)+
paulson@13437
    96
done
paulson@13437
    97
paulson@13316
    98
subsection{*Separation for Cartesian Product*}
paulson@13306
    99
paulson@13323
   100
lemma cartprod_Reflects:
paulson@13314
   101
     "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)),
wenzelm@13428
   102
                \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). y\<in>B &
paulson@13314
   103
                                   pair(**Lset(i),x,y,z))]"
paulson@13323
   104
by (intro FOL_reflections function_reflections)
paulson@13306
   105
paulson@13306
   106
lemma cartprod_separation:
wenzelm@13428
   107
     "[| L(A); L(B) |]
paulson@13306
   108
      ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
wenzelm@13428
   109
apply (rule separation_CollectI)
wenzelm@13428
   110
apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
paulson@13306
   111
apply (rule ReflectsE [OF cartprod_Reflects], assumption)
wenzelm@13428
   112
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   113
apply (erule reflection_imp_L_separation)
wenzelm@13428
   114
  apply (simp_all add: lt_Ord2, clarify)
paulson@13385
   115
apply (rule DPow_LsetI)
wenzelm@13428
   116
apply (rename_tac u)
wenzelm@13428
   117
apply (rule bex_iff_sats)
paulson@13306
   118
apply (rule conj_iff_sats)
paulson@13306
   119
apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
paulson@13316
   120
apply (rule sep_rules | simp)+
paulson@13306
   121
done
paulson@13306
   122
paulson@13316
   123
subsection{*Separation for Image*}
paulson@13306
   124
paulson@13306
   125
lemma image_Reflects:
paulson@13314
   126
     "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)),
paulson@13314
   127
           \<lambda>i y. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). x\<in>A & pair(**Lset(i),x,y,p))]"
paulson@13323
   128
by (intro FOL_reflections function_reflections)
paulson@13306
   129
paulson@13306
   130
lemma image_separation:
wenzelm@13428
   131
     "[| L(A); L(r) |]
paulson@13306
   132
      ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
wenzelm@13428
   133
apply (rule separation_CollectI)
wenzelm@13428
   134
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
paulson@13306
   135
apply (rule ReflectsE [OF image_Reflects], assumption)
wenzelm@13428
   136
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   137
apply (erule reflection_imp_L_separation)
paulson@13306
   138
  apply (simp_all add: lt_Ord2, clarify)
paulson@13385
   139
apply (rule DPow_LsetI)
wenzelm@13428
   140
apply (rule bex_iff_sats)
paulson@13306
   141
apply (rule conj_iff_sats)
paulson@13306
   142
apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
paulson@13316
   143
apply (rule sep_rules | simp)+
paulson@13306
   144
done
paulson@13306
   145
paulson@13306
   146
paulson@13316
   147
subsection{*Separation for Converse*}
paulson@13306
   148
paulson@13306
   149
lemma converse_Reflects:
paulson@13314
   150
  "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)),
wenzelm@13428
   151
     \<lambda>i z. \<exists>p\<in>Lset(i). p\<in>r & (\<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i).
paulson@13314
   152
                     pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]"
paulson@13323
   153
by (intro FOL_reflections function_reflections)
paulson@13306
   154
paulson@13306
   155
lemma converse_separation:
wenzelm@13428
   156
     "L(r) ==> separation(L,
paulson@13306
   157
         \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
wenzelm@13428
   158
apply (rule separation_CollectI)
wenzelm@13428
   159
apply (rule_tac A="{r,z}" in subset_LsetE, blast )
paulson@13306
   160
apply (rule ReflectsE [OF converse_Reflects], assumption)
wenzelm@13428
   161
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   162
apply (erule reflection_imp_L_separation)
paulson@13306
   163
  apply (simp_all add: lt_Ord2, clarify)
paulson@13385
   164
apply (rule DPow_LsetI)
wenzelm@13428
   165
apply (rename_tac u)
wenzelm@13428
   166
apply (rule bex_iff_sats)
paulson@13306
   167
apply (rule conj_iff_sats)
paulson@13339
   168
apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
paulson@13316
   169
apply (rule sep_rules | simp)+
paulson@13306
   170
done
paulson@13306
   171
paulson@13306
   172
paulson@13316
   173
subsection{*Separation for Restriction*}
paulson@13306
   174
paulson@13306
   175
lemma restrict_Reflects:
paulson@13314
   176
     "REFLECTS[\<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)),
paulson@13314
   177
        \<lambda>i z. \<exists>x\<in>Lset(i). x\<in>A & (\<exists>y\<in>Lset(i). pair(**Lset(i),x,y,z))]"
paulson@13323
   178
by (intro FOL_reflections function_reflections)
paulson@13306
   179
paulson@13306
   180
lemma restrict_separation:
paulson@13306
   181
   "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
wenzelm@13428
   182
apply (rule separation_CollectI)
wenzelm@13428
   183
apply (rule_tac A="{A,z}" in subset_LsetE, blast )
paulson@13306
   184
apply (rule ReflectsE [OF restrict_Reflects], assumption)
wenzelm@13428
   185
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   186
apply (erule reflection_imp_L_separation)
paulson@13306
   187
  apply (simp_all add: lt_Ord2, clarify)
paulson@13385
   188
apply (rule DPow_LsetI)
wenzelm@13428
   189
apply (rename_tac u)
wenzelm@13428
   190
apply (rule bex_iff_sats)
paulson@13306
   191
apply (rule conj_iff_sats)
paulson@13339
   192
apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
paulson@13316
   193
apply (rule sep_rules | simp)+
paulson@13306
   194
done
paulson@13306
   195
paulson@13306
   196
paulson@13316
   197
subsection{*Separation for Composition*}
paulson@13306
   198
paulson@13306
   199
lemma comp_Reflects:
wenzelm@13428
   200
     "REFLECTS[\<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
wenzelm@13428
   201
                  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
paulson@13306
   202
                  xy\<in>s & yz\<in>r,
wenzelm@13428
   203
        \<lambda>i xz. \<exists>x\<in>Lset(i). \<exists>y\<in>Lset(i). \<exists>z\<in>Lset(i). \<exists>xy\<in>Lset(i). \<exists>yz\<in>Lset(i).
wenzelm@13428
   204
                  pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) &
paulson@13314
   205
                  pair(**Lset(i),y,z,yz) & xy\<in>s & yz\<in>r]"
paulson@13323
   206
by (intro FOL_reflections function_reflections)
paulson@13306
   207
paulson@13306
   208
lemma comp_separation:
paulson@13306
   209
     "[| L(r); L(s) |]
wenzelm@13428
   210
      ==> separation(L, \<lambda>xz. \<exists>x[L]. \<exists>y[L]. \<exists>z[L]. \<exists>xy[L]. \<exists>yz[L].
wenzelm@13428
   211
                  pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
paulson@13306
   212
                  xy\<in>s & yz\<in>r)"
wenzelm@13428
   213
apply (rule separation_CollectI)
wenzelm@13428
   214
apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
paulson@13306
   215
apply (rule ReflectsE [OF comp_Reflects], assumption)
wenzelm@13428
   216
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   217
apply (erule reflection_imp_L_separation)
paulson@13306
   218
  apply (simp_all add: lt_Ord2, clarify)
paulson@13385
   219
apply (rule DPow_LsetI)
wenzelm@13428
   220
apply (rename_tac u)
paulson@13306
   221
apply (rule bex_iff_sats)+
wenzelm@13428
   222
apply (rename_tac x y z)
paulson@13306
   223
apply (rule conj_iff_sats)
paulson@13306
   224
apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
paulson@13316
   225
apply (rule sep_rules | simp)+
paulson@13306
   226
done
paulson@13306
   227
paulson@13316
   228
subsection{*Separation for Predecessors in an Order*}
paulson@13306
   229
paulson@13306
   230
lemma pred_Reflects:
paulson@13314
   231
     "REFLECTS[\<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p),
paulson@13314
   232
                    \<lambda>i y. \<exists>p \<in> Lset(i). p\<in>r & pair(**Lset(i),y,x,p)]"
paulson@13323
   233
by (intro FOL_reflections function_reflections)
paulson@13306
   234
paulson@13306
   235
lemma pred_separation:
paulson@13306
   236
     "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
wenzelm@13428
   237
apply (rule separation_CollectI)
wenzelm@13428
   238
apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
paulson@13306
   239
apply (rule ReflectsE [OF pred_Reflects], assumption)
wenzelm@13428
   240
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   241
apply (erule reflection_imp_L_separation)
paulson@13306
   242
  apply (simp_all add: lt_Ord2, clarify)
paulson@13385
   243
apply (rule DPow_LsetI)
wenzelm@13428
   244
apply (rename_tac u)
paulson@13306
   245
apply (rule bex_iff_sats)
paulson@13306
   246
apply (rule conj_iff_sats)
wenzelm@13428
   247
apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats)
paulson@13316
   248
apply (rule sep_rules | simp)+
paulson@13306
   249
done
paulson@13306
   250
paulson@13306
   251
paulson@13316
   252
subsection{*Separation for the Membership Relation*}
paulson@13306
   253
paulson@13306
   254
lemma Memrel_Reflects:
paulson@13314
   255
     "REFLECTS[\<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y,
paulson@13314
   256
            \<lambda>i z. \<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). pair(**Lset(i),x,y,z) & x \<in> y]"
paulson@13323
   257
by (intro FOL_reflections function_reflections)
paulson@13306
   258
paulson@13306
   259
lemma Memrel_separation:
paulson@13306
   260
     "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
wenzelm@13428
   261
apply (rule separation_CollectI)
wenzelm@13428
   262
apply (rule_tac A="{z}" in subset_LsetE, blast )
paulson@13306
   263
apply (rule ReflectsE [OF Memrel_Reflects], assumption)
wenzelm@13428
   264
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   265
apply (erule reflection_imp_L_separation)
paulson@13306
   266
  apply (simp_all add: lt_Ord2)
paulson@13385
   267
apply (rule DPow_LsetI)
wenzelm@13428
   268
apply (rename_tac u)
paulson@13316
   269
apply (rule bex_iff_sats conj_iff_sats)+
wenzelm@13428
   270
apply (rule_tac env = "[y,x,u]" in pair_iff_sats)
paulson@13316
   271
apply (rule sep_rules | simp)+
paulson@13306
   272
done
paulson@13306
   273
paulson@13306
   274
paulson@13316
   275
subsection{*Replacement for FunSpace*}
wenzelm@13428
   276
paulson@13306
   277
lemma funspace_succ_Reflects:
wenzelm@13428
   278
 "REFLECTS[\<lambda>z. \<exists>p[L]. p\<in>A & (\<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
wenzelm@13428
   279
            pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
wenzelm@13428
   280
            upair(L,cnbf,cnbf,z)),
wenzelm@13428
   281
        \<lambda>i z. \<exists>p \<in> Lset(i). p\<in>A & (\<exists>f \<in> Lset(i). \<exists>b \<in> Lset(i).
wenzelm@13428
   282
              \<exists>nb \<in> Lset(i). \<exists>cnbf \<in> Lset(i).
wenzelm@13428
   283
                pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) &
wenzelm@13428
   284
                is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]"
paulson@13323
   285
by (intro FOL_reflections function_reflections)
paulson@13306
   286
paulson@13306
   287
lemma funspace_succ_replacement:
wenzelm@13428
   288
     "L(n) ==>
wenzelm@13428
   289
      strong_replacement(L, \<lambda>p z. \<exists>f[L]. \<exists>b[L]. \<exists>nb[L]. \<exists>cnbf[L].
paulson@13306
   290
                pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) &
paulson@13306
   291
                upair(L,cnbf,cnbf,z))"
wenzelm@13428
   292
apply (rule strong_replacementI)
wenzelm@13428
   293
apply (rule rallI)
wenzelm@13428
   294
apply (rule separation_CollectI)
wenzelm@13428
   295
apply (rule_tac A="{n,A,z}" in subset_LsetE, blast )
paulson@13306
   296
apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
wenzelm@13428
   297
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   298
apply (erule reflection_imp_L_separation)
paulson@13306
   299
  apply (simp_all add: lt_Ord2)
paulson@13385
   300
apply (rule DPow_LsetI)
wenzelm@13428
   301
apply (rename_tac u)
paulson@13306
   302
apply (rule bex_iff_sats)
paulson@13306
   303
apply (rule conj_iff_sats)
wenzelm@13428
   304
apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats)
paulson@13316
   305
apply (rule sep_rules | simp)+
paulson@13306
   306
done
paulson@13306
   307
paulson@13306
   308
paulson@13316
   309
subsection{*Separation for Order-Isomorphisms*}
paulson@13306
   310
paulson@13306
   311
lemma well_ord_iso_Reflects:
wenzelm@13428
   312
  "REFLECTS[\<lambda>x. x\<in>A -->
paulson@13314
   313
                (\<exists>y[L]. \<exists>p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r),
wenzelm@13428
   314
        \<lambda>i x. x\<in>A --> (\<exists>y \<in> Lset(i). \<exists>p \<in> Lset(i).
paulson@13314
   315
                fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \<in> r)]"
paulson@13323
   316
by (intro FOL_reflections function_reflections)
paulson@13306
   317
paulson@13306
   318
lemma well_ord_iso_separation:
wenzelm@13428
   319
     "[| L(A); L(f); L(r) |]
wenzelm@13428
   320
      ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
wenzelm@13428
   321
                     fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
wenzelm@13428
   322
apply (rule separation_CollectI)
wenzelm@13428
   323
apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast )
paulson@13306
   324
apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
wenzelm@13428
   325
apply (drule subset_Lset_ltD, assumption)
paulson@13306
   326
apply (erule reflection_imp_L_separation)
paulson@13306
   327
  apply (simp_all add: lt_Ord2)
paulson@13385
   328
apply (rule DPow_LsetI)
wenzelm@13428
   329
apply (rename_tac u)
paulson@13306
   330
apply (rule imp_iff_sats)
wenzelm@13428
   331
apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats)
paulson@13316
   332
apply (rule sep_rules | simp)+
paulson@13316
   333
done
paulson@13316
   334
paulson@13316
   335
paulson@13316
   336
subsection{*Separation for @{term "obase"}*}
paulson@13316
   337
paulson@13316
   338
lemma obase_reflects:
wenzelm@13428
   339
  "REFLECTS[\<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
wenzelm@13428
   340
             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
wenzelm@13428
   341
             order_isomorphism(L,par,r,x,mx,g),
wenzelm@13428
   342
        \<lambda>i a. \<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i). \<exists>par \<in> Lset(i).
wenzelm@13428
   343
             ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
wenzelm@13428
   344
             order_isomorphism(**Lset(i),par,r,x,mx,g)]"
paulson@13323
   345
by (intro FOL_reflections function_reflections fun_plus_reflections)
paulson@13316
   346
paulson@13316
   347
lemma obase_separation:
paulson@13316
   348
     --{*part of the order type formalization*}
wenzelm@13428
   349
     "[| L(A); L(r) |]
wenzelm@13428
   350
      ==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
wenzelm@13428
   351
             ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
wenzelm@13428
   352
             order_isomorphism(L,par,r,x,mx,g))"
wenzelm@13428
   353
apply (rule separation_CollectI)
wenzelm@13428
   354
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
paulson@13316
   355
apply (rule ReflectsE [OF obase_reflects], assumption)
wenzelm@13428
   356
apply (drule subset_Lset_ltD, assumption)
paulson@13316
   357
apply (erule reflection_imp_L_separation)
paulson@13316
   358
  apply (simp_all add: lt_Ord2)
paulson@13385
   359
apply (rule DPow_LsetI)
wenzelm@13428
   360
apply (rename_tac u)
paulson@13306
   361
apply (rule bex_iff_sats)
paulson@13306
   362
apply (rule conj_iff_sats)
wenzelm@13428
   363
apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats)
paulson@13316
   364
apply (rule sep_rules | simp)+
paulson@13316
   365
done
paulson@13316
   366
paulson@13316
   367
paulson@13319
   368
subsection{*Separation for a Theorem about @{term "obase"}*}
paulson@13316
   369
paulson@13316
   370
lemma obase_equals_reflects:
wenzelm@13428
   371
  "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
wenzelm@13428
   372
                ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
wenzelm@13428
   373
                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
wenzelm@13428
   374
                order_isomorphism(L,pxr,r,y,my,g))),
wenzelm@13428
   375
        \<lambda>i x. x\<in>A --> ~(\<exists>y \<in> Lset(i). \<exists>g \<in> Lset(i).
wenzelm@13428
   376
                ordinal(**Lset(i),y) & (\<exists>my \<in> Lset(i). \<exists>pxr \<in> Lset(i).
wenzelm@13428
   377
                membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) &
wenzelm@13428
   378
                order_isomorphism(**Lset(i),pxr,r,y,my,g)))]"
paulson@13323
   379
by (intro FOL_reflections function_reflections fun_plus_reflections)
paulson@13316
   380
paulson@13316
   381
paulson@13316
   382
lemma obase_equals_separation:
wenzelm@13428
   383
     "[| L(A); L(r) |]
wenzelm@13428
   384
      ==> separation (L, \<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].
wenzelm@13428
   385
                              ordinal(L,y) & (\<exists>my[L]. \<exists>pxr[L].
wenzelm@13428
   386
                              membership(L,y,my) & pred_set(L,A,x,r,pxr) &
wenzelm@13428
   387
                              order_isomorphism(L,pxr,r,y,my,g))))"
wenzelm@13428
   388
apply (rule separation_CollectI)
wenzelm@13428
   389
apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
paulson@13316
   390
apply (rule ReflectsE [OF obase_equals_reflects], assumption)
wenzelm@13428
   391
apply (drule subset_Lset_ltD, assumption)
paulson@13316
   392
apply (erule reflection_imp_L_separation)
paulson@13316
   393
  apply (simp_all add: lt_Ord2)
paulson@13385
   394
apply (rule DPow_LsetI)
wenzelm@13428
   395
apply (rename_tac u)
paulson@13316
   396
apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
wenzelm@13428
   397
apply (rule_tac env = "[u,A,r]" in mem_iff_sats)
paulson@13316
   398
apply (rule sep_rules | simp)+
paulson@13316
   399
done
paulson@13316
   400
paulson@13316
   401
paulson@13316
   402
subsection{*Replacement for @{term "omap"}*}
paulson@13316
   403
paulson@13316
   404
lemma omap_reflects:
wenzelm@13428
   405
 "REFLECTS[\<lambda>z. \<exists>a[L]. a\<in>B & (\<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
wenzelm@13428
   406
     ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
paulson@13316
   407
     pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)),
wenzelm@13428
   408
 \<lambda>i z. \<exists>a \<in> Lset(i). a\<in>B & (\<exists>x \<in> Lset(i). \<exists>g \<in> Lset(i). \<exists>mx \<in> Lset(i).
wenzelm@13428
   409
        \<exists>par \<in> Lset(i).
wenzelm@13428
   410
         ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) &
wenzelm@13428
   411
         membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) &
paulson@13316
   412
         order_isomorphism(**Lset(i),par,r,x,mx,g))]"
paulson@13323
   413
by (intro FOL_reflections function_reflections fun_plus_reflections)
paulson@13316
   414
paulson@13316
   415
lemma omap_replacement:
wenzelm@13428
   416
     "[| L(A); L(r) |]
paulson@13316
   417
      ==> strong_replacement(L,
wenzelm@13428
   418
             \<lambda>a z. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
wenzelm@13428
   419
             ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
wenzelm@13428
   420
             pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
wenzelm@13428
   421
apply (rule strong_replacementI)
paulson@13316
   422
apply (rule rallI)
wenzelm@13428
   423
apply (rename_tac B)
wenzelm@13428
   424
apply (rule separation_CollectI)
wenzelm@13428
   425
apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
paulson@13316
   426
apply (rule ReflectsE [OF omap_reflects], assumption)
wenzelm@13428
   427
apply (drule subset_Lset_ltD, assumption)
paulson@13316
   428
apply (erule reflection_imp_L_separation)
paulson@13316
   429
  apply (simp_all add: lt_Ord2)
paulson@13385
   430
apply (rule DPow_LsetI)
wenzelm@13428
   431
apply (rename_tac u)
paulson@13316
   432
apply (rule bex_iff_sats conj_iff_sats)+
wenzelm@13428
   433
apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats)
paulson@13316
   434
apply (rule sep_rules | simp)+
paulson@13306
   435
done
paulson@13306
   436
paulson@13323
   437
paulson@13323
   438
subsection{*Separation for a Theorem about @{term "obase"}*}
paulson@13323
   439
paulson@13323
   440
lemma is_recfun_reflects:
wenzelm@13428
   441
  "REFLECTS[\<lambda>x. \<exists>xa[L]. \<exists>xb[L].
wenzelm@13428
   442
                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
wenzelm@13428
   443
                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
paulson@13323
   444
                                   fx \<noteq> gx),
wenzelm@13428
   445
   \<lambda>i x. \<exists>xa \<in> Lset(i). \<exists>xb \<in> Lset(i).
paulson@13323
   446
          pair(**Lset(i),x,a,xa) & xa \<in> r & pair(**Lset(i),x,b,xb) & xb \<in> r &
wenzelm@13428
   447
                (\<exists>fx \<in> Lset(i). \<exists>gx \<in> Lset(i). fun_apply(**Lset(i),f,x,fx) &
paulson@13323
   448
                  fun_apply(**Lset(i),g,x,gx) & fx \<noteq> gx)]"
paulson@13323
   449
by (intro FOL_reflections function_reflections fun_plus_reflections)
paulson@13323
   450
paulson@13323
   451
lemma is_recfun_separation:
paulson@13323
   452
     --{*for well-founded recursion*}
wenzelm@13428
   453
     "[| L(r); L(f); L(g); L(a); L(b) |]
wenzelm@13428
   454
     ==> separation(L,
wenzelm@13428
   455
            \<lambda>x. \<exists>xa[L]. \<exists>xb[L].
wenzelm@13428
   456
                pair(L,x,a,xa) & xa \<in> r & pair(L,x,b,xb) & xb \<in> r &
wenzelm@13428
   457
                (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
paulson@13323
   458
                                   fx \<noteq> gx))"
wenzelm@13428
   459
apply (rule separation_CollectI)
wenzelm@13428
   460
apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast )
paulson@13323
   461
apply (rule ReflectsE [OF is_recfun_reflects], assumption)
wenzelm@13428
   462
apply (drule subset_Lset_ltD, assumption)
paulson@13323
   463
apply (erule reflection_imp_L_separation)
paulson@13323
   464
  apply (simp_all add: lt_Ord2)
paulson@13385
   465
apply (rule DPow_LsetI)
wenzelm@13428
   466
apply (rename_tac u)
paulson@13323
   467
apply (rule bex_iff_sats conj_iff_sats)+
wenzelm@13428
   468
apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats)
paulson@13323
   469
apply (rule sep_rules | simp)+
paulson@13323
   470
done
paulson@13323
   471
paulson@13323
   472
paulson@13363
   473
subsection{*Instantiating the locale @{text M_axioms}*}
paulson@13363
   474
text{*Separation (and Strong Replacement) for basic set-theoretic constructions
paulson@13363
   475
such as intersection, Cartesian Product and image.*}
paulson@13363
   476
paulson@13437
   477
lemma M_axioms_axioms_L: "M_axioms_axioms(L)"
wenzelm@13428
   478
  apply (rule M_axioms_axioms.intro)
paulson@13437
   479
       apply (assumption | rule
paulson@13437
   480
	 Inter_separation Diff_separation cartprod_separation image_separation
paulson@13437
   481
	 converse_separation restrict_separation
paulson@13437
   482
	 comp_separation pred_separation Memrel_separation
paulson@13437
   483
	 funspace_succ_replacement well_ord_iso_separation
paulson@13437
   484
	 obase_separation obase_equals_separation
paulson@13437
   485
	 omap_replacement is_recfun_separation)+
wenzelm@13428
   486
  done
paulson@13323
   487
paulson@13437
   488
theorem M_axioms_L: "PROP M_axioms(L)"
paulson@13437
   489
by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L])
paulson@13437
   490
paulson@13437
   491
wenzelm@13428
   492
lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
wenzelm@13428
   493
  and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
wenzelm@13428
   494
  and sum_closed = M_axioms.sum_closed [OF M_axioms_L]
wenzelm@13428
   495
  and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L]
wenzelm@13428
   496
  and converse_closed = M_axioms.converse_closed [OF M_axioms_L]
wenzelm@13428
   497
  and converse_abs = M_axioms.converse_abs [OF M_axioms_L]
wenzelm@13428
   498
  and image_closed = M_axioms.image_closed [OF M_axioms_L]
wenzelm@13428
   499
  and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L]
wenzelm@13428
   500
  and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L]
wenzelm@13428
   501
  and domain_abs = M_axioms.domain_abs [OF M_axioms_L]
wenzelm@13428
   502
  and domain_closed = M_axioms.domain_closed [OF M_axioms_L]
wenzelm@13428
   503
  and range_abs = M_axioms.range_abs [OF M_axioms_L]
wenzelm@13428
   504
  and range_closed = M_axioms.range_closed [OF M_axioms_L]
wenzelm@13428
   505
  and field_abs = M_axioms.field_abs [OF M_axioms_L]
wenzelm@13428
   506
  and field_closed = M_axioms.field_closed [OF M_axioms_L]
wenzelm@13428
   507
  and relation_abs = M_axioms.relation_abs [OF M_axioms_L]
wenzelm@13428
   508
  and function_abs = M_axioms.function_abs [OF M_axioms_L]
wenzelm@13428
   509
  and apply_closed = M_axioms.apply_closed [OF M_axioms_L]
wenzelm@13428
   510
  and apply_abs = M_axioms.apply_abs [OF M_axioms_L]
wenzelm@13428
   511
  and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L]
wenzelm@13428
   512
  and injection_abs = M_axioms.injection_abs [OF M_axioms_L]
wenzelm@13428
   513
  and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L]
wenzelm@13428
   514
  and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L]
wenzelm@13428
   515
  and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L]
wenzelm@13428
   516
  and comp_closed = M_axioms.comp_closed [OF M_axioms_L]
wenzelm@13428
   517
  and composition_abs = M_axioms.composition_abs [OF M_axioms_L]
wenzelm@13428
   518
  and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L]
wenzelm@13428
   519
  and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L]
wenzelm@13428
   520
  and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L]
wenzelm@13428
   521
  and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L]
wenzelm@13428
   522
  and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L]
wenzelm@13428
   523
  and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L]
wenzelm@13428
   524
  and Int_closed = M_axioms.Int_closed [OF M_axioms_L]
wenzelm@13428
   525
  and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L]
wenzelm@13428
   526
  and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L]
wenzelm@13428
   527
  and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L]
wenzelm@13428
   528
  and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L]
wenzelm@13428
   529
  and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L]
paulson@13323
   530
wenzelm@13428
   531
lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L]
wenzelm@13428
   532
  and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L]
wenzelm@13428
   533
  and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L]
wenzelm@13428
   534
  and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L]
wenzelm@13428
   535
  and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L]
wenzelm@13428
   536
  and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L]
wenzelm@13428
   537
  and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L]
wenzelm@13428
   538
  and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L]
wenzelm@13428
   539
  and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L]
wenzelm@13428
   540
  and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L]
wenzelm@13428
   541
  and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L]
wenzelm@13428
   542
  and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L]
wenzelm@13428
   543
  and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L]
wenzelm@13428
   544
  and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L]
wenzelm@13428
   545
  and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L]
wenzelm@13428
   546
  and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L]
wenzelm@13428
   547
  and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L]
wenzelm@13428
   548
  and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L]
wenzelm@13428
   549
  and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L]
wenzelm@13428
   550
  and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L]
wenzelm@13428
   551
  and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L]
wenzelm@13428
   552
  and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L]
wenzelm@13428
   553
  and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L]
wenzelm@13428
   554
  and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L]
wenzelm@13428
   555
  and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L]
wenzelm@13428
   556
  and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L]
wenzelm@13428
   557
  and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L]
wenzelm@13428
   558
  and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L]
wenzelm@13428
   559
  and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L]
wenzelm@13428
   560
  and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L]
wenzelm@13428
   561
  and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L]
wenzelm@13428
   562
  and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L]
paulson@13323
   563
wenzelm@13428
   564
lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L]
wenzelm@13428
   565
  and membership_abs = M_axioms.membership_abs [OF M_axioms_L]
wenzelm@13428
   566
  and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L]
wenzelm@13428
   567
  and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L]
wenzelm@13428
   568
  and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L]
wenzelm@13428
   569
  and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L]
wenzelm@13428
   570
  and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L]
wenzelm@13428
   571
  and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L]
wenzelm@13428
   572
  and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L]
wenzelm@13428
   573
  and obase_iff = M_axioms.obase_iff [OF M_axioms_L]
wenzelm@13428
   574
  and omap_iff = M_axioms.omap_iff [OF M_axioms_L]
wenzelm@13428
   575
  and omap_unique = M_axioms.omap_unique [OF M_axioms_L]
wenzelm@13428
   576
  and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L]
wenzelm@13428
   577
  and otype_iff = M_axioms.otype_iff [OF M_axioms_L]
wenzelm@13428
   578
  and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L]
wenzelm@13428
   579
  and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L]
wenzelm@13428
   580
  and domain_omap = M_axioms.domain_omap [OF M_axioms_L]
wenzelm@13428
   581
  and omap_subset = M_axioms.omap_subset [OF M_axioms_L]
wenzelm@13428
   582
  and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L]
wenzelm@13428
   583
  and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L]
wenzelm@13428
   584
  and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L]
wenzelm@13428
   585
  and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L]
wenzelm@13428
   586
  and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L]
wenzelm@13428
   587
  and obase_equals = M_axioms.obase_equals [OF M_axioms_L]
wenzelm@13428
   588
  and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L]
wenzelm@13428
   589
  and obase_exists = M_axioms.obase_exists [OF M_axioms_L]
wenzelm@13428
   590
  and omap_exists = M_axioms.omap_exists [OF M_axioms_L]
wenzelm@13428
   591
  and otype_exists = M_axioms.otype_exists [OF M_axioms_L]
wenzelm@13428
   592
  and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L]
wenzelm@13428
   593
  and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L]
wenzelm@13428
   594
  and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
wenzelm@13428
   595
  and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
wenzelm@13428
   596
wenzelm@13429
   597
declare cartprod_closed [intro, simp]
wenzelm@13429
   598
declare sum_closed [intro, simp]
wenzelm@13429
   599
declare converse_closed [intro, simp]
paulson@13323
   600
declare converse_abs [simp]
wenzelm@13429
   601
declare image_closed [intro, simp]
paulson@13323
   602
declare vimage_abs [simp]
wenzelm@13429
   603
declare vimage_closed [intro, simp]
paulson@13323
   604
declare domain_abs [simp]
wenzelm@13429
   605
declare domain_closed [intro, simp]
paulson@13323
   606
declare range_abs [simp]
wenzelm@13429
   607
declare range_closed [intro, simp]
paulson@13323
   608
declare field_abs [simp]
wenzelm@13429
   609
declare field_closed [intro, simp]
paulson@13323
   610
declare relation_abs [simp]
paulson@13323
   611
declare function_abs [simp]
wenzelm@13429
   612
declare apply_closed [intro, simp]
paulson@13323
   613
declare typed_function_abs [simp]
paulson@13323
   614
declare injection_abs [simp]
paulson@13323
   615
declare surjection_abs [simp]
paulson@13323
   616
declare bijection_abs [simp]
wenzelm@13429
   617
declare comp_closed [intro, simp]
paulson@13323
   618
declare composition_abs [simp]
paulson@13323
   619
declare restriction_abs [simp]
wenzelm@13429
   620
declare restrict_closed [intro, simp]
paulson@13323
   621
declare Inter_abs [simp]
wenzelm@13429
   622
declare Inter_closed [intro, simp]
wenzelm@13429
   623
declare Int_closed [intro, simp]
paulson@13323
   624
declare is_funspace_abs [simp]
wenzelm@13429
   625
declare finite_funspace_closed [intro, simp]
paulson@13440
   626
declare membership_abs [simp] 
paulson@13440
   627
declare Memrel_closed  [intro,simp]
paulson@13323
   628
paulson@13306
   629
end