changed comments to text blocks, cleaned up a few proofs
authorhuffman
Thu Mar 31 00:10:35 2005 +0200 (2005-03-31 ago)
changeset 15637d2a06007ebfa
parent 15636 57c437b70521
child 15638 1fb24e545f88
changed comments to text blocks, cleaned up a few proofs
src/HOLCF/Fix.thy
     1.1 --- a/src/HOLCF/Fix.thy	Wed Mar 30 08:33:41 2005 +0200
     1.2 +++ b/src/HOLCF/Fix.thy	Thu Mar 31 00:10:35 2005 +0200
     1.3 @@ -35,53 +35,36 @@
     1.4  admw_def:      "admw P == !F. (!n. P (iterate n F UU)) -->
     1.5                              P (lub(range (%i. iterate i F UU)))" 
     1.6  
     1.7 -(*  Title:      HOLCF/Fix.ML
     1.8 -    ID:         $Id$
     1.9 -    Author:     Franz Regensburger
    1.10 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.11 -
    1.12 -fixed point operator and admissibility
    1.13 -*)
    1.14 -
    1.15 -(* ------------------------------------------------------------------------ *)
    1.16 -(* derive inductive properties of iterate from primitive recursion          *)
    1.17 -(* ------------------------------------------------------------------------ *)
    1.18 +text {* derive inductive properties of iterate from primitive recursion *}
    1.19  
    1.20  lemma iterate_Suc2: "iterate (Suc n) F x = iterate n F (F$x)"
    1.21  apply (induct_tac "n")
    1.22  apply auto
    1.23  done
    1.24  
    1.25 -(* ------------------------------------------------------------------------ *)
    1.26 -(* the sequence of function itertaions is a chain                           *)
    1.27 -(* This property is essential since monotonicity of iterate makes no sense  *)
    1.28 -(* ------------------------------------------------------------------------ *)
    1.29 +text {*
    1.30 +  The sequence of function iterations is a chain.
    1.31 +  This property is essential since monotonicity of iterate makes no sense.
    1.32 +*}
    1.33  
    1.34  lemma chain_iterate2: "x << F$x ==> chain (%i. iterate i F x)"
    1.35 -
    1.36 -apply (unfold chain_def)
    1.37 -apply (intro strip)
    1.38 +apply (rule chainI)
    1.39  apply (induct_tac "i")
    1.40  apply auto
    1.41  apply (erule monofun_cfun_arg)
    1.42  done
    1.43  
    1.44 -
    1.45  lemma chain_iterate: "chain (%i. iterate i F UU)"
    1.46  apply (rule chain_iterate2)
    1.47  apply (rule minimal)
    1.48  done
    1.49  
    1.50 -
    1.51 -(* ------------------------------------------------------------------------ *)
    1.52 -(* Kleene's fixed point theorems for continuous functions in pointed        *)
    1.53 -(* omega cpo's                                                              *)
    1.54 -(* ------------------------------------------------------------------------ *)
    1.55 -
    1.56 +text {*
    1.57 +  Kleene's fixed point theorems for continuous functions in pointed
    1.58 +  omega cpo's
    1.59 +*}
    1.60  
    1.61  lemma Ifix_eq: "Ifix F =F$(Ifix F)"
    1.62 -
    1.63 -
    1.64  apply (unfold Ifix_def)
    1.65  apply (subst contlub_cfun_arg)
    1.66  apply (rule chain_iterate)
    1.67 @@ -102,9 +85,7 @@
    1.68  apply (rule chain_iterate)
    1.69  done
    1.70  
    1.71 -
    1.72  lemma Ifix_least: "F$x=x ==> Ifix(F) << x"
    1.73 -
    1.74  apply (unfold Ifix_def)
    1.75  apply (rule is_lub_thelub)
    1.76  apply (rule chain_iterate)
    1.77 @@ -117,33 +98,27 @@
    1.78  apply (erule monofun_cfun_arg)
    1.79  done
    1.80  
    1.81 -
    1.82 -(* ------------------------------------------------------------------------ *)
    1.83 -(* monotonicity and continuity of iterate                                   *)
    1.84 -(* ------------------------------------------------------------------------ *)
    1.85 +text {* monotonicity and continuity of @{term iterate} *}
    1.86  
    1.87  lemma monofun_iterate: "monofun(iterate(i))"
    1.88 -apply (unfold monofun)
    1.89 -apply (intro strip)
    1.90 +apply (rule monofunI [rule_format])
    1.91  apply (induct_tac "i")
    1.92 -apply (simp (no_asm_simp))
    1.93 +apply (simp)
    1.94  apply (simp add: less_fun monofun_cfun)
    1.95  done
    1.96  
    1.97 -(* ------------------------------------------------------------------------ *)
    1.98 -(* the following lemma uses contlub_cfun which itself is based on a         *)
    1.99 -(* diagonalisation lemma for continuous functions with two arguments.       *)
   1.100 -(* In this special case it is the application function Rep_CFun                 *)
   1.101 -(* ------------------------------------------------------------------------ *)
   1.102 +text {*
   1.103 +  The following lemma uses @{thm [source] contlub_cfun} which itself is based
   1.104 +  on a diagonalisation lemma for continuous functions with two arguments. In
   1.105 +  this special case it is the application function @{term Rep_CFun}
   1.106 +*}
   1.107  
   1.108  lemma contlub_iterate: "contlub(iterate(i))"
   1.109 -
   1.110 -apply (unfold contlub)
   1.111 -apply (intro strip)
   1.112 +apply (rule contlubI [rule_format])
   1.113  apply (induct_tac "i")
   1.114 -apply (simp (no_asm_simp))
   1.115 +apply (simp)
   1.116  apply (rule lub_const [THEN thelubI, symmetric])
   1.117 -apply (simp (no_asm_simp) del: range_composition)
   1.118 +apply (simp del: range_composition)
   1.119  apply (rule ext)
   1.120  apply (simplesubst thelub_fun)
   1.121  apply (rule chainI)
   1.122 @@ -165,32 +140,27 @@
   1.123  apply (erule monofun_iterate [THEN ch2ch_monofun, THEN ch2ch_fun])
   1.124  done
   1.125  
   1.126 -
   1.127  lemma cont_iterate: "cont(iterate(i))"
   1.128  apply (rule monocontlub2cont)
   1.129  apply (rule monofun_iterate)
   1.130  apply (rule contlub_iterate)
   1.131  done
   1.132  
   1.133 -(* ------------------------------------------------------------------------ *)
   1.134 -(* a lemma about continuity of iterate in its third argument                *)
   1.135 -(* ------------------------------------------------------------------------ *)
   1.136 +text {* a lemma about continuity of @{term iterate} in its third argument *}
   1.137  
   1.138  lemma monofun_iterate2: "monofun(iterate n F)"
   1.139 -apply (rule monofunI)
   1.140 -apply (intro strip)
   1.141 +apply (rule monofunI [rule_format])
   1.142  apply (induct_tac "n")
   1.143 -apply (simp (no_asm_simp))
   1.144 -apply (simp (no_asm_simp))
   1.145 +apply (simp)
   1.146 +apply (simp)
   1.147  apply (erule monofun_cfun_arg)
   1.148  done
   1.149  
   1.150  lemma contlub_iterate2: "contlub(iterate n F)"
   1.151 -apply (rule contlubI)
   1.152 -apply (intro strip)
   1.153 +apply (rule contlubI [rule_format])
   1.154  apply (induct_tac "n")
   1.155 -apply (simp (no_asm))
   1.156 -apply (simp (no_asm))
   1.157 +apply (simp)
   1.158 +apply (simp)
   1.159  apply (rule_tac t = "iterate n F (lub (range (%u. Y u))) " and s = "lub (range (%i. iterate n F (Y i))) " in ssubst)
   1.160  apply assumption
   1.161  apply (rule contlub_cfun_arg)
   1.162 @@ -203,14 +173,11 @@
   1.163  apply (rule contlub_iterate2)
   1.164  done
   1.165  
   1.166 -(* ------------------------------------------------------------------------ *)
   1.167 -(* monotonicity and continuity of Ifix                                      *)
   1.168 -(* ------------------------------------------------------------------------ *)
   1.169 +text {* monotonicity and continuity of @{term Ifix} *}
   1.170  
   1.171  lemma monofun_Ifix: "monofun(Ifix)"
   1.172 -
   1.173 -apply (unfold monofun Ifix_def)
   1.174 -apply (intro strip)
   1.175 +apply (rule monofunI [rule_format])
   1.176 +apply (unfold Ifix_def)
   1.177  apply (rule lub_mono)
   1.178  apply (rule chain_iterate)
   1.179  apply (rule chain_iterate)
   1.180 @@ -218,10 +185,10 @@
   1.181  apply (rule less_fun [THEN iffD1, THEN spec], erule monofun_iterate [THEN monofunE, THEN spec, THEN spec, THEN mp])
   1.182  done
   1.183  
   1.184 -(* ------------------------------------------------------------------------ *)
   1.185 -(* since iterate is not monotone in its first argument, special lemmas must *)
   1.186 -(* be derived for lubs in this argument                                     *)
   1.187 -(* ------------------------------------------------------------------------ *)
   1.188 +text {*
   1.189 +  since iterate is not monotone in its first argument, special lemmas must
   1.190 +  be derived for lubs in this argument
   1.191 +*}
   1.192  
   1.193  lemma chain_iterate_lub: 
   1.194  "chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"
   1.195 @@ -229,23 +196,22 @@
   1.196  apply (rule lub_mono)
   1.197  apply (rule chain_iterate)
   1.198  apply (rule chain_iterate)
   1.199 -apply (intro strip)
   1.200 +apply (rule allI)
   1.201  apply (erule monofun_iterate [THEN ch2ch_monofun, THEN ch2ch_fun, THEN chainE])
   1.202  done
   1.203  
   1.204 -(* ------------------------------------------------------------------------ *)
   1.205 -(* this exchange lemma is analog to the one for monotone functions          *)
   1.206 -(* observe that monotonicity is not really needed. The propagation of       *)
   1.207 -(* chains is the essential argument which is usually derived from monot.    *)
   1.208 -(* ------------------------------------------------------------------------ *)
   1.209 +text {*
   1.210 +  this exchange lemma is analog to the one for monotone functions
   1.211 +  observe that monotonicity is not really needed. The propagation of
   1.212 +  chains is the essential argument which is usually derived from monot.
   1.213 +*}
   1.214  
   1.215  lemma contlub_Ifix_lemma1: "chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"
   1.216  apply (rule thelub_fun [THEN subst])
   1.217  apply (erule monofun_iterate [THEN ch2ch_monofun])
   1.218 -apply (simp (no_asm_simp) add: contlub_iterate [THEN contlubE])
   1.219 +apply (simp add: contlub_iterate [THEN contlubE])
   1.220  done
   1.221  
   1.222 -
   1.223  lemma ex_lub_iterate: "chain(Y) ==> 
   1.224            lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) = 
   1.225            lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"
   1.226 @@ -258,7 +224,7 @@
   1.227  apply (rule lub_mono)
   1.228  apply (erule monofun_iterate [THEN ch2ch_monofun, THEN ch2ch_fun])
   1.229  apply (erule chain_iterate_lub)
   1.230 -apply (intro strip)
   1.231 +apply (rule allI)
   1.232  apply (rule is_ub_thelub)
   1.233  apply (rule chain_iterate)
   1.234  apply (rule is_lub_thelub)
   1.235 @@ -269,46 +235,39 @@
   1.236  apply (rule contlub_Ifix_lemma1 [THEN ext, THEN subst])
   1.237  apply assumption
   1.238  apply (rule chain_iterate)
   1.239 -apply (intro strip)
   1.240 +apply (rule allI)
   1.241  apply (rule is_ub_thelub)
   1.242  apply (erule monofun_iterate [THEN ch2ch_monofun, THEN ch2ch_fun])
   1.243  done
   1.244  
   1.245 -
   1.246  lemma contlub_Ifix: "contlub(Ifix)"
   1.247 -
   1.248 -apply (unfold contlub Ifix_def)
   1.249 -apply (intro strip)
   1.250 +apply (rule contlubI [rule_format])
   1.251 +apply (unfold Ifix_def)
   1.252  apply (subst contlub_Ifix_lemma1 [THEN ext])
   1.253  apply assumption
   1.254  apply (erule ex_lub_iterate)
   1.255  done
   1.256  
   1.257 -
   1.258  lemma cont_Ifix: "cont(Ifix)"
   1.259  apply (rule monocontlub2cont)
   1.260  apply (rule monofun_Ifix)
   1.261  apply (rule contlub_Ifix)
   1.262  done
   1.263  
   1.264 -(* ------------------------------------------------------------------------ *)
   1.265 -(* propagate properties of Ifix to its continuous counterpart               *)
   1.266 -(* ------------------------------------------------------------------------ *)
   1.267 +text {* propagate properties of @{term Ifix} to its continuous counterpart *}
   1.268  
   1.269  lemma fix_eq: "fix$F = F$(fix$F)"
   1.270 -
   1.271  apply (unfold fix_def)
   1.272 -apply (simp (no_asm_simp) add: cont_Ifix)
   1.273 +apply (simp add: cont_Ifix)
   1.274  apply (rule Ifix_eq)
   1.275  done
   1.276  
   1.277  lemma fix_least: "F$x = x ==> fix$F << x"
   1.278  apply (unfold fix_def)
   1.279 -apply (simp (no_asm_simp) add: cont_Ifix)
   1.280 +apply (simp add: cont_Ifix)
   1.281  apply (erule Ifix_least)
   1.282  done
   1.283  
   1.284 -
   1.285  lemma fix_eqI: 
   1.286  "[| F$x = x; !z. F$z = z --> x << z |] ==> x = fix$F"
   1.287  apply (rule antisym_less)
   1.288 @@ -318,14 +277,11 @@
   1.289  apply (erule fix_least)
   1.290  done
   1.291  
   1.292 -
   1.293  lemma fix_eq2: "f == fix$F ==> f = F$f"
   1.294 -apply (simp (no_asm_simp) add: fix_eq [symmetric])
   1.295 -done
   1.296 +by (simp add: fix_eq [symmetric])
   1.297  
   1.298  lemma fix_eq3: "f == fix$F ==> f$x = F$f$x"
   1.299 -apply (erule fix_eq2 [THEN cfun_fun_cong])
   1.300 -done
   1.301 +by (erule fix_eq2 [THEN cfun_fun_cong])
   1.302  
   1.303  (* fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)) *)
   1.304  
   1.305 @@ -371,10 +327,7 @@
   1.306  	Auto_tac
   1.307  	])
   1.308  *)
   1.309 -(* ------------------------------------------------------------------------ *)
   1.310 -(* better access to definitions                                             *)
   1.311 -(* ------------------------------------------------------------------------ *)
   1.312 -
   1.313 +text {* better access to definitions *}
   1.314  
   1.315  lemma Ifix_def2: "Ifix=(%x. lub(range(%i. iterate i x UU)))"
   1.316  apply (rule ext)
   1.317 @@ -382,9 +335,7 @@
   1.318  apply (rule refl)
   1.319  done
   1.320  
   1.321 -(* ------------------------------------------------------------------------ *)
   1.322 -(* direct connection between fix and iteration without Ifix                 *)
   1.323 -(* ------------------------------------------------------------------------ *)
   1.324 +text {* direct connection between @{term fix} and iteration without @{term Ifix} *}
   1.325  
   1.326  lemma fix_def2: "fix$F = lub(range(%i. iterate i F UU))"
   1.327  apply (unfold fix_def)
   1.328 @@ -392,14 +343,9 @@
   1.329  apply (simp (no_asm_simp) add: cont_Ifix)
   1.330  done
   1.331  
   1.332 +text {* Lemmas about admissibility and fixed point induction *}
   1.333  
   1.334 -(* ------------------------------------------------------------------------ *)
   1.335 -(* Lemmas about admissibility and fixed point induction                     *)
   1.336 -(* ------------------------------------------------------------------------ *)
   1.337 -
   1.338 -(* ------------------------------------------------------------------------ *)
   1.339 -(* access to definitions                                                    *)
   1.340 -(* ------------------------------------------------------------------------ *)
   1.341 +text {* access to definitions *}
   1.342  
   1.343  lemma admI:
   1.344     "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P"
   1.345 @@ -423,9 +369,7 @@
   1.346  apply (rule refl)
   1.347  done
   1.348  
   1.349 -(* ------------------------------------------------------------------------ *)
   1.350 -(* an admissible formula is also weak admissible                            *)
   1.351 -(* ------------------------------------------------------------------------ *)
   1.352 +text {* an admissible formula is also weak admissible *}
   1.353  
   1.354  lemma adm_impl_admw: "adm(P)==>admw(P)"
   1.355  apply (unfold admw_def)
   1.356 @@ -435,9 +379,7 @@
   1.357  apply assumption
   1.358  done
   1.359  
   1.360 -(* ------------------------------------------------------------------------ *)
   1.361 -(* fixed point induction                                                    *)
   1.362 -(* ------------------------------------------------------------------------ *)
   1.363 +text {* fixed point induction *}
   1.364  
   1.365  lemma fix_ind:
   1.366       "[| adm(P); P(UU); !!x. P(x) ==> P(F$x)|] ==> P(fix$F)"
   1.367 @@ -457,10 +399,8 @@
   1.368  apply assumption
   1.369  apply fast
   1.370  done
   1.371 -	
   1.372 -(* ------------------------------------------------------------------------ *)
   1.373 -(* computational induction for weak admissible formulae                     *)
   1.374 -(* ------------------------------------------------------------------------ *)
   1.375 +
   1.376 +text {* computational induction for weak admissible formulae *}
   1.377  
   1.378  lemma wfix_ind: "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix$F)"
   1.379  apply (subst fix_def2)
   1.380 @@ -477,9 +417,7 @@
   1.381  apply assumption
   1.382  done
   1.383  
   1.384 -(* ------------------------------------------------------------------------ *)
   1.385 -(* for chain-finite (easy) types every formula is admissible                *)
   1.386 -(* ------------------------------------------------------------------------ *)
   1.387 +text {* for chain-finite (easy) types every formula is admissible *}
   1.388  
   1.389  lemma adm_max_in_chain: 
   1.390  "!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
   1.391 @@ -497,9 +435,7 @@
   1.392  
   1.393  lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard]
   1.394  
   1.395 -(* ------------------------------------------------------------------------ *)
   1.396 -(* some lemmata for functions with flat/chfin domain/range types	    *)
   1.397 -(* ------------------------------------------------------------------------ *)
   1.398 +text {* some lemmata for functions with flat/chfin domain/range types *}
   1.399  
   1.400  lemma adm_chfindom: "adm (%(u::'a::cpo->'b::chfin). P(u$s))"
   1.401  apply (unfold adm_def)
   1.402 @@ -511,9 +447,7 @@
   1.403  
   1.404  (* adm_flat not needed any more, since it is a special case of adm_chfindom *)
   1.405  
   1.406 -(* ------------------------------------------------------------------------ *)
   1.407 -(* improved admisibility introduction                                       *)
   1.408 -(* ------------------------------------------------------------------------ *)
   1.409 +text {* improved admissibility introduction *}
   1.410  
   1.411  lemma admI2:
   1.412   "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |] 
   1.413 @@ -525,12 +459,9 @@
   1.414  apply fast
   1.415  done
   1.416  
   1.417 +text {* admissibility of special formulae and propagation *}
   1.418  
   1.419 -(* ------------------------------------------------------------------------ *)
   1.420 -(* admissibility of special formulae and propagation                        *)
   1.421 -(* ------------------------------------------------------------------------ *)
   1.422 -
   1.423 -lemma adm_less: "[|cont u;cont v|]==> adm(%x. u x << v x)"
   1.424 +lemma adm_less [simp]: "[|cont u;cont v|]==> adm(%x. u x << v x)"
   1.425  apply (unfold adm_def)
   1.426  apply (intro strip)
   1.427  apply (frule_tac f = "u" in cont2mono [THEN ch2ch_monofun])
   1.428 @@ -543,18 +474,14 @@
   1.429  apply assumption
   1.430  apply (blast intro: lub_mono)
   1.431  done
   1.432 -declare adm_less [simp]
   1.433  
   1.434 -lemma adm_conj: "[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
   1.435 -apply (fast elim: admD intro: admI)
   1.436 -done
   1.437 -declare adm_conj [simp]
   1.438 +lemma adm_conj [simp]: "[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
   1.439 +by (fast elim: admD intro: admI)
   1.440  
   1.441 -lemma adm_not_free: "adm(%x. t)"
   1.442 +lemma adm_not_free [simp]: "adm(%x. t)"
   1.443  apply (unfold adm_def)
   1.444  apply fast
   1.445  done
   1.446 -declare adm_not_free [simp]
   1.447  
   1.448  lemma adm_not_less: "cont t ==> adm(%x.~ (t x) << u)"
   1.449  apply (unfold adm_def)
   1.450 @@ -569,8 +496,7 @@
   1.451  done
   1.452  
   1.453  lemma adm_all: "!y. adm(P y) ==> adm(%x.!y. P y x)"
   1.454 -apply (fast intro: admI elim: admD)
   1.455 -done
   1.456 +by (fast intro: admI elim: admD)
   1.457  
   1.458  lemmas adm_all2 = allI [THEN adm_all, standard]
   1.459  
   1.460 @@ -586,12 +512,9 @@
   1.461  done
   1.462  
   1.463  lemma adm_UU_not_less: "adm(%x.~ UU << t(x))"
   1.464 -apply (simp (no_asm))
   1.465 -done
   1.466 -
   1.467 +by simp
   1.468  
   1.469  lemma adm_not_UU: "cont(t)==> adm(%x.~ (t x) = UU)"
   1.470 -
   1.471  apply (unfold adm_def)
   1.472  apply (intro strip)
   1.473  apply (rule contrapos_nn)
   1.474 @@ -605,36 +528,27 @@
   1.475  done
   1.476  
   1.477  lemma adm_eq: "[|cont u ; cont v|]==> adm(%x. u x = v x)"
   1.478 -apply (simp (no_asm_simp) add: po_eq_conv)
   1.479 -done
   1.480 -
   1.481 -
   1.482 +by (simp add: po_eq_conv)
   1.483  
   1.484 -(* ------------------------------------------------------------------------ *)
   1.485 -(* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
   1.486 -(* ------------------------------------------------------------------------ *)
   1.487 -
   1.488 +text {* admissibility for disjunction is hard to prove. It takes 10 Lemmas *}
   1.489  
   1.490  lemma adm_disj_lemma1: "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
   1.491 -apply fast
   1.492 -done
   1.493 +by fast
   1.494  
   1.495  lemma adm_disj_lemma2: "[| adm(Q); ? X. chain(X) & (!n. Q(X(n))) & 
   1.496        lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
   1.497 -apply (force elim: admD)
   1.498 -done
   1.499 +by (force elim: admD)
   1.500  
   1.501  lemma adm_disj_lemma3: "chain Y ==> chain (%m. if m < Suc i then Y (Suc i) else Y m)"
   1.502  apply (unfold chain_def)
   1.503 -apply (simp (no_asm_simp))
   1.504 +apply (simp)
   1.505  apply safe
   1.506  apply (subgoal_tac "ia = i")
   1.507 -apply (simp_all (no_asm_simp))
   1.508 +apply (simp_all)
   1.509  done
   1.510  
   1.511  lemma adm_disj_lemma4: "!j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
   1.512 -apply (simp (no_asm_simp))
   1.513 -done
   1.514 +by (simp)
   1.515  
   1.516  lemma adm_disj_lemma5: 
   1.517    "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==> 
   1.518 @@ -642,7 +556,7 @@
   1.519  apply (safe intro!: lub_equal2 adm_disj_lemma3)
   1.520  prefer 2 apply (assumption)
   1.521  apply (rule_tac x = "i" in exI)
   1.522 -apply (simp (no_asm_simp))
   1.523 +apply (simp)
   1.524  done
   1.525  
   1.526  lemma adm_disj_lemma6: 
   1.527 @@ -737,7 +651,6 @@
   1.528  apply assumption
   1.529  done
   1.530  
   1.531 -
   1.532  lemma adm_lemma11: 
   1.533  "[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
   1.534  apply (erule adm_disj_lemma2)
   1.535 @@ -764,13 +677,13 @@
   1.536  apply (erule ssubst)
   1.537  apply (erule adm_disj)
   1.538  apply assumption
   1.539 -apply (simp (no_asm))
   1.540 +apply (simp)
   1.541  done
   1.542  
   1.543  lemma adm_iff: "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |]  
   1.544              ==> adm (%x. P x = Q x)"
   1.545  apply (subgoal_tac " (%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))")
   1.546 -apply (simp (no_asm_simp))
   1.547 +apply (simp)
   1.548  apply (rule ext)
   1.549  apply fast
   1.550  done