src/HOLCF/Cprod3.ML

 (* ------------------------------------------------------------------------ *)
 (* continuity of (_,_) , fst, snd                                           *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "Cprod3_lemma1" Cprod3.thy 
-"is_chain(Y::(nat=>'a::cpo)) ==>\
+"chain(Y::(nat=>'a::cpo)) ==>\
 \ (lub(range(Y)),(x::'b::cpo)) =\
 \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),

         (etac (monofun_pair1 RS ch2ch_monofun) 2),
         (etac Cprod3_lemma1 1)
         ]);
 
 qed_goal "Cprod3_lemma2" Cprod3.thy 
-"is_chain(Y::(nat=>'a::cpo)) ==>\
+"chain(Y::(nat=>'a::cpo)) ==>\
 \ ((x::'b::cpo),lub(range Y)) =\
 \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),

         (dtac (beta_cfun_cprod RS subst) 1),
         (atac 1)
         ]);
 
 qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
 \ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (stac beta_cfun_cprod 1),

         (atac 1)
         ]);
 
 bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
 (*
-is_chain ?S1 ==>
+chain ?S1 ==>
  lub (range ?S1) =
  <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" 
 *)
 qed_goalw "csplit2" Cprod3.thy [csplit_def]
         "csplit`f`<x,y> = f`x`y"