added Classlib.* and Witness.*,
moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.*
and Stream.* from HOLCF/explicit_domains to here
adapted several proofs; now they work again.
Hope that the following strange errors (when committing) do not matter:
rlog error: RCS/Classlib.ML,v: No such file or directory
rlog error: RCS/Classlib.thy,v: No such file or directory
rlog error: RCS/Coind.ML,v: No such file or directory
rlog error: RCS/Coind.thy,v: No such file or directory
rlog error: RCS/Dagstuhl.ML,v: No such file or directory
rlog error: RCS/Dagstuhl.thy,v: No such file or directory
rlog error: RCS/Dlist.ML,v: No such file or directory
rlog error: RCS/Dlist.thy,v: No such file or directory
rlog error: RCS/Dnat.ML,v: No such file or directory
rlog error: RCS/Dnat.thy,v: No such file or directory
rlog error: RCS/Focus_ex.ML,v: No such file or directory
rlog error: RCS/Focus_ex.thy,v: No such file or directory
rlog error: RCS/Stream.ML,v: No such file or directory
rlog error: RCS/Stream.thy,v: No such file or directory
rlog error: RCS/Witness.ML,v: No such file or directory
rlog error: RCS/Witness.thy,v: No such file or directory

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Classlib.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,196 @@
+open Classlib;
+
+qed_goal "strict_qless" Classlib.thy "(UU .< x) = UU & (x .< UU) = UU"
+ (fn prems =>
+	[
+	(simp_tac (HOLCF_ss addsimps [strict_qpo,qless_def,strict_per]) 1)
+	]);
+
+qed_goal "total_qless" Classlib.thy "[|x ~= UU; y ~= UU|] ==> (x .< y) ~= UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
+	(res_inst_tac [("p","x .= y")] trE 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1),
+	(res_inst_tac [("P","x .= y = UU")] notE 1),
+	(etac total_per 1),
+	(atac 1),
+	(atac 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1)
+	]);
+
+qed_goal "irrefl_qless" Classlib.thy "[|x ~= UU|] ==> (x .< x)=FF"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (HOLCF_ss addsimps [total_per,qless_def,refl_per]) 1)
+	]);
+
+qed_goal "asym_qless" Classlib.thy "~((x .< y)=TT & (y .< x)=TT)"
+ (fn prems =>
+	[
+	(case_tac "x ~= UU & y ~= UU" 1),
+	(etac conjE 1),
+	(asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
+	(res_inst_tac [("p","x .= y")] trE 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(asm_simp_tac HOLCF_ss 1),
+	(rtac (sym_per RS subst) 1),
+	(asm_simp_tac HOLCF_ss  1),
+	(rtac (de_Morgan_conj RS iffD1) 1),
+	(res_inst_tac [("Pa","(x .= y)=TT")] classical2 1),
+	(asm_simp_tac (HOLCF_ss addsimps []) 1),
+	(etac conjE 1),
+	(rtac antisym_qpo 1),
+	(atac 1),
+	(atac 1),
+	(subgoal_tac "x=UU Á y=UU" 1),
+	(etac disjE 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1),
+	(fast_tac HOL_cs 1)
+	]);
+
+
+qed_goal "qless_iff" Classlib.thy "((x .< y)=TT) = ((x.=y)=FF & (x .<= y)=TT)"
+ (fn prems =>
+	[
+	(rtac iffI 1),
+	(asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
+	(res_inst_tac [("p","x .= y")] trE 1),
+	(res_inst_tac [("P","TT=UU")] notE 1),
+	(simp_tac (HOLCF_ss addsimps []) 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(asm_simp_tac (HOLCF_ss addsimps []) 1),
+	(res_inst_tac [("P","TT=FF")] notE 1),
+	(simp_tac (HOLCF_ss addsimps []) 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(asm_full_simp_tac (HOLCF_ss addsimps []) 1),
+	(rtac conjI 1),
+	(atac 1),
+	(rtac trans 1),
+	(atac 2),
+	(asm_full_simp_tac (HOLCF_ss addsimps []) 1),
+	(asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1)
+	]);
+
+qed_goal "trans_qless" Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (qless_iff RS iffD2) 1),
+	(rtac conjI 1),
+	(dtac (qless_iff RS iffD1) 1),
+	(dtac (qless_iff RS iffD1) 1),
+	(REPEAT (etac conjE 1)),
+	(case_tac "x~=UU & z~=UU" 1),
+	(REPEAT (etac conjE 1)),
+	(res_inst_tac [("p","x .= z")] trE 1),
+	(res_inst_tac [("P","x .= z = UU")] notE 1),
+	(rtac total_per 1),
+	(atac 1),
+	(atac 1),
+	(atac 1),
+	(res_inst_tac [("P","TT = FF")] notE 1),
+	(simp_tac (HOLCF_ss addsimps []) 1),
+	(subgoal_tac "(y.=z)=TT" 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(atac 1),
+	(rtac antisym_qpo 1),
+	(atac 1),
+	(rtac trans_qpo 1),
+	(atac 2),
+	(etac (antisym_qpo_rev RS conjunct2) 1),
+	(atac 1),
+	(dtac (de_Morgan_conj RS iffD1) 1),
+	(etac disjE 1),
+	(dtac notnotD 1),
+	(res_inst_tac [("P","FF=UU")] notE 1),
+	(simp_tac (HOLCF_ss addsimps []) 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1),
+	(dtac notnotD 1),
+	(res_inst_tac [("P","FF=UU")] notE 1),
+	(simp_tac (HOLCF_ss addsimps []) 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1),
+	(dtac (qless_iff RS iffD1) 1),
+	(dtac (qless_iff RS iffD1) 1),
+	(REPEAT (etac conjE 1)),
+	(rtac trans_qpo 1),
+	(atac 1),
+	(atac 1)
+	]);
+
+(*
+
+proof for transitivity depends on property antisym_qpo_rev
+the proof is a bit lengthy
+
+val prems = goal Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT";
+by (cut_facts_tac prems 1);
+by (rtac (qless_iff RS iffD2) 1);
+by (rtac conjI 1);
+
+by (dtac (qless_iff RS iffD1) 1);
+by (dtac (qless_iff RS iffD1) 1);
+by (REPEAT (etac conjE 1));
+by (case_tac "x~=UU & z~=UU" 1);
+by (REPEAT (etac conjE 1));
+by (res_inst_tac [("p","x .= z")] trE 1);
+by (res_inst_tac [("P","x .= z = UU")] notE 1);
+
+by (rtac total_per 1);
+by (atac 1);
+by (atac 1);
+by (atac 1);
+
+by (res_inst_tac [("P","TT = FF")] notE 1);
+by (simp_tac (HOLCF_ss addsimps []) 1);
+by (subgoal_tac "(y.=z)=TT" 1);
+by (rtac trans 1);
+by (etac sym 1);
+back();
+back();
+back();
+by (atac 1);
+by (rtac antisym_qpo 1);
+by (atac 1);
+by (rtac trans_qpo 1);
+by (atac 2);
+by (etac (antisym_qpo_rev RS conjunct2) 1);
+by (atac 1);
+
+by (dtac (de_Morgan_conj RS iffD1) 1);
+by (etac disjE 1);
+by (dtac notnotD 1);
+by (res_inst_tac [("P","FF=UU")] notE 1);
+by (simp_tac (HOLCF_ss addsimps []) 1);
+by (rtac trans 1);
+by (etac sym 1);
+by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1);
+
+by (dtac notnotD 1);
+by (res_inst_tac [("P","FF=UU")] notE 1);
+by (simp_tac (HOLCF_ss addsimps []) 1);
+by (rtac trans 1);
+by (etac sym 1);
+back();
+by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1);
+
+by (dtac (qless_iff RS iffD1) 1);
+by (dtac (qless_iff RS iffD1) 1);
+by (REPEAT (etac conjE 1));
+by (rtac trans_qpo 1);
+by (atac 1);
+by (atac 1);
+val trans_qless = result();
+*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Classlib.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,195 @@
+(*  Title:      FOCUS/Classlib.thy
+    ID:         $ $
+    Author:     Franz Regensburger
+    Copyright   1995 Technical University Munich
+
+Introduce various type classes
+
+The 8bit package is needed for this theory
+
+The type void of HOLCF/Void.thy is a witness for all the introduced classes.
+Inspect theory Witness.thy for all the proofs. 
+
+the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
+the trivial instance for .= and .<=  is LAM x y.(UU::tr)
+
+the class hierarchy is as follows
+
+        pcpo 
+         |        
+          ----------------
+         |               | 
+         |      --------------------- 
+         |      |       |      |    | 
+        per   cplus  cminus ctimes cdvi
+         |
+       equiv
+       /  \
+      /    \
+     |     |
+    qpo    eq
+     | 
+     |    
+  qlinear
+
+
+*)
+
+Classlib = HOLCF +
+
+(* -------------------------------------------------------------------- *)
+(* class cplus with characteristic constant  ++                         *)
+ 
+classes cplus < pcpo	
+
+arities void :: cplus
+
+ops curried 
+	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)
+
+
+(* class cplus has no characteristic axioms                             *)
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class cminus with characteristic constant --                         *)
+ 
+classes cminus < pcpo	
+
+arities void :: cminus
+
+ops curried 
+	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)
+
+(* class cminus has no characteristic axioms                            *)
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class ctimes with characteristic constant **                         *)
+ 
+classes ctimes < pcpo	
+
+arities void :: ctimes
+
+ops curried 
+	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)
+
+(* class ctimes has no characteristic axioms                            *)
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class cdiv with characteristic constant //                           *)
+ 
+classes cdiv < pcpo	
+
+arities void :: cdiv
+
+ops curried 
+	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)
+
+(* class cdiv has no characteristic axioms                              *)
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class per with characteristic constant .=                            *)
+ 
+classes per < pcpo	
+
+arities void :: per
+
+ops curried 
+	".="	:: "'a::per -> 'a -> tr"	(cinfixl 55)
+syntax (symbols)
+	"op .=" :: "'a::per => 'a => tr"	(infixl "\\<doteq>" 55)
+
+rules 
+
+strict_per	"(UU .= x) = UU & (x .= UU) = UU"
+total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
+flat_per	"flat (UU::'a::per)"
+
+sym_per		"(x .= y) = (y .= x)"
+trans_per	"[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
+
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class equiv is a refinement of of class per                          *)
+ 
+classes equiv < per 	
+
+arities void :: equiv
+
+rules 
+
+refl_per	"[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"
+
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class eq is a refinement of of class equiv                           *)
+ 
+classes eq < equiv  	
+
+arities void :: eq
+
+rules 
+
+weq	"[| (x::'a::eq) ~= UU; y ~= UU |] ==> 
+	 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"
+
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class qpo with characteristic constant .<=                           *)
+(*  .<= is a partial order wrt an equivalence                           *)
+ 
+classes qpo < equiv	
+
+arities void :: qpo
+
+ops curried 
+	".<="	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
+syntax (symbols)
+	"op .<=":: "'a::qpo => 'a => tr"	(infixl "\\<preceq>" 55)
+rules 
+
+strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
+total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
+
+refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
+antisym_qpo	"[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .=  y)=TT"
+trans_qpo	"[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
+
+antisym_qpo_rev	"(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
+
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* irreflexive part .< defined via .<=                                  *)
+ 
+ops curried 
+	".<"	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
+syntax (symbols)
+	"op .<"	:: "'a::qpo => 'a => tr"	(infixl "\\<prec>" 55)
+
+defs
+
+qless_def	"(op .<) Ú LAM x y.If x .= y then FF else x .<= y fi"
+
+(* -------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------- *)
+(* class qlinear is a refinement of of class qpo                        *)
+ 
+classes qlinear < qpo  	
+
+arities void :: qlinear
+
+rules 
+
+qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT Á (y .<= x)=TT "
+
+(* -------------------------------------------------------------------- *)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Coind.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,126 @@
+(*  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();

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Coind.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,33 @@
+(*  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))
+*)
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dagstuhl.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,71 @@
+(* $Id$ *)
+
+open Dagstuhl;
+
+val YS_def2  = fix_prover2 Dagstuhl.thy  YS_def  "YS = y && YS";
+val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = y && y && YYS";
+
+
+val prems = goal Dagstuhl.thy "YYS << y && YYS";
+by (rtac (YYS_def RS def_fix_ind) 1);
+by (Simp_tac 1);
+by (cont_tacR 1);
+by (stac beta_cfun 1);
+by (cont_tacR 1);
+by (rtac monofun_cfun_arg 1);
+by (rtac monofun_cfun_arg 1);
+by (atac 1);
+val lemma3 = result();
+
+val prems = goal Dagstuhl.thy "y && YYS << YYS";
+by (stac YYS_def2 1);
+back();
+by (rtac monofun_cfun_arg 1);
+by (rtac lemma3 1);
+val lemma4=result();
+
+(* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
+
+val prems = goal Dagstuhl.thy "y && YYS = YYS";
+by (rtac antisym_less 1);
+by (rtac lemma4 1);
+by (rtac lemma3 1);
+val lemma5=result();
+
+val prems = goal Dagstuhl.thy "YS = YYS";
+by (rtac stream.take_lemma 1);
+by (nat_ind_tac "n" 1);
+by (simp_tac (!simpset addsimps stream.rews) 1);
+by (stac YS_def2 1);
+by (stac YYS_def2 1);
+by (asm_simp_tac (!simpset addsimps stream.rews) 1);
+by (rtac (lemma5 RS sym RS subst) 1);
+by (rtac refl 1);
+val wir_moel=result();
+
+(* ------------------------------------------------------------------------ *)
+(* Zweite L"osung: Bernhard M"oller                                         *)
+(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
+(* verwendet lemma5                                                         *)
+(* ------------------------------------------------------------------------ *)
+
+val prems = goal Dagstuhl.thy "YYS << YS";
+by (rewtac YYS_def);
+by (rtac fix_least 1);
+by (stac beta_cfun 1);
+by (cont_tacR 1);
+by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
+val lemma6=result();
+
+val prems = goal Dagstuhl.thy "YS << YYS";
+by (rtac (YS_def RS def_fix_ind) 1);
+by (Simp_tac 1);
+by (cont_tacR 1);
+by (stac beta_cfun 1);
+by (cont_tacR 1);
+by (stac (lemma5 RS sym) 1);
+by (etac monofun_cfun_arg 1);
+val lemma7 = result();
+
+val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dagstuhl.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,17 @@
+(* $Id$ *)
+
+
+Dagstuhl  =  Stream +
+
+consts
+        y  :: "'a"
+       YS  :: "'a stream"
+       YYS :: "'a stream"
+
+defs
+
+YS_def    "YS  == fix`(LAM x. y && x)"
+YYS_def   "YYS == fix`(LAM z. y && y && z)"
+  
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dlist.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,37 @@
+open Dlist;
+
+(* ------------------------------------------------------------------------- *)
+(* expand fixed point properties of lmap                                     *)
+(* ------------------------------------------------------------------------- *)
+
+bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def 
+        "lmap = (LAM f s.case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
+
+(* ------------------------------------------------------------------------- *)
+(* recursive  properties   of lmap                                           *)
+(* ------------------------------------------------------------------------- *)
+
+qed_goal "lmap1" Dlist.thy "lmap`f`UU = UU"
+ (fn prems =>
+	[
+	(rtac (lmap_def2 RS ssubst) 1),
+	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
+	]);
+
+qed_goal "lmap2" Dlist.thy "lmap`f`dnil = dnil"
+ (fn prems =>
+	[
+	(rtac (lmap_def2 RS ssubst) 1),
+	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
+	]);
+
+qed_goal "lmap3" Dlist.thy 
+	"[|x~=UU; xs~=UU|] ==> lmap`f`(x##xs) = (f`x)##(lmap`f`xs)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac trans 1),
+	(rtac (lmap_def2 RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dlist.rews) 1),
+	(rtac refl 1)
+	]);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dlist.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,27 @@
+(*  Title:      HOLCF/Dlist.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
+*)
+
+Dlist = Classlib +
+
+domain 'a dlist = dnil | "##" (dhd::'a) (dtl::'a dlist) (cinfixr 65)
+
+ops curried
+
+lmap	:: "('a -> 'b) -> 'a dlist -> 'b dlist"
+lmem	:: "('a::eq)  -> 'a dlist -> tr"		(cinfixl 50)
+
+defs
+
+lmap_def "   lmap Ú fix`(LAM h f s. case s of dnil => dnil 
+				      | x ## xs => f`x ## h`f`xs)"
+
+lmem_def "op lmem Ú fix`(LAM h e l. case l of dnil => FF
+			 | x ## xs => If e Ù x then TT else h`e`xs fi)"
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dnat.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,74 @@
+(*  Title:      HOLCF/Dnat.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993, 1995 Technische Universitaet Muenchen
+
+*)
+
+open Dnat;
+
+(* ------------------------------------------------------------------------- *)
+(* expand fixed point properties                                             *)
+(* ------------------------------------------------------------------------- *)
+
+bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def 
+	"iterator = (LAM n f x. case n of dzero => x | \
+\                                     dsucc`m => f`(iterator`m`f`x))");
+
+(* ------------------------------------------------------------------------- *)
+(* recursive  properties                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+qed_goal "iterator1" Dnat.thy "iterator`UU`f`x = UU"
+ (fn prems =>
+	[
+	(rtac (iterator_def2 RS ssubst) 1),
+	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
+	]);
+
+qed_goal "iterator2" Dnat.thy "iterator`dzero`f`x = x"
+ (fn prems =>
+	[
+	(rtac (iterator_def2 RS ssubst) 1),
+	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
+	]);
+
+qed_goal "iterator3" Dnat.thy 
+"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac trans 1),
+	(rtac (iterator_def2 RS ssubst) 1),
+	(asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1),
+	(rtac refl 1)
+	]);
+
+val iterator_rews = 
+	[iterator1, iterator2, iterator3];
+
+val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(x::dnat)" (fn _ => [
+	(rtac allI 1),
+	(res_inst_tac [("x","x")] dnat.ind 1),
+	(fast_tac HOL_cs 1),
+	(rtac allI 1),
+	(res_inst_tac [("x","y")] dnat.cases 1),
+	(fast_tac (HOL_cs addSIs [UU_I]) 1),
+	(Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps dnat.dists_le) 1),
+	(rtac allI 1),
+	(res_inst_tac [("x","y")] dnat.cases 1),
+	(fast_tac (HOL_cs addSIs [UU_I]) 1),
+	(asm_simp_tac (!simpset addsimps dnat.dists_le) 1),
+	(asm_simp_tac (!simpset addsimps dnat.rews) 1),
+	(strip_tac 1),
+	(subgoal_tac "d<<da" 1),
+	(etac allE 1),
+	(dtac mp 1),
+	(atac 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(Asm_simp_tac 1),
+	(resolve_tac  dnat.inverts 1),
+	(REPEAT (atac 1))]);
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dnat.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,19 @@
+(*  Title:      HOLCF/Dnat.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Theory for the domain of natural numbers  dnat = one ++ dnat
+*)
+
+Dnat = HOLCF +
+
+domain dnat = dzero | dsucc (dpred :: dnat)
+
+constdefs
+
+iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
+            "iterator == fix`(LAM h n f x . case n of dzero   => x
+                                                    | dsucc`m => f`(h`m`f`x))"
+
+end

--- a/src/HOLCF/ex/Fix2.thy	Fri Jan 31 16:51:58 1997 +0100
+++ b/src/HOLCF/ex/Fix2.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -20,19 +20,3 @@
 gix2_def "F`y=y ==> gix`F << y"
 
 end
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Focus_ex.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,148 @@
+open Focus_ex;
+
+(* first some logical trading *)
+
+val prems = goal Focus_ex.thy
+"is_g(g) = \ 
+\ (? f. is_f(f) &  (!x.(? z. <g`x,z> = f`<x,z> &  \
+\                  (! w y. <y,w> = f`<x,w>  --> z << w))))";
+by (simp_tac (HOL_ss addsimps [is_g,is_net_g]) 1);
+by (fast_tac HOL_cs 1);
+val lemma1 = result();
+
+val prems = goal Focus_ex.thy
+"(? f. is_f(f) &  (!x. (? z. <g`x,z> = f`<x,z> &  \
+\                 (!w y. <y,w> = f`<x,w>  --> z << w)))) \
+\ = \ 
+\ (? f. is_f(f) &  (!x. ? z.\
+\       g`x = cfst`(f`<x,z>) &  \
+\         z = csnd`(f`<x,z>) &  \
+\       (! w y.  <y,w> = f`<x,w> --> z << w)))";
+by (rtac iffI 1);
+by (etac exE 1);
+by (res_inst_tac [("x","f")] exI 1);
+by (REPEAT (etac conjE 1));
+by (etac conjI 1);
+by (strip_tac 1);
+by (etac allE 1);
+by (etac exE 1);
+by (res_inst_tac [("x","z")] exI 1);
+by (REPEAT (etac conjE 1));
+by (rtac conjI 1);
+by (rtac conjI 2);
+by (atac 3);
+by (dtac sym 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (dtac sym 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (etac exE 1);
+by (res_inst_tac [("x","f")] exI 1);
+by (REPEAT (etac conjE 1));
+by (etac conjI 1);
+by (strip_tac 1);
+by (etac allE 1);
+by (etac exE 1);
+by (res_inst_tac [("x","z")] exI 1);
+by (REPEAT (etac conjE 1));
+by (rtac conjI 1);
+by (atac 2);
+by (rtac trans 1);
+by (rtac (surjective_pairing_Cprod2) 2);
+by (etac subst 1);
+by (etac subst 1);
+by (rtac refl 1);
+val lemma2 = result();
+
+(* direction def_g(g) --> is_g(g) *)
+
+val prems = goal Focus_ex.thy "def_g(g) --> is_g(g)";
+by (simp_tac (HOL_ss addsimps [def_g,lemma1, lemma2]) 1);
+by (rtac impI 1);
+by (etac exE 1);
+by (res_inst_tac [("x","f")] exI 1);
+by (REPEAT (etac conjE 1));
+by (etac conjI 1);
+by (strip_tac 1);
+by (res_inst_tac [("x","fix`(LAM k.csnd`(f`<x,k>))")] exI 1);
+by (rtac conjI 1);
+ by (asm_simp_tac HOLCF_ss 1);
+ by (rtac trans 1);
+  by (rtac surjective_pairing_Cprod2 2);
+ by (rtac cfun_arg_cong 1);
+ by (rtac trans 1);
+  by (rtac fix_eq 1);
+ by (Simp_tac 1);
+by (strip_tac 1);
+by (rtac fix_least 1);
+by (Simp_tac 1);
+by(etac exE 1);
+by (dtac sym 1);
+back();
+by (asm_simp_tac HOLCF_ss 1);
+val lemma3 = result();
+
+(* direction is_g(g) --> def_g(g) *)
+val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)";
+by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
+		     addsimps [lemma1,lemma2,def_g]) 1);
+by (rtac impI 1);
+by (etac exE 1);
+by (res_inst_tac [("x","f")] exI 1);
+by (REPEAT (etac conjE 1));
+by (etac conjI 1);
+by (rtac ext_cfun 1);
+by (eres_inst_tac [("x","x")] allE 1);
+by (etac exE 1);
+by (REPEAT (etac conjE 1));
+by (subgoal_tac "fix`(LAM k. csnd`(f`<x, k>)) = z" 1);
+ by (asm_simp_tac HOLCF_ss 1);
+by (subgoal_tac "! w y. f`<x, w> = <y, w>  --> z << w" 1);
+by (rtac sym 1);
+by (rtac fix_eqI 1);
+by (asm_simp_tac HOLCF_ss 1);
+by (etac sym 1);
+by (rtac allI 1);
+by (simp_tac HOLCF_ss 1);
+by (strip_tac 1);
+by (subgoal_tac "f`<x, za> = <cfst`(f`<x,za>),za>" 1);
+by (fast_tac HOL_cs 1);
+by (rtac trans 1);
+by (rtac (surjective_pairing_Cprod2 RS sym) 1);
+by (etac cfun_arg_cong 1);
+by (strip_tac 1);
+by (REPEAT (etac allE 1));
+by (etac mp 1);
+by (etac sym 1);
+val lemma4 = result();
+
+(* now we assemble the result *)
+
+val prems = goal Focus_ex.thy "def_g = is_g";
+by (rtac ext 1);
+by (rtac iffI 1);
+by (etac (lemma3 RS mp) 1);
+by (etac (lemma4 RS mp) 1);
+val loopback_eq = result();
+
+val prems = goal Focus_ex.thy 
+"(? f.\
+\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
+\ -->\
+\ (? g. def_g(g::'b stream -> 'c stream ))";
+by (simp_tac (HOL_ss addsimps [def_g]) 1);
+by (strip_tac 1);
+by (etac exE 1);
+by (rtac exI 1);
+by (rtac exI 1);
+by (etac conjI 1);
+by (rtac refl 1);
+val L2 = result();
+
+val prems = goal Focus_ex.thy 
+"(? f.\
+\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
+\ -->\
+\ (? g. is_g(g::'b stream -> 'c stream ))";
+by (rtac (loopback_eq RS subst) 1);
+by (rtac L2 1);
+val conservative_loopback = result();

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Focus_ex.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,136 @@
+(* Specification of the following loop back device
+
+
+          g 
+           --------------------
+          |      -------       |
+       x  |     |       |      |  y
+    ------|---->|       |------| ----->        
+          |  z  |   f   | z    |
+          |  -->|       |---   |
+          | |   |       |   |  |
+          | |    -------    |  |
+          | |               |  |
+          |  <--------------   |
+          |                    | 
+           --------------------
+
+
+First step: Notation in Agent Network Description Language (ANDL)
+-----------------------------------------------------------------
+
+agent f
+	input  channel i1:'b i2: ('b,'c) tc
+	output channel o1:'c o2: ('b,'c) tc
+is
+	Rf(i1,i2,o1,o2)  (left open in the example)
+end f
+
+agent g
+	input  channel x:'b 
+	output channel y:'c 
+is network
+	<y,z> = f`<x,z>
+end network
+end g
+
+
+Remark: the type of the feedback depends at most on the types of the input and
+        output of g. (No type miracles inside g)
+
+Second step: Translation of ANDL specification to HOLCF Specification
+---------------------------------------------------------------------
+
+Specification of agent f ist translated to predicate is_f
+
+is_f :: ('b stream * ('b,'c) tc stream -> 
+		'c stream * ('b,'c) tc stream) => bool
+
+is_f f  = !i1 i2 o1 o2. 
+	f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
+
+Specification of agent g is translated to predicate is_g which uses
+predicate is_net_g
+
+is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
+	    'b stream => 'c stream => bool
+
+is_net_g f x y = 
+	? z. <y,z> = f`<x,z> & 
+	!oy hz. <oy,hz> = f`<x,hz> --> z << hz 
+
+
+is_g :: ('b stream -> 'c stream) => bool
+
+is_g g  = ? f. is_f f  & (!x y. g`x = y --> is_net_g f x y
+	  
+Third step: (show conservativity)
+-----------
+
+Suppose we have a model for the theory TH1 which contains the axiom
+
+	? f. is_f f 
+
+In this case there is also a model for the theory TH2 that enriches TH1 by
+axiom
+
+	? g. is_g g 
+
+The result is proved by showing that there is a definitional extension
+that extends TH1 by a definition of g.
+
+
+We define:
+
+def_g g  = 
+         (? f. is_f f  & 
+	      g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
+	
+Now we prove:
+
+	(? f. is_f f ) --> (? g. is_g g) 
+
+using the theorems
+
+loopback_eq)	def_g = is_g			(real work) 
+
+L1)		(? f. is_f f ) --> (? g. def_g g)  (trivial)
+
+*)
+
+Focus_ex = Stream +
+
+types  tc 2
+
+arities tc:: (pcpo,pcpo)pcpo
+
+consts
+
+is_f     ::
+ "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
+is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
+	    'b stream => 'c stream => bool"
+is_g     :: "('b stream -> 'c stream) => bool"
+def_g    :: "('b stream -> 'c stream) => bool"
+Rf	 :: 
+"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
+
+defs
+
+is_f		"is_f f == (!i1 i2 o1 o2.
+			f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
+
+is_net_g	"is_net_g f x y == (? z. 
+			<y,z> = f`<x,z> &
+			(!oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
+
+is_g		"is_g g  == (? f.
+			is_f f  & 
+			(!x y. g`x = y --> is_net_g f x y))"
+
+
+def_g		"def_g g == (? f.
+			is_f f  & 
+	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k.csnd`(f`<x,k>))>)))" 
+
+end

