# HG changeset patch
# User slotosch
# Date 864569829 -7200
# Node ID 6b26b886ff693bd37ec4a375c73e9170ae5447cc
# Parent  194ae2e0c1938fc064d2e9ecf8800b880109605d
Eliminated the prediates flat,chfin
Changed theorems with flat(x::'a) to (x::'a::flat)
Since flat<chfin theorems adm_flat,adm_flatdom are eliminated.
Use adm_chain_finite and adm_chfindom instead!
Examples do not use flat_flat any more

diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Fix.ML	Sun May 25 16:17:09 1997 +0200
@@ -550,114 +550,71 @@
         (etac spec 1)
         ]);
 
-qed_goalw "adm_chain_finite"  thy  [chain_finite_def]
-        "chain_finite(x::'a) ==> adm(P::'a=>bool)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac adm_max_in_chain 1)
-        ]);
+bind_thm ("adm_chain_finite" ,chfin RS adm_max_in_chain);
 
 (* ------------------------------------------------------------------------ *)
 (* flat types are chain_finite                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_imp_chain_finite"  thy  [flat_def,chain_finite_def]
-        "flat(x::'a)==>chain_finite(x::'a)"
- (fn prems =>
+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 _ =>
         [
-        (rewtac max_in_chain_def),
-        (cut_facts_tac prems 1),
         (strip_tac 1),
         (case_tac "!i.Y(i)=UU" 1),
         (res_inst_tac [("x","0")] exI 1),
-        (strip_tac 1),
-        (rtac trans 1),
-        (etac spec 1),
-        (rtac sym 1),
-        (etac spec 1),
-        (rtac (chain_mono2 RS exE) 1),
-        (fast_tac HOL_cs 1),
-        (atac 1),
-        (res_inst_tac [("x","Suc(x)")] exI 1),
+	(Asm_simp_tac 1),
+ 	(Asm_full_simp_tac 1),
+ 	(etac exE 1),
+        (res_inst_tac [("x","i")] exI 1),
         (strip_tac 1),
-        (rtac disjE 1),
-        (atac 3),
-        (rtac mp 1),
-        (dtac spec 1),
-        (etac spec 1),
+        (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
         (etac (le_imp_less_or_eq RS disjE) 1),
-        (etac (chain_mono RS mp) 1),
-        (atac 1),
-        (hyp_subst_tac 1),
-        (rtac refl_less 1),
-        (res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1),
-        (atac 2),
-        (rtac mp 1),
-        (etac spec 1),
-        (Asm_simp_tac 1)
+	(safe_tac HOL_cs),
+	(dtac (ax_flat RS spec RS spec RS mp) 1),
+	(fast_tac HOL_cs 1)
         ]);
 
-
-bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
-(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
+(* flat subclass of chfin --> adm_flat not needed *)
 
 (* ------------------------------------------------------------------------ *)
 (* some properties of flat			 			    *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flatI" thy [flat_def] "!x y::'a.x<<y-->x=UU|x=y==>flat(x::'a)"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "flatE" thy [flat_def] "flat(x::'a)==>!x y::'a.x<<y-->x=UU|x=y"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "flat_flat" thy [flat_def] "flat(x::'a::flat)"
-(fn prems => [rtac ax_flat 1]);
-
-qed_goalw "flatdom2monofun" thy [flat_def] 
-  "[| flat(x::'a::pcpo); f UU = UU |] ==> monofun (f::'a=>'b::pcpo)" 
+qed_goalw "flatdom2monofun" thy [monofun]
+  "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" 
 (fn prems => 
 	[
 	cut_facts_tac prems 1,
-	fast_tac ((HOL_cs addss !simpset) addSIs [monofunI]) 1
+	strip_tac 1,
+	dtac (ax_flat RS spec RS spec RS mp) 1,
+	fast_tac ((HOL_cs addss !simpset)) 1
 	]);
 
-
-qed_goalw "flat_eq" thy [flat_def] 
-        "[| flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
-        (cut_facts_tac prems 1),
-        (fast_tac (HOL_cs addIs [refl_less]) 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_goalw "chfinI" thy [chain_finite_def] 
-  "!Y::nat=>'a.is_chain Y-->(? n.max_in_chain n Y)==>chain_finite(x::'a)"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "chfinE" Fix.thy [chain_finite_def] 
-  "chain_finite(x::'a)==>!Y::nat=>'a.is_chain Y-->(? n.max_in_chain n Y)"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "chfin_chfin" thy [chain_finite_def] "chain_finite(x::'a::chfin)"
-(fn prems => [rtac ax_chfin 1]);
-
 qed_goal "chfin2finch" thy 
-    "[| is_chain (Y::nat=>'a); chain_finite(x::'a) |] ==> finite_chain Y"
-(fn prems => 
+    "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
+	(fn prems => 
 	[
 	cut_facts_tac prems 1,
 	fast_tac (HOL_cs addss 
-		 (!simpset addsimps [chain_finite_def,finite_chain_def])) 1
+		 (!simpset addsimps [chfin,finite_chain_def])) 1
 	]);
 
-bind_thm("flat_subclass_chfin",flat_flat RS flat_imp_chain_finite RS chfinE);
-
-qed_goal "chfindom_monofun2cont" thy 
-  "[| chain_finite(x::'a::pcpo); monofun f |] ==> cont (f::'a=>'b::pcpo)"
+qed_goal "chfindom_monofun2cont" thy  "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
 (fn prems => 
 	[
 	cut_facts_tac prems 1,
@@ -665,55 +622,42 @@
 	 atac 1,
 	rtac contlubI 1,
 	strip_tac 1,
-	dtac (chfin2finch COMP swap_prems_rl) 1,
-	 atac 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,
-	fast_tac ((HOL_cs 
-	    addIs [is_ub_thelub,(monofunE RS spec RS spec RS mp)]) 
-	    addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 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_monofun2cont",flat_imp_chain_finite RS chfindom_monofun2cont);
-(* [| flat ?x; monofun ?f |] ==> cont ?f *)
 
-qed_goal "flatdom_strict2cont" thy 
-  "[| flat(x::'a::pcpo); f UU = UU |] ==> cont (f::'a=>'b::pcpo)" 
-(fn prems =>
-	[
-	cut_facts_tac prems 1,
-	fast_tac ((HOL_cs addSIs [flatdom2monofun,
-			flat_imp_chain_finite RS chfindom_monofun2cont])) 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); chain_finite(x::'b) |] ==> \
-\    !s. ? n. lub(range(Y))`s = Y n`s" 
+    "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,lub_finch2,chfin2finch,ch2ch_fappL])1
+	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
 	]);
 
-qed_goalw "adm_chfindom" thy [adm_def]
-    "chain_finite (x::'b) ==> adm (%(u::'a::cpo->'b). P(u`s))"
-    (fn prems => [
-	cut_facts_tac prems 1,
+qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
+    (fn _ => [
 	strip_tac 1,
 	dtac chfin_fappR 1,
-	 atac 1,
 	eres_inst_tac [("x","s")] allE 1,
-	fast_tac (HOL_cs addss !simpset) 1]);
+	fast_tac (HOL_cs addss (!simpset addsimps [chfin])) 1]);
 
-bind_thm("adm_flatdom",flat_imp_chain_finite RS adm_chfindom);
-(* flat ?x ==> adm (%u. ?P (u`?s)) *)
-
+(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
 
 (* ------------------------------------------------------------------------ *)
 (* lemmata for improved admissibility introdution rule                      *)
@@ -809,9 +753,9 @@
 (* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "chfin2chfin"  thy  [chain_finite_def]
-"!!f g.[|chain_finite(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> chain_finite(y::'b)"
+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),
@@ -832,9 +776,9 @@
         (atac 1)
         ]);
 
-qed_goalw "flat2flat"  thy  [flat_def]
-"!!f g.[|flat(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> flat(y::'b)"
+
+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),
@@ -863,8 +807,8 @@
 (* a result about functions with flat codomain                               *)
 (* ------------------------------------------------------------------------- *)
 
-qed_goalw "flat_codom" thy [flat_def]
-"[|flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+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),
@@ -878,23 +822,15 @@
         (etac disjI1 1),
         (rtac disjI2 1),
         (rtac allI 1),
-        (res_inst_tac [("s","f`x"),("t","c")] subst 1),
-        (atac 1),
+        (hyp_subst_tac 1),
         (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
-        (etac allE 1),(etac allE 1),
-        (dtac mp 1),
-        (res_inst_tac [("fo","f")] (minimal RS monofun_cfun_arg) 1),
-        (etac disjE 1),
-        (contr_tac 1),
-        (atac 1),
-        (etac allE 1),
-        (etac allE 1),
-        (dtac mp 1),
-        (res_inst_tac [("fo","f")] (minimal RS monofun_cfun_arg) 1),
-        (etac 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),
+        (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 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Fix.thy	Sun May 25 16:17:09 1997 +0200
@@ -17,8 +17,6 @@
 fix	:: "('a->'a)->'a"
 adm		:: "('a::cpo=>bool)=>bool"
 admw		:: "('a=>bool)=>bool"
-chain_finite	:: "'a::cpo=>bool"
-flat		:: "'a=>bool"
 
 defs
 
@@ -32,16 +30,11 @@
 admw_def      "admw P == !F. (!n.P (iterate n F UU)) -->
                             P (lub(range (%i. iterate i F UU)))" 
 
-chain_finite_def  "chain_finite (x::'a::cpo)==
-                   !Y. is_chain (Y::nat=>'a::cpo) --> (? n.max_in_chain n Y)"
-
-flat_def	  "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
-
 (* further useful class for HOLCF *)
 
 axclass chfin<pcpo
 
-ax_chfin 	"!Y.is_chain Y-->(? n.max_in_chain n Y)"
+chfin 	"!Y.is_chain Y-->(? n.max_in_chain n Y)"
 
 axclass flat<pcpo
 
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Sun May 25 16:17:09 1997 +0200
@@ -37,7 +37,7 @@
  by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
 by (Simp_tac 1);
 br fix_ind 1;
-  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
+  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,flat_lift])) 1);
  by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (safe_tac HOL_cs);
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/IsaMakefile	Sun May 25 16:17:09 1997 +0200
@@ -17,9 +17,9 @@
        Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
        One.thy Tr.thy\
        Discrete0.thy Discrete1.thy Discrete.thy\
-       Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
+       Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
 
-ONLYTHYS = Lift.thy
+ONLYTHYS = 
 
 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
         ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/Lift.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift.ML	Sun May 25 16:17:09 1997 +0200
@@ -0,0 +1,100 @@
+open Lift;
+
+(* ---------------------------------------------------------- *)
+    section"Continuity Proofs for flift1, flift2, if";
+(* need the instance into flat *)
+(* ---------------------------------------------------------- *)
+
+
+(* flift1 is continuous in its argument itself*)
+goal thy "cont (lift_case UU f)"; 
+br flatdom_strict2cont 1;
+by (Simp_tac 1);
+qed"cont_flift1_arg";
+
+(* flift1 is continuous in a variable that occurs only 
+   in the Def branch *)
+
+goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
+\          cont (%y. lift_case UU (f y))";
+br cont2cont_CF1L_rev 1;
+by (strip_tac 1);
+by (res_inst_tac [("x","y")] Lift_cases 1);
+by (Asm_simp_tac 1);
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed"cont_flift1_not_arg";
+
+(* flift1 is continuous in a variable that occurs either 
+   in the Def branch or in the argument *)
+
+goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
+\   cont (%y. lift_case UU (f y) (g y))";
+br cont2cont_app 1;
+back();
+by (safe_tac set_cs);
+br cont_flift1_not_arg 1;
+auto();
+br cont_flift1_arg 1;
+qed"cont_flift1_arg_and_not_arg";
+
+(* flift2 is continuous in its argument itself *)
+
+goal thy "cont (lift_case UU (%y. Def (f y)))";
+br flatdom_strict2cont 1;
+by (Simp_tac 1);
+qed"cont_flift2_arg";
+
+
+(* ---------------------------------------------------------- *)
+(*    Extension of cont_tac and installation of simplifier    *)
+(* ---------------------------------------------------------- *)
+
+bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
+
+val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
+                       cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, 
+                       cont_fapp_app,cont_fapp_app_app,cont_if];
+
+val cont_lemmas2 =  cont_lemmas1 @ cont_lemmas_ext;
+                 
+Addsimps cont_lemmas_ext;         
+
+fun cont_tac  i = resolve_tac cont_lemmas2 i;
+fun cont_tacR i = REPEAT (cont_tac i);
+
+fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
+                  REPEAT (cont_tac i);
+
+
+simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+
+(* ---------------------------------------------------------- *)
+              section"flift1, flift2";
+(* ---------------------------------------------------------- *)
+
+
+goal thy "flift1 f`(Def x) = (f x)";
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"flift1_Def";
+
+goal thy "flift2 f`(Def x) = Def (f x)";
+by (simp_tac (!simpset addsimps [flift2_def]) 1);
+qed"flift2_Def";
+
+goal thy "flift1 f`UU = UU";
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"flift1_UU";
+
+goal thy "flift2 f`UU = UU";
+by (simp_tac (!simpset addsimps [flift2_def]) 1);
+qed"flift2_UU";
+
+Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
+
+goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU";
+by (def_tac 1);
+qed"flift2_nUU";
+
+Addsimps [flift2_nUU];
+
+
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Lift3.ML	Sun May 25 16:17:09 1997 +0200
@@ -139,58 +139,9 @@
               section"Lift is flat";
 (* ---------------------------------------------------------- *)
 
-goalw thy [flat_def] "flat (x::'a lift)";
+goal thy "! x y::'a lift. x << y --> x = UU | x = y";
 by (simp_tac (!simpset addsimps [less_lift]) 1);
-qed"flat_lift";
-
-bind_thm("ax_flat_lift",flat_lift RS flatE);
-
-
-(* ---------------------------------------------------------- *)
-    section"Continuity Proofs for flift1, flift2, if";
-(* ---------------------------------------------------------- *)
-
-
-(* flift1 is continuous in its argument itself*)
-
-goal thy "cont (lift_case UU f)"; 
-br flatdom_strict2cont 1;
-br flat_lift 1;
-by (Simp_tac 1);
-qed"cont_flift1_arg";
-
-(* flift1 is continuous in a variable that occurs only 
-   in the Def branch *)
-
-goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
-\          cont (%y. lift_case UU (f y))";
-br cont2cont_CF1L_rev 1;
-by (strip_tac 1);
-by (res_inst_tac [("x","y")] Lift_cases 1);
-by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addss !simpset) 1);
-qed"cont_flift1_not_arg";
-
-(* flift1 is continuous in a variable that occurs either 
-   in the Def branch or in the argument *)
-
-goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
-\   cont (%y. lift_case UU (f y) (g y))";
-br cont2cont_app 1;
-back();
-by (safe_tac set_cs);
-br cont_flift1_not_arg 1;
-auto();
-br cont_flift1_arg 1;
-qed"cont_flift1_arg_and_not_arg";
-
-(* flift2 is continuous in its argument itself *)
-
-goal thy "cont (lift_case UU (%y. Def (f y)))";
-br flatdom_strict2cont 1;
-br flat_lift 1;
-by (Simp_tac 1);
-qed"cont_flift2_arg";
+qed"ax_flat_lift";
 
 (* Two specific lemmas for the combination of LCF and HOL terms *)
 
@@ -208,7 +159,6 @@
 
 
 (* continuity of if then else *)
-
 val prems = goal thy "[| cont f1; cont f2 |] ==> \
 \   cont (%x. if b then f1 x else f2 x)";
 by (cut_facts_tac prems 1);
@@ -216,57 +166,3 @@
 by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
 qed"cont_if";
 
-
-(* ---------------------------------------------------------- *)
-(*    Extension of cont_tac and installation of simplifier    *)
-(* ---------------------------------------------------------- *)
-
-bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
-
-val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
-                       cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, 
-                       cont_fapp_app,cont_fapp_app_app,cont_if];
-
-val cont_lemmas2 =  cont_lemmas1 @ cont_lemmas_ext;
-                 
-Addsimps cont_lemmas_ext;         
-
-fun cont_tac  i = resolve_tac cont_lemmas2 i;
-fun cont_tacR i = REPEAT (cont_tac i);
-
-fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
-                  REPEAT (cont_tac i);
-
-
-simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
-
-(* ---------------------------------------------------------- *)
-              section"flift1, flift2";
-(* ---------------------------------------------------------- *)
-
-
-goal thy "flift1 f`(Def x) = (f x)";
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
-qed"flift1_Def";
-
-goal thy "flift2 f`(Def x) = Def (f x)";
-by (simp_tac (!simpset addsimps [flift2_def]) 1);
-qed"flift2_Def";
-
-goal thy "flift1 f`UU = UU";
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
-qed"flift1_UU";
-
-goal thy "flift2 f`UU = UU";
-by (simp_tac (!simpset addsimps [flift2_def]) 1);
-qed"flift2_UU";
-
-Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
-
-goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU";
-by (def_tac 1);
-qed"flift2_nUU";
-
-Addsimps [flift2_nUU];
-
-
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Makefile	Sun May 25 16:17:09 1997 +0200
@@ -29,9 +29,9 @@
        Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
        Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
        One.thy Tr.thy \
-       Lift1.thy Lift2.thy Lift3.thy HOLCF.thy 
+       Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy 
 
-ONLYTHYS = Lift.thy
+ONLYTHYS = 
 
 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
         ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/ccc1.thy
--- a/src/HOLCF/ccc1.thy	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ccc1.thy	Sun May 25 16:17:09 1997 +0200
@@ -9,7 +9,7 @@
 
 ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix + 
 
-instance flat<chfin (flat_subclass_chfin)
+instance flat<chfin (flat_imp_chain_finite)
 
 consts
         ID      :: "('a::cpo) -> 'a"
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/ex/Dnat.ML
--- a/src/HOLCF/ex/Dnat.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Dnat.ML	Sun May 25 16:17:09 1997 +0200
@@ -47,7 +47,8 @@
 val iterator_rews = 
 	[iterator1, iterator2, iterator3];
 
-val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(x::dnat)" (fn _ => [
+val dnat_flat = prove_goal Dnat.thy "!x y::dnat.x<<y --> x=UU | x=y" 
+(fn _ => [
 	(rtac allI 1),
 	(res_inst_tac [("x","x")] dnat.ind 1),
 	(fast_tac HOL_cs 1),
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Sun May 25 16:17:09 1997 +0200
@@ -95,7 +95,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (etac (flat_flat RS flat_codom RS disjE) 1),
+        (etac (flat_codom RS disjE) 1),
         (atac 1),
         (etac spec 1)
         ]);
@@ -323,7 +323,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac (flat_flat RS flat_codom) 1),
+        (rtac (flat_codom) 1),
         (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
         (etac spec 1)
         ]);
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/ex/Loop.ML
--- a/src/HOLCF/ex/Loop.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Loop.ML	Sun May 25 16:17:09 1997 +0200
@@ -57,7 +57,7 @@
         (asm_simp_tac HOLCF_ss 1),
         (stac while_unfold 1),
         (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
-        (etac (flat_flat RS flat_codom RS disjE) 1),
+        (etac (flat_codom RS disjE) 1),
         (atac 1),
         (etac spec 1),
         (simp_tac HOLCF_ss 1),
@@ -92,7 +92,7 @@
         (rtac step_def2 1),
         (asm_simp_tac HOLCF_ss 1),
         (etac exE 1),
-        (etac (flat_flat RS flat_codom RS disjE) 1),
+        (etac (flat_codom RS disjE) 1),
         (asm_simp_tac HOLCF_ss 1),
         (asm_simp_tac HOLCF_ss 1)
         ]);
diff -r 194ae2e0c193 -r 6b26b886ff69 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Stream.ML	Sun May 25 16:17:09 1997 +0200
@@ -44,14 +44,15 @@
 	fast_tac (HOL_cs addDs stream.inverts) 1]);
 
 qed_goal "stream_flat_prefix" thy 
-"[| x && xs << y && ys; (x::'a) ~= UU; flat (z::'a) |] ==> x = y &  xs << ys"(fn prems=>[
+"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
+(fn prems=>[
 	cut_facts_tac prems 1,
+	(cut_facts_tac [read_instantiate[("x1","x::'a::flat"),("x","y::'a::flat")]
+		(ax_flat RS spec RS spec)] 1),
 	(forward_tac stream.inverts 1),
 	(safe_tac HOL_cs),
 	(dtac (hd stream.con_rews RS subst) 1),
-	(fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1),
-	(rewtac flat_def),
-	(fast_tac HOL_cs 1)]);
+	(fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1)]);
 
 qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \
 \(x = UU |  (? a y. x = a && y &  a ~= UU &  a << b &  y << z))" (fn prems => [