Changes of HOLCF from Oscar Slotosch:
1. axclass instead of class
* less instead of
less_fun,
less_cfun,
less_sprod,
less_cprod,
less_ssum,
less_up,
less_lift
* @x.!y.x<<y instead of UUU instead of
UU_fun, UU_cfun, ...
* no witness type void needed (eliminated Void.thy.Void.ML)
* inst_<typ>_<class> derived as theorems
2. improved some proves on less_sprod and less_cprod
* eliminated the following theorems
Sprod1.ML: less_sprod1a
Sprod1.ML: less_sprod1b
Sprod1.ML: less_sprod2a
Sprod1.ML: less_sprod2b
Sprod1.ML: less_sprod2c
Sprod2.ML: less_sprod3a
Sprod2.ML: less_sprod3b
Sprod2.ML: less_sprod4b
Sprod2.ML: less_sprod4c
Sprod3.ML: less_sprod5b
Sprod3.ML: less_sprod5c
Cprod1.ML: less_cprod1b
Cprod1.ML: less_cprod2a
Cprod1.ML: less_cprod2b
Cprod1.ML: less_cprod2c
Cprod2.ML: less_cprod3a
Cprod2.ML: less_cprod3b
3. new classes:
* cpo<po,
* chfin<pcpo,
* flat<pcpo,
* derived: flat<chfin
to do: show instances for lift
4. Data Type One
* Used lift for the definition: one = unit lift
* Changed the constant one into ONE
5. Data Type Tr
* Used lift for the definition: tr = bool lift
* adopted definitions of if,andalso,orelse,neg
* only one theory Tr.thy,Tr.ML instead of
Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML
* reintroduced ceils for =TT,=FF
6. typedef
* Using typedef instead of faking type definitions
to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun
7. adopted examples and domain construct to theses changes
These changes eliminated all rules and arities from HOLCF
#
# $Id$
#
# IsaMakefile for HOLCF
#
#### Base system
OUT = $(ISABELLE_OUTPUT_DIR)
THYS = Porder.thy Porder0.thy Pcpo.thy \
Fun1.thy Fun2.thy Fun3.thy \
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
Cprod1.thy Cprod2.thy Cprod3.thy \
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
One.thy Tr.thy\
Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
ONLYTHYS = Lift.thy
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
@chmod -w $@
$(OUT)/HOL:
@cd ../HOL; $(ISATOOL) make
#### Tests and examples
## Miscellaneous examples
EX_THYS = ex/Classlib.thy ex/Witness.thy\
ex/Dnat.thy ex/Dlist.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)
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