src/HOL/IsaMakefile
author wenzelm
Fri Dec 19 12:09:08 1997 +0100 (1997-12-19)
changeset 4455 c0a6ad614fa0
parent 4447 b7ee449eb345
child 4518 74c01296e818
permissions -rw-r--r--
added record.ML;
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@4455
    24
	ind_syntax.ML cladata.ML record.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
nipkow@2527
   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)
wenzelm@2448
   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@4447
   218
wenzelm@4447
   219
$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
wenzelm@4447
   220
  $(AXC_GROUP_FILES:%=AxClasses/Group/%)
wenzelm@4447
   221
	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
wenzelm@2545
   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