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