--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 23 16:53:05 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 23 17:12:54 2011 +0200
@@ -176,14 +176,14 @@
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
+with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
-reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
-say, Vampire 11.5.}%
+reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
+than, say, Vampire 9.0 or 11.5.}%
. Since the ATPs' output formats are neither documented nor stable, other
versions of the ATPs might or might not work well with Sledgehammer. Ideally,
also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.3'').
+\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.4'').
\end{enum}
To check whether E and SPASS are successfully installed, follow the example in
@@ -750,7 +750,9 @@
prover developed by Andrei Voronkov and his colleagues
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
-executable. Sledgehammer has been tested with versions 11, 0.6, and 1.0.
+executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
+Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
+supports the TPTP many-typed first-order format (TFF).
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
SRI \cite{yices}. To use Yices, set the environment variable
@@ -760,12 +762,13 @@
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name, and set \texttt{Z3\_NON\_COMMERCIAL=yes} to confirm that you are a
+name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
-\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
-ATP, exploiting Z3's undocumented support for the TPTP format. It is included
-for experimental purposes. It requires version 2.18 or above.
+\item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
+an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
+formats (FOF and TFF). It is included for experimental purposes. It requires
+version 3.0 or above.
\end{enum}
In addition, the following remote provers are supported:
@@ -799,7 +802,7 @@
Geoff Sutcliffe's Miami servers.
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
+Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used.
\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
@@ -811,8 +814,8 @@
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
point).
-\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3
-as an ATP'' runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
+with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
@@ -929,7 +932,7 @@
\item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
higher-order types if the prover supports the THF syntax; otherwise, fall back
-on \textit{simple} or \textit{mangled\_guards\_heavy}. The problem is
+on \textit{simple} or \textit{mangled\_guards\_uniform}. The problem is
monomorphized.
\item[$\bullet$]
@@ -960,17 +963,17 @@
finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
the types are not actually erased but rather replaced by a shared uniform type
of individuals.) As argument to the \textit{metis} proof method, the exclamation
-mark is replaced by a \hbox{``\textit{\_bang}''} suffix.
+mark is replaced by the suffix \hbox{``\textit{\_bang}''}.
\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient virtually sound encoding for that ATP.
\end{enum}
In addition, all the \textit{guards} and \textit{tags} type encodings are
-available in two variants, a lightweight and a heavyweight variant. The
-lightweight variants are generally more efficient and are the default; the
-heavyweight variants are identified by a \textit{\_heavy} suffix (e.g.,
-\textit{mangled\_guards\_heavy}{?}).
+available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
+nonuniform variants are generally more efficient and are the default; the
+uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
+\textit{mangled\_guards\_uniform}{?}).
For SMT solvers, the type encoding is always \textit{simple}, irrespective of
the value of this option.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_Set.thy Tue Aug 23 17:12:54 2011 +0200
@@ -0,0 +1,77 @@
+(* Title: HOL/Library/Quotient_Set.thy
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+
+header {* Quotient infrastructure for the set type *}
+
+theory Quotient_Set
+imports Main Quotient_Syntax
+begin
+
+lemma set_quotient [quot_thm]:
+ assumes "Quotient R Abs Rep"
+ shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
+proof (rule QuotientI)
+ from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+ then show "\<And>xs. Rep -` (Abs -` xs) = xs"
+ unfolding vimage_def by auto
+next
+ show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
+ unfolding set_rel_def vimage_def
+ by auto (metis Quotient_rel_abs[OF assms])+
+next
+ fix r s
+ show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
+ unfolding set_rel_def vimage_def set_eq_iff
+ by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
+qed
+
+lemma empty_set_rsp[quot_respect]:
+ "set_rel R {} {}"
+ unfolding set_rel_def by simp
+
+lemma collect_rsp[quot_respect]:
+ assumes "Quotient R Abs Rep"
+ shows "((R ===> op =) ===> set_rel R) Collect Collect"
+ by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
+
+lemma collect_prs[quot_preserve]:
+ assumes "Quotient R Abs Rep"
+ shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
+ unfolding fun_eq_iff
+ by (simp add: Quotient_abs_rep[OF assms])
+
+lemma union_rsp[quot_respect]:
+ assumes "Quotient R Abs Rep"
+ shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
+ by (intro fun_relI) (auto simp add: set_rel_def)
+
+lemma union_prs[quot_preserve]:
+ assumes "Quotient R Abs Rep"
+ shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
+ unfolding fun_eq_iff
+ by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+
+lemma diff_rsp[quot_respect]:
+ assumes "Quotient R Abs Rep"
+ shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
+ by (intro fun_relI) (auto simp add: set_rel_def)
+
+lemma diff_prs[quot_preserve]:
+ assumes "Quotient R Abs Rep"
+ shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
+ unfolding fun_eq_iff
+ by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
+
+lemma inter_rsp[quot_respect]:
+ assumes "Quotient R Abs Rep"
+ shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
+ by (intro fun_relI) (auto simp add: set_rel_def)
+
+lemma inter_prs[quot_preserve]:
+ assumes "Quotient R Abs Rep"
+ shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
+ unfolding fun_eq_iff
+ by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+
+end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Aug 23 17:12:54 2011 +0200
@@ -22,51 +22,49 @@
lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
ML {*
-(* The commented-out type systems are too incomplete for our exhaustive
- tests. *)
val type_encs =
["erased",
"poly_guards",
- "poly_guards_heavy",
+ "poly_guards_uniform",
"poly_tags",
- "poly_tags_heavy",
+ "poly_tags_uniform",
"poly_args",
"mono_guards",
- "mono_guards_heavy",
+ "mono_guards_uniform",
"mono_tags",
- "mono_tags_heavy",
+ "mono_tags_uniform",
"mono_args",
"mangled_guards",
- "mangled_guards_heavy",
+ "mangled_guards_uniform",
"mangled_tags",
- "mangled_tags_heavy",
+ "mangled_tags_uniform",
"mangled_args",
"simple",
"poly_guards?",
- "poly_guards_heavy?",
+ "poly_guards_uniform?",
"poly_tags?",
-(* "poly_tags_heavy?", *)
+ "poly_tags_uniform?",
"mono_guards?",
- "mono_guards_heavy?",
+ "mono_guards_uniform?",
"mono_tags?",
- "mono_tags_heavy?",
+ "mono_tags_uniform?",
"mangled_guards?",
- "mangled_guards_heavy?",
+ "mangled_guards_uniform?",
"mangled_tags?",
- "mangled_tags_heavy?",
+ "mangled_tags_uniform?",
"simple?",
"poly_guards!",
- "poly_guards_heavy!",
-(* "poly_tags!", *)
- "poly_tags_heavy!",
+ "poly_guards_uniform!",
+ "poly_tags!",
+ "poly_tags_uniform!",
"mono_guards!",
- "mono_guards_heavy!",
+ "mono_guards_uniform!",
"mono_tags!",
- "mono_tags_heavy!",
+ "mono_tags_uniform!",
"mangled_guards!",
- "mangled_guards_heavy!",
+ "mangled_guards_uniform!",
"mangled_tags!",
- "mangled_tags_heavy!",
+ "mangled_tags_uniform!",
"simple!"]
fun metis_exhaust_tac ctxt ths =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 23 17:12:54 2011 +0200
@@ -361,7 +361,7 @@
fun set_file_name (SOME dir) =
Config.put Sledgehammer_Provers.dest_dir dir
#> Config.put Sledgehammer_Provers.problem_prefix
- ("prob_" ^ str0 (Position.line_of pos))
+ ("prob_" ^ str0 (Position.line_of pos) ^ "__")
#> Config.put SMT_Config.debug_files
(dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
^ serial_string ())
--- a/src/HOL/Predicate.thy Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Predicate.thy Tue Aug 23 17:12:54 2011 +0200
@@ -47,7 +47,7 @@
done
lemma rev_predicate1D:
- "P x ==> P <= Q ==> Q x"
+ "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
by (rule predicate1D)
lemma predicate2I [Pure.intro!, intro!]:
@@ -67,100 +67,100 @@
done
lemma rev_predicate2D:
- "P x y ==> P <= Q ==> Q x y"
+ "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
by (rule predicate2D)
subsubsection {* Equality *}
-lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
- by (simp add: mem_def)
+lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
+ by (simp add: set_eq_iff fun_eq_iff mem_def)
-lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
- by (simp add: fun_eq_iff mem_def)
+lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
+ by (simp add: set_eq_iff fun_eq_iff mem_def)
subsubsection {* Order relation *}
-lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
- by (simp add: mem_def)
+lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+ by (simp add: subset_iff le_fun_def mem_def)
-lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
- by fast
+lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+ by (simp add: subset_iff le_fun_def mem_def)
subsubsection {* Top and bottom elements *}
-lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
+lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
by (simp add: bot_fun_def)
-lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
+lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
by (simp add: bot_fun_def)
-lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
+lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
by (auto simp add: fun_eq_iff)
-lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
+lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
by (auto simp add: fun_eq_iff)
-lemma top1I [intro!]: "top x"
+lemma top1I [intro!]: "\<top> x"
by (simp add: top_fun_def)
-lemma top2I [intro!]: "top x y"
+lemma top2I [intro!]: "\<top> x y"
by (simp add: top_fun_def)
subsubsection {* Binary intersection *}
-lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
+lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
by (simp add: inf_fun_def)
-lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
+lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
by (simp add: inf_fun_def)
-lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
+lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: inf_fun_def)
-lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
+lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: inf_fun_def)
-lemma inf1D1: "inf A B x ==> A x"
+lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
by (simp add: inf_fun_def)
-lemma inf2D1: "inf A B x y ==> A x y"
+lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
by (simp add: inf_fun_def)
-lemma inf1D2: "inf A B x ==> B x"
+lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
by (simp add: inf_fun_def)
-lemma inf2D2: "inf A B x y ==> B x y"
+lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
by (simp add: inf_fun_def)
-lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
by (simp add: inf_fun_def mem_def)
-lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
+lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
by (simp add: inf_fun_def mem_def)
subsubsection {* Binary union *}
-lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
+lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
by (simp add: sup_fun_def)
-lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
+lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
by (simp add: sup_fun_def)
-lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
+lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
by (simp add: sup_fun_def)
-lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
+lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
by (simp add: sup_fun_def)
-lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
+lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: sup_fun_def) iprover
-lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
+lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: sup_fun_def) iprover
text {*
@@ -168,76 +168,76 @@
@{text B}.
*}
-lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
+lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
by (auto simp add: sup_fun_def)
-lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
+lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
by (auto simp add: sup_fun_def)
-lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
+lemma sup_Un_eq: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
by (simp add: sup_fun_def mem_def)
-lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
+lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
by (simp add: sup_fun_def mem_def)
subsubsection {* Intersections of families *}
-lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
+lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
by (simp add: INFI_apply)
-lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
+lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
by (simp add: INFI_apply)
-lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
+lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
by (auto simp add: INFI_apply)
-lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
+lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
by (auto simp add: INFI_apply)
-lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
+lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
by (auto simp add: INFI_apply)
-lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
+lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
by (auto simp add: INFI_apply)
-lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
+lemma INF1_E [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
by (auto simp add: INFI_apply)
-lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
+lemma INF2_E [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
by (auto simp add: INFI_apply)
-lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
+lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
by (simp add: INFI_apply fun_eq_iff)
-lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
+lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
by (simp add: INFI_apply fun_eq_iff)
subsubsection {* Unions of families *}
-lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
+lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
by (simp add: SUPR_apply)
-lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
+lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
by (simp add: SUPR_apply)
-lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
+lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
by (auto simp add: SUPR_apply)
-lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
+lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
by (auto simp add: SUPR_apply)
-lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
+lemma SUP1_E [elim!]: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
by (auto simp add: SUPR_apply)
-lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
+lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
by (auto simp add: SUPR_apply)
-lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
+lemma SUP_UN_eq: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
by (simp add: SUPR_apply fun_eq_iff)
-lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
+lemma SUP_UN_eq2: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
by (simp add: SUPR_apply fun_eq_iff)
@@ -245,12 +245,9 @@
subsubsection {* Composition *}
-inductive
- pred_comp :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
- (infixr "OO" 75)
- for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
-where
- pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
+inductive pred_comp :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
+ pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
inductive_cases pred_compE [elim!]: "(r OO s) a c"
@@ -261,12 +258,9 @@
subsubsection {* Converse *}
-inductive
- conversep :: "('a => 'b => bool) => 'b => 'a => bool"
- ("(_^--1)" [1000] 1000)
- for r :: "'a => 'b => bool"
-where
- conversepI: "r a b ==> r^--1 b a"
+inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+ conversepI: "r a b \<Longrightarrow> r^--1 b a"
notation (xsymbols)
conversep ("(_\<inverse>\<inverse>)" [1000] 1000)
@@ -290,13 +284,13 @@
by (iprover intro: order_antisym conversepI pred_compI
elim: pred_compE dest: conversepD)
-lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
+lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
-lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
+lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
-lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
+lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
by (auto simp add: fun_eq_iff)
lemma conversep_eq [simp]: "(op =)^--1 = op ="
@@ -305,11 +299,9 @@
subsubsection {* Domain *}
-inductive
- DomainP :: "('a => 'b => bool) => 'a => bool"
- for r :: "'a => 'b => bool"
-where
- DomainPI [intro]: "r a b ==> DomainP r a"
+inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+ DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
inductive_cases DomainPE [elim!]: "DomainP r a"
@@ -319,11 +311,9 @@
subsubsection {* Range *}
-inductive
- RangeP :: "('a => 'b => bool) => 'b => bool"
- for r :: "'a => 'b => bool"
-where
- RangePI [intro]: "r a b ==> RangeP r b"
+inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+ RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
inductive_cases RangePE [elim!]: "RangeP r b"
@@ -333,9 +323,8 @@
subsubsection {* Inverse image *}
-definition
- inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
- "inv_imagep r f == %x y. r (f x) (f y)"
+definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+ "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
by (simp add: inv_image_def inv_imagep_def)
@@ -347,7 +336,7 @@
subsubsection {* Powerset *}
definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
- "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
+ "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
by (auto simp add: Powp_def fun_eq_iff)
@@ -357,14 +346,14 @@
subsubsection {* Properties of relations *}
-abbreviation antisymP :: "('a => 'a => bool) => bool" where
- "antisymP r == antisym {(x, y). r x y}"
+abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "antisymP r \<equiv> antisym {(x, y). r x y}"
-abbreviation transP :: "('a => 'a => bool) => bool" where
- "transP r == trans {(x, y). r x y}"
+abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "transP r \<equiv> trans {(x, y). r x y}"
-abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
- "single_valuedP r == single_valued {(x, y). r x y}"
+abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+ "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
@@ -474,17 +463,17 @@
by (simp add: Sup_pred_def)
instance proof
-qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def)
+qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def le_fun_def less_fun_def)
end
lemma eval_INFI [simp]:
"eval (INFI A f) = INFI A (eval \<circ> f)"
- by (unfold INFI_def) simp
+ by (simp only: INFI_def eval_Inf image_compose)
lemma eval_SUPR [simp]:
"eval (SUPR A f) = SUPR A (eval \<circ> f)"
- by (unfold SUPR_def) simp
+ by (simp only: SUPR_def eval_Sup image_compose)
instantiation pred :: (type) complete_boolean_algebra
begin
@@ -504,7 +493,7 @@
by (simp add: minus_pred_def)
instance proof
-qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply)
+qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
end
@@ -524,7 +513,7 @@
lemma bind_bind:
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
- by (rule pred_eqI) auto
+ by (rule pred_eqI) (auto simp add: SUP_apply)
lemma bind_single:
"P \<guillemotright>= single = P"
@@ -544,7 +533,7 @@
lemma Sup_bind:
"(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
- by (rule pred_eqI) auto
+ by (rule pred_eqI) (auto simp add: SUP_apply)
lemma pred_iffI:
assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -589,8 +578,7 @@
lemma not_bot:
assumes "A \<noteq> \<bottom>"
obtains x where "eval A x"
- using assms by (cases A)
- (auto simp add: bot_pred_def, auto simp add: mem_def)
+ using assms by (cases A) (auto simp add: bot_pred_def, simp add: mem_def)
subsubsection {* Emptiness check and definite choice *}
@@ -761,7 +749,7 @@
assumes "P \<bottom>"
assumes "P (single ())"
shows "P Q"
-using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
+using assms unfolding bot_pred_def bot_fun_def bot_bool_def empty_def single_def proof (cases Q)
fix f
assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
then have "P (Pred f)"
@@ -790,7 +778,7 @@
lemma eval_map [simp]:
"eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
- by (auto simp add: map_def)
+ by (auto simp add: map_def comp_def)
enriched_type map: map
by (rule ext, rule pred_eqI, auto)+
@@ -801,9 +789,9 @@
datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
- "pred_of_seq Empty = \<bottom>"
- | "pred_of_seq (Insert x P) = single x \<squnion> P"
- | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
+ "pred_of_seq Empty = \<bottom>"
+| "pred_of_seq (Insert x P) = single x \<squnion> P"
+| "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
"Seq f = pred_of_seq (f ())"
@@ -812,8 +800,8 @@
primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool" where
"member Empty x \<longleftrightarrow> False"
- | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
- | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
+| "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
+| "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
lemma eval_member:
"member xq = eval (pred_of_seq xq)"
@@ -836,9 +824,9 @@
unfolding Seq_def by simp
primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
- "apply f Empty = Empty"
- | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
- | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
+ "apply f Empty = Empty"
+| "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
+| "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
lemma apply_bind:
"pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
@@ -862,9 +850,9 @@
unfolding Seq_def by simp
primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
- "adjunct P Empty = Join P Empty"
- | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
- | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
+ "adjunct P Empty = Join P Empty"
+| "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
+| "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
lemma adjunct_sup:
"pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
@@ -891,13 +879,13 @@
qed
primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
- "contained Empty Q \<longleftrightarrow> True"
- | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
- | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
+ "contained Empty Q \<longleftrightarrow> True"
+| "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
+| "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
lemma single_less_eq_eval:
"single x \<le> P \<longleftrightarrow> eval P x"
- by (auto simp add: single_def less_eq_pred_def mem_def)
+ by (auto simp add: less_eq_pred_def le_fun_def)
lemma contained_less_eq:
"contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
@@ -934,9 +922,9 @@
by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
primrec null :: "'a seq \<Rightarrow> bool" where
- "null Empty \<longleftrightarrow> True"
- | "null (Insert x P) \<longleftrightarrow> False"
- | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
+ "null Empty \<longleftrightarrow> True"
+| "null (Insert x P) \<longleftrightarrow> False"
+| "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
lemma null_is_empty:
"null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
@@ -948,8 +936,8 @@
primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
[code del]: "the_only dfault Empty = dfault ()"
- | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
- | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
+| "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
+| "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
else let x = singleton dfault P; y = the_only dfault xq in
if x = y then x else dfault ())"
@@ -973,23 +961,21 @@
(auto simp add: Seq_def the_only_singleton is_empty_def
null_is_empty singleton_bot singleton_single singleton_sup Let_def)
-definition not_unique :: "'a pred => 'a"
-where
- [code del]: "not_unique A = (THE x. eval A x)"
-
-definition the :: "'a pred => 'a"
-where
+definition the :: "'a pred \<Rightarrow> 'a" where
"the A = (THE x. eval A x)"
lemma the_eqI:
"(THE x. eval P x) = x \<Longrightarrow> the P = x"
by (simp add: the_def)
+definition not_unique :: "'a pred \<Rightarrow> 'a" where
+ [code del]: "not_unique A = (THE x. eval A x)"
+
+code_abort not_unique
+
lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
by (rule the_eqI) (simp add: singleton_def not_unique_def)
-code_abort not_unique
-
code_reflect Predicate
datatypes pred = Seq and seq = Empty | Insert | Join
functions map
--- a/src/HOL/Quotient.thy Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Quotient.thy Tue Aug 23 17:12:54 2011 +0200
@@ -69,6 +69,24 @@
shows "((op =) ===> (op =)) = (op =)"
by (auto simp add: fun_eq_iff elim: fun_relE)
+subsection {* set map (vimage) and set relation *}
+
+definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
+
+lemma vimage_id:
+ "vimage id = id"
+ unfolding vimage_def fun_eq_iff by auto
+
+lemma set_rel_eq:
+ "set_rel op = = op ="
+ by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
+
+lemma set_rel_equivp:
+ assumes e: "equivp R"
+ shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
+ unfolding set_rel_def
+ using equivp_reflp[OF e]
+ by auto (metis equivp_symp[OF e])+
subsection {* Quotient Predicate *}
@@ -665,6 +683,7 @@
setup Quotient_Info.setup
declare [[map "fun" = (map_fun, fun_rel)]]
+declare [[map set = (vimage, set_rel)]]
lemmas [quot_thm] = fun_quotient
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
@@ -680,6 +699,8 @@
id_o
o_id
eq_comp_r
+ set_rel_eq
+ vimage_id
text {* Translation functions for the lifting process. *}
use "Tools/Quotient/quotient_term.ML"
--- a/src/HOL/TPTP/ATP_Export.thy Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/TPTP/ATP_Export.thy Tue Aug 23 17:12:54 2011 +0200
@@ -27,8 +27,8 @@
ML {*
if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy"
- "/tmp/infs_poly_tags_heavy.tptp"
+ ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_uniform"
+ "/tmp/infs_poly_tags_uniform.tptp"
else
()
*}
--- a/src/HOL/TPTP/atp_export.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Tue Aug 23 17:12:54 2011 +0200
@@ -152,15 +152,15 @@
fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
let
val format = FOF
- val type_enc = type_enc |> type_enc_from_string
+ val type_enc = type_enc |> type_enc_from_string Sound
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
val (atp_problem, _, _, _, _, _, _) =
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
- |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
- combinatorsN false true [] @{prop False}
+ |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN
+ false true [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 23 17:12:54 2011 +0200
@@ -30,8 +30,10 @@
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
- Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
- * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
+ Formula of string * formula_kind
+ * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+ * (string, string ho_type) ho_term option
+ * (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
val tptp_cnf : string
@@ -503,6 +505,7 @@
s
else
s |> no_qualifiers
+ |> perhaps (try (unprefix "'"))
|> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
|> (fn s =>
if size s > max_readable_name_size then
@@ -526,7 +529,7 @@
fun add j =
let
val nice_name =
- nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j)
+ nice_prefix ^ (if j = 0 then "" else string_of_int j)
in
case Symtab.lookup (snd the_pool) nice_name of
SOME full_name' =>
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 23 17:12:54 2011 +0200
@@ -348,7 +348,6 @@
Scan.optional ($$ "," |-- parse_annotation
--| Scan.option ($$ "," |-- parse_annotations)) []
-val vampire_unknown_fact = "unknown"
val waldmeister_conjecture = "conjecture_1"
val tofof_fact_prefix = "fof_"
@@ -408,9 +407,7 @@
case deps of
["file", _, s] =>
((num,
- if s = vampire_unknown_fact then
- NONE
- else if s = waldmeister_conjecture then
+ if s = waldmeister_conjecture then
find_formula_in_problem problem (mk_anot phi)
else
SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]),
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Aug 23 17:12:54 2011 +0200
@@ -165,6 +165,12 @@
exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
| _ => false)
+(* (quasi-)underapproximation of the truth *)
+fun is_locality_global Local = false
+ | is_locality_global Assum = false
+ | is_locality_global Chained = false
+ | is_locality_global _ = true
+
fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE
| used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset
fact_names atp_proof =
@@ -386,7 +392,7 @@
| NONE => NONE)
(nth us (length us - 2))
end
- else if s' = type_pred_name then
+ else if s' = type_guard_name then
@{const True} (* ignore type predicates *)
else
let
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 17:12:54 2011 +0200
@@ -21,9 +21,8 @@
known_failures : (failure * string) list,
conj_sym_kind : formula_kind,
prem_kind : formula_kind,
- formats : format list,
best_slices :
- Proof.context -> (real * (bool * (int * string * string))) list}
+ Proof.context -> (real * (bool * (int * format * string * string))) list}
val force_sos : bool Config.T
val e_smartN : string
@@ -46,12 +45,12 @@
val snarkN : string
val e_tofofN : string
val waldmeisterN : string
- val z3_atpN : string
+ val z3_tptpN : string
val remote_prefix : string
val remote_atp :
string -> string -> string list -> (string * string) list
- -> (failure * string) list -> formula_kind -> formula_kind -> format list
- -> (Proof.context -> int * string) -> string * atp_config
+ -> (failure * string) list -> formula_kind -> formula_kind
+ -> (Proof.context -> int * format * string) -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -78,9 +77,8 @@
known_failures : (failure * string) list,
conj_sym_kind : formula_kind,
prem_kind : formula_kind,
- formats : format list,
best_slices :
- Proof.context -> (real * (bool * (int * string * string))) list}
+ Proof.context -> (real * (bool * (int * format * string * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
the ATPs are run in parallel. The "real" components give the faction of the
@@ -106,7 +104,7 @@
val satallaxN = "satallax"
val spassN = "spass"
val vampireN = "vampire"
-val z3_atpN = "z3_atp"
+val z3_tptpN = "z3_tptp"
val e_sineN = "e_sine"
val snarkN = "snark"
val e_tofofN = "e_tofof"
@@ -132,6 +130,8 @@
(* E *)
+fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
+
val tstp_proof_delims =
[("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
@@ -190,8 +190,6 @@
\1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
\FIFOWeight(PreferProcessed))'"
-fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
-
fun effective_e_weight_method ctxt =
if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
@@ -214,16 +212,15 @@
(OutOfResources, "SZS status ResourceOut")],
conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
- formats = [FOF],
best_slices = fn ctxt =>
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
- (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
- (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
+ [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
+ (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
+ (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, "mangled_tags?", method)))]
+ [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
end}
val e = (eN, e_config)
@@ -242,11 +239,10 @@
known_failures = [],
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
- formats = [THF Without_Choice, FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (150, "simple_higher", sosN))),
- (0.333, (true, (50, "simple_higher", no_sosN)))]
+ [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
+ (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -265,8 +261,8 @@
known_failures = [(ProofMissing, "SZS status Theorem")],
conj_sym_kind = Axiom,
prem_kind = Hypothesis,
- formats = [THF With_Choice],
- best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+ best_slices =
+ K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
val satallax = (satallaxN, satallax_config)
@@ -290,16 +286,16 @@
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
+ (Unprovable, "No formulae and clauses found in input file"),
(SpassTooOld, "tptp2dfg"),
(InternalError, "Please report this error")],
conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
- formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, "mangled_tags", sosN))),
- (0.333, (false, (300, "poly_tags?", sosN))),
- (0.334, (true, (50, "mangled_tags?", no_sosN)))]
+ [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
+ (0.333, (false, (300, FOF, "poly_tags?", sosN))),
+ (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -308,12 +304,16 @@
(* Vampire *)
+fun is_old_vampire_version () =
+ string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS
+
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
- "--proof tptp --mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
- " --thanks \"Andrei and Krystof\" --input_file"
+ "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
+ " --proof tptp --output_axiom_names on \
+ \ --thanks \"Andrei and Krystof\" --input_file"
|> sos = sosN ? prefix "--sos on ",
proof_delims =
[("=========== Refutation ==========",
@@ -332,12 +332,16 @@
(Interrupted, "Aborted by signal SIGINT")],
conj_sym_kind = Conjecture,
prem_kind = Conjecture,
- formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, "poly_guards", sosN))),
- (0.334, (true, (50, "mangled_guards?", no_sosN))),
- (0.333, (false, (500, "mangled_tags?", sosN)))]
+ (if is_old_vampire_version () then
+ [(0.333, (false, (150, FOF, "poly_guards", sosN))),
+ (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+ (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
+ else
+ [(0.333, (false, (150, TFF, "poly_guards", sosN))),
+ (0.334, (true, (50, TFF, "simple", no_sosN))),
+ (0.333, (false, (500, TFF, "simple", sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -346,29 +350,28 @@
(* Z3 with TPTP syntax *)
-val z3_atp_config : atp_config =
+val z3_tptp_config : atp_config =
{exec = ("Z3_HOME", "z3"),
required_execs = [],
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "MBQI=true -p -t:" ^ string_of_int (to_secs 1 timeout),
+ "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
proof_delims = [],
known_failures =
- [(Unprovable, "\nsat"),
- (GaveUp, "\nunknown"),
- (GaveUp, "SZS status Satisfiable"),
- (ProofMissing, "\nunsat"),
- (ProofMissing, "SZS status Unsatisfiable")],
+ [(GaveUp, "SZS status Satisfiable"),
+ (GaveUp, "SZS status CounterSatisfiable"),
+ (GaveUp, "SZS status GaveUp"),
+ (ProofMissing, "SZS status Unsatisfiable"),
+ (ProofMissing, "SZS status Theorem")],
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
- formats = [FOF],
best_slices =
- (* FUDGE (FIXME) *)
- K [(0.5, (false, (250, "mangled_guards?", ""))),
- (0.25, (false, (125, "mangled_guards?", ""))),
- (0.125, (false, (62, "mangled_guards?", ""))),
- (0.125, (false, (31, "mangled_guards?", "")))]}
+ (* FUDGE *)
+ K [(0.5, (false, (250, TFF, "simple", ""))),
+ (0.25, (false, (125, TFF, "simple", ""))),
+ (0.125, (false, (62, TFF, "simple", ""))),
+ (0.125, (false, (31, TFF, "simple", "")))]}
-val z3_atp = (z3_atpN, z3_atp_config)
+val z3_tptp = (z3_tptpN, z3_tptp_config)
(* Remote ATP invocation via SystemOnTPTP *)
@@ -406,7 +409,7 @@
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
fun remote_config system_name system_versions proof_delims known_failures
- conj_sym_kind prem_kind formats best_slice : atp_config =
+ conj_sym_kind prem_kind best_slice : atp_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
@@ -424,58 +427,56 @@
(Inappropriate, "says Inappropriate")],
conj_sym_kind = conj_sym_kind,
prem_kind = prem_kind,
- formats = formats,
best_slices = fn ctxt =>
- let val (max_relevant, type_enc) = best_slice ctxt in
- [(1.0, (false, (max_relevant, type_enc, "")))]
+ let val (max_relevant, format, type_enc) = best_slice ctxt in
+ [(1.0, (false, (max_relevant, format, type_enc, "")))]
end}
fun remotify_config system_name system_versions best_slice
- ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...}
+ ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
: atp_config) : atp_config =
remote_config system_name system_versions proof_delims known_failures
- conj_sym_kind prem_kind formats best_slice
+ conj_sym_kind prem_kind best_slice
fun remote_atp name system_name system_versions proof_delims known_failures
- conj_sym_kind prem_kind formats best_slice =
+ conj_sym_kind prem_kind best_slice =
(remote_prefix ^ name,
remote_config system_name system_versions proof_delims known_failures
- conj_sym_kind prem_kind formats best_slice)
+ conj_sym_kind prem_kind best_slice)
fun remotify_atp (name, config) system_name system_versions best_slice =
(remote_prefix ^ name,
remotify_config system_name system_versions best_slice config)
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, "mangled_tags?") (* FUDGE *))
+ (K (750, FOF, "mangled_tags?") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
- (K (100, "simple_higher") (* FUDGE *))
+ (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
val remote_satallax =
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
- (K (100, "simple_higher") (* FUDGE *))
+ (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
- (K (200, "mangled_guards?") (* FUDGE *))
-val remote_z3_atp =
- remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
+ remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
+val remote_z3_tptp =
+ remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
- Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
+ Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- [TFF, FOF] (K (100, "simple") (* FUDGE *))
+ (K (100, TFF, "simple") (* FUDGE *))
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
+ Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
[(OutOfResources, "Too many function symbols"),
(Crashed, "Unrecoverable Segmentation Fault")]
- Hypothesis Hypothesis [CNF_UEQ]
- (K (50, "mangled_tags?") (* FUDGE *))
+ Hypothesis Hypothesis
+ (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
(* Setup *)
@@ -498,8 +499,8 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
- remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+ [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
+ remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 23 17:12:54 2011 +0200
@@ -21,15 +21,19 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+ datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
datatype type_level =
- All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
+ All_Types |
+ Noninf_Nonmono_Types of soundness |
+ Fin_Nonmono_Types |
+ Const_Arg_Types |
No_Types
- datatype type_heaviness = Heavyweight | Lightweight
+ datatype type_uniformity = Uniform | Nonuniform
datatype type_enc =
Simple_Types of order * type_level |
- Guards of polymorphism * type_level * type_heaviness |
- Tags of polymorphism * type_level * type_heaviness
+ Guards of polymorphism * type_level * type_uniformity |
+ Tags of polymorphism * type_level * type_uniformity
val no_lambdasN : string
val concealedN : string
@@ -38,7 +42,6 @@
val hybridN : string
val lambdasN : string
val smartN : string
- val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
val tvar_prefix : string
@@ -53,7 +56,7 @@
val type_decl_prefix : string
val sym_decl_prefix : string
val guards_sym_formula_prefix : string
- val lightweight_tags_sym_formula_prefix : string
+ val tags_sym_formula_prefix : string
val fact_prefix : string
val conjecture_prefix : string
val helper_prefix : string
@@ -65,8 +68,8 @@
val type_tag_idempotence_helper_name : string
val predicator_name : string
val app_op_name : string
+ val type_guard_name : string
val type_tag_name : string
- val type_pred_name : string
val simple_type_prefix : string
val prefixed_predicator_name : string
val prefixed_app_op_name : string
@@ -81,14 +84,13 @@
val new_skolem_var_name_from_const : string -> string
val atp_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
- val is_locality_global : locality -> bool
- val type_enc_from_string : string -> type_enc
+ val type_enc_from_string : soundness -> string -> type_enc
val is_type_enc_higher_order : type_enc -> bool
val polymorphism_of_type_enc : type_enc -> polymorphism
val level_of_type_enc : type_enc -> type_level
- val is_type_enc_virtually_sound : type_enc -> bool
+ val is_type_enc_quasi_sound : type_enc -> bool
val is_type_enc_fairly_sound : type_enc -> bool
- val choose_format : format list -> type_enc -> format * type_enc
+ val adjust_type_enc : format -> type_enc -> type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -96,7 +98,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
+ Proof.context -> format -> formula_kind -> formula_kind -> type_enc
-> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -131,6 +133,8 @@
val simpN = "simp"
val bound_var_prefix = "B_"
+val all_bound_var_prefix = "BA_"
+val exist_bound_var_prefix = "BE_"
val schematic_var_prefix = "V_"
val fixed_var_prefix = "v_"
val tvar_prefix = "T_"
@@ -148,7 +152,7 @@
val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
val guards_sym_formula_prefix = "gsy_"
-val lightweight_tags_sym_formula_prefix = "tsy_"
+val tags_sym_formula_prefix = "tsy_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
@@ -163,8 +167,8 @@
val predicator_name = "hBOOL"
val app_op_name = "hAPP"
-val type_tag_name = "ti"
-val type_pred_name = "is"
+val type_guard_name = "g"
+val type_tag_name = "t"
val simple_type_prefix = "ty_"
val prefixed_predicator_name = const_prefix ^ predicator_name
@@ -294,6 +298,8 @@
| ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
fun make_bound_var x = bound_var_prefix ^ ascii_of x
+fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
+fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
@@ -502,43 +508,39 @@
else
IVar ((make_schematic_var v, s), T), atyps_of T)
| iterm_from_term _ bs (Bound j) =
- nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T))
+ nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
| iterm_from_term thy bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
- val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t
- in
- (IAbs ((`make_bound_var s, T), tm),
- union (op =) atomic_Ts (atyps_of T))
- end
+ val name = `make_bound_var s
+ val (tm, atomic_Ts) = iterm_from_term thy ((s, (name, T)) :: bs) t
+ in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
datatype locality =
General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
Chained
-(* (quasi-)underapproximation of the truth *)
-fun is_locality_global Local = false
- | is_locality_global Assum = false
- | is_locality_global Chained = false
- | is_locality_global _ = true
-
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
datatype type_level =
- All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
+ All_Types |
+ Noninf_Nonmono_Types of soundness |
+ Fin_Nonmono_Types |
+ Const_Arg_Types |
No_Types
-datatype type_heaviness = Heavyweight | Lightweight
+datatype type_uniformity = Uniform | Nonuniform
datatype type_enc =
Simple_Types of order * type_level |
- Guards of polymorphism * type_level * type_heaviness |
- Tags of polymorphism * type_level * type_heaviness
+ Guards of polymorphism * type_level * type_uniformity |
+ Tags of polymorphism * type_level * type_uniformity
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-fun type_enc_from_string s =
+fun type_enc_from_string soundness s =
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
| NONE =>
@@ -552,30 +554,31 @@
(* "_query" and "_bang" are for the ASCII-challenged Metis and
Mirabelle. *)
case try_unsuffixes ["?", "_query"] s of
- SOME s => (Noninf_Nonmono_Types, s)
+ SOME s => (Noninf_Nonmono_Types soundness, s)
| NONE =>
case try_unsuffixes ["!", "_bang"] s of
SOME s => (Fin_Nonmono_Types, s)
| NONE => (All_Types, s))
||> apsnd (fn s =>
- case try (unsuffix "_heavy") s of
- SOME s => (Heavyweight, s)
- | NONE => (Lightweight, s))
- |> (fn (poly, (level, (heaviness, core))) =>
- case (core, (poly, level, heaviness)) of
- ("simple", (NONE, _, Lightweight)) =>
+ case try (unsuffix "_uniform") s of
+ SOME s => (Uniform, s)
+ | NONE => (Nonuniform, s))
+ |> (fn (poly, (level, (uniformity, core))) =>
+ case (core, (poly, level, uniformity)) of
+ ("simple", (NONE, _, Nonuniform)) =>
Simple_Types (First_Order, level)
- | ("simple_higher", (NONE, _, Lightweight)) =>
- if level = Noninf_Nonmono_Types then raise Same.SAME
- else Simple_Types (Higher_Order, level)
- | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
+ | ("simple_higher", (NONE, _, Nonuniform)) =>
+ (case level of
+ Noninf_Nonmono_Types _ => raise Same.SAME
+ | _ => Simple_Types (Higher_Order, level))
+ | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
| ("tags", (SOME Polymorphic, _, _)) =>
- Tags (Polymorphic, level, heaviness)
- | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
- | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
- Guards (poly, Const_Arg_Types, Lightweight)
- | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
- Guards (Polymorphic, No_Types, Lightweight)
+ Tags (Polymorphic, level, uniformity)
+ | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
+ | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
+ Guards (poly, Const_Arg_Types, Nonuniform)
+ | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
+ Guards (Polymorphic, No_Types, Nonuniform)
| _ => raise Same.SAME)
handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
@@ -590,37 +593,32 @@
| level_of_type_enc (Guards (_, level, _)) = level
| level_of_type_enc (Tags (_, level, _)) = level
-fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
- | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
- | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
+fun uniformity_of_type_enc (Simple_Types _) = Uniform
+ | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
+ | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
-fun is_type_level_virtually_sound level =
- level = All_Types orelse level = Noninf_Nonmono_Types
-val is_type_enc_virtually_sound =
- is_type_level_virtually_sound o level_of_type_enc
+fun is_type_level_quasi_sound All_Types = true
+ | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
+ | is_type_level_quasi_sound _ = false
+val is_type_enc_quasi_sound =
+ is_type_level_quasi_sound o level_of_type_enc
fun is_type_level_fairly_sound level =
- is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
+ is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
-fun choose_format formats (Simple_Types (order, level)) =
- (case find_first is_format_thf formats of
- SOME format => (format, Simple_Types (order, level))
- | NONE =>
- if member (op =) formats TFF then
- (TFF, Simple_Types (First_Order, level))
- else
- choose_format formats
- (Guards (Mangled_Monomorphic, level, Heavyweight)))
- | choose_format formats type_enc =
- (case hd formats of
- CNF_UEQ =>
- (CNF_UEQ, case type_enc of
- Guards stuff =>
- (if is_type_enc_fairly_sound type_enc then Tags else Guards)
- stuff
- | _ => type_enc)
- | format => (format, type_enc))
+fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
+ | is_type_level_monotonicity_based Fin_Nonmono_Types = true
+ | is_type_level_monotonicity_based _ = false
+
+fun adjust_type_enc (THF _) type_enc = type_enc
+ | adjust_type_enc TFF (Simple_Types (_, level)) =
+ Simple_Types (First_Order, level)
+ | adjust_type_enc format (Simple_Types (_, level)) =
+ adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
+ | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
+ (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
+ | adjust_type_enc _ type_enc = type_enc
fun lift_lambdas ctxt type_enc =
map (close_form o Envir.eta_contract) #> rpair ctxt
@@ -659,12 +657,10 @@
fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
-val type_instance = Sign.typ_instance o Proof_Context.theory_of
-
fun insert_type ctxt get_T x xs =
let val T = get_T x in
- if exists (curry (type_instance ctxt) T o get_T) xs then xs
- else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
+ if exists (type_instance ctxt T o get_T) xs then xs
+ else x :: filter_out (type_generalization ctxt T o get_T) xs
end
(* The Booleans indicate whether all type arguments should be kept. *)
@@ -677,7 +673,7 @@
false (* since TFF doesn't support overloading *)
| should_drop_arg_type_args type_enc =
level_of_type_enc type_enc = All_Types andalso
- heaviness_of_type_enc type_enc = Heavyweight
+ uniformity_of_type_enc type_enc = Uniform
fun type_arg_policy type_enc s =
if s = type_tag_name then
@@ -686,19 +682,19 @@
else
Explicit_Type_Args) false
else case type_enc of
- Tags (_, All_Types, Heavyweight) => No_Type_Args
+ Tags (_, All_Types, Uniform) => No_Type_Args
| _ =>
- if level_of_type_enc type_enc = No_Types orelse
- s = @{const_name HOL.eq} orelse
- (s = app_op_name andalso
- level_of_type_enc type_enc = Const_Arg_Types) then
- No_Type_Args
- else
- should_drop_arg_type_args type_enc
- |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
- Mangled_Type_Args
- else
- Explicit_Type_Args)
+ let val level = level_of_type_enc type_enc in
+ if level = No_Types orelse s = @{const_name HOL.eq} orelse
+ (s = app_op_name andalso level = Const_Arg_Types) then
+ No_Type_Args
+ else
+ should_drop_arg_type_args type_enc
+ |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+ Mangled_Type_Args
+ else
+ Explicit_Type_Args)
+ end
(* Make literals for sorted type variables. *)
fun generic_add_sorts_on_type (_, []) = I
@@ -784,6 +780,9 @@
^ ")"
| generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
+fun mangled_type format type_enc =
+ generic_mangled_type_name fst o ho_term_from_typ format type_enc
+
val bool_atype = AType (`I tptp_bool_type)
fun make_simple_type s =
@@ -894,26 +893,35 @@
iterm_from_term thy bs (Envir.eta_contract t)
|>> (introduce_proxies type_enc #> AAtom)
||> union (op =) atomic_types
- fun do_quant bs q s T t' =
- let val s = singleton (Name.variant_list (map fst bs)) s in
- do_formula ((s, T) :: bs) t'
- #>> mk_aquant q [(`make_bound_var s, SOME T)]
+ fun do_quant bs q pos s T t' =
+ let
+ val s = singleton (Name.variant_list (map fst bs)) s
+ val universal = Option.map (q = AExists ? not) pos
+ val name =
+ s |> `(case universal of
+ SOME true => make_all_bound_var
+ | SOME false => make_exist_bound_var
+ | NONE => make_bound_var)
+ in
+ do_formula ((s, (name, T)) :: bs) pos t'
+ #>> mk_aquant q [(name, SOME T)]
end
- and do_conn bs c t1 t2 =
- do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
- and do_formula bs t =
+ and do_conn bs c pos1 t1 pos2 t2 =
+ do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
+ and do_formula bs pos t =
case t of
- @{const Trueprop} $ t1 => do_formula bs t1
- | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
+ @{const Trueprop} $ t1 => do_formula bs pos t1
+ | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
| Const (@{const_name All}, _) $ Abs (s, T, t') =>
- do_quant bs AForall s T t'
+ do_quant bs AForall pos s T t'
| Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
- do_quant bs AExists s T t'
- | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ do_quant bs AExists pos s T t'
+ | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
+ | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
+ | @{const HOL.implies} $ t1 $ t2 =>
+ do_conn bs AImplies (Option.map not pos) t1 pos t2
| Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
- if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
+ if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
| _ => do_term bs t
in do_formula [] end
@@ -1036,7 +1044,7 @@
fun make_formula thy type_enc eq_as_iff name loc kind t =
let
val (iformula, atomic_types) =
- iformula_from_prop thy type_enc eq_as_iff t []
+ iformula_from_prop thy type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
in
{name = name, locality = loc, kind = kind, iformula = iformula,
atomic_types = atomic_types}
@@ -1064,32 +1072,60 @@
(** Finite and infinite type inference **)
-fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
- | deep_freeze_atyp T = T
-val deep_freeze_type = map_atyps deep_freeze_atyp
+type monotonicity_info =
+ {maybe_finite_Ts : typ list,
+ surely_finite_Ts : typ list,
+ maybe_infinite_Ts : typ list,
+ surely_infinite_Ts : typ list,
+ maybe_nonmono_Ts : typ list}
+
+(* These types witness that the type classes they belong to allow infinite
+ models and hence that any types with these type classes is monotonic. *)
+val known_infinite_types =
+ [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
+
+fun is_type_surely_infinite' ctxt soundness cached_Ts T =
+ (* Unlike virtually any other polymorphic fact whose type variables can be
+ instantiated by a known infinite type, extensionality actually encodes a
+ cardinality constraints. *)
+ soundness <> Sound andalso
+ is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Löwenheim-Skolem). *)
-fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
- exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
- | should_encode_type _ _ All_Types _ = true
- | should_encode_type ctxt _ Fin_Nonmono_Types T =
- is_type_surely_finite ctxt false T
+fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
+ | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
+ maybe_nonmono_Ts, ...}
+ (Noninf_Nonmono_Types soundness) T =
+ exists (type_instance ctxt T orf type_generalization ctxt T)
+ maybe_nonmono_Ts andalso
+ not (exists (type_instance ctxt T) surely_infinite_Ts orelse
+ (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
+ is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
+ | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
+ maybe_nonmono_Ts, ...}
+ Fin_Nonmono_Types T =
+ exists (type_instance ctxt T orf type_generalization ctxt T)
+ maybe_nonmono_Ts andalso
+ (exists (type_instance ctxt T) surely_finite_Ts orelse
+ (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
+ is_type_surely_finite ctxt T))
| should_encode_type _ _ _ _ = false
-fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
- should_predicate_on_var T =
- (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
- should_encode_type ctxt nonmono_Ts level T
- | should_predicate_on_type _ _ _ _ _ = false
+fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
+ T =
+ (uniformity = Uniform orelse should_guard_var ()) andalso
+ should_encode_type ctxt mono level T
+ | should_guard_type _ _ _ _ _ = false
-fun is_var_or_bound_var (IConst ((s, _), _, _)) =
- String.isPrefix bound_var_prefix s
- | is_var_or_bound_var (IVar _) = true
- | is_var_or_bound_var _ = false
+fun is_maybe_universal_var (IConst ((s, _), _, _)) =
+ String.isPrefix bound_var_prefix s orelse
+ String.isPrefix all_bound_var_prefix s
+ | is_maybe_universal_var (IVar _) = true
+ | is_maybe_universal_var _ = false
datatype tag_site =
Top_Level of bool option |
@@ -1097,26 +1133,18 @@
Elsewhere
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
- | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
- u T =
- (case heaviness of
- Heavyweight => should_encode_type ctxt nonmono_Ts level T
- | Lightweight =>
- case (site, is_var_or_bound_var u) of
- (Eq_Arg pos, true) =>
- (* The first disjunct prevents a subtle soundness issue explained in
- Blanchette's Ph.D. thesis. See also
- "formula_lines_for_lightweight_tags_sym_decl". *)
- (pos <> SOME false andalso poly = Polymorphic andalso
- level <> All_Types andalso heaviness = Lightweight andalso
- exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
- should_encode_type ctxt nonmono_Ts level T
+ | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
+ (case uniformity of
+ Uniform => should_encode_type ctxt mono level T
+ | Nonuniform =>
+ case (site, is_maybe_universal_var u) of
+ (Eq_Arg _, true) => should_encode_type ctxt mono level T
| _ => false)
| should_tag_with_type _ _ _ _ _ _ = false
-fun homogenized_type ctxt nonmono_Ts level =
+fun homogenized_type ctxt mono level =
let
- val should_encode = should_encode_type ctxt nonmono_Ts level
+ val should_encode = should_encode_type ctxt mono level
fun homo 0 T = if should_encode T then T else homo_infinite_type
| homo ary (Type (@{type_name fun}, [T1, T2])) =
homo 0 T1 --> homo (ary - 1) T2
@@ -1133,13 +1161,13 @@
fun consider_var_arity const_T var_T max_ary =
let
fun iter ary T =
- if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
- type_instance ctxt (T, var_T) then
+ if ary = max_ary orelse type_instance ctxt var_T T orelse
+ type_instance ctxt T var_T then
ary
else
iter (ary + 1) (range_type T)
in iter 0 const_T end
- fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
+ fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
if explicit_apply = NONE andalso
(can dest_funT T orelse T = @{typ bool}) then
let
@@ -1163,8 +1191,9 @@
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, _), T, _) =>
- if String.isPrefix bound_var_prefix s then
- add_var_or_bound_var T accum
+ if String.isPrefix bound_var_prefix s orelse
+ String.isPrefix all_bound_var_prefix s then
+ add_universal_var T accum
else
let val ary = length args in
((bool_vars, fun_var_Ts),
@@ -1202,8 +1231,8 @@
sym_tab
end)
end
- | IVar (_, T) => add_var_or_bound_var T accum
- | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm
+ | IVar (_, T) => add_universal_var T accum
+ | IAbs ((_, T), tm) => accum |> add_universal_var T |> add false tm
| _ => accum)
|> fold (add false) args
end
@@ -1238,7 +1267,7 @@
let val s = s |> unmangled_const_name |> invert_const in
if s = predicator_name then 1
else if s = app_op_name then 2
- else if s = type_pred_name then 1
+ else if s = type_guard_name then 1
else 0
end
| NONE => 0
@@ -1386,17 +1415,34 @@
(("If", true), @{thms if_True if_False True_or_False})]
|> map (apsnd (map zero_var_indexes))
+fun fo_literal_from_type_literal (TyLitVar (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+ | fo_literal_from_type_literal (TyLitFree (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+
+fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
+
+fun bound_tvars type_enc Ts =
+ mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
+ (type_literals_for_types type_enc add_sorts_on_tvar Ts))
+
+fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
+ (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
+ else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
+ |> bound_tvars type_enc atomic_Ts
+ |> close_formula_universally
+
val type_tag = `make_fixed_const type_tag_name
-fun type_tag_idempotence_fact () =
+fun type_tag_idempotence_fact type_enc =
let
fun var s = ATerm (`I s, [])
- fun tag tm = ATerm (type_tag, [var "T", tm])
- val tagged_a = tag (var "A")
+ fun tag tm = ATerm (type_tag, [var "A", tm])
+ val tagged_var = tag (var "X")
in
Formula (type_tag_idempotence_helper_name, Axiom,
- AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
- |> close_formula_universally, isabelle_info simpN, NONE)
+ eq_formula type_enc [] false (tag tagged_var) tagged_var,
+ isabelle_info simpN, NONE)
end
fun should_specialize_helper type_enc t =
@@ -1533,37 +1579,36 @@
(conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
end
-fun fo_literal_from_type_literal (TyLitVar (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
- | fo_literal_from_type_literal (TyLitFree (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
+val type_guard = `make_fixed_const type_guard_name
-fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-val type_pred = `make_fixed_const type_pred_name
-
-fun type_pred_iterm ctxt format type_enc T tm =
- IApp (IConst (type_pred, T --> @{typ bool}, [T])
+fun type_guard_iterm ctxt format type_enc T tm =
+ IApp (IConst (type_guard, T --> @{typ bool}, [T])
|> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
| is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
| is_var_positively_naked_in_term _ _ _ _ = true
-fun should_predicate_on_var_in_formula pos phi (SOME true) name =
+
+fun should_guard_var_in_formula pos phi (SOME true) name =
formula_fold pos (is_var_positively_naked_in_term name) phi false
- | should_predicate_on_var_in_formula _ _ _ _ = true
+ | should_guard_var_in_formula _ _ _ _ = true
+
+fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
+ | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
+ should_encode_type ctxt mono level T
+ | should_generate_tag_bound_decl _ _ _ _ _ = false
fun mk_aterm format type_enc name T_args args =
ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
-fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
+fun tag_with_type ctxt format mono type_enc pos T tm =
IConst (type_tag, T --> T, [T])
|> enforce_type_arg_policy_in_iterm ctxt format type_enc
- |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+ |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
| _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
+and ho_term_from_iterm ctxt format mono type_enc =
let
fun aux site u =
let
@@ -1589,28 +1634,33 @@
| IApp _ => raise Fail "impossible \"IApp\""
val T = ityp_of u
in
- t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
- tag_with_type ctxt format nonmono_Ts type_enc pos T
+ t |> (if should_tag_with_type ctxt mono type_enc site u T then
+ tag_with_type ctxt format mono type_enc pos T
else
I)
end
in aux end
-and formula_from_iformula ctxt format nonmono_Ts type_enc
- should_predicate_on_var =
+and formula_from_iformula ctxt format mono type_enc should_guard_var =
let
- val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level
+ val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
val do_bound_type =
case type_enc of
Simple_Types (_, level) =>
- homogenized_type ctxt nonmono_Ts level 0
+ homogenized_type ctxt mono level 0
#> ho_type_from_typ format type_enc false 0 #> SOME
| _ => K NONE
fun do_out_of_bound_type pos phi universal (name, T) =
- if should_predicate_on_type ctxt nonmono_Ts type_enc
- (fn () => should_predicate_on_var pos phi universal name) T then
+ if should_guard_type ctxt mono type_enc
+ (fn () => should_guard_var pos phi universal name) T then
IVar (name, T)
- |> type_pred_iterm ctxt format type_enc T
+ |> type_guard_iterm ctxt format type_enc T
|> do_term pos |> AAtom |> SOME
+ else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
+ let
+ val var = ATerm (name, [])
+ val tagged_var =
+ ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
+ in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
else
NONE
fun do_formula pos (AQuant (q, xs, phi)) =
@@ -1632,20 +1682,16 @@
| do_formula pos (AAtom tm) = AAtom (do_term pos tm)
in do_formula end
-fun bound_tvars type_enc Ts =
- mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
- (type_literals_for_types type_enc add_sorts_on_tvar Ts))
-
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
-fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
- type_enc (j, {name, locality, kind, iformula, atomic_types}) =
+fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
+ (j, {name, locality, kind, iformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
iformula
|> close_iformula_universally
- |> formula_from_iformula ctxt format nonmono_Ts type_enc
- should_predicate_on_var_in_formula
+ |> formula_from_iformula ctxt format mono type_enc
+ should_guard_var_in_formula
(if pos then SOME true else NONE)
|> bound_tvars type_enc atomic_types
|> close_formula_universally,
@@ -1680,11 +1726,11 @@
(fo_literal_from_arity_literal concl_lits))
|> close_formula_universally, isabelle_info introN, NONE)
-fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
+fun formula_line_for_conjecture ctxt format mono type_enc
({name, kind, iformula, atomic_types, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
- formula_from_iformula ctxt format nonmono_Ts type_enc
- should_predicate_on_var_in_formula (SOME false)
+ formula_from_iformula ctxt format mono type_enc
+ should_guard_var_in_formula (SOME false)
(close_iformula_universally iformula)
|> bound_tvars type_enc atomic_types
|> close_formula_universally, NONE, NONE)
@@ -1705,11 +1751,12 @@
(** Symbol declarations **)
fun should_declare_sym type_enc pred_sym s =
- is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
(case type_enc of
- Simple_Types _ => true
- | Tags (_, _, Lightweight) => true
- | _ => not pred_sym)
+ Guards _ => not pred_sym
+ | _ => true) andalso
+ is_tptp_user_symbol s andalso
+ forall (fn prefix => not (String.isPrefix prefix s))
+ [bound_var_prefix, all_bound_var_prefix, exist_bound_var_prefix]
fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
(conjs, facts) =
@@ -1762,37 +1809,103 @@
| _ => fold add_undefined_const (var_types ())))
end
+(* We add "bool" in case the helper "True_or_False" is included later. *)
+val default_mono =
+ {maybe_finite_Ts = [@{typ bool}],
+ surely_finite_Ts = [@{typ bool}],
+ maybe_infinite_Ts = known_infinite_types,
+ surely_infinite_Ts = known_infinite_types,
+ maybe_nonmono_Ts = [@{typ bool}]}
+
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
-fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
- | add_iterm_nonmonotonic_types ctxt level sound locality _
- (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
- (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
- (case level of
- Noninf_Nonmono_Types =>
- not (is_locality_global locality) orelse
- not (is_type_surely_infinite ctxt sound T)
- | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
- | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
- | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level sound
- ({kind, locality, iformula, ...} : translated_formula) =
+fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
+ | add_iterm_mononotonicity_info ctxt level _
+ (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
+ (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
+ surely_infinite_Ts, maybe_nonmono_Ts}) =
+ if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
+ case level of
+ Noninf_Nonmono_Types soundness =>
+ if exists (type_instance ctxt T) surely_infinite_Ts orelse
+ member (type_aconv ctxt) maybe_finite_Ts T then
+ mono
+ else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts
+ T then
+ {maybe_finite_Ts = maybe_finite_Ts,
+ surely_finite_Ts = surely_finite_Ts,
+ maybe_infinite_Ts = maybe_infinite_Ts,
+ surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
+ maybe_nonmono_Ts = maybe_nonmono_Ts}
+ else
+ {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
+ surely_finite_Ts = surely_finite_Ts,
+ maybe_infinite_Ts = maybe_infinite_Ts,
+ surely_infinite_Ts = surely_infinite_Ts,
+ maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
+ | Fin_Nonmono_Types =>
+ if exists (type_instance ctxt T) surely_finite_Ts orelse
+ member (type_aconv ctxt) maybe_infinite_Ts T then
+ mono
+ else if is_type_surely_finite ctxt T then
+ {maybe_finite_Ts = maybe_finite_Ts,
+ surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
+ maybe_infinite_Ts = maybe_infinite_Ts,
+ surely_infinite_Ts = surely_infinite_Ts,
+ maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
+ else
+ {maybe_finite_Ts = maybe_finite_Ts,
+ surely_finite_Ts = surely_finite_Ts,
+ maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
+ surely_infinite_Ts = surely_infinite_Ts,
+ maybe_nonmono_Ts = maybe_nonmono_Ts}
+ | _ => mono
+ else
+ mono
+ | add_iterm_mononotonicity_info _ _ _ _ mono = mono
+fun add_fact_mononotonicity_info ctxt level
+ ({kind, iformula, ...} : translated_formula) =
formula_fold (SOME (kind <> Conjecture))
- (add_iterm_nonmonotonic_types ctxt level sound locality)
- iformula
-fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
+ (add_iterm_mononotonicity_info ctxt level) iformula
+fun mononotonicity_info_for_facts ctxt type_enc facts =
let val level = level_of_type_enc type_enc in
- if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
- [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
- (* We must add "bool" in case the helper "True_or_False" is added
- later. In addition, several places in the code rely on the list of
- nonmonotonic types not being empty. (FIXME?) *)
- |> insert_type ctxt I @{typ bool}
- else
- []
+ default_mono
+ |> is_type_level_monotonicity_based level
+ ? fold (add_fact_mononotonicity_info ctxt level) facts
end
-fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
+fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
+ Formula (guards_sym_formula_prefix ^
+ ascii_of (mangled_type format type_enc T),
+ Axiom,
+ IConst (`make_bound_var "X", T, [])
+ |> type_guard_iterm ctxt format type_enc T
+ |> AAtom
+ |> formula_from_iformula ctxt format mono type_enc
+ (K (K (K (K true)))) (SOME true)
+ |> bound_tvars type_enc (atyps_of T)
+ |> close_formula_universally,
+ isabelle_info introN, NONE)
+
+fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
+ let val x_var = ATerm (`make_bound_var "X", []) in
+ Formula (tags_sym_formula_prefix ^
+ ascii_of (mangled_type format type_enc T),
+ Axiom,
+ eq_formula type_enc (atyps_of T) false
+ (tag_with_type ctxt format mono type_enc NONE T x_var)
+ x_var,
+ isabelle_info simpN, NONE)
+ end
+
+fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
+ case type_enc of
+ Simple_Types _ => []
+ | Guards _ =>
+ map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
+ | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
+
+fun decl_line_for_sym ctxt format mono type_enc s
(s', T_args, T, pred_sym, ary, _) =
let
val (T_arg_Ts, level) =
@@ -1801,12 +1914,12 @@
| _ => (replicate (length T_args) homo_infinite_type, No_Types)
in
Decl (sym_decl_prefix ^ s, (s, s'),
- (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
+ (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
|> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
end
-fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
+fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
+ j (s', T_args, T, _, ary, in_conj) =
let
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1819,8 +1932,8 @@
bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
fun should_keep_arg_type T =
- sym_needs_arg_types orelse
- not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
+ sym_needs_arg_types andalso
+ should_guard_type ctxt mono type_enc (K true) T
val bound_Ts =
arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
in
@@ -1828,9 +1941,9 @@
(if n > 1 then "_" ^ string_of_int j else ""), kind,
IConst ((s, s'), T, T_args)
|> fold (curry (IApp o swap)) bounds
- |> type_pred_iterm ctxt format type_enc res_T
+ |> type_guard_iterm ctxt format type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc
+ |> formula_from_iformula ctxt format mono type_enc
(K (K (K (K true)))) (SOME true)
|> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally
@@ -1838,12 +1951,11 @@
isabelle_info introN, NONE)
end
-fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
- poly_nonmono_Ts type_enc n s
- (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
+ type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val ident_base =
- lightweight_tags_sym_formula_prefix ^ s ^
+ tags_sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else "")
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1853,25 +1965,14 @@
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
val cst = mk_aterm format type_enc (s, s') T_args
- val atomic_Ts = atyps_of T
- fun eq tms =
- (if pred_sym then AConn (AIff, map AAtom tms)
- else AAtom (ATerm (`I tptp_equal, tms)))
- |> bound_tvars type_enc atomic_Ts
- |> close_formula_universally
- |> maybe_negate
- (* See also "should_tag_with_type". *)
- fun should_encode T =
- should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
- (case type_enc of
- Tags (Polymorphic, level, Lightweight) =>
- level <> All_Types andalso Monomorph.typ_has_tvars T
- | _ => false)
- val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
+ val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
+ val should_encode =
+ should_encode_type ctxt mono (level_of_type_enc type_enc)
+ val tag_with = tag_with_type ctxt format mono type_enc NONE
val add_formula_for_res =
if should_encode res_T then
cons (Formula (ident_base ^ "_res", kind,
- eq [tag_with res_T (cst bounds), cst bounds],
+ eq (tag_with res_T (cst bounds)) (cst bounds),
isabelle_info simpN, NONE))
else
I
@@ -1881,8 +1982,8 @@
case chop k bounds of
(bounds1, bound :: bounds2) =>
cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
- eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
- cst bounds],
+ eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
+ (cst bounds),
isabelle_info simpN, NONE))
| _ => raise Fail "expected nonempty tail"
else
@@ -1895,19 +1996,19 @@
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
-fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_enc (s, decls) =
+fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
+ (s, decls) =
case type_enc of
Simple_Types _ =>
- decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
- | Guards _ =>
+ decls |> map (decl_line_for_sym ctxt format mono type_enc s)
+ | Guards (_, level, _) =>
let
val decls =
case decls of
decl :: (decls' as _ :: _) =>
let val T = result_type_of_decl decl in
- if forall (curry (type_instance ctxt o swap) T
- o result_type_of_decl) decls' then
+ if forall (type_generalization ctxt T o result_type_of_decl)
+ decls' then
[decl]
else
decls
@@ -1915,34 +2016,47 @@
| _ => decls
val n = length decls
val decls =
- decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
- (K true)
+ decls |> filter (should_encode_type ctxt mono level
o result_type_of_decl)
in
(0 upto length decls - 1, decls)
- |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
- nonmono_Ts poly_nonmono_Ts type_enc n s)
+ |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
+ type_enc n s)
end
- | Tags (_, _, heaviness) =>
- (case heaviness of
- Heavyweight => []
- | Lightweight =>
+ | Tags (_, _, uniformity) =>
+ (case uniformity of
+ Uniform => []
+ | Nonuniform =>
let val n = length decls in
(0 upto n - 1 ~~ decls)
- |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
- conj_sym_kind poly_nonmono_Ts type_enc n s)
+ |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
+ conj_sym_kind mono type_enc n s)
end)
-fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_enc sym_decl_tab =
- sym_decl_tab |> Symtab.dest |> sort_wrt fst |> rpair []
- |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
- nonmono_Ts poly_nonmono_Ts type_enc)
+fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
+ sym_decl_tab =
+ let
+ val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
+ val mono_Ts =
+ if polymorphism_of_type_enc type_enc = Polymorphic then
+ syms |> maps (map result_type_of_decl o snd)
+ |> filter_out (should_encode_type ctxt mono
+ (level_of_type_enc type_enc))
+ |> rpair [] |-> fold (insert_type ctxt I)
+ else
+ []
+ val mono_lines =
+ problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
+ val decl_lines =
+ fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
+ mono type_enc)
+ syms []
+ in mono_lines @ decl_lines end
-fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
+fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
poly <> Mangled_Monomorphic andalso
- ((level = All_Types andalso heaviness = Lightweight) orelse
- level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
+ ((level = All_Types andalso uniformity = Nonuniform) orelse
+ is_type_level_monotonicity_based level)
| needs_type_tag_idempotence _ = false
fun offset_of_heading_in_problem _ [] j = j
@@ -1961,10 +2075,10 @@
val explicit_apply = NONE (* for experiments *)
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
+fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
+ lambda_trans readable_names preproc hyp_ts concl_t facts =
let
- val (format, type_enc) = choose_format [format] type_enc
+ val type_enc = type_enc |> adjust_type_enc format
val lambda_trans =
if lambda_trans = smartN then
if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
@@ -1996,8 +2110,7 @@
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
- val nonmono_Ts =
- conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
+ val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
val repair = repair_fact ctxt format type_enc sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map repair)
val repaired_sym_tab =
@@ -2005,23 +2118,17 @@
val helpers =
repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map repair
- val poly_nonmono_Ts =
- if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] (* FIXME? *) orelse
- polymorphism_of_type_enc type_enc <> Polymorphic then
- nonmono_Ts
- else
- [tvar_a]
val sym_decl_lines =
(conjs, helpers @ facts)
|> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
- |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
- poly_nonmono_Ts type_enc
+ |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
+ type_enc
val helper_lines =
0 upto length helpers - 1 ~~ helpers
- |> map (formula_line_for_fact ctxt format helper_prefix I false true
- poly_nonmono_Ts type_enc)
+ |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
+ type_enc)
|> (if needs_type_tag_idempotence type_enc then
- cons (type_tag_idempotence_fact ())
+ cons (type_tag_idempotence_fact type_enc)
else
I)
(* Reordering these might confuse the proof reconstruction code or the SPASS
@@ -2030,15 +2137,14 @@
[(explicit_declsN, sym_decl_lines),
(factsN,
map (formula_line_for_fact ctxt format fact_prefix ascii_of
- (not exporter) (not exporter) nonmono_Ts
+ (not exporter) (not exporter) mono
type_enc)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
(helpersN, helper_lines),
(conjsN,
- map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
- conjs),
+ map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
(free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
val problem =
problem
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Aug 23 17:12:54 2011 +0200
@@ -15,14 +15,17 @@
val maybe_quote : string -> string
val string_from_ext_time : bool * Time.time -> string
val string_from_time : Time.time -> string
+ val type_instance : Proof.context -> typ -> typ -> bool
+ val type_generalization : Proof.context -> typ -> typ -> bool
+ val type_aconv : Proof.context -> typ * typ -> bool
val varify_type : Proof.context -> typ -> typ
val instantiate_type : theory -> typ -> typ -> typ -> typ
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
val typ_of_dtyp :
Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
-> typ
- val is_type_surely_finite : Proof.context -> bool -> typ -> bool
- val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
+ val is_type_surely_finite : Proof.context -> typ -> bool
+ val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool
val s_not : term -> term
val s_conj : term * term -> term
val s_disj : term * term -> term
@@ -111,6 +114,12 @@
val string_from_time = string_from_ext_time o pair false
+fun type_instance ctxt T T' =
+ Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
+fun type_generalization ctxt T T' = type_instance ctxt T' T
+fun type_aconv ctxt (T, T') =
+ type_instance ctxt T T' andalso type_instance ctxt T' T
+
fun varify_type ctxt T =
Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
|> snd |> the_single |> dest_Const |> snd
@@ -149,65 +158,70 @@
0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
cardinality 2 or more. The specified default cardinality is returned if the
cardinality of the type can't be determined. *)
-fun tiny_card_of_type ctxt sound default_card T =
+fun tiny_card_of_type ctxt inst_tvars assigns default_card T =
let
val thy = Proof_Context.theory_of ctxt
val max = 2 (* 1 would be too small for the "fun" case *)
+ val type_cmp =
+ if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt
fun aux slack avoid T =
if member (op =) avoid T then
0
- else case T of
- Type (@{type_name fun}, [T1, T2]) =>
- (case (aux slack avoid T1, aux slack avoid T2) of
- (k, 1) => if slack andalso k = 0 then 0 else 1
- | (0, _) => 0
- | (_, 0) => 0
- | (k1, k2) =>
- if k1 >= max orelse k2 >= max then max
- else Int.min (max, Integer.pow k2 k1))
- | @{typ prop} => 2
- | @{typ bool} => 2 (* optimization *)
- | @{typ nat} => 0 (* optimization *)
- | Type ("Int.int", []) => 0 (* optimization *)
- | Type (s, _) =>
- (case datatype_constrs thy T of
- constrs as _ :: _ =>
- let
- val constr_cards =
- map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
- o snd) constrs
- in
- if exists (curry (op =) 0) constr_cards then 0
- else Int.min (max, Integer.sum constr_cards)
- end
- | [] =>
- case Typedef.get_info ctxt s of
- ({abs_type, rep_type, ...}, _) :: _ =>
- (* We cheat here by assuming that typedef types are infinite if
- their underlying type is infinite. This is unsound in general
- but it's hard to think of a realistic example where this would
- not be the case. We are also slack with representation types:
- If a representation type has the form "sigma => tau", we
- consider it enough to check "sigma" for infiniteness. (Look
- for "slack" in this function.) *)
- (case varify_and_instantiate_type ctxt
- (Logic.varifyT_global abs_type) T
- (Logic.varifyT_global rep_type)
- |> aux true avoid of
- 0 => if sound then default_card else 0
- | 1 => 1
- | _ => default_card)
- | [] => default_card)
- (* Very slightly unsound: Type variables are assumed not to be
- constrained to cardinality 1. (In practice, the user would most
- likely have used "unit" directly anyway.) *)
- | TFree _ =>
- if default_card = 1 andalso not sound then 2 else default_card
- | TVar _ => default_card
+ else case AList.lookup type_cmp assigns T of
+ SOME k => k
+ | NONE =>
+ case T of
+ Type (@{type_name fun}, [T1, T2]) =>
+ (case (aux slack avoid T1, aux slack avoid T2) of
+ (k, 1) => if slack andalso k = 0 then 0 else 1
+ | (0, _) => 0
+ | (_, 0) => 0
+ | (k1, k2) =>
+ if k1 >= max orelse k2 >= max then max
+ else Int.min (max, Integer.pow k2 k1))
+ | @{typ prop} => 2
+ | @{typ bool} => 2 (* optimization *)
+ | @{typ nat} => 0 (* optimization *)
+ | Type ("Int.int", []) => 0 (* optimization *)
+ | Type (s, _) =>
+ (case datatype_constrs thy T of
+ constrs as _ :: _ =>
+ let
+ val constr_cards =
+ map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
+ o snd) constrs
+ in
+ if exists (curry (op =) 0) constr_cards then 0
+ else Int.min (max, Integer.sum constr_cards)
+ end
+ | [] =>
+ case Typedef.get_info ctxt s of
+ ({abs_type, rep_type, ...}, _) :: _ =>
+ (* We cheat here by assuming that typedef types are infinite if
+ their underlying type is infinite. This is unsound in general
+ but it's hard to think of a realistic example where this would
+ not be the case. We are also slack with representation types:
+ If a representation type has the form "sigma => tau", we
+ consider it enough to check "sigma" for infiniteness. (Look
+ for "slack" in this function.) *)
+ (case varify_and_instantiate_type ctxt
+ (Logic.varifyT_global abs_type) T
+ (Logic.varifyT_global rep_type)
+ |> aux true avoid of
+ 0 => 0
+ | 1 => 1
+ | _ => default_card)
+ | [] => default_card)
+ (* Very slightly unsound: Type variables are assumed not to be
+ constrained to cardinality 1. (In practice, the user would most
+ likely have used "unit" directly anyway.) *)
+ | TFree _ => if default_card = 1 then 2 else default_card
+ | TVar _ => default_card
in Int.min (max, aux false [] T) end
-fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
-fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0
+fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T =
+ tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0
(* Simple simplifications to ensure that sort annotations don't leave a trail of
spurious "True"s. *)
--- a/src/HOL/Tools/ATP/scripts/spass Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/spass Tue Aug 23 17:12:54 2011 +0200
@@ -11,6 +11,7 @@
"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
| sed 's/description({$/description({*/' \
+ | sed 's/set_ClauseFormulaRelation()\.//' \
> $name.cnf.dfg
rm -f $name.fof.dfg
cat $name.cnf.dfg
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Aug 23 17:12:54 2011 +0200
@@ -39,8 +39,8 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_enc = "mangled_tags_heavy"
-val full_type_enc = "poly_guards_heavy_query"
+val really_full_type_enc = "mangled_tags_uniform"
+val full_type_enc = "poly_guards_uniform_query"
val partial_type_enc = "poly_args"
val no_type_enc = "erased"
@@ -78,7 +78,10 @@
let val thy = Proof_Context.theory_of ctxt in
case hol_clause_from_metis ctxt sym_tab old_skolems mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
- t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
+ let
+ val ct = cterm_of thy t
+ val cT = ctyp_of_term ct
+ in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
@@ -86,12 +89,19 @@
end
|> Meson.make_meta_clause
-val clause_params =
+fun clause_params type_enc =
{ordering = Metis_KnuthBendixOrder.default,
- orderLiterals = Metis_Clause.UnsignedLiteralOrder,
+ orderLiterals =
+ (* Type axioms seem to benefit from the positive literal order, but for
+ compatibility we keep the unsigned order for Metis's default
+ "partial_types" mode. *)
+ if is_type_enc_fairly_sound type_enc then
+ Metis_Clause.PositiveLiteralOrder
+ else
+ Metis_Clause.UnsignedLiteralOrder,
orderTerms = true}
-val active_params =
- {clause = clause_params,
+fun active_params type_enc =
+ {clause = clause_params type_enc,
prefactor = #prefactor Metis_Active.default,
postfactor = #postfactor Metis_Active.default}
val waiting_params =
@@ -99,7 +109,8 @@
variablesWeight = 0.0,
literalsWeight = 0.0,
models = []}
-val resolution_params = {active = active_params, waiting = waiting_params}
+fun resolution_params type_enc =
+ {active = active_params type_enc, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
@@ -117,6 +128,8 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
+ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
+ val type_enc = type_enc_from_string Unsound type_enc
val (sym_tab, axioms, old_skolems) =
prepare_metis_problem ctxt type_enc cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
@@ -126,13 +139,13 @@
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
val thms = axioms |> map fst
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
- val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
in
case filter (fn t => prop_of t aconv @{prop False}) cls of
false_th :: _ => [false_th RS @{thm FalseE}]
| [] =>
- case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
+ case Metis_Resolution.new (resolution_params type_enc)
+ {axioms = thms, conjecture = []}
|> Metis_Resolution.loop of
Metis_Resolution.Contradiction mth =>
let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Aug 23 17:12:54 2011 +0200
@@ -9,6 +9,8 @@
signature METIS_TRANSLATE =
sig
+ type type_enc = ATP_Translate.type_enc
+
datatype isa_thm =
Isa_Reflexive_or_Trivial |
Isa_Raw of thm
@@ -25,7 +27,7 @@
val metis_name_table : ((string * int) * (string * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val prepare_metis_problem :
- Proof.context -> string -> thm list -> thm list
+ Proof.context -> type_enc -> thm list -> thm list
-> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
end
@@ -141,7 +143,7 @@
|> Metis_Thm.axiom, isa)
in
if ident = type_tag_idempotence_helper_name orelse
- String.isPrefix lightweight_tags_sym_formula_prefix ident then
+ String.isPrefix tags_sym_formula_prefix ident then
Isa_Reflexive_or_Trivial |> some
else if String.isPrefix conjecture_prefix ident then
NONE
@@ -167,7 +169,6 @@
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
let
- val type_enc = type_enc_from_string type_enc
val (conj_clauses, fact_clauses) =
if polymorphism_of_type_enc type_enc = Polymorphic then
(conj_clauses, fact_clauses)
@@ -196,13 +197,13 @@
tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- no_lambdasN false false [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN
+ false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
*)
- (* "rev" is for compatibility *)
+ (* "rev" is for compatibility. *)
val axioms =
atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
|> rev
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 23 17:12:54 2011 +0200
@@ -928,8 +928,10 @@
forall (KK.is_problem_trivially_false o fst)
sound_problems then
print_n (fn () =>
- "Warning: The conjecture either trivially holds for the \
- \given scopes or lies outside Nitpick's supported \
+ "Warning: The conjecture " ^
+ (if falsify then "either trivially holds"
+ else "is either trivially unsatisfiable") ^
+ " for the given scopes or lies outside Nitpick's supported \
\fragment." ^
(if exists (not o KK.is_problem_trivially_false o fst)
unsound_problems then
--- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Aug 23 17:12:54 2011 +0200
@@ -208,6 +208,13 @@
in
list_comb (get_mapfun ctxt "fun", [arg1, arg2])
end
+(* FIXME: use type_name antiquotation if set type becomes explicit *)
+ | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) =>
+ let
+ val arg = absrep_fun (negF flag) ctxt (ty, ty')
+ in
+ get_mapfun ctxt "Set.set" $ arg
+ end
| (Type (s, tys), Type (s', tys')) =>
if s = s'
then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 23 17:12:54 2011 +0200
@@ -36,7 +36,6 @@
only : bool}
val trace : bool Config.T
- val new_monomorphizer : bool Config.T
val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
val const_names_in_fact :
@@ -70,8 +69,6 @@
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
(* experimental features *)
-val new_monomorphizer =
- Attrib.setup_config_bool @{binding sledgehammer_new_monomorphizer} (K false)
val ignore_no_atp =
Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
val instantiate_inducts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 23 17:12:54 2011 +0200
@@ -131,7 +131,7 @@
(name, value)
else if is_prover_list ctxt name andalso null value then
("provers", [name])
- else if can type_enc_from_string name andalso null value then
+ else if can (type_enc_from_string Sound) name andalso null value then
("type_enc", [name])
else
error ("Unknown parameter: " ^ quote name ^ ".")
@@ -269,7 +269,7 @@
NONE
else case lookup_string "type_enc" of
"smart" => NONE
- | s => SOME (type_enc_from_string s)
+ | s => (type_enc_from_string Sound s; SOME s)
val sound = mode = Auto_Try orelse lookup_bool "sound"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 23 17:12:54 2011 +0200
@@ -24,7 +24,7 @@
overlord: bool,
blocking: bool,
provers: string list,
- type_enc: type_enc option,
+ type_enc: string option,
sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -65,6 +65,7 @@
val measure_run_time : bool Config.T
val atp_lambda_translation : string Config.T
val atp_readable_names : bool Config.T
+ val atp_sound_modulo_infiniteness : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
val smt_weight_min_facts : int Config.T
@@ -153,7 +154,9 @@
fun is_unit_equational_atp ctxt name =
let val thy = Proof_Context.theory_of ctxt in
case try (get_atp thy) name of
- SOME {formats, ...} => member (op =) formats CNF_UEQ
+ SOME {best_slices, ...} =>
+ exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
+ (best_slices ctxt)
| NONE => false
end
@@ -290,7 +293,7 @@
overlord: bool,
blocking: bool,
provers: string list,
- type_enc: type_enc option,
+ type_enc: string option,
sound: bool,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -341,10 +344,13 @@
Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
(K smartN)
(* In addition to being easier to read, readable names are often much shorter,
- especially if types are mangled in names. For these reason, they are enabled
- by default. *)
+ especially if types are mangled in names. This makes a difference for some
+ provers (e.g., E). For these reason, short names are enabled by default. *)
val atp_readable_names =
Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
+val atp_sound_modulo_infiniteness =
+ Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
+ (K true)
val smt_triggers =
Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
@@ -498,7 +504,7 @@
are omitted. *)
fun is_dangerous_prop ctxt =
transform_elim_prop
- #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf
+ #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
is_exhaustive_finite)
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
@@ -508,11 +514,10 @@
them each time. *)
val atp_important_message_keep_quotient = 10
-fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
- (case type_enc_opt of
- SOME ts => ts
- | NONE => type_enc_from_string best_type_enc)
- |> choose_format formats
+fun choose_type_enc soundness best_type_enc format =
+ the_default best_type_enc
+ #> type_enc_from_string soundness
+ #> adjust_type_enc format
val metis_minimize_max_time = seconds 2.0
@@ -531,13 +536,13 @@
#> Config.put Monomorph.max_new_instances max_new_instances
#> Config.put Monomorph.keep_partial_instances false
-(* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
+(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
Linux appears to be the only ATP that does not honor its time limit. *)
val atp_timeout_slack = seconds 1.0
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
- conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
+ conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
({debug, verbose, overlord, type_enc, sound, max_relevant,
max_mono_iters, max_new_mono_instances, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
@@ -606,14 +611,23 @@
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, best_type_enc, extra))))
+ (best_max_relevant, format, best_type_enc,
+ extra))))
time_left =
let
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
- val (format, type_enc) =
- choose_format_and_type_enc best_type_enc formats type_enc
+ val soundness =
+ if sound then
+ if Config.get ctxt atp_sound_modulo_infiniteness then
+ Sound_Modulo_Infiniteness
+ else
+ Sound
+ else
+ Unsound
+ val type_enc =
+ type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc
val facts =
facts |> map untranslated_fact
@@ -645,8 +659,7 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc sound false
- (Config.get ctxt atp_lambda_translation)
+ type_enc false (Config.get ctxt atp_lambda_translation)
(Config.get ctxt atp_readable_names) true hyp_ts concl_t
facts
fun weights () = atp_problem_weights atp_problem
@@ -694,7 +707,7 @@
conjecture_shape facts_offset fact_names atp_proof
|> Option.map (fn facts =>
UnsoundProof
- (if is_type_enc_virtually_sound type_enc then
+ (if is_type_enc_quasi_sound type_enc then
SOME sound
else
NONE, facts |> sort string_ord))
--- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 23 16:53:05 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 23 17:12:54 2011 +0200
@@ -19,7 +19,7 @@
let
val chained_ths = [] (* a tactic has no chained ths *)
val params as {relevance_thresholds, max_relevant, slicing, ...} =
- ((if force_full_types then [("full_types", "true")] else [])
+ ((if force_full_types then [("sound", "true")] else [])
@ [("timeout", string_of_int (Time.toSeconds timeout))])
(* @ [("overlord", "true")] *)
|> Sledgehammer_Isar.default_params ctxt