src/HOLCF/ex/loeckx.ML
changeset 10835 f4745d77e620
parent 9248 e1dee89de037
child 13524 604d0f3622d6
     1.1 --- a/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -19,16 +19,16 @@
     1.4  Since we already proved the theorem
     1.5  
     1.6  val cont_lubcfun = prove_goal Cfun2.thy 
     1.7 -        "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
     1.8 +        "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))"
     1.9  
    1.10  
    1.11  it suffices to prove:
    1.12  
    1.13 -Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
    1.14 +Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
    1.15  
    1.16  and 
    1.17  
    1.18 -cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
    1.19 +cont (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
    1.20  
    1.21  Note that if we use the term 
    1.22  
    1.23 @@ -40,15 +40,15 @@
    1.24  
    1.25  Goal "cont(Ifix)";
    1.26  by (res_inst_tac 
    1.27 - [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
    1.28 + [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)$f)))")]
    1.29    ssubst 1);
    1.30  by (rtac ext 1);
    1.31  by (rewtac Ifix_def );
    1.32  by (subgoal_tac 
    1.33 -  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
    1.34 +  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)$f)" 1);
    1.35  by (etac arg_cong 1);
    1.36  by (subgoal_tac 
    1.37 -        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
    1.38 +        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)" 1);
    1.39  by (etac arg_cong 1);
    1.40  by (rtac ext 1);
    1.41  by (stac beta_cfun 1);
    1.42 @@ -70,19 +70,19 @@
    1.43  
    1.44  (* the proof in little steps *)
    1.45  
    1.46 -Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
    1.47 +Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)";
    1.48  by (rtac ext 1);
    1.49  by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1);
    1.50  qed "fix_lemma1";
    1.51  
    1.52 -Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
    1.53 +Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)$f)))";
    1.54  by (rtac ext 1);
    1.55  by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1);
    1.56  qed "fix_lemma2";
    1.57  
    1.58  (*
    1.59  - cont_lubcfun;
    1.60 -val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
    1.61 +val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))" : thm   
    1.62  
    1.63  *)
    1.64