src/HOLCF/ex/loeckx.ML

Simplified proofs by omitting PA = {|XA, ...|} from RA2

(* $Id$ *)
(* Elegant proof for continuity of fixed-point operator *)
(* Loeckx & Sieber S.88                                 *)

val prems = goalw Fix.thy [Ifix_def]
"Ifix F= lub (range (%i.%G. iterate i G UU)) F";
by (stac thelub_fun 1);
by (rtac ch2ch_fun 1);
back();
by (rtac refl 2);
by (rtac is_chainI 1);
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
by (rtac (less_fun RS iffD2) 1);
by (strip_tac 1);
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
val loeckx_sieber = result();

(* 

Idea: (%i.%G.iterate i G UU) is a chain of continuous functions and
      Ifix is the lub of this chain. Hence Ifix is continuous.

----- The proof  in HOLCF ----------------------- 

Since we already proved the theorem

val cont_lubcfun = prove_goal Cfun2.thy 
        "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"


it suffices to prove:

Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))

and 

cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))

Note that if we use the term 

%i.%G.iterate i G UU instead of (%j.(LAM f. iterate j f UU))

we cannot use the theorem cont_lubcfun    

*)

val prems = goal Fix.thy  "cont(Ifix)";
by (res_inst_tac 
 [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
  ssubst 1);
by (rtac ext 1);
by (rewtac Ifix_def );
by (subgoal_tac 
  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
by (etac arg_cong 1);
by (subgoal_tac 
        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
by (etac arg_cong 1);
by (rtac ext 1);
by (stac beta_cfun 1);
by (rtac  cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac refl 1);
by (rtac cont_lubcfun 1);
by (rtac is_chainI 1);
by (strip_tac 1);
by (rtac less_cfun2 1);
by (stac beta_cfun 1);
by (rtac  cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (stac beta_cfun 1);
by (rtac  cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
val cont_Ifix2 = result();

(* the proof in little steps *)

val prems = goal Fix.thy  
"(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
by (rtac ext 1);
by (stac beta_cfun 1);
by (rtac  cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac refl 1);
val fix_lemma1 = result();

val prems = goal Fix.thy  
" Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
by (rtac ext 1);
by (rewtac Ifix_def ); 
by (stac fix_lemma1 1);
by (rtac refl 1);
val fix_lemma2 = result();

(*
- cont_lubcfun;
val it = "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   

*)

val prems = goal Fix.thy "cont Ifix";
by (stac fix_lemma2 1);
by (rtac cont_lubcfun 1);
by (rtac is_chainI 1);
by (strip_tac 1);
by (rtac less_cfun2 1);
by (stac beta_cfun 1);
by (rtac  cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (stac beta_cfun 1);
by (rtac  cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
val cont_Ifix2 = result();