src/HOLCF/ex/loeckx.ML
author regensbu
Tue Feb 07 17:26:32 1995 +0100 (1995-02-07)
changeset 894 6fcddbebabac
child 896 56b9c2626e81
permissions -rw-r--r--
CVS:
CVS:
regensbu@894
     1
(* Elegant proof for continuity of fixed-point operator *)
regensbu@894
     2
(* Loeckx & Sieber S.88                                 *)
regensbu@894
     3
regensbu@894
     4
val prems = goalw Fix.thy [Ifix_def]
regensbu@894
     5
"Ifix(F)=lub(range(%i.%G.iterate(i,G,UU)))(F)";
regensbu@894
     6
by (rtac (thelub_fun RS ssubst) 1);
regensbu@894
     7
by (rtac ch2ch_fun 1);
regensbu@894
     8
back();
regensbu@894
     9
by (rtac refl 2);
regensbu@894
    10
by (rtac is_chainI 1);
regensbu@894
    11
by (strip_tac 1);
regensbu@894
    12
by (rtac (less_fun RS iffD2) 1);
regensbu@894
    13
by (strip_tac 1);
regensbu@894
    14
by (rtac (less_fun RS iffD2) 1);
regensbu@894
    15
by (strip_tac 1);
regensbu@894
    16
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
regensbu@894
    17
val loeckx_sieber = result();
regensbu@894
    18
regensbu@894
    19
(* 
regensbu@894
    20
regensbu@894
    21
Idea: %i.%G.iterate(i,G,UU)) is a chain of continuous functions and
regensbu@894
    22
      Ifix is the lub of this chain. Hence Ifix is continuous.
regensbu@894
    23
regensbu@894
    24
----- The proof  in HOLCF ----------------------- 
regensbu@894
    25
regensbu@894
    26
Since we already proved the theorem
regensbu@894
    27
regensbu@894
    28
val contX_lubcfun = prove_goal Cfun2.thy 
regensbu@894
    29
	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
regensbu@894
    30
regensbu@894
    31
regensbu@894
    32
we suffices to prove:
regensbu@894
    33
regensbu@894
    34
Ifix  = (%f.lub(range(%j.(LAM f. iterate(j, f, UU))[f])))
regensbu@894
    35
regensbu@894
    36
and 
regensbu@894
    37
regensbu@894
    38
contX(%f.lub(range(%j.(LAM f. iterate(j, f, UU))[f])))
regensbu@894
    39
regensbu@894
    40
Note that if we use the term 
regensbu@894
    41
regensbu@894
    42
%i.%G.iterate(i,G,UU)) instead of (%j.(LAM f. iterate(j, f, UU)))
regensbu@894
    43
regensbu@894
    44
we cannot use the theorem contX_lubcfun    
regensbu@894
    45
regensbu@894
    46
*)
regensbu@894
    47
regensbu@894
    48
val prems = goal Fix.thy  "contX(Ifix)";
regensbu@894
    49
by (res_inst_tac [("t","Ifix"),("s","(%f.lub(range(%j.(LAM f. iterate(j, f, UU))[f])))")] ssubst 1);
regensbu@894
    50
by (rtac ext 1);
regensbu@894
    51
by (rewrite_goals_tac [Ifix_def] );
regensbu@894
    52
by (subgoal_tac " range(% i.iterate(i, f, UU)) = range(%j.(LAM f. iterate(j, f, UU))[f])" 1);
regensbu@894
    53
by (etac arg_cong 1);
regensbu@894
    54
by (subgoal_tac " (% i.iterate(i, f, UU)) = (%j.(LAM f. iterate(j, f, UU))[f])" 1);
regensbu@894
    55
by (etac arg_cong 1);
regensbu@894
    56
by (rtac ext 1);
regensbu@894
    57
by (rtac (beta_cfun RS ssubst) 1);
regensbu@894
    58
by (rtac  contX2contX_CF1L 1);
regensbu@894
    59
by (rtac contX_iterate 1);
regensbu@894
    60
by (rtac refl 1);
regensbu@894
    61
by (rtac contX_lubcfun 1);
regensbu@894
    62
by (rtac is_chainI 1);
regensbu@894
    63
by (strip_tac 1);
regensbu@894
    64
by (rtac less_cfun2 1);
regensbu@894
    65
by (rtac (beta_cfun RS ssubst) 1);
regensbu@894
    66
by (rtac  contX2contX_CF1L 1);
regensbu@894
    67
by (rtac contX_iterate 1);
regensbu@894
    68
by (rtac (beta_cfun RS ssubst) 1);
regensbu@894
    69
by (rtac  contX2contX_CF1L 1);
regensbu@894
    70
by (rtac contX_iterate 1);
regensbu@894
    71
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
regensbu@894
    72
val contX_Ifix2 = result();
regensbu@894
    73
regensbu@894
    74
(* the proof in little steps *)
regensbu@894
    75
regensbu@894
    76
val prems = goal Fix.thy  
regensbu@894
    77
"(% i.iterate(i, f, UU)) = (%j.(LAM f. iterate(j, f, UU))[f])";
regensbu@894
    78
by (rtac ext 1);
regensbu@894
    79
by (rtac (beta_cfun RS ssubst) 1);
regensbu@894
    80
by (rtac  contX2contX_CF1L 1);
regensbu@894
    81
by (rtac contX_iterate 1);
regensbu@894
    82
by (rtac refl 1);
regensbu@894
    83
val fix_lemma1 = result();
regensbu@894
    84
regensbu@894
    85
val prems = goal Fix.thy  
regensbu@894
    86
" Ifix = (%f.lub(range(%j.(LAM f.iterate(j,f,UU))[f])))";
regensbu@894
    87
by (rtac ext 1);
regensbu@894
    88
by (rewrite_goals_tac [Ifix_def] ); 
regensbu@894
    89
by (rtac (fix_lemma1 RS ssubst) 1);
regensbu@894
    90
by (rtac refl 1);
regensbu@894
    91
val fix_lemma2 = result();
regensbu@894
    92
regensbu@894
    93
(*
regensbu@894
    94
- contX_lubcfun;
regensbu@894
    95
val it = "is_chain(?F) ==> contX(%x. lub(range(%j. ?F(j)[x])))" : thm
regensbu@894
    96
regensbu@894
    97
*)
regensbu@894
    98
regensbu@894
    99
val prems = goal Fix.thy "contX(Ifix)";
regensbu@894
   100
by (rtac ( fix_lemma2  RS ssubst) 1);
regensbu@894
   101
by (rtac contX_lubcfun 1);
regensbu@894
   102
by (rtac is_chainI 1);
regensbu@894
   103
by (strip_tac 1);
regensbu@894
   104
by (rtac less_cfun2 1);
regensbu@894
   105
by (rtac (beta_cfun RS ssubst) 1);
regensbu@894
   106
by (rtac  contX2contX_CF1L 1);
regensbu@894
   107
by (rtac contX_iterate 1);
regensbu@894
   108
by (rtac (beta_cfun RS ssubst) 1);
regensbu@894
   109
by (rtac  contX2contX_CF1L 1);
regensbu@894
   110
by (rtac contX_iterate 1);
regensbu@894
   111
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
regensbu@894
   112
val contX_Ifix2 = result();
regensbu@894
   113
regensbu@894
   114
regensbu@894
   115
regensbu@894
   116
regensbu@894
   117
regensbu@894
   118
regensbu@894
   119
regensbu@894
   120