author  paulson 
Tue, 01 Jul 1997 17:42:36 +0200  
changeset 3482  ef918a90f9bf 
parent 3417  58ccb80eb50a 
child 3505  1cb4ea47d967 
permissions  rwrr 
2448  1 
# 
2 
# $Id$ 

3 
# 

4 
# IsaMakefile for HOL 

5 
# 

6 

7 
#### Base system 

8 

3118  9 
OUT = $(ISABELLE_OUTPUT) 
2448  10 

3195  11 
NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \ 
3025  12 
mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \ 
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
3369
diff
changeset

13 
Divides Power Sexp Univ List RelPow Option 
2448  14 

3232
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

15 
PROVERS = hypsubst.ML classical.ML blast.ML \ 
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

16 
simplifier.ML splitter.ML nat_transitive.ML 
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

17 

3354  18 
TFL = dcterm.sml post.sml rules.new.sml rules.sig \ 
3232
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

19 
sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml \ 
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

20 
usyntax.sig usyntax.sml utils.sig utils.sml 
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

21 

2448  22 
FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \ 
23 
ind_syntax.ML cladata.ML simpdata.ML \ 

24 
typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \ 

3232
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

25 
$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \ 
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

26 
$(PROVERS:%=../Provers/%) 
2448  27 

28 
$(OUT)/HOL: $(OUT)/Pure $(FILES) 

2826  29 
@$(ISATOOL) usedir b $(OUT)/Pure HOL 
2448  30 
@chmod w $@ 
31 

32 
$(OUT)/Pure: 

2473  33 
@cd ../Pure; $(ISATOOL) make 
2448  34 

35 

2473  36 
#### Tests and examples 
37 

3125  38 
## Inductive definitions: simple examples 
39 

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

41 

42 
INDUCT_FILES = Induct/ROOT.ML \ 

43 
$(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML) 

44 

45 
Induct: $(OUT)/HOL $(INDUCT_FILES) 

46 
@$(ISATOOL) usedir $(OUT)/HOL Induct 

47 

48 

2448  49 
## IMPsemantics example 
50 

51 
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC 

52 
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) 

53 

54 
IMP: $(OUT)/HOL $(IMP_FILES) 

2826  55 
@$(ISATOOL) usedir $(OUT)/HOL IMP 
2448  56 

57 

58 
## Hoare logic 

59 

60 
Hoare_NAMES = Hoare Arith2 Examples 

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

62 
$(Hoare_NAMES:%=Hoare/%.ML) 

63 

64 
Hoare: $(OUT)/HOL $(Hoare_FILES) 

2826  65 
@$(ISATOOL) usedir $(OUT)/HOL Hoare 
2448  66 

67 

68 
## The integers in HOL 

69 

70 
INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing 

71 

72 
INTEG_FILES = Integ/ROOT.ML \ 

73 
$(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) 

74 

75 
Integ: $(OUT)/HOL $(INTEG_FILES) 

2826  76 
@$(ISATOOL) usedir $(OUT)/HOL Integ 
2448  77 

78 

3079  79 
## I/O Automata (meta theory only) 
2448  80 

81 

3079  82 
IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \ 
83 
IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML 

2448  84 

3079  85 
IOA: $(OUT)/HOL $(IOA_FILES) 
86 
@$(ISATOOL) usedir $(OUT)/HOL IOA 

2448  87 

88 

89 
## Authentication & Security Protocols 

90 

91 
Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \ 

3482  92 
Recur WooLam Yahalom Yahalom2 \ 
93 
Public NS_Public_Bad NS_Public TLS 

2448  94 

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

96 

97 
Auth: $(OUT)/HOL $(AUTH_FILES) 

2826  98 
@$(ISATOOL) usedir $(OUT)/HOL Auth 
2448  99 

100 

3218  101 
## Modelchecker invocation 
102 

103 
MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \ 

104 
Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \ 

105 
Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML 

106 

107 
Modelcheck: $(OUT)/HOL $(MC_FILES) 

108 
@$(ISATOOL) usedir $(OUT)/HOL Modelcheck 

109 

110 

2448  111 
## Properties of substitutions 
112 

