src/HOL/IsaMakefile

ex/LFilter is a new theory (and dependency)

#
# $Id$
#
# IsaMakefile for HOL
#

#### Base system

OUT = $(ISABELLE_OUTPUT_DIR)

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

FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
	ind_syntax.ML cladata.ML simpdata.ML \
	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
	../Provers/simplifier.ML ../Provers/splitter.ML \
	../Provers/nat_transitive.ML \
	$(NAMES:%=%.thy) $(NAMES:%=%.ML)

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

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


## TFL (requires integration into HOL proper)

TFL_NAMES = mask tfl thms thry usyntax utils
TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
            $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)

TFL:	$(OUT)/HOL $(TFL_FILES)
	@$(ISABELLE) -qe 'exit_use_dir"../TFL"; quit();' HOL



#### Tests and examples

## 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)

IMP:	$(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)

Hoare:	$(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)

Integ:	$(OUT)/HOL $(INTEG_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Integ


## I/O Automata

IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \
		Receiver Sender
IOA_ABP_NAMES = Action Correctness Lemmas
IOA_MT_NAMES = Asig IOA Solve

IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \
 $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \
 IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \
 IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \
 IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \
 $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \
 $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)

IOA:	$(OUT)/HOL $(IOA_FILES)
	@$(ISATOOL) usedir -s IOA-NTP $(OUT)/HOL IOA/NTP
	@$(ISATOOL) usedir -s IOA-ABP $(OUT)/HOL IOA/ABP


## Authentication & Security Protocols

Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
	     Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public

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

Auth:	$(OUT)/HOL $(AUTH_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Auth


## Properties of substitutions

SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas

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

Subst:	$(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)

Lambda:	 $(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)

W0: $(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)

MiniML: $(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)

Lex:	$(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

AXCLASSES_FILES = AxClasses/ROOT.ML \
	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)

AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
	@$(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
Quot:	$(OUT)/HOL $(QUOT_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL Quot


## Miscellaneous examples

EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
	   Primes NatSum SList LList LFilter Acc PropLog Term Simult 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)

ex:	$(OUT)/HOL $(EX_FILES)
	@$(ISATOOL) usedir $(OUT)/HOL ex


## Full test

test:	$(OUT)/HOL \
	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
	echo 'Test examples ran successfully' > test


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