author | wenzelm |
Fri, 19 Dec 1997 10:18:58 +0100 | |
changeset 4447 | b7ee449eb345 |
parent 4289 | 5c1bfefd39b7 |
child 4455 | c0a6ad614fa0 |
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@4447 | 10 |
LOG = $(OUT)/log |
wenzelm@2448 | 11 |
|
paulson@3195 | 12 |
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \ |
nipkow@3025 | 13 |
mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \ |
nipkow@3981 | 14 |
Divides Power Sexp Univ List RelPow Option Map |
wenzelm@2448 | 15 |
|
paulson@3232 | 16 |
PROVERS = hypsubst.ML classical.ML blast.ML \ |
wenzelm@4289 | 17 |
simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML |
paulson@3232 | 18 |
|
paulson@3354 | 19 |
TFL = dcterm.sml post.sml rules.new.sml rules.sig \ |
paulson@3232 | 20 |
sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml \ |
paulson@3232 | 21 |
usyntax.sig usyntax.sml utils.sig utils.sml |
paulson@3232 | 22 |
|
wenzelm@2448 | 23 |
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \ |
wenzelm@4289 | 24 |
ind_syntax.ML cladata.ML simpdata.ML arith_data.ML \ |
wenzelm@4289 | 25 |
typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \ |
paulson@3232 | 26 |
$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \ |
wenzelm@4289 | 27 |
$(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%) |
wenzelm@2448 | 28 |
|
wenzelm@2448 | 29 |
$(OUT)/HOL: $(OUT)/Pure $(FILES) |
wenzelm@2826 | 30 |
@$(ISATOOL) usedir -b $(OUT)/Pure HOL |
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 |
|
oheimb@4263 | 40 |
INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult Com Exp |
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 |
|
wenzelm@4447 | 45 |
$(LOG)/HOL-Induct.gz: $(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@4447 | 54 |
$(LOG)/HOL-IMP.gz: $(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@4447 | 64 |
$(LOG)/HOL-Hoare.gz: $(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@4447 | 75 |
$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES) |
wenzelm@2826 | 76 |
@$(ISATOOL) usedir $(OUT)/HOL Integ |
wenzelm@2448 | 77 |
|
wenzelm@2448 | 78 |
|
wenzelm@3819 | 79 |
## TLA -- Temporal Logic of Actions |
wenzelm@3819 | 80 |
|
wenzelm@3819 | 81 |
TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \ |
wenzelm@3819 | 82 |
TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \ |
wenzelm@3819 | 83 |
TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML |
wenzelm@3819 | 84 |
|
wenzelm@3819 | 85 |
TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy |
wenzelm@3819 | 86 |
|
wenzelm@3819 | 87 |
TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \ |
wenzelm@3819 | 88 |
TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML |
wenzelm@3819 | 89 |
|
wenzelm@3819 | 90 |
TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \ |
wenzelm@3819 | 91 |
TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \ |
wenzelm@3819 | 92 |
TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \ |
wenzelm@3819 | 93 |
TLA/Memory/Memory.ML TLA/Memory/Memory.thy \ |
wenzelm@3819 | 94 |
TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \ |
wenzelm@3819 | 95 |
TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \ |
wenzelm@3819 | 96 |
TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \ |
wenzelm@3819 | 97 |
TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \ |
wenzelm@3819 | 98 |
TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy |
wenzelm@3819 | 99 |
|
wenzelm@3819 | 100 |
|
wenzelm@4447 | 101 |
$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES) |
wenzelm@3819 | 102 |
@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA |
wenzelm@3819 | 103 |
|
wenzelm@4447 | 104 |
$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES) |
wenzelm@3819 | 105 |
@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc |
wenzelm@3819 | 106 |
|
wenzelm@4447 | 107 |
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES) |
wenzelm@3819 | 108 |
@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer |
wenzelm@3819 | 109 |
|
wenzelm@4447 | 110 |
$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES) |
wenzelm@3819 | 111 |
@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory |
wenzelm@3819 | 112 |
|
wenzelm@3819 | 113 |
|
mueller@3079 | 114 |
## I/O Automata (meta theory only) |
wenzelm@2448 | 115 |
|
mueller@3079 | 116 |
IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \ |
mueller@3079 | 117 |
IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML |
wenzelm@2448 | 118 |
|
wenzelm@4447 | 119 |
$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES) |
mueller@3079 | 120 |
@$(ISATOOL) usedir $(OUT)/HOL IOA |
wenzelm@2448 | 121 |
|
wenzelm@2448 | 122 |
|
wenzelm@2448 | 123 |
## Authentication & Security Protocols |
wenzelm@2448 | 124 |
|
paulson@3540 | 125 |
AUTH_NAMES = Message Event Shared NS_Shared \ |
paulson@3540 | 126 |
OtwayRees OtwayRees_AN OtwayRees_Bad \ |
paulson@3482 | 127 |
Recur WooLam Yahalom Yahalom2 \ |
paulson@3482 | 128 |
Public NS_Public_Bad NS_Public TLS |
wenzelm@2448 | 129 |
|
wenzelm@2448 | 130 |
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) |
wenzelm@2448 | 131 |
|
wenzelm@4447 | 132 |
$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES) |
wenzelm@2826 | 133 |
@$(ISATOOL) usedir $(OUT)/HOL Auth |
wenzelm@2448 | 134 |
|
wenzelm@2448 | 135 |
|
mueller@3218 | 136 |
## Modelchecker invocation |
mueller@3218 | 137 |
|
mueller@3218 | 138 |
MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \ |
mueller@3218 | 139 |
Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \ |
mueller@3218 | 140 |
Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML |
mueller@3218 | 141 |
|
wenzelm@4447 | 142 |
$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES) |
mueller@3218 | 143 |
@$(ISATOOL) usedir $(OUT)/HOL Modelcheck |
mueller@3218 | 144 |
|
mueller@3218 | 145 |
|
wenzelm@2448 | 146 |
## Properties of substitutions |
wenzelm@2448 | 147 |
|
paulson@3195 | 148 |
SUBST_NAMES = AList Subst Unifier UTerm Unify |
wenzelm@2448 | 149 |
|
wenzelm@2448 | 150 |
SUBST_FILES = Subst/ROOT.ML \ |
wenzelm@2448 | 151 |
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
wenzelm@2448 | 152 |
|
wenzelm@4447 | 153 |
$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES) |
wenzelm@2826 | 154 |
@$(ISATOOL) usedir $(OUT)/HOL Subst |
wenzelm@2448 | 155 |
|
wenzelm@2448 | 156 |
|
wenzelm@2448 | 157 |
## Confluence of Lambda-calculus |
wenzelm@2448 | 158 |
|
wenzelm@2448 | 159 |
LAMBDA_NAMES = Lambda ParRed Commutation Eta |
wenzelm@2448 | 160 |
|
wenzelm@2448 | 161 |
LAMBDA_FILES = Lambda/ROOT.ML \ |
wenzelm@2448 | 162 |
$(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) |
wenzelm@2448 | 163 |
|
wenzelm@4447 | 164 |
$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES) |
wenzelm@2826 | 165 |
@$(ISATOOL) usedir $(OUT)/HOL Lambda |
wenzelm@2448 | 166 |
|
wenzelm@2448 | 167 |
|
nipkow@2527 | 168 |
## Type inference without let |
wenzelm@2448 | 169 |
|
nipkow@2527 | 170 |
W0_NAMES = I Maybe MiniML Type W |
nipkow@2527 | 171 |
|
nipkow@2527 | 172 |
W0_FILES = W0/ROOT.ML \ |
nipkow@2527 | 173 |
$(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) |
nipkow@2527 | 174 |
|
wenzelm@4447 | 175 |
$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES) |
wenzelm@2826 | 176 |
@$(ISATOOL) usedir $(OUT)/HOL W0 |
nipkow@2527 | 177 |
|
nipkow@2527 | 178 |
|
nipkow@2527 | 179 |
## Type inference with let |
nipkow@2527 | 180 |
|
nipkow@2527 | 181 |
MINIML_NAMES = Generalize Instance Maybe MiniML Type W |
wenzelm@2448 | 182 |
|
wenzelm@2448 | 183 |
MINIML_FILES = MiniML/ROOT.ML \ |
wenzelm@2448 | 184 |
$(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) |
wenzelm@2448 | 185 |
|
wenzelm@4447 | 186 |
$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES) |
wenzelm@2826 | 187 |
@$(ISATOOL) usedir $(OUT)/HOL MiniML |
wenzelm@2448 | 188 |
|
wenzelm@2448 | 189 |
|
wenzelm@2448 | 190 |
## Lexical analysis |
wenzelm@2448 | 191 |
|
wenzelm@2448 | 192 |
LEX_FILES = Auto AutoChopper Chopper Prefix |
wenzelm@2448 | 193 |
|
wenzelm@2448 | 194 |
LEX_FILES = Lex/ROOT.ML \ |
wenzelm@2448 | 195 |
$(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) |
wenzelm@2448 | 196 |
|
wenzelm@4447 | 197 |
$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES) |
wenzelm@2826 | 198 |
@$(ISATOOL) usedir $(OUT)/HOL Lex |
wenzelm@2448 | 199 |
|
wenzelm@2448 | 200 |
|
wenzelm@2545 | 201 |
## Axiomatic type classes examples |
wenzelm@2545 | 202 |
|
wenzelm@2545 | 203 |
AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \ |
wenzelm@2545 | 204 |
GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy |
wenzelm@2545 | 205 |
|
wenzelm@2545 | 206 |
AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \ |
wenzelm@2545 | 207 |
LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \ |
wenzelm@2545 | 208 |
Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \ |
wenzelm@2545 | 209 |
Order.ML Order.thy ROOT.ML tools.ML |
wenzelm@2545 | 210 |
|
wenzelm@2545 | 211 |
AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \ |
wenzelm@2545 | 212 |
MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \ |
wenzelm@2545 | 213 |
ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ |
wenzelm@2545 | 214 |
Xor.ML Xor.thy |
wenzelm@2545 | 215 |
|
wenzelm@4447 | 216 |
$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL |
wenzelm@4447 | 217 |
@$(ISATOOL) usedir $(OUT)/HOL AxClasses |
wenzelm@2545 | 218 |
|
wenzelm@4447 | 219 |
$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \ |
wenzelm@4447 | 220 |
$(AXC_GROUP_FILES:%=AxClasses/Group/%) |
wenzelm@2827 | 221 |
@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group |
wenzelm@4447 | 222 |
|
wenzelm@4447 | 223 |
$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \ |
wenzelm@4447 | 224 |
$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) |
wenzelm@2827 | 225 |
@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice |
wenzelm@4447 | 226 |
|
wenzelm@4447 | 227 |
$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \ |
wenzelm@4447 | 228 |
$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) |
wenzelm@2827 | 229 |
@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial |
wenzelm@2545 | 230 |
|
wenzelm@2545 | 231 |
|
slotosch@2909 | 232 |
## Higher-order quotients and example fractionals |
wenzelm@2900 | 233 |
|
slotosch@2909 | 234 |
QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \ |
slotosch@2909 | 235 |
Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \ |
slotosch@2909 | 236 |
Quot/FRACT.thy Quot/FRACT.ML |
wenzelm@4447 | 237 |
|
wenzelm@4447 | 238 |
$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES) |
wenzelm@2900 | 239 |
@$(ISATOOL) usedir $(OUT)/HOL Quot |
wenzelm@2900 | 240 |
|
wenzelm@2900 | 241 |
|
wenzelm@2448 | 242 |
## Miscellaneous examples |
wenzelm@2448 | 243 |
|
paulson@3417 | 244 |
EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT |
wenzelm@2448 | 245 |
|
wenzelm@2448 | 246 |
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
wenzelm@2448 | 247 |
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
wenzelm@2448 | 248 |
|
wenzelm@4447 | 249 |
$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES) |
wenzelm@2826 | 250 |
@$(ISATOOL) usedir $(OUT)/HOL ex |
wenzelm@2448 | 251 |
|
wenzelm@2448 | 252 |
|
wenzelm@2448 | 253 |
## Full test |
wenzelm@2448 | 254 |
|
wenzelm@4447 | 255 |
ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \ |
wenzelm@4447 | 256 |
$(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \ |
wenzelm@4447 | 257 |
$(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \ |
wenzelm@4447 | 258 |
$(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ |
wenzelm@4447 | 259 |
$(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \ |
wenzelm@4447 | 260 |
$(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \ |
wenzelm@4447 | 261 |
$(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \ |
wenzelm@4447 | 262 |
$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz |
wenzelm@4447 | 263 |
|
wenzelm@4447 | 264 |
test: $(ALL_TARGETS) |
wenzelm@4447 | 265 |
|
wenzelm@4447 | 266 |
clean: |
wenzelm@4447 | 267 |
@rm -f $(ALL_TARGETS) |
wenzelm@2448 | 268 |
|
wenzelm@2448 | 269 |
|
wenzelm@2448 | 270 |
.PRECIOUS: $(OUT)/Pure $(OUT)/HOL |