1.1 --- a/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:37 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:38 2011 +0200
1.3 @@ -50,215 +50,215 @@
1.4 by linarith
1.5
1.6 lemma "B \<subseteq> C"
1.7 -sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
1.8 +sledgehammer [type_enc = poly_args, max_relevant = 200, expect = some]
1.9 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
1.10
1.11
1.12 text {* Proxies for logical constants *}
1.13
1.14 lemma "id (op =) x x"
1.15 -sledgehammer [type_sys = erased, expect = none] (id_apply)
1.16 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.17 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.18 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.19 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.20 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.21 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.22 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.23 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.24 +sledgehammer [type_enc = erased, expect = none] (id_apply)
1.25 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.26 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.27 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.28 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.29 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.30 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.31 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.32 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.33 by (metis (full_types) id_apply)
1.34
1.35 lemma "id True"
1.36 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.37 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.38 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.39 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.40 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.41 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.42 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.43 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.44 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.45 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.46 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.47 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.48 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.49 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.50 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.51 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.52 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.53 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.54 by (metis_exhaust id_apply)
1.55
1.56 lemma "\<not> id False"
1.57 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.58 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.59 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.60 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.61 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.62 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.63 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.64 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.65 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.66 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.67 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.68 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.69 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.70 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.71 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.72 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.73 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.74 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.75 by (metis_exhaust id_apply)
1.76
1.77 lemma "x = id True \<or> x = id False"
1.78 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.79 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.80 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.81 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.82 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.83 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.84 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.85 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.86 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.87 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.88 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.89 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.90 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.91 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.92 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.93 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.94 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.95 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.96 by (metis_exhaust id_apply)
1.97
1.98 lemma "id x = id True \<or> id x = id False"
1.99 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.100 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.101 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.102 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.103 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.104 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.105 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.106 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.107 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.108 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.109 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.110 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.111 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.112 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.113 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.114 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.115 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.116 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.117 by (metis_exhaust id_apply)
1.118
1.119 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
1.120 -sledgehammer [type_sys = erased, expect = none] ()
1.121 -sledgehammer [type_sys = poly_args, expect = none] ()
1.122 -sledgehammer [type_sys = poly_tags?, expect = some] ()
1.123 -sledgehammer [type_sys = poly_tags, expect = some] ()
1.124 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.125 -sledgehammer [type_sys = poly_preds, expect = some] ()
1.126 -sledgehammer [type_sys = mangled_tags?, expect = some] ()
1.127 -sledgehammer [type_sys = mangled_tags, expect = some] ()
1.128 -sledgehammer [type_sys = mangled_preds?, expect = some] ()
1.129 -sledgehammer [type_sys = mangled_preds, expect = some] ()
1.130 +sledgehammer [type_enc = erased, expect = none] ()
1.131 +sledgehammer [type_enc = poly_args, expect = none] ()
1.132 +sledgehammer [type_enc = poly_tags?, expect = some] ()
1.133 +sledgehammer [type_enc = poly_tags, expect = some] ()
1.134 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.135 +sledgehammer [type_enc = poly_preds, expect = some] ()
1.136 +sledgehammer [type_enc = mangled_tags?, expect = some] ()
1.137 +sledgehammer [type_enc = mangled_tags, expect = some] ()
1.138 +sledgehammer [type_enc = mangled_preds?, expect = some] ()
1.139 +sledgehammer [type_enc = mangled_preds, expect = some] ()
1.140 by (metis (full_types))
1.141
1.142 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
1.143 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.144 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.145 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.146 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.147 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.148 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.149 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.150 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.151 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.152 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.153 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.154 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.155 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.156 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.157 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.158 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.159 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.160 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.161 by (metis_exhaust id_apply)
1.162
1.163 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
1.164 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.165 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.166 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.167 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.168 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.169 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.170 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.171 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.172 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.173 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.174 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.175 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.176 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.177 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.178 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.179 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.180 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.181 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.182 by (metis_exhaust id_apply)
1.183
1.184 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
1.185 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.186 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.187 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.188 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.189 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.190 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.191 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.192 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.193 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.194 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.195 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.196 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.197 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.198 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.199 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.200 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.201 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.202 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.203 by (metis_exhaust id_apply)
1.204
1.205 lemma "id (a \<and> b) \<Longrightarrow> id a"
1.206 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.207 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.208 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.209 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.210 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.211 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.212 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.213 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.214 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.215 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.216 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.217 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.218 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.219 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.220 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.221 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.222 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.223 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.224 by (metis_exhaust id_apply)
1.225
1.226 lemma "id (a \<and> b) \<Longrightarrow> id b"
1.227 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.228 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.229 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.230 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.231 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.232 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.233 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.234 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.235 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.236 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.237 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.238 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.239 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.240 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.241 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.242 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.243 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.244 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.245 by (metis_exhaust id_apply)
1.246
1.247 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
1.248 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.249 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.250 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.251 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.252 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.253 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.254 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.255 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.256 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.257 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.258 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.259 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.260 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.261 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.262 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.263 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.264 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.265 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.266 by (metis_exhaust id_apply)
1.267
1.268 lemma "id a \<Longrightarrow> id (a \<or> b)"
1.269 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.270 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.271 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.272 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.273 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.274 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.275 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.276 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.277 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.278 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.279 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.280 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.281 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.282 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.283 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.284 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.285 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.286 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.287 by (metis_exhaust id_apply)
1.288
1.289 lemma "id b \<Longrightarrow> id (a \<or> b)"
1.290 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.291 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.292 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.293 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.294 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.295 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.296 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.297 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.298 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.299 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.300 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.301 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.302 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.303 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.304 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.305 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.306 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.307 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.308 by (metis_exhaust id_apply)
1.309
1.310 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
1.311 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.312 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.313 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.314 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.315 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.316 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.317 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.318 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.319 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.320 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.321 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.322 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.323 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.324 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.325 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.326 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.327 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.328 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.329 by (metis_exhaust id_apply)
1.330
1.331 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
1.332 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.333 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.334 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.335 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.336 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.337 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.338 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.339 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.340 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.341 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.342 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.343 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.344 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.345 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.346 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.347 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.348 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.349 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.350 by (metis_exhaust id_apply)
1.351
1.352 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
1.353 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.354 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.355 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.356 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.357 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.358 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.359 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.360 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.361 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.362 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.363 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.364 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.365 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.366 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.367 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.368 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.369 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.370 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.371 by (metis_exhaust id_apply)
1.372
1.373 end
2.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 15:53:37 2011 +0200
2.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jul 01 15:53:38 2011 +0200
2.3 @@ -24,7 +24,7 @@
2.4 ML {*
2.5 (* The commented-out type systems are too incomplete for our exhaustive
2.6 tests. *)
2.7 -val type_syss =
2.8 +val type_encs =
2.9 ["erased",
2.10 "poly_preds",
2.11 "poly_preds_heavy",
2.12 @@ -72,18 +72,18 @@
2.13 fun metis_exhaust_tac ctxt ths =
2.14 let
2.15 fun tac [] st = all_tac st
2.16 - | tac (type_sys :: type_syss) st =
2.17 - st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
2.18 - |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
2.19 - THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1
2.20 + | tac (type_enc :: type_encs) st =
2.21 + st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
2.22 + |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
2.23 + THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1
2.24 THEN COND (has_fewer_prems 2) all_tac no_tac
2.25 - THEN tac type_syss)
2.26 + THEN tac type_encs)
2.27 in tac end
2.28 *}
2.29
2.30 method_setup metis_exhaust = {*
2.31 Attrib.thms >>
2.32 - (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
2.33 + (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))
2.34 *} "exhaustively run the new Metis with all type encodings"
2.35
2.36
3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 01 15:53:37 2011 +0200
3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 01 15:53:38 2011 +0200
3.3 @@ -8,7 +8,7 @@
3.4 val proverK = "prover"
3.5 val prover_timeoutK = "prover_timeout"
3.6 val keepK = "keep"
3.7 -val type_sysK = "type_sys"
3.8 +val type_encK = "type_enc"
3.9 val slicingK = "slicing"
3.10 val e_weight_methodK = "e_weight_method"
3.11 val spass_force_sosK = "spass_force_sos"
3.12 @@ -353,7 +353,7 @@
3.13 SH_FAIL of int * int |
3.14 SH_ERROR
3.15
3.16 -fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
3.17 +fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
3.18 vampire_force_sos hard_timeout timeout dir st =
3.19 let
3.20 val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
3.21 @@ -377,7 +377,7 @@
3.22 val params as {relevance_thresholds, max_relevant, slicing, ...} =
3.23 Sledgehammer_Isar.default_params ctxt
3.24 [("verbose", "true"),
3.25 - ("type_sys", type_sys),
3.26 + ("type_enc", type_enc),
3.27 ("max_relevant", max_relevant),
3.28 ("slicing", slicing),
3.29 ("timeout", string_of_int timeout)]
3.30 @@ -452,7 +452,7 @@
3.31 val _ = change_data id inc_sh_calls
3.32 val _ = if trivial then () else change_data id inc_sh_nontriv_calls
3.33 val (prover_name, prover) = get_prover (Proof.context_of st) args
3.34 - val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
3.35 + val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
3.36 val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
3.37 val slicing = AList.lookup (op =) args slicingK |> the_default "true"
3.38 val e_weight_method = AList.lookup (op =) args e_weight_methodK
3.39 @@ -466,7 +466,7 @@
3.40 minimizer has a chance to do its magic *)
3.41 val hard_timeout = SOME (2 * timeout)
3.42 val (msg, result) =
3.43 - run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos
3.44 + run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
3.45 vampire_force_sos hard_timeout timeout dir st
3.46 in
3.47 case result of
3.48 @@ -503,7 +503,7 @@
3.49 val ctxt = Proof.context_of st
3.50 val n0 = length (these (!named_thms))
3.51 val (prover_name, _) = get_prover ctxt args
3.52 - val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
3.53 + val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
3.54 val timeout =
3.55 AList.lookup (op =) args minimize_timeoutK
3.56 |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
3.57 @@ -511,7 +511,7 @@
3.58 val params = Sledgehammer_Isar.default_params ctxt
3.59 [("provers", prover_name),
3.60 ("verbose", "true"),
3.61 - ("type_sys", type_sys),
3.62 + ("type_enc", type_enc),
3.63 ("timeout", string_of_int timeout)]
3.64 val minimize =
3.65 Sledgehammer_Minimize.minimize_facts prover_name params
3.66 @@ -546,9 +546,9 @@
3.67 else if !reconstructor = "smt" then
3.68 SMT_Solver.smt_tac
3.69 else if full orelse !reconstructor = "metis (full_types)" then
3.70 - Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
3.71 + Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
3.72 else if !reconstructor = "metis (no_types)" then
3.73 - Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
3.74 + Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
3.75 else
3.76 Metis_Tactics.metis_tac []) ctxt thms
3.77 fun apply_reconstructor thms =
4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 01 15:53:37 2011 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 01 15:53:38 2011 +0200
4.3 @@ -386,8 +386,8 @@
4.4 prem_kind = prem_kind,
4.5 formats = formats,
4.6 best_slices = fn ctxt =>
4.7 - let val (max_relevant, type_sys) = best_slice ctxt in
4.8 - [(1.0, (false, (max_relevant, type_sys, "")))]
4.9 + let val (max_relevant, type_enc) = best_slice ctxt in
4.10 + [(1.0, (false, (max_relevant, type_enc, "")))]
4.11 end}
4.12
4.13 fun remotify_config system_name system_versions best_slice
5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:37 2011 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:38 2011 +0200
5.3 @@ -26,7 +26,7 @@
5.4 No_Types
5.5 datatype type_heaviness = Heavyweight | Lightweight
5.6
5.7 - datatype type_sys =
5.8 + datatype type_enc =
5.9 Simple_Types of order * type_level |
5.10 Preds of polymorphism * type_level * type_heaviness |
5.11 Tags of polymorphism * type_level * type_heaviness
5.12 @@ -75,12 +75,12 @@
5.13 val atp_irrelevant_consts : string list
5.14 val atp_schematic_consts_of : term -> typ list Symtab.table
5.15 val is_locality_global : locality -> bool
5.16 - val type_sys_from_string : string -> type_sys
5.17 - val polymorphism_of_type_sys : type_sys -> polymorphism
5.18 - val level_of_type_sys : type_sys -> type_level
5.19 - val is_type_sys_virtually_sound : type_sys -> bool
5.20 - val is_type_sys_fairly_sound : type_sys -> bool
5.21 - val choose_format : format list -> type_sys -> format * type_sys
5.22 + val type_enc_from_string : string -> type_enc
5.23 + val polymorphism_of_type_enc : type_enc -> polymorphism
5.24 + val level_of_type_enc : type_enc -> type_level
5.25 + val is_type_enc_virtually_sound : type_enc -> bool
5.26 + val is_type_enc_fairly_sound : type_enc -> bool
5.27 + val choose_format : format list -> type_enc -> format * type_enc
5.28 val mk_aconns :
5.29 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
5.30 val unmangled_const : string -> string * string fo_term list
5.31 @@ -88,7 +88,7 @@
5.32 val helper_table : ((string * bool) * thm list) list
5.33 val factsN : string
5.34 val prepare_atp_problem :
5.35 - Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
5.36 + Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
5.37 -> bool -> bool -> bool -> term list -> term
5.38 -> ((string * locality) * term) list
5.39 -> string problem * string Symtab.table * int * int
5.40 @@ -509,7 +509,7 @@
5.41 No_Types
5.42 datatype type_heaviness = Heavyweight | Lightweight
5.43
5.44 -datatype type_sys =
5.45 +datatype type_enc =
5.46 Simple_Types of order * type_level |
5.47 Preds of polymorphism * type_level * type_heaviness |
5.48 Tags of polymorphism * type_level * type_heaviness
5.49 @@ -517,7 +517,7 @@
5.50 fun try_unsuffixes ss s =
5.51 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
5.52
5.53 -fun type_sys_from_string s =
5.54 +fun type_enc_from_string s =
5.55 (case try (unprefix "poly_") s of
5.56 SOME s => (SOME Polymorphic, s)
5.57 | NONE =>
5.58 @@ -557,29 +557,29 @@
5.59 | _ => raise Same.SAME)
5.60 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
5.61
5.62 -fun is_type_sys_higher_order (Simple_Types (Higher_Order, _)) = true
5.63 - | is_type_sys_higher_order _ = false
5.64 +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
5.65 + | is_type_enc_higher_order _ = false
5.66
5.67 -fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
5.68 - | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
5.69 - | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
5.70 +fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
5.71 + | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
5.72 + | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
5.73
5.74 -fun level_of_type_sys (Simple_Types (_, level)) = level
5.75 - | level_of_type_sys (Preds (_, level, _)) = level
5.76 - | level_of_type_sys (Tags (_, level, _)) = level
5.77 +fun level_of_type_enc (Simple_Types (_, level)) = level
5.78 + | level_of_type_enc (Preds (_, level, _)) = level
5.79 + | level_of_type_enc (Tags (_, level, _)) = level
5.80
5.81 -fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
5.82 - | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
5.83 - | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
5.84 +fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
5.85 + | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
5.86 + | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
5.87
5.88 fun is_type_level_virtually_sound level =
5.89 level = All_Types orelse level = Noninf_Nonmono_Types
5.90 -val is_type_sys_virtually_sound =
5.91 - is_type_level_virtually_sound o level_of_type_sys
5.92 +val is_type_enc_virtually_sound =
5.93 + is_type_level_virtually_sound o level_of_type_enc
5.94
5.95 fun is_type_level_fairly_sound level =
5.96 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
5.97 -val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
5.98 +val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
5.99
5.100 fun choose_format formats (Simple_Types (order, level)) =
5.101 if member (op =) formats THF then
5.102 @@ -588,15 +588,15 @@
5.103 (TFF, Simple_Types (First_Order, level))
5.104 else
5.105 choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
5.106 - | choose_format formats type_sys =
5.107 + | choose_format formats type_enc =
5.108 (case hd formats of
5.109 CNF_UEQ =>
5.110 - (CNF_UEQ, case type_sys of
5.111 + (CNF_UEQ, case type_enc of
5.112 Preds stuff =>
5.113 - (if is_type_sys_fairly_sound type_sys then Tags else Preds)
5.114 + (if is_type_enc_fairly_sound type_enc then Tags else Preds)
5.115 stuff
5.116 - | _ => type_sys)
5.117 - | format => (format, type_sys))
5.118 + | _ => type_enc)
5.119 + | format => (format, type_enc))
5.120
5.121 type translated_formula =
5.122 {name : string,
5.123 @@ -628,30 +628,30 @@
5.124
5.125 fun should_drop_arg_type_args (Simple_Types _) =
5.126 false (* since TFF doesn't support overloading *)
5.127 - | should_drop_arg_type_args type_sys =
5.128 - level_of_type_sys type_sys = All_Types andalso
5.129 - heaviness_of_type_sys type_sys = Heavyweight
5.130 + | should_drop_arg_type_args type_enc =
5.131 + level_of_type_enc type_enc = All_Types andalso
5.132 + heaviness_of_type_enc type_enc = Heavyweight
5.133
5.134 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
5.135 - | general_type_arg_policy type_sys =
5.136 - if level_of_type_sys type_sys = No_Types then
5.137 + | general_type_arg_policy type_enc =
5.138 + if level_of_type_enc type_enc = No_Types then
5.139 No_Type_Args
5.140 - else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
5.141 - Mangled_Type_Args (should_drop_arg_type_args type_sys)
5.142 + else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
5.143 + Mangled_Type_Args (should_drop_arg_type_args type_enc)
5.144 else
5.145 - Explicit_Type_Args (should_drop_arg_type_args type_sys)
5.146 + Explicit_Type_Args (should_drop_arg_type_args type_enc)
5.147
5.148 -fun type_arg_policy type_sys s =
5.149 +fun type_arg_policy type_enc s =
5.150 if s = @{const_name HOL.eq} orelse
5.151 - (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
5.152 + (s = app_op_name andalso level_of_type_enc type_enc = Const_Arg_Types) then
5.153 No_Type_Args
5.154 else if s = type_tag_name then
5.155 - (if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
5.156 + (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
5.157 Mangled_Type_Args
5.158 else
5.159 Explicit_Type_Args) false
5.160 else
5.161 - general_type_arg_policy type_sys
5.162 + general_type_arg_policy type_enc
5.163
5.164 (*Make literals for sorted type variables*)
5.165 fun generic_add_sorts_on_type (_, []) = I
5.166 @@ -669,8 +669,8 @@
5.167 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
5.168 | add_sorts_on_tvar _ = I
5.169
5.170 -fun type_literals_for_types type_sys add_sorts_on_typ Ts =
5.171 - [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
5.172 +fun type_literals_for_types type_enc add_sorts_on_typ Ts =
5.173 + [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
5.174
5.175 fun mk_aconns c phis =
5.176 let val (phis', phi') = split_last phis in
5.177 @@ -705,10 +705,10 @@
5.178 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
5.179 val homo_infinite_type = Type (homo_infinite_type_name, [])
5.180
5.181 -fun fo_term_from_typ format type_sys =
5.182 +fun fo_term_from_typ format type_enc =
5.183 let
5.184 fun term (Type (s, Ts)) =
5.185 - ATerm (case (is_type_sys_higher_order type_sys, s) of
5.186 + ATerm (case (is_type_enc_higher_order type_enc, s) of
5.187 (true, @{type_name bool}) => `I tptp_bool_type
5.188 | (true, @{type_name fun}) => `I tptp_fun_type
5.189 | _ => if s = homo_infinite_type_name andalso
5.190 @@ -722,8 +722,8 @@
5.191 ATerm ((make_schematic_type_var x, s), [])
5.192 in term end
5.193
5.194 -fun fo_term_for_type_arg format type_sys T =
5.195 - if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
5.196 +fun fo_term_for_type_arg format type_enc T =
5.197 + if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
5.198
5.199 (* This shouldn't clash with anything else. *)
5.200 val mangled_type_sep = "\000"
5.201 @@ -742,7 +742,7 @@
5.202 else
5.203 simple_type_prefix ^ ascii_of s
5.204
5.205 -fun ho_type_from_fo_term type_sys pred_sym ary =
5.206 +fun ho_type_from_fo_term type_enc pred_sym ary =
5.207 let
5.208 fun to_atype ty =
5.209 AType ((make_simple_type (generic_mangled_type_name fst ty),
5.210 @@ -752,15 +752,15 @@
5.211 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
5.212 fun to_ho (ty as ATerm ((s, _), tys)) =
5.213 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
5.214 - in if is_type_sys_higher_order type_sys then to_ho else to_fo ary end
5.215 + in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
5.216
5.217 -fun mangled_type format type_sys pred_sym ary =
5.218 - ho_type_from_fo_term type_sys pred_sym ary
5.219 - o fo_term_from_typ format type_sys
5.220 +fun mangled_type format type_enc pred_sym ary =
5.221 + ho_type_from_fo_term type_enc pred_sym ary
5.222 + o fo_term_from_typ format type_enc
5.223
5.224 -fun mangled_const_name format type_sys T_args (s, s') =
5.225 +fun mangled_const_name format type_enc T_args (s, s') =
5.226 let
5.227 - val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
5.228 + val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
5.229 fun type_suffix f g =
5.230 fold_rev (curry (op ^) o g o prefix mangled_type_sep
5.231 o generic_mangled_type_name f) ty_args ""
5.232 @@ -789,14 +789,14 @@
5.233 (hd ss, map unmangled_type (tl ss))
5.234 end
5.235
5.236 -fun introduce_proxies type_sys =
5.237 +fun introduce_proxies type_enc =
5.238 let
5.239 fun intro top_level (CombApp (tm1, tm2)) =
5.240 CombApp (intro top_level tm1, intro false tm2)
5.241 | intro top_level (CombConst (name as (s, _), T, T_args)) =
5.242 (case proxify_const s of
5.243 SOME proxy_base =>
5.244 - if top_level orelse is_type_sys_higher_order type_sys then
5.245 + if top_level orelse is_type_enc_higher_order type_enc then
5.246 case (top_level, s) of
5.247 (_, "c_False") => (`I tptp_false, [])
5.248 | (_, "c_True") => (`I tptp_true, [])
5.249 @@ -815,11 +815,11 @@
5.250 | intro _ tm = tm
5.251 in intro true end
5.252
5.253 -fun combformula_from_prop thy type_sys eq_as_iff =
5.254 +fun combformula_from_prop thy type_enc eq_as_iff =
5.255 let
5.256 fun do_term bs t atomic_types =
5.257 combterm_from_term thy bs (Envir.eta_contract t)
5.258 - |>> (introduce_proxies type_sys #> AAtom)
5.259 + |>> (introduce_proxies type_enc #> AAtom)
5.260 ||> union (op =) atomic_types
5.261 fun do_quant bs q s T t' =
5.262 let val s = singleton (Name.variant_list (map fst bs)) s in
5.263 @@ -940,27 +940,27 @@
5.264 end
5.265
5.266 (* making fact and conjecture formulas *)
5.267 -fun make_formula thy type_sys eq_as_iff name loc kind t =
5.268 +fun make_formula thy type_enc eq_as_iff name loc kind t =
5.269 let
5.270 val (combformula, atomic_types) =
5.271 - combformula_from_prop thy type_sys eq_as_iff t []
5.272 + combformula_from_prop thy type_enc eq_as_iff t []
5.273 in
5.274 {name = name, locality = loc, kind = kind, combformula = combformula,
5.275 atomic_types = atomic_types}
5.276 end
5.277
5.278 -fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
5.279 +fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
5.280 ((name, loc), t) =
5.281 let val thy = Proof_Context.theory_of ctxt in
5.282 case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
5.283 - |> make_formula thy type_sys (eq_as_iff andalso format <> CNF) name
5.284 + |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
5.285 loc Axiom of
5.286 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
5.287 if s = tptp_true then NONE else SOME formula
5.288 | formula => SOME formula
5.289 end
5.290
5.291 -fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
5.292 +fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
5.293 let
5.294 val thy = Proof_Context.theory_of ctxt
5.295 val last = length ts - 1
5.296 @@ -977,7 +977,7 @@
5.297 in
5.298 t |> preproc ?
5.299 (preprocess_prop ctxt presimp_consts kind #> freeze_term)
5.300 - |> make_formula thy type_sys (format <> CNF) (string_of_int j)
5.301 + |> make_formula thy type_enc (format <> CNF) (string_of_int j)
5.302 Local kind
5.303 |> maybe_negate
5.304 end)
5.305 @@ -1231,7 +1231,7 @@
5.306 end
5.307 handle TYPE _ => T_args
5.308
5.309 -fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
5.310 +fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
5.311 let
5.312 val thy = Proof_Context.theory_of ctxt
5.313 fun aux arity (CombApp (tm1, tm2)) =
5.314 @@ -1245,11 +1245,11 @@
5.315 fun filtered_T_args false = T_args
5.316 | filtered_T_args true = filter_type_args thy s'' arity T_args
5.317 in
5.318 - case type_arg_policy type_sys s'' of
5.319 + case type_arg_policy type_enc s'' of
5.320 Explicit_Type_Args drop_args =>
5.321 (name, filtered_T_args drop_args)
5.322 | Mangled_Type_Args drop_args =>
5.323 - (mangled_const_name format type_sys (filtered_T_args drop_args)
5.324 + (mangled_const_name format type_enc (filtered_T_args drop_args)
5.325 name, [])
5.326 | No_Type_Args => (name, [])
5.327 end)
5.328 @@ -1257,14 +1257,14 @@
5.329 | aux _ tm = tm
5.330 in aux 0 end
5.331
5.332 -fun repair_combterm ctxt format type_sys sym_tab =
5.333 - not (is_type_sys_higher_order type_sys)
5.334 +fun repair_combterm ctxt format type_enc sym_tab =
5.335 + not (is_type_enc_higher_order type_enc)
5.336 ? (introduce_explicit_apps_in_combterm sym_tab
5.337 #> introduce_predicators_in_combterm sym_tab)
5.338 - #> enforce_type_arg_policy_in_combterm ctxt format type_sys
5.339 -fun repair_fact ctxt format type_sys sym_tab =
5.340 + #> enforce_type_arg_policy_in_combterm ctxt format type_enc
5.341 +fun repair_fact ctxt format type_enc sym_tab =
5.342 update_combformula (formula_map
5.343 - (repair_combterm ctxt format type_sys sym_tab))
5.344 + (repair_combterm ctxt format type_enc sym_tab))
5.345
5.346 (** Helper facts **)
5.347
5.348 @@ -1313,12 +1313,12 @@
5.349 |> close_formula_universally, simp_info, NONE)
5.350 end
5.351
5.352 -fun should_specialize_helper type_sys t =
5.353 - case general_type_arg_policy type_sys of
5.354 +fun should_specialize_helper type_enc t =
5.355 + case general_type_arg_policy type_enc of
5.356 Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
5.357 | _ => false
5.358
5.359 -fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
5.360 +fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
5.361 case strip_prefix_and_unascii const_prefix s of
5.362 SOME mangled_s =>
5.363 let
5.364 @@ -1331,14 +1331,14 @@
5.365 else untyped_helper_suffix),
5.366 Helper),
5.367 let val t = th |> prop_of in
5.368 - t |> should_specialize_helper type_sys t
5.369 + t |> should_specialize_helper type_enc t
5.370 ? (case types of
5.371 [T] => specialize_type thy (invert_const unmangled_s, T)
5.372 | _ => I)
5.373 end)
5.374 val make_facts =
5.375 - map_filter (make_fact ctxt format type_sys false false [])
5.376 - val fairly_sound = is_type_sys_fairly_sound type_sys
5.377 + map_filter (make_fact ctxt format type_enc false false [])
5.378 + val fairly_sound = is_type_enc_fairly_sound type_enc
5.379 in
5.380 helper_table
5.381 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
5.382 @@ -1351,8 +1351,8 @@
5.383 |> make_facts)
5.384 end
5.385 | NONE => []
5.386 -fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
5.387 - Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
5.388 +fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
5.389 + Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
5.390 []
5.391
5.392 (***************************************************************)
5.393 @@ -1393,13 +1393,13 @@
5.394 fun type_constrs_of_terms thy ts =
5.395 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
5.396
5.397 -fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
5.398 +fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
5.399 facts =
5.400 let
5.401 val thy = Proof_Context.theory_of ctxt
5.402 val fact_ts = facts |> map snd
5.403 val presimp_consts = Meson.presimplified_consts ctxt
5.404 - val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
5.405 + val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
5.406 val (facts, fact_names) =
5.407 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
5.408 |> map_filter (try (apfst the))
5.409 @@ -1416,9 +1416,9 @@
5.410 val tycons = type_constrs_of_terms thy all_ts
5.411 val conjs =
5.412 hyp_ts @ [concl_t]
5.413 - |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
5.414 + |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
5.415 val (supers', arity_clauses) =
5.416 - if level_of_type_sys type_sys = No_Types then ([], [])
5.417 + if level_of_type_enc type_enc = No_Types then ([], [])
5.418 else make_arity_clauses thy tycons supers
5.419 val class_rel_clauses = make_class_rel_clauses thy subs supers'
5.420 in
5.421 @@ -1434,9 +1434,9 @@
5.422
5.423 val type_pred = `make_fixed_const type_pred_name
5.424
5.425 -fun type_pred_combterm ctxt format type_sys T tm =
5.426 +fun type_pred_combterm ctxt format type_enc T tm =
5.427 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
5.428 - |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
5.429 + |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
5.430
5.431 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
5.432 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
5.433 @@ -1445,15 +1445,15 @@
5.434 formula_fold pos (is_var_positively_naked_in_term name) phi false
5.435 | should_predicate_on_var_in_formula _ _ _ _ = true
5.436
5.437 -fun mk_const_aterm format type_sys x T_args args =
5.438 - ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
5.439 +fun mk_const_aterm format type_enc x T_args args =
5.440 + ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
5.441
5.442 -fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
5.443 +fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
5.444 CombConst (type_tag, T --> T, [T])
5.445 - |> enforce_type_arg_policy_in_combterm ctxt format type_sys
5.446 - |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
5.447 + |> enforce_type_arg_policy_in_combterm ctxt format type_enc
5.448 + |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
5.449 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
5.450 -and term_from_combterm ctxt format nonmono_Ts type_sys =
5.451 +and term_from_combterm ctxt format nonmono_Ts type_enc =
5.452 let
5.453 fun aux site u =
5.454 let
5.455 @@ -1469,32 +1469,32 @@
5.456 (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
5.457 | Eq_Arg pos => (pos, Elsewhere)
5.458 | Elsewhere => (NONE, Elsewhere)
5.459 - val t = mk_const_aterm format type_sys x T_args
5.460 + val t = mk_const_aterm format type_enc x T_args
5.461 (map (aux arg_site) args)
5.462 val T = combtyp_of u
5.463 in
5.464 - t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
5.465 - tag_with_type ctxt format nonmono_Ts type_sys pos T
5.466 + t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
5.467 + tag_with_type ctxt format nonmono_Ts type_enc pos T
5.468 else
5.469 I)
5.470 end
5.471 in aux end
5.472 -and formula_from_combformula ctxt format nonmono_Ts type_sys
5.473 +and formula_from_combformula ctxt format nonmono_Ts type_enc
5.474 should_predicate_on_var =
5.475 let
5.476 fun do_term pos =
5.477 - term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
5.478 + term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
5.479 val do_bound_type =
5.480 - case type_sys of
5.481 + case type_enc of
5.482 Simple_Types (_, level) =>
5.483 homogenized_type ctxt nonmono_Ts level 0
5.484 - #> mangled_type format type_sys false 0 #> SOME
5.485 + #> mangled_type format type_enc false 0 #> SOME
5.486 | _ => K NONE
5.487 fun do_out_of_bound_type pos phi universal (name, T) =
5.488 - if should_predicate_on_type ctxt nonmono_Ts type_sys
5.489 + if should_predicate_on_type ctxt nonmono_Ts type_enc
5.490 (fn () => should_predicate_on_var pos phi universal name) T then
5.491 CombVar (name, T)
5.492 - |> type_pred_combterm ctxt format type_sys T
5.493 + |> type_pred_combterm ctxt format type_enc T
5.494 |> do_term pos |> AAtom |> SOME
5.495 else
5.496 NONE
5.497 @@ -1517,23 +1517,23 @@
5.498 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
5.499 in do_formula end
5.500
5.501 -fun bound_tvars type_sys Ts =
5.502 +fun bound_tvars type_enc Ts =
5.503 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
5.504 - (type_literals_for_types type_sys add_sorts_on_tvar Ts))
5.505 + (type_literals_for_types type_enc add_sorts_on_tvar Ts))
5.506
5.507 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
5.508 of monomorphization). The TPTP explicitly forbids name clashes, and some of
5.509 the remote provers might care. *)
5.510 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
5.511 - type_sys (j, {name, locality, kind, combformula, atomic_types}) =
5.512 + type_enc (j, {name, locality, kind, combformula, atomic_types}) =
5.513 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
5.514 kind,
5.515 combformula
5.516 |> close_combformula_universally
5.517 - |> formula_from_combformula ctxt format nonmono_Ts type_sys
5.518 + |> formula_from_combformula ctxt format nonmono_Ts type_enc
5.519 should_predicate_on_var_in_formula
5.520 (if pos then SOME true else NONE)
5.521 - |> bound_tvars type_sys atomic_types
5.522 + |> bound_tvars type_enc atomic_types
5.523 |> close_formula_universally,
5.524 NONE,
5.525 case locality of
5.526 @@ -1566,45 +1566,45 @@
5.527 (fo_literal_from_arity_literal concl_lits))
5.528 |> close_formula_universally, intro_info, NONE)
5.529
5.530 -fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
5.531 +fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
5.532 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
5.533 Formula (conjecture_prefix ^ name, kind,
5.534 - formula_from_combformula ctxt format nonmono_Ts type_sys
5.535 + formula_from_combformula ctxt format nonmono_Ts type_enc
5.536 should_predicate_on_var_in_formula (SOME false)
5.537 (close_combformula_universally combformula)
5.538 - |> bound_tvars type_sys atomic_types
5.539 + |> bound_tvars type_enc atomic_types
5.540 |> close_formula_universally, NONE, NONE)
5.541
5.542 -fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
5.543 - atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
5.544 +fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
5.545 + atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
5.546 |> map fo_literal_from_type_literal
5.547
5.548 fun formula_line_for_free_type j lit =
5.549 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
5.550 formula_from_fo_literal lit, NONE, NONE)
5.551 -fun formula_lines_for_free_types type_sys facts =
5.552 +fun formula_lines_for_free_types type_enc facts =
5.553 let
5.554 - val litss = map (free_type_literals type_sys) facts
5.555 + val litss = map (free_type_literals type_enc) facts
5.556 val lits = fold (union (op =)) litss []
5.557 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
5.558
5.559 (** Symbol declarations **)
5.560
5.561 -fun should_declare_sym type_sys pred_sym s =
5.562 +fun should_declare_sym type_enc pred_sym s =
5.563 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
5.564 - (case type_sys of
5.565 + (case type_enc of
5.566 Simple_Types _ => true
5.567 | Tags (_, _, Lightweight) => true
5.568 | _ => not pred_sym)
5.569
5.570 -fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
5.571 +fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
5.572 let
5.573 fun add_combterm in_conj tm =
5.574 let val (head, args) = strip_combterm_comb tm in
5.575 (case head of
5.576 CombConst ((s, s'), T, T_args) =>
5.577 let val pred_sym = is_pred_sym repaired_sym_tab s in
5.578 - if should_declare_sym type_sys pred_sym s then
5.579 + if should_declare_sym type_enc pred_sym s then
5.580 Symtab.map_default (s, [])
5.581 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
5.582 in_conj))
5.583 @@ -1618,7 +1618,7 @@
5.584 fact_lift (formula_fold NONE (K (add_combterm in_conj)))
5.585 in
5.586 Symtab.empty
5.587 - |> is_type_sys_fairly_sound type_sys
5.588 + |> is_type_enc_fairly_sound type_enc
5.589 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
5.590 end
5.591
5.592 @@ -1641,8 +1641,8 @@
5.593 formula_fold (SOME (kind <> Conjecture))
5.594 (add_combterm_nonmonotonic_types ctxt level sound locality)
5.595 combformula
5.596 -fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
5.597 - let val level = level_of_type_sys type_sys in
5.598 +fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
5.599 + let val level = level_of_type_enc type_enc in
5.600 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
5.601 [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
5.602 (* We must add "bool" in case the helper "True_or_False" is added
5.603 @@ -1653,21 +1653,21 @@
5.604 []
5.605 end
5.606
5.607 -fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
5.608 +fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
5.609 (s', T_args, T, pred_sym, ary, _) =
5.610 let
5.611 val (T_arg_Ts, level) =
5.612 - case type_sys of
5.613 + case type_enc of
5.614 Simple_Types (_, level) => ([], level)
5.615 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
5.616 in
5.617 Decl (sym_decl_prefix ^ s, (s, s'),
5.618 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
5.619 - |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
5.620 + |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
5.621 end
5.622
5.623 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
5.624 - poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
5.625 + poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
5.626 let
5.627 val (kind, maybe_negate) =
5.628 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
5.629 @@ -1681,7 +1681,7 @@
5.630 val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
5.631 fun should_keep_arg_type T =
5.632 sym_needs_arg_types orelse
5.633 - not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
5.634 + not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
5.635 val bound_Ts =
5.636 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
5.637 in
5.638 @@ -1689,18 +1689,18 @@
5.639 (if n > 1 then "_" ^ string_of_int j else ""), kind,
5.640 CombConst ((s, s'), T, T_args)
5.641 |> fold (curry (CombApp o swap)) bounds
5.642 - |> type_pred_combterm ctxt format type_sys res_T
5.643 + |> type_pred_combterm ctxt format type_enc res_T
5.644 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
5.645 - |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
5.646 + |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
5.647 (K (K (K (K true)))) (SOME true)
5.648 - |> n > 1 ? bound_tvars type_sys (atyps_of T)
5.649 + |> n > 1 ? bound_tvars type_enc (atyps_of T)
5.650 |> close_formula_universally
5.651 |> maybe_negate,
5.652 intro_info, NONE)
5.653 end
5.654
5.655 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
5.656 - poly_nonmono_Ts type_sys n s
5.657 + poly_nonmono_Ts type_enc n s
5.658 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
5.659 let
5.660 val ident_base =
5.661 @@ -1713,22 +1713,22 @@
5.662 val bound_names =
5.663 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
5.664 val bounds = bound_names |> map (fn name => ATerm (name, []))
5.665 - val cst = mk_const_aterm format type_sys (s, s') T_args
5.666 + val cst = mk_const_aterm format type_enc (s, s') T_args
5.667 val atomic_Ts = atyps_of T
5.668 fun eq tms =
5.669 (if pred_sym then AConn (AIff, map AAtom tms)
5.670 else AAtom (ATerm (`I tptp_equal, tms)))
5.671 - |> bound_tvars type_sys atomic_Ts
5.672 + |> bound_tvars type_enc atomic_Ts
5.673 |> close_formula_universally
5.674 |> maybe_negate
5.675 (* See also "should_tag_with_type". *)
5.676 fun should_encode T =
5.677 should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
5.678 - (case type_sys of
5.679 + (case type_enc of
5.680 Tags (Polymorphic, level, Lightweight) =>
5.681 level <> All_Types andalso Monomorph.typ_has_tvars T
5.682 | _ => false)
5.683 - val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
5.684 + val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
5.685 val add_formula_for_res =
5.686 if should_encode res_T then
5.687 cons (Formula (ident_base ^ "_res", kind,
5.688 @@ -1757,10 +1757,10 @@
5.689 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
5.690
5.691 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
5.692 - poly_nonmono_Ts type_sys (s, decls) =
5.693 - case type_sys of
5.694 + poly_nonmono_Ts type_enc (s, decls) =
5.695 + case type_enc of
5.696 Simple_Types _ =>
5.697 - decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
5.698 + decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
5.699 | Preds _ =>
5.700 let
5.701 val decls =
5.702 @@ -1776,13 +1776,13 @@
5.703 | _ => decls
5.704 val n = length decls
5.705 val decls =
5.706 - decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
5.707 + decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
5.708 (K true)
5.709 o result_type_of_decl)
5.710 in
5.711 (0 upto length decls - 1, decls)
5.712 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
5.713 - nonmono_Ts poly_nonmono_Ts type_sys n s)
5.714 + nonmono_Ts poly_nonmono_Ts type_enc n s)
5.715 end
5.716 | Tags (_, _, heaviness) =>
5.717 (case heaviness of
5.718 @@ -1791,17 +1791,17 @@
5.719 let val n = length decls in
5.720 (0 upto n - 1 ~~ decls)
5.721 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
5.722 - conj_sym_kind poly_nonmono_Ts type_sys n s)
5.723 + conj_sym_kind poly_nonmono_Ts type_enc n s)
5.724 end)
5.725
5.726 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
5.727 - poly_nonmono_Ts type_sys sym_decl_tab =
5.728 + poly_nonmono_Ts type_enc sym_decl_tab =
5.729 sym_decl_tab
5.730 |> Symtab.dest
5.731 |> sort_wrt fst
5.732 |> rpair []
5.733 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
5.734 - nonmono_Ts poly_nonmono_Ts type_sys)
5.735 + nonmono_Ts poly_nonmono_Ts type_enc)
5.736
5.737 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
5.738 poly <> Mangled_Monomorphic andalso
5.739 @@ -1825,39 +1825,39 @@
5.740
5.741 val explicit_apply = NONE (* for experimental purposes *)
5.742
5.743 -fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
5.744 +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
5.745 exporter readable_names preproc hyp_ts concl_t facts =
5.746 let
5.747 - val (format, type_sys) = choose_format [format] type_sys
5.748 + val (format, type_enc) = choose_format [format] type_enc
5.749 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
5.750 - translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
5.751 + translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
5.752 facts
5.753 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
5.754 val nonmono_Ts =
5.755 - conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
5.756 - val repair = repair_fact ctxt format type_sys sym_tab
5.757 + conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
5.758 + val repair = repair_fact ctxt format type_enc sym_tab
5.759 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
5.760 val repaired_sym_tab =
5.761 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
5.762 val helpers =
5.763 - repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
5.764 + repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
5.765 |> map repair
5.766 val poly_nonmono_Ts =
5.767 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
5.768 - polymorphism_of_type_sys type_sys <> Polymorphic then
5.769 + polymorphism_of_type_enc type_enc <> Polymorphic then
5.770 nonmono_Ts
5.771 else
5.772 [TVar (("'a", 0), HOLogic.typeS)]
5.773 val sym_decl_lines =
5.774 (conjs, helpers @ facts)
5.775 - |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
5.776 + |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
5.777 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
5.778 - poly_nonmono_Ts type_sys
5.779 + poly_nonmono_Ts type_enc
5.780 val helper_lines =
5.781 0 upto length helpers - 1 ~~ helpers
5.782 |> map (formula_line_for_fact ctxt format helper_prefix I false true
5.783 - poly_nonmono_Ts type_sys)
5.784 - |> (if needs_type_tag_idempotence type_sys then
5.785 + poly_nonmono_Ts type_enc)
5.786 + |> (if needs_type_tag_idempotence type_enc then
5.787 cons (type_tag_idempotence_fact ())
5.788 else
5.789 I)
5.790 @@ -1868,15 +1868,15 @@
5.791 (factsN,
5.792 map (formula_line_for_fact ctxt format fact_prefix ascii_of
5.793 (not exporter) (not exporter) nonmono_Ts
5.794 - type_sys)
5.795 + type_enc)
5.796 (0 upto length facts - 1 ~~ facts)),
5.797 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
5.798 (aritiesN, map formula_line_for_arity_clause arity_clauses),
5.799 (helpersN, helper_lines),
5.800 (conjsN,
5.801 - map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
5.802 + map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
5.803 conjs),
5.804 - (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
5.805 + (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
5.806 val problem =
5.807 problem
5.808 |> (case format of
6.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Jul 01 15:53:37 2011 +0200
6.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri Jul 01 15:53:38 2011 +0200
6.3 @@ -13,10 +13,10 @@
6.4 val full_typesN : string
6.5 val partial_typesN : string
6.6 val no_typesN : string
6.7 - val really_full_type_sys : string
6.8 - val full_type_sys : string
6.9 - val partial_type_sys : string
6.10 - val no_type_sys : string
6.11 + val really_full_type_enc : string
6.12 + val full_type_enc : string
6.13 + val partial_type_enc : string
6.14 + val no_type_enc : string
6.15 val full_type_syss : string list
6.16 val partial_type_syss : string list
6.17 val trace : bool Config.T
6.18 @@ -39,22 +39,22 @@
6.19 val partial_typesN = "partial_types"
6.20 val no_typesN = "no_types"
6.21
6.22 -val really_full_type_sys = "poly_tags_heavy"
6.23 -val full_type_sys = "poly_preds_heavy_query"
6.24 -val partial_type_sys = "poly_args"
6.25 -val no_type_sys = "erased"
6.26 +val really_full_type_enc = "poly_tags_heavy"
6.27 +val full_type_enc = "poly_preds_heavy_query"
6.28 +val partial_type_enc = "poly_args"
6.29 +val no_type_enc = "erased"
6.30
6.31 -val full_type_syss = [full_type_sys, really_full_type_sys]
6.32 -val partial_type_syss = partial_type_sys :: full_type_syss
6.33 +val full_type_syss = [full_type_enc, really_full_type_enc]
6.34 +val partial_type_syss = partial_type_enc :: full_type_syss
6.35
6.36 -val type_sys_aliases =
6.37 +val type_enc_aliases =
6.38 [(full_typesN, full_type_syss),
6.39 (partial_typesN, partial_type_syss),
6.40 - (no_typesN, [no_type_sys])]
6.41 + (no_typesN, [no_type_enc])]
6.42
6.43 -fun method_call_for_type_sys type_syss =
6.44 +fun method_call_for_type_enc type_syss =
6.45 metisN ^ " (" ^
6.46 - (case AList.find (op =) type_sys_aliases type_syss of
6.47 + (case AList.find (op =) type_enc_aliases type_syss of
6.48 [alias] => alias
6.49 | _ => hd type_syss) ^ ")"
6.50
6.51 @@ -102,7 +102,7 @@
6.52 val resolution_params = {active = active_params, waiting = waiting_params}
6.53
6.54 (* Main function to start Metis proof and reconstruction *)
6.55 -fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
6.56 +fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
6.57 let val thy = Proof_Context.theory_of ctxt
6.58 val new_skolemizer =
6.59 Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
6.60 @@ -118,7 +118,7 @@
6.61 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
6.62 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
6.63 val (sym_tab, axioms, old_skolems) =
6.64 - prepare_metis_problem ctxt type_sys cls ths
6.65 + prepare_metis_problem ctxt type_enc cls ths
6.66 fun get_isa_thm mth Isa_Reflexive_or_Trivial =
6.67 reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
6.68 | get_isa_thm _ (Isa_Raw ith) = ith
6.69 @@ -126,7 +126,7 @@
6.70 val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
6.71 val thms = axioms |> map fst
6.72 val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
6.73 - val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
6.74 + val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
6.75 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
6.76 in
6.77 case filter (fn t => prop_of t aconv @{prop False}) cls of
6.78 @@ -186,7 +186,7 @@
6.79 | _ =>
6.80 (verbose_warning ctxt
6.81 ("Falling back on " ^
6.82 - quote (method_call_for_type_sys fallback_type_syss) ^ "...");
6.83 + quote (method_call_for_type_enc fallback_type_syss) ^ "...");
6.84 FOL_SOLVE fallback_type_syss ctxt cls ths0)
6.85
6.86 val neg_clausify =
6.87 @@ -249,7 +249,7 @@
6.88
6.89 fun setup_method (binding, type_syss) =
6.90 ((Args.parens (Scan.repeat Parse.short_ident)
6.91 - >> maps (fn s => case AList.lookup (op =) type_sys_aliases s of
6.92 + >> maps (fn s => case AList.lookup (op =) type_enc_aliases s of
6.93 SOME tss => tss
6.94 | NONE => [s]))
6.95 |> Scan.option |> Scan.lift)
7.1 --- a/src/HOL/Tools/Metis/metis_translate.ML Fri Jul 01 15:53:37 2011 +0200
7.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Jul 01 15:53:38 2011 +0200
7.3 @@ -165,11 +165,11 @@
7.4 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
7.5
7.6 (* Function to generate metis clauses, including comb and type clauses *)
7.7 -fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
7.8 +fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
7.9 let
7.10 - val type_sys = type_sys_from_string type_sys
7.11 + val type_enc = type_enc_from_string type_enc
7.12 val (conj_clauses, fact_clauses) =
7.13 - if polymorphism_of_type_sys type_sys = Polymorphic then
7.14 + if polymorphism_of_type_enc type_enc = Polymorphic then
7.15 (conj_clauses, fact_clauses)
7.16 else
7.17 conj_clauses @ fact_clauses
7.18 @@ -196,7 +196,7 @@
7.19 tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
7.20 *)
7.21 val (atp_problem, _, _, _, _, _, sym_tab) =
7.22 - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false
7.23 + prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false
7.24 false [] @{prop False} props
7.25 (*
7.26 val _ = tracing ("ATP PROBLEM: " ^
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 01 15:53:37 2011 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 01 15:53:38 2011 +0200
8.3 @@ -84,7 +84,7 @@
8.4 ("verbose", "false"),
8.5 ("overlord", "false"),
8.6 ("blocking", "false"),
8.7 - ("type_sys", "smart"),
8.8 + ("type_enc", "smart"),
8.9 ("sound", "false"),
8.10 ("relevance_thresholds", "0.45 0.85"),
8.11 ("max_relevant", "smart"),
8.12 @@ -107,7 +107,7 @@
8.13 ("no_slicing", "slicing")]
8.14
8.15 val params_for_minimize =
8.16 - ["debug", "verbose", "overlord", "type_sys", "sound", "max_mono_iters",
8.17 + ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
8.18 "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
8.19 "preplay_timeout"]
8.20
8.21 @@ -124,15 +124,15 @@
8.22 ss as _ :: _ => forall (is_prover_supported ctxt) ss
8.23 | _ => false
8.24
8.25 -(* "provers =" and "type_sys =" can be left out. The latter is a secret
8.26 +(* "provers =" and "type_enc =" can be left out. The latter is a secret
8.27 feature. *)
8.28 fun check_and_repair_raw_param ctxt (name, value) =
8.29 if is_known_raw_param name then
8.30 (name, value)
8.31 else if is_prover_list ctxt name andalso null value then
8.32 ("provers", [name])
8.33 - else if can type_sys_from_string name andalso null value then
8.34 - ("type_sys", [name])
8.35 + else if can type_enc_from_string name andalso null value then
8.36 + ("type_enc", [name])
8.37 else
8.38 error ("Unknown parameter: " ^ quote name ^ ".")
8.39
8.40 @@ -264,12 +264,12 @@
8.41 lookup_bool "blocking"
8.42 val provers = lookup_string "provers" |> space_explode " "
8.43 |> mode = Auto_Try ? single o hd
8.44 - val type_sys =
8.45 + val type_enc =
8.46 if mode = Auto_Try then
8.47 NONE
8.48 - else case lookup_string "type_sys" of
8.49 + else case lookup_string "type_enc" of
8.50 "smart" => NONE
8.51 - | s => SOME (type_sys_from_string s)
8.52 + | s => SOME (type_enc_from_string s)
8.53 val sound = mode = Auto_Try orelse lookup_bool "sound"
8.54 val relevance_thresholds = lookup_real_pair "relevance_thresholds"
8.55 val max_relevant = lookup_option lookup_int "max_relevant"
8.56 @@ -288,7 +288,7 @@
8.57 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
8.58 provers = provers, relevance_thresholds = relevance_thresholds,
8.59 max_relevant = max_relevant, max_mono_iters = max_mono_iters,
8.60 - max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
8.61 + max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
8.62 sound = sound, isar_proof = isar_proof,
8.63 isar_shrink_factor = isar_shrink_factor, slicing = slicing,
8.64 timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 01 15:53:37 2011 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 01 15:53:38 2011 +0200
9.3 @@ -47,7 +47,7 @@
9.4 fun print silent f = if silent then () else Output.urgent_message (f ())
9.5
9.6 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
9.7 - max_new_mono_instances, type_sys, isar_proof,
9.8 + max_new_mono_instances, type_enc, isar_proof,
9.9 isar_shrink_factor, preplay_timeout, ...} : params)
9.10 silent (prover : prover) timeout i n state facts =
9.11 let
9.12 @@ -59,7 +59,7 @@
9.13 val {goal, ...} = Proof.goal state
9.14 val params =
9.15 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
9.16 - provers = provers, type_sys = type_sys, sound = true,
9.17 + provers = provers, type_enc = type_enc, sound = true,
9.18 relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
9.19 max_mono_iters = max_mono_iters,
9.20 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 01 15:53:37 2011 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 01 15:53:38 2011 +0200
10.3 @@ -10,7 +10,7 @@
10.4 sig
10.5 type failure = ATP_Proof.failure
10.6 type locality = ATP_Translate.locality
10.7 - type type_sys = ATP_Translate.type_sys
10.8 + type type_enc = ATP_Translate.type_enc
10.9 type reconstructor = ATP_Reconstruct.reconstructor
10.10 type play = ATP_Reconstruct.play
10.11 type minimize_command = ATP_Reconstruct.minimize_command
10.12 @@ -24,7 +24,7 @@
10.13 overlord: bool,
10.14 blocking: bool,
10.15 provers: string list,
10.16 - type_sys: type_sys option,
10.17 + type_enc: type_enc option,
10.18 sound: bool,
10.19 relevance_thresholds: real * real,
10.20 max_relevant: int option,
10.21 @@ -289,7 +289,7 @@
10.22 overlord: bool,
10.23 blocking: bool,
10.24 provers: string list,
10.25 - type_sys: type_sys option,
10.26 + type_enc: type_enc option,
10.27 sound: bool,
10.28 relevance_thresholds: real * real,
10.29 max_relevant: int option,
10.30 @@ -407,11 +407,11 @@
10.31 in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
10.32
10.33 fun tac_for_reconstructor Metis =
10.34 - Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
10.35 + Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
10.36 | tac_for_reconstructor Metis_Full_Types =
10.37 Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
10.38 | tac_for_reconstructor Metis_No_Types =
10.39 - Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
10.40 + Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
10.41 | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
10.42
10.43 fun timed_reconstructor reconstructor debug timeout ths =
10.44 @@ -504,10 +504,10 @@
10.45 them each time. *)
10.46 val atp_important_message_keep_quotient = 10
10.47
10.48 -fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
10.49 - (case type_sys_opt of
10.50 +fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
10.51 + (case type_enc_opt of
10.52 SOME ts => ts
10.53 - | NONE => type_sys_from_string best_type_sys)
10.54 + | NONE => type_enc_from_string best_type_enc)
10.55 |> choose_format formats
10.56
10.57 val metis_minimize_max_time = seconds 2.0
10.58 @@ -530,7 +530,7 @@
10.59 fun run_atp mode name
10.60 ({exec, required_execs, arguments, proof_delims, known_failures,
10.61 conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
10.62 - ({debug, verbose, overlord, type_sys, sound, max_relevant,
10.63 + ({debug, verbose, overlord, type_enc, sound, max_relevant,
10.64 max_mono_iters, max_new_mono_instances, isar_proof,
10.65 isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
10.66 minimize_command
10.67 @@ -598,21 +598,21 @@
10.68 |> maps (fn (name, rths) => map (pair name o snd) rths)
10.69 end
10.70 fun run_slice (slice, (time_frac, (complete,
10.71 - (best_max_relevant, best_type_sys, extra))))
10.72 + (best_max_relevant, best_type_enc, extra))))
10.73 time_left =
10.74 let
10.75 val num_facts =
10.76 length facts |> is_none max_relevant
10.77 ? Integer.min best_max_relevant
10.78 - val (format, type_sys) =
10.79 - choose_format_and_type_sys best_type_sys formats type_sys
10.80 - val fairly_sound = is_type_sys_fairly_sound type_sys
10.81 + val (format, type_enc) =
10.82 + choose_format_and_type_enc best_type_enc formats type_enc
10.83 + val fairly_sound = is_type_enc_fairly_sound type_enc
10.84 val facts =
10.85 facts |> map untranslated_fact
10.86 |> not fairly_sound
10.87 ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
10.88 |> take num_facts
10.89 - |> polymorphism_of_type_sys type_sys <> Polymorphic
10.90 + |> polymorphism_of_type_enc type_enc <> Polymorphic
10.91 ? monomorphize_facts
10.92 |> map (apsnd prop_of)
10.93 val real_ms = Real.fromInt o Time.toMilliseconds
10.94 @@ -635,7 +635,7 @@
10.95 val (atp_problem, pool, conjecture_offset, facts_offset,
10.96 fact_names, typed_helpers, sym_tab) =
10.97 prepare_atp_problem ctxt format conj_sym_kind prem_kind
10.98 - type_sys sound false (Config.get ctxt atp_readable_names)
10.99 + type_enc sound false (Config.get ctxt atp_readable_names)
10.100 true hyp_ts concl_t facts
10.101 fun weights () = atp_problem_weights atp_problem
10.102 val full_proof = debug orelse isar_proof
10.103 @@ -675,7 +675,7 @@
10.104 used_facts_in_unsound_atp_proof ctxt
10.105 conjecture_shape facts_offset fact_names atp_proof
10.106 |> Option.map (fn facts =>
10.107 - UnsoundProof (is_type_sys_virtually_sound type_sys,
10.108 + UnsoundProof (is_type_enc_virtually_sound type_enc,
10.109 facts |> sort string_ord))
10.110 | _ => outcome
10.111 in
11.1 --- a/src/HOL/ex/atp_export.ML Fri Jul 01 15:53:37 2011 +0200
11.2 +++ b/src/HOL/ex/atp_export.ML Fri Jul 01 15:53:38 2011 +0200
11.3 @@ -149,17 +149,17 @@
11.4 if heading = factsN then (heading, order_facts ord lines) :: problem
11.5 else (heading, lines) :: order_problem_facts ord problem
11.6
11.7 -fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name =
11.8 +fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
11.9 let
11.10 val format = FOF
11.11 - val type_sys = type_sys |> type_sys_from_string
11.12 + val type_enc = type_enc |> type_enc_from_string
11.13 val path = file_name |> Path.explode
11.14 val _ = File.write path ""
11.15 val facts = facts_of thy
11.16 val (atp_problem, _, _, _, _, _, _) =
11.17 facts
11.18 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
11.19 - |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false
11.20 + |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
11.21 true [] @{prop False}
11.22 val atp_problem =
11.23 atp_problem