author | paulson |
Tue, 20 May 1997 11:33:45 +0200 | |
changeset 3232 | 19a2b853ba7b |
parent 3222 | 726a9b069947 |
child 3294 | 4c73b6508f53 |
permissions | -rw-r--r-- |
wenzelm@2448 | 1 |
# |
wenzelm@2448 | 2 |
# $Id$ |
wenzelm@2448 | 3 |
# |
wenzelm@2448 | 4 |
# IsaMakefile for HOL |
wenzelm@2448 | 5 |
# |
wenzelm@2448 | 6 |
|
wenzelm@2448 | 7 |
#### Base system |
wenzelm@2448 | 8 |
|
wenzelm@3118 | 9 |
OUT = $(ISABELLE_OUTPUT) |
wenzelm@2448 | 10 |
|
paulson@3195 | 11 |
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \ |
nipkow@3025 | 12 |
mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \ |
nipkow@3222 | 13 |
Sexp Univ List RelPow Option |
wenzelm@2448 | 14 |
|
paulson@3232 | 15 |
PROVERS = hypsubst.ML classical.ML blast.ML \ |
paulson@3232 | 16 |
simplifier.ML splitter.ML nat_transitive.ML |
paulson@3232 | 17 |
|
paulson@3232 | 18 |
TFL = dcterm.sml mask.sig mask.sml post.sml rules.new.sml rules.sig \ |
paulson@3232 | 19 |
sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml \ |
paulson@3232 | 20 |
usyntax.sig usyntax.sml utils.sig utils.sml |
paulson@3232 | 21 |
|
wenzelm@2448 | 22 |
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \ |
wenzelm@2448 | 23 |
ind_syntax.ML cladata.ML simpdata.ML \ |
wenzelm@2448 | 24 |
typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \ |
paulson@3232 | 25 |
$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \ |
paulson@3232 | 26 |
$(PROVERS:%=../Provers/%) |
wenzelm@2448 | 27 |
|
wenzelm@2448 | 28 |
$(OUT)/HOL: $(OUT)/Pure $(FILES) |
wenzelm@2826 | 29 |
@$(ISATOOL) usedir -b $(OUT)/Pure HOL |
wenzelm@2448 | 30 |
@chmod -w $@ |
wenzelm@2448 | 31 |
|
wenzelm@2448 | 32 |
$(OUT)/Pure: |
wenzelm@2473 | 33 |
@cd ../Pure; $(ISATOOL) make |
wenzelm@2448 | 34 |
|
wenzelm@2448 | 35 |
|
wenzelm@2473 | 36 |
#### Tests and examples |
wenzelm@2473 | 37 |
|
paulson@3125 | 38 |
## Inductive definitions: simple examples |
paulson@3125 | 39 |
|
paulson@3125 | 40 |
INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult |
paulson@3125 | 41 |
|
paulson@3125 | 42 |
INDUCT_FILES = Induct/ROOT.ML \ |
paulson@3125 | 43 |
$(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML) |
paulson@3125 | 44 |
|
paulson@3125 | 45 |
Induct: $(OUT)/HOL $(INDUCT_FILES) |
paulson@3125 | 46 |
@$(ISATOOL) usedir $(OUT)/HOL Induct |
paulson@3125 | 47 |
|
paulson@3125 | 48 |
|
wenzelm@2448 | 49 |
## IMP-semantics example |
wenzelm@2448 | 50 |
|
wenzelm@2448 | 51 |
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC |
wenzelm@2448 | 52 |
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
wenzelm@2448 | 53 |
|
wenzelm@2448 | 54 |
IMP: $(OUT)/HOL $(IMP_FILES) |
wenzelm@2826 | 55 |
@$(ISATOOL) usedir $(OUT)/HOL IMP |
wenzelm@2448 | 56 |
|
wenzelm@2448 | 57 |
|
wenzelm@2448 | 58 |
## Hoare logic |
wenzelm@2448 | 59 |
|
wenzelm@2448 | 60 |
Hoare_NAMES = Hoare Arith2 Examples |
wenzelm@2448 | 61 |
Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \ |
wenzelm@2448 | 62 |
$(Hoare_NAMES:%=Hoare/%.ML) |
wenzelm@2448 | 63 |
|
wenzelm@2448 | 64 |
Hoare: $(OUT)/HOL $(Hoare_FILES) |
wenzelm@2826 | 65 |
@$(ISATOOL) usedir $(OUT)/HOL Hoare |
wenzelm@2448 | 66 |
|
wenzelm@2448 | 67 |
|
wenzelm@2448 | 68 |
## The integers in HOL |
wenzelm@2448 | 69 |
|
wenzelm@2448 | 70 |
INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing |
wenzelm@2448 | 71 |
|
wenzelm@2448 | 72 |
INTEG_FILES = Integ/ROOT.ML \ |
wenzelm@2448 | 73 |
$(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) |
wenzelm@2448 | 74 |
|
wenzelm@2448 | 75 |
Integ: $(OUT)/HOL $(INTEG_FILES) |
wenzelm@2826 | 76 |
@$(ISATOOL) usedir $(OUT)/HOL Integ |
wenzelm@2448 | 77 |
|
wenzelm@2448 | 78 |
|
mueller@3079 | 79 |
## I/O Automata (meta theory only) |
wenzelm@2448 | 80 |
|
wenzelm@2448 | 81 |
|
mueller@3079 | 82 |
IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \ |
mueller@3079 | 83 |
IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML |
wenzelm@2448 | 84 |
|
mueller@3079 | 85 |
IOA: $(OUT)/HOL $(IOA_FILES) |
mueller@3079 | 86 |
@$(ISATOOL) usedir $(OUT)/HOL IOA |
wenzelm@2448 | 87 |
|
wenzelm@2448 | 88 |
|
wenzelm@2448 | 89 |
## Authentication & Security Protocols |
wenzelm@2448 | 90 |
|
wenzelm@2448 | 91 |
Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \ |
wenzelm@2473 | 92 |
Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public |
wenzelm@2448 | 93 |
|
wenzelm@2448 | 94 |
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) |
wenzelm@2448 | 95 |
|
wenzelm@2448 | 96 |
Auth: $(OUT)/HOL $(AUTH_FILES) |
wenzelm@2826 | 97 |
@$(ISATOOL) usedir $(OUT)/HOL Auth |
wenzelm@2448 | 98 |
|
wenzelm@2448 | 99 |
|
mueller@3218 | 100 |
## Modelchecker invocation |
mueller@3218 | 101 |
|
mueller@3218 | 102 |
MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \ |
mueller@3218 | 103 |
Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \ |
mueller@3218 | 104 |
Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML |
mueller@3218 | 105 |
|
mueller@3218 | 106 |
Modelcheck: $(OUT)/HOL $(MC_FILES) |
mueller@3218 | 107 |
@$(ISATOOL) usedir $(OUT)/HOL Modelcheck |
mueller@3218 | 108 |
|
mueller@3218 | 109 |
|
wenzelm@2448 | 110 |
## Properties of substitutions |
wenzelm@2448 | 111 |
|
paulson@3195 | 112 |
SUBST_NAMES = AList Subst Unifier UTerm Unify |
wenzelm@2448 | 113 |
|
wenzelm@2448 | 114 |
SUBST_FILES = Subst/ROOT.ML \ |
wenzelm@2448 | 115 |
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
wenzelm@2448 | 116 |
|
wenzelm@2448 | 117 |
Subst: $(OUT)/HOL $(SUBST_FILES) |
wenzelm@2826 | 118 |
@$(ISATOOL) usedir $(OUT)/HOL Subst |
wenzelm@2448 | 119 |
|
wenzelm@2448 | 120 |
|
wenzelm@2448 | 121 |
## Confluence of Lambda-calculus |
wenzelm@2448 | 122 |
|
wenzelm@2448 | 123 |
LAMBDA_NAMES = Lambda ParRed Commutation Eta |
wenzelm@2448 | 124 |
|
wenzelm@2448 | 125 |
LAMBDA_FILES = Lambda/ROOT.ML \ |
wenzelm@2448 | 126 |
$(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) |
wenzelm@2448 | 127 |
|
wenzelm@2448 | 128 |
Lambda: $(OUT)/HOL $(LAMBDA_FILES) |
wenzelm@2826 | 129 |
@$(ISATOOL) usedir $(OUT)/HOL Lambda |
wenzelm@2448 | 130 |
|
wenzelm@2448 | 131 |
|
nipkow@2527 | 132 |
## Type inference without let |
wenzelm@2448 | 133 |
|
nipkow@2527 | 134 |
W0_NAMES = I Maybe MiniML Type W |
nipkow@2527 | 135 |
|
nipkow@2527 | 136 |
W0_FILES = W0/ROOT.ML \ |
nipkow@2527 | 137 |
$(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) |
nipkow@2527 | 138 |
|
nipkow@2527 | 139 |
W0: $(OUT)/HOL $(W0_FILES) |
wenzelm@2826 | 140 |
@$(ISATOOL) usedir $(OUT)/HOL W0 |
nipkow@2527 | 141 |
|
nipkow@2527 | 142 |
|
nipkow@2527 | 143 |
## Type inference with let |
nipkow@2527 | 144 |
|
nipkow@2527 | 145 |
MINIML_NAMES = Generalize Instance Maybe MiniML Type W |
wenzelm@2448 | 146 |
|
wenzelm@2448 | 147 |
MINIML_FILES = MiniML/ROOT.ML \ |
wenzelm@2448 | 148 |
$(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) |
wenzelm@2448 | 149 |
|
wenzelm@2448 | 150 |
MiniML: $(OUT)/HOL $(MINIML_FILES) |
wenzelm@2826 | 151 |
@$(ISATOOL) usedir $(OUT)/HOL MiniML |
wenzelm@2448 | 152 |
|
wenzelm@2448 | 153 |
|
wenzelm@2448 | 154 |
## Lexical analysis |
wenzelm@2448 | 155 |
|
wenzelm@2448 | 156 |
LEX_FILES = Auto AutoChopper Chopper Prefix |
wenzelm@2448 | 157 |
|
wenzelm@2448 | 158 |
LEX_FILES = Lex/ROOT.ML \ |
wenzelm@2448 | 159 |
$(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) |
wenzelm@2448 | 160 |
|
wenzelm@2448 | 161 |
Lex: $(OUT)/HOL $(LEX_FILES) |
wenzelm@2826 | 162 |
@$(ISATOOL) usedir $(OUT)/HOL Lex |
wenzelm@2448 | 163 |
|
wenzelm@2448 | 164 |
|
wenzelm@2545 | 165 |
## Axiomatic type classes examples |
wenzelm@2545 | 166 |
|
wenzelm@2545 | 167 |
AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \ |
wenzelm@2545 | 168 |
GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy |
wenzelm@2545 | 169 |
|
wenzelm@2545 | 170 |
AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \ |
wenzelm@2545 | 171 |
LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \ |
wenzelm@2545 | 172 |
Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \ |
wenzelm@2545 | 173 |
Order.ML Order.thy ROOT.ML tools.ML |
wenzelm@2545 | 174 |
|
wenzelm@2545 | 175 |
AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \ |
wenzelm@2545 | 176 |
MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \ |
wenzelm@2545 | 177 |
ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ |
wenzelm@2545 | 178 |
Xor.ML Xor.thy |
wenzelm@2545 | 179 |
|
wenzelm@2545 | 180 |
AXCLASSES_FILES = AxClasses/ROOT.ML \ |
wenzelm@2545 | 181 |
$(AXC_GROUP_FILES:%=AxClasses/Group/%) \ |
wenzelm@2545 | 182 |
$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \ |
wenzelm@2545 | 183 |
$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) |
wenzelm@2545 | 184 |
|
wenzelm@2545 | 185 |
AxClasses: $(OUT)/HOL $(AXCLASSES_FILES) |
wenzelm@2826 | 186 |
@$(ISATOOL) usedir $(OUT)/HOL AxClasses |
wenzelm@2827 | 187 |
@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group |
wenzelm@2827 | 188 |
@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice |
wenzelm@2827 | 189 |
@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial |
wenzelm@2545 | 190 |
|
wenzelm@2545 | 191 |
|
slotosch@2909 | 192 |
## Higher-order quotients and example fractionals |
wenzelm@2900 | 193 |
|
slotosch@2909 | 194 |
QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \ |
slotosch@2909 | 195 |
Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \ |
slotosch@2909 | 196 |
Quot/FRACT.thy Quot/FRACT.ML |
wenzelm@2900 | 197 |
Quot: $(OUT)/HOL $(QUOT_FILES) |
wenzelm@2900 | 198 |
@$(ISATOOL) usedir $(OUT)/HOL Quot |
wenzelm@2900 | 199 |
|
wenzelm@2900 | 200 |
|
wenzelm@2448 | 201 |
## Miscellaneous examples |
wenzelm@2448 | 202 |
|
paulson@3232 | 203 |
EX_NAMES = String BT InSort Qsort Puzzle Primes NatSum MT |
wenzelm@2448 | 204 |
|
wenzelm@2448 | 205 |
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
wenzelm@2448 | 206 |
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
wenzelm@2448 | 207 |
|
wenzelm@2448 | 208 |
ex: $(OUT)/HOL $(EX_FILES) |
wenzelm@2826 | 209 |
@$(ISATOOL) usedir $(OUT)/HOL ex |
wenzelm@2448 | 210 |
|
wenzelm@2448 | 211 |
|
wenzelm@2448 | 212 |
## Full test |
wenzelm@2448 | 213 |
|
oheimb@2635 | 214 |
test: $(OUT)/HOL \ |
mueller@3218 | 215 |
Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda \ |
paulson@3125 | 216 |
W0 MiniML IOA AxClasses Quot ex |
wenzelm@2448 | 217 |
echo 'Test examples ran successfully' > test |
wenzelm@2448 | 218 |
|
wenzelm@2448 | 219 |
|
wenzelm@2448 | 220 |
.PRECIOUS: $(OUT)/Pure $(OUT)/HOL |