# HG changeset patch # User wenzelm # Date 877344351 -7200 # Node ID d52a49a7d8f3a11c2b454821f36be1882ad9da99 # Parent e9d5bcae8351789413d575a8d242aa0a75abea1f removed Dlist; diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Mon Oct 20 11:53:42 1997 +0200 +++ b/src/HOLCF/IsaMakefile Mon Oct 20 12:45:51 1997 +0200 @@ -89,6 +89,7 @@ IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES) @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP + ## IMP IMP_THYS = IMP/Denotational.thy @@ -97,20 +98,23 @@ IMP: $(OUT)/HOLCF $(IMP_FILES) @$(ISATOOL) usedir $(OUT)/HOLCF IMP + ## Miscellaneous examples -EX_THYS = ex/Dnat.thy ex/Dlist.thy ex/Stream.thy \ +EX_THYS = ex/Dnat.thy ex/Stream.thy \ ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \ ex/Hoare.thy ex/Loop.thy EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) -EX: ex/ROOT.ML $(EX_FILES) +ex: ex/ROOT.ML $(EX_FILES) @$(ISATOOL) usedir $(OUT)/HOLCF ex + ## Full test -test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX +test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex echo 'Test examples ran successfully' > test + .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/ex/Dlist.ML --- a/src/HOLCF/ex/Dlist.ML Mon Oct 20 11:53:42 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -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) - ]); diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/ex/Dlist.thy --- a/src/HOLCF/ex/Dlist.thy Mon Oct 20 11:53:42 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -(* 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) - - -consts - -lmap :: "('a -> 'b) -> 'a dlist -> 'b dlist" -lmem :: "('a::eq) -> 'a dlist -> tr" - -defs - -lmap_def "lmap == fix`(LAM h f s. case s of dnil => dnil - | x ## xs => f`x ## h`f`xs)" - -lmem_def "lmem == fix`(LAM h e l. case l of dnil => FF - | x ## xs => If e Ù x then TT else h`e`xs fi)" - -end diff -r e9d5bcae8351 -r d52a49a7d8f3 src/HOLCF/ex/ROOT.ML --- a/src/HOLCF/ex/ROOT.ML Mon Oct 20 11:53:42 1997 +0200 +++ b/src/HOLCF/ex/ROOT.ML Mon Oct 20 12:45:51 1997 +0200 @@ -11,9 +11,7 @@ writeln"Root file for HOLCF examples"; proof_timing := true; -time_use_thy "Classlib"; time_use_thy "Dnat"; -time_use_thy "Dlist"; time_use_thy "Stream"; time_use_thy "Dagstuhl"; time_use_thy "Focus_ex";