# HG changeset patch
# User slotosch
# Date 864572380 -7200
# Node ID 930c9bed5a091d82de2c707fee09a51918fae54b
# Parent  4e4ee8a101be9503cc163711f062f9901d7599a8
Moved the classes flat chfin from Fix to Pcpo.
Corresponding theorems from Fix into Pcpo,Cont,Cfun3

diff -r 4e4ee8a101be -r 930c9bed5a09 src/HOLCF/Cfun3.ML
--- 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)
+]);
+
diff -r 4e4ee8a101be -r 930c9bed5a09 src/HOLCF/Cont.ML
--- 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)" *)
diff -r 4e4ee8a101be -r 930c9bed5a09 src/HOLCF/Fix.ML
--- 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                        *)
 (* ------------------------------------------------------------------------ *)
 
diff -r 4e4ee8a101be -r 930c9bed5a09 src/HOLCF/Fix.thy
--- 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
 
diff -r 4e4ee8a101be -r 930c9bed5a09 src/HOLCF/Pcpo.ML
--- 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]);
diff -r 4e4ee8a101be -r 930c9bed5a09 src/HOLCF/Pcpo.thy
--- 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