removed explicit_domains/, which is now covered by ex/
authoroheimb
Mon, 24 Feb 1997 16:12:24 +0100
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
removed explicit_domains/, which is now covered by ex/
src/HOLCF/IsaMakefile
src/HOLCF/Makefile
src/HOLCF/ex/Coind.ML
src/HOLCF/ex/Coind.thy
src/HOLCF/explicit_domains/Dlist.ML
src/HOLCF/explicit_domains/Dlist.thy
src/HOLCF/explicit_domains/Dnat.ML
src/HOLCF/explicit_domains/Dnat.thy
src/HOLCF/explicit_domains/Dnat2.ML
src/HOLCF/explicit_domains/Dnat2.thy
src/HOLCF/explicit_domains/README
src/HOLCF/explicit_domains/ROOT.ML
src/HOLCF/explicit_domains/Stream.ML
src/HOLCF/explicit_domains/Stream.thy
src/HOLCF/explicit_domains/Stream2.ML
src/HOLCF/explicit_domains/Stream2.thy
--- a/src/HOLCF/IsaMakefile	Mon Feb 24 09:46:12 1997 +0100
+++ b/src/HOLCF/IsaMakefile	Mon Feb 24 16:12:24 1997 +0100
@@ -45,18 +45,4 @@
 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
 	@$(ISATOOL) testdir $(OUT)/HOLCF ex
 
-
-## Explicit domains
-#
-#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\
-#		 explicit_domains/Dlist.thy \
-#		 explicit_domains/Stream.thy explicit_domains/Stream2.thy
-
-#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
-#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
-#
-#test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
-#	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
-
-
 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
--- a/src/HOLCF/Makefile	Mon Feb 24 09:46:12 1997 +0100
+++ b/src/HOLCF/Makefile	Mon Feb 24 16:12:24 1997 +0100
@@ -86,29 +86,5 @@
 			\"$(COMP)\" is not poly or sml;;\
 	esac
 
-#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy \
-#		explicit_domains/Dlist.thy \
-#		explicit_domains/Stream.thy explicit_domains/Stream2.thy
-
-#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
-#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
-
-#test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
-#	@case `basename "$(COMP)"` in \
-#	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-#		then echo 'make_html := true; exit_use_dir"explicit_domains";\
-#			  quit();' | $(COMP) $(BIN)/HOLCF;\
-#		else echo 'exit_use_dir"explicit_domains"; quit();' \
-#		       | $(COMP) $(BIN)/HOLCF;\
-#		fi;;\
-#	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-#		then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
-#		       | $(BIN)/HOLCF;\
-#		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
-#		fi;;\
-#	*)	echo Bad value for ISABELLECOMP: \
-#			\"$(COMP)\" is not poly or sml;;\
-#	esac
-
 .PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
 
