1.1 --- a/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:37 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy Fri Jul 01 15:53:38 2011 +0200
1.3 @@ -50,215 +50,215 @@
1.4 by linarith
1.5
1.6 lemma "B \<subseteq> C"
1.7 -sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
1.8 +sledgehammer [type_enc = poly_args, max_relevant = 200, expect = some]
1.9 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
1.10
1.11
1.12 text {* Proxies for logical constants *}
1.13
1.14 lemma "id (op =) x x"
1.15 -sledgehammer [type_sys = erased, expect = none] (id_apply)
1.16 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.17 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.18 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.19 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.20 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.21 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.22 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.23 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.24 +sledgehammer [type_enc = erased, expect = none] (id_apply)
1.25 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.26 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.27 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.28 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.29 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.30 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.31 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.32 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.33 by (metis (full_types) id_apply)
1.34
1.35 lemma "id True"
1.36 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.37 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.38 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.39 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.40 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.41 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.42 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.43 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.44 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.45 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.46 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.47 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.48 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.49 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.50 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.51 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.52 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.53 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.54 by (metis_exhaust id_apply)
1.55
1.56 lemma "\<not> id False"
1.57 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.58 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.59 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.60 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.61 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.62 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.63 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.64 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.65 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.66 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.67 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.68 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.69 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.70 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.71 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.72 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.73 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.74 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.75 by (metis_exhaust id_apply)
1.76
1.77 lemma "x = id True \<or> x = id False"
1.78 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.79 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.80 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.81 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.82 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.83 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.84 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.85 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.86 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.87 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.88 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.89 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.90 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.91 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.92 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.93 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.94 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.95 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.96 by (metis_exhaust id_apply)
1.97
1.98 lemma "id x = id True \<or> id x = id False"
1.99 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.100 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.101 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.102 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.103 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.104 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.105 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.106 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.107 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.108 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.109 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.110 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.111 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.112 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.113 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.114 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.115 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.116 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.117 by (metis_exhaust id_apply)
1.118
1.119 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
1.120 -sledgehammer [type_sys = erased, expect = none] ()
1.121 -sledgehammer [type_sys = poly_args, expect = none] ()
1.122 -sledgehammer [type_sys = poly_tags?, expect = some] ()
1.123 -sledgehammer [type_sys = poly_tags, expect = some] ()
1.124 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.125 -sledgehammer [type_sys = poly_preds, expect = some] ()
1.126 -sledgehammer [type_sys = mangled_tags?, expect = some] ()
1.127 -sledgehammer [type_sys = mangled_tags, expect = some] ()
1.128 -sledgehammer [type_sys = mangled_preds?, expect = some] ()
1.129 -sledgehammer [type_sys = mangled_preds, expect = some] ()
1.130 +sledgehammer [type_enc = erased, expect = none] ()
1.131 +sledgehammer [type_enc = poly_args, expect = none] ()
1.132 +sledgehammer [type_enc = poly_tags?, expect = some] ()
1.133 +sledgehammer [type_enc = poly_tags, expect = some] ()
1.134 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.135 +sledgehammer [type_enc = poly_preds, expect = some] ()
1.136 +sledgehammer [type_enc = mangled_tags?, expect = some] ()
1.137 +sledgehammer [type_enc = mangled_tags, expect = some] ()
1.138 +sledgehammer [type_enc = mangled_preds?, expect = some] ()
1.139 +sledgehammer [type_enc = mangled_preds, expect = some] ()
1.140 by (metis (full_types))
1.141
1.142 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
1.143 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.144 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.145 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.146 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.147 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.148 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.149 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.150 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.151 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.152 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.153 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.154 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.155 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.156 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.157 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.158 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.159 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.160 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.161 by (metis_exhaust id_apply)
1.162
1.163 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
1.164 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.165 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.166 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.167 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.168 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.169 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.170 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.171 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.172 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.173 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.174 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.175 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.176 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.177 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.178 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.179 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.180 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.181 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.182 by (metis_exhaust id_apply)
1.183
1.184 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
1.185 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.186 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.187 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.188 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.189 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.190 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.191 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.192 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.193 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.194 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.195 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.196 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.197 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.198 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.199 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.200 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.201 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.202 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.203 by (metis_exhaust id_apply)
1.204
1.205 lemma "id (a \<and> b) \<Longrightarrow> id a"
1.206 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.207 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.208 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.209 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.210 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.211 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.212 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.213 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.214 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.215 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.216 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.217 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.218 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.219 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.220 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.221 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.222 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.223 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.224 by (metis_exhaust id_apply)
1.225
1.226 lemma "id (a \<and> b) \<Longrightarrow> id b"
1.227 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.228 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.229 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.230 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.231 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.232 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.233 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.234 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.235 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.236 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.237 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.238 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.239 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.240 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.241 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.242 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.243 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.244 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.245 by (metis_exhaust id_apply)
1.246
1.247 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
1.248 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.249 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.250 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.251 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.252 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.253 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.254 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.255 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.256 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.257 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.258 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.259 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.260 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.261 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.262 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.263 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.264 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.265 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.266 by (metis_exhaust id_apply)
1.267
1.268 lemma "id a \<Longrightarrow> id (a \<or> b)"
1.269 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.270 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.271 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.272 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.273 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.274 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.275 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.276 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.277 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.278 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.279 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.280 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.281 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.282 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.283 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.284 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.285 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.286 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.287 by (metis_exhaust id_apply)
1.288
1.289 lemma "id b \<Longrightarrow> id (a \<or> b)"
1.290 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.291 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.292 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.293 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.294 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.295 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.296 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.297 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.298 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.299 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.300 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.301 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.302 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.303 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.304 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.305 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.306 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.307 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.308 by (metis_exhaust id_apply)
1.309
1.310 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
1.311 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.312 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.313 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.314 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.315 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.316 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.317 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.318 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.319 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.320 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.321 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.322 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.323 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.324 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.325 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.326 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.327 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.328 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.329 by (metis_exhaust id_apply)
1.330
1.331 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
1.332 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.333 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.334 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.335 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.336 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.337 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.338 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.339 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.340 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.341 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.342 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.343 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.344 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.345 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.346 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.347 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.348 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.349 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.350 by (metis_exhaust id_apply)
1.351
1.352 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
1.353 -sledgehammer [type_sys = erased, expect = some] (id_apply)
1.354 -sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
1.355 -sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
1.356 -sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
1.357 -sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
1.358 -sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)
1.359 -sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
1.360 -sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
1.361 -sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
1.362 +sledgehammer [type_enc = erased, expect = some] (id_apply)
1.363 +sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
1.364 +sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
1.365 +sledgehammer [type_enc = poly_preds?, expect = some] (id_apply)
1.366 +sledgehammer [type_enc = poly_preds, expect = some] (id_apply)
1.367 +sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
1.368 +sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
1.369 +sledgehammer [type_enc = mangled_preds?, expect = some] (id_apply)
1.370 +sledgehammer [type_enc = mangled_preds, expect = some] (id_apply)
1.371 by (metis_exhaust id_apply)
1.372
1.373 end