# HG changeset patch
# User nipkow
# Date 781465218 -3600
# Node ID 119391dd1d59a9b72c2ce216b6b11a8243d6f453
# Parent  33b9b5da3e6faee6ca6969d17e79634d49e5b46a
New version

diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cfun3.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -17,11 +17,11 @@
 	(strip_tac 1),
 	(rtac (expand_fun_eq RS iffD2) 1),
 	(strip_tac 1),
-	(rtac (lub_cfun RS thelubI RS ssubst) 1),
+	(rtac (thelub_cfun RS ssubst) 1),
 	(atac 1),
 	(rtac (Cfunapp2 RS ssubst) 1),
 	(etac contX_lubcfun 1),
-	(rtac (lub_fun RS thelubI RS ssubst) 1),
+	(rtac (thelub_fun RS ssubst) 1),
 	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
 	(rtac refl 1)
 	]);
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cont.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -312,15 +312,12 @@
 (* in both arguments                                                        *)
 (* ------------------------------------------------------------------------ *)
 
-val diag_lubCF2_1 = prove_goal Cont.thy 
+val diag_lemma1 = prove_goal Cont.thy 
 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
-\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
-\ lub(range(%i. CF2(FY(i))(TY(i))))"
-(fn prems =>
+\ is_chain(%i. lub(range(%j. CF2(FY(j), TY(i)))))"
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(rtac antisym_less 1),
-	(rtac is_lub_thelub 1),
 	(rtac ch2ch_lubMF2L 1),
 	(rtac contX2mono 1),
 	(atac 1),
@@ -328,109 +325,124 @@
 	(rtac contX2mono 1),
 	(etac spec 1),
 	(atac 1),
-	(atac 1),
-	(rtac ub_rangeI 1),
-	(strip_tac 1 ),
-	(rtac is_lub_thelub 1),
-	((rtac ch2ch_MF2L 1) THEN (rtac contX2mono 1) THEN (atac 1)),
-	(atac 1),
-	(rtac ub_rangeI 1),
-	(strip_tac 1 ),
-	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
-	(rtac trans_less 1),
-	(rtac is_ub_thelub 2),
-	(rtac (chain_mono RS mp) 1),
-	((rtac ch2ch_MF2R 1) THEN (rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
+	(atac 1)
+	]);
+
+val diag_lemma2 = prove_goal Cont.thy 
+"[|contX(CF2);is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(m), TY(n::nat)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac (contX2mono RS ch2ch_MF2L) 1),
+	(atac 1)
+	]);
+
+val diag_lemma3 = prove_goal Cont.thy 
+"[|!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(n), TY(m)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac allE 1),
+	(etac (contX2mono RS ch2ch_MF2R) 1),
+	(atac 1)
+	]);
+
+val diag_lemma4 = prove_goal Cont.thy 
+"[|contX(CF2);!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(m), TY(m)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac (contX2mono RS ch2ch_MF2LR) 1),
 	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(hyp_subst_tac 1),
-	(rtac is_ub_thelub 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
+	(etac allE 1),
+	(etac contX2mono 1),
 	(atac 1),
-	(rtac trans_less 1),
-	(rtac is_ub_thelub 2),
-	(res_inst_tac [("x1","ia")] (chain_mono RS mp) 1),
-	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
-	(atac 1),
-	(atac 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(rtac lub_mono 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(rtac ch2ch_lubMF2L 1),
-	(rtac contX2mono 1),
-	(atac 1),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(strip_tac 1 ),
-	(rtac is_ub_thelub 1),
-	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
 	(atac 1)
 	]);
 
 
+val diag_lubCF2_1 = prove_goal Cont.thy 
+"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
+\ lub(range(%i. CF2(FY(i))(TY(i))))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac antisym_less 1),
+	(rtac is_lub_thelub 1),
+	(etac diag_lemma1 1),
+	(REPEAT (atac 1)),
+	(rtac ub_rangeI 1),
+	(strip_tac 1 ),
+	(rtac lub_mono3 1),
+	(etac diag_lemma2 1),
+	(REPEAT (atac 1)),
+	(etac diag_lemma4 1),
+	(REPEAT (atac 1)),
+	(rtac allI 1),
+	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
+	(res_inst_tac [("x","ia")] exI 1),
+	(rtac (chain_mono RS mp) 1),
+	(etac diag_lemma3 1),
+	(REPEAT (atac 1)),
+	(hyp_subst_tac 1),
+	(res_inst_tac [("x","ia")] exI 1),
+	(rtac refl_less 1),
+	(res_inst_tac [("x","i")] exI 1),
+	(rtac (chain_mono RS mp) 1),
+	(etac diag_lemma2 1),
+	(REPEAT (atac 1)),
+	(rtac lub_mono 1),
+	(etac diag_lemma4 1),
+	(REPEAT (atac 1)),
+	(etac diag_lemma1 1),
+	(REPEAT (atac 1)),
+	(strip_tac 1 ),
+	(rtac is_ub_thelub 1),
+	(etac diag_lemma2 1),
+	(REPEAT (atac 1))
+	]);
+
 val diag_lubCF2_2 = prove_goal Cont.thy 
 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. CF2(FY(i))(TY(i))))"