3195  113 
SUBST_NAMES = AList Subst Unifier UTerm Unify 
2448  114 

115 
SUBST_FILES = Subst/ROOT.ML \ 

116 
$(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) 

117 

118 
Subst: $(OUT)/HOL $(SUBST_FILES) 

2826  119 
@$(ISATOOL) usedir $(OUT)/HOL Subst 
2448  120 

121 

122 
## Confluence of Lambdacalculus 

123 

124 
LAMBDA_NAMES = Lambda ParRed Commutation Eta 

125 

126 
LAMBDA_FILES = Lambda/ROOT.ML \ 

127 
$(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) 

128 

129 
Lambda: $(OUT)/HOL $(LAMBDA_FILES) 

2826  130 
@$(ISATOOL) usedir $(OUT)/HOL Lambda 
2448  131 

132 

2527  133 
## Type inference without let 
134 

135 
W0_NAMES = I Maybe MiniML Type W 

136 

137 
W0_FILES = W0/ROOT.ML \ 

138 
$(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) 

2448  139 

2527  140 
W0: $(OUT)/HOL $(W0_FILES) 
2826  141 
@$(ISATOOL) usedir $(OUT)/HOL W0 
2527  142 

143 

144 
## Type inference with let 

145 

146 
MINIML_NAMES = Generalize Instance Maybe MiniML Type W 

2448  147 

148 
MINIML_FILES = MiniML/ROOT.ML \ 

149 
$(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) 

150 

151 
MiniML: $(OUT)/HOL $(MINIML_FILES) 

2826  152 
@$(ISATOOL) usedir $(OUT)/HOL MiniML 
2448  153 

154 

155 
## Lexical analysis 

156 

157 
LEX_FILES = Auto AutoChopper Chopper Prefix 

158 

159 
LEX_FILES = Lex/ROOT.ML \ 

160 
$(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) 

161 

162 
Lex: $(OUT)/HOL $(LEX_FILES) 

2826  163 
@$(ISATOOL) usedir $(OUT)/HOL Lex 
2448  164 

165 

2545  166 
## Axiomatic type classes examples 
167 

168 
AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \ 

169 
GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy 

170 

171 
AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \ 

172 
LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \ 

173 
Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \ 

174 
Order.ML Order.thy ROOT.ML tools.ML 

175 

176 
AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \ 

177 
MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \ 

178 
ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ 

179 
Xor.ML Xor.thy 

180 

181 
AXCLASSES_FILES = AxClasses/ROOT.ML \ 

182 
$(AXC_GROUP_FILES:%=AxClasses/Group/%) \ 

183 
$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \ 

184 
$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) 

185 

186 
AxClasses: $(OUT)/HOL $(AXCLASSES_FILES) 

2826  187 
@$(ISATOOL) usedir $(OUT)/HOL AxClasses 
2827  188 
@$(ISATOOL) usedir s AxClassesGroup $(OUT)/HOL AxClasses/Group 
189 
@$(ISATOOL) usedir s AxClassesLattice $(OUT)/HOL AxClasses/Lattice 

190 
@$(ISATOOL) usedir s AxClassesTutorial $(OUT)/HOL AxClasses/Tutorial 

2545  191 

192 

2909  193 
## Higherorder quotients and example fractionals 
2900  194 

2909  195 
QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \ 
196 
Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \ 

197 
Quot/FRACT.thy Quot/FRACT.ML 

2900  198 
Quot: $(OUT)/HOL $(QUOT_FILES) 
199 
@$(ISATOOL) usedir $(OUT)/HOL Quot 

200 

201 

2448  202 
## Miscellaneous examples 
203 

3417  204 
EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT 
2448  205 

206 
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ 

207 
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) 

208 

209 
ex: $(OUT)/HOL $(EX_FILES) 

2826  210 
@$(ISATOOL) usedir $(OUT)/HOL ex 
2448  211 

212 

213 
## Full test 

214 

2635  215 
test: $(OUT)/HOL \ 
3218  216 
Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda \ 
3125  217 
W0 MiniML IOA AxClasses Quot ex 
2448  218 
echo 'Test examples ran successfully' > test 
219 

220 

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