src/HOL/IsaMakefile
changeset 33010 39f73a59e855
parent 32812 6a8663ff5e44
child 33024 60a098883d81
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 20 08:10:47 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 20 10:11:30 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Generate-HOL HOL-Generate-HOLLight
     1.7 -images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     1.8 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-SMT HOL-Word TLA HOL4
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    1.11  test: \
    1.12 @@ -40,7 +40,7 @@
    1.13    HOL-Prolog \
    1.14    HOL-SET-Protocol \
    1.15    HOL-SizeChange \
    1.16 -  HOL-SMT \
    1.17 +  HOL-SMT-Examples \
    1.18    HOL-Statespace \
    1.19    HOL-Subst \
    1.20        TLA-Buffer \
    1.21 @@ -1146,15 +1146,222 @@
    1.22  
    1.23  HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz
    1.24  
    1.25 -$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \
    1.26 +$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy SMT/SMT.thy \
    1.27    SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
    1.28    SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \
    1.29    SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \
    1.30    SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \
    1.31 -  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML
    1.32 +  SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML \
    1.33 +  SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \
    1.34 +  SMT/Tools/z3_solver.ML
    1.35  	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
    1.36  
    1.37  
    1.38 +## HOL-SMT-Examples
    1.39 +
    1.40 +HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz
    1.41 +
    1.42 +$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML	\
    1.43 +  SMT/Examples/SMT_Examples.thy \
    1.44 +  SMT/Examples/cert/z3_arith_quant_01 \
    1.45 +  SMT/Examples/cert/z3_arith_quant_01.proof \
    1.46 +  SMT/Examples/cert/z3_arith_quant_02 \
    1.47 +  SMT/Examples/cert/z3_arith_quant_02.proof \
    1.48 +  SMT/Examples/cert/z3_arith_quant_03 \
    1.49 +  SMT/Examples/cert/z3_arith_quant_03.proof \
    1.50 +  SMT/Examples/cert/z3_arith_quant_04 \
    1.51 +  SMT/Examples/cert/z3_arith_quant_04.proof \
    1.52 +  SMT/Examples/cert/z3_arith_quant_05 \
    1.53 +  SMT/Examples/cert/z3_arith_quant_05.proof \
    1.54 +  SMT/Examples/cert/z3_arith_quant_06 \
    1.55 +  SMT/Examples/cert/z3_arith_quant_06.proof \
    1.56 +  SMT/Examples/cert/z3_arith_quant_07 \
    1.57 +  SMT/Examples/cert/z3_arith_quant_07.proof \
    1.58 +  SMT/Examples/cert/z3_arith_quant_08 \
    1.59 +  SMT/Examples/cert/z3_arith_quant_08.proof \
    1.60 +  SMT/Examples/cert/z3_arith_quant_09 \
    1.61 +  SMT/Examples/cert/z3_arith_quant_09.proof \
    1.62 +  SMT/Examples/cert/z3_arith_quant_10 \
    1.63 +  SMT/Examples/cert/z3_arith_quant_10.proof \
    1.64 +  SMT/Examples/cert/z3_arith_quant_11 \
    1.65 +  SMT/Examples/cert/z3_arith_quant_11.proof \
    1.66 +  SMT/Examples/cert/z3_arith_quant_12 \
    1.67 +  SMT/Examples/cert/z3_arith_quant_12.proof \
    1.68 +  SMT/Examples/cert/z3_arith_quant_13 \
    1.69 +  SMT/Examples/cert/z3_arith_quant_13.proof \
    1.70 +  SMT/Examples/cert/z3_arith_quant_14 \
    1.71 +  SMT/Examples/cert/z3_arith_quant_14.proof \
    1.72 +  SMT/Examples/cert/z3_arith_quant_15 \
    1.73 +  SMT/Examples/cert/z3_arith_quant_15.proof \
    1.74 +  SMT/Examples/cert/z3_arith_quant_16 \
    1.75 +  SMT/Examples/cert/z3_arith_quant_16.proof \
    1.76 +  SMT/Examples/cert/z3_arith_quant_17 \
    1.77 +  SMT/Examples/cert/z3_arith_quant_17.proof \
    1.78 +  SMT/Examples/cert/z3_arith_quant_18 \
    1.79 +  SMT/Examples/cert/z3_arith_quant_18.proof \
    1.80 +  SMT/Examples/cert/z3_bv_01 \
    1.81 +  SMT/Examples/cert/z3_bv_01.proof \
    1.82 +  SMT/Examples/cert/z3_bv_02 \
    1.83 +  SMT/Examples/cert/z3_bv_02.proof \
    1.84 +  SMT/Examples/cert/z3_bv_arith_01 \
    1.85 +  SMT/Examples/cert/z3_bv_arith_01.proof \
    1.86 +  SMT/Examples/cert/z3_bv_arith_02 \
    1.87 +  SMT/Examples/cert/z3_bv_arith_02.proof \
    1.88 +  SMT/Examples/cert/z3_bv_arith_03 \
    1.89 +  SMT/Examples/cert/z3_bv_arith_03.proof \
    1.90 +  SMT/Examples/cert/z3_bv_arith_04 \
    1.91 +  SMT/Examples/cert/z3_bv_arith_04.proof \
    1.92 +  SMT/Examples/cert/z3_bv_arith_05 \
    1.93 +  SMT/Examples/cert/z3_bv_arith_05.proof \
    1.94 +  SMT/Examples/cert/z3_bv_arith_06 \
    1.95 +  SMT/Examples/cert/z3_bv_arith_06.proof \
    1.96 +  SMT/Examples/cert/z3_bv_arith_07 \
    1.97 +  SMT/Examples/cert/z3_bv_arith_07.proof \
    1.98 +  SMT/Examples/cert/z3_bv_arith_08 \
    1.99 +  SMT/Examples/cert/z3_bv_arith_08.proof \
   1.100 +  SMT/Examples/cert/z3_bv_arith_09 \
   1.101 +  SMT/Examples/cert/z3_bv_arith_09.proof \
   1.102 +  SMT/Examples/cert/z3_bv_arith_10 \
   1.103 +  SMT/Examples/cert/z3_bv_arith_10.proof \
   1.104 +  SMT/Examples/cert/z3_bv_bit_01 \
   1.105 +  SMT/Examples/cert/z3_bv_bit_01.proof \
   1.106 +  SMT/Examples/cert/z3_bv_bit_02 \
   1.107 +  SMT/Examples/cert/z3_bv_bit_02.proof \
   1.108 +  SMT/Examples/cert/z3_bv_bit_03 \
   1.109 +  SMT/Examples/cert/z3_bv_bit_03.proof \
   1.110 +  SMT/Examples/cert/z3_bv_bit_04 \
   1.111 +  SMT/Examples/cert/z3_bv_bit_04.proof \
   1.112 +  SMT/Examples/cert/z3_bv_bit_05 \
   1.113 +  SMT/Examples/cert/z3_bv_bit_05.proof \
   1.114 +  SMT/Examples/cert/z3_bv_bit_06 \
   1.115 +  SMT/Examples/cert/z3_bv_bit_06.proof \
   1.116 +  SMT/Examples/cert/z3_bv_bit_07 \
   1.117 +  SMT/Examples/cert/z3_bv_bit_07.proof \
   1.118 +  SMT/Examples/cert/z3_bv_bit_08 \
   1.119 +  SMT/Examples/cert/z3_bv_bit_08.proof \
   1.120 +  SMT/Examples/cert/z3_bv_bit_09 \
   1.121 +  SMT/Examples/cert/z3_bv_bit_09.proof \
   1.122 +  SMT/Examples/cert/z3_bv_bit_10 \
   1.123 +  SMT/Examples/cert/z3_bv_bit_10.proof \
   1.124 +  SMT/Examples/cert/z3_bv_bit_11 \
   1.125 +  SMT/Examples/cert/z3_bv_bit_11.proof \
   1.126 +  SMT/Examples/cert/z3_bv_bit_12 \
   1.127 +  SMT/Examples/cert/z3_bv_bit_12.proof \
   1.128 +  SMT/Examples/cert/z3_bv_bit_13 \
   1.129 +  SMT/Examples/cert/z3_bv_bit_13.proof \
   1.130 +  SMT/Examples/cert/z3_bv_bit_14 \
   1.131 +  SMT/Examples/cert/z3_bv_bit_14.proof \
   1.132 +  SMT/Examples/cert/z3_bv_bit_15 \
   1.133 +  SMT/Examples/cert/z3_bv_bit_15.proof \
   1.134 +  SMT/Examples/cert/z3_fol_01 \
   1.135 +  SMT/Examples/cert/z3_fol_01.proof \
   1.136 +  SMT/Examples/cert/z3_fol_02 \
   1.137 +  SMT/Examples/cert/z3_fol_02.proof \
   1.138 +  SMT/Examples/cert/z3_fol_03 \
   1.139 +  SMT/Examples/cert/z3_fol_03.proof \
   1.140 +  SMT/Examples/cert/z3_fol_04 \
   1.141 +  SMT/Examples/cert/z3_fol_04.proof \
   1.142 +  SMT/Examples/cert/z3_hol_01 \
   1.143 +  SMT/Examples/cert/z3_hol_01.proof \
   1.144 +  SMT/Examples/cert/z3_hol_02 \
   1.145 +  SMT/Examples/cert/z3_hol_02.proof \
   1.146 +  SMT/Examples/cert/z3_hol_03 \
   1.147 +  SMT/Examples/cert/z3_hol_03.proof \
   1.148 +  SMT/Examples/cert/z3_hol_04 \
   1.149 +  SMT/Examples/cert/z3_hol_04.proof \
   1.150 +  SMT/Examples/cert/z3_hol_05 \
   1.151 +  SMT/Examples/cert/z3_hol_05.proof \
   1.152 +  SMT/Examples/cert/z3_hol_06 \
   1.153 +  SMT/Examples/cert/z3_hol_06.proof \
   1.154 +  SMT/Examples/cert/z3_hol_07 \
   1.155 +  SMT/Examples/cert/z3_hol_07.proof \
   1.156 +  SMT/Examples/cert/z3_hol_08 \
   1.157 +  SMT/Examples/cert/z3_hol_08.proof \
   1.158 +  SMT/Examples/cert/z3_linarith_01 \
   1.159 +  SMT/Examples/cert/z3_linarith_01.proof \
   1.160 +  SMT/Examples/cert/z3_linarith_02 \
   1.161 +  SMT/Examples/cert/z3_linarith_02.proof \
   1.162 +  SMT/Examples/cert/z3_linarith_03 \
   1.163 +  SMT/Examples/cert/z3_linarith_03.proof \
   1.164 +  SMT/Examples/cert/z3_linarith_04 \
   1.165 +  SMT/Examples/cert/z3_linarith_04.proof \
   1.166 +  SMT/Examples/cert/z3_linarith_05 \
   1.167 +  SMT/Examples/cert/z3_linarith_05.proof \
   1.168 +  SMT/Examples/cert/z3_linarith_06 \
   1.169 +  SMT/Examples/cert/z3_linarith_06.proof \
   1.170 +  SMT/Examples/cert/z3_linarith_07 \
   1.171 +  SMT/Examples/cert/z3_linarith_07.proof \
   1.172 +  SMT/Examples/cert/z3_linarith_08 \
   1.173 +  SMT/Examples/cert/z3_linarith_08.proof \
   1.174 +  SMT/Examples/cert/z3_linarith_09 \
   1.175 +  SMT/Examples/cert/z3_linarith_09.proof \
   1.176 +  SMT/Examples/cert/z3_linarith_10 \
   1.177 +  SMT/Examples/cert/z3_linarith_10.proof \
   1.178 +  SMT/Examples/cert/z3_linarith_11 \
   1.179 +  SMT/Examples/cert/z3_linarith_11.proof \
   1.180 +  SMT/Examples/cert/z3_linarith_12 \
   1.181 +  SMT/Examples/cert/z3_linarith_12.proof \
   1.182 +  SMT/Examples/cert/z3_linarith_13 \
   1.183 +  SMT/Examples/cert/z3_linarith_13.proof \
   1.184 +  SMT/Examples/cert/z3_linarith_14 \
   1.185 +  SMT/Examples/cert/z3_linarith_14.proof \
   1.186 +  SMT/Examples/cert/z3_linarith_15 \
   1.187 +  SMT/Examples/cert/z3_linarith_15.proof \
   1.188 +  SMT/Examples/cert/z3_linarith_16 \
   1.189 +  SMT/Examples/cert/z3_linarith_16.proof \
   1.190 +  SMT/Examples/cert/z3_mono_01 \
   1.191 +  SMT/Examples/cert/z3_mono_01.proof \
   1.192 +  SMT/Examples/cert/z3_mono_02 \
   1.193 +  SMT/Examples/cert/z3_mono_02.proof \
   1.194 +  SMT/Examples/cert/z3_nat_arith_01 \
   1.195 +  SMT/Examples/cert/z3_nat_arith_01.proof \
   1.196 +  SMT/Examples/cert/z3_nat_arith_02 \
   1.197 +  SMT/Examples/cert/z3_nat_arith_02.proof \
   1.198 +  SMT/Examples/cert/z3_nat_arith_03 \
   1.199 +  SMT/Examples/cert/z3_nat_arith_03.proof \
   1.200 +  SMT/Examples/cert/z3_nat_arith_04 \
   1.201 +  SMT/Examples/cert/z3_nat_arith_04.proof \
   1.202 +  SMT/Examples/cert/z3_nat_arith_05 \
   1.203 +  SMT/Examples/cert/z3_nat_arith_05.proof \
   1.204 +  SMT/Examples/cert/z3_nat_arith_06 \
   1.205 +  SMT/Examples/cert/z3_nat_arith_06.proof \
   1.206 +  SMT/Examples/cert/z3_nat_arith_07 \
   1.207 +  SMT/Examples/cert/z3_nat_arith_07.proof \
   1.208 +  SMT/Examples/cert/z3_nlarith_01 \
   1.209 +  SMT/Examples/cert/z3_nlarith_01.proof \
   1.210 +  SMT/Examples/cert/z3_nlarith_02 \
   1.211 +  SMT/Examples/cert/z3_nlarith_02.proof \
   1.212 +  SMT/Examples/cert/z3_nlarith_03 \
   1.213 +  SMT/Examples/cert/z3_nlarith_03.proof \
   1.214 +  SMT/Examples/cert/z3_nlarith_04 \
   1.215 +  SMT/Examples/cert/z3_nlarith_04.proof \
   1.216 +  SMT/Examples/cert/z3_pair_01 \
   1.217 +  SMT/Examples/cert/z3_pair_01.proof \
   1.218 +  SMT/Examples/cert/z3_pair_02 \
   1.219 +  SMT/Examples/cert/z3_pair_02.proof \
   1.220 +  SMT/Examples/cert/z3_prop_01 \
   1.221 +  SMT/Examples/cert/z3_prop_01.proof \
   1.222 +  SMT/Examples/cert/z3_prop_02 \
   1.223 +  SMT/Examples/cert/z3_prop_02.proof \
   1.224 +  SMT/Examples/cert/z3_prop_03 \
   1.225 +  SMT/Examples/cert/z3_prop_03.proof \
   1.226 +  SMT/Examples/cert/z3_prop_04 \
   1.227 +  SMT/Examples/cert/z3_prop_04.proof \
   1.228 +  SMT/Examples/cert/z3_prop_05 \
   1.229 +  SMT/Examples/cert/z3_prop_05.proof \
   1.230 +  SMT/Examples/cert/z3_prop_06 \
   1.231 +  SMT/Examples/cert/z3_prop_06.proof \
   1.232 +  SMT/Examples/cert/z3_prop_07 \
   1.233 +  SMT/Examples/cert/z3_prop_07.proof \
   1.234 +  SMT/Examples/cert/z3_prop_08 \
   1.235 +  SMT/Examples/cert/z3_prop_08.proof \
   1.236 +  SMT/Examples/cert/z3_prop_09 \
   1.237 +  SMT/Examples/cert/z3_prop_09.proof \
   1.238 +  SMT/Examples/cert/z3_prop_10 \
   1.239 +  SMT/Examples/cert/z3_prop_10.proof
   1.240 +	@cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples
   1.241 +
   1.242 +
   1.243  ## clean
   1.244  
   1.245  clean:
   1.246 @@ -1177,4 +1384,6 @@
   1.247  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
   1.248  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
   1.249  		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
   1.250 -                $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz
   1.251 +                $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz               \
   1.252 +                $(LOG)/HOL-SMT-Examples.gz
   1.253 +