-(fn prems =>
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac trans 1),
 	(rtac ex_lubMF2 1),
-	(rtac ((hd prems) RS contX2mono) 1), 
+	(etac contX2mono 1),
 	(rtac allI 1),
-	(rtac (((hd (tl prems)) RS spec RS contX2mono)) 1),
-	(atac 1),
-	(atac 1),
+	(etac allE 1),
+	(etac contX2mono 1),
+	(REPEAT (atac 1)),
 	(rtac diag_lubCF2_1 1),
-	(atac 1),
-	(atac 1),
-	(atac 1),
-	(atac 1)
+	(REPEAT (atac 1))
 	]);
 
-
 val contlub_CF2 = prove_goal Cont.thy 
 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
-(fn prems =>
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(rtac ((hd prems) RS contX2contlub RS contlubE RS 
-		spec RS mp RS ssubst) 1),
+	(rtac ((hd prems) RS contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
 	(atac 1),
 	(rtac (thelub_fun RS ssubst) 1),
-	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1), 
+	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac trans 1),
-	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS 
-	contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1),
+	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS contlubE RS 
+               spec RS mp RS ext RS arg_cong RS arg_cong) 1),
 	(atac 1),
 	(rtac diag_lubCF2_2 1),
-	(atac 1),
-	(atac 1),
-	(atac 1),
-	(atac 1)
+	(REPEAT (atac 1))
 	]);
-
+ 
 (* ------------------------------------------------------------------------ *)
 (* The following results are about application for functions in 'a=>'b      *)
 (* ------------------------------------------------------------------------ *)
@@ -574,24 +586,20 @@
 	(atac 1)
 	]);
 
+
 val contX2contlub_app = prove_goal Cont.thy 
-"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
-\	 contlub(%x.(ft(x))(tt(x)))"
+"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac contlubI 1),
 	(strip_tac 1),
 	(res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
-	(rtac contX2contlub 1),
-	(resolve_tac prems 1),
+	(etac contX2contlub 1),
 	(atac 1),
 	(rtac contlub_CF2 1),
-	(resolve_tac prems 1),
-	(resolve_tac prems 1),
-	(atac 1),
-	(rtac (contX2mono RS ch2ch_monofun) 1),
-	(resolve_tac prems 1),
+	(REPEAT (atac 1)),
+	(etac (contX2mono RS ch2ch_monofun) 1),
 	(atac 1)
 	]);
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Cprod3.thy
--- a/src/HOLCF/Cprod3.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cprod3.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -20,6 +20,8 @@
 	csnd         :: "('a*'b)->'b"
 	csplit       :: "('a->'b->'c)->('a*'b)->'c"
 
+translations "x#y" => "cpair[x][y]"
+
 rules 
 
 inst_cprod_pcpo	"(UU::'a*'b) = <UU,UU>"
@@ -31,13 +33,6 @@
 
 end
 
-ML
-
-(* ----------------------------------------------------------------------*)
-(* parse translations for the above mixfix                               *)
-(* ----------------------------------------------------------------------*)
-
-val parse_translation = [("@cpair",mk_cinfixtr "@cpair")];
 
 
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Dlist.thy
--- a/src/HOLCF/Dlist.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Dlist.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -4,7 +4,19 @@
     ID:         $ $
     Copyright   1994 Technische Universitaet Muenchen
 