--- a/src/HOLCF/ex/Hoare.ML	Fri Jan 31 16:51:58 1997 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -103,22 +103,6 @@
 
 (* ----- access to definitions ----- *)
 
-val p_def2 = prove_goalw Hoare.thy [p_def]
-"p = fix`(LAM f x. If b1`x then f`(g`x) else x fi)"
- (fn prems =>
-        [
-        (rtac refl 1)
-        ]);
-
-val q_def2 = prove_goalw Hoare.thy [q_def]
-"q = fix`(LAM f x. If b1`x orelse b2`x then \
-\     f`(g`x) else x fi)"
- (fn prems =>
-        [
-        (rtac refl 1)
-        ]);
-
-
 val p_def3 = prove_goal Hoare.thy 
 "p`x = If b1`x then p`(g`x) else x fi"
  (fn prems =>
@@ -275,8 +259,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (stac p_def2 1),
-        (rtac fix_ind 1),
+        (rtac (p_def RS def_fix_ind) 1),
         (rtac adm_all 1),
         (rtac allI 1),
         (rtac adm_eq 1),
@@ -309,8 +292,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (stac q_def2 1),
-        (rtac fix_ind 1),
+        (rtac (q_def RS def_fix_ind) 1),
         (rtac adm_all 1),
         (rtac allI 1),
         (rtac adm_eq 1),
@@ -351,8 +333,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (stac q_def2 1),
-        (rtac fix_ind 1),
+        (rtac (q_def RS def_fix_ind) 1),
         (rtac adm_all 1),
         (rtac allI 1),
         (rtac adm_eq 1),

--- a/src/HOLCF/ex/ROOT.ML	Fri Jan 31 16:51:58 1997 +0100
+++ b/src/HOLCF/ex/ROOT.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -11,9 +11,16 @@
 writeln"Root file for HOLCF examples";
 proof_timing := true;
 
+time_use_thy "Classlib";
+time_use_thy "Witness";
+time_use_thy "Dnat";
+time_use_thy "Dlist";
+time_use_thy "Stream";
+time_use_thy "Dagstuhl";
+time_use_thy "Focus_ex";
+time_use_thy "Fix2";
 time_use_thy "Hoare";
 time_use_thy "Loop";
-time_use_thy "Fix2";
 time_use "loeckx.ML";
 
 OS.FileSys.chDir "..";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Stream.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,370 @@
+(*  Title: 	FOCUS/Stream.ML
+    ID:         $ $
+    Author: 	Franz Regensburger, David von Oheimb
+    Copyright   1993, 1995 Technische Universitaet Muenchen
+
+Theorems for Stream.thy
+*)
+
+open Stream;
+
+fun stream_case_tac s i = res_inst_tac [("x",s)] stream.cases i
+			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
+
+
+(* ----------------------------------------------------------------------- *)
+(* theorems about scons                                                    *)
+(* ----------------------------------------------------------------------- *)
+
+section "scons";
+
+qed_goal "scons_eq_UU" thy "a && s = UU = (a = UU)" (fn _ => [
+	safe_tac HOL_cs,
+	etac contrapos2 1,
+	safe_tac (HOL_cs addSIs stream.con_rews)]);
+
+qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R" (fn prems => [
+	cut_facts_tac prems 1,
+	dresolve_tac stream.con_rews 1,
+	contr_tac 1]);
+
+qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU &  x = a && y)" (fn _ =>[
+	cut_facts_tac [stream.exhaust] 1,
+	safe_tac HOL_cs,
+	   contr_tac 1,
+	  fast_tac (HOL_cs addDs (tl stream.con_rews)) 1,
+	 fast_tac HOL_cs 1,
+	fast_tac (HOL_cs addDs (tl stream.con_rews)) 1]);
+
+qed_goal "stream_prefix" thy 
+"[| a && s << t; a ~= UU  |] ==> ? b tt. t = b && tt &  b ~= UU &  s << tt" (fn prems => [
+	cut_facts_tac prems 1,
+	stream_case_tac "t" 1,
+	 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2,hd (tl stream.con_rews)]) 1,
+	fast_tac (HOL_cs addDs stream.inverts) 1]);
+
+qed_goal "stream_flat_prefix" thy 
+"[| x && xs << y && ys; (x::'a) ~= UU; flat (z::'a) |] ==> x = y &  xs << ys"(fn prems=>[
+	cut_facts_tac prems 1,
+	(forward_tac stream.inverts 1),
+	(safe_tac HOL_cs),
+	(dtac (hd stream.con_rews RS subst) 1),
+	(fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1),
+	(rewtac flat_def),
+	(fast_tac HOL_cs 1)]);
+
+qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \
+\(x = UU |  (? a y. x = a && y &  a ~= UU &  a << b &  y << z))" (fn prems => [
+	cut_facts_tac prems 1,
+	safe_tac HOL_cs,
+	  stream_case_tac "x" 1,
+	   safe_tac (HOL_cs addSDs stream.inverts 
+			    addSIs [minimal, monofun_cfun, monofun_cfun_arg]),
+	fast_tac HOL_cs 1]);
+
+qed_goal "stream_inject_eq" thy
+ "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)" (fn prems => [
+	cut_facts_tac prems 1,
+	safe_tac (HOL_cs addSEs stream.injects)]);	
+
+
+(* ----------------------------------------------------------------------- *)
+(* theorems about stream_when                                              *)
+(* ----------------------------------------------------------------------- *)
+
+section "stream_when";
+
+qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [
+	stream_case_tac "s" 1,
+	ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews))
+	]);
+	
+
+(* ----------------------------------------------------------------------- *)
+(* theorems about ft and rt                                                *)
+(* ----------------------------------------------------------------------- *)
+
+section "ft & rt";
+
+(*
+qed_goal "stream_ft_lemma1" thy "ft`s=UU --> s=UU" (fn prems => [
+	stream_case_tac "s" 1,
+	REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)]);
+*)
+
+qed_goal "ft_defin" thy "s~=UU ==> ft`s~=UU" (fn prems => [
+	cut_facts_tac prems 1,
+	stream_case_tac "s" 1,
+	fast_tac HOL_cs 1,
+	asm_simp_tac (HOLCF_ss addsimps stream.rews) 1]);
+
+qed_goal "rt_strict_rev" thy "rt`s~=UU ==> s~=UU" (fn prems => [
+	cut_facts_tac prems 1,
+	etac contrapos 1,
+	asm_simp_tac (HOLCF_ss addsimps stream.sel_rews) 1]);
+
+qed_goal "surjectiv_scons" thy "(ft`s)&&(rt`s)=s"
+ (fn prems =>
+	[
+	stream_case_tac "s" 1,
+	REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)
+	]);
+
+qed_goal_spec_mp "monofun_rt_mult" thy 
+"!x s. x << s --> iterate i rt x << iterate i rt s" (fn _ => [
+	nat_ind_tac "i" 1,
+	simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
+	strip_tac 1,
+	stream_case_tac "x" 1,
+	rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1,
+	dtac stream_prefix 1,
+	 safe_tac HOL_cs,
+	asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1]);
+			
+
+(* ----------------------------------------------------------------------- *)
+(* theorems about stream_take                                              *)
+(* ----------------------------------------------------------------------- *)
+
+section "stream_take";
+
+qed_goal "stream_reach2" thy  "(LUB i. stream_take i`s) = s"
+ (fn prems =>
+	[
+	(res_inst_tac [("t","s")] (stream.reach RS subst) 1),
+	(stac fix_def2 1),
+	(rewrite_goals_tac [stream.take_def]),
+	(stac contlub_cfun_fun 1),
+	(rtac is_chain_iterate 1),
+	(rtac refl 1)
+	]);
+
+qed_goal "chain_stream_take" thy "is_chain (%i.stream_take i`s)" (fn _ => [
+	rtac is_chainI 1,
+	subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
+	fast_tac HOL_cs 1,
+	rtac allI 1,
+	nat_ind_tac "i" 1,
+	 simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
+	rtac allI 1,
+	stream_case_tac "s" 1,
+	 simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
+	asm_simp_tac (HOLCF_ss addsimps monofun_cfun_arg::stream.take_rews) 1]);
+
+qed_goalw "stream_take_more" thy [stream.take_def] 
+	"stream_take n`x = x ==> stream_take (Suc n)`x = x" (fn prems => [
+		cut_facts_tac prems 1,
+		rtac antisym_less 1,
+		rtac (stream.reach RS subst) 1, (* 1*back(); *)
+		rtac monofun_cfun_fun 1,
+		stac fix_def2 1,
+		rtac is_ub_thelub 1,
+		rtac is_chain_iterate 1,
+		etac subst 1, (* 2*back(); *)
+		rtac monofun_cfun_fun 1,
+		rtac (rewrite_rule [is_chain] is_chain_iterate RS spec) 1]);
+
+(*
+val stream_take_lemma2 = prove_goal 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),
+	(hyp_subst_tac  1),
+	(simp_tac (!simpset addsimps stream_rews) 1),
+	(rtac allI 1),
+	(res_inst_tac [("s","s2")] streamE 1),
+	(asm_simp_tac (!simpset addsimps stream_rews) 1),
+	(asm_simp_tac (!simpset addsimps stream_rews) 1),
+	(strip_tac 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)
+	]);
+*)
+
+val stream_take_lemma3 = prove_goal thy 
+ "!x xs.x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
+ (fn prems => [
+	(nat_ind_tac "n" 1),
+	(asm_simp_tac (HOL_ss addsimps stream.take_rews) 1),
+	(strip_tac 1),
+	(res_inst_tac [("P","x && xs=UU")] notE 1),
+	(eresolve_tac stream.con_rews 1),
+	(etac sym 1),
+	(strip_tac 1),
+	(rtac stream_take_more 1),
+	(res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1),
+	(etac (hd(tl(tl(stream.take_rews))) RS subst) 1),
+	(atac 1),
+	(atac 1)]) RS spec RS spec RS mp RS mp;
+
+val stream_take_lemma4 = prove_goal thy 
+ "!x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs"
+ (fn _ => [
+	(nat_ind_tac "n" 1),
+	(simp_tac (HOL_ss addsimps stream.take_rews) 1),
+	(simp_tac (HOL_ss addsimps stream.take_rews) 1)
+	]) RS spec RS spec RS mp;
+
+
+(* ------------------------------------------------------------------------- *)
+(* special induction rules                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+section "induction";
+
+qed_goalw "stream_finite_ind" thy [stream.finite_def] 
+ "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" 
+ (fn prems => [
+	(cut_facts_tac prems 1),
+	(etac exE 1),
+	(etac subst 1),
+	(rtac stream.finite_ind 1),
+	(atac 1),
+	(eresolve_tac prems 1),
+	(atac 1)]);
+
+qed_goal "stream_finite_ind2" thy
+"[| P UU;\
+\   !! x    .    x ~= UU                  ==> P (x      && UU); \
+\   !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )  \
+\   |] ==> !s. P (stream_take n`s)" (fn prems => [
+	res_inst_tac [("n","n")] nat_induct2 1,
+	  asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
+	 rtac allI 1,
+	 stream_case_tac "s" 1,
+	  asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
+	 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
+	rtac allI 1,
+	stream_case_tac "s" 1,
+	 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
+	res_inst_tac [("x","sa")] stream.cases 1,
+	 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
+	asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1]);
+
+
+qed_goal "stream_ind2" thy
+"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \
+\   !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\
+\ |] ==> P x" (fn prems => [
+	rtac (stream.reach RS subst) 1,
+	rtac (adm_impl_admw RS wfix_ind) 1,
+	rtac adm_subst 1,
+	cont_tacR 1,
+	resolve_tac prems 1,
+	rtac allI 1,
+	rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1,
+	resolve_tac prems 1,
+	eresolve_tac prems 1,
+	eresolve_tac prems 1, atac 1, atac 1]);
+
+
+(* ----------------------------------------------------------------------- *)
+(* simplify use of coinduction                                             *)
+(* ----------------------------------------------------------------------- *)
+
+section "coinduction";
+
+qed_goalw "stream_coind_lemma2" thy [stream.bisim_def]
+"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 &  R (rt`s1) (rt`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 "x = UU & x' = 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","ft`x")] exI 1),
+	(res_inst_tac [("x","rt`x")] exI 1),
+	(res_inst_tac [("x","rt`x'")] exI 1),
+	(rtac conjI 1),
+	(etac ft_defin 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
+	(eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1),
+	(simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
+	(res_inst_tac [("x","ft`x'")] exI 1),
+	(res_inst_tac [("x","rt`x")] exI 1),
+	(res_inst_tac [("x","rt`x'")] exI 1),
+	(rtac conjI 1),
+	(etac ft_defin 1),
+	(asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
+	(res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1),
+	(etac sym 1),
+	(simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1)
+	]);
+
+(* ----------------------------------------------------------------------- *)
+(* theorems about stream_finite                                            *)
+(* ----------------------------------------------------------------------- *)
+
+section "stream_finite";
+
+qed_goalw "stream_finite_UU" thy [stream.finite_def] "stream_finite UU" 
+	(fn prems => [
+	(rtac exI 1),
+	(simp_tac (HOLCF_ss addsimps stream.rews) 1)]);
+
+qed_goal "stream_finite_UU_rev" thy  "~  stream_finite s ==> s ~= UU"  (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac contrapos 1),
+	(hyp_subst_tac  1),
+	(rtac stream_finite_UU 1)
+	]);
+
+qed_goalw "stream_finite_lemma1" thy [stream.finite_def]
+ "stream_finite xs ==> stream_finite (x && xs)" (fn prems => [
+	(cut_facts_tac prems 1),
+	(etac exE 1),
+	(rtac exI 1),
+	(etac stream_take_lemma4 1)
+	]);
+
+qed_goalw "stream_finite_lemma2" thy [stream.finite_def]
+ "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac exE 1),
+	(rtac exI 1),
+	(etac stream_take_lemma3 1),
+	(atac 1)
+	]);
+
+qed_goal "stream_finite_rt_eq" thy "stream_finite (rt`s) = stream_finite s"
+	(fn _ => [
+	stream_case_tac "s" 1,
+	 simp_tac (HOL_ss addsimps stream_finite_UU::stream.sel_rews) 1,
+	asm_simp_tac (HOL_ss addsimps stream.sel_rews) 1,
+	fast_tac (HOL_cs addIs [stream_finite_lemma1] 
+			 addDs [stream_finite_lemma2]) 1]);
+
+qed_goal_spec_mp "stream_finite_less" thy 
+ "stream_finite s ==> !t. t<<s --> stream_finite t" (fn prems => [
+	cut_facts_tac prems 1,
+	eres_inst_tac [("x","s")] stream_finite_ind 1,
+	 strip_tac 1, dtac UU_I 1,
+	 asm_simp_tac (HOLCF_ss addsimps [stream_finite_UU]) 1,
+	strip_tac 1,
+	asm_full_simp_tac (HOL_ss addsimps [stream_prefix']) 1,
+	fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]);
+
+qed_goal "adm_not_stream_finite" thy "adm (%x. ~  stream_finite x)" (fn _ => [
+	rtac admI 1,
+	dtac spec 1,
+	etac contrapos 1,
+	dtac stream_finite_less 1,
+	 etac is_ub_thelub 1,
+	atac 1]);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Stream.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,15 @@
+(*  Title: 	FOCUS/Stream.thy
+    ID:         $ $
+    Author: 	Franz Regensburger, David von Oheimb
+    Copyright   1993, 1995 Technische Universitaet Muenchen
+
+general Stream domain
+*)
+
+Stream = HOLCF + 
+
+domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (cinfixr 65)
+
+end
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Witness.ML	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,132 @@
+open Witness;
+
+(* -------------------------------------------------------------------- *)
+(* classes cplus, cminus, ctimes, cdiv introduce 
+   characteristic constants  o+ o- o* o/
+
+	"bullet":: "void -> void -> void"
+
+   is the witness for o+ o- o* o/	
+
+   No characteristic axioms are to be checked
+*)
+
+(* -------------------------------------------------------------------- *)
+(* classes per and qpo introduce characteristic constants
+	".="	:: "'a::per -> 'a -> tr"		(cinfixl 55)
+	".<="	:: "'a::qpo -> 'a -> tr"		(cinfixl 55)
+
+   The witness for these is 
+
+	"cric"	:: "void -> void -> tr"			(cinfixl 55)
+
+   the classes equiv, eq, qlinear impose additional axioms
+*)
+
+(* -------------------------------------------------------------------- *)
+(* 
+
+characteristic axioms of class per:
+
+strict_per	"(UU .= x) = UU & (x .= UU) = UU"
+total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
+flat_per	"flat (UU::'a::per)"
+
+sym_per		"(x .= y) = (y .= x)"
+trans_per	"[|(x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
+
+   --------------------------------------------------------------------
+
+characteristic axioms of class equiv:
+
+refl_per	"[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"
+
+   --------------------------------------------------------------------
+
+characteristic axioms of class eq:
+
+weq	"[|(x::'a::eq) ~= UU; y ~= UU|] ==> (x = y --> (x .= y)=TT) & (x ~= y --> Çx .= yÈ)"
+
+
+   --------------------------------------------------------------------
+
+characteristic axioms of class qpo:
+
+strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
+total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
+
+refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
+antisym_qpo	"[|(x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT"
+trans_qpo	"[|(x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
+antisym_qpo_rev	" (x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
+
+   --------------------------------------------------------------------
+
+characteristic axioms of class qlinear:
+
+qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT | (y .<= x)=TT "
+
+*)
+
+(* strict_per, strict_qpo *)
+val prems = goal thy "(UU circ x) = UU & (x circ UU) = UU";
+by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
+result();
+
+(* total_per, total_qpo *)
+val prems = goal thy "[|x ~= UU; y ~= UU|] ==> (x circ y) ~= UU";
+by (cut_facts_tac prems 1);
+by (etac notE 1);
+by (rtac unique_void2 1);
+result();
+
+(* flat_per *)
+
+val prems = goal thy "flat (UU::void)";
+by (rtac flat_void 1);
+result();
+
+(* sym_per *)  
+val prems = goal thy "(x circ y) = (y circ x)";
+by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
+result();
+
+(* trans_per, trans_qpo *)
+val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT |] ==> (x bullet z)=TT";
+by (cut_facts_tac prems 1);
+by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
+result();
+
+(* refl_per *)
+val prems = goal thy "[|(x::void) ~= UU|] ==> (x bullet x)=TT";
+by (cut_facts_tac prems 1);
+by (etac notE 1);
+by (rtac unique_void2 1);
+result();
+
+(* weq *)
+val prems = goal thy 
+	"[|(x::void) ~= UU; y ~= UU|] ==> (x = y --> (x bullet y)=TT) & (x ~= y --> (x bullet y)=FF)";
+by (cut_facts_tac prems 1);
+by (etac notE 1);
+by (rtac unique_void2 1);
+result();
+
+(* antisym_qpo *)
+val prems = goal thy "[|(x bullet y)=TT; (y bullet x)=TT |] ==> (x bullet y)=TT";
+by (cut_facts_tac prems 1);
+by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
+result();
+
+(* antisym_qpo_rev *)
+val prems = goal thy "(x bullet y)=TT ==> (x bullet y)=TT & (y bullet x)=TT";
+by (cut_facts_tac prems 1);
+by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
+
+(* qlinear *)
+val prems = goal thy 
+	"[|(x::void) ~= UU; y ~= UU|] ==> (x bullet y)=TT | (y bullet x)=TT ";
+by (cut_facts_tac prems 1);
+by (etac notE 1);
+by (rtac unique_void2 1);
+result();

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Witness.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,29 @@
+(*  Title:      FOCUS/Witness.thy
+    ID:         $ $
+    Author:     Franz Regensburger
+    Copyright   1995 Technical University Munich
+
+Witnesses for introduction of type cleasse in theory Classlib
+
+The 8bit package is needed for this theory
+
+The type void of HOLCF/Void.thy is a witness for all the introduced classes.
+
+the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
+the trivial instance for .= and .<=  is LAM x y.(UU::tr)
+
+*)
+
+Witness = HOLCF +
+
+ops curried 
+	"circ"	:: "void -> void -> void"		(cinfixl 65)
+	"bullet":: "void -> void -> tr"			(cinfixl 55)
+
+defs 
+
+circ_def	"(op circ) Ú (LAM x y.UU)"
+
+bullet_def	"(op bullet) Ú (LAM x y.UU)"
+
+end