src/HOL/IsaMakefile

added record.ML;

#
# $Id$
#
# IsaMakefile for HOL
#

#### Base system

OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log

NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
	Divides Power Sexp Univ List RelPow Option Map

PROVERS = hypsubst.ML classical.ML blast.ML \
	simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML

TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
	usyntax.sig usyntax.sml utils.sig utils.sml

FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
	ind_syntax.ML cladata.ML record.ML simpdata.ML arith_data.ML \
	typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \
	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
	$(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)

$(OUT)/HOL: $(OUT)/Pure $(FILES)
	@$(ISATOOL) usedir -b $(OUT)/Pure HOL

$(OUT)/Pure:
	@cd ../Pure; $(ISATOOL) make


#### Tests and examples

## Inductive definitions: simple examples

INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult Com Exp

INDUCT_FILES = Induct/ROOT.ML \
	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)

$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Induct


## IMP-semantics example

IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)

$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL IMP


## Hoare logic

Hoare_NAMES = Hoare Arith2 Examples
Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
	      $(Hoare_NAMES:%=Hoare/%.ML)

$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Hoare


## The integers in HOL

INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing

INTEG_FILES = Integ/ROOT.ML \
	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)

$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Integ


## TLA -- Temporal Logic of Actions

TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \
	TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \
	TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML

TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy

TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \
	TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML

TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \
	TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \
	TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \
	TLA/Memory/Memory.ML TLA/Memory/Memory.thy \
	TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \
	TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \
	TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \
	TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \
	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy


$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES)
	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA

$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES)
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc

$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES)
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer

$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES)
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory


## I/O Automata (meta theory only)

IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML

$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL IOA


## Authentication & Security Protocols

AUTH_NAMES = Message Event Shared NS_Shared \
	     OtwayRees OtwayRees_AN OtwayRees_Bad \
	     Recur WooLam Yahalom Yahalom2 \
	     Public NS_Public_Bad NS_Public TLS

AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)

$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Auth


## Modelchecker invocation

MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
  Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
  Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML

$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck


## Properties of substitutions

SUBST_NAMES = AList Subst Unifier UTerm Unify

SUBST_FILES = Subst/ROOT.ML \
	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)

$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Subst


## Confluence of Lambda-calculus

LAMBDA_NAMES = Lambda ParRed Commutation Eta

LAMBDA_FILES = Lambda/ROOT.ML \
	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)

$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Lambda


## Type inference without let

W0_NAMES = I Maybe MiniML Type W

W0_FILES = W0/ROOT.ML \
	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)

$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL W0


## Type inference with let

MINIML_NAMES = Generalize Instance Maybe MiniML Type W

MINIML_FILES = MiniML/ROOT.ML \
	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)

$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL MiniML


## Lexical analysis

LEX_FILES = Auto AutoChopper Chopper Prefix

LEX_FILES = Lex/ROOT.ML \
	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)

$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Lex


## Axiomatic type classes examples

AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy

AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
	Order.ML Order.thy ROOT.ML tools.ML

AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
	Xor.ML Xor.thy

$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses

$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
  $(AXC_GROUP_FILES:%=AxClasses/Group/%)
	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group

$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
  $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice

$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
  $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial


## Higher-order quotients and example fractionals

QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
	Quot/FRACT.thy Quot/FRACT.ML

$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Quot


## Miscellaneous examples

EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT

EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)

$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL ex


## Full test

ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
  $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
  $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
  $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
  $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
  $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz

test: $(ALL_TARGETS)

clean:
	@rm -f $(ALL_TARGETS)


.PRECIOUS: $(OUT)/Pure $(OUT)/HOL