1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 25 14:25:07 2011 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Aug 25 14:25:07 2011 +0200
1.3 @@ -896,7 +896,7 @@
1.4 arguments, to resolve overloading.
1.5
1.6 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
1.7 -tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
1.8 +tagged with its type using a function $\mathit{type\/}(\tau, t)$.
1.9
1.10 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
1.11 Like for \textit{poly\_guards} constants are annotated with their types to
1.12 @@ -905,8 +905,8 @@
1.13
1.14 \item[$\bullet$]
1.15 \textbf{%
1.16 -\textit{mono\_guards}, \textit{mono\_tags} (sound);
1.17 -\textit{mono\_args} (unsound):} \\
1.18 +\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
1.19 +\textit{raw\_mono\_args} (unsound):} \\
1.20 Similar to \textit{poly\_guards}, \textit{poly\_tags}, and \textit{poly\_args},
1.21 respectively, but the problem is additionally monomorphized, meaning that type
1.22 variables are instantiated with heuristically chosen ground types.
1.23 @@ -915,33 +915,34 @@
1.24
1.25 \item[$\bullet$]
1.26 \textbf{%
1.27 -\textit{mangled\_guards},
1.28 -\textit{mangled\_tags} (sound); \\
1.29 -\textit{mangled\_args} (unsound):} \\
1.30 +\textit{mono\_guards}, \textit{mono\_tags} (sound);
1.31 +\textit{mono\_args} (unsound):} \\
1.32 Similar to
1.33 -\textit{mono\_guards}, \textit{mono\_tags}, and \textit{mono\_args},
1.34 -respectively but types are mangled in constant names instead of being supplied
1.35 -as ground term arguments. The binary predicate $\mathit{has\_type\/}(\tau, t)$
1.36 -becomes a unary predicate $\mathit{has\_type\_}\tau(t)$, and the binary function
1.37 -$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
1.38 -$\mathit{type\_info\_}\tau(t)$.
1.39 +\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
1.40 +\textit{raw\_mono\_args}, respectively but types are mangled in constant names
1.41 +instead of being supplied as ground term arguments. The binary predicate
1.42 +$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
1.43 +$\mathit{has\_type\_}\tau(t)$, and the binary function
1.44 +$\mathit{type\/}(\tau, t)$ becomes a unary function
1.45 +$\mathit{type\_}\tau(t)$.
1.46
1.47 \item[$\bullet$] \textbf{\textit{simple} (sound):} Exploit simple first-order
1.48 types if the prover supports the TFF or THF syntax; otherwise, fall back on
1.49 -\textit{mangled\_guards}. The problem is monomorphized.
1.50 +\textit{mono\_guards}. The problem is monomorphized.
1.51
1.52 \item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
1.53 higher-order types if the prover supports the THF syntax; otherwise, fall back
1.54 -on \textit{simple} or \textit{mangled\_guards\_uniform}. The problem is
1.55 +on \textit{simple} or \textit{mono\_guards\_uniform}. The problem is
1.56 monomorphized.
1.57
1.58 \item[$\bullet$]
1.59 \textbf{%
1.60 -\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
1.61 -\textit{mangled\_guards}?, \textit{mangled\_tags}?, \textit{simple}? (quasi-sound):} \\
1.62 +\textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
1.63 +\textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
1.64 +\textit{simple}? (quasi-sound):} \\
1.65 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
1.66 -\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
1.67 -\textit{mangled\_tags}, and \textit{simple} are fully
1.68 +\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
1.69 +\textit{mono\_tags}, and \textit{simple} are fully
1.70 typed and sound. For each of these, Sledgehammer also provides a lighter,
1.71 virtually sound variant identified by a question mark (`{?}')\ that detects and
1.72 erases monotonic types, notably infinite types. (For \textit{simple}, the types
1.73 @@ -952,12 +953,12 @@
1.74
1.75 \item[$\bullet$]
1.76 \textbf{%
1.77 -\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
1.78 -\textit{mangled\_guards}!, \textit{mangled\_tags}!, \textit{simple}!, \textit{simple\_higher}! \\
1.79 -(mildly unsound):} \\
1.80 +\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
1.81 +\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \textit{simple}!, \\
1.82 +\textit{simple\_higher}! (mildly unsound):} \\
1.83 The type encodings \textit{poly\_guards}, \textit{poly\_tags},
1.84 -\textit{mono\_guards}, \textit{mono\_tags}, \textit{mangled\_guards},
1.85 -\textit{mangled\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
1.86 +\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
1.87 +\textit{mono\_tags}, \textit{simple}, and \textit{simple\_higher} also admit
1.88 a mildly unsound (but very efficient) variant identified by an exclamation mark
1.89 (`{!}') that detects and erases erases all types except those that are clearly
1.90 finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
1.91 @@ -973,7 +974,7 @@
1.92 available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
1.93 nonuniform variants are generally more efficient and are the default; the
1.94 uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
1.95 -\textit{mangled\_guards\_uniform}{?}).
1.96 +\textit{mono\_guards\_uniform}{?}).
1.97
1.98 For SMT solvers, the type encoding is always \textit{simple}, irrespective of
1.99 the value of this option.
2.1 --- a/src/HOL/Metis_Examples/Proxies.thy Thu Aug 25 14:25:07 2011 +0200
2.2 +++ b/src/HOL/Metis_Examples/Proxies.thy Thu Aug 25 14:25:07 2011 +0200
2.3 @@ -62,10 +62,10 @@
2.4 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.5 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.6 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.7 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.8 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.9 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.10 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.11 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.12 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.13 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.14 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.15 by (metis (full_types) id_apply)
2.16
2.17 lemma "id True"
2.18 @@ -74,10 +74,10 @@
2.19 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.20 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.21 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.22 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.23 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.24 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.25 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.26 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.27 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.28 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.29 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.30 by (metis_exhaust id_apply)
2.31
2.32 lemma "\<not> id False"
2.33 @@ -86,10 +86,10 @@
2.34 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.35 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.36 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.37 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.38 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.39 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.40 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.41 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.42 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.43 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.44 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.45 by (metis_exhaust id_apply)
2.46
2.47 lemma "x = id True \<or> x = id False"
2.48 @@ -98,10 +98,10 @@
2.49 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.50 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.51 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.52 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.53 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.54 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.55 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.56 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.57 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.58 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.59 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.60 by (metis_exhaust id_apply)
2.61
2.62 lemma "id x = id True \<or> id x = id False"
2.63 @@ -110,10 +110,10 @@
2.64 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.65 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.66 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.67 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.68 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.69 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.70 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.71 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.72 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.73 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.74 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.75 by (metis_exhaust id_apply)
2.76
2.77 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
2.78 @@ -123,10 +123,10 @@
2.79 sledgehammer [type_enc = poly_tags, expect = some] ()
2.80 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.81 sledgehammer [type_enc = poly_guards, expect = some] ()
2.82 -sledgehammer [type_enc = mangled_tags?, expect = some] ()
2.83 -sledgehammer [type_enc = mangled_tags, expect = some] ()
2.84 -sledgehammer [type_enc = mangled_guards?, expect = some] ()
2.85 -sledgehammer [type_enc = mangled_guards, expect = some] ()
2.86 +sledgehammer [type_enc = mono_tags?, expect = some] ()
2.87 +sledgehammer [type_enc = mono_tags, expect = some] ()
2.88 +sledgehammer [type_enc = mono_guards?, expect = some] ()
2.89 +sledgehammer [type_enc = mono_guards, expect = some] ()
2.90 by (metis (full_types))
2.91
2.92 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
2.93 @@ -135,10 +135,10 @@
2.94 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.95 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.96 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.97 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.98 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.99 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.100 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.101 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.102 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.103 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.104 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.105 by (metis_exhaust id_apply)
2.106
2.107 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
2.108 @@ -147,10 +147,10 @@
2.109 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.110 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.111 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.112 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.113 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.114 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.115 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.116 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.117 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.118 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.119 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.120 by (metis_exhaust id_apply)
2.121
2.122 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
2.123 @@ -159,10 +159,10 @@
2.124 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.125 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.126 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.127 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.128 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.129 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.130 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.131 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.132 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.133 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.134 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.135 by (metis_exhaust id_apply)
2.136
2.137 lemma "id (a \<and> b) \<Longrightarrow> id a"
2.138 @@ -171,10 +171,10 @@
2.139 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.140 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.141 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.142 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.143 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.144 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.145 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.146 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.147 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.148 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.149 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.150 by (metis_exhaust id_apply)
2.151
2.152 lemma "id (a \<and> b) \<Longrightarrow> id b"
2.153 @@ -183,10 +183,10 @@
2.154 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.155 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.156 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.157 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.158 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.159 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.160 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.161 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.162 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.163 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.164 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.165 by (metis_exhaust id_apply)
2.166
2.167 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
2.168 @@ -195,10 +195,10 @@
2.169 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.170 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.171 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.172 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.173 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.174 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.175 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.176 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.177 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.178 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.179 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.180 by (metis_exhaust id_apply)
2.181
2.182 lemma "id a \<Longrightarrow> id (a \<or> b)"
2.183 @@ -207,10 +207,10 @@
2.184 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.185 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.186 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.187 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.188 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.189 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.190 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.191 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.192 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.193 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.194 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.195 by (metis_exhaust id_apply)
2.196
2.197 lemma "id b \<Longrightarrow> id (a \<or> b)"
2.198 @@ -219,10 +219,10 @@
2.199 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.200 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.201 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.202 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.203 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.204 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.205 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.206 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.207 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.208 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.209 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.210 by (metis_exhaust id_apply)
2.211
2.212 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
2.213 @@ -231,10 +231,10 @@
2.214 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.215 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.216 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.217 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.218 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.219 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.220 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.221 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.222 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.223 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.224 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.225 by (metis_exhaust id_apply)
2.226
2.227 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
2.228 @@ -243,10 +243,10 @@
2.229 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.230 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.231 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.232 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.233 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.234 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.235 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.236 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.237 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.238 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.239 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.240 by (metis_exhaust id_apply)
2.241
2.242 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
2.243 @@ -255,10 +255,10 @@
2.244 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
2.245 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
2.246 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
2.247 -sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
2.248 -sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
2.249 -sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
2.250 -sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
2.251 +sledgehammer [type_enc = mono_tags?, expect = some] (id_apply)
2.252 +sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
2.253 +sledgehammer [type_enc = mono_guards?, expect = some] (id_apply)
2.254 +sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
2.255 by (metis_exhaust id_apply)
2.256
2.257 end
3.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Aug 25 14:25:07 2011 +0200
3.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Aug 25 14:25:07 2011 +0200
3.3 @@ -29,42 +29,42 @@
3.4 "poly_tags",
3.5 "poly_tags_uniform",
3.6 "poly_args",
3.7 + "raw_mono_guards",
3.8 + "raw_mono_guards_uniform",
3.9 + "raw_mono_tags",
3.10 + "raw_mono_tags_uniform",
3.11 + "raw_mono_args",
3.12 "mono_guards",
3.13 "mono_guards_uniform",
3.14 "mono_tags",
3.15 "mono_tags_uniform",
3.16 "mono_args",
3.17 - "mangled_guards",
3.18 - "mangled_guards_uniform",
3.19 - "mangled_tags",
3.20 - "mangled_tags_uniform",
3.21 - "mangled_args",
3.22 "simple",
3.23 "poly_guards?",
3.24 "poly_guards_uniform?",
3.25 "poly_tags?",
3.26 "poly_tags_uniform?",
3.27 + "raw_mono_guards?",
3.28 + "raw_mono_guards_uniform?",
3.29 + "raw_mono_tags?",
3.30 + "raw_mono_tags_uniform?",
3.31 "mono_guards?",
3.32 "mono_guards_uniform?",
3.33 "mono_tags?",
3.34 "mono_tags_uniform?",
3.35 - "mangled_guards?",
3.36 - "mangled_guards_uniform?",
3.37 - "mangled_tags?",
3.38 - "mangled_tags_uniform?",
3.39 "simple?",
3.40 "poly_guards!",
3.41 "poly_guards_uniform!",
3.42 "poly_tags!",
3.43 "poly_tags_uniform!",
3.44 + "raw_mono_guards!",
3.45 + "raw_mono_guards_uniform!",
3.46 + "raw_mono_tags!",
3.47 + "raw_mono_tags_uniform!",
3.48 "mono_guards!",
3.49 "mono_guards_uniform!",
3.50 "mono_tags!",
3.51 "mono_tags_uniform!",
3.52 - "mangled_guards!",
3.53 - "mangled_guards_uniform!",
3.54 - "mangled_tags!",
3.55 - "mangled_tags_uniform!",
3.56 "simple!"]
3.57
3.58 fun metis_exhaust_tac ctxt ths =
4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 25 14:25:07 2011 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 25 14:25:07 2011 +0200
4.3 @@ -216,11 +216,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, "mangled_tags?", e_fun_weightN))),
4.8 - (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
4.9 - (0.333, (true, (1000, FOF, "mangled_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, "mangled_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 @@ -293,9 +293,9 @@
4.20 prem_kind = Conjecture,
4.21 best_slices = fn ctxt =>
4.22 (* FUDGE *)
4.23 - [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
4.24 + [(0.333, (false, (150, FOF, "mono_tags", sosN))),
4.25 (0.333, (false, (300, FOF, "poly_tags?", sosN))),
4.26 - (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
4.27 + (0.334, (true, (50, FOF, "mono_tags?", no_sosN)))]
4.28 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
4.29 else I)}
4.30
4.31 @@ -335,8 +335,8 @@
4.32 (* FUDGE *)
4.33 (if is_old_vampire_version () then
4.34 [(0.333, (false, (150, FOF, "poly_guards", sosN))),
4.35 - (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
4.36 - (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
4.37 + (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
4.38 + (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
4.39 else
4.40 [(0.333, (false, (150, TFF, "poly_guards", sosN))),
4.41 (0.334, (true, (50, TFF, "simple", no_sosN))),
4.42 @@ -448,7 +448,7 @@
4.43
4.44 val remote_e =
4.45 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
4.46 - (K (750, FOF, "mangled_tags?") (* FUDGE *))
4.47 + (K (750, FOF, "mono_tags?") (* FUDGE *))
4.48 val remote_leo2 =
4.49 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
4.50 (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
4.51 @@ -461,7 +461,7 @@
4.52 remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
4.53 val remote_e_sine =
4.54 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
4.55 - Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
4.56 + Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
4.57 val remote_snark =
4.58 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
4.59 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
4.60 @@ -475,7 +475,7 @@
4.61 [(OutOfResources, "Too many function symbols"),
4.62 (Crashed, "Unrecoverable Segmentation Fault")]
4.63 Hypothesis Hypothesis
4.64 - (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
4.65 + (K (50, CNF_UEQ, "mono_tags?") (* FUDGE *))
4.66
4.67 (* Setup *)
4.68
5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Aug 25 14:25:07 2011 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Aug 25 14:25:07 2011 +0200
5.3 @@ -20,7 +20,7 @@
5.4 Chained
5.5
5.6 datatype order = First_Order | Higher_Order
5.7 - datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
5.8 + datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
5.9 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
5.10 datatype type_level =
5.11 All_Types |
5.12 @@ -522,7 +522,7 @@
5.13 Chained
5.14
5.15 datatype order = First_Order | Higher_Order
5.16 -datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
5.17 +datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
5.18 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
5.19 datatype type_level =
5.20 All_Types |
5.21 @@ -544,10 +544,10 @@
5.22 (case try (unprefix "poly_") s of
5.23 SOME s => (SOME Polymorphic, s)
5.24 | NONE =>
5.25 - case try (unprefix "mono_") s of
5.26 - SOME s => (SOME Monomorphic, s)
5.27 + case try (unprefix "raw_mono_") s of
5.28 + SOME s => (SOME Raw_Monomorphic, s)
5.29 | NONE =>
5.30 - case try (unprefix "mangled_") s of
5.31 + case try (unprefix "mono_") s of
5.32 SOME s => (SOME Mangled_Monomorphic, s)
5.33 | NONE => (NONE, s))
5.34 ||> (fn s =>
6.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML Thu Aug 25 14:25:07 2011 +0200
6.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu Aug 25 14:25:07 2011 +0200
6.3 @@ -39,7 +39,7 @@
6.4 val partial_typesN = "partial_types"
6.5 val no_typesN = "no_types"
6.6
6.7 -val really_full_type_enc = "mangled_tags_uniform"
6.8 +val really_full_type_enc = "mono_tags_uniform"
6.9 val full_type_enc = "poly_guards_uniform_query"
6.10 val partial_type_enc = "poly_args"
6.11 val no_type_enc = "erased"
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 25 14:25:07 2011 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 25 14:25:07 2011 +0200
7.3 @@ -148,7 +148,7 @@
7.4 | _ => value)
7.5 | NONE => (name, value)
7.6
7.7 -(* Ensure that type systems such as "simple!" and "mangled_guards?" are handled
7.8 +(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
7.9 correctly. *)
7.10 fun implode_param [s, "?"] = s ^ "?"
7.11 | implode_param [s, "!"] = s ^ "!"