--- a/src/HOLCF/Cfun2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cfun2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -75,10 +75,10 @@
(* ------------------------------------------------------------------------ *)
bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
-(* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *)
+(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *)
bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
-(* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
+(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
(* ------------------------------------------------------------------------ *)
@@ -138,7 +138,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ch2ch_fappR" thy
- "is_chain(Y) ==> is_chain(%i. f`(Y i))"
+ "chain(Y) ==> chain(%i. f`(Y i))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -147,7 +147,7 @@
bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
-(* is_chain(?F) ==> is_chain (%i. ?F i`?x) *)
+(* chain(?F) ==> chain (%i. ?F i`?x) *)
(* ------------------------------------------------------------------------ *)
@@ -156,7 +156,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cfun_mono" thy
- "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
+ "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -172,7 +172,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ex_lubcfun" thy
- "[| is_chain(F); is_chain(Y) |] ==>\
+ "[| chain(F); chain(Y) |] ==>\
\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
(fn prems =>
@@ -190,7 +190,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "cont_lubcfun" thy
- "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
+ "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -209,7 +209,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cfun" thy
- "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
+ "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -233,11 +233,11 @@
bind_thm ("thelub_cfun", lub_cfun RS thelubI);
(*
-is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
+chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
*)
qed_goal "cpo_cfun" thy
- "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
+ "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cfun3.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cfun3.ML Tue Mar 10 18:33:13 1998 +0100
@@ -52,7 +52,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "contlub_cfun_fun" thy
-"is_chain(FY) ==>\
+"chain(FY) ==>\
\ lub(range FY)`x = lub(range (%i. FY(i)`x))"
(fn prems =>
[
@@ -66,7 +66,7 @@
qed_goal "cont_cfun_fun" thy
-"is_chain(FY) ==>\
+"chain(FY) ==>\
\ range(%i. FY(i)`x) <<| lub(range FY)`x"
(fn prems =>
[
@@ -82,7 +82,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "contlub_cfun" thy
-"[|is_chain(FY);is_chain(TY)|] ==>\
+"[|chain(FY);chain(TY)|] ==>\
\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
(fn prems =>
[
@@ -96,7 +96,7 @@
]);
qed_goal "cont_cfun" thy
-"[|is_chain(FY);is_chain(TY)|] ==>\
+"[|chain(FY);chain(TY)|] ==>\
\ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
(fn prems =>
[
@@ -373,11 +373,11 @@
(*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
(* ------------------------------------------------------------------------ *)
-(* some lemmata for functions with flat/chain_finite domain/range types *)
+(* some lemmata for functions with flat/chfin domain/range types *)
(* ------------------------------------------------------------------------ *)
qed_goal "chfin_fappR" thy
- "is_chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s"
+ "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s"
(fn prems =>
[
cut_facts_tac prems 1,
@@ -441,15 +441,15 @@
(* propagation of flatness and chainfiniteness by continuous isomorphisms *)
(* ------------------------------------------------------------------------ *)
-qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. is_chain Y --> (? n. max_in_chain n Y); \
+qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
-\ ==> ! Y::nat=>'b. is_chain Y --> (? n. max_in_chain n Y)"
+\ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)"
(fn prems =>
[
(rewtac max_in_chain_def),
(strip_tac 1),
(rtac exE 1),
- (res_inst_tac [("P","is_chain(%i. g`(Y i))")] mp 1),
+ (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
(etac spec 1),
(etac ch2ch_fappR 1),
(rtac exI 1),
--- a/src/HOLCF/Cont.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cont.ML Tue Mar 10 18:33:13 1998 +0100
@@ -13,7 +13,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "contlubI" thy [contlub]
- "! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
+ "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
\ contlub(f)"
(fn prems =>
[
@@ -23,7 +23,7 @@
qed_goalw "contlubE" thy [contlub]
" contlub(f)==>\
-\ ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
+\ ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -32,7 +32,7 @@
qed_goalw "contI" thy [cont]
- "! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
+ "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -40,7 +40,7 @@
]);
qed_goalw "contE" thy [cont]
- "cont(f) ==> ! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
+ "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -74,14 +74,14 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ch2ch_monofun" thy
- "[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
+ "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac is_chainI 1),
+ (rtac chainI 1),
(rtac allI 1),
(etac (monofunE RS spec RS spec RS mp) 1),
- (etac (is_chainE RS spec) 1)
+ (etac (chainE RS spec) 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -194,7 +194,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ch2ch_MF2L" thy
-"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)"
+"[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -204,7 +204,7 @@
qed_goal "ch2ch_MF2R" thy
-"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))"
+"[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -213,36 +213,36 @@
]);
qed_goal "ch2ch_MF2LR" thy
-"[|monofun(MF2); !f. monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
-\ is_chain(%i. MF2(F(i))(Y(i)))"
+"[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> \
+\ chain(%i. MF2(F(i))(Y(i)))"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac is_chainI 1),
+ (rtac chainI 1),
(strip_tac 1 ),
(rtac trans_less 1),
- (etac (ch2ch_MF2L RS is_chainE RS spec) 1),
+ (etac (ch2ch_MF2L RS chainE RS spec) 1),
(atac 1),
((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
- (etac (is_chainE RS spec) 1)
+ (etac (chainE RS spec) 1)
]);
qed_goal "ch2ch_lubMF2R" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\ is_chain(F);is_chain(Y)|] ==> \
-\ is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
+\ chain(F);chain(Y)|] ==> \
+\ chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (lub_mono RS allI RS is_chainI) 1),
+ (rtac (lub_mono RS allI RS chainI) 1),
((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
(atac 1),
((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
(atac 1),
(strip_tac 1),
- (rtac (is_chainE RS spec) 1),
+ (rtac (chainE RS spec) 1),
(etac ch2ch_MF2L 1),
(atac 1)
]);
@@ -251,18 +251,18 @@
qed_goal "ch2ch_lubMF2L" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\ is_chain(F);is_chain(Y)|] ==> \
-\ is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
+\ chain(F);chain(Y)|] ==> \
+\ chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (lub_mono RS allI RS is_chainI) 1),
+ (rtac (lub_mono RS allI RS chainI) 1),
(etac ch2ch_MF2L 1),
(atac 1),
(etac ch2ch_MF2L 1),
(atac 1),
(strip_tac 1),
- (rtac (is_chainE RS spec) 1),
+ (rtac (chainE RS spec) 1),
((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
(atac 1)
]);
@@ -271,7 +271,7 @@
qed_goal "lub_MF2_mono" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\ is_chain(F)|] ==> \
+\ chain(F)|] ==> \
\ monofun(% x. lub(range(% j. MF2 (F j) (x))))"
(fn prems =>
[
@@ -291,7 +291,7 @@
qed_goal "ex_lubMF2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\ is_chain(F); is_chain(Y)|] ==> \
+\ chain(F); chain(Y)|] ==> \
\ lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
\ lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
(fn prems =>
@@ -330,7 +330,7 @@
qed_goal "diag_lubMF2_1" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\ is_chain(FY);is_chain(TY)|] ==>\
+\ chain(FY);chain(TY)|] ==>\
\ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. MF2(FY(i))(TY(i))))"
(fn prems =>
@@ -374,7 +374,7 @@
qed_goal "diag_lubMF2_2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
\ !f. monofun(MF2(f)::('b::po=>'c::cpo));\
-\ is_chain(FY);is_chain(TY)|] ==>\
+\ chain(FY);chain(TY)|] ==>\
\ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
\ lub(range(%i. MF2(FY(i))(TY(i))))"
(fn prems =>
@@ -394,7 +394,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "contlub_CF2" thy
-"[|cont(CF2);!f. cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+"[|cont(CF2);!f. cont(CF2(f));chain(FY);chain(TY)|] ==>\
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
(fn prems =>
[
@@ -524,7 +524,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "contlub_abstraction" thy
-"[|is_chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
+"[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
\ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
(fn prems =>
[
--- a/src/HOLCF/Cont.thy Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cont.thy Tue Mar 10 18:33:13 1998 +0100
@@ -27,10 +27,10 @@
monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)"
-contlub "contlub(f) == ! Y. is_chain(Y) -->
+contlub "contlub(f) == ! Y. chain(Y) -->
f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
-cont "cont(f) == ! Y. is_chain(Y) -->
+cont "cont(f) == ! Y. chain(Y) -->
range(% i. f(Y(i))) <<| f(lub(range(Y)))"
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Cprod2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cprod2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -116,7 +116,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_cprod" thy
-"is_chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
+"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -141,13 +141,13 @@
bind_thm ("thelub_cprod", lub_cprod RS thelubI);
(*
-"is_chain ?S1 ==>
+"chain ?S1 ==>
lub (range ?S1) =
(lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
*)
-qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
+qed_goal "cpo_cprod" thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cprod3.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Cprod3.ML Tue Mar 10 18:33:13 1998 +0100
@@ -20,7 +20,7 @@
(* ------------------------------------------------------------------------ *)
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 =>
@@ -57,7 +57,7 @@
]);
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 =>
@@ -261,7 +261,7 @@
]);
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 =>
[
@@ -277,7 +277,7 @@
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)))>"
*)
--- a/src/HOLCF/Discrete.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Discrete.ML Tue Mar 10 18:33:13 1998 +0100
@@ -10,7 +10,7 @@
Addsimps [undiscr_Discr];
goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
+ "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
--- a/src/HOLCF/Discrete1.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Discrete1.ML Tue Mar 10 18:33:13 1998 +0100
@@ -11,8 +11,8 @@
qed "discr_less_eq";
AddIffs [discr_less_eq];
-goalw thy [is_chain]
- "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
+goalw thy [chain]
+ "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
by (nat_ind_tac "i" 1);
by (rtac refl 1);
by (etac subst 1);
@@ -21,12 +21,12 @@
qed "discr_chain0";
goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
+ "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
by (fast_tac (claset() addEs [discr_chain0]) 1);
qed "discr_chain_range0";
Addsimps [discr_chain_range0];
goalw thy [is_lub,is_ub]
- "!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
+ "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
by (Asm_simp_tac 1);
qed "discr_cpo";
--- a/src/HOLCF/Fix.thy Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Fix.thy Tue Mar 10 18:33:13 1998 +0100
@@ -24,7 +24,7 @@
Ifix_def "Ifix F == lub(range(%i. iterate i F UU))"
fix_def "fix == (LAM f. Ifix f)"
-adm_def "adm P == !Y. is_chain(Y) -->
+adm_def "adm P == !Y. chain(Y) -->
(!i. P(Y i)) --> P(lub(range Y))"
admw_def "admw P == !F. (!n. P (iterate n F UU)) -->
--- a/src/HOLCF/Fun1.thy Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Fun1.thy Tue Mar 10 18:33:13 1998 +0100
@@ -12,7 +12,7 @@
Fun1 = Pcpo +
-instance flat<chfin (flat_imp_chain_finite)
+instance flat<chfin (flat_imp_chfin)
(* to make << defineable: *)
instance fun :: (term,sq_ord)sq_ord
--- a/src/HOLCF/Fun2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Fun2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -52,11 +52,11 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ch2ch_fun" thy
- "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i. S(i)(x))"
+ "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rewtac is_chain),
+ (rewtac chain),
(rtac allI 1),
(rtac spec 1),
(rtac (less_fun RS subst) 1),
@@ -86,7 +86,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_fun" Fun2.thy
- "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
+ "chain(S::nat=>('a::term => 'b::cpo)) ==> \
\ range(S) <<| (% x. lub(range(% i. S(i)(x))))"
(fn prems =>
[
@@ -108,10 +108,10 @@
]);
bind_thm ("thelub_fun", lub_fun RS thelubI);
-(* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
+(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
qed_goal "cpo_fun" Fun2.thy
- "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
+ "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Mar 10 18:33:13 1998 +0100
@@ -920,12 +920,12 @@
by (res_inst_tac [("t","s2")] (seq.reach RS subst) 1);
by (rtac (fix_def2 RS ssubst ) 1);
by (stac contlub_cfun_fun 1);
-by (rtac is_chain_iterate 1);
+by (rtac chain_iterate 1);
by (stac contlub_cfun_fun 1);
-by (rtac is_chain_iterate 1);
+by (rtac chain_iterate 1);
by (rtac lub_mono 1);
-by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
-by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_fappL) 1);
by (rtac allI 1);
by (resolve_tac prems 1);
qed"take_lemma_less1";
--- a/src/HOLCF/Lift2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Lift2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -56,7 +56,7 @@
(* Tailoring chain_mono2 of Pcpo.ML to Undef *)
goal Lift2.thy
-"!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
+"!!Y. [|? j.~Y(j)=Undef;chain(Y::nat=>('a)lift)|] \
\ ==> ? j.!i. j<i-->~Y(i)=Undef";
by Safe_tac;
by (Step_tac 1);
@@ -68,10 +68,10 @@
qed"chain_mono2_po";
-(* Tailoring flat_imp_chain_finite of Fix.ML to lift *)
+(* Tailoring flat_imp_chfin of Fix.ML to lift *)
goal Lift2.thy
- "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
+ "(! Y. chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
by (rewtac max_in_chain_def);
by (strip_tac 1);
by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm 1);
@@ -104,14 +104,14 @@
by (rtac mp 1);
by (etac spec 1);
by (Asm_simp_tac 1);
-qed"flat_imp_chain_finite_poo";
+qed"flat_imp_chfin_poo";
(* Main Lemma: cpo_lift *)
goal Lift2.thy
- "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
-by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
+ "!!Y. chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
+by (cut_inst_tac [] flat_imp_chfin_poo 1);
by (Step_tac 1);
by Safe_tac;
by (Step_tac 1);
--- a/src/HOLCF/Pcpo.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Pcpo.ML Tue Mar 10 18:33:13 1998 +0100
@@ -25,7 +25,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "thelubE" thy
- "[| is_chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
+ "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -40,12 +40,12 @@
bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
-(* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *)
+(* chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *)
bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
-(* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *)
+(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *)
-qed_goal "maxinch_is_thelub" thy "is_chain Y ==> \
+qed_goal "maxinch_is_thelub" thy "chain Y ==> \
\ max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))"
(fn prems =>
[
@@ -65,7 +65,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_mono" thy
- "[|is_chain(C1::(nat=>'a::cpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
+ "[|chain(C1::(nat=>'a::cpo));chain(C2); ! k. C1(k) << C2(k)|]\
\ ==> lub(range(C1)) << lub(range(C2))"
(fn prems =>
[
@@ -83,7 +83,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_equal" thy
-"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k. C1(k)=C2(k)|]\
+"[| chain(C1::(nat=>'a::cpo));chain(C2);!k. C1(k)=C2(k)|]\
\ ==> lub(range(C1))=lub(range(C2))"
(fn prems =>
[
@@ -108,7 +108,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_mono2" thy
-"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
+"[|? j.!i. j<i --> X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
\ ==> lub(range(X))<<lub(range(Y))"
(fn prems =>
[
@@ -137,7 +137,7 @@
]);
qed_goal "lub_equal2" thy
-"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
+"[|? j.!i. j<i --> X(i)=Y(i);chain(X::nat=>'a::cpo);chain(Y)|]\
\ ==> lub(range(X))=lub(range(Y))"
(fn prems =>
[
@@ -153,7 +153,7 @@
(Fast_tac 1)
]);
-qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::cpo);is_chain(X);\
+qed_goal "lub_mono3" thy "[|chain(Y::nat=>'a::cpo);chain(X);\
\! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
(fn prems =>
[
@@ -206,7 +206,7 @@
]);
qed_goal "chain_UU_I" thy
- "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
+ "[|chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -256,7 +256,7 @@
qed_goal "chain_mono2" thy
-"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
+"[|? j.~Y(j)=UU;chain(Y::nat=>'a::pcpo)|]\
\ ==> ? j.!i. j<i-->~Y(i)=UU"
(fn prems =>
[
@@ -275,11 +275,11 @@
(**************************************)
(* ------------------------------------------------------------------------ *)
-(* flat types are chain_finite *)
+(* flat types are chfin *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
- "!Y::nat=>'a::flat. is_chain Y-->(? n. max_in_chain n Y)"
+qed_goalw "flat_imp_chfin" thy [max_in_chain_def]
+ "!Y::nat=>'a::flat. chain Y-->(? n. max_in_chain n Y)"
(fn _ =>
[
(strip_tac 1),
@@ -309,7 +309,7 @@
]);
qed_goal "chfin2finch" thy
- "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
+ "chain (Y::nat=>'a::chfin) ==> finite_chain Y"
(fn prems =>
[
cut_facts_tac prems 1,
@@ -322,8 +322,8 @@
(* ------------------------------------------------------------------------ *)
qed_goal "infinite_chain_adm_lemma" Porder.thy
-"[|is_chain Y; !i. P (Y i); \
-\ (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
+"[|chain Y; !i. P (Y i); \
+\ (!!Y. [| chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
\ |] ==> P (lub (range Y))"
(fn prems => [
cut_facts_tac prems 1,
@@ -334,8 +334,8 @@
etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
qed_goal "increasing_chain_adm_lemma" Porder.thy
-"[|is_chain Y; !i. P (Y i); \
-\ (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
+"[|chain Y; !i. P (Y i); \
+\ (!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
(fn prems => [
cut_facts_tac prems 1,
--- a/src/HOLCF/Pcpo.thy Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Pcpo.thy Tue Mar 10 18:33:13 1998 +0100
@@ -11,7 +11,7 @@
(* ********************************************** *)
axclass cpo < po
(* class axiom: *)
- cpo "is_chain S ==> ? x. range(S) <<| (x::'a::po)"
+ cpo "chain S ==> ? x. range(S) <<| (x::'a::po)"
(* The class pcpo of pointed cpos *)
(* ****************************** *)
@@ -32,7 +32,7 @@
axclass chfin<cpo
-chfin "!Y. is_chain Y-->(? n. max_in_chain n Y)"
+chfin "!Y. chain Y-->(? n. max_in_chain n Y)"
axclass flat<pcpo
--- a/src/HOLCF/Porder.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Porder.ML Tue Mar 10 18:33:13 1998 +0100
@@ -28,7 +28,7 @@
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_mono" thy [is_chain] "is_chain F ==> x<y --> F x<<F y"
+qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
( fn prems =>
[
(cut_facts_tac prems 1),
@@ -47,7 +47,7 @@
(atac 1)
]);
-qed_goal "chain_mono3" thy "[| is_chain F; x <= y |] ==> F x << F y"
+qed_goal "chain_mono3" thy "[| chain F; x <= y |] ==> F x << F y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -64,8 +64,8 @@
(* The range of a chain is a totaly ordered << *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_is_tord" thy [is_tord]
-"!!F. is_chain(F) ==> is_tord(range(F))"
+qed_goalw "chain_tord" thy [tord]
+"!!F. chain(F) ==> tord(range(F))"
(fn _ =>
[
Safe_tac,
@@ -138,13 +138,13 @@
(atac 1)
]);
-qed_goalw "is_chainE" thy [is_chain] "is_chain F ==> !i. F(i) << F(Suc(i))"
+qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)]);
-qed_goalw "is_chainI" thy [is_chain] "!i. F i << F(Suc i) ==> is_chain F"
+qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -185,7 +185,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "lub_finch1" thy [max_in_chain_def]
- "[| is_chain C; max_in_chain i C|] ==> range C <<| C i"
+ "[| chain C; max_in_chain i C|] ==> range C <<| C i"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -218,11 +218,11 @@
]);
-qed_goal "bin_chain" thy "x<<y ==> is_chain (%i. if i=0 then x else y)"
+qed_goal "bin_chain" thy "x<<y ==> chain (%i. if i=0 then x else y)"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac is_chainI 1),
+ (rtac chainI 1),
(rtac allI 1),
(nat_ind_tac "i" 1),
(Asm_simp_tac 1),
--- a/src/HOLCF/Porder.thy Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Porder.thy Tue Mar 10 18:33:13 1998 +0100
@@ -13,8 +13,8 @@
"<|" :: "['a set,'a::po] => bool" (infixl 55)
"<<|" :: "['a set,'a::po] => bool" (infixl 55)
lub :: "'a set => 'a::po"
- is_tord :: "'a::po set => bool"
- is_chain :: "(nat=>'a::po) => bool"
+ tord :: "'a::po set => bool"
+ chain :: "(nat=>'a::po) => bool"
max_in_chain :: "[nat,nat=>'a::po]=>bool"
finite_chain :: "(nat=>'a::po)=>bool"
@@ -37,14 +37,14 @@
is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)"
(* Arbitrary chains are total orders *)
-is_tord "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
+tord "tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
(* Here we use countable chains and I prefer to code them as functions! *)
-is_chain "is_chain F == (! i. F(i) << F(Suc(i)))"
+chain "chain F == (! i. F(i) << F(Suc(i)))"
(* finite chains, needed for monotony of continouous functions *)
max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)"
-finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
+finite_chain_def "finite_chain C == chain(C) & (? i. max_in_chain i C)"
lub_def "lub S == (@x. S <<| x)"
--- a/src/HOLCF/Sprod2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Sprod2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -95,7 +95,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_sprod" Sprod2.thy
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
(fn prems =>
[
@@ -123,7 +123,7 @@
qed_goal "cpo_sprod" Sprod2.thy
- "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
+ "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Sprod3.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Sprod3.ML Tue Mar 10 18:33:13 1998 +0100
@@ -19,7 +19,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "sprod3_lemma1" thy
-"[| is_chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\
+"[| chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
\ (lub(range(%i. Issnd(Ispair(Y i) x))))"
@@ -56,7 +56,7 @@
]);
qed_goal "sprod3_lemma2" thy
-"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
+"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
\ (lub(range(%i. Issnd(Ispair(Y i) x))))"
@@ -78,7 +78,7 @@
qed_goal "sprod3_lemma3" thy
-"[| is_chain(Y); x = UU |] ==>\
+"[| chain(Y); x = UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
\ (lub(range(%i. Issnd(Ispair (Y i) x))))"
@@ -124,7 +124,7 @@
]);
qed_goal "sprod3_lemma4" thy
-"[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
+"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
\ (lub(range(%i. Issnd (Ispair x (Y i)))))"
@@ -160,7 +160,7 @@
]);
qed_goal "sprod3_lemma5" thy
-"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
+"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
\ (lub(range(%i. Issnd(Ispair x (Y i)))))"
@@ -181,7 +181,7 @@
]);
qed_goal "sprod3_lemma6" thy
-"[| is_chain(Y); x = UU |] ==>\
+"[| chain(Y); x = UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
\ (lub(range(%i. Issnd (Ispair x (Y i)))))"
@@ -563,7 +563,7 @@
qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
-"[|is_chain(S)|] ==> range(S) <<| \
+"[|chain(S)|] ==> range(S) <<| \
\ (| lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) |)"
(fn prems =>
[
@@ -580,7 +580,7 @@
bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
(*
- "is_chain ?S1 ==>
+ "chain ?S1 ==>
lub (range ?S1) =
(|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm
*)
--- a/src/HOLCF/Ssum2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Ssum2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -198,7 +198,7 @@
qed_goal "ssum_lemma3" thy
-"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
+"[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
\ (!i.? y. Y(i)=Isinr(y))"
(fn prems =>
[
@@ -231,7 +231,7 @@
]);
qed_goal "ssum_lemma4" thy
-"is_chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
+"chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -317,7 +317,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_ssum1a" thy
-"[|is_chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
+"[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
\ range(Y) <<|\
\ Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
(fn prems =>
@@ -358,7 +358,7 @@
qed_goal "lub_ssum1b" thy
-"[|is_chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
+"[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
\ range(Y) <<|\
\ Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
(fn prems =>
@@ -400,20 +400,20 @@
bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI);
(*
-[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
+[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
lub (range ?Y1) = Isinl
(lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
*)
bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI);
(*
-[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
+[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
lub (range ?Y1) = Isinr
(lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
*)
qed_goal "cpo_ssum" thy
- "is_chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
+ "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Ssum3.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Ssum3.ML Tue Mar 10 18:33:13 1998 +0100
@@ -156,7 +156,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "ssum_lemma9" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
+"[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -174,7 +174,7 @@
qed_goal "ssum_lemma10" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
+"[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -193,7 +193,7 @@
]);
qed_goal "ssum_lemma11" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
(fn prems =>
[
@@ -210,7 +210,7 @@
]);
qed_goal "ssum_lemma12" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
(fn prems =>
[
@@ -269,7 +269,7 @@
qed_goal "ssum_lemma13" Ssum3.thy
-"[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
+"[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
(fn prems =>
[
@@ -579,7 +579,7 @@
]);
qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def]
- "is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
+ "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -589,7 +589,7 @@
qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def]
-"[| is_chain(Y); !i.? x. Y(i) = sinl`x |] ==>\
+"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\
\ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))"
(fn prems =>
[
@@ -614,7 +614,7 @@
]);
qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def]
-"[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\
+"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\
\ lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
(fn prems =>
[
@@ -641,7 +641,7 @@
]);
qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def]
- "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
+ "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -655,7 +655,7 @@
]);
qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def]
- "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
+ "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -669,7 +669,7 @@
]);
qed_goal "thelub_ssum3" Ssum3.thy
-"is_chain(Y) ==>\
+"chain(Y) ==>\
\ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
(fn prems =>
--- a/src/HOLCF/Up2.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Up2.ML Tue Mar 10 18:33:13 1998 +0100
@@ -111,7 +111,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "lub_up1a" thy
-"[|is_chain(Y);? i x. Y(i)=Iup(x)|] ==>\
+"[|chain(Y);? i x. Y(i)=Iup(x)|] ==>\
\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
(fn prems =>
[
@@ -148,7 +148,7 @@
]);
qed_goal "lub_up1b" thy
-"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
+"[|chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
\ range(Y) <<| Abs_Up (Inl ())"
(fn prems =>
[
@@ -172,18 +172,18 @@
bind_thm ("thelub_up1a", lub_up1a RS thelubI);
(*
-[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
+[| chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
*)
bind_thm ("thelub_up1b", lub_up1b RS thelubI);
(*
-[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
+[| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
lub (range ?Y1) = UU_up
*)
qed_goal "cpo_up" thy
- "is_chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
+ "chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Up3.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Up3.ML Tue Mar 10 18:33:13 1998 +0100
@@ -230,7 +230,7 @@
]);
qed_goalw "thelub_up2a" thy [up_def,fup_def]
-"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\
+"[| chain(Y); ? i x. Y(i) = up`x |] ==>\
\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
(fn prems =>
[
@@ -255,7 +255,7 @@
qed_goalw "thelub_up2b" thy [up_def,fup_def]
-"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
+"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -289,7 +289,7 @@
qed_goal "thelub_up2a_rev" thy
-"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
+"[| chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -303,7 +303,7 @@
]);
qed_goal "thelub_up2b_rev" thy
-"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"
+"[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -316,7 +316,7 @@
qed_goal "thelub_up3" thy
-"is_chain(Y) ==> lub(range(Y)) = UU |\
+"chain(Y) ==> lub(range(Y)) = UU |\
\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
(fn prems =>
[
--- a/src/HOLCF/adm.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/adm.ML Tue Mar 10 18:33:13 1998 +0100
@@ -10,7 +10,7 @@
[| cont t; adm P |] ==> adm (%x. P (t x))
"t" is instantiated with a term of chain-finite type, so that
-adm_chain_finite can be applied:
+adm_chfin can be applied:
adm (P::'a::{chfin,pcpo} => bool)
@@ -177,7 +177,7 @@
compose_tac (false, rule, 2) i THEN
rtac cont_thm i THEN
REPEAT (assume_tac i) THEN
- rtac adm_chain_finite i
+ rtac adm_chfin i
end
| [] => no_tac)
end)
--- a/src/HOLCF/domain/theorems.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/domain/theorems.ML Tue Mar 10 18:33:13 1998 +0100
@@ -41,7 +41,7 @@
asm_simp_tac (HOLCF_ss addsimps rews) i;
val chain_tac = REPEAT_DETERM o resolve_tac
- [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
+ [chain_iterate, ch2ch_fappR, ch2ch_fappL];
(* ----- general proofs ----------------------------------------------------- *)
--- a/src/HOLCF/ex/Stream.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/ex/Stream.ML Tue Mar 10 18:33:13 1998 +0100
@@ -136,12 +136,12 @@
(stac fix_def2 1),
(rewrite_goals_tac [stream.take_def]),
(stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
+ (rtac chain_iterate 1),
(rtac refl 1)
]);
-qed_goal "chain_stream_take" thy "is_chain (%i. stream_take i`s)" (fn _ => [
- rtac is_chainI 1,
+qed_goal "chain_stream_take" thy "chain (%i. stream_take i`s)" (fn _ => [
+ rtac chainI 1,
subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
fast_tac HOL_cs 1,
rtac allI 1,
@@ -160,10 +160,10 @@
rtac monofun_cfun_fun 1,
stac fix_def2 1,
rtac is_ub_thelub 1,
- rtac is_chain_iterate 1,
+ rtac chain_iterate 1,
etac subst 1, (* 2*back(); *)
rtac monofun_cfun_fun 1,
- rtac (rewrite_rule [is_chain] is_chain_iterate RS spec) 1]);
+ rtac (rewrite_rule [chain] chain_iterate RS spec) 1]);
(*
val stream_take_lemma2 = prove_goal thy
--- a/src/HOLCF/ex/loeckx.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/ex/loeckx.ML Tue Mar 10 18:33:13 1998 +0100
@@ -8,13 +8,13 @@
by (rtac ch2ch_fun 1);
back();
by (rtac refl 2);
-by (rtac is_chainI 1);
+by (rtac 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);
+by (rtac (chain_iterate RS chainE RS spec) 1);
val loeckx_sieber = result();
(*
@@ -27,7 +27,7 @@
Since we already proved the theorem
val cont_lubcfun = prove_goal Cfun2.thy
- "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
+ "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
it suffices to prove:
@@ -64,7 +64,7 @@
by (rtac cont_iterate 1);
by (rtac refl 1);
by (rtac cont_lubcfun 1);
-by (rtac is_chainI 1);
+by (rtac chainI 1);
by (strip_tac 1);
by (rtac less_cfun2 1);
by (stac beta_cfun 1);
@@ -73,7 +73,7 @@
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);
+by (rtac (chain_iterate RS chainE RS spec) 1);
val cont_Ifix2 = result();
(* the proof in little steps *)
@@ -97,14 +97,14 @@
(*
- cont_lubcfun;
-val it = "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm
+val it = "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 (rtac chainI 1);
by (strip_tac 1);
by (rtac less_cfun2 1);
by (stac beta_cfun 1);
@@ -113,6 +113,6 @@
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);
+by (rtac (chain_iterate RS chainE RS spec) 1);
val cont_Ifix2 = result();