rationalize uniform encodings
authorblanchet
Wed Sep 07 09:10:41 2011 +0200 (2011-09-07)
changeset 44768a7bc1bdb8bb4
parent 44767 233f30abb040
child 44769 15102294a166
rationalize uniform encodings
src/HOL/Metis_Examples/Proxies.thy
src/HOL/Metis_Examples/Type_Encodings.thy
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     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 =