removed Dlist;
authorwenzelm
Mon Oct 20 12:45:51 1997 +0200 (1997-10-20)
changeset 3951d52a49a7d8f3
parent 3950 e9d5bcae8351
child 3952 dca1bce88ec8
removed Dlist;
src/HOLCF/IsaMakefile
src/HOLCF/ex/Dlist.ML
src/HOLCF/ex/Dlist.thy
src/HOLCF/ex/ROOT.ML
     1.1 --- a/src/HOLCF/IsaMakefile	Mon Oct 20 11:53:42 1997 +0200
     1.2 +++ b/src/HOLCF/IsaMakefile	Mon Oct 20 12:45:51 1997 +0200
     1.3 @@ -89,6 +89,7 @@
     1.4  IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
     1.5  	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
     1.6  
     1.7 +
     1.8  ## IMP
     1.9  
    1.10  IMP_THYS = IMP/Denotational.thy
    1.11 @@ -97,20 +98,23 @@
    1.12  IMP:	$(OUT)/HOLCF $(IMP_FILES)
    1.13  	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
    1.14  
    1.15 +
    1.16  ## Miscellaneous examples
    1.17  
    1.18 -EX_THYS = ex/Dnat.thy ex/Dlist.thy ex/Stream.thy \
    1.19 +EX_THYS = ex/Dnat.thy ex/Stream.thy \
    1.20  	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \
    1.21  	  ex/Hoare.thy ex/Loop.thy
    1.22  
    1.23  EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    1.24  
    1.25 -EX:	ex/ROOT.ML $(EX_FILES)
    1.26 +ex:	ex/ROOT.ML $(EX_FILES)
    1.27  	@$(ISATOOL) usedir $(OUT)/HOLCF ex
    1.28  
    1.29 +
    1.30  ## Full test
    1.31  
    1.32 -test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX
    1.33 +test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex
    1.34  	echo 'Test examples ran successfully' > test
    1.35  
    1.36 +
    1.37  .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
     2.1 --- a/src/HOLCF/ex/Dlist.ML	Mon Oct 20 11:53:42 1997 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,37 +0,0 @@
     2.4 -open Dlist;
     2.5 -
     2.6 -(* ------------------------------------------------------------------------- *)
     2.7 -(* expand fixed point properties of lmap                                     *)
     2.8 -(* ------------------------------------------------------------------------- *)
     2.9 -
    2.10 -bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def 
    2.11 -        "lmap = (LAM f s. case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
    2.12 -
    2.13 -(* ------------------------------------------------------------------------- *)
    2.14 -(* recursive  properties   of lmap                                           *)
    2.15 -(* ------------------------------------------------------------------------- *)
    2.16 -
    2.17 -qed_goal "lmap1" Dlist.thy "lmap`f`UU = UU"
    2.18 - (fn prems =>
    2.19 -	[
    2.20 -	(rtac (lmap_def2 RS ssubst) 1),
    2.21 -	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
    2.22 -	]);
    2.23 -
    2.24 -qed_goal "lmap2" Dlist.thy "lmap`f`dnil = dnil"
    2.25 - (fn prems =>
    2.26 -	[
    2.27 -	(rtac (lmap_def2 RS ssubst) 1),
    2.28 -	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
    2.29 -	]);
    2.30 -
    2.31 -qed_goal "lmap3" Dlist.thy 
    2.32 -	"[|x~=UU; xs~=UU|] ==> lmap`f`(x##xs) = (f`x)##(lmap`f`xs)"
    2.33 - (fn prems =>
    2.34 -	[
    2.35 -	(cut_facts_tac prems 1),
    2.36 -	(rtac trans 1),
    2.37 -	(rtac (lmap_def2 RS ssubst) 1),
    2.38 -	(asm_simp_tac (HOLCF_ss addsimps dlist.rews) 1),
    2.39 -	(rtac refl 1)
    2.40 -	]);
     3.1 --- a/src/HOLCF/ex/Dlist.thy	Mon Oct 20 11:53:42 1997 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,27 +0,0 @@
     3.4 -(*  Title:      HOLCF/Dlist.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Franz Regensburger
     3.7 -    Copyright   1993 Technische Universitaet Muenchen
     3.8 -
     3.9 -Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
    3.10 -*)
    3.11 -
    3.12 -Dlist = Classlib +
    3.13 -
    3.14 -domain 'a dlist = dnil | "##" (dhd::'a) (dtl::'a dlist) (cinfixr 65)
    3.15 -
    3.16 -
    3.17 -consts
    3.18 -
    3.19 -lmap	:: "('a -> 'b) -> 'a dlist -> 'b dlist"
    3.20 -lmem	:: "('a::eq)  -> 'a dlist -> tr"
    3.21 -
    3.22 -defs
    3.23 -
    3.24 -lmap_def "lmap == fix`(LAM h f s. case s of dnil => dnil
    3.25 -			          | x ## xs => f`x ## h`f`xs)"
    3.26 -
    3.27 -lmem_def "lmem == fix`(LAM h e l. case l of dnil => FF
    3.28 -     	 	  		  | x ## xs => If e  x then TT else h`e`xs fi)"
    3.29 -
    3.30 -end
     4.1 --- a/src/HOLCF/ex/ROOT.ML	Mon Oct 20 11:53:42 1997 +0200
     4.2 +++ b/src/HOLCF/ex/ROOT.ML	Mon Oct 20 12:45:51 1997 +0200
     4.3 @@ -11,9 +11,7 @@
     4.4  writeln"Root file for HOLCF examples";
     4.5  proof_timing := true;
     4.6  
     4.7 -time_use_thy "Classlib";
     4.8  time_use_thy "Dnat";
     4.9 -time_use_thy "Dlist";
    4.10  time_use_thy "Stream";
    4.11  time_use_thy "Dagstuhl";
    4.12  time_use_thy "Focus_ex";