-Theory for lists
+Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
+
+The type is axiomatized as the least solution of the domain equation above.
+The functor term that specifies the domain equation is: 
+
+  FT = <++,K_{one},<**,K_{'a},I>>
+
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+                     Dissertation, Technische Universit"at M"unchen, 1994
+
+
 *)
 
 Dlist = Stream2 +
@@ -47,8 +59,9 @@
 (* axiomatization of recursive type 'a dlist                               *)
 (* ----------------------------------------------------------------------- *)
 (* ('a dlist,dlist_abs) is the initial F-algebra where                     *)
-(* F is the locally continuous functor determined by domain equation       *)
-(* X = one ++ 'a ** X                                                      *)
+(* F is the locally continuous functor determined by functor term FT.      *)
+(* domain equation: 'a dlist = one ++ ('a ** 'a dlist)                     *)
+(* functor term:    FT = <++,K_{one},<**,K_{'a},I>>                        *)
 (* ----------------------------------------------------------------------- *)
 (* dlist_abs is an isomorphism with inverse dlist_rep                      *)
 (* identity is the least endomorphism on 'a dlist                          *)
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Dnat.ML
--- a/src/HOLCF/Dnat.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Dnat.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -12,7 +12,7 @@
 (* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
 (* ------------------------------------------------------------------------*)
 
-val dnat_iso_strict= dnat_rep_iso RS (dnat_abs_iso RS 
+val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS 
 	(allI  RSN (2,allI RS iso_strict)));
 
 val dnat_rews = [dnat_iso_strict RS conjunct1,
@@ -530,3 +530,5 @@
 
 
 
+
+
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Dnat.thy
--- a/src/HOLCF/Dnat.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Dnat.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -3,7 +3,17 @@
     Author: 	Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Theory for the domain of natural numbers
+Theory for the domain of natural numbers  dnat = one ++ dnat
+
+The type is axiomatized as the least solution of the domain equation above.
+The functor term that specifies the domain equation is: 
+
+  FT = <++,K_{one},I>
+
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+                     Dissertation, Technische Universit"at M"unchen, 1994
 
 *)
 
@@ -44,8 +54,9 @@
 (* axiomatization of recursive type dnat                                   *)
 (* ----------------------------------------------------------------------- *)
 (* (dnat,dnat_abs) is the initial F-algebra where                          *)
-(* F is the locally continuous functor determined by domain equation       *)
-(* X = one ++ X                                                            *)
+(* F is the locally continuous functor determined by functor term FT.      *)
+(* domain equation: dnat = one ++ dnat                                     *)
+(* functor term:    FT = <++,K_{one},I>                                    *) 
 (* ----------------------------------------------------------------------- *)
 (* dnat_abs is an isomorphism with inverse dnat_rep                        *)
 (* identity is the least endomorphism on dnat                              *)
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Fix.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -688,6 +688,43 @@
 	(etac cfun_arg_cong 1)
 	]);
 
+(* ------------------------------------------------------------------------- *)
+(* a result about functions with flat codomain                               *)
+(* ------------------------------------------------------------------------- *)
+
+val flat_codom = prove_goalw Fix.thy [flat_def]
+"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 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),
+	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
+	(etac disjI1 1),
+	(rtac disjI2 1),
+	(rtac allI 1),
+	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
+	(atac 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 [("fo5","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 [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(atac 1)
+	]);
+
 (* ------------------------------------------------------------------------ *)
 (* admissibility of special formulae and propagation                        *)
 (* ------------------------------------------------------------------------ *)
@@ -777,6 +814,8 @@
 	(etac spec 1)
 	]);
 
+val adm_all2 = (allI RS adm_all);
+
 val adm_subst = prove_goal  Fix.thy  
 	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
  (fn prems =>
@@ -1127,45 +1166,8 @@
 	]);
 
 
-val adm_all2 = (allI RS adm_all);
 
 val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
 	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
 	];
 
-(* ------------------------------------------------------------------------- *)
-(* a result about functions with flat codomain                               *)
-(* ------------------------------------------------------------------------- *)
-
-val flat_codom = prove_goalw Fix.thy [flat_def]
-"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 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),
-	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
-	(etac disjI1 1),
-	(rtac disjI2 1),
-	(rtac allI 1),
-	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
-	(atac 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 [("fo5","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 [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
-	(etac disjE 1),
-	(contr_tac 1),
-	(atac 1)
-	]);
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Holcfb.ML
--- a/src/HOLCF/Holcfb.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Holcfb.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -9,10 +9,10 @@
 open Holcfb;
 
 (* ------------------------------------------------------------------------ *)
-(* <::nat=>nat=>bool is well-founded                                        *)
+(* <::nat=>nat=>bool is a well-ordering                                     *)
 (* ------------------------------------------------------------------------ *)
 
-val well_founded_nat = prove_goal  Nat.thy 
+val well_ordering_nat = prove_goal  Nat.thy 
 	"!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
  (fn prems =>
 	[
@@ -45,7 +45,7 @@
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(rtac (well_founded_nat RS spec RS mp RS exE) 1),
+	(rtac (well_ordering_nat RS spec RS mp RS exE) 1),
 	(atac 1),
 	(rtac selectI 1),
 	(atac 1)
@@ -150,3 +150,21 @@
 val classical3 = (notE RS notI);
 (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
 
+
+val nat_less_cases = prove_goal Nat.thy 
+    "[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
+( fn prems =>
+	[
+	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
+	(etac disjE 2),
+	(etac (hd (tl (tl prems))) 1),
+	(etac (sym RS hd (tl prems)) 1),
+	(etac (hd prems) 1)
+	]);
+
+
+
+
+
+
+
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/One.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -68,15 +68,17 @@
 (* one is flat                                                              *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw One.thy [flat_def] "flat(one)";
-by (rtac allI 1);
-by (rtac allI 1);
-by (res_inst_tac [("p","x")] oneE 1);
-by (asm_simp_tac ccc1_ss  1);
-by (res_inst_tac [("p","y")] oneE 1);
-by (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1);
-by (asm_simp_tac ccc1_ss  1);
-val flat_one = result();
+val flat_one = prove_goalw One.thy [flat_def] "flat(one)"
+ (fn prems =>
+	[
+	(rtac allI 1),
+	(rtac allI 1),
+	(res_inst_tac [("p","x")] oneE 1),
+	(asm_simp_tac ccc1_ss  1),
+	(res_inst_tac [("p","y")] oneE 1),
+	(asm_simp_tac (ccc1_ss addsimps dist_less_one) 1),
+	(asm_simp_tac ccc1_ss  1)
+	]);
 
 
 (* ------------------------------------------------------------------------ *)
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/One.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -3,27 +3,17 @@
     Author: 	Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Introduve atomic type one = (void)u
+Introduce atomic type one = (void)u
 
-This is the first type that is introduced using a domain isomorphism.
-The type axiom 
-
-	arities one :: pcpo
+The type is axiomatized as the least solution of a domain equation.
+The functor term that specifies the domain equation is: 
 
-and the continuity of the Isomorphisms are taken for granted. Since the
-type is not recursive, it could be easily introduced in a purely conservative
-style as it was used for the types sprod, ssum, lift. The definition of the 
-ordering is canonical using abstraction and representation, but this would take
-again a lot of internal constants. It can easily be seen that the axioms below
-are consistent.
+  FT = <U,K_{void}>
 
-The partial ordering on type one is implicitly defined via the
-isomorphism axioms and the continuity of abs_one and rep_one.
+For details see chapter 5 of:
 
-We could also introduce the function less_one with definition
-
-less_one(x,y) = rep_one[x] << rep_one[y]
-
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+                     Dissertation, Technische Universit"at M"unchen, 1994
 
 *)
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -1,38 +1,14 @@
-(*  Title: 	HOLCF/pcpo.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Definition of class pcpo (pointed complete partial order)
-
-The prototype theory for this class is porder.thy 
-
-*)
-
 Pcpo = Porder +
 
-(* Introduction of new class. The witness is type void. *)
-
 classes pcpo < po
-
-(* default class is still term *)
-(* void is the prototype in pcpo *)
-
 arities void :: pcpo
 
 consts	
-	UU	::	"'a::pcpo"		(* UU is the least element *)
+	UU :: "'a::pcpo"	
 rules
 
-(* class axioms: justification is theory Porder *)
-
-minimal		"UU << x"			(* witness is minimal_void *)
-
-cpo		"is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))" 
-						(* witness is cpo_void     *)
-						(* needs explicit type     *)
-
-(* instance of UU for the prototype void *)
+minimal	"UU << x"	
+cpo	"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
 
 inst_void_pcpo	"(UU::void) = UU_void"
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Porder.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -9,6 +9,21 @@
 open Porder0;
 open Porder;
 
+
+(* ------------------------------------------------------------------------ *)
+(* the reverse law of anti--symmetrie of <<                                 *)
+(* ------------------------------------------------------------------------ *)
+
+val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
+(fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac conjI 1),
+	((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
+	((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
+	]);
+
+
 val box_less = prove_goal Porder.thy 
 "[| a << b; c << a; b << d|] ==> c << d"
  (fn prems =>
@@ -72,20 +87,6 @@
 	(rtac refl_less 1)
 	]);
 
-(* ------------------------------------------------------------------------ *)
-(* Lemma for reasoning by cases on the natural numbers                      *)
-(* ------------------------------------------------------------------------ *)
-
-val nat_less_cases = prove_goal Porder.thy 
-	"[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
-( fn prems =>
-	[
-	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
-	(etac disjE 2),
-	(etac (hd (tl (tl prems))) 1),
-	(etac (sym RS hd (tl prems)) 1),
-	(etac (hd prems) 1)
-	]);
 
 (* ------------------------------------------------------------------------ *)
 (* The range of a chain is a totaly ordered     <<                           *)
@@ -123,7 +124,7 @@
 
 
 (* ------------------------------------------------------------------------ *)
-(* technical lemmas about lub and is_lub, use above results about @         *)
+(* technical lemmas about lub and is_lub                                    *)
 (* ------------------------------------------------------------------------ *)
 
 val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
@@ -303,19 +304,6 @@
 
 
 (* ------------------------------------------------------------------------ *)
-(* the reverse law of anti--symmetrie of <<                                 *)
-(* ------------------------------------------------------------------------ *)
-
-val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac conjI 1),
-	((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
-	((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
-	]);
-
-(* ------------------------------------------------------------------------ *)
 (* results about finite chains                                              *)
 (* ------------------------------------------------------------------------ *)
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/ROOT.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -55,7 +55,7 @@
 use_thy "One";
 use_thy "Tr1";
 use_thy "Tr2";
-
+ 
 use_thy "HOLCF";
 
 use_thy "Dnat";
@@ -64,7 +64,6 @@
 use_thy "Stream2";
 use_thy "Dlist";
 
-
 use "../Pure/install_pp.ML";
 print_depth 8;  
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Sprod3.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -18,6 +18,8 @@
 	ssnd         :: "('a**'b)->'b"
 	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
 
+translations "x##y" => "spair[x][y]"
+
 rules 
 
 inst_sprod_pcpo	"(UU::'a**'b) = Ispair(UU,UU)"
@@ -28,12 +30,5 @@
 
 end
 
-ML
-
-(* ----------------------------------------------------------------------*)
-(* parse translations for the above mixfix                               *)
-(* ----------------------------------------------------------------------*)
-
-val parse_translation = [("@spair",mk_cinfixtr "@spair")];
 
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Stream.ML
--- a/src/HOLCF/Stream.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Stream.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -419,6 +419,30 @@
 	(REPEAT (atac 1))
 	]);
 
+(* prove induction using definition of admissibility 
+   stream_reach rsp. stream_reach2 
+   and finite induction stream_finite_ind *)
+
+val stream_ind = prove_goal Stream.thy
+"[|adm(P);\
+\  P(UU);\
+\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
+\  |] ==> P(s)"
+ (fn prems =>
+	[
+	(rtac (stream_reach2 RS subst) 1),
+	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
+	(resolve_tac prems 1),
+	(SELECT_GOAL (rewrite_goals_tac [stream_take_def]) 1),
+	(rtac ch2ch_fappL 1),
+	(rtac is_chain_iterate 1),
+	(rtac allI 1),
+	(rtac (stream_finite_ind RS spec) 1),
+	(REPEAT (resolve_tac prems 1)),
+	(REPEAT (atac 1))
+	]);
+
+(* prove induction with usual LCF-Method using fixed point induction *)
 val stream_ind = prove_goal Stream.thy
 "[|adm(P);\
 \  P(UU);\
@@ -440,6 +464,7 @@
 	(REPEAT (atac 1))
 	]);
 
+
 (* ------------------------------------------------------------------------*)
 (* simplify use of Co-induction                                            *)
 (* ------------------------------------------------------------------------*)
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Stream.thy
--- a/src/HOLCF/Stream.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Stream.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -3,7 +3,18 @@
     Author: 	Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Theory for streams without defined empty stream
+Theory for streams without defined empty stream 
+  'a stream = 'a ** ('a stream)u
+
+The type is axiomatized as the least solution of the domain equation above.
+The functor term that specifies the domain equation is: 
+
+  FT = <**,K_{'a},U>
+
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+                     Dissertation, Technische Universit"at M"unchen, 1994
 *)
 
 Stream = Dnat2 +
@@ -44,8 +55,9 @@
 (* axiomatization of recursive type 'a stream                              *)
 (* ----------------------------------------------------------------------- *)
 (* ('a stream,stream_abs) is the initial F-algebra where                   *)
-(* F is the locally continuous functor determined by domain equation       *)
-(* X = 'a ** (X)u                                                          *)
+(* F is the locally continuous functor determined by functor term FT.      *)
+(* domain equation: 'a stream = 'a ** ('a stream)u                         *)
+(* functor term:    FT = <**,K_{'a},U>                                     *)
 (* ----------------------------------------------------------------------- *)
 (* stream_abs is an isomorphism with inverse stream_rep                    *)
 (* identity is the least endomorphism on 'a stream                         *)
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Tr1.thy
--- a/src/HOLCF/Tr1.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Tr1.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -3,22 +3,17 @@
     Author: 	Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Introduve the domain of truth values tr = {UU,TT,FF}
-
-This type is introduced using a domain isomorphism.
+Introduce the domain of truth values tr = one ++ one
 
-The type axiom 
-
-	arities tr :: pcpo
+The type is axiomatized as the least solution of a domain equation.
+The functor term that specifies the domain equation is: 
 
-and the continuity of the Isomorphisms are taken for granted. Since the
-type is not recursive, it could be easily introduced in a purely conservative
-style as it was used for the types sprod, ssum, lift. The definition of the 
-ordering is canonical using abstraction and representation, but this would take
-again a lot of internal constants. It can be easily seen that the axioms below
-are consistent.
+  FT = <++,K_{one},K_{one}>
 
-Partial Ordering is implicit in isomorphims abs_tr,rep_tr and their continuity
+For details see chapter 5 of:
+
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+                     Dissertation, Technische Universit"at M"unchen, 1994
 
 *)
 
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/Tr2.thy
--- a/src/HOLCF/Tr2.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Tr2.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -20,6 +20,10 @@
 
         "neg"           :: "tr -> tr"
 
+translations "x andalso y" => "trand[x][y]"
+             "x orelse y"  => "tror[x][y]"
+             "If b then e1 else e2 fi" => "Icifte[b][e1][e2]"
+              
 rules
 
   ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
@@ -29,29 +33,7 @@
 
 end
 
-ML
-
-(* ----------------------------------------------------------------------*)
-(* translations for the above mixfixes                                   *)
-(* ----------------------------------------------------------------------*)
-
-fun ciftetr ts =
-	let val Cfapp = Const("fapp",dummyT) in	
-	Cfapp $ 
-	   	(Cfapp $
-			(Cfapp$Const("Icifte",dummyT)$(nth_elem (0,ts)))$
-		(nth_elem (1,ts)))$
-	(nth_elem (2,ts))
-	end;
-
-
-val parse_translation = [("@andalso",mk_cinfixtr "@andalso"),
-			("@orelse",mk_cinfixtr "@orelse"),
-			("@cifte",ciftetr)];
-
-val print_translation = [];
 
 
 
 
-
diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/ccc1.thy
--- a/src/HOLCF/ccc1.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/ccc1.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -16,6 +16,7 @@
 	"@oo"		:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
 	"cop @oo"	:: "('b->'c)->('a->'b)->'a->'c" ("cfcomp")
 
+translations "f1 oo f2" => "cfcomp[f1][f2]"
 
 rules
 
@@ -24,15 +25,6 @@
 
 end
 
-ML
-
-(* ----------------------------------------------------------------------*)
-(* parse translations for the above mixfix  oo                           *)
-(* ----------------------------------------------------------------------*)
-
-val parse_translation = [("@oo",mk_cinfixtr "@oo")];
-val print_translation = [];
 
 
 
-