1.1 --- a/src/HOL/Metis_Examples/Proxies.thy Tue Jul 26 18:11:38 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy Tue Jul 26 22:53:06 2011 +0200
1.3 @@ -60,60 +60,60 @@
1.4 sledgehammer [type_enc = erased, expect = none] (id_apply)
1.5 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.6 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.7 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.8 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.9 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.10 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.11 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.12 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.13 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.14 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.15 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.16 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.17 by (metis (full_types) id_apply)
1.18
1.19 lemma "id True"
1.20 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.21 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.22 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.23 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.24 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.25 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.26 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.27 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.28 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.29 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.30 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.31 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.32 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.33 by (metis_exhaust id_apply)
1.34
1.35 lemma "\<not> id False"
1.36 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.37 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.38 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.39 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.40 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.41 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.42 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.43 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.44 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.45 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.46 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.47 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.48 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.49 by (metis_exhaust id_apply)
1.50
1.51 lemma "x = id True \<or> x = id False"
1.52 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.53 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.54 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.55 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.56 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.57 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.58 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.59 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.60 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.61 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.62 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.63 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.64 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.65 by (metis_exhaust id_apply)
1.66
1.67 lemma "id x = id True \<or> id x = id False"
1.68 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.69 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.70 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.71 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.72 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.73 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.74 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.75 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.76 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.77 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.78 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.79 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.80 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.81 by (metis_exhaust id_apply)
1.82
1.83 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
1.84 @@ -121,144 +121,144 @@
1.85 sledgehammer [type_enc = poly_args, expect = none] ()
1.86 sledgehammer [type_enc = poly_tags?, expect = some] ()
1.87 sledgehammer [type_enc = poly_tags, expect = some] ()
1.88 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.89 -sledgehammer [type_enc = poly_preds, expect = some] ()
1.90 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.91 +sledgehammer [type_enc = poly_guards, expect = some] ()
1.92 sledgehammer [type_enc = mangled_tags?, expect = some] ()
1.93 sledgehammer [type_enc = mangled_tags, expect = some] ()
1.94 -sledgehammer [type_enc = mangled_preds?, expect = some] ()
1.95 -sledgehammer [type_enc = mangled_preds, expect = some] ()
1.96 +sledgehammer [type_enc = mangled_guards?, expect = some] ()
1.97 +sledgehammer [type_enc = mangled_guards, expect = some] ()
1.98 by (metis (full_types))
1.99
1.100 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
1.101 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.102 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.103 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.104 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.105 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.106 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.107 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.108 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.109 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.110 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.111 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.112 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.113 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.114 by (metis_exhaust id_apply)
1.115
1.116 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
1.117 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.118 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.119 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.120 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.121 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.122 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.123 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.124 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.125 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.126 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.127 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.128 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.129 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.130 by (metis_exhaust id_apply)
1.131
1.132 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
1.133 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.134 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.135 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.136 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.137 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.138 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.139 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.140 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.141 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.142 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.143 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.144 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.145 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.146 by (metis_exhaust id_apply)
1.147
1.148 lemma "id (a \<and> b) \<Longrightarrow> id a"
1.149 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.150 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.151 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.152 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.153 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.154 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.155 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.156 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.157 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.158 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.159 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.160 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.161 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.162 by (metis_exhaust id_apply)
1.163
1.164 lemma "id (a \<and> b) \<Longrightarrow> id b"
1.165 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.166 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.167 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.168 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.169 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.170 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.171 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.172 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.173 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.174 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.175 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.176 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.177 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.178 by (metis_exhaust id_apply)
1.179
1.180 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
1.181 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.182 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.183 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.184 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.185 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.186 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.187 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.188 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.189 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.190 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.191 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.192 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.193 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.194 by (metis_exhaust id_apply)
1.195
1.196 lemma "id a \<Longrightarrow> id (a \<or> b)"
1.197 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.198 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.199 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.200 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.201 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.202 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.203 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.204 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.205 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.206 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.207 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.208 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.209 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.210 by (metis_exhaust id_apply)
1.211
1.212 lemma "id b \<Longrightarrow> id (a \<or> b)"
1.213 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.214 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.215 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.216 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.217 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.218 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.219 +sledgehammer [type_enc = poly_guards, 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 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.225 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.226 by (metis_exhaust id_apply)
1.227
1.228 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
1.229 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.230 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.231 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.232 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.233 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.234 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.235 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.236 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.237 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.238 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.239 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.240 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.241 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.242 by (metis_exhaust id_apply)
1.243
1.244 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
1.245 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.246 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.247 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.248 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.249 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.250 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.251 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.252 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.253 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.254 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.255 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.256 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.257 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.258 by (metis_exhaust id_apply)
1.259
1.260 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
1.261 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.262 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.263 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.264 -sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.265 -sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.266 +sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.267 +sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.268 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.269 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.270 -sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.271 -sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.272 +sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
1.273 +sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
1.274 by (metis_exhaust id_apply)
1.275
1.276 end
2.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jul 26 18:11:38 2011 +0200
2.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jul 26 22:53:06 2011 +0200
2.3 @@ -26,45 +26,45 @@
2.4 tests. *)
2.5 val type_encs =
2.6 ["erased",
2.7 - "poly_preds",
2.8 - "poly_preds_heavy",
2.9 + "poly_guards",
2.10 + "poly_guards_heavy",
2.11 "poly_tags",
2.12 "poly_tags_heavy",
2.13 "poly_args",
2.14 - "mono_preds",
2.15 - "mono_preds_heavy",
2.16 + "mono_guards",
2.17 + "mono_guards_heavy",
2.18 "mono_tags",
2.19 "mono_tags_heavy",
2.20 "mono_args",
2.21 - "mangled_preds",
2.22 - "mangled_preds_heavy",
2.23 + "mangled_guards",
2.24 + "mangled_guards_heavy",
2.25 "mangled_tags",
2.26 "mangled_tags_heavy",
2.27 "mangled_args",
2.28 "simple",
2.29 - "poly_preds?",
2.30 - "poly_preds_heavy?",
2.31 + "poly_guards?",
2.32 + "poly_guards_heavy?",
2.33 "poly_tags?",
2.34 (* "poly_tags_heavy?", *)
2.35 - "mono_preds?",
2.36 - "mono_preds_heavy?",
2.37 + "mono_guards?",
2.38 + "mono_guards_heavy?",
2.39 "mono_tags?",
2.40 "mono_tags_heavy?",
2.41 - "mangled_preds?",
2.42 - "mangled_preds_heavy?",
2.43 + "mangled_guards?",
2.44 + "mangled_guards_heavy?",
2.45 "mangled_tags?",
2.46 "mangled_tags_heavy?",
2.47 "simple?",
2.48 - "poly_preds!",
2.49 - "poly_preds_heavy!",
2.50 + "poly_guards!",
2.51 + "poly_guards_heavy!",
2.52 (* "poly_tags!", *)
2.53 "poly_tags_heavy!",
2.54 - "mono_preds!",
2.55 - "mono_preds_heavy!",
2.56 + "mono_guards!",
2.57 + "mono_guards_heavy!",
2.58 "mono_tags!",
2.59 "mono_tags_heavy!",
2.60 - "mangled_preds!",
2.61 - "mangled_preds_heavy!",
2.62 + "mangled_guards!",
2.63 + "mangled_guards_heavy!",
2.64 "mangled_tags!",
2.65 "mangled_tags_heavy!",
2.66 "simple!"]
3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jul 26 18:11:38 2011 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jul 26 22:53:06 2011 +0200
3.3 @@ -219,7 +219,7 @@
3.4 (* FUDGE *)
3.5 if method = e_smartN then
3.6 [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
3.7 - (0.334, (true, (50, "mangled_preds?", e_fun_weightN))),
3.8 + (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
3.9 (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
3.10 else
3.11 [(1.0, (true, (500, "mangled_tags?", method)))]
3.12 @@ -298,8 +298,8 @@
3.13 formats = [FOF],
3.14 best_slices = fn ctxt =>
3.15 (* FUDGE *)
3.16 - [(0.333, (false, (150, "poly_preds", sosN))),
3.17 - (0.334, (true, (50, "mangled_preds?", no_sosN))),
3.18 + [(0.333, (false, (150, "poly_guards", sosN))),
3.19 + (0.334, (true, (50, "mangled_guards?", no_sosN))),
3.20 (0.333, (false, (500, "mangled_tags?", sosN)))]
3.21 |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
3.22 else I)}
3.23 @@ -326,10 +326,10 @@
3.24 formats = [FOF],
3.25 best_slices =
3.26 (* FUDGE (FIXME) *)
3.27 - K [(0.5, (false, (250, "mangled_preds?", ""))),
3.28 - (0.25, (false, (125, "mangled_preds?", ""))),
3.29 - (0.125, (false, (62, "mangled_preds?", ""))),
3.30 - (0.125, (false, (31, "mangled_preds?", "")))]}
3.31 + K [(0.5, (false, (250, "mangled_guards?", ""))),
3.32 + (0.25, (false, (125, "mangled_guards?", ""))),
3.33 + (0.125, (false, (62, "mangled_guards?", ""))),
3.34 + (0.125, (false, (31, "mangled_guards?", "")))]}
3.35
3.36 val z3_atp = (z3_atpN, z3_atp_config)
3.37
3.38 @@ -413,9 +413,9 @@
3.39 (K (750, "mangled_tags?") (* FUDGE *))
3.40 val remote_vampire =
3.41 remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
3.42 - (K (200, "mangled_preds?") (* FUDGE *))
3.43 + (K (200, "mangled_guards?") (* FUDGE *))
3.44 val remote_z3_atp =
3.45 - remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
3.46 + remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
3.47 val remote_leo2 =
3.48 remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
3.49 (K (100, "simple_higher") (* FUDGE *))
3.50 @@ -424,7 +424,7 @@
3.51 (K (64, "simple_higher") (* FUDGE *))
3.52 val remote_sine_e =
3.53 remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
3.54 - Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
3.55 + Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
3.56 val remote_snark =
3.57 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
3.58 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
4.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 26 18:11:38 2011 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 26 22:53:06 2011 +0200
4.3 @@ -28,7 +28,7 @@
4.4
4.5 datatype type_enc =
4.6 Simple_Types of order * type_level |
4.7 - Preds of polymorphism * type_level * type_heaviness |
4.8 + Guards of polymorphism * type_level * type_heaviness |
4.9 Tags of polymorphism * type_level * type_heaviness
4.10
4.11 val bound_var_prefix : string
4.12 @@ -45,7 +45,7 @@
4.13 val new_skolem_const_prefix : string
4.14 val type_decl_prefix : string
4.15 val sym_decl_prefix : string
4.16 - val preds_sym_formula_prefix : string
4.17 + val guards_sym_formula_prefix : string
4.18 val lightweight_tags_sym_formula_prefix : string
4.19 val fact_prefix : string
4.20 val conjecture_prefix : string
4.21 @@ -133,7 +133,7 @@
4.22
4.23 val type_decl_prefix = "ty_"
4.24 val sym_decl_prefix = "sy_"
4.25 -val preds_sym_formula_prefix = "psy_"
4.26 +val guards_sym_formula_prefix = "gsy_"
4.27 val lightweight_tags_sym_formula_prefix = "tsy_"
4.28 val fact_prefix = "fact_"
4.29 val conjecture_prefix = "conj_"
4.30 @@ -518,7 +518,7 @@
4.31
4.32 datatype type_enc =
4.33 Simple_Types of order * type_level |
4.34 - Preds of polymorphism * type_level * type_heaviness |
4.35 + Guards of polymorphism * type_level * type_heaviness |
4.36 Tags of polymorphism * type_level * type_heaviness
4.37
4.38 fun try_unsuffixes ss s =
4.39 @@ -554,14 +554,14 @@
4.40 | ("simple_higher", (NONE, _, Lightweight)) =>
4.41 if level = Noninf_Nonmono_Types then raise Same.SAME
4.42 else Simple_Types (Higher_Order, level)
4.43 - | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
4.44 + | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
4.45 | ("tags", (SOME Polymorphic, _, _)) =>
4.46 Tags (Polymorphic, level, heaviness)
4.47 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
4.48 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
4.49 - Preds (poly, Const_Arg_Types, Lightweight)
4.50 + Guards (poly, Const_Arg_Types, Lightweight)
4.51 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
4.52 - Preds (Polymorphic, No_Types, Lightweight)
4.53 + Guards (Polymorphic, No_Types, Lightweight)
4.54 | _ => raise Same.SAME)
4.55 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
4.56
4.57 @@ -569,15 +569,15 @@
4.58 | is_type_enc_higher_order _ = false
4.59
4.60 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
4.61 - | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
4.62 + | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
4.63 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
4.64
4.65 fun level_of_type_enc (Simple_Types (_, level)) = level
4.66 - | level_of_type_enc (Preds (_, level, _)) = level
4.67 + | level_of_type_enc (Guards (_, level, _)) = level
4.68 | level_of_type_enc (Tags (_, level, _)) = level
4.69
4.70 fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
4.71 - | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
4.72 + | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
4.73 | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
4.74
4.75 fun is_type_level_virtually_sound level =
4.76 @@ -595,13 +595,13 @@
4.77 else if member (op =) formats TFF then
4.78 (TFF, Simple_Types (First_Order, level))
4.79 else
4.80 - choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
4.81 + choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
4.82 | choose_format formats type_enc =
4.83 (case hd formats of
4.84 CNF_UEQ =>
4.85 (CNF_UEQ, case type_enc of
4.86 - Preds stuff =>
4.87 - (if is_type_enc_fairly_sound type_enc then Tags else Preds)
4.88 + Guards stuff =>
4.89 + (if is_type_enc_fairly_sound type_enc then Tags else Guards)
4.90 stuff
4.91 | _ => type_enc)
4.92 | format => (format, type_enc))
4.93 @@ -1035,7 +1035,7 @@
4.94 is_type_surely_finite ctxt false T
4.95 | should_encode_type _ _ _ _ = false
4.96
4.97 -fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
4.98 +fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
4.99 should_predicate_on_var T =
4.100 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
4.101 should_encode_type ctxt nonmono_Ts level T
4.102 @@ -1756,7 +1756,7 @@
4.103 |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
4.104 end
4.105
4.106 -fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
4.107 +fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
4.108 poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
4.109 let
4.110 val (kind, maybe_negate) =
4.111 @@ -1775,7 +1775,7 @@
4.112 val bound_Ts =
4.113 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
4.114 in
4.115 - Formula (preds_sym_formula_prefix ^ s ^
4.116 + Formula (guards_sym_formula_prefix ^ s ^
4.117 (if n > 1 then "_" ^ string_of_int j else ""), kind,
4.118 IConst ((s, s'), T, T_args)
4.119 |> fold (curry (IApp o swap)) bounds
4.120 @@ -1851,7 +1851,7 @@
4.121 case type_enc of
4.122 Simple_Types _ =>
4.123 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
4.124 - | Preds _ =>
4.125 + | Guards _ =>
4.126 let
4.127 val decls =
4.128 case decls of
4.129 @@ -1871,7 +1871,7 @@
4.130 o result_type_of_decl)
4.131 in
4.132 (0 upto length decls - 1, decls)
4.133 - |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
4.134 + |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
4.135 nonmono_Ts poly_nonmono_Ts type_enc n s)
4.136 end
4.137 | Tags (_, _, heaviness) =>
5.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Jul 26 18:11:38 2011 +0200
5.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Jul 26 22:53:06 2011 +0200
5.3 @@ -40,7 +40,7 @@
5.4 val no_typesN = "no_types"
5.5
5.6 val really_full_type_enc = "mangled_tags_heavy"
5.7 -val full_type_enc = "poly_preds_heavy_query"
5.8 +val full_type_enc = "poly_guards_heavy_query"
5.9 val partial_type_enc = "poly_args"
5.10 val no_type_enc = "erased"
5.11
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 26 18:11:38 2011 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 26 22:53:06 2011 +0200
6.3 @@ -148,7 +148,7 @@
6.4 | _ => value)
6.5 | NONE => (name, value)
6.6
6.7 -(* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
6.8 +(* Ensure that type systems such as "simple!" and "mangled_guards?" are handled
6.9 correctly. *)
6.10 fun implode_param [s, "?"] = s ^ "?"
6.11 | implode_param [s, "!"] = s ^ "!"