src/HOLCF/ex/loeckx.ML
author wenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524 604d0f3622d6
parent 10835 f4745d77e620
child 16218 ea49a9c7ff7c
permissions -rw-r--r--
*** empty log message ***
regensbu@896
     1
(* $Id$ *)
regensbu@894
     2
(* Elegant proof for continuity of fixed-point operator *)
regensbu@894
     3
(* Loeckx & Sieber S.88                                 *)
regensbu@894
     4
paulson@9248
     5
Goalw [Ifix_def] "Ifix F= lub (range (%i.%G. iterate i G UU)) F";
paulson@2033
     6
by (stac thelub_fun 1);
regensbu@894
     7
by (rtac refl 2);
paulson@9248
     8
by (blast_tac (claset() addIs [ch2ch_fun, chainI, less_fun RS iffD2,
paulson@9248
     9
                               chain_iterate RS chainE]) 1); 
paulson@9248
    10
qed "loeckx_sieber";
regensbu@894
    11
regensbu@894
    12
(* 
regensbu@894
    13
regensbu@1168
    14
Idea: (%i.%G.iterate i G UU) is a chain of continuous functions and
regensbu@894
    15
      Ifix is the lub of this chain. Hence Ifix is continuous.
regensbu@894
    16
regensbu@894
    17
----- The proof  in HOLCF ----------------------- 
regensbu@894
    18
regensbu@894
    19
Since we already proved the theorem
regensbu@894
    20
regensbu@1168
    21
val cont_lubcfun = prove_goal Cfun2.thy 
nipkow@10835
    22
        "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))"
regensbu@894
    23
regensbu@894
    24
regensbu@1168
    25
it suffices to prove:
regensbu@894
    26
nipkow@10835
    27
Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
regensbu@894
    28
regensbu@894
    29
and 
regensbu@894
    30
nipkow@10835
    31
cont (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
regensbu@894
    32
regensbu@894
    33
Note that if we use the term 
regensbu@894
    34
regensbu@1168
    35
%i.%G.iterate i G UU instead of (%j.(LAM f. iterate j f UU))
regensbu@894
    36
regensbu@1168
    37
we cannot use the theorem cont_lubcfun    
regensbu@894
    38
regensbu@894
    39
*)
regensbu@894
    40
paulson@9248
    41
Goal "cont(Ifix)";
regensbu@1168
    42
by (res_inst_tac 
nipkow@10835
    43
 [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)$f)))")]
regensbu@1168
    44
  ssubst 1);
regensbu@894
    45
by (rtac ext 1);
clasohm@1461
    46
by (rewtac Ifix_def );
regensbu@1168
    47
by (subgoal_tac 
nipkow@10835
    48
  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)$f)" 1);
regensbu@894
    49
by (etac arg_cong 1);
regensbu@1168
    50
by (subgoal_tac 
nipkow@10835
    51
        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)" 1);
regensbu@894
    52
by (etac arg_cong 1);
regensbu@894
    53
by (rtac ext 1);
paulson@2033
    54
by (stac beta_cfun 1);
regensbu@1168
    55
by (rtac  cont2cont_CF1L 1);
regensbu@1168
    56
by (rtac cont_iterate 1);
regensbu@894
    57
by (rtac refl 1);
regensbu@1168
    58
by (rtac cont_lubcfun 1);
oheimb@4721
    59
by (rtac chainI 1);
regensbu@894
    60
by (strip_tac 1);
regensbu@894
    61
by (rtac less_cfun2 1);
paulson@2033
    62
by (stac beta_cfun 1);
regensbu@1168
    63
by (rtac  cont2cont_CF1L 1);
regensbu@1168
    64
by (rtac cont_iterate 1);
paulson@2033
    65
by (stac beta_cfun 1);
regensbu@1168
    66
by (rtac  cont2cont_CF1L 1);
regensbu@1168
    67
by (rtac cont_iterate 1);
paulson@9248
    68
by (rtac (chain_iterate RS chainE) 1);
wenzelm@13524
    69
qed "cont_Ifix2'";
regensbu@894
    70
regensbu@894
    71
(* the proof in little steps *)
regensbu@894
    72
nipkow@10835
    73
Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)";
regensbu@894
    74
by (rtac ext 1);
paulson@9248
    75
by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1);
paulson@9248
    76
qed "fix_lemma1";
regensbu@894
    77
nipkow@10835
    78
Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)$f)))";
regensbu@894
    79
by (rtac ext 1);
paulson@9248
    80
by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1);
paulson@9248
    81
qed "fix_lemma2";
regensbu@894
    82
regensbu@894
    83
(*
regensbu@1168
    84
- cont_lubcfun;
nipkow@10835
    85
val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))" : thm   
regensbu@894
    86
regensbu@894
    87
*)
regensbu@894
    88
paulson@9248
    89
Goal "cont Ifix";
paulson@2033
    90
by (stac fix_lemma2 1);
regensbu@1168
    91
by (rtac cont_lubcfun 1);
oheimb@4721
    92
by (rtac chainI 1);
regensbu@894
    93
by (rtac less_cfun2 1);
paulson@2033
    94
by (stac beta_cfun 1);
regensbu@1168
    95
by (rtac  cont2cont_CF1L 1);
regensbu@1168
    96
by (rtac cont_iterate 1);
paulson@2033
    97
by (stac beta_cfun 1);
regensbu@1168
    98
by (rtac  cont2cont_CF1L 1);
regensbu@1168
    99
by (rtac cont_iterate 1);
paulson@9248
   100
by (rtac (chain_iterate RS chainE) 1);
wenzelm@13524
   101
qed "cont_Ifix2''";
regensbu@894
   102