author huffman Thu Mar 31 00:10:35 2005 +0200 (2005-03-31 ago) changeset 15637 d2a06007ebfa parent 15636 57c437b70521 child 15638 1fb24e545f88
changed comments to text blocks, cleaned up a few proofs
 src/HOLCF/Fix.thy file | annotate | diff | revisions
```     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.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.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.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.311 -(* ------------------------------------------------------------------------ *)
1.312 -
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.333
1.334 -(* ------------------------------------------------------------------------ *)
1.336 -(* ------------------------------------------------------------------------ *)
1.337 -
1.338 -(* ------------------------------------------------------------------------ *)
1.340 -(* ------------------------------------------------------------------------ *)
1.342
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.351 -(* ------------------------------------------------------------------------ *)
1.353
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.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.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.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.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.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.433
1.436 -done
1.440
1.444  apply fast
1.445  done
1.447
1.450 @@ -569,8 +496,7 @@
1.451  done
1.452
1.455 -done
1.457
1.459
1.460 @@ -586,12 +512,9 @@
1.461  done
1.462
1.464 -apply (simp (no_asm))
1.465 -done
1.466 -
1.467 +by simp
1.468
1.470 -
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.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.498 -done
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.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.527 @@ -737,7 +651,6 @@
1.528  apply assumption
1.529  done
1.530
1.531 -
1.533  "[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
1.535 @@ -764,13 +677,13 @@
1.536  apply (erule ssubst)
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
```