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