author | wenzelm |
Tue, 06 May 1997 15:27:35 +0200 | |
changeset 3118 | 24dae6222579 |
parent 3057 | a5a42ff18a40 |
child 3505 | 1cb4ea47d967 |
permissions | -rw-r--r-- |
wenzelm@2500 | 1 |
# |
wenzelm@2500 | 2 |
# $Id$ |
wenzelm@2500 | 3 |
# |
wenzelm@2500 | 4 |
# IsaMakefile for ZF |
wenzelm@2500 | 5 |
# |
wenzelm@2500 | 6 |
|
wenzelm@2500 | 7 |
#### Base system |
wenzelm@2500 | 8 |
|
wenzelm@3118 | 9 |
OUT = $(ISABELLE_OUTPUT) |
wenzelm@2500 | 10 |
|
wenzelm@2500 | 11 |
NAMES = ZF upair subset pair domrange \ |
wenzelm@2500 | 12 |
func AC equalities Bool \ |
wenzelm@2500 | 13 |
Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \ |
wenzelm@2500 | 14 |
constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \ |
wenzelm@2500 | 15 |
WF Order Ordinal Epsilon Arith Univ \ |
wenzelm@2500 | 16 |
QUniv Datatype OrderArith OrderType \ |
wenzelm@2500 | 17 |
Cardinal CardinalArith Cardinal_AC InfDatatype \ |
wenzelm@2500 | 18 |
Zorn Nat Finite List |
wenzelm@2500 | 19 |
|
wenzelm@2500 | 20 |
FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \ |
wenzelm@2500 | 21 |
$(NAMES:%=%.thy) $(NAMES:%=%.ML) |
wenzelm@2500 | 22 |
|
wenzelm@2500 | 23 |
$(OUT)/ZF: $(OUT)/FOL $(FILES) |
wenzelm@3057 | 24 |
@$(ISATOOL) usedir -b $(OUT)/FOL ZF |
wenzelm@2500 | 25 |
@chmod -w $@ |
wenzelm@2500 | 26 |
|
wenzelm@2500 | 27 |
$(OUT)/FOL: |
wenzelm@2500 | 28 |
@cd ../FOL; $(ISATOOL) make |
wenzelm@2500 | 29 |
|
wenzelm@2500 | 30 |
|
wenzelm@2500 | 31 |
|
wenzelm@2500 | 32 |
#### Tests and examples |
wenzelm@2500 | 33 |
|
wenzelm@2500 | 34 |
## IMP-semantics example |
wenzelm@2500 | 35 |
|
wenzelm@2500 | 36 |
IMP_NAMES = Com Denotation Equiv |
wenzelm@2500 | 37 |
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
wenzelm@2500 | 38 |
|
wenzelm@2500 | 39 |
IMP: $(OUT)/ZF $(IMP_FILES) |
wenzelm@2828 | 40 |
@$(ISATOOL) usedir $(OUT)/ZF IMP |
wenzelm@2500 | 41 |
|
wenzelm@2500 | 42 |
|
wenzelm@2500 | 43 |
## Coinduction example |
wenzelm@2500 | 44 |
|
wenzelm@2500 | 45 |
COIND_NAMES = ECR MT Map Static Types Values |
wenzelm@2500 | 46 |
|
wenzelm@2500 | 47 |
COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \ |
wenzelm@2500 | 48 |
$(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML) |
wenzelm@2500 | 49 |
|
wenzelm@2500 | 50 |
Coind: $(OUT)/ZF $(COIND_FILES) |
wenzelm@2828 | 51 |
@$(ISATOOL) usedir $(OUT)/ZF Coind |
wenzelm@2500 | 52 |
|
wenzelm@2500 | 53 |
|
wenzelm@2500 | 54 |
## AC examples |
wenzelm@2500 | 55 |
|
wenzelm@2500 | 56 |
AC_NAMES = AC_Equiv Cardinal_aux \ |
wenzelm@2500 | 57 |
AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \ |
wenzelm@2500 | 58 |
DC DC_lemmas HH Hartog WO1_AC \ |
wenzelm@2500 | 59 |
WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun |
wenzelm@2500 | 60 |
|
wenzelm@2500 | 61 |
AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \ |
wenzelm@2500 | 62 |
AC/AC2_AC6.ML AC/AC7_AC9.ML \ |
wenzelm@2500 | 63 |
AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \ |
wenzelm@2500 | 64 |
$(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML) |
wenzelm@2500 | 65 |
|
wenzelm@2500 | 66 |
AC: $(OUT)/ZF $(AC_FILES) |
wenzelm@2828 | 67 |
@$(ISATOOL) usedir $(OUT)/ZF AC |
wenzelm@2500 | 68 |
|
wenzelm@2500 | 69 |
|
wenzelm@2500 | 70 |
## Residuals example |
wenzelm@2500 | 71 |
|
wenzelm@2500 | 72 |
RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \ |
wenzelm@2500 | 73 |
Cube Residuals Terms |
wenzelm@2500 | 74 |
|
wenzelm@2500 | 75 |
RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML) |
wenzelm@2500 | 76 |
|
wenzelm@2500 | 77 |
Resid: $(OUT)/ZF $(RESID_FILES) |
wenzelm@2828 | 78 |
@$(ISATOOL) usedir $(OUT)/ZF Resid |
wenzelm@2500 | 79 |
|
wenzelm@2500 | 80 |
|
wenzelm@2500 | 81 |
## Miscellaneous examples |
wenzelm@2500 | 82 |
|
wenzelm@2500 | 83 |
EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \ |
wenzelm@2500 | 84 |
Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit |
wenzelm@2500 | 85 |
|
wenzelm@2500 | 86 |
EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
wenzelm@2500 | 87 |
|
wenzelm@2500 | 88 |
ex: $(OUT)/ZF $(EX_FILES) |
wenzelm@2828 | 89 |
@$(ISATOOL) usedir $(OUT)/ZF ex |
wenzelm@2500 | 90 |
|
wenzelm@2500 | 91 |
|
wenzelm@2500 | 92 |
## Full test |
wenzelm@2500 | 93 |
|
wenzelm@2500 | 94 |
test: $(OUT)/ZF IMP Coind AC Resid ex |
wenzelm@2500 | 95 |
echo 'Test examples ran successfully' > test |
wenzelm@2500 | 96 |
|
wenzelm@2500 | 97 |
.PRECIOUS: $(OUT)/FOL $(OUT)/ZF |