renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
authoroheimb
Tue Mar 10 18:33:13 1998 +0100 (1998-03-10)
changeset 4721c8a8482a8124
parent 4720 c1b83b42f65a
child 4722 d2e44673c21e
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Cont.ML
src/HOLCF/Cont.thy
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod3.ML
src/HOLCF/Discrete.ML
src/HOLCF/Discrete1.ML
src/HOLCF/Fix.thy
src/HOLCF/Fun1.thy
src/HOLCF/Fun2.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/Lift2.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.ML
src/HOLCF/Porder.thy
src/HOLCF/Sprod2.ML
src/HOLCF/Sprod3.ML
src/HOLCF/Ssum2.ML
src/HOLCF/Ssum3.ML
src/HOLCF/Up2.ML
src/HOLCF/Up3.ML
src/HOLCF/adm.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/ex/Stream.ML
src/HOLCF/ex/loeckx.ML
     1.1 --- a/src/HOLCF/Cfun2.ML	Tue Mar 10 18:32:37 1998 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Tue Mar 10 18:33:13 1998 +0100
     1.3 @@ -75,10 +75,10 @@
     1.4  (* ------------------------------------------------------------------------ *)
     1.5  
     1.6  bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
     1.7 -(* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
     1.8 +(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
     1.9   
    1.10  bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
    1.11 -(* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.12 +(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.13  
    1.14  
    1.15  (* ------------------------------------------------------------------------ *)
    1.16 @@ -138,7 +138,7 @@
    1.17  (* ------------------------------------------------------------------------ *)
    1.18  
    1.19  qed_goal "ch2ch_fappR" thy 
    1.20 - "is_chain(Y) ==> is_chain(%i. f`(Y i))"
    1.21 + "chain(Y) ==> chain(%i. f`(Y i))"
    1.22  (fn prems =>
    1.23          [
    1.24          (cut_facts_tac prems 1),
    1.25 @@ -147,7 +147,7 @@
    1.26  
    1.27  
    1.28  bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
    1.29 -(* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
    1.30 +(* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
    1.31  
    1.32  
    1.33  (* ------------------------------------------------------------------------ *)
    1.34 @@ -156,7 +156,7 @@
    1.35  (* ------------------------------------------------------------------------ *)
    1.36  
    1.37  qed_goal "lub_cfun_mono" thy 
    1.38 -        "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
    1.39 +        "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
    1.40  (fn prems =>
    1.41          [
    1.42          (cut_facts_tac prems 1),
    1.43 @@ -172,7 +172,7 @@
    1.44  (* ------------------------------------------------------------------------ *)
    1.45  
    1.46  qed_goal "ex_lubcfun" thy
    1.47 -        "[| is_chain(F); is_chain(Y) |] ==>\
    1.48 +        "[| chain(F); chain(Y) |] ==>\
    1.49  \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
    1.50  \               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
    1.51  (fn prems =>
    1.52 @@ -190,7 +190,7 @@
    1.53  (* ------------------------------------------------------------------------ *)
    1.54  
    1.55  qed_goal "cont_lubcfun" thy 
    1.56 -        "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
    1.57 +        "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
    1.58  (fn prems =>
    1.59          [
    1.60          (cut_facts_tac prems 1),
    1.61 @@ -209,7 +209,7 @@
    1.62  (* ------------------------------------------------------------------------ *)
    1.63  
    1.64  qed_goal "lub_cfun" thy 
    1.65 -  "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
    1.66 +  "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
    1.67  (fn prems =>
    1.68          [
    1.69          (cut_facts_tac prems 1),
    1.70 @@ -233,11 +233,11 @@
    1.71  
    1.72  bind_thm ("thelub_cfun", lub_cfun RS thelubI);
    1.73  (* 
    1.74 -is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
    1.75 +chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
    1.76  *)
    1.77  
    1.78  qed_goal "cpo_cfun" thy 
    1.79 -  "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
    1.80 +  "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
    1.81  (fn prems =>
    1.82          [
    1.83          (cut_facts_tac prems 1),
     2.1 --- a/src/HOLCF/Cfun3.ML	Tue Mar 10 18:32:37 1998 +0100
     2.2 +++ b/src/HOLCF/Cfun3.ML	Tue Mar 10 18:33:13 1998 +0100
     2.3 @@ -52,7 +52,7 @@
     2.4  (* ------------------------------------------------------------------------ *)
     2.5  
     2.6  qed_goal "contlub_cfun_fun" thy 
     2.7 -"is_chain(FY) ==>\
     2.8 +"chain(FY) ==>\
     2.9  \ lub(range FY)`x = lub(range (%i. FY(i)`x))"
    2.10  (fn prems =>
    2.11          [
    2.12 @@ -66,7 +66,7 @@
    2.13  
    2.14  
    2.15  qed_goal "cont_cfun_fun" thy 
    2.16 -"is_chain(FY) ==>\
    2.17 +"chain(FY) ==>\
    2.18  \ range(%i. FY(i)`x) <<| lub(range FY)`x"
    2.19  (fn prems =>
    2.20          [
    2.21 @@ -82,7 +82,7 @@
    2.22  (* ------------------------------------------------------------------------ *)
    2.23  
    2.24  qed_goal "contlub_cfun" thy 
    2.25 -"[|is_chain(FY);is_chain(TY)|] ==>\
    2.26 +"[|chain(FY);chain(TY)|] ==>\
    2.27  \ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
    2.28  (fn prems =>
    2.29          [
    2.30 @@ -96,7 +96,7 @@
    2.31          ]);
    2.32  
    2.33  qed_goal "cont_cfun" thy 
    2.34 -"[|is_chain(FY);is_chain(TY)|] ==>\
    2.35 +"[|chain(FY);chain(TY)|] ==>\
    2.36  \ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
    2.37  (fn prems =>
    2.38          [
    2.39 @@ -373,11 +373,11 @@
    2.40  (*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
    2.41  
    2.42  (* ------------------------------------------------------------------------ *)
    2.43 -(* some lemmata for functions with flat/chain_finite domain/range types	    *)
    2.44 +(* some lemmata for functions with flat/chfin domain/range types	    *)
    2.45  (* ------------------------------------------------------------------------ *)
    2.46  
    2.47  qed_goal "chfin_fappR" thy 
    2.48 -    "is_chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
    2.49 +    "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
    2.50  (fn prems => 
    2.51  	[
    2.52  	cut_facts_tac prems 1,
    2.53 @@ -441,15 +441,15 @@
    2.54  (* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
    2.55  (* ------------------------------------------------------------------------ *)
    2.56  
    2.57 -qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. is_chain Y --> (? n. max_in_chain n Y); \
    2.58 +qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
    2.59  \ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
    2.60 -\ ==> ! Y::nat=>'b. is_chain Y --> (? n. max_in_chain n Y)"
    2.61 +\ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)"
    2.62   (fn prems =>
    2.63          [
    2.64          (rewtac max_in_chain_def),
    2.65          (strip_tac 1),
    2.66          (rtac exE 1),
    2.67 -        (res_inst_tac [("P","is_chain(%i. g`(Y i))")] mp 1),
    2.68 +        (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
    2.69          (etac spec 1),
    2.70          (etac ch2ch_fappR 1),
    2.71          (rtac exI 1),
     3.1 --- a/src/HOLCF/Cont.ML	Tue Mar 10 18:32:37 1998 +0100
     3.2 +++ b/src/HOLCF/Cont.ML	Tue Mar 10 18:33:13 1998 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  (* ------------------------------------------------------------------------ *)
     3.5  
     3.6  qed_goalw "contlubI" thy [contlub]
     3.7 -        "! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
     3.8 +        "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
     3.9  \        contlub(f)"
    3.10  (fn prems =>
    3.11          [
    3.12 @@ -23,7 +23,7 @@
    3.13  
    3.14  qed_goalw "contlubE" thy [contlub]
    3.15          " contlub(f)==>\
    3.16 -\         ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
    3.17 +\         ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
    3.18  (fn prems =>
    3.19          [
    3.20          (cut_facts_tac prems 1),
    3.21 @@ -32,7 +32,7 @@
    3.22  
    3.23  
    3.24  qed_goalw "contI" thy [cont]
    3.25 - "! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
    3.26 + "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
    3.27  (fn prems =>
    3.28          [
    3.29          (cut_facts_tac prems 1),
    3.30 @@ -40,7 +40,7 @@
    3.31          ]);
    3.32  
    3.33  qed_goalw "contE" thy [cont]
    3.34 - "cont(f) ==> ! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
    3.35 + "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
    3.36  (fn prems =>
    3.37          [
    3.38          (cut_facts_tac prems 1),
    3.39 @@ -74,14 +74,14 @@
    3.40  (* ------------------------------------------------------------------------ *)
    3.41  
    3.42  qed_goal "ch2ch_monofun" thy 
    3.43 -        "[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
    3.44 +        "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
    3.45  (fn prems =>
    3.46          [
    3.47          (cut_facts_tac prems 1),
    3.48 -        (rtac is_chainI 1),
    3.49 +        (rtac chainI 1),
    3.50          (rtac allI 1),
    3.51          (etac (monofunE RS spec RS spec RS mp) 1),
    3.52 -        (etac (is_chainE RS spec) 1)
    3.53 +        (etac (chainE RS spec) 1)
    3.54          ]);
    3.55  
    3.56  (* ------------------------------------------------------------------------ *)
    3.57 @@ -194,7 +194,7 @@
    3.58  (* ------------------------------------------------------------------------ *)
    3.59  
    3.60  qed_goal "ch2ch_MF2L" thy 
    3.61 -"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)"
    3.62 +"[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
    3.63  (fn prems =>
    3.64          [
    3.65          (cut_facts_tac prems 1),
    3.66 @@ -204,7 +204,7 @@
    3.67  
    3.68  
    3.69  qed_goal "ch2ch_MF2R" thy 
    3.70 -"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))"
    3.71 +"[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
    3.72  (fn prems =>
    3.73          [
    3.74          (cut_facts_tac prems 1),
    3.75 @@ -213,36 +213,36 @@
    3.76          ]);
    3.77  
    3.78  qed_goal "ch2ch_MF2LR" thy 
    3.79 -"[|monofun(MF2); !f. monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
    3.80 -\  is_chain(%i. MF2(F(i))(Y(i)))"
    3.81 +"[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
    3.82 +\  chain(%i. MF2(F(i))(Y(i)))"
    3.83   (fn prems =>
    3.84          [
    3.85          (cut_facts_tac prems 1),
    3.86 -        (rtac is_chainI 1),
    3.87 +        (rtac chainI 1),
    3.88          (strip_tac 1 ),
    3.89          (rtac trans_less 1),
    3.90 -        (etac (ch2ch_MF2L RS is_chainE RS spec) 1),
    3.91 +        (etac (ch2ch_MF2L RS chainE RS spec) 1),
    3.92          (atac 1),
    3.93          ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
    3.94 -        (etac (is_chainE RS spec) 1)
    3.95 +        (etac (chainE RS spec) 1)
    3.96          ]);
    3.97  
    3.98  
    3.99  qed_goal "ch2ch_lubMF2R" thy 
   3.100  "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   3.101  \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   3.102 -\       is_chain(F);is_chain(Y)|] ==> \
   3.103 -\       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
   3.104 +\       chain(F);chain(Y)|] ==> \
   3.105 +\       chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
   3.106  (fn prems =>
   3.107          [
   3.108          (cut_facts_tac prems 1),
   3.109 -        (rtac (lub_mono RS allI RS is_chainI) 1),
   3.110 +        (rtac (lub_mono RS allI RS chainI) 1),
   3.111          ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   3.112          (atac 1),
   3.113          ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   3.114          (atac 1),
   3.115          (strip_tac 1),
   3.116 -        (rtac (is_chainE RS spec) 1),
   3.117 +        (rtac (chainE RS spec) 1),
   3.118          (etac ch2ch_MF2L 1),
   3.119          (atac 1)
   3.120          ]);
   3.121 @@ -251,18 +251,18 @@
   3.122  qed_goal "ch2ch_lubMF2L" thy 
   3.123  "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   3.124  \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   3.125 -\       is_chain(F);is_chain(Y)|] ==> \
   3.126 -\       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
   3.127 +\       chain(F);chain(Y)|] ==> \
   3.128 +\       chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
   3.129  (fn prems =>
   3.130          [
   3.131          (cut_facts_tac prems 1),
   3.132 -        (rtac (lub_mono RS allI RS is_chainI) 1),
   3.133 +        (rtac (lub_mono RS allI RS chainI) 1),
   3.134          (etac ch2ch_MF2L 1),
   3.135          (atac 1),
   3.136          (etac ch2ch_MF2L 1),
   3.137          (atac 1),
   3.138          (strip_tac 1),
   3.139 -        (rtac (is_chainE RS spec) 1),
   3.140 +        (rtac (chainE RS spec) 1),
   3.141          ((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
   3.142          (atac 1)
   3.143          ]);
   3.144 @@ -271,7 +271,7 @@
   3.145  qed_goal "lub_MF2_mono" thy 
   3.146  "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   3.147  \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   3.148 -\       is_chain(F)|] ==> \
   3.149 +\       chain(F)|] ==> \
   3.150  \       monofun(% x. lub(range(% j. MF2 (F j) (x))))"
   3.151  (fn prems =>
   3.152          [
   3.153 @@ -291,7 +291,7 @@
   3.154  qed_goal "ex_lubMF2" thy 
   3.155  "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   3.156  \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   3.157 -\       is_chain(F); is_chain(Y)|] ==> \
   3.158 +\       chain(F); chain(Y)|] ==> \
   3.159  \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
   3.160  \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
   3.161   (fn prems =>
   3.162 @@ -330,7 +330,7 @@
   3.163  qed_goal "diag_lubMF2_1" thy 
   3.164  "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   3.165  \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   3.166 -\  is_chain(FY);is_chain(TY)|] ==>\
   3.167 +\  chain(FY);chain(TY)|] ==>\
   3.168  \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
   3.169  \ lub(range(%i. MF2(FY(i))(TY(i))))"
   3.170   (fn prems =>
   3.171 @@ -374,7 +374,7 @@
   3.172  qed_goal "diag_lubMF2_2" thy 
   3.173  "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
   3.174  \  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
   3.175 -\  is_chain(FY);is_chain(TY)|] ==>\
   3.176 +\  chain(FY);chain(TY)|] ==>\
   3.177  \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
   3.178  \ lub(range(%i. MF2(FY(i))(TY(i))))"
   3.179   (fn prems =>
   3.180 @@ -394,7 +394,7 @@
   3.181  (* ------------------------------------------------------------------------ *)
   3.182  
   3.183  qed_goal "contlub_CF2" thy 
   3.184 -"[|cont(CF2);!f. cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   3.185 +"[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
   3.186  \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
   3.187   (fn prems =>
   3.188          [
   3.189 @@ -524,7 +524,7 @@
   3.190  (* ------------------------------------------------------------------------ *)
   3.191  
   3.192  qed_goal "contlub_abstraction" thy
   3.193 -"[|is_chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
   3.194 +"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
   3.195  \ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
   3.196   (fn prems =>
   3.197          [
     4.1 --- a/src/HOLCF/Cont.thy	Tue Mar 10 18:32:37 1998 +0100
     4.2 +++ b/src/HOLCF/Cont.thy	Tue Mar 10 18:33:13 1998 +0100
     4.3 @@ -27,10 +27,10 @@
     4.4  
     4.5  monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
     4.6  
     4.7 -contlub         "contlub(f) == ! Y. is_chain(Y) --> 
     4.8 +contlub         "contlub(f) == ! Y. chain(Y) --> 
     4.9                                  f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
    4.10  
    4.11 -cont            "cont(f)   == ! Y. is_chain(Y) --> 
    4.12 +cont            "cont(f)   == ! Y. chain(Y) --> 
    4.13                                  range(% i. f(Y(i))) <<| f(lub(range(Y)))"
    4.14  
    4.15  (* ------------------------------------------------------------------------ *)
     5.1 --- a/src/HOLCF/Cprod2.ML	Tue Mar 10 18:32:37 1998 +0100
     5.2 +++ b/src/HOLCF/Cprod2.ML	Tue Mar 10 18:33:13 1998 +0100
     5.3 @@ -116,7 +116,7 @@
     5.4  (* ------------------------------------------------------------------------ *)
     5.5  
     5.6  qed_goal "lub_cprod" thy 
     5.7 -"is_chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
     5.8 +"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
     5.9   (fn prems =>
    5.10          [
    5.11          (cut_facts_tac prems 1),
    5.12 @@ -141,13 +141,13 @@
    5.13  
    5.14  bind_thm ("thelub_cprod", lub_cprod RS thelubI);
    5.15  (*
    5.16 -"is_chain ?S1 ==>
    5.17 +"chain ?S1 ==>
    5.18   lub (range ?S1) =
    5.19   (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
    5.20  
    5.21  *)
    5.22  
    5.23 -qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
    5.24 +qed_goal "cpo_cprod" thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
    5.25  (fn prems =>
    5.26          [
    5.27          (cut_facts_tac prems 1),
     6.1 --- a/src/HOLCF/Cprod3.ML	Tue Mar 10 18:32:37 1998 +0100
     6.2 +++ b/src/HOLCF/Cprod3.ML	Tue Mar 10 18:33:13 1998 +0100
     6.3 @@ -20,7 +20,7 @@
     6.4  (* ------------------------------------------------------------------------ *)
     6.5  
     6.6  qed_goal "Cprod3_lemma1" Cprod3.thy 
     6.7 -"is_chain(Y::(nat=>'a::cpo)) ==>\
     6.8 +"chain(Y::(nat=>'a::cpo)) ==>\
     6.9  \ (lub(range(Y)),(x::'b::cpo)) =\
    6.10  \ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
    6.11   (fn prems =>
    6.12 @@ -57,7 +57,7 @@
    6.13          ]);
    6.14  
    6.15  qed_goal "Cprod3_lemma2" Cprod3.thy 
    6.16 -"is_chain(Y::(nat=>'a::cpo)) ==>\
    6.17 +"chain(Y::(nat=>'a::cpo)) ==>\
    6.18  \ ((x::'b::cpo),lub(range Y)) =\
    6.19  \ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
    6.20   (fn prems =>
    6.21 @@ -261,7 +261,7 @@
    6.22          ]);
    6.23  
    6.24  qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
    6.25 -"[|is_chain(S)|] ==> range(S) <<| \
    6.26 +"[|chain(S)|] ==> range(S) <<| \
    6.27  \ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"
    6.28   (fn prems =>
    6.29          [
    6.30 @@ -277,7 +277,7 @@
    6.31  
    6.32  bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
    6.33  (*
    6.34 -is_chain ?S1 ==>
    6.35 +chain ?S1 ==>
    6.36   lub (range ?S1) =
    6.37   <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" 
    6.38  *)
     7.1 --- a/src/HOLCF/Discrete.ML	Tue Mar 10 18:32:37 1998 +0100
     7.2 +++ b/src/HOLCF/Discrete.ML	Tue Mar 10 18:33:13 1998 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4  Addsimps [undiscr_Discr];
     7.5  
     7.6  goal thy
     7.7 - "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
     7.8 + "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
     7.9  by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
    7.10  qed "discr_chain_f_range0";
    7.11  
     8.1 --- a/src/HOLCF/Discrete1.ML	Tue Mar 10 18:32:37 1998 +0100
     8.2 +++ b/src/HOLCF/Discrete1.ML	Tue Mar 10 18:33:13 1998 +0100
     8.3 @@ -11,8 +11,8 @@
     8.4  qed "discr_less_eq";
     8.5  AddIffs [discr_less_eq];
     8.6  
     8.7 -goalw thy [is_chain]
     8.8 - "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
     8.9 +goalw thy [chain]
    8.10 + "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
    8.11  by (nat_ind_tac "i" 1);
    8.12  by (rtac refl 1);
    8.13  by (etac subst 1);
    8.14 @@ -21,12 +21,12 @@
    8.15  qed "discr_chain0";
    8.16  
    8.17  goal thy
    8.18 - "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
    8.19 + "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
    8.20  by (fast_tac (claset() addEs [discr_chain0]) 1);
    8.21  qed "discr_chain_range0";
    8.22  Addsimps [discr_chain_range0];
    8.23  
    8.24  goalw thy [is_lub,is_ub]
    8.25 - "!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
    8.26 + "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
    8.27  by (Asm_simp_tac 1);
    8.28  qed "discr_cpo";
     9.1 --- a/src/HOLCF/Fix.thy	Tue Mar 10 18:32:37 1998 +0100
     9.2 +++ b/src/HOLCF/Fix.thy	Tue Mar 10 18:33:13 1998 +0100
     9.3 @@ -24,7 +24,7 @@
     9.4  Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
     9.5  fix_def       "fix == (LAM f. Ifix f)"
     9.6  
     9.7 -adm_def       "adm P == !Y. is_chain(Y) --> 
     9.8 +adm_def       "adm P == !Y. chain(Y) --> 
     9.9                          (!i. P(Y i)) --> P(lub(range Y))"
    9.10  
    9.11  admw_def      "admw P == !F. (!n. P (iterate n F UU)) -->
    10.1 --- a/src/HOLCF/Fun1.thy	Tue Mar 10 18:32:37 1998 +0100
    10.2 +++ b/src/HOLCF/Fun1.thy	Tue Mar 10 18:33:13 1998 +0100
    10.3 @@ -12,7 +12,7 @@
    10.4  
    10.5  Fun1 = Pcpo +
    10.6  
    10.7 -instance flat<chfin (flat_imp_chain_finite)
    10.8 +instance flat<chfin (flat_imp_chfin)
    10.9  
   10.10  (* to make << defineable: *)
   10.11  instance fun  :: (term,sq_ord)sq_ord
    11.1 --- a/src/HOLCF/Fun2.ML	Tue Mar 10 18:32:37 1998 +0100
    11.2 +++ b/src/HOLCF/Fun2.ML	Tue Mar 10 18:33:13 1998 +0100
    11.3 @@ -52,11 +52,11 @@
    11.4  (* ------------------------------------------------------------------------ *)
    11.5  
    11.6  qed_goal "ch2ch_fun" thy 
    11.7 -        "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i. S(i)(x))"
    11.8 +        "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"
    11.9  (fn prems =>
   11.10          [
   11.11          (cut_facts_tac prems 1),
   11.12 -        (rewtac is_chain),
   11.13 +        (rewtac chain),
   11.14          (rtac allI 1),
   11.15          (rtac spec 1),
   11.16          (rtac (less_fun RS subst) 1),
   11.17 @@ -86,7 +86,7 @@
   11.18  (* ------------------------------------------------------------------------ *)
   11.19  
   11.20  qed_goal "lub_fun"  Fun2.thy
   11.21 -        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
   11.22 +        "chain(S::nat=>('a::term => 'b::cpo)) ==> \
   11.23  \        range(S) <<| (% x. lub(range(% i. S(i)(x))))"
   11.24  (fn prems =>
   11.25          [
   11.26 @@ -108,10 +108,10 @@
   11.27          ]);
   11.28  
   11.29  bind_thm ("thelub_fun", lub_fun RS thelubI);
   11.30 -(* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
   11.31 +(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
   11.32  
   11.33  qed_goal "cpo_fun"  Fun2.thy
   11.34 -        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
   11.35 +        "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
   11.36  (fn prems =>
   11.37          [
   11.38          (cut_facts_tac prems 1),
    12.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 18:32:37 1998 +0100
    12.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Mar 10 18:33:13 1998 +0100
    12.3 @@ -920,12 +920,12 @@
    12.4  by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
    12.5  by (rtac (fix_def2 RS ssubst ) 1);
    12.6  by (stac contlub_cfun_fun 1);
    12.7 -by (rtac is_chain_iterate 1);
    12.8 +by (rtac chain_iterate 1);
    12.9  by (stac contlub_cfun_fun 1);
   12.10 -by (rtac is_chain_iterate 1);
   12.11 +by (rtac chain_iterate 1);
   12.12  by (rtac lub_mono 1);
   12.13 -by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
   12.14 -by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
   12.15 +by (rtac (chain_iterate RS ch2ch_fappL) 1);
   12.16 +by (rtac (chain_iterate RS ch2ch_fappL) 1);
   12.17  by (rtac allI 1);
   12.18  by (resolve_tac prems 1);
   12.19  qed"take_lemma_less1";
    13.1 --- a/src/HOLCF/Lift2.ML	Tue Mar 10 18:32:37 1998 +0100
    13.2 +++ b/src/HOLCF/Lift2.ML	Tue Mar 10 18:33:13 1998 +0100
    13.3 @@ -56,7 +56,7 @@
    13.4  (* Tailoring chain_mono2 of Pcpo.ML to Undef *)
    13.5  
    13.6  goal Lift2.thy
    13.7 -"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
    13.8 +"!!Y. [|? j.~Y(j)=Undef;chain(Y::nat=>('a)lift)|] \
    13.9  \ ==> ? j.!i. j<i-->~Y(i)=Undef";
   13.10  by Safe_tac;
   13.11  by (Step_tac 1);
   13.12 @@ -68,10 +68,10 @@
   13.13  qed"chain_mono2_po";
   13.14  
   13.15  
   13.16 -(* Tailoring flat_imp_chain_finite of Fix.ML to lift *)
   13.17 +(* Tailoring flat_imp_chfin of Fix.ML to lift *)
   13.18  
   13.19  goal Lift2.thy
   13.20 -        "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
   13.21 +        "(! Y. chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
   13.22  by (rewtac max_in_chain_def);  
   13.23  by (strip_tac 1);
   13.24  by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm  1);
   13.25 @@ -104,14 +104,14 @@
   13.26  by (rtac mp 1); 
   13.27  by (etac spec 1); 
   13.28  by (Asm_simp_tac 1);
   13.29 -qed"flat_imp_chain_finite_poo";
   13.30 +qed"flat_imp_chfin_poo";
   13.31  
   13.32  
   13.33  (* Main Lemma: cpo_lift *)
   13.34  
   13.35  goal Lift2.thy  
   13.36 -  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
   13.37 -by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
   13.38 +  "!!Y. chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
   13.39 +by (cut_inst_tac [] flat_imp_chfin_poo 1);
   13.40  by (Step_tac 1);
   13.41  by Safe_tac;
   13.42  by (Step_tac 1); 
    14.1 --- a/src/HOLCF/Pcpo.ML	Tue Mar 10 18:32:37 1998 +0100
    14.2 +++ b/src/HOLCF/Pcpo.ML	Tue Mar 10 18:33:13 1998 +0100
    14.3 @@ -25,7 +25,7 @@
    14.4  (* ------------------------------------------------------------------------ *)
    14.5  
    14.6  qed_goal "thelubE"  thy 
    14.7 -        "[| is_chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
    14.8 +        "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
    14.9  (fn prems =>
   14.10          [
   14.11          (cut_facts_tac prems 1), 
   14.12 @@ -40,12 +40,12 @@
   14.13  
   14.14  
   14.15  bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
   14.16 -(* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
   14.17 +(* chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
   14.18  
   14.19  bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
   14.20 -(* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
   14.21 +(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
   14.22  
   14.23 -qed_goal "maxinch_is_thelub" thy "is_chain Y ==> \
   14.24 +qed_goal "maxinch_is_thelub" thy "chain Y ==> \
   14.25  \       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))" 
   14.26  (fn prems => 
   14.27          [
   14.28 @@ -65,7 +65,7 @@
   14.29  (* ------------------------------------------------------------------------ *)
   14.30  
   14.31  qed_goal "lub_mono" thy 
   14.32 -        "[|is_chain(C1::(nat=>'a::cpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
   14.33 +        "[|chain(C1::(nat=>'a::cpo));chain(C2); ! k. C1(k) << C2(k)|]\
   14.34  \           ==> lub(range(C1)) << lub(range(C2))"
   14.35  (fn prems =>
   14.36          [
   14.37 @@ -83,7 +83,7 @@
   14.38  (* ------------------------------------------------------------------------ *)
   14.39  
   14.40  qed_goal "lub_equal" thy
   14.41 -"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k. C1(k)=C2(k)|]\
   14.42 +"[| chain(C1::(nat=>'a::cpo));chain(C2);!k. C1(k)=C2(k)|]\
   14.43  \       ==> lub(range(C1))=lub(range(C2))"
   14.44  (fn prems =>
   14.45          [
   14.46 @@ -108,7 +108,7 @@
   14.47  (* ------------------------------------------------------------------------ *)
   14.48  
   14.49  qed_goal "lub_mono2" thy 
   14.50 -"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
   14.51 +"[|? j.!i. j<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
   14.52  \ ==> lub(range(X))<<lub(range(Y))"
   14.53   (fn prems =>
   14.54          [
   14.55 @@ -137,7 +137,7 @@
   14.56          ]);
   14.57  
   14.58  qed_goal "lub_equal2" thy 
   14.59 -"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
   14.60 +"[|? j.!i. j<i --> X(i)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
   14.61  \ ==> lub(range(X))=lub(range(Y))"
   14.62   (fn prems =>
   14.63          [
   14.64 @@ -153,7 +153,7 @@
   14.65          (Fast_tac 1)
   14.66          ]);
   14.67  
   14.68 -qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::cpo);is_chain(X);\
   14.69 +qed_goal "lub_mono3" thy "[|chain(Y::nat=>'a::cpo);chain(X);\
   14.70  \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
   14.71   (fn prems =>
   14.72          [
   14.73 @@ -206,7 +206,7 @@
   14.74          ]);
   14.75  
   14.76  qed_goal "chain_UU_I" thy
   14.77 -        "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
   14.78 +        "[|chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
   14.79   (fn prems =>
   14.80          [
   14.81          (cut_facts_tac prems 1),
   14.82 @@ -256,7 +256,7 @@
   14.83  
   14.84  
   14.85  qed_goal "chain_mono2" thy 
   14.86 -"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
   14.87 +"[|? j.~Y(j)=UU;chain(Y::nat=>'a::pcpo)|]\
   14.88  \ ==> ? j.!i. j<i-->~Y(i)=UU"
   14.89   (fn prems =>
   14.90          [
   14.91 @@ -275,11 +275,11 @@
   14.92  (**************************************)
   14.93  
   14.94  (* ------------------------------------------------------------------------ *)
   14.95 -(* flat types are chain_finite                                              *)
   14.96 +(* flat types are chfin                                              *)
   14.97  (* ------------------------------------------------------------------------ *)
   14.98  
   14.99 -qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
  14.100 -        "!Y::nat=>'a::flat. is_chain Y-->(? n. max_in_chain n Y)"
  14.101 +qed_goalw "flat_imp_chfin" thy [max_in_chain_def]
  14.102 +        "!Y::nat=>'a::flat. chain Y-->(? n. max_in_chain n Y)"
  14.103   (fn _ =>
  14.104          [
  14.105          (strip_tac 1),
  14.106 @@ -309,7 +309,7 @@
  14.107  	]);
  14.108  
  14.109  qed_goal "chfin2finch" thy 
  14.110 -    "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
  14.111 +    "chain (Y::nat=>'a::chfin) ==> finite_chain Y"
  14.112  	(fn prems => 
  14.113  	[
  14.114  	cut_facts_tac prems 1,
  14.115 @@ -322,8 +322,8 @@
  14.116  (* ------------------------------------------------------------------------ *)
  14.117  
  14.118  qed_goal "infinite_chain_adm_lemma" Porder.thy 
  14.119 -"[|is_chain Y; !i. P (Y i); \
  14.120 -\  (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
  14.121 +"[|chain Y; !i. P (Y i); \
  14.122 +\  (!!Y. [| chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
  14.123  \ |] ==> P (lub (range Y))"
  14.124   (fn prems => [
  14.125          cut_facts_tac prems 1,
  14.126 @@ -334,8 +334,8 @@
  14.127          etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
  14.128  
  14.129  qed_goal "increasing_chain_adm_lemma" Porder.thy 
  14.130 -"[|is_chain Y; !i. P (Y i); \
  14.131 -\  (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
  14.132 +"[|chain Y; !i. P (Y i); \
  14.133 +\  (!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
  14.134  \ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
  14.135   (fn prems => [
  14.136          cut_facts_tac prems 1,
    15.1 --- a/src/HOLCF/Pcpo.thy	Tue Mar 10 18:32:37 1998 +0100
    15.2 +++ b/src/HOLCF/Pcpo.thy	Tue Mar 10 18:33:13 1998 +0100
    15.3 @@ -11,7 +11,7 @@
    15.4  (* ********************************************** *)
    15.5  axclass cpo < po
    15.6          (* class axiom: *)
    15.7 -  cpo   "is_chain S ==> ? x. range(S) <<| (x::'a::po)" 
    15.8 +  cpo   "chain S ==> ? x. range(S) <<| (x::'a::po)" 
    15.9  
   15.10  (* The class pcpo of pointed cpos *)
   15.11  (* ****************************** *)
   15.12 @@ -32,7 +32,7 @@
   15.13  
   15.14  axclass chfin<cpo
   15.15  
   15.16 -chfin 	"!Y. is_chain Y-->(? n. max_in_chain n Y)"
   15.17 +chfin 	"!Y. chain Y-->(? n. max_in_chain n Y)"
   15.18  
   15.19  axclass flat<pcpo
   15.20  
    16.1 --- a/src/HOLCF/Porder.ML	Tue Mar 10 18:32:37 1998 +0100
    16.2 +++ b/src/HOLCF/Porder.ML	Tue Mar 10 18:33:13 1998 +0100
    16.3 @@ -28,7 +28,7 @@
    16.4  (* chains are monotone functions                                            *)
    16.5  (* ------------------------------------------------------------------------ *)
    16.6  
    16.7 -qed_goalw "chain_mono" thy [is_chain] "is_chain F ==> x<y --> F x<<F y"
    16.8 +qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
    16.9  ( fn prems =>
   16.10          [
   16.11          (cut_facts_tac prems 1),
   16.12 @@ -47,7 +47,7 @@
   16.13          (atac 1)
   16.14          ]);
   16.15  
   16.16 -qed_goal "chain_mono3" thy "[| is_chain F; x <= y |] ==> F x << F y"
   16.17 +qed_goal "chain_mono3" thy "[| chain F; x <= y |] ==> F x << F y"
   16.18   (fn prems =>
   16.19          [
   16.20          (cut_facts_tac prems 1),
   16.21 @@ -64,8 +64,8 @@
   16.22  (* The range of a chain is a totaly ordered     <<                           *)
   16.23  (* ------------------------------------------------------------------------ *)
   16.24  
   16.25 -qed_goalw "chain_is_tord" thy [is_tord] 
   16.26 -"!!F. is_chain(F) ==> is_tord(range(F))"
   16.27 +qed_goalw "chain_tord" thy [tord] 
   16.28 +"!!F. chain(F) ==> tord(range(F))"
   16.29   (fn _ =>
   16.30          [
   16.31          Safe_tac,
   16.32 @@ -138,13 +138,13 @@
   16.33          (atac 1)
   16.34          ]);
   16.35  
   16.36 -qed_goalw "is_chainE" thy [is_chain] "is_chain F ==> !i. F(i) << F(Suc(i))"
   16.37 +qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
   16.38  (fn prems =>
   16.39          [
   16.40          (cut_facts_tac prems 1),
   16.41          (atac 1)]);
   16.42  
   16.43 -qed_goalw "is_chainI" thy [is_chain] "!i. F i << F(Suc i) ==> is_chain F"
   16.44 +qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
   16.45  (fn prems =>
   16.46          [
   16.47          (cut_facts_tac prems 1),
   16.48 @@ -185,7 +185,7 @@
   16.49  (* ------------------------------------------------------------------------ *)
   16.50  
   16.51  qed_goalw "lub_finch1" thy [max_in_chain_def]
   16.52 -        "[| is_chain C; max_in_chain i C|] ==> range C <<| C i"
   16.53 +        "[| chain C; max_in_chain i C|] ==> range C <<| C i"
   16.54  (fn prems =>
   16.55          [
   16.56          (cut_facts_tac prems 1),
   16.57 @@ -218,11 +218,11 @@
   16.58          ]);
   16.59  
   16.60  
   16.61 -qed_goal "bin_chain" thy "x<<y ==> is_chain (%i. if i=0 then x else y)"
   16.62 +qed_goal "bin_chain" thy "x<<y ==> chain (%i. if i=0 then x else y)"
   16.63   (fn prems =>
   16.64          [
   16.65          (cut_facts_tac prems 1),
   16.66 -        (rtac is_chainI 1),
   16.67 +        (rtac chainI 1),
   16.68          (rtac allI 1),
   16.69          (nat_ind_tac "i" 1),
   16.70          (Asm_simp_tac 1),
    17.1 --- a/src/HOLCF/Porder.thy	Tue Mar 10 18:32:37 1998 +0100
    17.2 +++ b/src/HOLCF/Porder.thy	Tue Mar 10 18:33:13 1998 +0100
    17.3 @@ -13,8 +13,8 @@
    17.4          "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)
    17.5          "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)
    17.6          lub     ::      "'a set => 'a::po"
    17.7 -        is_tord ::      "'a::po set => bool"
    17.8 -        is_chain ::     "(nat=>'a::po) => bool"
    17.9 +        tord ::      "'a::po set => bool"
   17.10 +        chain ::     "(nat=>'a::po) => bool"
   17.11          max_in_chain :: "[nat,nat=>'a::po]=>bool"
   17.12          finite_chain :: "(nat=>'a::po)=>bool"
   17.13  
   17.14 @@ -37,14 +37,14 @@
   17.15  is_lub          "S <<| x == S <| x & (! u. S <| u  --> x << u)"
   17.16  
   17.17  (* Arbitrary chains are total orders    *)                  
   17.18 -is_tord         "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
   17.19 +tord         "tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
   17.20  
   17.21  (* Here we use countable chains and I prefer to code them as functions! *)
   17.22 -is_chain        "is_chain F == (! i. F(i) << F(Suc(i)))"
   17.23 +chain        "chain F == (! i. F(i) << F(Suc(i)))"
   17.24  
   17.25  (* finite chains, needed for monotony of continouous functions *)
   17.26  max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
   17.27 -finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
   17.28 +finite_chain_def "finite_chain C == chain(C) & (? i. max_in_chain i C)"
   17.29  
   17.30  lub_def          "lub S == (@x. S <<| x)"
   17.31  
    18.1 --- a/src/HOLCF/Sprod2.ML	Tue Mar 10 18:32:37 1998 +0100
    18.2 +++ b/src/HOLCF/Sprod2.ML	Tue Mar 10 18:33:13 1998 +0100
    18.3 @@ -95,7 +95,7 @@
    18.4  (* ------------------------------------------------------------------------ *)
    18.5  
    18.6  qed_goal "lub_sprod" Sprod2.thy 
    18.7 -"[|is_chain(S)|] ==> range(S) <<| \
    18.8 +"[|chain(S)|] ==> range(S) <<| \
    18.9  \ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
   18.10  (fn prems =>
   18.11          [
   18.12 @@ -123,7 +123,7 @@
   18.13  
   18.14  
   18.15  qed_goal "cpo_sprod" Sprod2.thy 
   18.16 -        "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
   18.17 +        "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
   18.18  (fn prems =>
   18.19          [
   18.20          (cut_facts_tac prems 1),
    19.1 --- a/src/HOLCF/Sprod3.ML	Tue Mar 10 18:32:37 1998 +0100
    19.2 +++ b/src/HOLCF/Sprod3.ML	Tue Mar 10 18:33:13 1998 +0100
    19.3 @@ -19,7 +19,7 @@
    19.4  (* ------------------------------------------------------------------------ *)
    19.5  
    19.6  qed_goal "sprod3_lemma1" thy 
    19.7 -"[| is_chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
    19.8 +"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
    19.9  \ Ispair (lub(range Y)) x =\
   19.10  \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
   19.11  \        (lub(range(%i. Issnd(Ispair(Y i) x))))"
   19.12 @@ -56,7 +56,7 @@
   19.13          ]);
   19.14  
   19.15  qed_goal "sprod3_lemma2" thy 
   19.16 -"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
   19.17 +"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
   19.18  \   Ispair (lub(range Y)) x =\
   19.19  \   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
   19.20  \          (lub(range(%i. Issnd(Ispair(Y i) x))))"
   19.21 @@ -78,7 +78,7 @@
   19.22  
   19.23  
   19.24  qed_goal "sprod3_lemma3" thy 
   19.25 -"[| is_chain(Y); x = UU |] ==>\
   19.26 +"[| chain(Y); x = UU |] ==>\
   19.27  \          Ispair (lub(range Y)) x =\
   19.28  \          Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
   19.29  \                 (lub(range(%i. Issnd(Ispair (Y i) x))))"
   19.30 @@ -124,7 +124,7 @@
   19.31          ]);
   19.32  
   19.33  qed_goal "sprod3_lemma4" thy 
   19.34 -"[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
   19.35 +"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
   19.36  \         Ispair x (lub(range Y)) =\
   19.37  \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
   19.38  \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
   19.39 @@ -160,7 +160,7 @@
   19.40          ]);
   19.41  
   19.42  qed_goal "sprod3_lemma5" thy 
   19.43 -"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
   19.44 +"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
   19.45  \         Ispair x (lub(range Y)) =\
   19.46  \         Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
   19.47  \                (lub(range(%i. Issnd(Ispair x (Y i)))))"
   19.48 @@ -181,7 +181,7 @@
   19.49          ]);
   19.50  
   19.51  qed_goal "sprod3_lemma6" thy 
   19.52 -"[| is_chain(Y); x = UU |] ==>\
   19.53 +"[| chain(Y); x = UU |] ==>\
   19.54  \         Ispair x (lub(range Y)) =\
   19.55  \         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
   19.56  \                (lub(range(%i. Issnd (Ispair x (Y i)))))"
   19.57 @@ -563,7 +563,7 @@
   19.58  
   19.59  
   19.60  qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
   19.61 -"[|is_chain(S)|] ==> range(S) <<| \
   19.62 +"[|chain(S)|] ==> range(S) <<| \
   19.63  \ (| lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) |)"
   19.64   (fn prems =>
   19.65          [
   19.66 @@ -580,7 +580,7 @@
   19.67  
   19.68  bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
   19.69  (*
   19.70 - "is_chain ?S1 ==>
   19.71 + "chain ?S1 ==>
   19.72   lub (range ?S1) =
   19.73   (|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm
   19.74  *)
    20.1 --- a/src/HOLCF/Ssum2.ML	Tue Mar 10 18:32:37 1998 +0100
    20.2 +++ b/src/HOLCF/Ssum2.ML	Tue Mar 10 18:33:13 1998 +0100
    20.3 @@ -198,7 +198,7 @@
    20.4  
    20.5  
    20.6  qed_goal "ssum_lemma3" thy 
    20.7 -"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
    20.8 +"[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
    20.9  \ (!i.? y. Y(i)=Isinr(y))"
   20.10   (fn prems =>
   20.11          [
   20.12 @@ -231,7 +231,7 @@
   20.13          ]);
   20.14  
   20.15  qed_goal "ssum_lemma4" thy 
   20.16 -"is_chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
   20.17 +"chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
   20.18   (fn prems =>
   20.19          [
   20.20          (cut_facts_tac prems 1),
   20.21 @@ -317,7 +317,7 @@
   20.22  (* ------------------------------------------------------------------------ *)
   20.23  
   20.24  qed_goal "lub_ssum1a" thy 
   20.25 -"[|is_chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
   20.26 +"[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
   20.27  \ range(Y) <<|\
   20.28  \ Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
   20.29   (fn prems =>
   20.30 @@ -358,7 +358,7 @@
   20.31  
   20.32  
   20.33  qed_goal "lub_ssum1b" thy 
   20.34 -"[|is_chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
   20.35 +"[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
   20.36  \ range(Y) <<|\
   20.37  \ Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
   20.38   (fn prems =>
   20.39 @@ -400,20 +400,20 @@
   20.40  
   20.41  bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI);
   20.42  (*
   20.43 -[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
   20.44 +[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
   20.45   lub (range ?Y1) = Isinl
   20.46   (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
   20.47  *)
   20.48  
   20.49  bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI);
   20.50  (*
   20.51 -[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
   20.52 +[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
   20.53   lub (range ?Y1) = Isinr
   20.54   (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
   20.55  *)
   20.56  
   20.57  qed_goal "cpo_ssum" thy 
   20.58 -        "is_chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
   20.59 +        "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
   20.60   (fn prems =>
   20.61          [
   20.62          (cut_facts_tac prems 1),
    21.1 --- a/src/HOLCF/Ssum3.ML	Tue Mar 10 18:32:37 1998 +0100
    21.2 +++ b/src/HOLCF/Ssum3.ML	Tue Mar 10 18:33:13 1998 +0100
    21.3 @@ -156,7 +156,7 @@
    21.4  (* ------------------------------------------------------------------------ *)
    21.5  
    21.6  qed_goal "ssum_lemma9" Ssum3.thy 
    21.7 -"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
    21.8 +"[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
    21.9   (fn prems =>
   21.10          [
   21.11          (cut_facts_tac prems 1),
   21.12 @@ -174,7 +174,7 @@
   21.13  
   21.14  
   21.15  qed_goal "ssum_lemma10" Ssum3.thy 
   21.16 -"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
   21.17 +"[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
   21.18   (fn prems =>
   21.19          [
   21.20          (cut_facts_tac prems 1),
   21.21 @@ -193,7 +193,7 @@
   21.22          ]);
   21.23  
   21.24  qed_goal "ssum_lemma11" Ssum3.thy 
   21.25 -"[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
   21.26 +"[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
   21.27  \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
   21.28   (fn prems =>
   21.29          [
   21.30 @@ -210,7 +210,7 @@
   21.31          ]);
   21.32  
   21.33  qed_goal "ssum_lemma12" Ssum3.thy 
   21.34 -"[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
   21.35 +"[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
   21.36  \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
   21.37   (fn prems =>
   21.38          [
   21.39 @@ -269,7 +269,7 @@
   21.40  
   21.41  
   21.42  qed_goal "ssum_lemma13" Ssum3.thy 
   21.43 -"[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
   21.44 +"[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
   21.45  \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
   21.46   (fn prems =>
   21.47          [
   21.48 @@ -579,7 +579,7 @@
   21.49          ]);
   21.50  
   21.51  qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] 
   21.52 -        "is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
   21.53 +        "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
   21.54   (fn prems =>
   21.55          [
   21.56          (cut_facts_tac prems 1),
   21.57 @@ -589,7 +589,7 @@
   21.58  
   21.59  
   21.60  qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
   21.61 -"[| is_chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
   21.62 +"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ 
   21.63  \   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))"
   21.64   (fn prems =>
   21.65          [
   21.66 @@ -614,7 +614,7 @@
   21.67          ]);
   21.68  
   21.69  qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
   21.70 -"[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
   21.71 +"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
   21.72  \   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
   21.73   (fn prems =>
   21.74          [
   21.75 @@ -641,7 +641,7 @@
   21.76          ]);
   21.77  
   21.78  qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] 
   21.79 -        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
   21.80 +        "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
   21.81   (fn prems =>
   21.82          [
   21.83          (cut_facts_tac prems 1),
   21.84 @@ -655,7 +655,7 @@
   21.85          ]);
   21.86  
   21.87  qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] 
   21.88 -        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
   21.89 +        "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
   21.90   (fn prems =>
   21.91          [
   21.92          (cut_facts_tac prems 1),
   21.93 @@ -669,7 +669,7 @@
   21.94          ]);
   21.95  
   21.96  qed_goal "thelub_ssum3" Ssum3.thy  
   21.97 -"is_chain(Y) ==>\ 
   21.98 +"chain(Y) ==>\ 
   21.99  \   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
  21.100  \ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  21.101   (fn prems =>
    22.1 --- a/src/HOLCF/Up2.ML	Tue Mar 10 18:32:37 1998 +0100
    22.2 +++ b/src/HOLCF/Up2.ML	Tue Mar 10 18:33:13 1998 +0100
    22.3 @@ -111,7 +111,7 @@
    22.4  (* ------------------------------------------------------------------------ *)
    22.5  
    22.6  qed_goal "lub_up1a" thy 
    22.7 -"[|is_chain(Y);? i x. Y(i)=Iup(x)|] ==>\
    22.8 +"[|chain(Y);? i x. Y(i)=Iup(x)|] ==>\
    22.9  \ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
   22.10   (fn prems =>
   22.11          [
   22.12 @@ -148,7 +148,7 @@
   22.13          ]);
   22.14  
   22.15  qed_goal "lub_up1b" thy 
   22.16 -"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
   22.17 +"[|chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
   22.18  \ range(Y) <<| Abs_Up (Inl ())"
   22.19   (fn prems =>
   22.20          [
   22.21 @@ -172,18 +172,18 @@
   22.22  
   22.23  bind_thm ("thelub_up1a", lub_up1a RS thelubI);
   22.24  (*
   22.25 -[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
   22.26 +[| chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
   22.27   lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
   22.28  *)
   22.29  
   22.30  bind_thm ("thelub_up1b", lub_up1b RS thelubI);
   22.31  (*
   22.32 -[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
   22.33 +[| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
   22.34   lub (range ?Y1) = UU_up
   22.35  *)
   22.36  
   22.37  qed_goal "cpo_up" thy 
   22.38 -        "is_chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
   22.39 +        "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
   22.40   (fn prems =>
   22.41          [
   22.42          (cut_facts_tac prems 1),
    23.1 --- a/src/HOLCF/Up3.ML	Tue Mar 10 18:32:37 1998 +0100
    23.2 +++ b/src/HOLCF/Up3.ML	Tue Mar 10 18:33:13 1998 +0100
    23.3 @@ -230,7 +230,7 @@
    23.4          ]);
    23.5  
    23.6  qed_goalw "thelub_up2a" thy [up_def,fup_def] 
    23.7 -"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\
    23.8 +"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
    23.9  \      lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
   23.10   (fn prems =>
   23.11          [
   23.12 @@ -255,7 +255,7 @@
   23.13  
   23.14  
   23.15  qed_goalw "thelub_up2b" thy [up_def,fup_def] 
   23.16 -"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
   23.17 +"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
   23.18   (fn prems =>
   23.19          [
   23.20          (cut_facts_tac prems 1),
   23.21 @@ -289,7 +289,7 @@
   23.22  
   23.23  
   23.24  qed_goal "thelub_up2a_rev" thy  
   23.25 -"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
   23.26 +"[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
   23.27   (fn prems =>
   23.28          [
   23.29          (cut_facts_tac prems 1),
   23.30 @@ -303,7 +303,7 @@
   23.31          ]);
   23.32  
   23.33  qed_goal "thelub_up2b_rev" thy  
   23.34 -"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
   23.35 +"[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up`x"
   23.36   (fn prems =>
   23.37          [
   23.38          (cut_facts_tac prems 1),
   23.39 @@ -316,7 +316,7 @@
   23.40  
   23.41  
   23.42  qed_goal "thelub_up3" thy  
   23.43 -"is_chain(Y) ==> lub(range(Y)) = UU |\
   23.44 +"chain(Y) ==> lub(range(Y)) = UU |\
   23.45  \                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
   23.46   (fn prems =>
   23.47          [
    24.1 --- a/src/HOLCF/adm.ML	Tue Mar 10 18:32:37 1998 +0100
    24.2 +++ b/src/HOLCF/adm.ML	Tue Mar 10 18:33:13 1998 +0100
    24.3 @@ -10,7 +10,7 @@
    24.4    [| cont t; adm P |] ==> adm (%x. P (t x))
    24.5  
    24.6  "t" is instantiated with a term of chain-finite type, so that
    24.7 -adm_chain_finite can be applied:
    24.8 +adm_chfin can be applied:
    24.9  
   24.10    adm (P::'a::{chfin,pcpo} => bool)
   24.11  
   24.12 @@ -177,7 +177,7 @@
   24.13                  compose_tac (false, rule, 2) i THEN
   24.14                  rtac cont_thm i THEN
   24.15                  REPEAT (assume_tac i) THEN
   24.16 -                rtac adm_chain_finite i
   24.17 +                rtac adm_chfin i
   24.18                end 
   24.19            | [] => no_tac)
   24.20          end)
    25.1 --- a/src/HOLCF/domain/theorems.ML	Tue Mar 10 18:32:37 1998 +0100
    25.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Mar 10 18:33:13 1998 +0100
    25.3 @@ -41,7 +41,7 @@
    25.4                                  asm_simp_tac (HOLCF_ss addsimps rews) i;
    25.5  
    25.6  val chain_tac = REPEAT_DETERM o resolve_tac 
    25.7 -                [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
    25.8 +                [chain_iterate, ch2ch_fappR, ch2ch_fappL];
    25.9  
   25.10  (* ----- general proofs ----------------------------------------------------- *)
   25.11  
    26.1 --- a/src/HOLCF/ex/Stream.ML	Tue Mar 10 18:32:37 1998 +0100
    26.2 +++ b/src/HOLCF/ex/Stream.ML	Tue Mar 10 18:33:13 1998 +0100
    26.3 @@ -136,12 +136,12 @@
    26.4  	(stac fix_def2 1),
    26.5  	(rewrite_goals_tac [stream.take_def]),
    26.6  	(stac contlub_cfun_fun 1),
    26.7 -	(rtac is_chain_iterate 1),
    26.8 +	(rtac chain_iterate 1),
    26.9  	(rtac refl 1)
   26.10  	]);
   26.11  
   26.12 -qed_goal "chain_stream_take" thy "is_chain (%i. stream_take i`s)" (fn _ => [
   26.13 -	rtac is_chainI 1,
   26.14 +qed_goal "chain_stream_take" thy "chain (%i. stream_take i`s)" (fn _ => [
   26.15 +	rtac chainI 1,
   26.16  	subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
   26.17  	fast_tac HOL_cs 1,
   26.18  	rtac allI 1,
   26.19 @@ -160,10 +160,10 @@
   26.20  		rtac monofun_cfun_fun 1,
   26.21  		stac fix_def2 1,
   26.22  		rtac is_ub_thelub 1,
   26.23 -		rtac is_chain_iterate 1,
   26.24 +		rtac chain_iterate 1,
   26.25  		etac subst 1, (* 2*back(); *)
   26.26  		rtac monofun_cfun_fun 1,
   26.27 -		rtac (rewrite_rule [is_chain] is_chain_iterate RS spec) 1]);
   26.28 +		rtac (rewrite_rule [chain] chain_iterate RS spec) 1]);
   26.29  
   26.30  (*
   26.31  val stream_take_lemma2 = prove_goal thy 
    27.1 --- a/src/HOLCF/ex/loeckx.ML	Tue Mar 10 18:32:37 1998 +0100
    27.2 +++ b/src/HOLCF/ex/loeckx.ML	Tue Mar 10 18:33:13 1998 +0100
    27.3 @@ -8,13 +8,13 @@
    27.4  by (rtac ch2ch_fun 1);
    27.5  back();
    27.6  by (rtac refl 2);
    27.7 -by (rtac is_chainI 1);
    27.8 +by (rtac chainI 1);
    27.9  by (strip_tac 1);
   27.10  by (rtac (less_fun RS iffD2) 1);
   27.11  by (strip_tac 1);
   27.12  by (rtac (less_fun RS iffD2) 1);
   27.13  by (strip_tac 1);
   27.14 -by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
   27.15 +by (rtac (chain_iterate RS chainE RS spec) 1);
   27.16  val loeckx_sieber = result();
   27.17  
   27.18  (* 
   27.19 @@ -27,7 +27,7 @@
   27.20  Since we already proved the theorem
   27.21  
   27.22  val cont_lubcfun = prove_goal Cfun2.thy 
   27.23 -        "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
   27.24 +        "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
   27.25  
   27.26  
   27.27  it suffices to prove:
   27.28 @@ -64,7 +64,7 @@
   27.29  by (rtac cont_iterate 1);
   27.30  by (rtac refl 1);
   27.31  by (rtac cont_lubcfun 1);
   27.32 -by (rtac is_chainI 1);
   27.33 +by (rtac chainI 1);
   27.34  by (strip_tac 1);
   27.35  by (rtac less_cfun2 1);
   27.36  by (stac beta_cfun 1);
   27.37 @@ -73,7 +73,7 @@
   27.38  by (stac beta_cfun 1);
   27.39  by (rtac  cont2cont_CF1L 1);
   27.40  by (rtac cont_iterate 1);
   27.41 -by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
   27.42 +by (rtac (chain_iterate RS chainE RS spec) 1);
   27.43  val cont_Ifix2 = result();
   27.44  
   27.45  (* the proof in little steps *)
   27.46 @@ -97,14 +97,14 @@
   27.47  
   27.48  (*
   27.49  - cont_lubcfun;
   27.50 -val it = "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
   27.51 +val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
   27.52  
   27.53  *)
   27.54  
   27.55  val prems = goal Fix.thy "cont Ifix";
   27.56  by (stac fix_lemma2 1);
   27.57  by (rtac cont_lubcfun 1);
   27.58 -by (rtac is_chainI 1);
   27.59 +by (rtac chainI 1);
   27.60  by (strip_tac 1);
   27.61  by (rtac less_cfun2 1);
   27.62  by (stac beta_cfun 1);
   27.63 @@ -113,6 +113,6 @@
   27.64  by (stac beta_cfun 1);
   27.65  by (rtac  cont2cont_CF1L 1);
   27.66  by (rtac cont_iterate 1);
   27.67 -by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
   27.68 +by (rtac (chain_iterate RS chainE RS spec) 1);
   27.69  val cont_Ifix2 = result();
   27.70