src/ZF/Constructible/Rank.thy
author paulson
Mon Oct 14 11:32:00 2002 +0200 (2002-10-14)
changeset 13647 7f6f0ffc45c3
parent 13634 99a593b49b04
child 13721 2cf506c09946
permissions -rw-r--r--
tidying and reorganization
     1 (*  Title:      ZF/Constructible/Rank.thy
     2     ID:   $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header {*Absoluteness for Order Types, Rank Functions and Well-Founded 
     7          Relations*}
     8 
     9 theory Rank = WF_absolute:
    10 
    11 subsection {*Order Types: A Direct Construction by Replacement*}
    12 
    13 locale M_ordertype = M_basic +
    14 assumes well_ord_iso_separation:
    15      "[| M(A); M(f); M(r) |]
    16       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
    17 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
    18   and obase_separation:
    19      --{*part of the order type formalization*}
    20      "[| M(A); M(r) |]
    21       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
    22 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    23 	     order_isomorphism(M,par,r,x,mx,g))"
    24   and obase_equals_separation:
    25      "[| M(A); M(r) |]
    26       ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
    27 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
    28 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
    29 			      order_isomorphism(M,pxr,r,y,my,g))))"
    30   and omap_replacement:
    31      "[| M(A); M(r) |]
    32       ==> strong_replacement(M,
    33              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
    34 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
    35 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
    36 
    37 
    38 text{*Inductive argument for Kunen's Lemma I 6.1, etc.
    39       Simple proof from Halmos, page 72*}
    40 lemma  (in M_ordertype) wellordered_iso_subset_lemma: 
    41      "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
    42        M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
    43 apply (unfold wellordered_def ord_iso_def)
    44 apply (elim conjE CollectE) 
    45 apply (erule wellfounded_on_induct, assumption+)
    46  apply (insert well_ord_iso_separation [of A f r])
    47  apply (simp, clarify) 
    48 apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
    49 done
    50 
    51 
    52 text{*Kunen's Lemma I 6.1, page 14: 
    53       there's no order-isomorphism to an initial segment of a well-ordering*}
    54 lemma (in M_ordertype) wellordered_iso_predD:
    55      "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);  
    56        M(A);  M(f);  M(r) |] ==> x \<notin> A"
    57 apply (rule notI) 
    58 apply (frule wellordered_iso_subset_lemma, assumption)
    59 apply (auto elim: predE)  
    60 (*Now we know  ~ (f`x < x) *)
    61 apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
    62 (*Now we also know f`x  \<in> pred(A,x,r);  contradiction! *)
    63 apply (simp add: Order.pred_def)
    64 done
    65 
    66 
    67 lemma (in M_ordertype) wellordered_iso_pred_eq_lemma:
    68      "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
    69        wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
    70 apply (frule wellordered_is_trans_on, assumption)
    71 apply (rule notI) 
    72 apply (drule_tac x2=y and x=x and r2=r in 
    73          wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) 
    74 apply (simp add: trans_pred_pred_eq) 
    75 apply (blast intro: predI dest: transM)+
    76 done
    77 
    78 
    79 text{*Simple consequence of Lemma 6.1*}
    80 lemma (in M_ordertype) wellordered_iso_pred_eq:
    81      "[| wellordered(M,A,r);
    82        f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);   
    83        M(A);  M(f);  M(r);  a\<in>A;  c\<in>A |] ==> a=c"
    84 apply (frule wellordered_is_trans_on, assumption)
    85 apply (frule wellordered_is_linear, assumption)
    86 apply (erule_tac x=a and y=c in linearE, auto) 
    87 apply (drule ord_iso_sym)
    88 (*two symmetric cases*)
    89 apply (blast dest: wellordered_iso_pred_eq_lemma)+ 
    90 done
    91 
    92 
    93 text{*Following Kunen's Theorem I 7.6, page 17.  Note that this material is
    94 not required elsewhere.*}
    95 
    96 text{*Can't use @{text well_ord_iso_preserving} because it needs the
    97 strong premise @{term "well_ord(A,r)"}*}
    98 lemma (in M_ordertype) ord_iso_pred_imp_lt:
    99      "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   100          g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
   101          wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
   102          Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
   103       ==> i < j"
   104 apply (frule wellordered_is_trans_on, assumption)
   105 apply (frule_tac y=y in transM, assumption) 
   106 apply (rule_tac i=i and j=j in Ord_linear_lt, auto)  
   107 txt{*case @{term "i=j"} yields a contradiction*}
   108  apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in 
   109           wellordered_iso_predD [THEN notE]) 
   110    apply (blast intro: wellordered_subset [OF _ pred_subset]) 
   111   apply (simp add: trans_pred_pred_eq)
   112   apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
   113  apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
   114 txt{*case @{term "j<i"} also yields a contradiction*}
   115 apply (frule restrict_ord_iso2, assumption+) 
   116 apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
   117 apply (frule apply_type, blast intro: ltD) 
   118   --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
   119 apply (simp add: pred_iff) 
   120 apply (subgoal_tac
   121        "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 
   122                                Order.pred(A, converse(f)`j, r), r)")
   123  apply (clarify, frule wellordered_iso_pred_eq, assumption+)
   124  apply (blast dest: wellordered_asym)  
   125 apply (intro rexI)
   126  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
   127 done
   128 
   129 
   130 lemma ord_iso_converse1:
   131      "[| f: ord_iso(A,r,B,s);  <b, f`a>: s;  a:A;  b:B |] 
   132       ==> <converse(f) ` b, a> : r"
   133 apply (frule ord_iso_converse, assumption+) 
   134 apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) 
   135 apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
   136 done
   137 
   138 
   139 constdefs
   140   
   141   obase :: "[i=>o,i,i] => i"
   142        --{*the domain of @{text om}, eventually shown to equal @{text A}*}
   143    "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
   144                           g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
   145 
   146   omap :: "[i=>o,i,i,i] => o"  
   147     --{*the function that maps wosets to order types*}
   148    "omap(M,A,r,f) == 
   149 	\<forall>z[M].
   150          z \<in> f <-> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
   151                         g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
   152 
   153 
   154   otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
   155    "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
   156 
   157 
   158 text{*Can also be proved with the premise @{term "M(z)"} instead of
   159       @{term "M(f)"}, but that version is less useful.  This lemma
   160       is also more useful than the definition, @{text omap_def}.*}
   161 lemma (in M_ordertype) omap_iff:
   162      "[| omap(M,A,r,f); M(A); M(f) |] 
   163       ==> z \<in> f <->
   164           (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
   165                                 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
   166 apply (simp add: omap_def Memrel_closed pred_closed) 
   167 apply (rule iffI)
   168  apply (drule_tac [2] x=z in rspec)
   169  apply (drule_tac x=z in rspec)
   170  apply (blast dest: transM)+
   171 done
   172 
   173 lemma (in M_ordertype) omap_unique:
   174      "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" 
   175 apply (rule equality_iffI) 
   176 apply (simp add: omap_iff) 
   177 done
   178 
   179 lemma (in M_ordertype) omap_yields_Ord:
   180      "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
   181   by (simp add: omap_def)
   182 
   183 lemma (in M_ordertype) otype_iff:
   184      "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
   185       ==> x \<in> i <-> 
   186           (M(x) & Ord(x) & 
   187            (\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))"
   188 apply (auto simp add: omap_iff otype_def)
   189  apply (blast intro: transM) 
   190 apply (rule rangeI) 
   191 apply (frule transM, assumption)
   192 apply (simp add: omap_iff, blast)
   193 done
   194 
   195 lemma (in M_ordertype) otype_eq_range:
   196      "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] 
   197       ==> i = range(f)"
   198 apply (auto simp add: otype_def omap_iff)
   199 apply (blast dest: omap_unique) 
   200 done
   201 
   202 
   203 lemma (in M_ordertype) Ord_otype:
   204      "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
   205 apply (rule OrdI) 
   206 prefer 2 
   207     apply (simp add: Ord_def otype_def omap_def) 
   208     apply clarify 
   209     apply (frule pair_components_in_M, assumption) 
   210     apply blast 
   211 apply (auto simp add: Transset_def otype_iff) 
   212   apply (blast intro: transM)
   213  apply (blast intro: Ord_in_Ord) 
   214 apply (rename_tac y a g)
   215 apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 
   216 			  THEN apply_funtype],  assumption)  
   217 apply (rule_tac x="converse(g)`y" in bexI)
   218  apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 
   219 apply (safe elim!: predE) 
   220 apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM)
   221 done
   222 
   223 lemma (in M_ordertype) domain_omap:
   224      "[| omap(M,A,r,f);  M(A); M(r); M(B); M(f) |] 
   225       ==> domain(f) = obase(M,A,r)"
   226 apply (simp add: domain_closed obase_def) 
   227 apply (rule equality_iffI) 
   228 apply (simp add: domain_iff omap_iff, blast) 
   229 done
   230 
   231 lemma (in M_ordertype) omap_subset: 
   232      "[| omap(M,A,r,f); otype(M,A,r,i); 
   233        M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> obase(M,A,r) * i"
   234 apply clarify 
   235 apply (simp add: omap_iff obase_def) 
   236 apply (force simp add: otype_iff) 
   237 done
   238 
   239 lemma (in M_ordertype) omap_funtype: 
   240      "[| omap(M,A,r,f); otype(M,A,r,i); 
   241          M(A); M(r); M(f); M(i) |] ==> f \<in> obase(M,A,r) -> i"
   242 apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 
   243 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
   244 done
   245 
   246 
   247 lemma (in M_ordertype) wellordered_omap_bij:
   248      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
   249        M(A); M(r); M(f); M(i) |] ==> f \<in> bij(obase(M,A,r),i)"
   250 apply (insert omap_funtype [of A r f i]) 
   251 apply (auto simp add: bij_def inj_def) 
   252 prefer 2  apply (blast intro: fun_is_surj dest: otype_eq_range) 
   253 apply (frule_tac a=w in apply_Pair, assumption) 
   254 apply (frule_tac a=x in apply_Pair, assumption) 
   255 apply (simp add: omap_iff) 
   256 apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 
   257 done
   258 
   259 
   260 text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
   261 lemma (in M_ordertype) omap_ord_iso:
   262      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
   263        M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(obase(M,A,r),r,i,Memrel(i))"
   264 apply (rule ord_isoI)
   265  apply (erule wellordered_omap_bij, assumption+) 
   266 apply (insert omap_funtype [of A r f i], simp) 
   267 apply (frule_tac a=x in apply_Pair, assumption) 
   268 apply (frule_tac a=y in apply_Pair, assumption) 
   269 apply (auto simp add: omap_iff)
   270  txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
   271  apply (blast intro: ltD ord_iso_pred_imp_lt)
   272  txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
   273 apply (rename_tac x y g ga) 
   274 apply (frule wellordered_is_linear, assumption, 
   275        erule_tac x=x and y=y in linearE, assumption+) 
   276 txt{*the case @{term "x=y"} leads to immediate contradiction*} 
   277 apply (blast elim: mem_irrefl) 
   278 txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
   279 apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 
   280 done
   281 
   282 lemma (in M_ordertype) Ord_omap_image_pred:
   283      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
   284        M(A); M(r); M(f); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
   285 apply (frule wellordered_is_trans_on, assumption)
   286 apply (rule OrdI) 
   287 	prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
   288 txt{*Hard part is to show that the image is a transitive set.*}
   289 apply (simp add: Transset_def, clarify) 
   290 apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f i]])
   291 apply (rename_tac c j, clarify)
   292 apply (frule omap_funtype [of A r f, THEN apply_funtype], assumption+)
   293 apply (subgoal_tac "j : i") 
   294 	prefer 2 apply (blast intro: Ord_trans Ord_otype)
   295 apply (subgoal_tac "converse(f) ` j : obase(M,A,r)") 
   296 	prefer 2 
   297 	apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, 
   298                                       THEN bij_is_fun, THEN apply_funtype])
   299 apply (rule_tac x="converse(f) ` j" in bexI) 
   300  apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) 
   301 apply (intro predI conjI)
   302  apply (erule_tac b=c in trans_onD) 
   303  apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f i]])
   304 apply (auto simp add: obase_def)
   305 done
   306 
   307 lemma (in M_ordertype) restrict_omap_ord_iso:
   308      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
   309        D \<subseteq> obase(M,A,r); M(A); M(r); M(f); M(i) |] 
   310       ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
   311 apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f i]], 
   312        assumption+)
   313 apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) 
   314 apply (blast dest: subsetD [OF omap_subset]) 
   315 apply (drule ord_iso_sym, simp) 
   316 done
   317 
   318 lemma (in M_ordertype) obase_equals: 
   319      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
   320        M(A); M(r); M(f); M(i) |] ==> obase(M,A,r) = A"
   321 apply (rule equalityI, force simp add: obase_def, clarify) 
   322 apply (unfold obase_def, simp) 
   323 apply (frule wellordered_is_wellfounded_on, assumption)
   324 apply (erule wellfounded_on_induct, assumption+)
   325  apply (frule obase_equals_separation [of A r], assumption) 
   326  apply (simp, clarify) 
   327 apply (rename_tac b) 
   328 apply (subgoal_tac "Order.pred(A,b,r) <= obase(M,A,r)") 
   329  apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred)
   330 apply (force simp add: pred_iff obase_def)  
   331 done
   332 
   333 
   334 
   335 text{*Main result: @{term om} gives the order-isomorphism 
   336       @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
   337 theorem (in M_ordertype) omap_ord_iso_otype:
   338      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
   339        M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
   340 apply (frule omap_ord_iso, assumption+)
   341 apply (simp add: obase_equals)  
   342 done 
   343 
   344 lemma (in M_ordertype) obase_exists:
   345      "[| M(A); M(r) |] ==> M(obase(M,A,r))"
   346 apply (simp add: obase_def) 
   347 apply (insert obase_separation [of A r])
   348 apply (simp add: separation_def)  
   349 done
   350 
   351 lemma (in M_ordertype) omap_exists:
   352      "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"
   353 apply (simp add: omap_def) 
   354 apply (insert omap_replacement [of A r])
   355 apply (simp add: strong_replacement_def) 
   356 apply (drule_tac x="obase(M,A,r)" in rspec) 
   357  apply (simp add: obase_exists) 
   358 apply (simp add: Memrel_closed pred_closed obase_def)
   359 apply (erule impE) 
   360  apply (clarsimp simp add: univalent_def)
   361  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
   362 apply (rule_tac x=Y in rexI) 
   363 apply (simp add: Memrel_closed pred_closed obase_def, blast, assumption)
   364 done
   365 
   366 declare rall_simps [simp] rex_simps [simp]
   367 
   368 lemma (in M_ordertype) otype_exists:
   369      "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
   370 apply (insert omap_exists [of A r])  
   371 apply (simp add: otype_def, safe)
   372 apply (rule_tac x="range(x)" in rexI) 
   373 apply blast+
   374 done
   375 
   376 lemma (in M_ordertype) ordertype_exists:
   377      "[| wellordered(M,A,r); M(A); M(r) |]
   378       ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   379 apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   380 apply (rename_tac i) 
   381 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
   382 apply (rule Ord_otype) 
   383     apply (force simp add: otype_def range_closed) 
   384    apply (simp_all add: wellordered_is_trans_on) 
   385 done
   386 
   387 
   388 lemma (in M_ordertype) relativized_imp_well_ord: 
   389      "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
   390 apply (insert ordertype_exists [of A r], simp)
   391 apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
   392 done
   393 
   394 subsection {*Kunen's theorem 5.4, page 127*}
   395 
   396 text{*(a) The notion of Wellordering is absolute*}
   397 theorem (in M_ordertype) well_ord_abs [simp]: 
   398      "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" 
   399 by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)  
   400 
   401 
   402 text{*(b) Order types are absolute*}
   403 theorem (in M_ordertype) 
   404      "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
   405        M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
   406 by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
   407                  Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
   408 
   409 
   410 subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
   411 
   412 text{*Note: the remainder of this theory is not needed elsewhere.*}
   413 
   414 subsubsection{*Ordinal Addition*}
   415 
   416 (*FIXME: update to use new techniques!!*)
   417 constdefs
   418  (*This expresses ordinal addition in the language of ZF.  It also 
   419    provides an abbreviation that can be used in the instance of strong
   420    replacement below.  Here j is used to define the relation, namely
   421    Memrel(succ(j)), while x determines the domain of f.*)
   422  is_oadd_fun :: "[i=>o,i,i,i,i] => o"
   423     "is_oadd_fun(M,i,j,x,f) == 
   424        (\<forall>sj msj. M(sj) --> M(msj) --> 
   425                  successor(M,j,sj) --> membership(M,sj,msj) --> 
   426 	         M_is_recfun(M, 
   427 		     %x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y),
   428 		     msj, x, f))"
   429 
   430  is_oadd :: "[i=>o,i,i,i] => o"
   431     "is_oadd(M,i,j,k) == 
   432         (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) |
   433         (~ ordinal(M,i) & ordinal(M,j) & k=j) |
   434         (ordinal(M,i) & ~ ordinal(M,j) & k=i) |
   435         (ordinal(M,i) & ordinal(M,j) & 
   436 	 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
   437 		    successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & 
   438 		    fun_apply(M,f,j,fj) & fj = k))"
   439 
   440  (*NEEDS RELATIVIZATION*)
   441  omult_eqns :: "[i,i,i,i] => o"
   442     "omult_eqns(i,x,g,z) ==
   443             Ord(x) & 
   444 	    (x=0 --> z=0) &
   445             (\<forall>j. x = succ(j) --> z = g`j ++ i) &
   446             (Limit(x) --> z = \<Union>(g``x))"
   447 
   448  is_omult_fun :: "[i=>o,i,i,i] => o"
   449     "is_omult_fun(M,i,j,f) == 
   450 	    (\<exists>df. M(df) & is_function(M,f) & 
   451                   is_domain(M,f,df) & subset(M, j, df)) & 
   452             (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))"
   453 
   454  is_omult :: "[i=>o,i,i,i] => o"
   455     "is_omult(M,i,j,k) == 
   456 	\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
   457                   successor(M,j,sj) & is_omult_fun(M,i,sj,f) & 
   458                   fun_apply(M,f,j,fj) & fj = k"
   459 
   460 
   461 locale M_ord_arith = M_ordertype +
   462   assumes oadd_strong_replacement:
   463    "[| M(i); M(j) |] ==>
   464     strong_replacement(M, 
   465          \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & 
   466                   (\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & 
   467 		           image(M,f,x,fx) & y = i Un fx))"
   468 
   469  and omult_strong_replacement':
   470    "[| M(i); M(j) |] ==>
   471     strong_replacement(M, 
   472          \<lambda>x z. \<exists>y[M]. z = <x,y> &
   473 	     (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
   474 	     y = (THE z. omult_eqns(i, x, g, z))))" 
   475 
   476 
   477 
   478 text{*@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF*}
   479 lemma (in M_ord_arith) is_oadd_fun_iff:
   480    "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
   481     ==> is_oadd_fun(M,i,j,a,f) <->
   482 	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
   483 apply (frule lt_Ord) 
   484 apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
   485              relation2_def is_recfun_abs [of "%x g. i Un g``x"]
   486              image_closed is_recfun_iff_equation  
   487              Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
   488 apply (simp add: lt_def) 
   489 apply (blast dest: transM) 
   490 done
   491 
   492 
   493 lemma (in M_ord_arith) oadd_strong_replacement':
   494     "[| M(i); M(j) |] ==>
   495      strong_replacement(M, 
   496             \<lambda>x z. \<exists>y[M]. z = <x,y> &
   497 		  (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
   498 		  y = i Un g``x))" 
   499 apply (insert oadd_strong_replacement [of i j]) 
   500 apply (simp add: is_oadd_fun_def relation2_def
   501                  is_recfun_abs [of "%x g. i Un g``x"])  
   502 done
   503 
   504 
   505 lemma (in M_ord_arith) exists_oadd:
   506     "[| Ord(j);  M(i);  M(j) |]
   507      ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
   508 apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
   509     apply (simp_all add: Memrel_type oadd_strong_replacement') 
   510 done 
   511 
   512 lemma (in M_ord_arith) exists_oadd_fun:
   513     "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)"
   514 apply (rule exists_oadd [THEN rexE])
   515 apply (erule Ord_succ, assumption, simp) 
   516 apply (rename_tac f) 
   517 apply (frule is_recfun_type)
   518 apply (rule_tac x=f in rexI) 
   519  apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   520                   is_oadd_fun_iff Ord_trans [OF _ succI1], assumption)
   521 done
   522 
   523 lemma (in M_ord_arith) is_oadd_fun_apply:
   524     "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] 
   525      ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
   526 apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 
   527 apply (frule lt_closed, simp)
   528 apply (frule leI [THEN le_imp_subset])  
   529 apply (simp add: image_fun, blast) 
   530 done
   531 
   532 lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]:
   533     "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
   534      ==> j<J --> f`j = i++j"
   535 apply (erule_tac i=j in trans_induct, clarify) 
   536 apply (subgoal_tac "\<forall>k\<in>x. k<J")
   537  apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply)
   538 apply (blast intro: lt_trans ltI lt_Ord) 
   539 done
   540 
   541 lemma (in M_ord_arith) Ord_oadd_abs:
   542     "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
   543 apply (simp add: is_oadd_def is_oadd_fun_iff_oadd)
   544 apply (frule exists_oadd_fun [of j i], blast+)
   545 done
   546 
   547 lemma (in M_ord_arith) oadd_abs:
   548     "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
   549 apply (case_tac "Ord(i) & Ord(j)")
   550  apply (simp add: Ord_oadd_abs)
   551 apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
   552 done
   553 
   554 lemma (in M_ord_arith) oadd_closed [intro,simp]:
   555     "[| M(i); M(j) |] ==> M(i++j)"
   556 apply (simp add: oadd_eq_if_raw_oadd, clarify) 
   557 apply (simp add: raw_oadd_eq_oadd) 
   558 apply (frule exists_oadd_fun [of j i], auto)
   559 apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 
   560 done
   561 
   562 
   563 subsubsection{*Ordinal Multiplication*}
   564 
   565 lemma omult_eqns_unique:
   566      "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
   567 apply (simp add: omult_eqns_def, clarify) 
   568 apply (erule Ord_cases, simp_all) 
   569 done
   570 
   571 lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0"
   572 by (simp add: omult_eqns_def)
   573 
   574 lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0"
   575 by (simp add: omult_eqns_0)
   576 
   577 lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i"
   578 by (simp add: omult_eqns_def)
   579 
   580 lemma the_omult_eqns_succ:
   581      "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i"
   582 by (simp add: omult_eqns_succ) 
   583 
   584 lemma omult_eqns_Limit:
   585      "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)"
   586 apply (simp add: omult_eqns_def) 
   587 apply (blast intro: Limit_is_Ord) 
   588 done
   589 
   590 lemma the_omult_eqns_Limit:
   591      "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)"
   592 by (simp add: omult_eqns_Limit)
   593 
   594 lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)"
   595 by (simp add: omult_eqns_def)
   596 
   597 
   598 lemma (in M_ord_arith) the_omult_eqns_closed:
   599     "[| M(i); M(x); M(g); function(g) |] 
   600      ==> M(THE z. omult_eqns(i, x, g, z))"
   601 apply (case_tac "Ord(x)")
   602  prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
   603 apply (erule Ord_cases) 
   604   apply (simp add: omult_eqns_0)
   605  apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
   606 apply (simp add: omult_eqns_Limit) 
   607 done
   608 
   609 lemma (in M_ord_arith) exists_omult:
   610     "[| Ord(j);  M(i);  M(j) |]
   611      ==> \<exists>f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
   612 apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel])
   613     apply (simp_all add: Memrel_type omult_strong_replacement') 
   614 apply (blast intro: the_omult_eqns_closed) 
   615 done
   616 
   617 lemma (in M_ord_arith) exists_omult_fun:
   618     "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f[M]. is_omult_fun(M,i,succ(j),f)"
   619 apply (rule exists_omult [THEN rexE])
   620 apply (erule Ord_succ, assumption, simp) 
   621 apply (rename_tac f) 
   622 apply (frule is_recfun_type)
   623 apply (rule_tac x=f in rexI) 
   624 apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   625                  is_omult_fun_def Ord_trans [OF _ succI1])
   626  apply (force dest: Ord_in_Ord' 
   627               simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
   628                         the_omult_eqns_Limit, assumption)
   629 done
   630 
   631 lemma (in M_ord_arith) is_omult_fun_apply_0:
   632     "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
   633 by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
   634 
   635 lemma (in M_ord_arith) is_omult_fun_apply_succ:
   636     "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
   637 by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 
   638 
   639 lemma (in M_ord_arith) is_omult_fun_apply_Limit:
   640     "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
   641      ==> f ` x = (\<Union>y\<in>x. f`y)"
   642 apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
   643 apply (drule subset_trans [OF OrdmemD], assumption+)  
   644 apply (simp add: ball_conj_distrib omult_Limit image_function)
   645 done
   646 
   647 lemma (in M_ord_arith) is_omult_fun_eq_omult:
   648     "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] 
   649      ==> j<J --> f`j = i**j"
   650 apply (erule_tac i=j in trans_induct3)
   651 apply (safe del: impCE)
   652   apply (simp add: is_omult_fun_apply_0) 
   653  apply (subgoal_tac "x<J") 
   654   apply (simp add: is_omult_fun_apply_succ omult_succ)  
   655  apply (blast intro: lt_trans) 
   656 apply (subgoal_tac "\<forall>k\<in>x. k<J")
   657  apply (simp add: is_omult_fun_apply_Limit omult_Limit) 
   658 apply (blast intro: lt_trans ltI lt_Ord) 
   659 done
   660 
   661 lemma (in M_ord_arith) omult_abs:
   662     "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
   663 apply (simp add: is_omult_def is_omult_fun_eq_omult)
   664 apply (frule exists_omult_fun [of j i], blast+)
   665 done
   666 
   667 
   668 
   669 subsection {*Absoluteness of Well-Founded Relations*}
   670 
   671 text{*Relativized to @{term M}: Every well-founded relation is a subset of some
   672 inverse image of an ordinal.  Key step is the construction (in @{term M}) of a
   673 rank function.*}
   674 
   675 locale M_wfrank = M_trancl +
   676   assumes wfrank_separation:
   677      "M(r) ==>
   678       separation (M, \<lambda>x. 
   679          \<forall>rplus[M]. tran_closure(M,r,rplus) -->
   680          ~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))"
   681  and wfrank_strong_replacement:
   682      "M(r) ==>
   683       strong_replacement(M, \<lambda>x z. 
   684          \<forall>rplus[M]. tran_closure(M,r,rplus) -->
   685          (\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z)  & 
   686                         M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) &
   687                         is_range(M,f,y)))"
   688  and Ord_wfrank_separation:
   689      "M(r) ==>
   690       separation (M, \<lambda>x.
   691          \<forall>rplus[M]. tran_closure(M,r,rplus) --> 
   692           ~ (\<forall>f[M]. \<forall>rangef[M]. 
   693              is_range(M,f,rangef) -->
   694              M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) -->
   695              ordinal(M,rangef)))" 
   696 
   697 
   698 text{*Proving that the relativized instances of Separation or Replacement
   699 agree with the "real" ones.*}
   700 
   701 lemma (in M_wfrank) wfrank_separation':
   702      "M(r) ==>
   703       separation
   704 	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
   705 apply (insert wfrank_separation [of r])
   706 apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
   707 done
   708 
   709 lemma (in M_wfrank) wfrank_strong_replacement':
   710      "M(r) ==>
   711       strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>f[M]. 
   712 		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
   713 		  y = range(f))"
   714 apply (insert wfrank_strong_replacement [of r])
   715 apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
   716 done
   717 
   718 lemma (in M_wfrank) Ord_wfrank_separation':
   719      "M(r) ==>
   720       separation (M, \<lambda>x. 
   721          ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
   722 apply (insert Ord_wfrank_separation [of r])
   723 apply (simp add: relation2_def is_recfun_abs [of "%x. range"])
   724 done
   725 
   726 text{*This function, defined using replacement, is a rank function for
   727 well-founded relations within the class M.*}
   728 constdefs
   729  wellfoundedrank :: "[i=>o,i,i] => i"
   730     "wellfoundedrank(M,r,A) ==
   731         {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
   732                        p = <x,y> & is_recfun(r^+, x, %x f. range(f), f) &
   733                        y = range(f)}"
   734 
   735 lemma (in M_wfrank) exists_wfrank:
   736     "[| wellfounded(M,r); M(a); M(r) |]
   737      ==> \<exists>f[M]. is_recfun(r^+, a, %x f. range(f), f)"
   738 apply (rule wellfounded_exists_is_recfun)
   739       apply (blast intro: wellfounded_trancl)
   740      apply (rule trans_trancl)
   741     apply (erule wfrank_separation')
   742    apply (erule wfrank_strong_replacement')
   743 apply (simp_all add: trancl_subset_times)
   744 done
   745 
   746 lemma (in M_wfrank) M_wellfoundedrank:
   747     "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))"
   748 apply (insert wfrank_strong_replacement' [of r])
   749 apply (simp add: wellfoundedrank_def)
   750 apply (rule strong_replacement_closed)
   751    apply assumption+
   752  apply (rule univalent_is_recfun)
   753    apply (blast intro: wellfounded_trancl)
   754   apply (rule trans_trancl)
   755  apply (simp add: trancl_subset_times) 
   756 apply (blast dest: transM) 
   757 done
   758 
   759 lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
   760     "[| wellfounded(M,r); a\<in>A; M(r); M(A) |]
   761      ==> \<forall>f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))"
   762 apply (drule wellfounded_trancl, assumption)
   763 apply (rule wellfounded_induct, assumption, erule (1) transM)
   764   apply simp
   765  apply (blast intro: Ord_wfrank_separation', clarify)
   766 txt{*The reasoning in both cases is that we get @{term y} such that
   767    @{term "\<langle>y, x\<rangle> \<in> r^+"}.  We find that
   768    @{term "f`y = restrict(f, r^+ -`` {y})"}. *}
   769 apply (rule OrdI [OF _ Ord_is_Transset])
   770  txt{*An ordinal is a transitive set...*}
   771  apply (simp add: Transset_def)
   772  apply clarify
   773  apply (frule apply_recfun2, assumption)
   774  apply (force simp add: restrict_iff)
   775 txt{*...of ordinals.  This second case requires the induction hyp.*}
   776 apply clarify
   777 apply (rename_tac i y)
   778 apply (frule apply_recfun2, assumption)
   779 apply (frule is_recfun_imp_in_r, assumption)
   780 apply (frule is_recfun_restrict)
   781     (*simp_all won't work*)
   782     apply (simp add: trans_trancl trancl_subset_times)+
   783 apply (drule spec [THEN mp], assumption)
   784 apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))")
   785  apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec)
   786 apply assumption
   787  apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
   788 apply (blast dest: pair_components_in_M)
   789 done
   790 
   791 lemma (in M_wfrank) Ord_range_wellfoundedrank:
   792     "[| wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A) |]
   793      ==> Ord (range(wellfoundedrank(M,r,A)))"
   794 apply (frule wellfounded_trancl, assumption)
   795 apply (frule trancl_subset_times)
   796 apply (simp add: wellfoundedrank_def)
   797 apply (rule OrdI [OF _ Ord_is_Transset])
   798  prefer 2
   799  txt{*by our previous result the range consists of ordinals.*}
   800  apply (blast intro: Ord_wfrank_range)
   801 txt{*We still must show that the range is a transitive set.*}
   802 apply (simp add: Transset_def, clarify, simp)
   803 apply (rename_tac x i f u)
   804 apply (frule is_recfun_imp_in_r, assumption)
   805 apply (subgoal_tac "M(u) & M(i) & M(x)")
   806  prefer 2 apply (blast dest: transM, clarify)
   807 apply (rule_tac a=u in rangeI)
   808 apply (rule_tac x=u in ReplaceI)
   809   apply simp 
   810   apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI)
   811    apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2)
   812   apply simp 
   813 apply blast 
   814 txt{*Unicity requirement of Replacement*}
   815 apply clarify
   816 apply (frule apply_recfun2, assumption)
   817 apply (simp add: trans_trancl is_recfun_cut)
   818 done
   819 
   820 lemma (in M_wfrank) function_wellfoundedrank:
   821     "[| wellfounded(M,r); M(r); M(A)|]
   822      ==> function(wellfoundedrank(M,r,A))"
   823 apply (simp add: wellfoundedrank_def function_def, clarify)
   824 txt{*Uniqueness: repeated below!*}
   825 apply (drule is_recfun_functional, assumption)
   826      apply (blast intro: wellfounded_trancl)
   827     apply (simp_all add: trancl_subset_times trans_trancl)
   828 done
   829 
   830 lemma (in M_wfrank) domain_wellfoundedrank:
   831     "[| wellfounded(M,r); M(r); M(A)|]
   832      ==> domain(wellfoundedrank(M,r,A)) = A"
   833 apply (simp add: wellfoundedrank_def function_def)
   834 apply (rule equalityI, auto)
   835 apply (frule transM, assumption)
   836 apply (frule_tac a=x in exists_wfrank, assumption+, clarify)
   837 apply (rule_tac b="range(f)" in domainI)
   838 apply (rule_tac x=x in ReplaceI)
   839   apply simp 
   840   apply (rule_tac x=f in rexI, blast, simp_all)
   841 txt{*Uniqueness (for Replacement): repeated above!*}
   842 apply clarify
   843 apply (drule is_recfun_functional, assumption)
   844     apply (blast intro: wellfounded_trancl)
   845     apply (simp_all add: trancl_subset_times trans_trancl)
   846 done
   847 
   848 lemma (in M_wfrank) wellfoundedrank_type:
   849     "[| wellfounded(M,r);  M(r); M(A)|]
   850      ==> wellfoundedrank(M,r,A) \<in> A -> range(wellfoundedrank(M,r,A))"
   851 apply (frule function_wellfoundedrank [of r A], assumption+)
   852 apply (frule function_imp_Pi)
   853  apply (simp add: wellfoundedrank_def relation_def)
   854  apply blast
   855 apply (simp add: domain_wellfoundedrank)
   856 done
   857 
   858 lemma (in M_wfrank) Ord_wellfoundedrank:
   859     "[| wellfounded(M,r); a \<in> A; r \<subseteq> A*A;  M(r); M(A) |]
   860      ==> Ord(wellfoundedrank(M,r,A) ` a)"
   861 by (blast intro: apply_funtype [OF wellfoundedrank_type]
   862                  Ord_in_Ord [OF Ord_range_wellfoundedrank])
   863 
   864 lemma (in M_wfrank) wellfoundedrank_eq:
   865      "[| is_recfun(r^+, a, %x. range, f);
   866          wellfounded(M,r);  a \<in> A; M(f); M(r); M(A)|]
   867       ==> wellfoundedrank(M,r,A) ` a = range(f)"
   868 apply (rule apply_equality)
   869  prefer 2 apply (blast intro: wellfoundedrank_type)
   870 apply (simp add: wellfoundedrank_def)
   871 apply (rule ReplaceI)
   872   apply (rule_tac x="range(f)" in rexI) 
   873   apply blast
   874  apply simp_all
   875 txt{*Unicity requirement of Replacement*}
   876 apply clarify
   877 apply (drule is_recfun_functional, assumption)
   878     apply (blast intro: wellfounded_trancl)
   879     apply (simp_all add: trancl_subset_times trans_trancl)
   880 done
   881 
   882 
   883 lemma (in M_wfrank) wellfoundedrank_lt:
   884      "[| <a,b> \<in> r;
   885          wellfounded(M,r); r \<subseteq> A*A;  M(r); M(A)|]
   886       ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b"
   887 apply (frule wellfounded_trancl, assumption)
   888 apply (subgoal_tac "a\<in>A & b\<in>A")
   889  prefer 2 apply blast
   890 apply (simp add: lt_def Ord_wellfoundedrank, clarify)
   891 apply (frule exists_wfrank [of concl: _ b], erule (1) transM, assumption)
   892 apply clarify
   893 apply (rename_tac fb)
   894 apply (frule is_recfun_restrict [of concl: "r^+" a])
   895     apply (rule trans_trancl, assumption)
   896    apply (simp_all add: r_into_trancl trancl_subset_times)
   897 txt{*Still the same goal, but with new @{text is_recfun} assumptions.*}
   898 apply (simp add: wellfoundedrank_eq)
   899 apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
   900    apply (simp_all add: transM [of a])
   901 txt{*We have used equations for wellfoundedrank and now must use some
   902     for  @{text is_recfun}. *}
   903 apply (rule_tac a=a in rangeI)
   904 apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
   905                  r_into_trancl apply_recfun r_into_trancl)
   906 done
   907 
   908 
   909 lemma (in M_wfrank) wellfounded_imp_subset_rvimage:
   910      "[|wellfounded(M,r); r \<subseteq> A*A; M(r); M(A)|]
   911       ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   912 apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI)
   913 apply (rule_tac x="wellfoundedrank(M,r,A)" in exI)
   914 apply (simp add: Ord_range_wellfoundedrank, clarify)
   915 apply (frule subsetD, assumption, clarify)
   916 apply (simp add: rvimage_iff wellfoundedrank_lt [THEN ltD])
   917 apply (blast intro: apply_rangeI wellfoundedrank_type)
   918 done
   919 
   920 lemma (in M_wfrank) wellfounded_imp_wf:
   921      "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)"
   922 by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage
   923           intro: wf_rvimage_Ord [THEN wf_subset])
   924 
   925 lemma (in M_wfrank) wellfounded_on_imp_wf_on:
   926      "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)"
   927 apply (simp add: wellfounded_on_iff_wellfounded wf_on_def)
   928 apply (rule wellfounded_imp_wf)
   929 apply (simp_all add: relation_def)
   930 done
   931 
   932 
   933 theorem (in M_wfrank) wf_abs:
   934      "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)"
   935 by (blast intro: wellfounded_imp_wf wf_imp_relativized)
   936 
   937 theorem (in M_wfrank) wf_on_abs:
   938      "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)"
   939 by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized)
   940 
   941 end