--- a/src/HOLCF/ex/Coind.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,126 +0,0 @@
-(*  Title: 	FOCUS/ex/coind.ML
-    ID:         $ $
-    Author: 	Franz Regensburger
-    Copyright   1993, 1995 Technische Universitaet Muenchen
-*)
-
-open Coind;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties                                             *)
-(* ------------------------------------------------------------------------- *)
-
-
-val nats_def2 = fix_prover2 Coind.thy nats_def 
-	"nats = dzero&&(smap`dsucc`nats)";
-
-val from_def2 = fix_prover2 Coind.thy from_def 
-	"from = (n.n&&(from`(dsucc`n)))";
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-
-val from = prove_goal Coind.thy "from`n = n&&(from`(dsucc`n))"
- (fn prems =>
-	[
-	(rtac trans 1),
-	(rtac (from_def2 RS ssubst) 1),
-	(simp_tac HOLCF_ss  1),
-	(rtac refl 1)
-	]);
-
-
-val from1 = prove_goal Coind.thy "from` = "
- (fn prems =>
-	[
-	(rtac trans 1),
-	(rtac (from RS ssubst) 1),
-	(resolve_tac  stream.con_rews 1),
-	(rtac refl 1)
-	]);
-
-val coind_rews = 
-	[iterator1, iterator2, iterator3, smap1, smap2,from1];
-
-(* ------------------------------------------------------------------------- *)
-(* the example                                                               *)
-(* prove:        nats = from`dzero                                           *)
-(* ------------------------------------------------------------------------- *)
-
-val prems = goal Coind.thy "iterator`n`(smap`dsucc)`nats =\
-\		 n&&(iterator`(dsucc`n)`(smap`dsucc)`nats)";
-by (res_inst_tac [("x","n")] dnat.ind 1);
-by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
-by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
-by (rtac trans 1);
-by (rtac nats_def2 1);
-by (simp_tac (HOLCF_ss addsimps (coind_rews @ dnat.rews)) 1);
-by (rtac trans 1);
-by (etac iterator3 1);
-by (rtac trans 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (rtac trans 1);
-by (etac smap2 1);
-by (rtac cfun_arg_cong 1);
-by (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat.rews)) 1);
-val coind_lemma1 = result();
-
-val prems = goal Coind.thy "nats = from`dzero";
-by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
-by (res_inst_tac [("x","dzero")] exI 2);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2);
-by (rewrite_goals_tac [stream.bisim_def]);
-by (strip_tac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (case_tac "n=" 1);
-by (rtac disjI1 1);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
-by (rtac disjI2 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("x","n")] exI 1);
-by (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1);
-by (res_inst_tac [("x","from`(dsucc`n)")] exI 1);
-by (etac conjI 1);
-by (rtac conjI 1);
-by (res_inst_tac [("x","dsucc`n")] exI 1);
-by (fast_tac HOL_cs 1);
-by (rtac conjI 1);
-by (rtac coind_lemma1 1);
-by (rtac from 1);
-val nats_eq_from = result();
-
-(* another proof using stream_coind_lemma2 *)
-
-val prems = goal Coind.thy "nats = from`dzero";
-by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
-by (rtac stream_coind_lemma2 1);
-by (strip_tac 1);
-by (etac exE 1);
-by (case_tac "n=" 1);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
-by (res_inst_tac [("x","::dnat")] exI 1);
-by (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream.rews) 1);
-by (etac conjE 1);
-by (hyp_subst_tac 1);
-by (rtac conjI 1);
-by (rtac (coind_lemma1 RS ssubst) 1);
-by (rtac (from RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
-by (res_inst_tac [("x","dsucc`n")] exI 1);
-by (rtac conjI 1);
-by (rtac trans 1);
-by (rtac (coind_lemma1 RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
-by (rtac refl 1);
-by (rtac trans 1);
-by (rtac (from RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
-by (rtac refl 1);
-by (res_inst_tac [("x","dzero")] exI 1);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
-val nats_eq_from = result();
--- a/src/HOLCF/ex/Coind.thy	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title: 	FOCUS/ex/Coind.thy
-    ID:         $ $
-    Author: 	Franz Regensburger
-    Copyright   1993 195 Technische Universitaet Muenchen
-
-Example for co-induction on streams
-*)
-
-Coind = Stream + Dnat +
-
-
-consts
-
-	nats		:: "dnat stream"
-	from		:: "dnat  dnat stream"
-
-defs
-	nats_def	"nats  fix`(h.dzero&&(smap`dsucc`h))"
-
-	from_def	"from  fix`(h n.n&&(h`(dsucc`n)))"
-
-end
-
-(*
-		smap`f` = 
-	x  smap`f`(x&&xs) = (f`x)&&(smap`f`xs)
-
-		nats = dzero&&(smap`dsucc`nats)
-
-		from`n = n&&(from`(dsucc`n))
-*)
-
-
--- a/src/HOLCF/explicit_domains/Dlist.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,566 +0,0 @@
-(*  Title:      HOLCF/Dlist.ML
-    Author:     Franz Regensburger
-    ID:         $ $
-    Copyright   1994 Technische Universitaet Muenchen
-
-Lemmas for dlist.thy
-*)
-
-open Dlist;
-
-Delsimps (ex_simps @ all_simps);
-
-(* ------------------------------------------------------------------------*)
-(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict             *)
-(* ------------------------------------------------------------------------*)
-
-val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS 
-        (allI  RSN (2,allI RS iso_strict)));
-
-val dlist_rews = [dlist_iso_strict RS conjunct1,
-                dlist_iso_strict RS conjunct2];
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dlist_copy                                                *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goalw Dlist.thy  [dlist_copy_def] "dlist_copy`f`UU=UU"
- (fn prems =>
-        [
-        (asm_simp_tac (!simpset addsimps 
-                (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
-        ]);
-
-val dlist_copy = [temp];
-
-
-val temp = prove_goalw Dlist.thy  [dlist_copy_def,dnil_def] 
-    "dlist_copy`f`dnil=dnil"
- (fn prems =>
-        [
-        (asm_simp_tac (!simpset addsimps 
-                (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
-        ]);
-
-val dlist_copy = temp :: dlist_copy;
-
-
-val temp = prove_goalw Dlist.thy  [dlist_copy_def,dcons_def] 
-        "xl~=UU ==> dlist_copy`f`(dcons`x`xl)= dcons`x`(f`xl)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps 
-                (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
-        (case_tac "x=UU" 1),
-        (Asm_simp_tac  1),
-        (asm_simp_tac (!simpset addsimps [defined_spair]) 1)
-        ]);
-
-val dlist_copy = temp :: dlist_copy;
-
-val dlist_rews =  dlist_copy @ dlist_rews; 
-
-(* ------------------------------------------------------------------------*)
-(* Exhaustion and elimination for dlists                                   *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "Exh_dlist" Dlist.thy [dcons_def,dnil_def]
-        "l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)"
- (fn prems =>
-        [
-        (Simp_tac 1),
-        (rtac (dlist_rep_iso RS subst) 1),
-        (res_inst_tac [("p","dlist_rep`l")] ssumE 1),
-        (rtac disjI1 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (rtac disjI2 1),
-        (rtac disjI1 1),
-        (res_inst_tac [("p","x")] oneE 1),
-        (contr_tac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (rtac disjI2 1),
-        (rtac disjI2 1),
-        (res_inst_tac [("p","y")] sprodE 1),
-        (contr_tac 1),
-        (rtac exI 1),
-        (rtac exI 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-
-qed_goal "dlistE" Dlist.thy 
-"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons`x`xl;x~=UU;xl~=UU|]==>Q|]==>Q"
- (fn prems =>
-        [
-        (rtac (Exh_dlist RS disjE) 1),
-        (eresolve_tac prems 1),
-        (etac disjE 1),
-        (eresolve_tac prems 1),
-        (etac exE 1),
-        (etac exE 1),
-        (resolve_tac prems 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dlist_when                                                *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goalw  Dlist.thy  [dlist_when_def] "dlist_when`f1`f2`UU=UU"
- (fn prems =>
-        [
-        (asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1)
-        ]);
-
-val dlist_when = [temp];
-
-val temp = prove_goalw  Dlist.thy [dlist_when_def,dnil_def]
- "dlist_when`f1`f2`dnil= f1"
- (fn prems =>
-        [
-        (asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1)
-        ]);
-
-val dlist_when = temp::dlist_when;
-
-val temp = prove_goalw  Dlist.thy [dlist_when_def,dcons_def]
- "[|x~=UU;xl~=UU|] ==> dlist_when`f1`f2`(dcons`x`xl)= f2`x`xl"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1)
-        ]);
-
-val dlist_when = temp::dlist_when;
-
-val dlist_rews = dlist_when @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Rewrites for  discriminators and  selectors                             *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_discsel = [
-        prover [is_dnil_def] "is_dnil`UU=UU",
-        prover [is_dcons_def] "is_dcons`UU=UU",
-        prover [dhd_def] "dhd`UU=UU",
-        prover [dtl_def] "dtl`UU=UU"
-        ];
-
-fun prover defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_discsel = [
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "is_dnil`dnil=TT",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "[|x~=UU;xl~=UU|] ==> is_dnil`(dcons`x`xl)=FF",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "is_dcons`dnil=FF",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "[|x~=UU;xl~=UU|] ==> is_dcons`(dcons`x`xl)=TT",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "dhd`dnil=UU",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "[|x~=UU;xl~=UU|] ==> dhd`(dcons`x`xl)=x",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "dtl`dnil=UU",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
-  "[|x~=UU;xl~=UU|] ==> dtl`(dcons`x`xl)=xl"] @ dlist_discsel;
-
-val dlist_rews = dlist_discsel @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Definedness and strictness                                              *)
-(* ------------------------------------------------------------------------*)
-
-fun prover contr thm = prove_goal Dlist.thy thm
- (fn prems =>
-        [
-        (res_inst_tac [("P1",contr)] classical2 1),
-        (simp_tac (!simpset addsimps dlist_rews) 1),
-        (dtac sym 1),
-        (Asm_simp_tac  1),
-        (simp_tac (!simpset addsimps (prems @ dlist_rews)) 1)
-        ]);
-
-
-val dlist_constrdef = [
-prover "is_dnil`(UU::'a dlist) ~= UU" "dnil~=(UU::'a dlist)",
-prover "is_dcons`(UU::'a dlist) ~= UU" 
-        "[|x~=UU;xl~=UU|]==>dcons`(x::'a)`xl ~= UU"
- ];
-
-
-fun prover defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_constrdef = [
-        prover [dcons_def] "dcons`UU`xl=UU",
-        prover [dcons_def] "dcons`x`UU=UU"
-        ] @ dlist_constrdef;
-
-val dlist_rews = dlist_constrdef @ dlist_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Distinctness wrt. << and =                                              *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dlist.thy  "~dnil << dcons`(x::'a)`xl"
- (fn prems =>
-        [
-        (res_inst_tac [("P1","TT << FF")] classical2 1),
-        (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (case_tac "(x::'a)=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (case_tac "(xl ::'a dlist)=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_dist_less = [temp];
-
-val temp = prove_goal Dlist.thy  "[|x~=UU;xl~=UU|]==>~ dcons`x`xl << dnil"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (res_inst_tac [("P1","TT << FF")] classical2 1),
-        (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_dist_less = temp::dlist_dist_less;
-
-val temp = prove_goal Dlist.thy  "dnil ~= dcons`x`xl"
- (fn prems =>
-        [
-        (case_tac "x=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (case_tac "xl=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("P1","TT = FF")] classical2 1),
-        (resolve_tac dist_eq_tr 1),
-        (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_dist_eq = [temp,temp RS not_sym];
-
-val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Invertibility                                                           *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
-\ dcons`x1`x2 << dcons`y1`y2 |] ==> x1<< y1 & x2 << y2"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac conjI 1),
-        (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1)
-        ]);
-
-val dlist_invert =[temp];
-
-(* ------------------------------------------------------------------------*)
-(* Injectivity                                                             *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
-\ dcons`x1`x2 = dcons`y1`y2 |] ==> x1= y1 & x2 = y2"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac conjI 1),
-        (dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1),
-        (asm_simp_tac (!simpset addsimps dlist_when) 1)
-        ]);
-
-val dlist_inject = [temp];
- 
-
-(* ------------------------------------------------------------------------*)
-(* definedness for  discriminators and  selectors                          *)
-(* ------------------------------------------------------------------------*)
-
-fun prover thm = prove_goal Dlist.thy thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac dlistE 1),
-        (contr_tac 1),
-        (REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1))
-        ]);
-
-val dlist_discsel_def = 
-        [
-        prover "l~=UU ==> is_dnil`l~=UU", 
-        prover "l~=UU ==> is_dcons`l~=UU" 
-        ];
-
-val dlist_rews = dlist_discsel_def @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* enhance the simplifier                                                  *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "dhd2" Dlist.thy "xl~=UU ==> dhd`(dcons`x`xl)=x"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (case_tac "x=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (case_tac "xl=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Properties dlist_take                                                   *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take n`UU=UU"
- (fn prems =>
-        [
-        (res_inst_tac [("n","n")] natE 1),
-        (Asm_simp_tac 1),
-        (Asm_simp_tac 1),
-        (simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_take = [temp];
-
-val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU"
- (fn prems =>
-        [
-        (Asm_simp_tac 1)
-        ]);
-
-val dlist_take = temp::dlist_take;
-
-val temp = prove_goalw Dlist.thy [dlist_take_def]
-        "dlist_take (Suc n)`dnil=dnil"
- (fn prems =>
-        [
-        (Asm_simp_tac 1),
-        (simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_take = temp::dlist_take;
-
-val temp = prove_goalw Dlist.thy [dlist_take_def]
-  "dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)"
- (fn prems =>
-        [
-        (case_tac "x=UU" 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (case_tac "xl=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (res_inst_tac [("n","n")] natE 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-val dlist_take = temp::dlist_take;
-
-val dlist_rews = dlist_take @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* take lemma for dlists                                                  *)
-(* ------------------------------------------------------------------------*)
-
-fun prover reach defs thm  = prove_goalw Dlist.thy defs thm
- (fn prems =>
-        [
-        (res_inst_tac [("t","l1")] (reach RS subst) 1),
-        (res_inst_tac [("t","l2")] (reach RS subst) 1),
-        (stac fix_def2 1),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (rtac lub_equal 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac allI 1),
-        (resolve_tac prems 1)
-        ]);
-
-val dlist_take_lemma = prover dlist_reach  [dlist_take_def]
-        "(!!n.dlist_take n`l1 = dlist_take n`l2) ==> l1=l2";
-
-
-(* ------------------------------------------------------------------------*)
-(* Co -induction for dlists                                               *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "dlist_coind_lemma" Dlist.thy [dlist_bisim_def] 
-"dlist_bisim R ==> ! p q. R p q --> dlist_take n`p = dlist_take n`q"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps dlist_rews) 1),
-        (strip_tac 1),
-        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
-        (atac 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (etac disjE 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (etac exE 1),
-        (etac exE 1),
-        (etac exE 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (REPEAT (etac conjE 1)),
-        (rtac cfun_arg_cong 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "dlist_coind" Dlist.thy "[|dlist_bisim R ; R p q |] ==> p = q"
- (fn prems =>
-        [
-        (rtac dlist_take_lemma 1),
-        (rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
-        (resolve_tac prems 1),
-        (resolve_tac prems 1)
-        ]);
-
-(* ------------------------------------------------------------------------*)
-(* structural induction                                                    *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "dlist_finite_ind" Dlist.thy
-"[|P(UU);P(dnil);\
-\  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)\
-\  |] ==> !l.P(dlist_take n`l)"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps dlist_rews) 1),
-        (resolve_tac prems 1),
-        (rtac allI 1),
-        (res_inst_tac [("l","l")] dlistE 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (case_tac "dlist_take n1`xl=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (resolve_tac prems 1),
-        (resolve_tac prems 1),
-        (atac 1),
-        (atac 1),
-        (etac spec 1)
-        ]);
-
-qed_goal "dlist_all_finite_lemma1" Dlist.thy
-"!l.dlist_take n`l=UU |dlist_take n`l=l"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps dlist_rews) 1),
-        (rtac allI 1),
-        (res_inst_tac [("l","l")] dlistE 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (eres_inst_tac [("x","xl")] allE 1),
-        (etac disjE 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
-        ]);
-
-qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
- (fn prems =>
-        [
-        (case_tac "l=UU" 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
-        (etac disjE 1),
-        (eres_inst_tac [("P","l=UU")] notE 1),
-        (rtac dlist_take_lemma 1),
-        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
-        (atac 1),
-        (subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1),
-        (fast_tac HOL_cs 1),
-        (rtac allI 1),
-        (rtac dlist_all_finite_lemma1 1)
-        ]);
-
-qed_goalw "dlist_all_finite" Dlist.thy [dlist_finite_def] "dlist_finite(l)"
- (fn prems =>
-        [
-        (rtac  dlist_all_finite_lemma2 1)
-        ]);
-
-qed_goal "dlist_ind" Dlist.thy
-"[|P(UU);P(dnil);\
-\  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)|] ==> P(l)"
- (fn prems =>
-        [
-        (rtac (dlist_all_finite_lemma2 RS exE) 1),
-        (etac subst 1),
-        (rtac (dlist_finite_ind RS spec) 1),
-        (REPEAT (resolve_tac prems 1)),
-        (REPEAT (atac 1))
-        ]);
-
-
-
-
--- a/src/HOLCF/explicit_domains/Dlist.thy	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(*  Title:      HOLCF/Dlist.thy
-
-    Author:     Franz Regensburger
-    ID:         $ $
-    Copyright   1994 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dlist.thy INSTEAD.
-
-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 +
-
-types dlist 1
-
-(* ----------------------------------------------------------------------- *)
-(* arity axiom is validated by semantic reasoning                          *)
-(* partial ordering is implicit in the isomorphism axioms and their cont.  *)
-
-arities dlist::(pcpo)pcpo
-
-consts
-
-(* ----------------------------------------------------------------------- *)
-(* essential constants                                                     *)
-
-dlist_rep       :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
-dlist_abs       :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
-
-(* ----------------------------------------------------------------------- *)
-(* abstract constants and auxiliary constants                              *)
-
-dlist_copy      :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
-
-dnil            :: "'a dlist"
-dcons           :: "'a -> 'a dlist -> 'a dlist"
-dlist_when      :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
-is_dnil         :: "'a dlist -> tr"
-is_dcons        :: "'a dlist -> tr"
-dhd             :: "'a dlist -> 'a"
-dtl             :: "'a dlist -> 'a dlist"
-dlist_take      :: "nat => 'a dlist -> 'a dlist"
-dlist_finite    :: "'a dlist => bool"
-dlist_bisim     :: "('a dlist => 'a dlist => bool) => bool"
-
-rules
-
-(* ----------------------------------------------------------------------- *)
-(* axiomatization of recursive type 'a dlist                               *)
-(* ----------------------------------------------------------------------- *)
-(* ('a dlist,dlist_abs) is the initial F-algebra where                     *)
-(* 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                          *)
-
-dlist_abs_iso   "dlist_rep`(dlist_abs`x) = x"
-dlist_rep_iso   "dlist_abs`(dlist_rep`x) = x"
-dlist_copy_def  "dlist_copy == (LAM f. dlist_abs oo \
-\               (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
-\                                oo dlist_rep)"
-dlist_reach     "(fix`dlist_copy)`x=x"
-
-
-defs
-(* ----------------------------------------------------------------------- *)
-(* properties of additional constants                                      *)
-(* ----------------------------------------------------------------------- *)
-(* constructors                                                            *)
-
-dnil_def        "dnil  == dlist_abs`(sinl`one)"
-dcons_def       "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminator functional                                                *)
-
-dlist_when_def 
-"dlist_when == (LAM f1 f2 l.\
-\   sswhen`(LAM x.f1) `(ssplit`(LAM x l.f2`x`l)) `(dlist_rep`l))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminators and selectors                                            *)
-
-is_dnil_def     "is_dnil  == dlist_when`TT`(LAM x l.FF)"
-is_dcons_def    "is_dcons == dlist_when`FF`(LAM x l.TT)"
-dhd_def         "dhd == dlist_when`UU`(LAM x l.x)"
-dtl_def         "dtl == dlist_when`UU`(LAM x l.l)"
-
-(* ----------------------------------------------------------------------- *)
-(* the taker for dlists                                                   *)
-
-dlist_take_def "dlist_take == (%n.iterate n dlist_copy UU)"
-
-(* ----------------------------------------------------------------------- *)
-
-dlist_finite_def        "dlist_finite == (%s.? n.dlist_take n`s=s)"
-
-(* ----------------------------------------------------------------------- *)
-(* definition of bisimulation is determined by domain equation             *)
-(* simplification and rewriting for abstract constants yields def below    *)
-
-dlist_bisim_def "dlist_bisim ==
- ( %R.!l1 l2.
-        R l1 l2 -->
-  ((l1=UU & l2=UU) |
-   (l1=dnil & l2=dnil) |
-   (? x l11 l21. x~=UU & l11~=UU & l21~=UU & 
-               l1=dcons`x`l11 & l2 = dcons`x`l21 & R l11 l21)))"
-
-end
-
-
-
-
--- a/src/HOLCF/explicit_domains/Dnat.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,534 +0,0 @@
-(*  Title:      HOLCF/Dnat.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for dnat.thy 
-*)
-
-open Dnat;
-
-(* ------------------------------------------------------------------------*)
-(* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
-(* ------------------------------------------------------------------------*)
-
-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,
-                dnat_iso_strict RS conjunct2];
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dnat_copy                                                 *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm =  prove_goalw Dnat.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps 
-                (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
-        ]);
-
-val dnat_copy = 
-        [
-        prover [dnat_copy_def] "dnat_copy`f`UU=UU",
-        prover [dnat_copy_def,dzero_def] "dnat_copy`f`dzero= dzero",
-        prover [dnat_copy_def,dsucc_def] 
-                "n~=UU ==> dnat_copy`f`(dsucc`n) = dsucc`(f`n)"
-        ];
-
-val dnat_rews =  dnat_copy @ dnat_rews; 
-
-(* ------------------------------------------------------------------------*)
-(* Exhaustion and elimination for dnat                                     *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def]
-        "n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)"
- (fn prems =>
-        [
-        (Simp_tac  1),
-        (rtac (dnat_rep_iso RS subst) 1),
-        (res_inst_tac [("p","dnat_rep`n")] ssumE 1),
-        (rtac disjI1 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (rtac (disjI1 RS disjI2) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (res_inst_tac [("p","x")] oneE 1),
-        (contr_tac 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (rtac (disjI2 RS disjI2) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "dnatE" Dnat.thy 
- "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc`x;x~=UU|]==>Q|]==>Q"
- (fn prems =>
-        [
-        (rtac (Exh_dnat RS disjE) 1),
-        (eresolve_tac prems 1),
-        (etac disjE 1),
-        (eresolve_tac prems 1),
-        (REPEAT (etac exE 1)),
-        (resolve_tac prems 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dnat_when                                                 *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm =  prove_goalw Dnat.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps 
-                (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
-        ]);
-
-
-val dnat_when = [
-        prover [dnat_when_def] "dnat_when`c`f`UU=UU",
-        prover [dnat_when_def,dzero_def] "dnat_when`c`f`dzero=c",
-        prover [dnat_when_def,dsucc_def] 
-                "n~=UU ==> dnat_when`c`f`(dsucc`n)=f`n"
-        ];
-
-val dnat_rews = dnat_when @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Rewrites for  discriminators and  selectors                             *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_discsel = [
-        prover [is_dzero_def] "is_dzero`UU=UU",
-        prover [is_dsucc_def] "is_dsucc`UU=UU",
-        prover [dpred_def] "dpred`UU=UU"
-        ];
-
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_discsel = [
-        prover [is_dzero_def] "is_dzero`dzero=TT",
-        prover [is_dzero_def] "n~=UU ==>is_dzero`(dsucc`n)=FF",
-        prover [is_dsucc_def] "is_dsucc`dzero=FF",
-        prover [is_dsucc_def] "n~=UU ==> is_dsucc`(dsucc`n)=TT",
-        prover [dpred_def] "dpred`dzero=UU",
-        prover [dpred_def] "n~=UU ==> dpred`(dsucc`n)=n"
-        ] @ dnat_discsel;
-
-val dnat_rews = dnat_discsel @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Definedness and strictness                                              *)
-(* ------------------------------------------------------------------------*)
-
-fun prover contr thm = prove_goal Dnat.thy thm
- (fn prems =>
-        [
-        (res_inst_tac [("P1",contr)] classical2 1),
-        (simp_tac (!simpset addsimps dnat_rews) 1),
-        (dtac sym 1),
-        (Asm_simp_tac  1),
-        (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1)
-        ]);
-
-val dnat_constrdef = [
-        prover "is_dzero`UU ~= UU" "dzero~=UU",
-        prover "is_dsucc`UU ~= UU" "n~=UU ==> dsucc`n~=UU"
-        ]; 
-
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_constrdef = [
-        prover [dsucc_def] "dsucc`UU=UU"
-        ] @ dnat_constrdef;
-
-val dnat_rews = dnat_constrdef @ dnat_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Distinctness wrt. << and =                                              *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dnat.thy  "~dzero << dsucc`n"
- (fn prems =>
-        [
-        (res_inst_tac [("P1","TT << FF")] classical2 1),
-        (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (case_tac "n=UU" 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_dist_less = [temp];
-
-val temp = prove_goal Dnat.thy  "n~=UU ==> ~dsucc`n << dzero"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (res_inst_tac [("P1","TT << FF")] classical2 1),
-        (resolve_tac dist_less_tr 1),
-        (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_dist_less = temp::dnat_dist_less;
-
-val temp = prove_goal Dnat.thy   "dzero ~= dsucc`n"
- (fn prems =>
-        [
-        (case_tac "n=UU" 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (res_inst_tac [("P1","TT = FF")] classical2 1),
-        (resolve_tac dist_eq_tr 1),
-        (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_dist_eq = [temp, temp RS not_sym];
-
-val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Invertibility                                                           *)
-(* ------------------------------------------------------------------------*)
-
-val dnat_invert = 
-        [
-prove_goal Dnat.thy 
-"[|x1~=UU; y1~=UU; dsucc`x1 << dsucc`y1 |] ==> x1<< y1"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ])
-        ];
-
-(* ------------------------------------------------------------------------*)
-(* Injectivity                                                             *)
-(* ------------------------------------------------------------------------*)
-
-val dnat_inject = 
-        [
-prove_goal Dnat.thy 
-"[|x1~=UU; y1~=UU; dsucc`x1 = dsucc`y1 |] ==> x1= y1"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ])
-        ];
-
-(* ------------------------------------------------------------------------*)
-(* definedness for  discriminators and  selectors                          *)
-(* ------------------------------------------------------------------------*)
-
-
-fun prover thm = prove_goal Dnat.thy thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac dnatE 1),
-        (contr_tac 1),
-        (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1))
-        ]);
-
-val dnat_discsel_def = 
-        [
-        prover  "n~=UU ==> is_dzero`n ~= UU",
-        prover  "n~=UU ==> is_dsucc`n ~= UU"
-        ];
-
-val dnat_rews = dnat_discsel_def @ dnat_rews;
-
- 
-(* ------------------------------------------------------------------------*)
-(* Properties dnat_take                                                    *)
-(* ------------------------------------------------------------------------*)
-val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take n`UU = UU"
- (fn prems =>
-        [
-        (res_inst_tac [("n","n")] natE 1),
-        (Asm_simp_tac 1),
-        (Asm_simp_tac 1),
-        (simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_take = [temp];
-
-val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU"
- (fn prems =>
-        [
-        (Asm_simp_tac 1)
-        ]);
-
-val dnat_take = temp::dnat_take;
-
-val temp = prove_goalw Dnat.thy [dnat_take_def]
-        "dnat_take (Suc n)`dzero=dzero"
- (fn prems =>
-        [
-        (Asm_simp_tac 1),
-        (simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_take = temp::dnat_take;
-
-val temp = prove_goalw Dnat.thy [dnat_take_def]
-  "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)"
- (fn prems =>
-        [
-        (case_tac "xs=UU" 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (res_inst_tac [("n","n")] natE 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-val dnat_take = temp::dnat_take;
-
-val dnat_rews = dnat_take @ dnat_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* take lemma for dnats                                                  *)
-(* ------------------------------------------------------------------------*)
-
-fun prover reach defs thm  = prove_goalw Dnat.thy defs thm
- (fn prems =>
-        [
-        (res_inst_tac [("t","s1")] (reach RS subst) 1),
-        (res_inst_tac [("t","s2")] (reach RS subst) 1),
-        (stac fix_def2 1),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (rtac lub_equal 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac allI 1),
-        (resolve_tac prems 1)
-        ]);
-
-val dnat_take_lemma = prover dnat_reach  [dnat_take_def]
-        "(!!n.dnat_take n`s1 = dnat_take n`s2) ==> s1=s2";
-
-
-(* ------------------------------------------------------------------------*)
-(* Co -induction for dnats                                                 *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def] 
-"dnat_bisim R ==> ! p q. R p q --> dnat_take n`p = dnat_take n`q"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps dnat_take) 1),
-        (strip_tac 1),
-        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
-        (atac 1),
-        (asm_simp_tac (!simpset addsimps dnat_take) 1),
-        (etac disjE 1),
-        (asm_simp_tac (!simpset addsimps dnat_take) 1),
-        (etac exE 1),
-        (etac exE 1),
-        (asm_simp_tac (!simpset addsimps dnat_take) 1),
-        (REPEAT (etac conjE 1)),
-        (rtac cfun_arg_cong 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim R;R p q|] ==> p = q"
- (fn prems =>
-        [
-        (rtac dnat_take_lemma 1),
-        (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
-        (resolve_tac prems 1),
-        (resolve_tac prems 1)
-        ]);
-
-
-(* ------------------------------------------------------------------------*)
-(* structural induction for admissible predicates                          *)
-(* ------------------------------------------------------------------------*)
-
-(* not needed any longer
-qed_goal "dnat_ind" Dnat.thy
-"[| adm(P);\
-\   P(UU);\
-\   P(dzero);\
-\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc`s1)|] ==> P(s)"
- (fn prems =>
-        [
-        (rtac (dnat_reach RS subst) 1),
-        (res_inst_tac [("x","s")] spec 1),
-        (rtac fix_ind 1),
-        (rtac adm_all2 1),
-        (rtac adm_subst 1),
-        (cont_tacR 1),
-        (resolve_tac prems 1),
-        (Simp_tac 1),
-        (resolve_tac prems 1),
-        (strip_tac 1),
-        (res_inst_tac [("n","xa")] dnatE 1),
-        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
-        (case_tac "x`xb=UU" 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (resolve_tac prems 1),
-        (eresolve_tac prems 1),
-        (etac spec 1)
-        ]);
-*)
-
-qed_goal "dnat_finite_ind" Dnat.thy
-"[|P(UU);P(dzero);\
-\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
-\  |] ==> !s.P(dnat_take n`s)"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps dnat_rews) 1),
-        (resolve_tac prems 1),
-        (rtac allI 1),
-        (res_inst_tac [("n","s")] dnatE 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (case_tac "dnat_take n1`x=UU" 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (resolve_tac prems 1),
-        (resolve_tac prems 1),
-        (atac 1),
-        (etac spec 1)
-        ]);
-
-qed_goal "dnat_all_finite_lemma1" Dnat.thy
-"!s.dnat_take n`s=UU |dnat_take n`s=s"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps dnat_rews) 1),
-        (rtac allI 1),
-        (res_inst_tac [("n","s")] dnatE 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (eres_inst_tac [("x","x")] allE 1),
-        (etac disjE 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
-        ]);
-
-qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
- (fn prems =>
-        [
-        (case_tac "s=UU" 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
-        (etac disjE 1),
-        (eres_inst_tac [("P","s=UU")] notE 1),
-        (rtac dnat_take_lemma 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (atac 1),
-        (subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1),
-        (fast_tac HOL_cs 1),
-        (rtac allI 1),
-        (rtac dnat_all_finite_lemma1 1)
-        ]);
-
-
-qed_goal "dnat_ind" Dnat.thy
-"[|P(UU);P(dzero);\
-\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
-\  |] ==> P(s)"
- (fn prems =>
-        [
-        (rtac (dnat_all_finite_lemma2 RS exE) 1),
-        (etac subst 1),
-        (rtac (dnat_finite_ind RS spec) 1),
-        (REPEAT (resolve_tac prems 1)),
-        (REPEAT (atac 1))
-        ]);
-
-
-qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
- (fn prems =>
-        [
-        (rtac allI 1),
-        (res_inst_tac [("s","x")] dnat_ind 1),
-        (fast_tac HOL_cs 1),
-        (rtac allI 1),
-        (res_inst_tac [("n","y")] dnatE 1),
-        (fast_tac (HOL_cs addSIs [UU_I]) 1),
-        (Asm_simp_tac 1),
-        (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
-        (rtac allI 1),
-        (res_inst_tac [("n","y")] dnatE 1),
-        (fast_tac (HOL_cs addSIs [UU_I]) 1),
-        (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (strip_tac 1),
-        (subgoal_tac "s1<<xa" 1),
-        (etac allE 1),
-        (dtac mp 1),
-        (atac 1),
-        (etac disjE 1),
-        (contr_tac 1),
-        (Asm_simp_tac 1),
-        (resolve_tac  dnat_invert 1),
-        (REPEAT (atac 1))
-        ]);
-
-
-
-
-
-
--- a/src/HOLCF/explicit_domains/Dnat.thy	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-(*  Title:      HOLCF/Dnat.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
-
-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
-
-*)
-
-Dnat = HOLCF +
-
-types dnat 0
-
-(* ----------------------------------------------------------------------- *)
-(* arrity axiom is valuated by semantical reasoning                        *)
-
-arities dnat::pcpo
-
-consts
-
-(* ----------------------------------------------------------------------- *)
-(* essential constants                                                     *)
-
-dnat_rep        :: " dnat -> (one ++ dnat)"
-dnat_abs        :: "(one ++ dnat) -> dnat"
-
-(* ----------------------------------------------------------------------- *)
-(* abstract constants and auxiliary constants                              *)
-
-dnat_copy       :: "(dnat -> dnat) -> dnat -> dnat"
-
-dzero           :: "dnat"
-dsucc           :: "dnat -> dnat"
-dnat_when       :: "'b -> (dnat -> 'b) -> dnat -> 'b"
-is_dzero        :: "dnat -> tr"
-is_dsucc        :: "dnat -> tr"
-dpred           :: "dnat -> dnat"
-dnat_take       :: "nat => dnat -> dnat"
-dnat_bisim      :: "(dnat => dnat => bool) => bool"
-
-rules
-
-(* ----------------------------------------------------------------------- *)
-(* axiomatization of recursive type dnat                                   *)
-(* ----------------------------------------------------------------------- *)
-(* (dnat,dnat_abs) is the initial F-algebra where                          *)
-(* 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                              *)
-
-dnat_abs_iso    "dnat_rep`(dnat_abs`x) = x"
-dnat_rep_iso    "dnat_abs`(dnat_rep`x) = x"
-dnat_copy_def   "dnat_copy == (LAM f. dnat_abs oo 
-                 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
-dnat_reach      "(fix`dnat_copy)`x=x"
-
-
-defs
-(* ----------------------------------------------------------------------- *)
-(* properties of additional constants                                      *)
-(* ----------------------------------------------------------------------- *)
-(* constructors                                                            *)
-
-dzero_def       "dzero == dnat_abs`(sinl`one)"
-dsucc_def       "dsucc == (LAM n. dnat_abs`(sinr`n))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminator functional                                                *)
-
-dnat_when_def   "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
-
-
-(* ----------------------------------------------------------------------- *)
-(* discriminators and selectors                                            *)
-
-is_dzero_def    "is_dzero == dnat_when`TT`(LAM x.FF)"
-is_dsucc_def    "is_dsucc == dnat_when`FF`(LAM x.TT)"
-dpred_def       "dpred == dnat_when`UU`(LAM x.x)"
-
-
-(* ----------------------------------------------------------------------- *)
-(* the taker for dnats                                                   *)
-
-dnat_take_def "dnat_take == (%n.iterate n dnat_copy UU)"
-
-(* ----------------------------------------------------------------------- *)
-(* definition of bisimulation is determined by domain equation             *)
-(* simplification and rewriting for abstract constants yields def below    *)
-
-dnat_bisim_def "dnat_bisim ==
-(%R.!s1 s2.
-        R s1 s2 -->
-  ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
-  (? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
-                 s2 = dsucc`s21 & R s11 s21)))"
-
-end
--- a/src/HOLCF/explicit_domains/Dnat2.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(*  Title:      HOLCF/Dnat2.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for theory Dnat2.thy
-*)
-
-open Dnat2;
-
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties                                             *)
-(* ------------------------------------------------------------------------- *)
-
-val iterator_def2 = fix_prover2 Dnat2.thy iterator_def 
-        "iterator = (LAM n f x. dnat_when`x`(LAM m.f`(iterator`m`f`x)) `n)";
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
- (fn prems =>
-        [
-        (stac iterator_def2 1),
-        (simp_tac (!simpset addsimps dnat_when) 1)
-        ]);
-
-qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
- (fn prems =>
-        [
-        (stac iterator_def2 1),
-        (simp_tac (!simpset addsimps dnat_when) 1)
-        ]);
-
-qed_goal "iterator3" Dnat2.thy 
-"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac trans 1),
-        (stac iterator_def2 1),
-        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
-        (rtac refl 1)
-        ]);
-
-val dnat2_rews = 
-        [iterator1, iterator2, iterator3];
-
-
-
--- a/src/HOLCF/explicit_domains/Dnat2.thy	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOLCF/Dnat2.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
-
-Additional constants for dnat
-
-*)
-
-Dnat2 = Dnat +
-
-consts
-
-iterator        :: "dnat -> ('a -> 'a) -> 'a -> 'a"
-
-
-defs
-
-iterator_def    "iterator == fix`(LAM h n f x.
-                        dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
-end
-
-(*
-
-                iterator`UU`f`x = UU
-                iterator`dzero`f`x = x
-      n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)
-*)
-
--- a/src/HOLCF/explicit_domains/README	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1995 Technische Universitaet Muenchen
-
-*)
-
-The files contained in this directory are examples for the
-explicit construction of domains. The technique used is described
-in the thesis
-
-	HOLCF: Eine konservative Erweiterung von HOL um LCF
-
-The thesis is available via the web using URL
-
-	http://www4.informatik.tu-muenchen.de/~regensbu/papers.html
-
-
-The same construction is automatically performed if you use the
-type definition package of David Oheimb. See subdirectory HOLCF/domains
-for more details.
-
--- a/src/HOLCF/explicit_domains/ROOT.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1995 Technische Universitaet Muenchen
-
-*)
-
-HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
-
-writeln"Root file for HOLCF examples: explicit domain axiomatisation";
-proof_timing := true;
-
-time_use_thy "Dnat";
-time_use_thy "Dnat2";
-time_use_thy "Stream";
-time_use_thy "Stream2";
-time_use_thy "Dlist";
-
-OS.FileSys.chDir "..";
-maketest "END: Root file for HOLCF examples: explicit domain axiomatization";
--- a/src/HOLCF/explicit_domains/Stream.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,838 +0,0 @@
-(*  
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for stream.thy
-*)
-
-open Stream;
-
-(* ------------------------------------------------------------------------*)
-(* The isomorphisms stream_rep_iso and stream_abs_iso are strict           *)
-(* ------------------------------------------------------------------------*)
-
-val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS 
-        (allI  RSN (2,allI RS iso_strict)));
-
-val stream_rews = [stream_iso_strict RS conjunct1,
-                stream_iso_strict RS conjunct2];
-
-(* ------------------------------------------------------------------------*)
-(* Properties of stream_copy                                               *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm =  prove_goalw Stream.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps 
-                (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
-        ]);
-
-val stream_copy = 
-        [
-        prover [stream_copy_def] "stream_copy`f`UU=UU",
-        prover [stream_copy_def,scons_def] 
-        "x~=UU ==> stream_copy`f`(scons`x`xs)= scons`x`(f`xs)"
-        ];
-
-val stream_rews =  stream_copy @ stream_rews; 
-
-(* ------------------------------------------------------------------------*)
-(* Exhaustion and elimination for streams                                  *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "Exh_stream" Stream.thy [scons_def]
-        "s = UU | (? x xs. x~=UU & s = scons`x`xs)"
- (fn prems =>
-        [
-        (Simp_tac 1),
-        (rtac (stream_rep_iso RS subst) 1),
-        (res_inst_tac [("p","stream_rep`s")] sprodE 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (Asm_simp_tac  1),
-        (res_inst_tac [("p","y")] upE1 1),
-         (contr_tac 1),
-        (rtac disjI2 1),
-        (rtac exI 1),
-        (etac conjI 1),
-	(rtac exI 1),
-        (Asm_simp_tac  1)
-        ]);
-
-qed_goal "streamE" Stream.thy 
-        "[| s=UU ==> Q; !!x xs.[|s=scons`x`xs;x~=UU|]==>Q|]==>Q"
- (fn prems =>
-        [
-        (rtac (Exh_stream RS disjE) 1),
-        (eresolve_tac prems 1),
-        (etac exE 1),
-        (etac exE 1),
-        (resolve_tac prems 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-(* ------------------------------------------------------------------------*)
-(* Properties of stream_when                                               *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm =  prove_goalw Stream.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps 
-                (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
-        ]);
-
-
-val stream_when = [
-        prover [stream_when_def] "stream_when`f`UU=UU",
-        prover [stream_when_def,scons_def] 
-                "x~=UU ==> stream_when`f`(scons`x`xs)= f`x`xs"
-        ];
-
-val stream_rews = stream_when @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Rewrites for  discriminators and  selectors                             *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-val stream_discsel = [
-        prover [is_scons_def] "is_scons`UU=UU",
-        prover [shd_def] "shd`UU=UU",
-        prover [stl_def] "stl`UU=UU"
-        ];
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-val stream_discsel = [
-prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons`(scons`x`xs)=TT",
-prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd`(scons`x`xs)=x",
-prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl`(scons`x`xs)=xs"
-        ] @ stream_discsel;
-
-val stream_rews = stream_discsel @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Definedness and strictness                                              *)
-(* ------------------------------------------------------------------------*)
-
-fun prover contr thm = prove_goal Stream.thy thm
- (fn prems =>
-        [
-        (res_inst_tac [("P1",contr)] classical2 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (dtac sym 1),
-        (Asm_simp_tac 1),
-        (simp_tac (!simpset addsimps (prems @ stream_rews)) 1)
-        ]);
-
-val stream_constrdef = [
-        prover "is_scons`(UU::'a stream)~=UU" "x~=UU ==> scons`(x::'a)`xs~=UU"
-        ]; 
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-val stream_constrdef = [
-        prover [scons_def] "scons`UU`xs=UU"
-        ] @ stream_constrdef;
-
-val stream_rews = stream_constrdef @ stream_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Distinctness wrt. << and =                                              *)
-(* ------------------------------------------------------------------------*)
-
-
-(* ------------------------------------------------------------------------*)
-(* Invertibility                                                           *)
-(* ------------------------------------------------------------------------*)
-
-val stream_invert =
-        [
-prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
-\ scons`x1`x2 << scons`y1`y2|] ==> x1<< y1 & x2 << y2"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac conjI 1),
-        (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
-        (etac box_less 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1)
-        ])
-        ];
-
-(* ------------------------------------------------------------------------*)
-(* Injectivity                                                             *)
-(* ------------------------------------------------------------------------*)
-
-val stream_inject = 
-        [
-prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
-\ scons`x1`x2 = scons`y1`y2 |] ==> x1= y1 & x2 = y2"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac conjI 1),
-        (dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
-        (etac box_equals 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1),
-        (asm_simp_tac (!simpset addsimps stream_when) 1)
-        ])
-        ];
-
-(* ------------------------------------------------------------------------*)
-(* definedness for  discriminators and  selectors                          *)
-(* ------------------------------------------------------------------------*)
-
-fun prover thm = prove_goal Stream.thy thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac streamE 1),
-        (contr_tac 1),
-        (REPEAT (asm_simp_tac (!simpset addsimps stream_discsel) 1))
-        ]);
-
-val stream_discsel_def = 
-        [
-        prover "s~=UU ==> is_scons`s ~= UU", 
-        prover "s~=UU ==> shd`s ~=UU" 
-        ];
-
-val stream_rews = stream_discsel_def @ stream_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Properties stream_take                                                  *)
-(* ------------------------------------------------------------------------*)
-
-val stream_take =
-        [
-prove_goalw Stream.thy [stream_take_def] "stream_take n`UU = UU"
- (fn prems =>
-        [
-        (res_inst_tac [("n","n")] natE 1),
-        (Asm_simp_tac 1),
-        (Asm_simp_tac 1),
-        (simp_tac (!simpset addsimps stream_rews) 1)
-        ]),
-prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
- (fn prems =>
-        [
-        (Asm_simp_tac 1)
-        ])];
-
-fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (Simp_tac 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-val stream_take = [
-prover 
-  "x~=UU ==> stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
-        ] @ stream_take;
-
-val stream_rews = stream_take @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* enhance the simplifier                                                  *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "stream_copy2" Stream.thy 
-     "stream_copy`f`(scons`x`xs) = scons`x`(f`xs)"
- (fn prems =>
-        [
-        (case_tac "x=UU" 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
- (fn prems =>
-        [
-        (case_tac "x=UU" 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-qed_goal "stream_take2" Stream.thy 
- "stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
- (fn prems =>
-        [
-        (case_tac "x=UU" 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-val stream_rews = [stream_iso_strict RS conjunct1,
-                   stream_iso_strict RS conjunct2,
-                   hd stream_copy, stream_copy2]
-                  @ stream_when
-                  @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
-                  @ stream_constrdef
-                  @ stream_discsel_def
-                  @ [ stream_take2] @ (tl stream_take);
-
-
-(* ------------------------------------------------------------------------*)
-(* take lemma for streams                                                  *)
-(* ------------------------------------------------------------------------*)
-
-fun prover reach defs thm  = prove_goalw Stream.thy defs thm
- (fn prems =>
-        [
-        (res_inst_tac [("t","s1")] (reach RS subst) 1),
-        (res_inst_tac [("t","s2")] (reach RS subst) 1),
-        (stac fix_def2 1),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (rtac lub_equal 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
-        (rtac allI 1),
-        (resolve_tac prems 1)
-        ]);
-
-val stream_take_lemma = prover stream_reach  [stream_take_def]
-        "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";
-
-
-qed_goal "stream_reach2" Stream.thy  "lub(range(%i.stream_take i`s))=s"
- (fn prems =>
-        [
-        (res_inst_tac [("t","s")] (stream_reach RS subst) 1),
-        (stac fix_def2 1),
-        (rewtac stream_take_def),
-        (stac contlub_cfun_fun 1),
-        (rtac is_chain_iterate 1),
-        (rtac refl 1)
-        ]);
-
-(* ------------------------------------------------------------------------*)
-(* Co -induction for streams                                               *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def] 
-"stream_bisim R ==> ! p q. R p q --> stream_take n`p = stream_take n`q"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1),
-        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
-        (atac 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (etac exE 1),
-        (etac exE 1),
-        (etac exE 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (REPEAT (etac conjE 1)),
-        (rtac cfun_arg_cong 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "stream_coind" Stream.thy "[|stream_bisim R ;R p q|] ==> p = q"
- (fn prems =>
-        [
-        (rtac stream_take_lemma 1),
-        (rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
-        (resolve_tac prems 1),
-        (resolve_tac prems 1)
-        ]);
-
-(* ------------------------------------------------------------------------*)
-(* structural induction for admissible predicates                          *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "stream_finite_ind" Stream.thy
-"[|P(UU);\
-\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\  |] ==> !s.P(stream_take n`s)"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (resolve_tac prems 1),
-        (rtac allI 1),
-        (res_inst_tac [("s","s")] streamE 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (resolve_tac prems 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (resolve_tac prems 1),
-        (atac 1),
-        (etac spec 1)
-        ]);
-
-qed_goalw "stream_finite_ind2" Stream.thy  [stream_finite_def]
-"(!!n.P(stream_take n`s)) ==>  stream_finite(s) -->P(s)"
- (fn prems =>
-        [
-        (strip_tac 1),
-        (etac exE 1),
-        (etac subst 1),
-        (resolve_tac prems 1)
-        ]);
-
-qed_goal "stream_finite_ind3" Stream.thy 
-"[|P(UU);\
-\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\  |] ==> stream_finite(s) --> P(s)"
- (fn prems =>
-        [
-        (rtac stream_finite_ind2 1),
-        (rtac (stream_finite_ind RS spec) 1),
-        (REPEAT (resolve_tac prems 1)),
-        (REPEAT (atac 1))
-        ]);
-
-(* prove induction using definition of admissibility 
-   stream_reach rsp. stream_reach2 
-   and finite induction stream_finite_ind *)
-
-qed_goal "stream_ind" 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 (rewtac 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 *)
-qed_goal "stream_ind" Stream.thy
-"[|adm(P);\
-\  P(UU);\
-\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\  |] ==> P(s)"
- (fn prems =>
-        [
-        (rtac (stream_reach RS subst) 1),
-        (res_inst_tac [("x","s")] spec 1),
-        (rtac wfix_ind 1),
-        (rtac adm_impl_admw 1),
-        (REPEAT (resolve_tac adm_thms 1)),
-        (rtac adm_subst 1),
-        (cont_tacR 1),
-        (resolve_tac prems 1),
-        (rtac allI 1),
-        (rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
-        (REPEAT (resolve_tac prems 1)),
-        (REPEAT (atac 1))
-        ]);
-
-
-(* ------------------------------------------------------------------------*)
-(* simplify use of Co-induction                                            *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "surjectiv_scons" Stream.thy "scons`(shd`s)`(stl`s)=s"
- (fn prems =>
-        [
-        (res_inst_tac [("s","s")] streamE 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-
-qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
-"!s1 s2. R s1 s2 --> shd`s1 = shd`s2 & R (stl`s1) (stl`s2) ==> stream_bisim R"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (strip_tac 1),
-        (etac allE 1),
-        (etac allE 1),
-        (dtac mp 1),
-        (atac 1),
-        (etac conjE 1),
-        (case_tac "s1 = UU & s2 = UU" 1),
-        (rtac disjI1 1),
-        (fast_tac HOL_cs 1),
-        (rtac disjI2 1),
-        (rtac disjE 1),
-        (etac (de_Morgan_conj RS subst) 1),
-        (res_inst_tac [("x","shd`s1")] exI 1),
-        (res_inst_tac [("x","stl`s1")] exI 1),
-        (res_inst_tac [("x","stl`s2")] exI 1),
-        (rtac conjI 1),
-        (eresolve_tac stream_discsel_def 1),
-        (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
-        (eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
-        (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
-        (res_inst_tac [("x","shd`s2")] exI 1),
-        (res_inst_tac [("x","stl`s1")] exI 1),
-        (res_inst_tac [("x","stl`s2")] exI 1),
-        (rtac conjI 1),
-        (eresolve_tac stream_discsel_def 1),
-        (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
-        (res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
-        (etac sym 1),
-        (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1)
-        ]);
-
-
-(* ------------------------------------------------------------------------*)
-(* theorems about finite and infinite streams                              *)
-(* ------------------------------------------------------------------------*)
-
-(* ----------------------------------------------------------------------- *)
-(* 2 lemmas about stream_finite                                            *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
-         "stream_finite(UU)"
- (fn prems =>
-        [
-        (rtac exI 1),
-        (simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac swap 1),
-        (dtac notnotD 1),
-        (hyp_subst_tac  1),
-        (rtac stream_finite_UU 1)
-        ]);
-
-(* ----------------------------------------------------------------------- *)
-(* a lemma about shd                                                       *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goal "stream_shd_lemma1" Stream.thy "shd`s=UU --> s=UU"
- (fn prems =>
-        [
-        (res_inst_tac [("s","s")] streamE 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (hyp_subst_tac 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-
-(* ----------------------------------------------------------------------- *)
-(* lemmas about stream_take                                                *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goal "stream_take_lemma1" Stream.thy 
- "!x xs.x~=UU --> \
-\  stream_take (Suc n)`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
- (fn prems =>
-        [
-        (rtac allI 1),
-        (rtac allI 1),
-        (rtac impI 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1),
-        (rtac ((hd stream_inject) RS conjunct2) 1),
-        (atac 1),
-        (atac 1),
-        (atac 1)
-        ]);
-
-
-qed_goal "stream_take_lemma2" Stream.thy 
- "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1),
-        (res_inst_tac [("s","s2")] streamE 1),
-         (asm_simp_tac (!simpset addsimps stream_rews) 1),
-	(hyp_subst_tac 1),
-	(rotate_tac ~1 1),
-        (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
-        (subgoal_tac "stream_take n1`xs = xs" 1),
-         (rtac ((hd stream_inject) RS conjunct2) 2),
-           (atac 4),
-          (atac 2),
-         (atac 2),
-        (rtac cfun_arg_cong 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "stream_take_lemma3" Stream.thy 
- "!x xs.x~=UU --> \
-\  stream_take n`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1 ),
-        (res_inst_tac [("P","scons`x`xs=UU")] notE 1),
-        (eresolve_tac stream_constrdef 1),
-        (etac sym 1),
-        (strip_tac 1 ),
-        (rtac (stream_take_lemma2 RS spec RS mp) 1),
-        (res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
-        (atac 1),
-        (atac 1),
-        (etac (stream_take2 RS subst) 1)
-        ]);
-
-qed_goal "stream_take_lemma4" Stream.thy 
- "!x xs.\
-\stream_take n`xs=xs --> stream_take (Suc n)`(scons`x`xs) = scons`x`xs"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-(* ---- *)
-
-qed_goal "stream_take_lemma5" Stream.thy 
-"!s. stream_take n`s=s --> iterate n stl s=UU"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (Simp_tac 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1),
-        (res_inst_tac [("s","s")] streamE 1),
-        (hyp_subst_tac 1),
-        (stac iterate_Suc2 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (stac iterate_Suc2 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (etac allE 1),
-        (etac mp 1),
-        (hyp_subst_tac 1),
-        (etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
-        (atac 1)
-        ]);
-
-qed_goal "stream_take_lemma6" Stream.thy 
-"!s.iterate n stl s =UU --> stream_take n`s=s"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (Simp_tac 1),
-        (strip_tac 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (rtac allI 1),
-        (res_inst_tac [("s","s")] streamE 1),
-        (hyp_subst_tac 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (hyp_subst_tac 1),
-        (stac iterate_Suc2 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1)
-        ]);
-
-qed_goal "stream_take_lemma7" Stream.thy 
-"(iterate n stl s=UU) = (stream_take n`s=s)"
- (fn prems =>
-        [
-        (rtac iffI 1),
-        (etac (stream_take_lemma6 RS spec RS mp) 1),
-        (etac (stream_take_lemma5 RS spec RS mp) 1)
-        ]);
-
-
-qed_goal "stream_take_lemma8" Stream.thy
-"[|adm(P); !n. ? m. n < m & P (stream_take m`s)|] ==> P(s)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac (stream_reach2 RS subst) 1),
-        (rtac adm_lemma11 1),
-        (atac 1),
-        (atac 2),
-        (rewtac stream_take_def),
-        (rtac ch2ch_fappL 1),
-        (rtac is_chain_iterate 1)
-        ]);
-
-(* ----------------------------------------------------------------------- *)
-(* lemmas stream_finite                                                    *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
- "stream_finite(xs) ==> stream_finite(scons`x`xs)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac exE 1),
-        (rtac exI 1),
-        (etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
-        ]);
-
-qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
- "[|x~=UU; stream_finite(scons`x`xs)|] ==> stream_finite(xs)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac exE 1),
-        (rtac exI 1),
-        (etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
-        (atac 1)
-        ]);
-
-qed_goal "stream_finite_lemma3" Stream.thy 
- "x~=UU ==> stream_finite(scons`x`xs) = stream_finite(xs)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac iffI 1),
-        (etac stream_finite_lemma2 1),
-        (atac 1),
-        (etac stream_finite_lemma1 1)
-        ]);
-
-
-qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
- "(!n. s1 << s2  --> stream_take n`s2 = s2 --> stream_finite(s1))\
-\=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
- (fn prems =>
-        [
-        (rtac iffI 1),
-        (fast_tac HOL_cs 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-qed_goal "stream_finite_lemma6" Stream.thy
- "!s1 s2. s1 << s2  --> stream_take n`s2 = s2 --> stream_finite(s1)"
- (fn prems =>
-        [
-        (nat_ind_tac "n" 1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1 ),
-        (hyp_subst_tac  1),
-        (dtac UU_I 1),
-        (hyp_subst_tac  1),
-        (rtac stream_finite_UU 1),
-        (rtac allI 1),
-        (rtac allI 1),
-        (res_inst_tac [("s","s1")] streamE 1),
-        (hyp_subst_tac  1),
-        (strip_tac 1 ),
-        (rtac stream_finite_UU 1),
-        (hyp_subst_tac  1),
-        (res_inst_tac [("s","s2")] streamE 1),
-        (hyp_subst_tac  1),
-        (strip_tac 1 ),
-        (dtac UU_I 1),
-        (asm_simp_tac(!simpset addsimps (stream_rews @ [stream_finite_UU])) 1),
-        (hyp_subst_tac  1),
-        (simp_tac (!simpset addsimps stream_rews) 1),
-        (strip_tac 1 ),
-        (rtac stream_finite_lemma1 1),
-        (subgoal_tac "xs << xsa" 1),
-        (subgoal_tac "stream_take n1`xsa = xsa" 1),
-        (fast_tac HOL_cs 1),
-        (res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
-                   ((hd stream_inject) RS conjunct2) 1),
-        (atac 1),
-        (atac 1),
-        (atac 1),
-        (res_inst_tac [("x1.1","x"),("y1.1","xa")]
-         ((hd stream_invert) RS conjunct2) 1),
-        (atac 1),
-        (atac 1),
-        (atac 1)
-        ]);
-
-qed_goal "stream_finite_lemma7" Stream.thy 
-"s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
- (fn prems =>
-        [
-        (rtac (stream_finite_lemma5 RS iffD1) 1),
-        (rtac allI 1),
-        (rtac (stream_finite_lemma6 RS spec RS spec) 1)
-        ]);
-
-qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
-"stream_finite(s) = (? n. iterate n stl s = UU)"
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps [stream_take_lemma7]) 1)
-        ]);
-
-
-(* ----------------------------------------------------------------------- *)
-(* admissibility of ~stream_finite                                         *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
- "adm(%s. ~ stream_finite(s))"
- (fn prems =>
-        [
-        (strip_tac 1 ),
-        (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical2 1),
-        (atac 2),
-        (subgoal_tac "!i.stream_finite(Y(i))" 1),
-        (fast_tac HOL_cs 1),
-        (rtac allI 1),
-        (rtac (stream_finite_lemma7 RS mp RS mp) 1),
-        (etac is_ub_thelub 1),
-        (atac 1)
-        ]);
-
-(* ----------------------------------------------------------------------- *)
-(* alternative prove for admissibility of ~stream_finite                   *)
-(* show that stream_finite(s) = (? n. iterate n stl s = UU)                *)
-(* and prove adm. of ~(? n. iterate n stl s = UU)                          *)
-(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
-(* ----------------------------------------------------------------------- *)
-
-
-qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
- (fn prems =>
-        [
-        (subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate n stl s ~=UU))" 1),
-        (etac (adm_cong RS iffD2)1),
-        (REPEAT(resolve_tac adm_thms 1)),
-        (rtac  cont_iterate2 1),
-        (rtac allI 1),
-        (stac stream_finite_lemma8 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-
--- a/src/HOLCF/explicit_domains/Stream.thy	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(* 
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
-
-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 +
-
-types stream 1
-
-(* ----------------------------------------------------------------------- *)
-(* arity axiom is validated by semantic reasoning                          *)
-(* partial ordering is implicit in the isomorphism axioms and their cont.  *)
-
-arities stream::(pcpo)pcpo
-
-consts
-
-(* ----------------------------------------------------------------------- *)
-(* essential constants                                                     *)
-
-stream_rep      :: "('a stream) -> ('a ** ('a stream)u)"
-stream_abs      :: "('a ** ('a stream)u) -> ('a stream)"
-
-(* ----------------------------------------------------------------------- *)
-(* abstract constants and auxiliary constants                              *)
-
-stream_copy     :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
-
-scons           :: "'a -> 'a stream -> 'a stream"
-stream_when     :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
-is_scons        :: "'a stream -> tr"
-shd             :: "'a stream -> 'a"
-stl             :: "'a stream -> 'a stream"
-stream_take     :: "nat => 'a stream -> 'a stream"
-stream_finite   :: "'a stream => bool"
-stream_bisim    :: "('a stream => 'a stream => bool) => bool"
-
-rules
-
-(* ----------------------------------------------------------------------- *)
-(* axiomatization of recursive type 'a stream                              *)
-(* ----------------------------------------------------------------------- *)
-(* ('a stream,stream_abs) is the initial F-algebra where                   *)
-(* 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                         *)
-
-stream_abs_iso  "stream_rep`(stream_abs`x) = x"
-stream_rep_iso  "stream_abs`(stream_rep`x) = x"
-stream_copy_def "stream_copy == (LAM f. stream_abs oo 
-                (ssplit`(LAM x y. (|x , (fup`(up oo f))`y|) )) oo stream_rep)"
-stream_reach    "(fix`stream_copy)`x = x"
-
-defs
-(* ----------------------------------------------------------------------- *)
-(* properties of additional constants                                      *)
-(* ----------------------------------------------------------------------- *)
-(* constructors                                                            *)
-
-scons_def       "scons == (LAM x l. stream_abs`(| x, up`l |))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminator functional                                                *)
-
-stream_when_def 
-"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(fup`ID`l)) `(stream_rep`l))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminators and selectors                                            *)
-
-is_scons_def    "is_scons == stream_when`(LAM x l.TT)"
-shd_def         "shd == stream_when`(LAM x l.x)"
-stl_def         "stl == stream_when`(LAM x l.l)"
-
-(* ----------------------------------------------------------------------- *)
-(* the taker for streams                                                   *)
-
-stream_take_def "stream_take == (%n.iterate n stream_copy UU)"
-
-(* ----------------------------------------------------------------------- *)
-
-stream_finite_def       "stream_finite == (%s.? n.stream_take n `s=s)"
-
-(* ----------------------------------------------------------------------- *)
-(* definition of bisimulation is determined by domain equation             *)
-(* simplification and rewriting for abstract constants yields def below    *)
-
-stream_bisim_def "stream_bisim ==
-(%R.!s1 s2.
-        R s1 s2 -->
-  ((s1=UU & s2=UU) |
-  (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
-
-end
-
-
-
-
--- a/src/HOLCF/explicit_domains/Stream2.ML	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for theory Stream2.thy
-*)
-
-open Stream2;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties                                             *)
-(* ------------------------------------------------------------------------- *)
-
-val smap_def2 = fix_prover2 Stream2.thy smap_def 
-        "smap = (LAM f s. stream_when`(LAM x l.scons`(f`x) `(smap`f`l)) `s)";
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-
-qed_goal "smap1" Stream2.thy "smap`f`UU = UU"
- (fn prems =>
-        [
-        (stac smap_def2 1),
-        (simp_tac (!simpset addsimps stream_when) 1)
-        ]);
-
-qed_goal "smap2" Stream2.thy 
-        "x~=UU ==> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (rtac trans 1),
-        (stac smap_def2 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (rtac refl 1)
-        ]);
-
-
-val stream2_rews = [smap1, smap2];
--- a/src/HOLCF/explicit_domains/Stream2.thy	Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* 
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
-
-Additional constants for stream
-*)
-
-Stream2 = Stream +
-
-consts
-
-smap            :: "('a -> 'b) -> 'a stream -> 'b stream"
-
-defs
-
-smap_def
-  "smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
-
-
-end
-      
-
-(*
-                smap`f`UU = UU
-      x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
-
-*)
-