Moved the classes flat chfin from Fix to Pcpo.
Corresponding theorems from Fix into Pcpo,Cont,Cfun3
--- a/src/HOLCF/Cfun3.ML Sun May 25 16:57:19 1997 +0200
+++ b/src/HOLCF/Cfun3.ML Sun May 25 16:59:40 1997 +0200
@@ -371,3 +371,152 @@
(* HINT: cont_tac is now installed in simplifier in Lift3.ML ! *)
(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
+
+(* ------------------------------------------------------------------------ *)
+(* some lemmata for functions with flat/chain_finite 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"
+(fn prems =>
+ [
+ cut_facts_tac prems 1,
+ rtac allI 1,
+ rtac (contlub_cfun_fun RS ssubst) 1,
+ atac 1,
+ fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* continuous isomorphisms are strict *)
+(* a prove for embedding projection pairs is similar *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "iso_strict" thy
+"!!f g.[|!y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
+\ ==> f`UU=UU & g`UU=UU"
+ (fn prems =>
+ [
+ (rtac conjI 1),
+ (rtac UU_I 1),
+ (res_inst_tac [("s","f`(g`(UU::'b))"),("t","UU::'b")] subst 1),
+ (etac spec 1),
+ (rtac (minimal RS monofun_cfun_arg) 1),
+ (rtac UU_I 1),
+ (res_inst_tac [("s","g`(f`(UU::'a))"),("t","UU::'a")] subst 1),
+ (etac spec 1),
+ (rtac (minimal RS monofun_cfun_arg) 1)
+ ]);
+
+
+qed_goal "isorep_defined" thy
+ "[|!x.rep`(abs`x)=x;!y.abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac swap 1),
+ (dtac notnotD 1),
+ (dres_inst_tac [("f","abs")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (fast_tac HOL_cs 1),
+ (etac (iso_strict RS conjunct1) 1),
+ (atac 1)
+ ]);
+
+qed_goal "isoabs_defined" thy
+ "[|!x.rep`(abs`x) = x;!y.abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac swap 1),
+ (dtac notnotD 1),
+ (dres_inst_tac [("f","rep")] cfun_arg_cong 1),
+ (etac box_equals 1),
+ (fast_tac HOL_cs 1),
+ (etac (iso_strict RS conjunct2) 1),
+ (atac 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* 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); \
+\ !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)"
+ (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),
+ (etac spec 1),
+ (etac ch2ch_fappR 1),
+ (rtac exI 1),
+ (strip_tac 1),
+ (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1),
+ (etac spec 1),
+ (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1),
+ (etac spec 1),
+ (rtac cfun_arg_cong 1),
+ (rtac mp 1),
+ (etac spec 1),
+ (atac 1)
+ ]);
+
+
+qed_goal "flat2flat" thy "!!f g.[|!x y::'a.x<<y --> x=UU | x=y; \
+\ !y.f`(g`y)=(y::'b); !x.g`(f`x)=(x::'a)|] ==> !x y::'b.x<<y --> x=UU | x=y"
+ (fn prems =>
+ [
+ (strip_tac 1),
+ (rtac disjE 1),
+ (res_inst_tac [("P","g`x<<g`y")] mp 1),
+ (etac monofun_cfun_arg 2),
+ (dtac spec 1),
+ (etac spec 1),
+ (rtac disjI1 1),
+ (rtac trans 1),
+ (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
+ (etac spec 1),
+ (etac cfun_arg_cong 1),
+ (rtac (iso_strict RS conjunct1) 1),
+ (atac 1),
+ (atac 1),
+ (rtac disjI2 1),
+ (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
+ (etac spec 1),
+ (res_inst_tac [("s","f`(g`y)"),("t","y")] subst 1),
+ (etac spec 1),
+ (etac cfun_arg_cong 1)
+ ]);
+
+(* ------------------------------------------------------------------------- *)
+(* a result about functions with flat codomain *)
+(* ------------------------------------------------------------------------- *)
+
+qed_goal "flat_codom" thy
+"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (case_tac "f`(x::'a)=(UU::'b)" 1),
+ (rtac disjI1 1),
+ (rtac UU_I 1),
+ (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1),
+ (atac 1),
+ (rtac (minimal RS monofun_cfun_arg) 1),
+ (case_tac "f`(UU::'a)=(UU::'b)" 1),
+ (etac disjI1 1),
+ (rtac disjI2 1),
+ (rtac allI 1),
+ (hyp_subst_tac 1),
+ (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
+ (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS
+ (ax_flat RS spec RS spec RS mp) RS disjE) 1),
+ (contr_tac 1),(atac 1),
+ (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS
+ (ax_flat RS spec RS spec RS mp) RS disjE) 1),
+ (contr_tac 1),(atac 1)
+]);
+
--- a/src/HOLCF/Cont.ML Sun May 25 16:57:19 1997 +0200
+++ b/src/HOLCF/Cont.ML Sun May 25 16:59:40 1997 +0200
@@ -654,3 +654,43 @@
(rtac CollectI 1),
(rtac cont_const 1)
]);
+
+(* ------------------------------------------------------------------------ *)
+(* some properties of flat *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goalw "flatdom2monofun" thy [monofun]
+ "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)"
+(fn prems =>
+ [
+ cut_facts_tac prems 1,
+ strip_tac 1,
+ dtac (ax_flat RS spec RS spec RS mp) 1,
+ fast_tac ((HOL_cs addss (!simpset addsimps [minimal]))) 1
+ ]);
+
+
+qed_goal "chfindom_monofun2cont" thy "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
+(fn prems =>
+ [
+ cut_facts_tac prems 1,
+ rtac monocontlub2cont 1,
+ atac 1,
+ rtac contlubI 1,
+ strip_tac 1,
+ forward_tac [chfin2finch] 1,
+ rtac antisym_less 1,
+ fast_tac ((HOL_cs addIs [is_ub_thelub,ch2ch_monofun])
+ addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1,
+ dtac (monofun_finch2finch COMP swap_prems_rl) 1,
+ atac 1,
+ asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1,
+ etac conjE 1, etac exE 1,
+ asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1,
+ etac (monofunE RS spec RS spec RS mp) 1,
+ etac is_ub_thelub 1
+ ]);
+
+
+bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
+(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)
--- a/src/HOLCF/Fix.ML Sun May 25 16:57:19 1997 +0200
+++ b/src/HOLCF/Fix.ML Sun May 25 16:59:40 1997 +0200
@@ -553,103 +553,9 @@
bind_thm ("adm_chain_finite" ,chfin RS adm_max_in_chain);
(* ------------------------------------------------------------------------ *)
-(* flat types are chain_finite *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
- "!Y::nat=>'a::flat.is_chain Y-->(? n.max_in_chain n Y)"
- (fn _ =>
- [
- (strip_tac 1),
- (case_tac "!i.Y(i)=UU" 1),
- (res_inst_tac [("x","0")] exI 1),
- (Asm_simp_tac 1),
- (Asm_full_simp_tac 1),
- (etac exE 1),
- (res_inst_tac [("x","i")] exI 1),
- (strip_tac 1),
- (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
- (etac (le_imp_less_or_eq RS disjE) 1),
- (safe_tac HOL_cs),
- (dtac (ax_flat RS spec RS spec RS mp) 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* flat subclass of chfin --> adm_flat not needed *)
-
-(* ------------------------------------------------------------------------ *)
-(* some properties of flat *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "flatdom2monofun" thy [monofun]
- "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)"
-(fn prems =>
- [
- cut_facts_tac prems 1,
- strip_tac 1,
- dtac (ax_flat RS spec RS spec RS mp) 1,
- fast_tac ((HOL_cs addss !simpset)) 1
- ]);
-
-qed_goal "flat_eq" thy "(a::'a::flat) ~= UU ==> a << b = (a = b)"
-(fn prems=>
- [
- cut_facts_tac prems 1,
- safe_tac (HOL_cs addSIs [refl_less]),
- dtac (ax_flat RS spec RS spec RS mp) 1,
- fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
(* some lemmata for functions with flat/chain_finite domain/range types *)
(* ------------------------------------------------------------------------ *)
-qed_goal "chfin2finch" thy
- "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
- (fn prems =>
- [
- cut_facts_tac prems 1,
- fast_tac (HOL_cs addss
- (!simpset addsimps [chfin,finite_chain_def])) 1
- ]);
-
-qed_goal "chfindom_monofun2cont" thy "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
-(fn prems =>
- [
- cut_facts_tac prems 1,
- rtac monocontlub2cont 1,
- atac 1,
- rtac contlubI 1,
- strip_tac 1,
- forward_tac [chfin2finch] 1,
- rtac antisym_less 1,
- fast_tac ((HOL_cs addIs [is_ub_thelub,ch2ch_monofun])
- addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1,
- dtac (monofun_finch2finch COMP swap_prems_rl) 1,
- atac 1,
- asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1,
- etac conjE 1, etac exE 1,
- asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1,
- etac (monofunE RS spec RS spec RS mp) 1,
- etac is_ub_thelub 1
- ]);
-
-
-bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
-(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)
-
-qed_goal "chfin_fappR" thy
- "is_chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s"
-(fn prems =>
- [
- cut_facts_tac prems 1,
- rtac allI 1,
- rtac (contlub_cfun_fun RS ssubst) 1,
- atac 1,
- fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
- ]);
-
qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
(fn _ => [
strip_tac 1,
@@ -660,36 +566,9 @@
(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
(* ------------------------------------------------------------------------ *)
-(* lemmata for improved admissibility introdution rule *)
+(* improved admisibility introduction *)
(* ------------------------------------------------------------------------ *)
-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)))\
-\ |] ==> P (lub (range Y))"
- (fn prems => [
- cut_facts_tac prems 1,
- case_tac "finite_chain Y" 1,
- eresolve_tac prems 2, atac 2, atac 2,
- rewtac finite_chain_def,
- safe_tac HOL_cs,
- 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|]\
-\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
- (fn prems => [
- cut_facts_tac prems 1,
- etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
- rewtac finite_chain_def,
- safe_tac HOL_cs,
- etac swap 1,
- rewtac max_in_chain_def,
- resolve_tac prems 1, atac 1, atac 1,
- fast_tac (HOL_cs addDs [le_imp_less_or_eq]
- addEs [chain_mono RS mp]) 1]);
-
qed_goalw "admI" thy [adm_def]
"(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
\ ==> P(lub (range Y))) ==> adm P"
@@ -700,139 +579,6 @@
(* ------------------------------------------------------------------------ *)
-(* continuous isomorphisms are strict *)
-(* a prove for embedding projection pairs is similar *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "iso_strict" thy
-"!!f g.[|!y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> f`UU=UU & g`UU=UU"
- (fn prems =>
- [
- (rtac conjI 1),
- (rtac UU_I 1),
- (res_inst_tac [("s","f`(g`(UU::'b))"),("t","UU::'b")] subst 1),
- (etac spec 1),
- (rtac (minimal RS monofun_cfun_arg) 1),
- (rtac UU_I 1),
- (res_inst_tac [("s","g`(f`(UU::'a))"),("t","UU::'a")] subst 1),
- (etac spec 1),
- (rtac (minimal RS monofun_cfun_arg) 1)
- ]);
-
-
-qed_goal "isorep_defined" thy
- "[|!x.rep`(abs`x)=x;!y.abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac swap 1),
- (dtac notnotD 1),
- (dres_inst_tac [("f","abs")] cfun_arg_cong 1),
- (etac box_equals 1),
- (fast_tac HOL_cs 1),
- (etac (iso_strict RS conjunct1) 1),
- (atac 1)
- ]);
-
-qed_goal "isoabs_defined" thy
- "[|!x.rep`(abs`x) = x;!y.abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac swap 1),
- (dtac notnotD 1),
- (dres_inst_tac [("f","rep")] cfun_arg_cong 1),
- (etac box_equals 1),
- (fast_tac HOL_cs 1),
- (etac (iso_strict RS conjunct2) 1),
- (atac 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* 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); \
-\ !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)"
- (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),
- (etac spec 1),
- (etac ch2ch_fappR 1),
- (rtac exI 1),
- (strip_tac 1),
- (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1),
- (etac spec 1),
- (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1),
- (etac spec 1),
- (rtac cfun_arg_cong 1),
- (rtac mp 1),
- (etac spec 1),
- (atac 1)
- ]);
-
-
-qed_goal "flat2flat" thy "!!f g.[|!x y::'a.x<<y --> x=UU | x=y; \
-\ !y.f`(g`y)=(y::'b); !x.g`(f`x)=(x::'a)|] ==> !x y::'b.x<<y --> x=UU | x=y"
- (fn prems =>
- [
- (strip_tac 1),
- (rtac disjE 1),
- (res_inst_tac [("P","g`x<<g`y")] mp 1),
- (etac monofun_cfun_arg 2),
- (dtac spec 1),
- (etac spec 1),
- (rtac disjI1 1),
- (rtac trans 1),
- (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
- (etac spec 1),
- (etac cfun_arg_cong 1),
- (rtac (iso_strict RS conjunct1) 1),
- (atac 1),
- (atac 1),
- (rtac disjI2 1),
- (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
- (etac spec 1),
- (res_inst_tac [("s","f`(g`y)"),("t","y")] subst 1),
- (etac spec 1),
- (etac cfun_arg_cong 1)
- ]);
-
-(* ------------------------------------------------------------------------- *)
-(* a result about functions with flat codomain *)
-(* ------------------------------------------------------------------------- *)
-
-qed_goal "flat_codom" thy
-"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (case_tac "f`(x::'a)=(UU::'b)" 1),
- (rtac disjI1 1),
- (rtac UU_I 1),
- (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1),
- (atac 1),
- (rtac (minimal RS monofun_cfun_arg) 1),
- (case_tac "f`(UU::'a)=(UU::'b)" 1),
- (etac disjI1 1),
- (rtac disjI2 1),
- (rtac allI 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
- (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS
- (ax_flat RS spec RS spec RS mp) RS disjE) 1),
- (contr_tac 1),(atac 1),
- (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS
- (ax_flat RS spec RS spec RS mp) RS disjE) 1),
- (contr_tac 1),(atac 1)
-]);
-
-(* ------------------------------------------------------------------------ *)
(* admissibility of special formulae and propagation *)
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Fix.thy Sun May 25 16:57:19 1997 +0200
+++ b/src/HOLCF/Fix.thy Sun May 25 16:59:40 1997 +0200
@@ -30,15 +30,5 @@
admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
P (lub(range (%i. iterate i F UU)))"
-(* further useful class for HOLCF *)
-
-axclass chfin<pcpo
-
-chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
-
-axclass flat<pcpo
-
-ax_flat "! x y.x << y --> (x = UU) | (x=y)"
-
end
--- a/src/HOLCF/Pcpo.ML Sun May 25 16:57:19 1997 +0200
+++ b/src/HOLCF/Pcpo.ML Sun May 25 16:59:40 1997 +0200
@@ -269,3 +269,81 @@
(etac (chain_mono RS mp) 1),
(atac 1)
]);
+
+(**************************************)
+(* some properties for chfin and flat *)
+(**************************************)
+
+(* ------------------------------------------------------------------------ *)
+(* flat types are chain_finite *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
+ "!Y::nat=>'a::flat.is_chain Y-->(? n.max_in_chain n Y)"
+ (fn _ =>
+ [
+ (strip_tac 1),
+ (case_tac "!i.Y(i)=UU" 1),
+ (res_inst_tac [("x","0")] exI 1),
+ (Asm_simp_tac 1),
+ (Asm_full_simp_tac 1),
+ (etac exE 1),
+ (res_inst_tac [("x","i")] exI 1),
+ (strip_tac 1),
+ (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
+ (etac (le_imp_less_or_eq RS disjE) 1),
+ (safe_tac HOL_cs),
+ (dtac (ax_flat RS spec RS spec RS mp) 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+(* flat subclass of chfin --> adm_flat not needed *)
+
+qed_goal "flat_eq" thy "(a::'a::flat) ~= UU ==> a << b = (a = b)"
+(fn prems=>
+ [
+ cut_facts_tac prems 1,
+ safe_tac (HOL_cs addSIs [refl_less]),
+ dtac (ax_flat RS spec RS spec RS mp) 1,
+ fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1
+ ]);
+
+qed_goal "chfin2finch" thy
+ "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
+ (fn prems =>
+ [
+ cut_facts_tac prems 1,
+ fast_tac (HOL_cs addss
+ (!simpset addsimps [chfin,finite_chain_def])) 1
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* lemmata for improved admissibility introdution rule *)
+(* ------------------------------------------------------------------------ *)
+
+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)))\
+\ |] ==> P (lub (range Y))"
+ (fn prems => [
+ cut_facts_tac prems 1,
+ case_tac "finite_chain Y" 1,
+ eresolve_tac prems 2, atac 2, atac 2,
+ rewtac finite_chain_def,
+ safe_tac HOL_cs,
+ 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|]\
+\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
+ (fn prems => [
+ cut_facts_tac prems 1,
+ etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
+ rewtac finite_chain_def,
+ safe_tac HOL_cs,
+ etac swap 1,
+ rewtac max_in_chain_def,
+ resolve_tac prems 1, atac 1, atac 1,
+ fast_tac (HOL_cs addDs [le_imp_less_or_eq]
+ addEs [chain_mono RS mp]) 1]);
--- a/src/HOLCF/Pcpo.thy Sun May 25 16:57:19 1997 +0200
+++ b/src/HOLCF/Pcpo.thy Sun May 25 16:59:40 1997 +0200
@@ -28,4 +28,14 @@
defs
UU_def "UU == @x.!y.x<<y"
+(* further useful classes for HOLCF domains *)
+
+axclass chfin<cpo
+
+chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
+
+axclass flat<pcpo
+
+ax_flat "! x y.x << y --> (x = UU) | (x=y)"
+
end