--- a/NEWS Thu Jul 14 22:30:31 2011 +0200
+++ b/NEWS Thu Jul 14 22:53:43 2011 +0200
@@ -60,6 +60,9 @@
*** HOL ***
+* Classes bot and top require underlying partial order rather than preorder:
+uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
+
* Archimedian_Field.thy:
floor now is defined as parameter of a separate type class floor_ceiling.
--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Jul 14 22:30:31 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Jul 14 22:53:43 2011 +0200
@@ -980,8 +980,9 @@
\opfalse{sound}{unsound}
Specifies whether Sledgehammer should run in its fully sound mode. In that mode,
-quasi-sound type encodings are made fully sound, at the cost of some (usually
-needless) clutter.
+quasi-sound type encodings (which are the default) are made fully sound, at the
+cost of some clutter in the generated problems. This option is ignored if
+\textit{type\_enc} is explicitly set to an unsound encoding.
\end{enum}
\subsection{Relevance Filter}
--- a/src/HOL/Complete_Lattice.thy Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Thu Jul 14 22:53:43 2011 +0200
@@ -76,11 +76,11 @@
lemma Inf_binary:
"\<Sqinter>{a, b} = a \<sqinter> b"
- by (simp add: Inf_empty Inf_insert)
+ by (simp add: Inf_insert)
lemma Sup_binary:
"\<Squnion>{a, b} = a \<squnion> b"
- by (simp add: Sup_empty Sup_insert)
+ by (simp add: Sup_insert)
lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
by (auto intro: Inf_greatest dest: Inf_lower)
@@ -116,11 +116,11 @@
"x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
by (rule antisym) auto
-lemma not_less_bot[simp]: "\<not> (x \<sqsubset> \<bottom>)"
- using bot_least[of x] by (auto simp: le_less)
+lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)"
+ using bot_least [of x] by (auto simp: le_less)
-lemma not_top_less[simp]: "\<not> (\<top> \<sqsubset> x)"
- using top_greatest[of x] by (auto simp: le_less)
+lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)"
+ using top_greatest [of x] by (auto simp: le_less)
lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
using Sup_upper[of u A] by auto
@@ -392,13 +392,32 @@
lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
by (fact Inf_union_distrib)
-(*lemma (in complete_lattice) Inf_top_conv [no_atp]:
- "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"*)
+lemma (in complete_lattice) Inf_top_conv [no_atp]:
+ "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+ "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+proof -
+ show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
+ proof
+ assume "\<forall>x\<in>A. x = \<top>"
+ then have "A = {} \<or> A = {\<top>}" by auto
+ then show "\<Sqinter>A = \<top>" by auto
+ next
+ assume "\<Sqinter>A = \<top>"
+ show "\<forall>x\<in>A. x = \<top>"
+ proof (rule ccontr)
+ assume "\<not> (\<forall>x\<in>A. x = \<top>)"
+ then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
+ then obtain B where "A = insert x B" by blast
+ with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
+ qed
+ qed
+ then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
+qed
lemma Inter_UNIV_conv [simp,no_atp]:
"\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
"UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
- by blast+
+ by (fact Inf_top_conv)+
lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
by (auto intro: Inf_greatest Inf_lower)
@@ -448,23 +467,23 @@
lemma Inter_image_eq [simp]:
"\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
- by (rule sym) (fact INTER_eq_Inter_image)
+ by (rule sym) (fact INFI_def)
-lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
+lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
by (unfold INTER_def) blast
-lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
+lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
by (unfold INTER_def) blast
-lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
+lemma INT_D [elim, Pure.elim]: "b : (\<Inter>x\<in>A. B x) \<Longrightarrow> a:A \<Longrightarrow> b: B a"
by auto
-lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
+lemma INT_E [elim]: "b : (\<Inter>x\<in>A. B x) \<Longrightarrow> (b: B a \<Longrightarrow> R) \<Longrightarrow> (a~:A \<Longrightarrow> R) \<Longrightarrow> R"
-- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
by (unfold INTER_def) blast
lemma INT_cong [cong]:
- "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
+ "A = B \<Longrightarrow> (\<And>x. x:B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
by (simp add: INTER_def)
lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
@@ -473,16 +492,16 @@
lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
by blast
-lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
+lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a"
by (fact INF_leI)
-lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
+lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
by (fact le_INFI)
lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
by blast
-lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
+lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
by blast
lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
@@ -495,7 +514,7 @@
by blast
lemma INT_insert_distrib:
- "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
+ "u \<in> A \<Longrightarrow> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
by blast
lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
@@ -506,23 +525,23 @@
by blast
lemma INTER_UNIV_conv[simp]:
- "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
- "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
+ "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
+ "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
by blast+
-lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
+lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
by (auto intro: bool_induct)
lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
by blast
lemma INT_anti_mono:
- "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
+ "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
(\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
-- {* The last inclusion is POSITIVE! *}
by (blast dest: subsetD)
-lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
+lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)"
by blast
@@ -555,40 +574,40 @@
by auto
lemma UnionE [elim!]:
- "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
+ "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A \<in> X \<Longrightarrow> X \<in> C \<Longrightarrow> R) \<Longrightarrow> R"
by auto
-lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
+lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
by (iprover intro: subsetI UnionI)
-lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
+lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
by (iprover intro: subsetI elim: UnionE dest: subsetD)
lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
by blast
-lemma Union_empty [simp]: "Union({}) = {}"
+lemma Union_empty [simp]: "\<Union>{} = {}"
by blast
-lemma Union_UNIV [simp]: "Union UNIV = UNIV"
+lemma Union_UNIV [simp]: "\<Union>UNIV = UNIV"
by blast
-lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
+lemma Union_insert [simp]: "\<Union>insert a B = a \<union> \<Union>B"
by blast
-lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
+lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
by blast
lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
by blast
-lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
by blast
-lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
by blast
-lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
+lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
by blast
lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
@@ -597,7 +616,7 @@
lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
by blast
-lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
+lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
by blast
@@ -638,7 +657,7 @@
*} -- {* to avoid eta-contraction of body *}
lemma UNION_eq_Union_image:
- "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
+ "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
by (fact SUPR_def)
lemma Union_def:
@@ -650,41 +669,41 @@
by (auto simp add: UNION_eq_Union_image Union_eq)
lemma Union_image_eq [simp]:
- "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
+ "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
by (rule sym) (fact UNION_eq_Union_image)
-lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
+lemma UN_iff [simp]: "(b: (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b: B x)"
by (unfold UNION_def) blast
-lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"
+lemma UN_I [intro]: "a:A \<Longrightarrow> b: B a \<Longrightarrow> b: (\<Union>x\<in>A. B x)"
-- {* The order of the premises presupposes that @{term A} is rigid;
@{term b} may be flexible. *}
by auto
-lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"
+lemma UN_E [elim!]: "b : (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> b: B x \<Longrightarrow> R) \<Longrightarrow> R"
by (unfold UNION_def) blast
lemma UN_cong [cong]:
- "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
+ "A = B \<Longrightarrow> (\<And>x. x:B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
by (simp add: UNION_def)
lemma strong_UN_cong:
- "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
+ "A = B \<Longrightarrow> (\<And>x. x:B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
by (simp add: UNION_def simp_implies_def)
-lemma image_eq_UN: "f`A = (UN x:A. {f x})"
+lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
by blast
-lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
+lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
by (fact le_SUPI)
-lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
+lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
by (iprover intro: subsetI elim: UN_E dest: subsetD)
lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
by blast
-lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
+lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
by blast
lemma UN_empty [simp,no_atp]: "(\<Union>x\<in>{}. B x) = {}"
@@ -696,7 +715,7 @@
lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
by blast
-lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
+lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
by auto
lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
@@ -721,8 +740,8 @@
by blast
lemma UNION_empty_conv[simp]:
- "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
- "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
+ "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
+ "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
by blast+
lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
@@ -737,29 +756,29 @@
lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
by (auto simp add: split_if_mem2)
-lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
+lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
by (auto intro: bool_contrapos)
lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
by blast
lemma UN_mono:
- "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
+ "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
(\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
by (blast dest: subsetD)
-lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
+lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
by blast
-lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
+lemma vimage_UN: "f -` (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. f -` B x)"
by blast
-lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
+lemma vimage_eq_UN: "f -` B = (\<Union>y\<in>B. f -` {y})"
-- {* NOT suitable for rewriting *}
by blast
-lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
-by blast
+lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
+ by blast
subsection {* Distributive laws *}
@@ -770,7 +789,7 @@
lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
by blast
-lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A`C) \<union> \<Union>(B`C)"
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A ` C) \<union> \<Union>(B ` C)"
-- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
-- {* Union of a family of unions *}
by blast
@@ -782,7 +801,7 @@
lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
by blast
-lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A`C) \<inter> \<Inter>(B`C)"
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A ` C) \<inter> \<Inter>(B ` C)"
by blast
lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
@@ -805,10 +824,10 @@
subsection {* Complement *}
-lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
+lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
by blast
-lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
+lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
by blast
@@ -818,94 +837,85 @@
and Intersections. *}
lemma UN_simps [simp]:
- "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"
- "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))"
- "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))"
- "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)"
- "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))"
- "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)"
- "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))"
- "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"
- "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)"
- "!!A B f. (UN x:f`A. B x) = (UN a:A. B (f a))"
+ "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
+ "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
+ "\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
+ "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter>B)"
+ "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
+ "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
+ "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
+ "\<And>A B. (UN x: \<Union>A. B x) = (\<Union>y\<in>A. UN x:y. B x)"
+ "\<And>A B C. (UN z: UNION A B. C z) = (\<Union>x\<in>A. UN z: B(x). C z)"
+ "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
by auto
lemma INT_simps [simp]:
- "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"
- "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"
- "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)"
- "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))"
- "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"
- "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)"
- "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))"
- "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"
- "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"
- "!!A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
+ "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter>B)"
+ "\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))"
+ "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
+ "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
+ "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)"
+ "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
+ "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
+ "\<And>A B. (INT x: \<Union>A. B x) = (\<Inter>y\<in>A. INT x:y. B x)"
+ "\<And>A B C. (INT z: UNION A B. C z) = (\<Inter>x\<in>A. INT z: B(x). C z)"
+ "\<And>A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
by auto
lemma ball_simps [simp,no_atp]:
- "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
- "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
- "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
- "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"
- "!!P. (ALL x:{}. P x) = True"
- "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"
- "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"
- "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"
- "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"
- "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"
- "!!A P f. (ALL x:f`A. P x) = (ALL x:A. P (f x))"
- "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
+ "\<And>A P Q. (\<forall>x\<in>A. P x | Q) = ((\<forall>x\<in>A. P x) | Q)"
+ "\<And>A P Q. (\<forall>x\<in>A. P | Q x) = (P | (\<forall>x\<in>A. Q x))"
+ "\<And>A P Q. (\<forall>x\<in>A. P --> Q x) = (P --> (\<forall>x\<in>A. Q x))"
+ "\<And>A P Q. (\<forall>x\<in>A. P x --> Q) = ((\<exists>x\<in>A. P x) --> Q)"
+ "\<And>P. (\<forall> x\<in>{}. P x) = True"
+ "\<And>P. (\<forall> x\<in>UNIV. P x) = (ALL x. P x)"
+ "\<And>a B P. (\<forall> x\<in>insert a B. P x) = (P a & (\<forall> x\<in>B. P x))"
+ "\<And>A P. (\<forall> x\<in>\<Union>A. P x) = (\<forall>y\<in>A. \<forall> x\<in>y. P x)"
+ "\<And>A B P. (\<forall> x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall> x\<in> B a. P x)"
+ "\<And>P Q. (\<forall> x\<in>Collect Q. P x) = (ALL x. Q x --> P x)"
+ "\<And>A P f. (\<forall> x\<in>f`A. P x) = (\<forall>x\<in>A. P (f x))"
+ "\<And>A P. (~(\<forall>x\<in>A. P x)) = (\<exists>x\<in>A. ~P x)"
by auto
lemma bex_simps [simp,no_atp]:
- "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
- "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
- "!!P. (EX x:{}. P x) = False"
- "!!P. (EX x:UNIV. P x) = (EX x. P x)"
- "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
- "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"
- "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
- "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
- "!!A P f. (EX x:f`A. P x) = (EX x:A. P (f x))"
- "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"
+ "\<And>A P Q. (\<exists>x\<in>A. P x & Q) = ((\<exists>x\<in>A. P x) & Q)"
+ "\<And>A P Q. (\<exists>x\<in>A. P & Q x) = (P & (\<exists>x\<in>A. Q x))"
+ "\<And>P. (EX x:{}. P x) = False"
+ "\<And>P. (EX x:UNIV. P x) = (EX x. P x)"
+ "\<And>a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
+ "\<And>A P. (EX x:\<Union>A. P x) = (EX y:A. EX x:y. P x)"
+ "\<And>A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
+ "\<And>P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
+ "\<And>A P f. (EX x:f`A. P x) = (\<exists>x\<in>A. P (f x))"
+ "\<And>A P. (~(\<exists>x\<in>A. P x)) = (\<forall>x\<in>A. ~P x)"
by auto
-lemma ball_conj_distrib:
- "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"
- by blast
-
-lemma bex_disj_distrib:
- "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"
- by blast
-
-
text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
lemma UN_extend_simps:
- "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"
- "!!A B C. (UN x:C. A x) Un B = (if C={} then B else (UN x:C. A x Un B))"
- "!!A B C. A Un (UN x:C. B x) = (if C={} then A else (UN x:C. A Un B x))"
- "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"
- "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"
- "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"
- "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"
- "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"
- "!!A B C. (UN x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
- "!!A B f. (UN a:A. B (f a)) = (UN x:f`A. B x)"
+ "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
+ "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
+ "\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
+ "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter>B) = (\<Union>x\<in>C. A x \<inter> B)"
+ "\<And>A B C. (A \<inter>(\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
+ "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
+ "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
+ "\<And>A B. (\<Union>y\<in>A. UN x:y. B x) = (UN x: \<Union>A. B x)"
+ "\<And>A B C. (\<Union>x\<in>A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
+ "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
by auto
lemma INT_extend_simps:
- "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"
- "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"
- "!!A B C. (INT x:C. A x) - B = (if C={} then UNIV-B else (INT x:C. A x - B))"
- "!!A B C. A - (UN x:C. B x) = (if C={} then A else (INT x:C. A - B x))"
- "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"
- "!!A B C. ((INT x:C. A x) Un B) = (INT x:C. A x Un B)"
- "!!A B C. A Un (INT x:C. B x) = (INT x:C. A Un B x)"
- "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"
- "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
- "!!A B f. (INT a:A. B (f a)) = (INT x:f`A. B x)"
+ "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter>B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))"
+ "\<And>A B C. A \<inter>(\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))"
+ "\<And>A B C. (\<Inter>x\<in>C. A x) - B = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))"
+ "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
+ "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))"
+ "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
+ "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
+ "\<And>A B. (\<Inter>y\<in>A. INT x:y. B x) = (INT x: \<Union>A. B x)"
+ "\<And>A B C. (\<Inter>x\<in>A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
+ "\<And>A B f. (INT a:A. B (f a)) = (INT x:f`A. B x)"
by auto
--- a/src/HOL/Import/hol4rews.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML Thu Jul 14 22:53:43 2011 +0200
@@ -160,7 +160,7 @@
let
val _ = message "Adding HOL4 rewrite"
val th1 = th RS @{thm eq_reflection}
- handle _ => th
+ handle THM _ => th
val current_rews = HOL4Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
@@ -168,7 +168,7 @@
(Context.Theory updated_thy,th1)
end
| add_hol4_rewrite (context, th) = (context,
- (th RS @{thm eq_reflection} handle _ => th)
+ (th RS @{thm eq_reflection} handle THM _ => th)
);
fun ignore_hol4 bthy bthm thy =
--- a/src/HOL/IsaMakefile Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 14 22:53:43 2011 +0200
@@ -74,6 +74,7 @@
TLA-Buffer \
TLA-Inc \
TLA-Memory \
+ HOL-TPTP \
HOL-UNITY \
HOL-Unix \
HOL-Word-Examples \
@@ -553,15 +554,15 @@
## HOL-Import
-IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
- Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
- Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
- Import/hol4rews.ML Import/import.ML Import/ROOT.ML
-
-IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
- Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
- Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
- Import/hol4rews.ML Import/import.ML Import/ROOT.ML
+IMPORTER_FILES = \
+ Import/ImportRecorder.thy Import/HOL4Compat.thy \
+ Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \
+ Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \
+ Import/import.ML Import/importrecorder.ML Import/import_syntax.ML \
+ Import/lazy_seq.ML Import/mono_scan.ML Import/mono_seq.ML \
+ Import/proof_kernel.ML Import/replay.ML Import/scan.ML Import/seq.ML \
+ Import/shuffler.ML Import/xml.ML Import/xmlconv.ML \
+ Library/ContNotDenum.thy Old_Number_Theory/Primes.thy
HOL-Import: HOL $(LOG)/HOL-Import.gz
@@ -587,7 +588,7 @@
HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \
- $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \
+ $(IMPORTER_FILES) Import/Generate-HOLLight/GenHOLLight.thy \
Import/Generate-HOLLight/ROOT.ML
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
@@ -616,7 +617,7 @@
HOLLight: HOL $(LOG)/HOLLight.gz
-$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \
+$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_FILES) \
Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
Import/HOLLight/ROOT.ML
@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
@@ -1047,9 +1048,9 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
- ex/ATP_Export.thy ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
+ ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
- ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \
+ ex/CTL.thy ex/Case_Product.thy \
ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
@@ -1164,6 +1165,19 @@
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
+## HOL-TPTP
+
+HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz
+
+$(LOG)/HOL-TPTP.gz: \
+ $(OUT)/HOL \
+ TPTP/ROOT.ML \
+ TPTP/ATP_Export.thy \
+ TPTP/CASC_Setup.thy \
+ TPTP/atp_export.ML
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
+
+
## HOL-Multivariate_Analysis
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
@@ -1457,8 +1471,9 @@
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
- Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
- Quotient_Examples/Quotient_Message.thy
+ Quotient_Examples/DList.thy Quotient_Examples/Cset.thy \
+ Quotient_Examples/FSet.thy Quotient_Examples/List_Cset.thy \
+ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- a/src/HOL/Library/Option_ord.thy Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Library/Option_ord.thy Thu Jul 14 22:53:43 2011 +0200
@@ -58,7 +58,7 @@
instance option :: (linorder) linorder proof
qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
-instantiation option :: (preorder) bot
+instantiation option :: (order) bot
begin
definition "bot = None"
--- a/src/HOL/Library/Quickcheck_Types.thy Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Thu Jul 14 22:53:43 2011 +0200
@@ -108,7 +108,7 @@
instance bot :: (linorder) linorder proof
qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
-instantiation bot :: (preorder) bot
+instantiation bot :: (order) bot
begin
definition "bot = Bot"
@@ -208,7 +208,7 @@
instance top :: (linorder) linorder proof
qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
-instantiation top :: (preorder) top
+instantiation top :: (order) top
begin
definition "top = Top"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 14 22:53:43 2011 +0200
@@ -10,6 +10,7 @@
val keepK = "keep"
val type_encK = "type_enc"
val slicingK = "slicing"
+val lambda_translationK = "lambda_translation"
val e_weight_methodK = "e_weight_method"
val spass_force_sosK = "spass_force_sos"
val vampire_force_sosK = "vampire_force_sos"
@@ -353,8 +354,9 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
- vampire_force_sos hard_timeout timeout dir st =
+fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
+ e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
+ st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -367,6 +369,9 @@
val st' =
st |> Proof.map_context
(change_dir dir
+ #> (Option.map (Config.put
+ Sledgehammer_Provers.atp_lambda_translation)
+ lambda_translation |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.spass_force_sos)
@@ -455,6 +460,7 @@
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
+ val lambda_translation = AList.lookup (op =) args lambda_translationK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
val spass_force_sos = AList.lookup (op =) args spass_force_sosK
|> Option.map (curry (op <>) "false")
@@ -466,8 +472,9 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
- vampire_force_sos hard_timeout timeout dir st
+ run_sh prover_name prover type_enc max_relevant slicing lambda_translation
+ e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
+ dir st
in
case result of
SH_OK (time_isa, time_prover, names) =>
--- a/src/HOL/Orderings.thy Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Orderings.thy Thu Jul 14 22:53:43 2011 +0200
@@ -1081,15 +1081,37 @@
done
-subsection {* Top and bottom elements *}
+subsection {* (Unique) top and bottom elements *}
-class bot = preorder +
+class bot = order +
fixes bot :: 'a
assumes bot_least [simp]: "bot \<le> x"
+begin
-class top = preorder +
+lemma bot_unique:
+ "a \<le> bot \<longleftrightarrow> a = bot"
+ by (auto simp add: intro: antisym)
+
+lemma bot_less:
+ "a \<noteq> bot \<longleftrightarrow> bot < a"
+ by (auto simp add: less_le_not_le intro!: antisym)
+
+end
+
+class top = order +
fixes top :: 'a
assumes top_greatest [simp]: "x \<le> top"
+begin
+
+lemma top_unique:
+ "top \<le> a \<longleftrightarrow> a = top"
+ by (auto simp add: intro: antisym)
+
+lemma less_top:
+ "a \<noteq> top \<longleftrightarrow> a < top"
+ by (auto simp add: less_le_not_le intro!: antisym)
+
+end
subsection {* Dense orders *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Cset.thy Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,119 @@
+(* Title: HOL/Quotient_Examples/Cset.thy
+ Author: Florian Haftmann, Alexander Krauss, TU Muenchen
+*)
+
+header {* A variant of theory Cset from Library, defined as a quotient *}
+
+theory Cset
+imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax"
+begin
+
+subsection {* Lifting *}
+
+(*FIXME: quotient package requires a dedicated constant*)
+definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp]: "set_eq \<equiv> op ="
+
+quotient_type 'a set = "'a Set.set" / "set_eq"
+by (simp add: identity_equivp)
+
+hide_type (open) set
+
+subsection {* Operations *}
+
+lemma [quot_respect]:
+ "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
+ "(op = ===> set_eq) Collect Collect"
+ "(set_eq ===> op =) More_Set.is_empty More_Set.is_empty"
+ "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
+ "(op = ===> set_eq ===> set_eq) More_Set.remove More_Set.remove"
+ "(op = ===> set_eq ===> set_eq) image image"
+ "(op = ===> set_eq ===> set_eq) More_Set.project More_Set.project"
+ "(set_eq ===> op =) Ball Ball"
+ "(set_eq ===> op =) Bex Bex"
+ "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
+ "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
+ "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
+ "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
+ "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
+ "set_eq {} {}"
+ "set_eq UNIV UNIV"
+ "(set_eq ===> set_eq) uminus uminus"
+ "(set_eq ===> set_eq ===> set_eq) minus minus"
+ "((set_eq ===> op =) ===> set_eq) Inf Inf"
+ "((set_eq ===> op =) ===> set_eq) Sup Sup"
+ "(op = ===> set_eq) List.set List.set"
+by (auto simp: fun_rel_eq)
+
+quotient_definition "member :: 'a => 'a Cset.set => bool"
+is "op \<in>"
+quotient_definition "Set :: ('a => bool) => 'a Cset.set"
+is Collect
+quotient_definition is_empty where "is_empty :: 'a Cset.set \<Rightarrow> bool"
+is More_Set.is_empty
+quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is Set.insert
+quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is More_Set.remove
+quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set"
+is image
+quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is More_Set.project
+quotient_definition "forall :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+is Ball
+quotient_definition "exists :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+is Bex
+quotient_definition card where "card :: 'a Cset.set \<Rightarrow> nat"
+is Finite_Set.card
+quotient_definition set where "set :: 'a list => 'a Cset.set"
+is List.set
+quotient_definition subset where "subset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool"
+is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+quotient_definition psubset where "psubset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool"
+is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+quotient_definition inter where "inter :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition union where "union :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition empty where "empty :: 'a Cset.set"
+is "{} :: 'a set"
+quotient_definition UNIV where "UNIV :: 'a Cset.set"
+is "Set.UNIV :: 'a set"
+quotient_definition uminus where "uminus :: 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
+quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition Inf where "Inf :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
+is "Inf_class.Inf :: 'a set set \<Rightarrow> 'a set"
+quotient_definition Sup where "Sup :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
+is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a set"
+
+
+context complete_lattice
+begin
+
+(* FIXME: Would like to use
+
+quotient_definition "Infimum :: 'a Cset.set \<Rightarrow> 'a"
+is "Inf"
+
+but it fails, presumably because @{term "Inf"} is a Free.
+*)
+
+definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
+ [simp]: "Infimum A = Inf (\<lambda>x. member x A)"
+
+definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
+ [simp]: "Supremum A = Sup (\<lambda>x. member x A)"
+
+end
+
+hide_const (open) is_empty insert remove map filter forall exists card
+ set subset psubset inter union empty UNIV uminus minus Inf Sup
+
+hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
+ forall_def exists_def card_def set_def subset_def psubset_def
+ inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/List_Cset.thy Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,197 @@
+(* Title: HOL/Quotient_Examples/List_Cset.thy
+ Author: Florian Haftmann, Alexander Krauss, TU Muenchen
+*)
+
+header {* Implementation of type Cset.set based on lists. Code equations obtained via quotient lifting. *}
+
+theory List_Cset
+imports Cset
+begin
+
+lemma [quot_respect]: "((op = ===> set_eq ===> set_eq) ===> op = ===> set_eq ===> set_eq)
+ foldr foldr"
+by (simp add: fun_rel_eq)
+
+lemma [quot_preserve]: "((id ---> abs_set ---> rep_set) ---> id ---> rep_set ---> abs_set) foldr = foldr"
+apply (rule ext)+
+by (induct_tac xa) (auto simp: Quotient_abs_rep[OF Quotient_set])
+
+
+subsection {* Relationship to lists *}
+
+(*FIXME: maybe define on sets first and then lift -> more canonical*)
+definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
+ "coset xs = Cset.uminus (Cset.set xs)"
+
+code_datatype Cset.set List_Cset.coset
+
+lemma member_code [code]:
+ "member x (Cset.set xs) \<longleftrightarrow> List.member xs x"
+ "member x (coset xs) \<longleftrightarrow> \<not> List.member xs x"
+unfolding coset_def
+apply (lifting in_set_member)
+by descending (simp add: in_set_member)
+
+definition (in term_syntax)
+ setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+ \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+ [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+instantiation Cset.set :: (random) random
+begin
+
+definition
+ "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+subsection {* Basic operations *}
+
+lemma is_empty_set [code]:
+ "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
+ by (lifting is_empty_set)
+hide_fact (open) is_empty_set
+
+lemma empty_set [code]:
+ "Cset.empty = Cset.set []"
+ by (lifting set.simps(1)[symmetric])
+hide_fact (open) empty_set
+
+lemma UNIV_set [code]:
+ "Cset.UNIV = coset []"
+ unfolding coset_def by descending simp
+hide_fact (open) UNIV_set
+
+lemma remove_set [code]:
+ "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
+ "Cset.remove x (coset xs) = coset (List.insert x xs)"
+unfolding coset_def
+apply descending
+apply (simp add: More_Set.remove_def)
+apply descending
+by (simp add: remove_set_compl)
+
+lemma insert_set [code]:
+ "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
+ "Cset.insert x (coset xs) = coset (removeAll x xs)"
+unfolding coset_def
+apply (lifting set_insert[symmetric])
+by descending simp
+
+lemma map_set [code]:
+ "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
+by descending simp
+
+lemma filter_set [code]:
+ "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
+by descending (simp add: project_set)
+
+lemma forall_set [code]:
+ "Cset.forall (Cset.set xs) P \<longleftrightarrow> list_all P xs"
+(* FIXME: why does (lifting Ball_set_list_all) fail? *)
+by descending (fact Ball_set_list_all)
+
+lemma exists_set [code]:
+ "Cset.exists (Cset.set xs) P \<longleftrightarrow> list_ex P xs"
+by descending (fact Bex_set_list_ex)
+
+lemma card_set [code]:
+ "Cset.card (Cset.set xs) = length (remdups xs)"
+by (lifting length_remdups_card_conv[symmetric])
+
+lemma compl_set [simp, code]:
+ "Cset.uminus (Cset.set xs) = coset xs"
+unfolding coset_def by descending simp
+
+lemma compl_coset [simp, code]:
+ "Cset.uminus (coset xs) = Cset.set xs"
+unfolding coset_def by descending simp
+
+context complete_lattice
+begin
+
+(* FIXME: automated lifting fails, since @{term inf} and @{term top}
+ are variables (???) *)
+lemma Infimum_inf [code]:
+ "Infimum (Cset.set As) = foldr inf As top"
+ "Infimum (coset []) = bot"
+unfolding Infimum_def member_code List.member_def
+apply (simp add: mem_def Inf_set_foldr)
+apply (simp add: Inf_UNIV[unfolded UNIV_def Collect_def])
+done
+
+lemma Supremum_sup [code]:
+ "Supremum (Cset.set As) = foldr sup As bot"
+ "Supremum (coset []) = top"
+unfolding Supremum_def member_code List.member_def
+apply (simp add: mem_def Sup_set_foldr)
+apply (simp add: Sup_UNIV[unfolded UNIV_def Collect_def])
+done
+
+end
+
+
+
+subsection {* Derived operations *}
+
+lemma subset_eq_forall [code]:
+ "Cset.subset A B \<longleftrightarrow> Cset.forall A (\<lambda>x. member x B)"
+by descending blast
+
+lemma subset_subset_eq [code]:
+ "Cset.psubset A B \<longleftrightarrow> Cset.subset A B \<and> \<not> Cset.subset B A"
+by descending blast
+
+instantiation Cset.set :: (type) equal
+begin
+
+definition [code]:
+ "HOL.equal A B \<longleftrightarrow> Cset.subset A B \<and> Cset.subset B A"
+
+instance
+apply intro_classes
+unfolding equal_set_def
+by descending auto
+
+end
+
+lemma [code nbe]:
+ "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
+ by (fact equal_refl)
+
+
+subsection {* Functorial operations *}
+
+lemma inter_project [code]:
+ "Cset.inter A (Cset.set xs) = Cset.set (List.filter (\<lambda>x. Cset.member x A) xs)"
+ "Cset.inter A (coset xs) = foldr Cset.remove xs A"
+apply descending
+apply auto
+unfolding coset_def
+apply descending
+apply simp
+by (metis diff_eq minus_set_foldr)
+
+lemma subtract_remove [code]:
+ "Cset.minus A (Cset.set xs) = foldr Cset.remove xs A"
+ "Cset.minus A (coset xs) = Cset.set (List.filter (\<lambda>x. member x A) xs)"
+unfolding coset_def
+apply (lifting minus_set_foldr)
+by descending auto
+
+lemma union_insert [code]:
+ "Cset.union (Cset.set xs) A = foldr Cset.insert xs A"
+ "Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)"
+unfolding coset_def
+apply (lifting union_set_foldr)
+by descending auto
+
+end
\ No newline at end of file
--- a/src/HOL/Quotient_Examples/ROOT.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Thu Jul 14 22:53:43 2011 +0200
@@ -4,5 +4,5 @@
Testing the quotient package.
*)
-use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Cset", "List_Cset"];
--- a/src/HOL/Set.thy Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Set.thy Thu Jul 14 22:53:43 2011 +0200
@@ -416,6 +416,14 @@
lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
by blast
+lemma ball_conj_distrib:
+ "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x))"
+ by blast
+
+lemma bex_disj_distrib:
+ "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x))"
+ by blast
+
text {* Congruence rules *}
@@ -535,7 +543,7 @@
lemma empty_def:
"{} = {x. False}"
- by (simp add: bot_fun_def bot_bool_def Collect_def)
+ by (simp add: bot_fun_def Collect_def)
lemma empty_iff [simp]: "(c : {}) = False"
by (simp add: empty_def)
@@ -568,7 +576,7 @@
lemma UNIV_def:
"UNIV = {x. True}"
- by (simp add: top_fun_def top_bool_def Collect_def)
+ by (simp add: top_fun_def Collect_def)
lemma UNIV_I [simp]: "x : UNIV"
by (simp add: UNIV_def)
@@ -627,7 +635,7 @@
subsubsection {* Set complement *}
lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
- by (simp add: mem_def fun_Compl_def bool_Compl_def)
+ by (simp add: mem_def fun_Compl_def)
lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
by (unfold mem_def fun_Compl_def bool_Compl_def) blast
@@ -638,7 +646,7 @@
right side of the notional turnstile ... *}
lemma ComplD [dest!]: "c : -A ==> c~:A"
- by (simp add: mem_def fun_Compl_def bool_Compl_def)
+ by (simp add: mem_def fun_Compl_def)
lemmas ComplE = ComplD [elim_format]
@@ -658,7 +666,7 @@
lemma Int_def:
"A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
- by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
+ by (simp add: inf_fun_def Collect_def mem_def)
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
by (unfold Int_def) blast
@@ -692,7 +700,7 @@
lemma Un_def:
"A \<union> B = {x. x \<in> A \<or> x \<in> B}"
- by (simp add: sup_fun_def sup_bool_def Collect_def mem_def)
+ by (simp add: sup_fun_def Collect_def mem_def)
lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
by (unfold Un_def) blast
@@ -724,7 +732,7 @@
subsubsection {* Set difference *}
lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
- by (simp add: mem_def fun_diff_def bool_diff_def)
+ by (simp add: mem_def fun_diff_def)
lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
by simp
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/ATP_Export.thy Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,44 @@
+theory ATP_Export
+imports Complex_Main
+uses "atp_export.ML"
+begin
+
+ML {*
+val do_it = false; (* switch to "true" to generate the files *)
+val thy = @{theory Complex_Main};
+val ctxt = @{context}
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds"
+ "/tmp/infs_poly_preds.tptp"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags"
+ "/tmp/infs_poly_tags.tptp"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy"
+ "/tmp/infs_poly_tags_heavy.tptp"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_graph_file_for_theory ctxt thy
+ "/tmp/graph.out"
+else
+ ()
+*}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/CASC_Setup.thy Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,150 @@
+(* Title: HOL/TPTP/CASC_Setup.thy
+ Author: Jasmin Blanchette
+ Copyright 2011
+
+Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
+TNT divisions. This theory file should be loaded by the Isabelle theory files
+generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files.
+*)
+
+theory CASC_Setup
+imports Complex_Main
+uses "../ex/sledgehammer_tactics.ML"
+begin
+
+consts
+ is_int :: "'a \<Rightarrow> bool"
+ is_rat :: "'a \<Rightarrow> bool"
+
+overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool"
+begin
+ definition "rat_is_int (q\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>int. q = of_int n)"
+end
+
+overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool"
+begin
+ definition "real_is_int (x\<Colon>real) \<longleftrightarrow> x \<in> \<int>"
+end
+
+overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool"
+begin
+ definition "real_is_rat (x\<Colon>real) \<longleftrightarrow> x \<in> \<rat>"
+end
+
+consts
+ to_int :: "'a \<Rightarrow> int"
+ to_rat :: "'a \<Rightarrow> rat"
+ to_real :: "'a \<Rightarrow> real"
+
+overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
+begin
+ definition "rat_to_int (q\<Colon>rat) = floor q"
+end
+
+overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
+begin
+ definition "real_to_int (x\<Colon>real) = floor x"
+end
+
+overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat"
+begin
+ definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)"
+end
+
+overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat"
+begin
+ definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)"
+end
+
+overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real"
+begin
+ definition "int_to_real (n\<Colon>int) = real n"
+end
+
+overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real"
+begin
+ definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>real)"
+end
+
+declare
+ rat_is_int_def [simp]
+ real_is_int_def [simp]
+ real_is_rat_def [simp]
+ rat_to_int_def [simp]
+ real_to_int_def [simp]
+ int_to_rat_def [simp]
+ real_to_rat_def [simp]
+ int_to_real_def [simp]
+ rat_to_real_def [simp]
+
+lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n\<Colon>int))"
+by (metis int_to_rat_def rat_is_int_def)
+
+lemma to_real_is_int [intro, simp]: "is_int (to_real (n\<Colon>int))"
+by (metis Ints_real_of_int int_to_real_def real_is_int_def)
+
+lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>rat))"
+by (metis Rats_of_rat rat_to_real_def real_is_rat_def)
+
+lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
+by (metis injI of_rat_eq_iff rat_to_real_def)
+
+declare mem_def [simp add]
+
+declare [[smt_oracle]]
+
+refute_params [maxtime = 10000, no_assms, expect = genuine]
+nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
+ batch_size = 1, expect = genuine]
+
+ML {* Proofterm.proofs := 0 *}
+
+ML {*
+fun SOLVE_TIMEOUT seconds name tac st =
+ let
+ val result =
+ TimeLimit.timeLimit (Time.fromSeconds seconds)
+ (fn () => SINGLE (SOLVE tac) st) ()
+ handle TimeLimit.TimeOut => NONE
+ | ERROR _ => NONE
+ in
+ (case result of
+ NONE => (warning ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
+ end
+*}
+
+ML {*
+fun isabellep_tac ctxt max_secs =
+ SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+ (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
+ THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "metis"
+ (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
+ ORELSE
+ SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
+*}
+
+method_setup isabellep = {*
+ Scan.lift (Scan.optional Parse.nat 6000) >>
+ (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
+*} "combination of Isabelle provers and oracles for CASC"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/ROOT.ML Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,14 @@
+(* Title: HOL/TPTP/ROOT.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Nik Sultana, University of Cambridge
+ Copyright 2011
+
+TPTP-related extensions.
+*)
+
+use_thys [
+ "ATP_Export"
+];
+
+Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
+ use_thy "CASC_Setup";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/atp_export.ML Thu Jul 14 22:53:43 2011 +0200
@@ -0,0 +1,196 @@
+(* Title: HOL/ex/atp_export.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2011
+
+Export Isabelle theories as first-order TPTP inferences, exploiting
+Sledgehammer's translation.
+*)
+
+signature ATP_EXPORT =
+sig
+ val theorems_mentioned_in_proof_term :
+ string list option -> thm -> string list
+ val generate_tptp_graph_file_for_theory :
+ Proof.context -> theory -> string -> unit
+ val generate_tptp_inference_file_for_theory :
+ Proof.context -> theory -> string -> string -> unit
+end;
+
+structure ATP_Export : ATP_EXPORT =
+struct
+
+open ATP_Problem
+open ATP_Translate
+open ATP_Proof
+open ATP_Systems
+
+val fact_name_of = prefix fact_prefix o ascii_of
+
+fun facts_of thy =
+ Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
+ true [] []
+ |> filter (curry (op =) @{typ bool} o fastype_of
+ o Object_Logic.atomize_term thy o prop_of o snd)
+
+(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
+ fixes that seem to be missing over there; or maybe the two code portions are
+ not doing the same? *)
+fun fold_body_thms thm_name all_names f =
+ let
+ fun app n (PBody {thms, ...}) =
+ thms |> fold (fn (_, (name, prop, body)) => fn x =>
+ let
+ val body' = Future.join body
+ val n' =
+ n + (if name = "" orelse
+ (is_some all_names andalso
+ not (member (op =) (the all_names) name)) orelse
+ (* uncommon case where the proved theorem occurs twice
+ (e.g., "Transitive_Closure.trancl_into_trancl") *)
+ n = 1 andalso name = thm_name then
+ 0
+ else
+ 1)
+ val x' = x |> n' <= 1 ? app n' body'
+ in (x' |> n = 1 ? f (name, prop, body')) end)
+ in fold (app 0) end
+
+fun theorems_mentioned_in_proof_term all_names thm =
+ let
+ fun collect (s, _, _) = if s <> "" then insert (op =) s else I
+ val names =
+ [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect
+ [Thm.proof_body_of thm]
+ |> map fact_name_of
+ in names end
+
+fun interesting_const_names ctxt =
+ let val thy = Proof_Context.theory_of ctxt in
+ Sledgehammer_Filter.const_names_in_fact thy
+ (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
+ end
+
+fun generate_tptp_graph_file_for_theory ctxt thy file_name =
+ let
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val axioms = Theory.all_axioms_of thy |> map fst
+ fun do_thm thm =
+ let
+ val name = Thm.get_name_hint thm
+ val s =
+ "[" ^ Thm.legacy_get_kind thm ^ "] " ^
+ (if member (op =) axioms name then "A" else "T") ^ " " ^
+ prefix fact_prefix (ascii_of name) ^ ": " ^
+ commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^
+ commas (map (prefix const_prefix o ascii_of)
+ (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
+ in File.append path s end
+ val thms = facts_of thy |> map snd
+ val _ = map do_thm thms
+ in () end
+
+fun inference_term [] = NONE
+ | inference_term ss =
+ ATerm ("inference",
+ [ATerm ("isabelle", []),
+ ATerm (tptp_empty_list, []),
+ ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)])
+ |> SOME
+fun inference infers ident =
+ these (AList.lookup (op =) infers ident) |> inference_term
+fun add_inferences_to_problem_line infers
+ (Formula (ident, Axiom, phi, NONE, NONE)) =
+ Formula (ident, Lemma, phi, inference infers ident, NONE)
+ | add_inferences_to_problem_line _ line = line
+val add_inferences_to_problem =
+ map o apsnd o map o add_inferences_to_problem_line
+
+fun ident_of_problem_line (Decl (ident, _, _)) = ident
+ | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
+
+fun run_some_atp ctxt problem =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *)
+ val {exec, arguments, proof_delims, known_failures, ...} =
+ get_atp thy spassN
+ val _ = problem |> tptp_lines_for_atp_problem FOF
+ |> File.write_list prob_file
+ val command =
+ File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
+ " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
+ File.shell_path prob_file
+ in
+ TimeLimit.timeLimit (seconds 0.3) bash_output command
+ |> fst
+ |> extract_tstplike_proof_and_outcome false true proof_delims
+ known_failures
+ |> snd
+ end
+ handle TimeLimit.TimeOut => SOME TimedOut
+
+val likely_tautology_prefixes =
+ [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
+ |> map (fact_name_of o Context.theory_name)
+
+fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =
+ exists (fn prefix => String.isPrefix prefix ident)
+ likely_tautology_prefixes andalso
+ is_none (run_some_atp ctxt
+ [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
+ | is_problem_line_tautology _ _ = false
+
+structure String_Graph = Graph(type key = string val ord = string_ord);
+
+fun order_facts ord = sort (ord o pairself ident_of_problem_line)
+fun order_problem_facts _ [] = []
+ | order_problem_facts ord ((heading, lines) :: problem) =
+ if heading = factsN then (heading, order_facts ord lines) :: problem
+ else (heading, lines) :: order_problem_facts ord problem
+
+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 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}
+ val atp_problem =
+ atp_problem
+ |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
+ val all_names = facts |> map (Thm.get_name_hint o snd)
+ val infers =
+ facts |> map (fn (_, th) =>
+ (fact_name_of (Thm.get_name_hint th),
+ theorems_mentioned_in_proof_term (SOME all_names) th))
+ val all_atp_problem_names =
+ atp_problem |> maps (map ident_of_problem_line o snd)
+ val infers =
+ infers |> filter (member (op =) all_atp_problem_names o fst)
+ |> map (apsnd (filter (member (op =) all_atp_problem_names)))
+ val ordered_names =
+ String_Graph.empty
+ |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
+ |> fold (fn (to, froms) =>
+ fold (fn from => String_Graph.add_edge (from, to)) froms)
+ infers
+ |> String_Graph.topological_order
+ val order_tab =
+ Symtab.empty
+ |> fold (Symtab.insert (op =))
+ (ordered_names ~~ (1 upto length ordered_names))
+ val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
+ val atp_problem =
+ atp_problem |> add_inferences_to_problem infers
+ |> order_problem_facts name_ord
+ val ss = tptp_lines_for_atp_problem FOF atp_problem
+ val _ = app (File.append path) ss
+ in () end
+
+end;
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Jul 14 22:53:43 2011 +0200
@@ -385,8 +385,9 @@
#> map negate_conjecture_line))
|> (fn problem =>
let
- val conjs = problem |> maps snd |> filter is_problem_line_negated
- in if length conjs = 1 then problem else [] end)
+ val lines = problem |> maps snd
+ val conjs = lines |> filter is_problem_line_negated
+ in if length conjs = 1 andalso conjs <> lines then problem else [] end)
(** Symbol declarations **)
@@ -479,7 +480,7 @@
|> (fn s =>
if size s > max_readable_name_size then
String.substring (s, 0, max_readable_name_size div 2 - 4) ^
- Word.toString (hashw_string (full_name, 0w0)) ^
+ string_of_int (hash_string full_name) ^
String.extract (s, size s - max_readable_name_size div 2 + 4,
NONE)
else
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Jul 14 22:53:43 2011 +0200
@@ -19,7 +19,7 @@
GaveUp |
ProofMissing |
ProofIncomplete |
- UnsoundProof of bool * string list |
+ UnsoundProof of bool option * string list | (* FIXME: doesn't belong here *)
CantConnect |
TimedOut |
Inappropriate |
@@ -76,7 +76,7 @@
GaveUp |
ProofMissing |
ProofIncomplete |
- UnsoundProof of bool * string list |
+ UnsoundProof of bool option * string list |
CantConnect |
TimedOut |
Inappropriate |
@@ -123,11 +123,15 @@
| string_for_failure ProofIncomplete =
"The prover claims the conjecture is a theorem but provided an incomplete \
\proof."
- | string_for_failure (UnsoundProof (false, ss)) =
+ | string_for_failure (UnsoundProof (NONE, ss)) =
+ "The prover found a type-unsound proof " ^ involving ss ^
+ "(or, less likely, your axioms are inconsistent). Specify a sound type \
+ \encoding or omit the \"type_enc\" option."
+ | string_for_failure (UnsoundProof (SOME false, ss)) =
"The prover found a type-unsound proof " ^ involving ss ^
"(or, less likely, your axioms are inconsistent). Try passing the \
- \\"full_types\" option to Sledgehammer to avoid such spurious proofs."
- | string_for_failure (UnsoundProof (true, ss)) =
+ \\"sound\" option to Sledgehammer to avoid such spurious proofs."
+ | string_for_failure (UnsoundProof (SOME true, ss)) =
"The prover found a type-unsound proof " ^ involving ss ^
"even though a supposedly type-sound encoding was used (or, less likely, \
\your axioms are inconsistent). Please report this to the Isabelle \
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 14 22:53:43 2011 +0200
@@ -31,6 +31,11 @@
Preds of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
+ val concealed_lambdasN : string
+ val lambda_liftingN : string
+ val combinatorsN : string
+ val lambdasN : string
+ val smartN : string
val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -76,6 +81,7 @@
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 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
@@ -89,7 +95,7 @@
val factsN : string
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> bool -> bool -> term list -> term
+ -> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
@@ -104,8 +110,13 @@
type name = string * string
-(* experimental *)
-val generate_info = false
+val concealed_lambdasN = "concealed_lambdas"
+val lambda_liftingN = "lambda_lifting"
+val combinatorsN = "combinators"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
+val generate_info = false (* experimental *)
fun isabelle_info s =
if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
@@ -158,6 +169,8 @@
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
+val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
+
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
The character _ goes to __
@@ -896,7 +909,14 @@
else
t
-fun process_abstractions_in_term ctxt type_enc kind t =
+fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
+ | conceal_lambdas Ts (Abs (_, T, t)) =
+ (* slightly unsound because of hash collisions *)
+ Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
+ T --> fastype_of1 (Ts, t))
+ | conceal_lambdas _ t = t
+
+fun process_abstractions_in_term ctxt lambda_trans kind t =
let val thy = Proof_Context.theory_of ctxt in
if Meson.is_fol_term thy t then
t
@@ -919,17 +939,27 @@
| (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else if is_type_enc_higher_order type_enc then
- t |> Envir.eta_contract
- else
- t |> conceal_bounds Ts
- |> Envir.eta_contract
- |> cterm_of thy
- |> Meson_Clausify.introduce_combinators_in_cterm
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
+ | _ =>
+ if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ let val t = t |> Envir.eta_contract in
+ if lambda_trans = concealed_lambdasN then
+ t |> conceal_lambdas []
+ else if lambda_trans = lambda_liftingN then
+ t (* TODO: implement *)
+ else if lambda_trans = combinatorsN then
+ t |> conceal_bounds Ts
+ |> cterm_of thy
+ |> Meson_Clausify.introduce_combinators_in_cterm
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ else if lambda_trans = lambdasN then
+ t
+ else
+ error ("Unknown lambda translation method: " ^
+ quote lambda_trans ^ ".")
+ end
val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
handle THM _ =>
@@ -949,7 +979,7 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-fun preprocess_prop ctxt type_enc presimp_consts kind t =
+fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -962,7 +992,7 @@
|> extensionalize_term ctxt
|> presimplify_term ctxt presimp_consts
|> perhaps (try (HOLogic.dest_Trueprop))
- |> process_abstractions_in_term ctxt type_enc kind
+ |> process_abstractions_in_term ctxt lambda_trans kind
end
(* making fact and conjecture formulas *)
@@ -975,10 +1005,10 @@
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
+ case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
|> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
loc Axiom of
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
@@ -986,7 +1016,8 @@
| formula => SOME formula
end
-fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
+fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+ presimp_consts ts =
let
val thy = Proof_Context.theory_of ctxt
val last = length ts - 1
@@ -1002,7 +1033,8 @@
else I)
in
t |> preproc ?
- (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
+ (preprocess_prop ctxt lambda_trans presimp_consts kind
+ #> freeze_term)
|> make_formula thy type_enc (format <> CNF) (string_of_int j)
Local kind
|> maybe_negate
@@ -1349,7 +1381,8 @@
level_of_type_enc type_enc <> No_Types andalso
not (null (Term.hidden_polymorphism t))
-fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc lambda_trans
+ (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -1371,7 +1404,7 @@
end
|> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
val make_facts =
- map_filter (make_fact ctxt format type_enc false false [])
+ map_filter (make_fact ctxt format type_enc lambda_trans false false [])
val fairly_sound = is_type_enc_fairly_sound type_enc
in
helper_table
@@ -1385,9 +1418,10 @@
|> make_facts)
end
| NONE => []
-fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
- Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
- []
+fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
+ Symtab.fold_rev (append
+ o helper_facts_for_sym ctxt format type_enc lambda_trans)
+ sym_tab []
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
@@ -1427,13 +1461,14 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
- facts =
+fun translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+ hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = facts |> map snd
val presimp_consts = Meson.presimplified_consts ctxt
- val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
+ val make_fact =
+ make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
val (facts, fact_names) =
facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
|> map_filter (try (apfst the))
@@ -1450,7 +1485,8 @@
val tycons = type_constrs_of_terms thy all_ts
val conjs =
hyp_ts @ [concl_t]
- |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
+ |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
+ presimp_consts
val (supers', arity_clauses) =
if level_of_type_enc type_enc = No_Types then ([], [])
else make_arity_clauses thy tycons supers
@@ -1864,15 +1900,15 @@
val conjsN = "Conjectures"
val free_typesN = "Type variables"
-val explicit_apply = NONE (* for experimental purposes *)
+val explicit_apply = NONE (* for experiments *)
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter readable_names preproc hyp_ts concl_t facts =
+ exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
let
val (format, type_enc) = choose_format [format] type_enc
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
- facts
+ translate_formulas ctxt format prem_kind type_enc lambda_trans 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
@@ -1881,8 +1917,9 @@
val repaired_sym_tab =
conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
- |> map repair
+ repaired_sym_tab
+ |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
+ |> map repair
val poly_nonmono_Ts =
if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
polymorphism_of_type_enc type_enc <> Polymorphic then
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Jul 14 22:53:43 2011 +0200
@@ -7,8 +7,8 @@
signature ATP_UTIL =
sig
val timestamp : unit -> string
- val hashw : word * word -> word
- val hashw_string : string * word -> word
+ val hash_string : string -> int
+ val hash_term : term -> int
val strip_spaces : bool -> (char -> bool) -> string -> string
val nat_subscript : int -> string
val unyxml : string -> string
@@ -42,6 +42,13 @@
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
+fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
+ | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
+ | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
+ | hashw_term _ = 0w0
+
+fun hash_string s = Word.toInt (hashw_string (s, 0w0))
+val hash_term = Word.toInt o hashw_term
fun strip_c_style_comment _ [] = []
| strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
--- a/src/HOL/Tools/Meson/meson.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Thu Jul 14 22:53:43 2011 +0200
@@ -575,6 +575,8 @@
if_eq_cancel cases_simp}
val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
+(* FIXME: "let_simp" is probably redundant now that we also rewrite with
+ "Let_def_raw". *)
val nnf_ss =
HOL_basic_ss addsimps nnf_extra_simps
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
@@ -592,7 +594,8 @@
#> simplify nnf_ss
(* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
when "metis_unfold_set_consts" becomes the only mode of operation. *)
- #> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
+ #> Raw_Simplifier.rewrite_rule
+ (@{thm Let_def_raw} :: unfold_set_const_simps ctxt)
fun make_nnf ctxt th = case prems_of th of
[] => th |> presimplify ctxt |> make_nnf1 ctxt
--- a/src/HOL/Tools/Metis/metis_tactics.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu Jul 14 22:53:43 2011 +0200
@@ -39,7 +39,7 @@
val partial_typesN = "partial_types"
val no_typesN = "no_types"
-val really_full_type_enc = "poly_tags_heavy"
+val really_full_type_enc = "mangled_tags_heavy"
val full_type_enc = "poly_preds_heavy_query"
val partial_type_enc = "poly_args"
val no_type_enc = "erased"
--- a/src/HOL/Tools/Metis/metis_translate.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Jul 14 22:53:43 2011 +0200
@@ -94,7 +94,7 @@
map_aterms (fn t as Const (s, _) =>
if String.isPrefix old_skolem_const_prefix s then
AList.lookup (op =) old_skolems s |> the
- |> map_types Type_Infer.paramify_vars
+ |> map_types (map_type_tvar (K dummyT))
else
t
| t => t)
@@ -196,8 +196,8 @@
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 false
- false [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
+ combinatorsN false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Nitpick/lib/Tools/nitrox Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Nitpick/lib/Tools/nitrox Thu Jul 14 22:53:43 2011 +0200
@@ -18,9 +18,11 @@
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
for FILE in "$@"
do
- (echo "theory Nitrox_Run imports Main begin" &&
- echo "ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *}" &&
- echo "end;") | isabelle tty
+ echo "theory $SCRATCH imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ $ISABELLE_PROCESS -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
done
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 14 22:53:43 2011 +0200
@@ -1229,11 +1229,6 @@
| is_ground_term (Const _) = true
| is_ground_term _ = false
-fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
- | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
- | hashw_term _ = 0w0
-val hash_term = Word.toInt o hashw_term
-
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Jul 14 22:53:43 2011 +0200
@@ -79,8 +79,7 @@
val pstrs : string -> Pretty.T list
val unyxml : string -> string
val pretty_maybe_quote : Pretty.T -> Pretty.T
- val hashw : word * word -> word
- val hashw_string : string * word -> word
+ val hash_term : term -> int
end;
structure Nitpick_Util : NITPICK_UTIL =
@@ -298,7 +297,6 @@
if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
end
-val hashw = ATP_Util.hashw
-val hashw_string = ATP_Util.hashw_string
+val hash_term = ATP_Util.hash_term
end;
--- a/src/HOL/Tools/Nitpick/nitrox.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Thu Jul 14 22:53:43 2011 +0200
@@ -21,7 +21,8 @@
exception SYNTAX of string
-val parse_keyword = Scan.this_string
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val tptp_explode = raw_explode o strip_spaces true is_ident_char
fun parse_file_path (c :: ss) =
if c = "'" orelse c = "\"" then
@@ -33,21 +34,20 @@
fun parse_include x =
let
val (file_name, rest) =
- (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
+ (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
--| $$ ".") x
- in
- ((), (file_name |> Path.explode |> File.read
- |> strip_spaces true (K true)
- |> raw_explode) @ rest)
- end
+ val path = file_name |> Path.explode
+ val path =
+ path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
+ in ((), (path |> File.read |> tptp_explode) @ rest) end
val parse_fof_or_cnf =
- (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
+ (Scan.this_string "fof" || Scan.this_string "cnf") |-- $$ "(" |--
Scan.many (not_equal ",") |-- $$ "," |--
- (parse_keyword "axiom" || parse_keyword "definition"
- || parse_keyword "theorem" || parse_keyword "lemma"
- || parse_keyword "hypothesis" || parse_keyword "conjecture"
- || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula
+ (Scan.this_string "axiom" || Scan.this_string "definition"
+ || Scan.this_string "theorem" || Scan.this_string "lemma"
+ || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
+ || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
--| $$ ")" --| $$ "."
>> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
@@ -59,7 +59,7 @@
Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
parse_problem))
- o raw_explode o strip_spaces true (K true)
+ o tptp_explode
val boolT = @{typ bool}
val iotaT = @{typ iota}
@@ -115,7 +115,8 @@
*)
val state = Proof.init @{context}
val params =
- [("card", "1\<emdash>8"),
+ [("card iota", "1\<emdash>100"),
+ ("card", "1\<emdash>8"),
("box", "false"),
("sat_solver", "smart"),
("max_threads", "1"),
@@ -126,7 +127,7 @@
("show_consts", "true"),
("format", "1000"),
("max_potential", "0"),
- (* ("timeout", "240 s"), *)
+ ("timeout", "none"),
("expect", genuineN)]
|> default_params @{theory}
val i = 1
--- a/src/HOL/Tools/SMT/smt_translate.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Jul 14 22:53:43 2011 +0200
@@ -38,7 +38,7 @@
(*translation*)
val add_config: SMT_Utils.class * (Proof.context -> config) ->
Context.generic -> Context.generic
- val lift_lambdas: Proof.context -> term list ->
+ val lift_lambdas: Proof.context -> bool -> term list ->
Proof.context * (term list * term list)
val translate: Proof.context -> string list -> (int * thm) list ->
string * recon
@@ -246,22 +246,25 @@
(** lambda-lifting **)
local
- fun mk_def Ts T lhs rhs =
+ fun mk_def triggers Ts T lhs rhs =
let
val eq = HOLogic.eq_const T $ lhs $ rhs
- val trigger =
+ fun trigger () =
[[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
|> map (HOLogic.mk_list @{typ SMT.pattern})
|> HOLogic.mk_list @{typ "SMT.pattern list"}
fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
- in fold mk_all Ts (@{const SMT.trigger} $ trigger $ eq) end
+ in
+ fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq
+ else eq)
+ end
fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts
fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
| dest_abs Ts t = (Ts, t)
- fun replace_lambda Us Ts t (cx as (defs, ctxt)) =
+ fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) =
let
val t1 = mk_abs Us t
val bs = sort int_ord (Term.add_loose_bnos (t1, 0, []))
@@ -284,31 +287,32 @@
val (is, UTs) = split_list (map_index I (Us @ Ts'))
val f = Free (n, rev UTs ---> T)
val lhs = Term.list_comb (f, map Bound (rev is))
- val def = mk_def UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
+ val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end)
end
- fun traverse Ts t =
+ fun traverse triggers Ts t =
(case t of
(q as Const (@{const_name All}, _)) $ Abs a =>
- abs_traverse Ts a #>> (fn a' => q $ Abs a')
+ abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
| (q as Const (@{const_name Ex}, _)) $ Abs a =>
- abs_traverse Ts a #>> (fn a' => q $ Abs a')
+ abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
| (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
- traverse Ts u ##>> abs_traverse Ts a #>>
+ traverse triggers Ts u ##>> abs_traverse triggers Ts a #>>
(fn (u', a') => l $ u' $ Abs a')
| Abs _ =>
let val (Us, u) = dest_abs [] t
- in traverse (Us @ Ts) u #-> replace_lambda Us Ts end
- | u1 $ u2 => traverse Ts u1 ##>> traverse Ts u2 #>> (op $)
+ in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end
+ | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $)
| _ => pair t)
- and abs_traverse Ts (n, T, t) = traverse (T::Ts) t #>> (fn t' => (n, T, t'))
+ and abs_traverse triggers Ts (n, T, t) =
+ traverse triggers (T::Ts) t #>> (fn t' => (n, T, t'))
in
-fun lift_lambdas ctxt ts =
+fun lift_lambdas ctxt triggers ts =
(Termtab.empty, ctxt)
- |> fold_map (traverse []) ts
+ |> fold_map (traverse triggers []) ts
|> (fn (us, (defs, ctxt')) =>
(ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
@@ -614,7 +618,7 @@
val (ctxt2, ts3) =
ts2
|> eta_expand ctxt1 is_fol funcs
- |> lift_lambdas ctxt1
+ |> lift_lambdas ctxt1 true
||> (op @)
|-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 14 22:53:43 2011 +0200
@@ -63,6 +63,7 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
+ val atp_lambda_translation : string Config.T
val atp_readable_names : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -336,6 +337,9 @@
val measure_run_time =
Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
+val atp_lambda_translation =
+ 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. *)
@@ -510,6 +514,18 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
+fun effective_atp_lambda_translation ctxt type_enc =
+ Config.get ctxt atp_lambda_translation
+ |> (fn trans =>
+ if trans = smartN then
+ if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+ else if trans = lambdasN andalso
+ not (is_type_enc_higher_order type_enc) then
+ error ("Lambda translation method incompatible with \
+ \first-order encoding.")
+ else
+ trans)
+
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
@@ -641,8 +657,10 @@
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_readable_names)
- true hyp_ts concl_t facts
+ type_enc sound false
+ (effective_atp_lambda_translation ctxt type_enc)
+ (Config.get ctxt atp_readable_names) true hyp_ts concl_t
+ facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
val core =
@@ -687,8 +705,11 @@
used_facts_in_unsound_atp_proof ctxt
conjecture_shape facts_offset fact_names atp_proof
|> Option.map (fn facts =>
- UnsoundProof (is_type_enc_virtually_sound type_enc,
- facts |> sort string_ord))
+ UnsoundProof
+ (if is_type_enc_virtually_sound type_enc then
+ SOME sound
+ else
+ NONE, facts |> sort string_ord))
| _ => outcome
in
((pool, conjecture_shape, facts_offset, fact_names,
--- a/src/HOL/ex/ATP_Export.thy Thu Jul 14 22:30:31 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-theory ATP_Export
-imports Complex_Main
-uses "atp_export.ML"
-begin
-
-ML {*
-val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory Complex_Main};
-val ctxt = @{context}
-*}
-
-ML {*
-if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds"
- "/tmp/infs_poly_preds.tptp"
-else
- ()
-*}
-
-ML {*
-if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags"
- "/tmp/infs_poly_tags.tptp"
-else
- ()
-*}
-
-ML {*
-if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy"
- "/tmp/infs_poly_tags_heavy.tptp"
-else
- ()
-*}
-
-ML {*
-if do_it then
- ATP_Export.generate_tptp_graph_file_for_theory ctxt thy
- "/tmp/graph.out"
-else
- ()
-*}
-
-end
--- a/src/HOL/ex/CASC_Setup.thy Thu Jul 14 22:30:31 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-(* Title: HOL/ex/CASC_Setup.thy
- Author: Jasmin Blanchette
- Copyright 2011
-
-Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
-TNT divisions. This theory file should be loaded by the Isabelle theory files
-generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files.
-*)
-
-theory CASC_Setup
-imports Main
-uses "sledgehammer_tactics.ML"
-begin
-
-declare mem_def [simp add]
-
-declare [[smt_oracle]]
-
-refute_params [maxtime = 10000, no_assms, expect = genuine]
-nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
- batch_size = 1, expect = genuine]
-
-ML {* Proofterm.proofs := 0 *}
-
-ML {*
-fun SOLVE_TIMEOUT seconds name tac st =
- let
- val result =
- TimeLimit.timeLimit (Time.fromSeconds seconds)
- (fn () => SINGLE (SOLVE tac) st) ()
- handle TimeLimit.TimeOut => NONE
- | ERROR _ => NONE
- in
- (case result of
- NONE => (warning ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
- end
-*}
-
-ML {*
-fun isabellep_tac ctxt max_secs =
- SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
- (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
- THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "metis"
- (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
- ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
- ORELSE
- SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
-*}
-
-method_setup isabellep = {*
- Scan.lift (Scan.optional Parse.nat 1) >>
- (fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
-*} "combination of Isabelle provers and oracles for CASC"
-
-end
--- a/src/HOL/ex/Quickcheck_Examples.thy Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Thu Jul 14 22:53:43 2011 +0200
@@ -21,6 +21,8 @@
*}
+declare [[quickcheck_timeout = 3600]]
+
subsection {* Lists *}
theorem "map g (map f xs) = map (g o f) xs"
--- a/src/HOL/ex/ROOT.ML Thu Jul 14 22:30:31 2011 +0200
+++ b/src/HOL/ex/ROOT.ML Thu Jul 14 22:53:43 2011 +0200
@@ -11,8 +11,7 @@
"Normalization_by_Evaluation",
"Hebrew",
"Chinese",
- "Serbian",
- "ATP_Export"
+ "Serbian"
];
use_thys [
@@ -78,9 +77,6 @@
"Set_Algebras"
];
-Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
- use_thy "CASC_Setup";
-
if getenv "ISABELLE_GHC" = "" then ()
else use_thy "Quickcheck_Narrowing_Examples";
--- a/src/HOL/ex/atp_export.ML Thu Jul 14 22:30:31 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,196 +0,0 @@
-(* Title: HOL/ex/atp_export.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2011
-
-Export Isabelle theories as first-order TPTP inferences, exploiting
-Sledgehammer's translation.
-*)
-
-signature ATP_EXPORT =
-sig
- val theorems_mentioned_in_proof_term :
- string list option -> thm -> string list
- val generate_tptp_graph_file_for_theory :
- Proof.context -> theory -> string -> unit
- val generate_tptp_inference_file_for_theory :
- Proof.context -> theory -> string -> string -> unit
-end;
-
-structure ATP_Export : ATP_EXPORT =
-struct
-
-open ATP_Problem
-open ATP_Translate
-open ATP_Proof
-open ATP_Systems
-
-val fact_name_of = prefix fact_prefix o ascii_of
-
-fun facts_of thy =
- Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
- true [] []
- |> filter (curry (op =) @{typ bool} o fastype_of
- o Object_Logic.atomize_term thy o prop_of o snd)
-
-(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
- fixes that seem to be missing over there; or maybe the two code portions are
- not doing the same? *)
-fun fold_body_thms thm_name all_names f =
- let
- fun app n (PBody {thms, ...}) =
- thms |> fold (fn (_, (name, prop, body)) => fn x =>
- let
- val body' = Future.join body
- val n' =
- n + (if name = "" orelse
- (is_some all_names andalso
- not (member (op =) (the all_names) name)) orelse
- (* uncommon case where the proved theorem occurs twice
- (e.g., "Transitive_Closure.trancl_into_trancl") *)
- n = 1 andalso name = thm_name then
- 0
- else
- 1)
- val x' = x |> n' <= 1 ? app n' body'
- in (x' |> n = 1 ? f (name, prop, body')) end)
- in fold (app 0) end
-
-fun theorems_mentioned_in_proof_term all_names thm =
- let
- fun collect (s, _, _) = if s <> "" then insert (op =) s else I
- val names =
- [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect
- [Thm.proof_body_of thm]
- |> map fact_name_of
- in names end
-
-fun interesting_const_names ctxt =
- let val thy = Proof_Context.theory_of ctxt in
- Sledgehammer_Filter.const_names_in_fact thy
- (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
- end
-
-fun generate_tptp_graph_file_for_theory ctxt thy file_name =
- let
- val path = file_name |> Path.explode
- val _ = File.write path ""
- val axioms = Theory.all_axioms_of thy |> map fst
- fun do_thm thm =
- let
- val name = Thm.get_name_hint thm
- val s =
- "[" ^ Thm.legacy_get_kind thm ^ "] " ^
- (if member (op =) axioms name then "A" else "T") ^ " " ^
- prefix fact_prefix (ascii_of name) ^ ": " ^
- commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^
- commas (map (prefix const_prefix o ascii_of)
- (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
- in File.append path s end
- val thms = facts_of thy |> map snd
- val _ = map do_thm thms
- in () end
-
-fun inference_term [] = NONE
- | inference_term ss =
- ATerm ("inference",
- [ATerm ("isabelle", []),
- ATerm (tptp_empty_list, []),
- ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)])
- |> SOME
-fun inference infers ident =
- these (AList.lookup (op =) infers ident) |> inference_term
-fun add_inferences_to_problem_line infers
- (Formula (ident, Axiom, phi, NONE, NONE)) =
- Formula (ident, Lemma, phi, inference infers ident, NONE)
- | add_inferences_to_problem_line _ line = line
-val add_inferences_to_problem =
- map o apsnd o map o add_inferences_to_problem_line
-
-fun ident_of_problem_line (Decl (ident, _, _)) = ident
- | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
-
-fun run_some_atp ctxt problem =
- let
- val thy = Proof_Context.theory_of ctxt
- val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *)
- val {exec, arguments, proof_delims, known_failures, ...} =
- get_atp thy spassN
- val _ = problem |> tptp_lines_for_atp_problem FOF
- |> File.write_list prob_file
- val command =
- File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
- " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
- File.shell_path prob_file
- in
- TimeLimit.timeLimit (seconds 0.3) bash_output command
- |> fst
- |> extract_tstplike_proof_and_outcome false true proof_delims
- known_failures
- |> snd
- end
- handle TimeLimit.TimeOut => SOME TimedOut
-
-val likely_tautology_prefixes =
- [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
- |> map (fact_name_of o Context.theory_name)
-
-fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =
- exists (fn prefix => String.isPrefix prefix ident)
- likely_tautology_prefixes andalso
- is_none (run_some_atp ctxt
- [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
- | is_problem_line_tautology _ _ = false
-
-structure String_Graph = Graph(type key = string val ord = string_ord);
-
-fun order_facts ord = sort (ord o pairself ident_of_problem_line)
-fun order_problem_facts _ [] = []
- | order_problem_facts ord ((heading, lines) :: problem) =
- if heading = factsN then (heading, order_facts ord lines) :: problem
- else (heading, lines) :: order_problem_facts ord problem
-
-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 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 false
- true [] @{prop False}
- val atp_problem =
- atp_problem
- |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
- val all_names = facts |> map (Thm.get_name_hint o snd)
- val infers =
- facts |> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
- theorems_mentioned_in_proof_term (SOME all_names) th))
- val all_atp_problem_names =
- atp_problem |> maps (map ident_of_problem_line o snd)
- val infers =
- infers |> filter (member (op =) all_atp_problem_names o fst)
- |> map (apsnd (filter (member (op =) all_atp_problem_names)))
- val ordered_names =
- String_Graph.empty
- |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
- |> fold (fn (to, froms) =>
- fold (fn from => String_Graph.add_edge (from, to)) froms)
- infers
- |> String_Graph.topological_order
- val order_tab =
- Symtab.empty
- |> fold (Symtab.insert (op =))
- (ordered_names ~~ (1 upto length ordered_names))
- val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
- val atp_problem =
- atp_problem |> add_inferences_to_problem infers
- |> order_problem_facts name_ord
- val ss = tptp_lines_for_atp_problem FOF atp_problem
- val _ = app (File.append path) ss
- in () end
-
-end;