1.1 --- a/src/HOL/Metis_Examples/Proxies.thy Tue Sep 06 22:41:35 2011 -0700
1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy Wed Sep 07 09:10:41 2011 +0200
1.3 @@ -58,206 +58,206 @@
1.4
1.5 lemma "id (op =) x x"
1.6 sledgehammer [type_enc = erased, expect = none] (id_apply)
1.7 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.8 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.9 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.10 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.11 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.12 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.13 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.14 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.15 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.16 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.17 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.18 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.19 by (metis (full_types) id_apply)
1.20
1.21 lemma "id True"
1.22 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.23 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.24 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.25 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.26 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.27 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.28 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.29 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.30 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.31 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.32 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.33 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.34 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.35 by (metis_exhaust id_apply)
1.36
1.37 lemma "\<not> id False"
1.38 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.39 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.40 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.41 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.42 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.43 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.44 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.45 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.46 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.47 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.48 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.49 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.50 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.51 by (metis_exhaust id_apply)
1.52
1.53 lemma "x = id True \<or> x = id False"
1.54 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.55 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.56 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.57 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.58 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.59 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.60 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.61 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.62 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.63 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.64 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.65 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.66 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.67 by (metis_exhaust id_apply)
1.68
1.69 lemma "id x = id True \<or> id x = id False"
1.70 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.71 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.72 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.73 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.74 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.75 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.76 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.77 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.78 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.79 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.80 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.81 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.82 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.83 by (metis_exhaust id_apply)
1.84
1.85 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
1.86 sledgehammer [type_enc = erased, expect = none] ()
1.87 sledgehammer [type_enc = poly_args, expect = none] ()
1.88 -sledgehammer [type_enc = poly_tags?, expect = some] ()
1.89 +sledgehammer [type_enc = poly_tags??, expect = some] ()
1.90 sledgehammer [type_enc = poly_tags, expect = some] ()
1.91 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.92 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.93 sledgehammer [type_enc = poly_guards, expect = some] ()
1.94 -sledgehammer [type_enc = mono_tags?, expect = some] ()
1.95 +sledgehammer [type_enc = mono_tags??, expect = some] ()
1.96 sledgehammer [type_enc = mono_tags, expect = some] ()
1.97 -sledgehammer [type_enc = mono_guards?, expect = some] ()
1.98 +sledgehammer [type_enc = mono_guards??, expect = some] ()
1.99 sledgehammer [type_enc = mono_guards, expect = some] ()
1.100 by (metis (full_types))
1.101
1.102 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
1.103 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.104 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.105 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.106 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.107 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.108 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.109 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.110 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.111 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.112 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.113 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.114 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.115 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.116 by (metis_exhaust id_apply)
1.117
1.118 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
1.119 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.120 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.121 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.122 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.123 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.124 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.125 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.126 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.127 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.128 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.129 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.130 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.131 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.132 by (metis_exhaust id_apply)
1.133
1.134 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
1.135 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.136 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.137 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.138 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.139 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.140 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.141 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.142 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.143 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.144 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.145 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.146 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.147 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.148 by (metis_exhaust id_apply)
1.149
1.150 lemma "id (a \<and> b) \<Longrightarrow> id a"
1.151 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.152 -sledgehammer [type_enc = poly_tags?, 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_guards?, expect = some] (id_apply)
1.156 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.157 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.158 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.159 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.160 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.161 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.162 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.163 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.164 by (metis_exhaust id_apply)
1.165
1.166 lemma "id (a \<and> b) \<Longrightarrow> id b"
1.167 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.168 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.169 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.170 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.171 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.172 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.173 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.174 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.175 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.176 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.177 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.178 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.179 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.180 by (metis_exhaust id_apply)
1.181
1.182 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
1.183 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.184 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.185 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.186 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.187 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.188 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.189 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.190 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.191 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.192 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.193 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.194 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.195 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.196 by (metis_exhaust id_apply)
1.197
1.198 lemma "id a \<Longrightarrow> id (a \<or> b)"
1.199 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.200 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.201 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.202 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.203 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.204 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.205 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.206 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.207 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.208 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.209 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.210 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.211 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.212 by (metis_exhaust id_apply)
1.213
1.214 lemma "id b \<Longrightarrow> id (a \<or> b)"
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_tags, expect = some] (id_apply)
1.219 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.220 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.221 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.222 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.223 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.224 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.225 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.226 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.227 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.228 by (metis_exhaust id_apply)
1.229
1.230 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
1.231 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.232 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.233 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.234 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.235 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.236 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.237 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.238 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.239 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.240 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.241 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.242 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.243 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.244 by (metis_exhaust id_apply)
1.245
1.246 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
1.247 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.248 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.249 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.250 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.251 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.252 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.253 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.254 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.255 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.256 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.257 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.258 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.259 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.260 by (metis_exhaust id_apply)
1.261
1.262 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
1.263 sledgehammer [type_enc = erased, expect = some] (id_apply)
1.264 -sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.265 +sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
1.266 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.267 -sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
1.268 +sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
1.269 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
1.270 -sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
1.271 +sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
1.272 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
1.273 -sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
1.274 +sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
1.275 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
1.276 by (metis_exhaust id_apply)
1.277
2.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Sep 06 22:41:35 2011 -0700
2.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Wed Sep 07 09:10:41 2011 +0200
2.3 @@ -25,44 +25,38 @@
2.4 val type_encs =
2.5 ["erased",
2.6 "poly_guards",
2.7 - "poly_guards_uniform",
2.8 + "poly_guards?",
2.9 + "poly_guards??",
2.10 + "poly_guards!",
2.11 + "poly_guards!!",
2.12 "poly_tags",
2.13 - "poly_tags_uniform",
2.14 + "poly_tags?",
2.15 + "poly_tags??",
2.16 + "poly_tags!",
2.17 + "poly_tags!!",
2.18 "poly_args",
2.19 "raw_mono_guards",
2.20 - "raw_mono_guards_uniform",
2.21 + "raw_mono_guards?",
2.22 + "raw_mono_guards??",
2.23 + "raw_mono_guards!",
2.24 + "raw_mono_guards!!",
2.25 "raw_mono_tags",
2.26 - "raw_mono_tags_uniform",
2.27 + "raw_mono_tags?",
2.28 + "raw_mono_tags??",
2.29 + "raw_mono_tags!",
2.30 + "raw_mono_tags!!",
2.31 "raw_mono_args",
2.32 "mono_guards",
2.33 - "mono_guards_uniform",
2.34 + "mono_guards?",
2.35 + "mono_guards??",
2.36 + "mono_guards!",
2.37 + "mono_guards!!",
2.38 "mono_tags",
2.39 - "mono_tags_uniform",
2.40 - "mono_args",
2.41 - "poly_guards?",
2.42 - "poly_guards_uniform?",
2.43 - "poly_tags?",
2.44 - "poly_tags_uniform?",
2.45 - "raw_mono_guards?",
2.46 - "raw_mono_guards_uniform?",
2.47 - "raw_mono_tags?",
2.48 - "raw_mono_tags_uniform?",
2.49 - "mono_guards?",
2.50 - "mono_guards_uniform?",
2.51 "mono_tags?",
2.52 - "mono_tags_uniform?",
2.53 - "poly_guards!",
2.54 - "poly_guards_uniform!",
2.55 - "poly_tags!",
2.56 - "poly_tags_uniform!",
2.57 - "raw_mono_guards!",
2.58 - "raw_mono_guards_uniform!",
2.59 - "raw_mono_tags!",
2.60 - "raw_mono_tags_uniform!",
2.61 - "mono_guards!",
2.62 - "mono_guards_uniform!",
2.63 + "mono_tags??",
2.64 "mono_tags!",
2.65 - "mono_tags_uniform!"]
2.66 + "mono_tags!!",
2.67 + "mono_args"]
2.68
2.69 fun metis_exhaust_tac ctxt ths =
2.70 let
3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 06 22:41:35 2011 -0700
3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 07 09:10:41 2011 +0200
3.3 @@ -574,9 +574,10 @@
3.4 relevance_override
3.5 in
3.6 if !reconstructor = "sledgehammer_tac" then
3.7 - sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
3.8 - ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
3.9 - ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
3.10 + sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple"
3.11 + ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
3.12 + ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
3.13 + ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
3.14 ORELSE' Metis_Tactic.metis_tac [] ctxt thms
3.15 else if !reconstructor = "smt" then
3.16 SMT_Solver.smt_tac ctxt thms
4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Sep 06 22:41:35 2011 -0700
4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 09:10:41 2011 +0200
4.3 @@ -222,11 +222,11 @@
4.4 let val method = effective_e_weight_method ctxt in
4.5 (* FUDGE *)
4.6 if method = e_smartN then
4.7 - [(0.333, (true, (500, FOF, "mono_tags?", e_fun_weightN))),
4.8 - (0.334, (true, (50, FOF, "mono_guards?", e_fun_weightN))),
4.9 - (0.333, (true, (1000, FOF, "mono_tags?", e_sym_offset_weightN)))]
4.10 + [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))),
4.11 + (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))),
4.12 + (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))]
4.13 else
4.14 - [(1.0, (true, (500, FOF, "mono_tags?", method)))]
4.15 + [(1.0, (true, (500, FOF, "mono_tags??", method)))]
4.16 end}
4.17
4.18 val e = (eN, e_config)
4.19 @@ -304,9 +304,9 @@
4.20 prem_kind = Conjecture,
4.21 best_slices = fn ctxt =>
4.22 (* FUDGE *)
4.23 - [(0.333, (false, (150, FOF, "mono_tags", sosN))),
4.24 - (0.333, (false, (300, FOF, "poly_tags?", sosN))),
4.25 - (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
4.26 + [(0.333, (false, (150, FOF, "mono_tags??", sosN))),
4.27 + (0.333, (false, (300, FOF, "poly_tags??", sosN))),
4.28 + (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
4.29 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
4.30 else I)}
4.31
4.32 @@ -349,11 +349,11 @@
4.33 best_slices = fn ctxt =>
4.34 (* FUDGE *)
4.35 (if is_old_vampire_version () then
4.36 - [(0.333, (false, (150, FOF, "poly_guards", sosN))),
4.37 - (0.333, (false, (500, FOF, "mono_tags?", sosN))),
4.38 - (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
4.39 + [(0.333, (false, (150, FOF, "poly_guards??", sosN))),
4.40 + (0.333, (false, (500, FOF, "mono_tags??", sosN))),
4.41 + (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))]
4.42 else
4.43 - [(0.333, (false, (150, vampire_tff0, "poly_guards", sosN))),
4.44 + [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))),
4.45 (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
4.46 (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
4.47 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
4.48 @@ -490,7 +490,7 @@
4.49
4.50 val remote_e =
4.51 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
4.52 - (K (750, FOF, "mono_tags?") (* FUDGE *))
4.53 + (K (750, FOF, "mono_tags??") (* FUDGE *))
4.54 val remote_leo2 =
4.55 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
4.56 (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
4.57 @@ -499,13 +499,13 @@
4.58 (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
4.59 val remote_vampire =
4.60 remotify_atp vampire "Vampire" ["1.8"]
4.61 - (K (250, FOF, "mono_guards?") (* FUDGE *))
4.62 + (K (250, FOF, "mono_guards??") (* FUDGE *))
4.63 val remote_z3_tptp =
4.64 remotify_atp z3_tptp "Z3" ["3.0"]
4.65 (K (250, z3_tff0, "mono_simple") (* FUDGE *))
4.66 val remote_e_sine =
4.67 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
4.68 - Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
4.69 + Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
4.70 val remote_snark =
4.71 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
4.72 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
4.73 @@ -519,7 +519,7 @@
4.74 [(OutOfResources, "Too many function symbols"),
4.75 (Crashed, "Unrecoverable Segmentation Fault")]
4.76 Hypothesis Hypothesis
4.77 - (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
4.78 + (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *))
4.79
4.80 (* Setup *)
4.81
5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Sep 06 22:41:35 2011 -0700
5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 09:10:41 2011 +0200
5.3 @@ -22,18 +22,18 @@
5.4 datatype order = First_Order | Higher_Order
5.5 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
5.6 datatype soundness = Sound_Modulo_Infiniteness | Sound
5.7 + datatype uniformity = Uniform | Nonuniform
5.8 datatype type_level =
5.9 All_Types |
5.10 - Noninf_Nonmono_Types of soundness |
5.11 - Fin_Nonmono_Types |
5.12 + Noninf_Nonmono_Types of soundness * uniformity |
5.13 + Fin_Nonmono_Types of uniformity |
5.14 Const_Arg_Types |
5.15 No_Types
5.16 - datatype type_uniformity = Uniform | Nonuniform
5.17
5.18 datatype type_enc =
5.19 Simple_Types of order * polymorphism * type_level |
5.20 - Guards of polymorphism * type_level * type_uniformity |
5.21 - Tags of polymorphism * type_level * type_uniformity
5.22 + Guards of polymorphism * type_level |
5.23 + Tags of polymorphism * type_level
5.24
5.25 val type_tag_idempotence : bool Config.T
5.26 val type_tag_arguments : bool Config.T
5.27 @@ -86,12 +86,12 @@
5.28 val new_skolem_var_name_from_const : string -> string
5.29 val atp_irrelevant_consts : string list
5.30 val atp_schematic_consts_of : term -> typ list Symtab.table
5.31 - val type_enc_from_string : soundness -> string -> type_enc
5.32 val is_type_enc_higher_order : type_enc -> bool
5.33 val polymorphism_of_type_enc : type_enc -> polymorphism
5.34 val level_of_type_enc : type_enc -> type_level
5.35 val is_type_enc_quasi_sound : type_enc -> bool
5.36 val is_type_enc_fairly_sound : type_enc -> bool
5.37 + val type_enc_from_string : soundness -> string -> type_enc
5.38 val adjust_type_enc : tptp_format -> type_enc -> type_enc
5.39 val mk_aconns :
5.40 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
5.41 @@ -537,22 +537,53 @@
5.42 datatype order = First_Order | Higher_Order
5.43 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
5.44 datatype soundness = Sound_Modulo_Infiniteness | Sound
5.45 +datatype uniformity = Uniform | Nonuniform
5.46 datatype type_level =
5.47 All_Types |
5.48 - Noninf_Nonmono_Types of soundness |
5.49 - Fin_Nonmono_Types |
5.50 + Noninf_Nonmono_Types of soundness * uniformity |
5.51 + Fin_Nonmono_Types of uniformity |
5.52 Const_Arg_Types |
5.53 No_Types
5.54 -datatype type_uniformity = Uniform | Nonuniform
5.55
5.56 datatype type_enc =
5.57 Simple_Types of order * polymorphism * type_level |
5.58 - Guards of polymorphism * type_level * type_uniformity |
5.59 - Tags of polymorphism * type_level * type_uniformity
5.60 + Guards of polymorphism * type_level |
5.61 + Tags of polymorphism * type_level
5.62 +
5.63 +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
5.64 + | is_type_enc_higher_order _ = false
5.65 +
5.66 +fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
5.67 + | polymorphism_of_type_enc (Guards (poly, _)) = poly
5.68 + | polymorphism_of_type_enc (Tags (poly, _)) = poly
5.69 +
5.70 +fun level_of_type_enc (Simple_Types (_, _, level)) = level
5.71 + | level_of_type_enc (Guards (_, level)) = level
5.72 + | level_of_type_enc (Tags (_, level)) = level
5.73 +
5.74 +fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false
5.75 + | is_level_uniform (Fin_Nonmono_Types Nonuniform) = false
5.76 + | is_level_uniform _ = true
5.77 +
5.78 +fun is_type_level_quasi_sound All_Types = true
5.79 + | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
5.80 + | is_type_level_quasi_sound _ = false
5.81 +val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
5.82 +
5.83 +fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
5.84 + | is_type_level_fairly_sound level = is_type_level_quasi_sound level
5.85 +val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
5.86 +
5.87 +fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
5.88 + | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
5.89 + | is_type_level_monotonicity_based _ = false
5.90
5.91 fun try_unsuffixes ss s =
5.92 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
5.93
5.94 +val queries = ["?", "_query"]
5.95 +val bangs = ["!", "_bang"]
5.96 +
5.97 fun type_enc_from_string soundness s =
5.98 (case try (unprefix "poly_") s of
5.99 SOME s => (SOME Polymorphic, s)
5.100 @@ -566,73 +597,51 @@
5.101 ||> (fn s =>
5.102 (* "_query" and "_bang" are for the ASCII-challenged Metis and
5.103 Mirabelle. *)
5.104 - case try_unsuffixes ["?", "_query"] s of
5.105 - SOME s => (Noninf_Nonmono_Types soundness, s)
5.106 + case try_unsuffixes queries s of
5.107 + SOME s =>
5.108 + (case try_unsuffixes queries s of
5.109 + SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s)
5.110 + | NONE => (Noninf_Nonmono_Types (soundness, Uniform), s))
5.111 | NONE =>
5.112 - case try_unsuffixes ["!", "_bang"] s of
5.113 - SOME s => (Fin_Nonmono_Types, s)
5.114 + case try_unsuffixes bangs s of
5.115 + SOME s =>
5.116 + (case try_unsuffixes bangs s of
5.117 + SOME s => (Fin_Nonmono_Types Nonuniform, s)
5.118 + | NONE => (Fin_Nonmono_Types Uniform, s))
5.119 | NONE => (All_Types, s))
5.120 - ||> apsnd (fn s =>
5.121 - case try (unsuffix "_uniform") s of
5.122 - SOME s => (Uniform, s)
5.123 - | NONE => (Nonuniform, s))
5.124 - |> (fn (poly, (level, (uniformity, core))) =>
5.125 - case (core, (poly, level, uniformity)) of
5.126 - ("simple", (SOME poly, _, Nonuniform)) =>
5.127 + |> (fn (poly, (level, core)) =>
5.128 + case (core, (poly, level)) of
5.129 + ("simple", (SOME poly, _)) =>
5.130 (case (poly, level) of
5.131 (Polymorphic, All_Types) =>
5.132 Simple_Types (First_Order, Polymorphic, All_Types)
5.133 | (Mangled_Monomorphic, _) =>
5.134 - Simple_Types (First_Order, Mangled_Monomorphic, level)
5.135 + if is_level_uniform level then
5.136 + Simple_Types (First_Order, Mangled_Monomorphic, level)
5.137 + else
5.138 + raise Same.SAME
5.139 | _ => raise Same.SAME)
5.140 - | ("simple_higher", (SOME poly, _, Nonuniform)) =>
5.141 + | ("simple_higher", (SOME poly, _)) =>
5.142 (case (poly, level) of
5.143 (Polymorphic, All_Types) =>
5.144 Simple_Types (Higher_Order, Polymorphic, All_Types)
5.145 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
5.146 | (Mangled_Monomorphic, _) =>
5.147 - Simple_Types (Higher_Order, Mangled_Monomorphic, level)
5.148 + if is_level_uniform level then
5.149 + Simple_Types (Higher_Order, Mangled_Monomorphic, level)
5.150 + else
5.151 + raise Same.SAME
5.152 | _ => raise Same.SAME)
5.153 - | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
5.154 - | ("tags", (SOME Polymorphic, _, _)) =>
5.155 - Tags (Polymorphic, level, uniformity)
5.156 - | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
5.157 - | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
5.158 - Guards (poly, Const_Arg_Types, Nonuniform)
5.159 - | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
5.160 - Guards (Polymorphic, No_Types, Nonuniform)
5.161 + | ("guards", (SOME poly, _)) => Guards (poly, level)
5.162 + | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
5.163 + | ("tags", (SOME poly, _)) => Tags (poly, level)
5.164 + | ("args", (SOME poly, All_Types (* naja *))) =>
5.165 + Guards (poly, Const_Arg_Types)
5.166 + | ("erased", (NONE, All_Types (* naja *))) =>
5.167 + Guards (Polymorphic, No_Types)
5.168 | _ => raise Same.SAME)
5.169 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
5.170
5.171 -fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
5.172 - | is_type_enc_higher_order _ = false
5.173 -
5.174 -fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
5.175 - | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
5.176 - | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
5.177 -
5.178 -fun level_of_type_enc (Simple_Types (_, _, level)) = level
5.179 - | level_of_type_enc (Guards (_, level, _)) = level
5.180 - | level_of_type_enc (Tags (_, level, _)) = level
5.181 -
5.182 -fun uniformity_of_type_enc (Simple_Types _) = Uniform
5.183 - | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
5.184 - | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
5.185 -
5.186 -fun is_type_level_quasi_sound All_Types = true
5.187 - | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
5.188 - | is_type_level_quasi_sound _ = false
5.189 -val is_type_enc_quasi_sound =
5.190 - is_type_level_quasi_sound o level_of_type_enc
5.191 -
5.192 -fun is_type_level_fairly_sound level =
5.193 - is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
5.194 -val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
5.195 -
5.196 -fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
5.197 - | is_type_level_monotonicity_based Fin_Nonmono_Types = true
5.198 - | is_type_level_monotonicity_based _ = false
5.199 -
5.200 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
5.201 (Simple_Types (order, _, level)) =
5.202 Simple_Types (order, Mangled_Monomorphic, level)
5.203 @@ -642,7 +651,7 @@
5.204 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
5.205 Simple_Types (First_Order, poly, level)
5.206 | adjust_type_enc format (Simple_Types (_, poly, level)) =
5.207 - adjust_type_enc format (Guards (poly, level, Uniform))
5.208 + adjust_type_enc format (Guards (poly, level))
5.209 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
5.210 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
5.211 | adjust_type_enc _ type_enc = type_enc
5.212 @@ -698,8 +707,7 @@
5.213
5.214 fun should_drop_arg_type_args (Simple_Types _) = false
5.215 | should_drop_arg_type_args type_enc =
5.216 - level_of_type_enc type_enc = All_Types andalso
5.217 - uniformity_of_type_enc type_enc = Uniform
5.218 + level_of_type_enc type_enc = All_Types
5.219
5.220 fun type_arg_policy type_enc s =
5.221 if s = type_tag_name then
5.222 @@ -708,7 +716,7 @@
5.223 else
5.224 Explicit_Type_Args) false
5.225 else case type_enc of
5.226 - Tags (_, All_Types, Uniform) => No_Type_Args
5.227 + Tags (_, All_Types) => No_Type_Args
5.228 | _ =>
5.229 let val level = level_of_type_enc type_enc in
5.230 if level = No_Types orelse s = @{const_name HOL.eq} orelse
5.231 @@ -1154,23 +1162,22 @@
5.232 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
5.233 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
5.234 maybe_nonmono_Ts, ...}
5.235 - (Noninf_Nonmono_Types soundness) T =
5.236 + (Noninf_Nonmono_Types (soundness, _)) T =
5.237 exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
5.238 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
5.239 (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
5.240 is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
5.241 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
5.242 maybe_nonmono_Ts, ...}
5.243 - Fin_Nonmono_Types T =
5.244 + (Fin_Nonmono_Types _) T =
5.245 exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
5.246 (exists (type_generalization ctxt T) surely_finite_Ts orelse
5.247 (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
5.248 is_type_surely_finite ctxt T))
5.249 | should_encode_type _ _ _ _ = false
5.250
5.251 -fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
5.252 - T =
5.253 - (uniformity = Uniform orelse should_guard_var ()) andalso
5.254 +fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
5.255 + (is_level_uniform level orelse should_guard_var ()) andalso
5.256 should_encode_type ctxt mono level T
5.257 | should_guard_type _ _ _ _ _ = false
5.258
5.259 @@ -1186,13 +1193,12 @@
5.260 Elsewhere
5.261
5.262 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
5.263 - | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
5.264 - (case uniformity of
5.265 - Uniform => should_encode_type ctxt mono level T
5.266 - | Nonuniform =>
5.267 - case (site, is_maybe_universal_var u) of
5.268 - (Eq_Arg _, true) => should_encode_type ctxt mono level T
5.269 - | _ => false)
5.270 + | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
5.271 + (if is_level_uniform level then
5.272 + should_encode_type ctxt mono level T
5.273 + else case (site, is_maybe_universal_var u) of
5.274 + (Eq_Arg _, true) => should_encode_type ctxt mono level T
5.275 + | _ => false)
5.276 | should_tag_with_type _ _ _ _ _ _ = false
5.277
5.278 fun fused_type ctxt mono level =
5.279 @@ -1636,8 +1642,8 @@
5.280 | should_guard_var_in_formula _ _ _ _ = true
5.281
5.282 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
5.283 - | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
5.284 - should_encode_type ctxt mono level T
5.285 + | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
5.286 + not (is_level_uniform level) andalso should_encode_type ctxt mono level T
5.287 | should_generate_tag_bound_decl _ _ _ _ _ = false
5.288
5.289 fun mk_aterm format type_enc name T_args args =
5.290 @@ -1870,7 +1876,7 @@
5.291 maybe_infinite_Ts = known_infinite_types,
5.292 surely_infinite_Ts =
5.293 case level of
5.294 - Noninf_Nonmono_Types Sound => []
5.295 + Noninf_Nonmono_Types (Sound, _) => []
5.296 | _ => known_infinite_types,
5.297 maybe_nonmono_Ts = [@{typ bool}]}
5.298
5.299 @@ -1883,7 +1889,7 @@
5.300 surely_infinite_Ts, maybe_nonmono_Ts}) =
5.301 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
5.302 case level of
5.303 - Noninf_Nonmono_Types soundness =>
5.304 + Noninf_Nonmono_Types (soundness, _) =>
5.305 if exists (type_instance ctxt T) surely_infinite_Ts orelse
5.306 member (type_aconv ctxt) maybe_finite_Ts T then
5.307 mono
5.308 @@ -1900,7 +1906,7 @@
5.309 maybe_infinite_Ts = maybe_infinite_Ts,
5.310 surely_infinite_Ts = surely_infinite_Ts,
5.311 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
5.312 - | Fin_Nonmono_Types =>
5.313 + | Fin_Nonmono_Types _ =>
5.314 if exists (type_instance ctxt T) surely_finite_Ts orelse
5.315 member (type_aconv ctxt) maybe_infinite_Ts T then
5.316 mono
5.317 @@ -2089,7 +2095,7 @@
5.318 case type_enc of
5.319 Simple_Types _ =>
5.320 decls |> map (decl_line_for_sym ctxt format mono type_enc s)
5.321 - | Guards (_, level, _) =>
5.322 + | Guards (_, level) =>
5.323 let
5.324 val decls =
5.325 case decls of
5.326 @@ -2111,15 +2117,15 @@
5.327 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
5.328 type_enc n s)
5.329 end
5.330 - | Tags (_, _, uniformity) =>
5.331 - (case uniformity of
5.332 - Uniform => []
5.333 - | Nonuniform =>
5.334 - let val n = length decls in
5.335 - (0 upto n - 1 ~~ decls)
5.336 - |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
5.337 - conj_sym_kind mono type_enc n s)
5.338 - end)
5.339 + | Tags (_, level) =>
5.340 + if is_level_uniform level then
5.341 + []
5.342 + else
5.343 + let val n = length decls in
5.344 + (0 upto n - 1 ~~ decls)
5.345 + |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
5.346 + conj_sym_kind mono type_enc n s)
5.347 + end
5.348
5.349 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
5.350 mono_Ts sym_decl_tab =
5.351 @@ -2133,11 +2139,10 @@
5.352 syms []
5.353 in mono_lines @ decl_lines end
5.354
5.355 -fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
5.356 +fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
5.357 Config.get ctxt type_tag_idempotence andalso
5.358 - poly <> Mangled_Monomorphic andalso
5.359 - ((level = All_Types andalso uniformity = Nonuniform) orelse
5.360 - is_type_level_monotonicity_based level)
5.361 + is_type_level_monotonicity_based level andalso
5.362 + poly <> Mangled_Monomorphic
5.363 | needs_type_tag_idempotence _ _ = false
5.364
5.365 fun offset_of_heading_in_problem _ [] j = j
6.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Sep 06 22:41:35 2011 -0700
6.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Sep 07 09:10:41 2011 +0200
6.3 @@ -39,8 +39,8 @@
6.4 val partial_typesN = "partial_types"
6.5 val no_typesN = "no_types"
6.6
6.7 -val really_full_type_enc = "mono_tags_uniform"
6.8 -val full_type_enc = "poly_guards_uniform_query"
6.9 +val really_full_type_enc = "mono_tags"
6.10 +val full_type_enc = "poly_guards_query"
6.11 val partial_type_enc = "poly_args"
6.12 val no_type_enc = "erased"
6.13
7.1 --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Sep 06 22:41:35 2011 -0700
7.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 09:10:41 2011 +0200
7.3 @@ -59,7 +59,7 @@
7.4 ((prefixed_predicator_name, 1), (K metis_predicator, false)),
7.5 ((prefixed_app_op_name, 2), (K metis_app_op, false)),
7.6 ((prefixed_type_tag_name, 2),
7.7 - (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag
7.8 + (fn Tags (_, All_Types) => metis_systematic_type_tag
7.9 | _ => metis_ad_hoc_type_tag, true))]
7.10
7.11 fun old_skolem_const_name i j num_T_args =
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Sep 06 22:41:35 2011 -0700
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 09:10:41 2011 +0200
8.3 @@ -151,10 +151,12 @@
8.4 error ("Unknown parameter: " ^ quote name ^ "."))
8.5
8.6
8.7 -(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
8.8 +(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
8.9 handled correctly. *)
8.10 fun implode_param [s, "?"] = s ^ "?"
8.11 + | implode_param [s, "??"] = s ^ "??"
8.12 | implode_param [s, "!"] = s ^ "!"
8.13 + | implode_param [s, "!!"] = s ^ "!!"
8.14 | implode_param ss = space_implode " " ss
8.15
8.16 structure Data = Theory_Data
8.17 @@ -376,12 +378,11 @@
8.18 |> sort_strings |> cat_lines))
8.19 end))
8.20
8.21 +val parse_query_bang = Parse.$$$ "?" || Parse.$$$ "!" || Parse.$$$ "!!"
8.22 val parse_key =
8.23 - Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
8.24 - >> implode_param
8.25 + Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param
8.26 val parse_value =
8.27 - Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
8.28 - || Parse.$$$ "!")
8.29 + Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
8.30 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
8.31 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
8.32 val parse_fact_refs =