moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex,
marked the remaining files as obsolete (new versions in HOLCF/ex)

--- a/src/HOLCF/explicit_domains/Coind.ML	Fri Jan 31 16:39:27 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(*  Title:      HOLCF/Coind.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-*)
-
-open Coind;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties                                             *)
-(* ------------------------------------------------------------------------- *)
-
-
-val nats_def2 = fix_prover2 Coind.thy nats_def 
-        "nats = scons`dzero`(smap`dsucc`nats)";
-
-val from_def2 = fix_prover2 Coind.thy from_def 
-        "from = (LAM n.scons`n`(from`(dsucc`n)))";
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-
-val from = prove_goal Coind.thy "from`n = scons`n`(from`(dsucc`n))"
- (fn prems =>
-        [
-        (rtac trans 1),
-        (stac from_def2 1),
-        (Simp_tac 1),
-        (rtac refl 1)
-        ]);
-
-
-val from1 = prove_goal Coind.thy "from`UU = UU"
- (fn prems =>
-        [
-        (rtac trans 1),
-        (stac from 1),
-        (resolve_tac  stream_constrdef 1),
-        (rtac refl 1)
-        ]);
-
-val coind_rews = 
-        [iterator1, iterator2, iterator3, smap1, smap2,from1];
-
-
-(* ------------------------------------------------------------------------- *)
-(* the example                                                               *)
-(* prove:        nats = from`dzero                                           *)
-(* ------------------------------------------------------------------------- *)
-
-
-val coind_lemma1 = prove_goal Coind.thy "iterator`n`(smap`dsucc)`nats =\
-\                scons`n`(iterator`(dsucc`n)`(smap`dsucc)`nats)"
- (fn prems =>
-        [
-        (res_inst_tac [("s","n")] dnat_ind 1),
-        (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1),
-        (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1),
-        (rtac trans 1),
-        (rtac nats_def2 1),
-        (simp_tac (!simpset addsimps (coind_rews @ dnat_rews)) 1),
-        (rtac trans 1),
-        (etac iterator3 1),
-        (rtac trans 1),
-        (Asm_simp_tac 1),
-        (rtac trans 1),
-        (etac smap2 1),
-        (rtac cfun_arg_cong 1),
-        (asm_simp_tac (!simpset addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
-        ]);
-
-
-val nats_eq_from = prove_goal Coind.thy "nats = from`dzero"
- (fn prems =>
-        [
-        (res_inst_tac [("R",
-"% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1),
-        (res_inst_tac [("x","dzero")] exI 2),
-        (asm_simp_tac (!simpset addsimps coind_rews) 2),
-        (rewtac stream_bisim_def),
-        (strip_tac 1),
-        (etac exE 1),
-        (case_tac "n=UU" 1),
-        (rtac disjI1 1),
-        (asm_simp_tac (!simpset addsimps coind_rews) 1),
-        (rtac disjI2 1),
-        (etac conjE 1),
-        (hyp_subst_tac 1),
-        (res_inst_tac [("x","n")] exI 1),
-        (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1),
-        (res_inst_tac [("x","from`(dsucc`n)")] exI 1),
-        (etac conjI 1),
-        (rtac conjI 1),
-        (rtac coind_lemma1 1),
-        (rtac conjI 1),
-        (rtac from 1),
-        (res_inst_tac [("x","dsucc`n")] exI 1),
-        (fast_tac HOL_cs 1)
-        ]);
-
-(* another proof using stream_coind_lemma2 *)
-
-val nats_eq_from = prove_goal Coind.thy "nats = from`dzero"
- (fn prems =>
-        [
-        (res_inst_tac [("R","% p q.? n. p = \
-\       iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1),
-        (rtac stream_coind_lemma2 1),
-        (strip_tac 1),
-        (etac exE 1),
-        (case_tac "n=UU" 1),
-        (asm_simp_tac (!simpset addsimps coind_rews) 1),
-        (res_inst_tac [("x","UU::dnat")] exI 1),
-        (simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1),
-        (etac conjE 1),
-        (hyp_subst_tac 1),
-        (rtac conjI 1),
-        (stac coind_lemma1 1),
-        (stac from 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (res_inst_tac [("x","dsucc`n")] exI 1),
-        (rtac conjI 1),
-        (rtac trans 1),
-        (stac coind_lemma1 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (rtac refl 1),
-        (rtac trans 1),
-        (stac from 1),
-        (asm_simp_tac (!simpset addsimps stream_rews) 1),
-        (rtac refl 1),
-        (res_inst_tac [("x","dzero")] exI 1),
-        (asm_simp_tac (!simpset addsimps coind_rews) 1)
-        ]);
-

--- a/src/HOLCF/explicit_domains/Coind.thy	Fri Jan 31 16:39:27 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      HOLCF/Coind.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Example for co-induction on streams
-*)
-
-Coind = Stream2 +
-
-
-consts
-
-        nats            :: "dnat stream"
-        from            :: "dnat -> dnat stream"
-
-defs
-        nats_def        "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
-
-        from_def        "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
-
-end
-
-(*
-                smap`f`UU = UU
-      x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs)
-
-                nats = scons`dzero`(smap`dsucc`nats)
-
-                from`n = scons`n`(from`(dsucc`n))
-*)
-
-

--- a/src/HOLCF/explicit_domains/Dagstuhl.ML	Fri Jan 31 16:39:27 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(* $Id$ *)
-
-open Dagstuhl;
-
-val YS_def2  = fix_prover2 Dagstuhl.thy  YS_def  "YS = scons`y`YS";
-val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = scons`y`(scons`y`YYS)";
-
-
-val prems = goal Dagstuhl.thy "YYS << scons`y`YYS";
-by (rewtac YYS_def);
-by (rtac fix_ind 1);
-by (resolve_tac adm_thms 1);
-by (cont_tacR 1);
-by (rtac minimal 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 "scons`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 "scons`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 (rewtac YS_def);
-by (rtac fix_ind 1);
-by (resolve_tac adm_thms 1);
-by (cont_tacR 1);
-by (rtac minimal 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);
-

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

--- a/src/HOLCF/explicit_domains/Dlist.thy	Fri Jan 31 16:39:27 1997 +0100
+++ b/src/HOLCF/explicit_domains/Dlist.thy	Fri Jan 31 16:51:58 1997 +0100
@@ -4,6 +4,8 @@
     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.

--- a/src/HOLCF/explicit_domains/Dnat.thy	Fri Jan 31 16:39:27 1997 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.thy	Fri Jan 31 16:51:58 1997 +0100
@@ -3,6 +3,8 @@
     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.

--- a/src/HOLCF/explicit_domains/Dnat2.thy	Fri Jan 31 16:39:27 1997 +0100
+++ b/src/HOLCF/explicit_domains/Dnat2.thy	Fri Jan 31 16:51:58 1997 +0100
@@ -3,6 +3,8 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
+NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
+
 Additional constants for dnat
 
 *)

--- a/src/HOLCF/explicit_domains/Focus_ex.ML	Fri Jan 31 16:39:27 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-(*
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1995 Technische Universitaet Muenchen
-
-*)
-
-open Focus_ex;
-
-	Delsimps (ex_simps @ all_simps);
-
-(* 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 (!simpset 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 1);
-by (dtac sym 1);
-by (Asm_simp_tac 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 (!simpset 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 1);
-by (rtac conjI 1);
-by (rtac trans 1);
-by (rtac fix_eq 1);
-by (Simp_tac 1);
-by (strip_tac 1);
-by (rtac fix_least 1);
-by (dtac sym 1);
-back();
-by (Asm_simp_tac 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 (!simpset 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 (etac 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 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 1);
-by (etac sym 1);
-by (rtac allI 1);
-by (Simp_tac 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 (!simpset 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();
-

--- a/src/HOLCF/explicit_domains/Focus_ex.thy	Fri Jan 31 16:39:27 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-(*
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1995 Technische Universitaet Muenchen
-
-*)
-
-(* 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/explicit_domains/ROOT.ML	Fri Jan 31 16:39:27 1997 +0100
+++ b/src/HOLCF/explicit_domains/ROOT.ML	Fri Jan 31 16:51:58 1997 +0100
@@ -16,9 +16,5 @@
 time_use_thy "Stream2";
 time_use_thy "Dlist";
 
-time_use_thy "Coind";
-time_use_thy "Dagstuhl";
-time_use_thy "Focus_ex";
-
 OS.FileSys.chDir "..";
 maketest "END: Root file for HOLCF examples: explicit domain axiomatization";

--- a/src/HOLCF/explicit_domains/Stream.thy	Fri Jan 31 16:39:27 1997 +0100
+++ b/src/HOLCF/explicit_domains/Stream.thy	Fri Jan 31 16:51:58 1997 +0100
@@ -3,6 +3,8 @@
     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
 

--- a/src/HOLCF/explicit_domains/Stream2.thy	Fri Jan 31 16:39:27 1997 +0100
+++ b/src/HOLCF/explicit_domains/Stream2.thy	Fri Jan 31 16:51:58 1997 +0100
@@ -3,6 +3,8 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
+NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
+
 Additional constants for stream
 *)