# HG changeset patch # User wenzelm # Date 1310676823 -7200 # Node ID 1162191cb57c203cca561cb559192a4b3d6d3645 # Parent 6ce89c4ec14197dfbc8484142b39c463d7a9765f# Parent fad7758421bf07d72a9bd6876ce2dcf07d83ec80 merged diff -r fad7758421bf -r 1162191cb57c NEWS --- 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. diff -r fad7758421bf -r 1162191cb57c doc-src/Sledgehammer/sledgehammer.tex --- 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} diff -r fad7758421bf -r 1162191cb57c src/HOL/Complete_Lattice.thy --- 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: "\{a, b} = a \ b" - by (simp add: Inf_empty Inf_insert) + by (simp add: Inf_insert) lemma Sup_binary: "\{a, b} = a \ b" - by (simp add: Sup_empty Sup_insert) + by (simp add: Sup_insert) lemma le_Inf_iff: "b \ \A \ (\a\A. b \ a)" by (auto intro: Inf_greatest dest: Inf_lower) @@ -116,11 +116,11 @@ "x \ \ \ x = \" by (rule antisym) auto -lemma not_less_bot[simp]: "\ (x \ \)" - using bot_least[of x] by (auto simp: le_less) +lemma not_less_bot [simp]: "\ (x \ \)" + using bot_least [of x] by (auto simp: le_less) -lemma not_top_less[simp]: "\ (\ \ x)" - using top_greatest[of x] by (auto simp: le_less) +lemma not_top_less [simp]: "\ (\ \ x)" + using top_greatest [of x] by (auto simp: le_less) lemma Sup_upper2: "u \ A \ v \ u \ v \ \A" using Sup_upper[of u A] by auto @@ -392,13 +392,32 @@ lemma Inter_Un_distrib: "\(A \ B) = \A \ \B" by (fact Inf_union_distrib) -(*lemma (in complete_lattice) Inf_top_conv [no_atp]: - "\A = \ \ (\x\A. x = \)"*) +lemma (in complete_lattice) Inf_top_conv [no_atp]: + "\A = \ \ (\x\A. x = \)" + "\ = \A \ (\x\A. x = \)" +proof - + show "\A = \ \ (\x\A. x = \)" + proof + assume "\x\A. x = \" + then have "A = {} \ A = {\}" by auto + then show "\A = \" by auto + next + assume "\A = \" + show "\x\A. x = \" + proof (rule ccontr) + assume "\ (\x\A. x = \)" + then obtain x where "x \ A" and "x \ \" by blast + then obtain B where "A = insert x B" by blast + with `\A = \` `x \ \` show False by (simp add: Inf_insert) + qed + qed + then show "\ = \A \ (\x\A. x = \)" by auto +qed lemma Inter_UNIV_conv [simp,no_atp]: "\A = UNIV \ (\x\A. x = UNIV)" "UNIV = \A \ (\x\A. x = UNIV)" - by blast+ + by (fact Inf_top_conv)+ lemma (in complete_lattice) Inf_anti_mono: "B \ A \ \A \ \B" by (auto intro: Inf_greatest Inf_lower) @@ -448,23 +467,23 @@ lemma Inter_image_eq [simp]: "\(B`A) = (\x\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 \ (\x\A. B x) \ (\x\A. b \ 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!]: "(\x. x \ A \ b \ B x) \ b \ (\x\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 : (\x\A. B x) \ a:A \ 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 : (\x\A. B x) \ (b: B a \ R) \ (a~:A \ R) \ 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 \ (\x. x:B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)" by (simp add: INTER_def) lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})" @@ -473,16 +492,16 @@ lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})" by blast -lemma INT_lower: "a \ A ==> (\x\A. B x) \ B a" +lemma INT_lower: "a \ A \ (\x\A. B x) \ B a" by (fact INF_leI) -lemma INT_greatest: "(!!x. x \ A ==> C \ B x) ==> C \ (\x\A. B x)" +lemma INT_greatest: "(\x. x \ A \ C \ B x) \ C \ (\x\A. B x)" by (fact le_INFI) lemma INT_empty [simp]: "(\x\{}. B x) = UNIV" by blast -lemma INT_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)" +lemma INT_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)" by blast lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)" @@ -495,7 +514,7 @@ by blast lemma INT_insert_distrib: - "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)" + "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)" by blast lemma INT_constant [simp]: "(\y\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)) = (\x\A. B x = UNIV)" - "((INT x:A. B x) = UNIV) = (\x\A. B x = UNIV)" + "(UNIV = (\x\A. B x)) = (\x\A. B x = UNIV)" + "((\x\A. B x) = UNIV) = (\x\A. B x = UNIV)" by blast+ -lemma INT_bool_eq: "(\b::bool. A b) = (A True \ A False)" +lemma INT_bool_eq: "(\b. A b) = (A True \ A False)" by (auto intro: bool_induct) lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))" by blast lemma INT_anti_mono: - "B \ A ==> (!!x. x \ A ==> f x \ g x) ==> + "B \ A \ (\x. x \ A \ f x \ g x) \ (\x\A. f x) \ (\x\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 -` (\x\A. B x) = (\x\A. f -` B x)" by blast @@ -555,40 +574,40 @@ by auto lemma UnionE [elim!]: - "A \ \C \ (\X. A\X \ X\C \ R) \ R" + "A \ \C \ (\X. A \ X \ X \ C \ R) \ R" by auto -lemma Union_upper: "B \ A ==> B \ Union A" +lemma Union_upper: "B \ A \ B \ \A" by (iprover intro: subsetI UnionI) -lemma Union_least: "(!!X. X \ A ==> X \ C) ==> Union A \ C" +lemma Union_least: "(\X. X \ A \ X \ C) \ \A \ C" by (iprover intro: subsetI elim: UnionE dest: subsetD) lemma Un_eq_Union: "A \ B = \{A, B}" by blast -lemma Union_empty [simp]: "Union({}) = {}" +lemma Union_empty [simp]: "\{} = {}" by blast -lemma Union_UNIV [simp]: "Union UNIV = UNIV" +lemma Union_UNIV [simp]: "\UNIV = UNIV" by blast -lemma Union_insert [simp]: "Union (insert a B) = a \ \B" +lemma Union_insert [simp]: "\insert a B = a \ \B" by blast -lemma Union_Un_distrib [simp]: "\(A Un B) = \A \ \B" +lemma Union_Un_distrib [simp]: "\(A \ B) = \A \ \B" by blast lemma Union_Int_subset: "\(A \ B) \ \A \ \B" by blast -lemma Union_empty_conv [simp,no_atp]: "(\A = {}) = (\x\A. x = {})" +lemma Union_empty_conv [simp,no_atp]: "(\A = {}) \ (\x\A. x = {})" by blast -lemma empty_Union_conv [simp,no_atp]: "({} = \A) = (\x\A. x = {})" +lemma empty_Union_conv [simp,no_atp]: "({} = \A) \ (\x\A. x = {})" by blast -lemma Union_disjoint: "(\C \ A = {}) = (\B\C. B \ A = {})" +lemma Union_disjoint: "(\C \ A = {}) \ (\B\C. B \ A = {})" by blast lemma subset_Pow_Union: "A \ Pow (\A)" @@ -597,7 +616,7 @@ lemma Union_Pow_eq [simp]: "\(Pow A) = A" by blast -lemma Union_mono: "A \ B ==> \A \ \B" +lemma Union_mono: "A \ B \ \A \ \B" by blast @@ -638,7 +657,7 @@ *} -- {* to avoid eta-contraction of body *} lemma UNION_eq_Union_image: - "(\x\A. B x) = \(B`A)" + "(\x\A. B x) = \(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]: - "\(B`A) = (\x\A. B x)" + "\(B ` A) = (\x\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: (\x\A. B x)) = (\x\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 \ b: B a \ b: (\x\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 : (\x\A. B x) \ (\x. x:A \ b: B x \ R) \ 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 \ (\x. x:B \ C x = D x) \ (\x\A. C x) = (\x\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 \ (\x. x:B =simp=> C x = D x) \ (\x\A. C x) = (\x\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 = (\x\A. {f x})" by blast -lemma UN_upper: "a \ A ==> B a \ (\x\A. B x)" +lemma UN_upper: "a \ A \ B a \ (\x\A. B x)" by (fact le_SUPI) -lemma UN_least: "(!!x. x \ A ==> B x \ C) ==> (\x\A. B x) \ C" +lemma UN_least: "(\x. x \ A \ B x \ C) \ (\x\A. B x) \ C" by (iprover intro: subsetI elim: UN_E dest: subsetD) lemma Collect_bex_eq [no_atp]: "{x. \y\A. P x y} = (\y\A. {x. P x y})" by blast -lemma UN_insert_distrib: "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)" +lemma UN_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)" by blast lemma UN_empty [simp,no_atp]: "(\x\{}. B x) = {}" @@ -696,7 +715,7 @@ lemma UN_singleton [simp]: "(\x\A. {x}) = A" by blast -lemma UN_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)" +lemma UN_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)" by auto lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ UNION A B" @@ -721,8 +740,8 @@ by blast lemma UNION_empty_conv[simp]: - "({} = (UN x:A. B x)) = (\x\A. B x = {})" - "((UN x:A. B x) = {}) = (\x\A. B x = {})" + "{} = (\x\A. B x) \ (\x\A. B x = {})" + "(\x\A. B x) = {} \ (\x\A. B x = {})" by blast+ lemma Collect_ex_eq [no_atp]: "{x. \y. P x y} = (\y. {x. P x y})" @@ -737,29 +756,29 @@ lemma Un_eq_UN: "A \ B = (\b. if b then A else B)" by (auto simp add: split_if_mem2) -lemma UN_bool_eq: "(\b::bool. A b) = (A True \ A False)" +lemma UN_bool_eq: "(\b. A b) = (A True \ A False)" by (auto intro: bool_contrapos) lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)" by blast lemma UN_mono: - "A \ B ==> (!!x. x \ A ==> f x \ g x) ==> + "A \ B \ (\x. x \ A \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)" by (blast dest: subsetD) -lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)" +lemma vimage_Union: "f -` (\A) = (\X\A. f -` X)" by blast -lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)" +lemma vimage_UN: "f -` (\x\A. B x) = (\x\A. f -` B x)" by blast -lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})" +lemma vimage_eq_UN: "f -` B = (\y\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 = (\x\A. f ` B x)" + by blast subsection {* Distributive laws *} @@ -770,7 +789,7 @@ lemma Int_Union2: "\B \ A = (\C\B. C \ A)" by blast -lemma Un_Union_image: "(\x\C. A x \ B x) = \(A`C) \ \(B`C)" +lemma Un_Union_image: "(\x\C. A x \ B x) = \(A ` C) \ \(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 \ \B = (\C\B. A \ C)" by blast -lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A`C) \ \(B`C)" +lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" by blast lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" @@ -805,10 +824,10 @@ subsection {* Complement *} -lemma Compl_UN [simp]: "-(\x\A. B x) = (\x\A. -B x)" +lemma Compl_UN [simp]: "- (\x\A. B x) = (\x\A. -B x)" by blast -lemma Compl_INT [simp]: "-(\x\A. B x) = (\x\A. -B x)" +lemma Compl_INT [simp]: "- (\x\A. B x) = (\x\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))" + "\a B C. (\x\C. insert a (B x)) = (if C={} then {} else insert a (\x\C. B x))" + "\A B C. (\x\C. A x \ B) = ((if C={} then {} else (\x\C. A x) \ B))" + "\A B C. (\x\C. A \ B x) = ((if C={} then {} else A \ (\x\C. B x)))" + "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \B)" + "\A B C. (\x\C. A \ B x) = (A \(\x\C. B x))" + "\A B C. (\x\C. A x - B) = ((\x\C. A x) - B)" + "\A B C. (\x\C. A - B x) = (A - (\x\C. B x))" + "\A B. (UN x: \A. B x) = (\y\A. UN x:y. B x)" + "\A B C. (UN z: UNION A B. C z) = (\x\A. UN z: B(x). C z)" + "\A B f. (\x\f`A. B x) = (\a\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))" + "\A B C. (\x\C. A x \ B) = (if C={} then UNIV else (\x\C. A x) \B)" + "\A B C. (\x\C. A \ B x) = (if C={} then UNIV else A \(\x\C. B x))" + "\A B C. (\x\C. A x - B) = (if C={} then UNIV else (\x\C. A x) - B)" + "\A B C. (\x\C. A - B x) = (if C={} then UNIV else A - (\x\C. B x))" + "\a B C. (\x\C. insert a (B x)) = insert a (\x\C. B x)" + "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)" + "\A B C. (\x\C. A \ B x) = (A \ (\x\C. B x))" + "\A B. (INT x: \A. B x) = (\y\A. INT x:y. B x)" + "\A B C. (INT z: UNION A B. C z) = (\x\A. INT z: B(x). C z)" + "\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)" + "\A P Q. (\x\A. P x | Q) = ((\x\A. P x) | Q)" + "\A P Q. (\x\A. P | Q x) = (P | (\x\A. Q x))" + "\A P Q. (\x\A. P --> Q x) = (P --> (\x\A. Q x))" + "\A P Q. (\x\A. P x --> Q) = ((\x\A. P x) --> Q)" + "\P. (\ x\{}. P x) = True" + "\P. (\ x\UNIV. P x) = (ALL x. P x)" + "\a B P. (\ x\insert a B. P x) = (P a & (\ x\B. P x))" + "\A P. (\ x\\A. P x) = (\y\A. \ x\y. P x)" + "\A B P. (\ x\ UNION A B. P x) = (\a\A. \ x\ B a. P x)" + "\P Q. (\ x\Collect Q. P x) = (ALL x. Q x --> P x)" + "\A P f. (\ x\f`A. P x) = (\x\A. P (f x))" + "\A P. (~(\x\A. P x)) = (\x\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)" + "\A P Q. (\x\A. P x & Q) = ((\x\A. P x) & Q)" + "\A P Q. (\x\A. P & Q x) = (P & (\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:\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) = (\x\A. P (f x))" + "\A P. (~(\x\A. P x)) = (\x\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)" + "\a B C. insert a (\x\C. B x) = (if C={} then {a} else (\x\C. insert a (B x)))" + "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))" + "\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))" + "\A B C. ((\x\C. A x) \B) = (\x\C. A x \ B)" + "\A B C. (A \(\x\C. B x)) = (\x\C. A \ B x)" + "\A B C. ((\x\C. A x) - B) = (\x\C. A x - B)" + "\A B C. (A - (\x\C. B x)) = (\x\C. A - B x)" + "\A B. (\y\A. UN x:y. B x) = (UN x: \A. B x)" + "\A B C. (\x\A. UN z: B(x). C z) = (UN z: UNION A B. C z)" + "\A B f. (\a\A. B (f a)) = (\x\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)" + "\A B C. (\x\C. A x) \B = (if C={} then B else (\x\C. A x \ B))" + "\A B C. A \(\x\C. B x) = (if C={} then A else (\x\C. A \ B x))" + "\A B C. (\x\C. A x) - B = (if C={} then UNIV - B else (\x\C. A x - B))" + "\A B C. A - (\x\C. B x) = (if C={} then A else (\x\C. A - B x))" + "\a B C. insert a (\x\C. B x) = (\x\C. insert a (B x))" + "\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)" + "\A B C. A \ (\x\C. B x) = (\x\C. A \ B x)" + "\A B. (\y\A. INT x:y. B x) = (INT x: \A. B x)" + "\A B C. (\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)" by auto diff -r fad7758421bf -r 1162191cb57c src/HOL/Import/hol4rews.ML --- 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 = diff -r fad7758421bf -r 1162191cb57c src/HOL/IsaMakefile --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Library/Option_ord.thy --- 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" diff -r fad7758421bf -r 1162191cb57c src/HOL/Library/Quickcheck_Types.thy --- 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" diff -r fad7758421bf -r 1162191cb57c src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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) => diff -r fad7758421bf -r 1162191cb57c src/HOL/Orderings.thy --- 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 \ x" +begin -class top = preorder + +lemma bot_unique: + "a \ bot \ a = bot" + by (auto simp add: intro: antisym) + +lemma bot_less: + "a \ bot \ bot < a" + by (auto simp add: less_le_not_le intro!: antisym) + +end + +class top = order + fixes top :: 'a assumes top_greatest [simp]: "x \ top" +begin + +lemma top_unique: + "top \ a \ a = top" + by (auto simp add: intro: antisym) + +lemma less_top: + "a \ top \ a < top" + by (auto simp add: less_le_not_le intro!: antisym) + +end subsection {* Dense orders *} diff -r fad7758421bf -r 1162191cb57c src/HOL/Quotient_Examples/Cset.thy --- /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 \ 'a set \ bool" +where [simp]: "set_eq \ 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 \) (op \)" + "(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 \) (op \)" + "(set_eq ===> set_eq ===> op =) (op \) (op \)" + "(set_eq ===> set_eq ===> set_eq) (op \) (op \)" + "(set_eq ===> set_eq ===> set_eq) (op \) (op \)" + "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 \" +quotient_definition "Set :: ('a => bool) => 'a Cset.set" +is Collect +quotient_definition is_empty where "is_empty :: 'a Cset.set \ bool" +is More_Set.is_empty +quotient_definition insert where "insert :: 'a \ 'a Cset.set \ 'a Cset.set" +is Set.insert +quotient_definition remove where "remove :: 'a \ 'a Cset.set \ 'a Cset.set" +is More_Set.remove +quotient_definition map where "map :: ('a \ 'b) \ 'a Cset.set \ 'b Cset.set" +is image +quotient_definition filter where "filter :: ('a \ bool) \ 'a Cset.set \ 'a Cset.set" +is More_Set.project +quotient_definition "forall :: 'a Cset.set \ ('a \ bool) \ bool" +is Ball +quotient_definition "exists :: 'a Cset.set \ ('a \ bool) \ bool" +is Bex +quotient_definition card where "card :: 'a Cset.set \ 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 \ 'a Cset.set \ bool" +is "op \ :: 'a set \ 'a set \ bool" +quotient_definition psubset where "psubset :: 'a Cset.set \ 'a Cset.set \ bool" +is "op \ :: 'a set \ 'a set \ bool" +quotient_definition inter where "inter :: 'a Cset.set \ 'a Cset.set \ 'a Cset.set" +is "op \ :: 'a set \ 'a set \ 'a set" +quotient_definition union where "union :: 'a Cset.set \ 'a Cset.set \ 'a Cset.set" +is "op \ :: 'a set \ 'a set \ '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 \ 'a Cset.set" +is "uminus_class.uminus :: 'a set \ 'a set" +quotient_definition minus where "minus :: 'a Cset.set \ 'a Cset.set \ 'a Cset.set" +is "(op -) :: 'a set \ 'a set \ 'a set" +quotient_definition Inf where "Inf :: 'a Cset.set set \ 'a Cset.set" +is "Inf_class.Inf :: 'a set set \ 'a set" +quotient_definition Sup where "Sup :: 'a Cset.set set \ 'a Cset.set" +is "Sup_class.Sup :: 'a set set \ 'a set" + + +context complete_lattice +begin + +(* FIXME: Would like to use + +quotient_definition "Infimum :: 'a Cset.set \ 'a" +is "Inf" + +but it fails, presumably because @{term "Inf"} is a Free. +*) + +definition Infimum :: "'a Cset.set \ 'a" where + [simp]: "Infimum A = Inf (\x. member x A)" + +definition Supremum :: "'a Cset.set \ 'a" where + [simp]: "Supremum A = Sup (\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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Quotient_Examples/List_Cset.thy --- /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 \ '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) \ List.member xs x" + "member x (coset xs) \ \ 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\typerep list \ (unit \ Code_Evaluation.term) + \ 'a Cset.set \ (unit \ Code_Evaluation.term)" where + [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\} xs" + +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) + +instantiation Cset.set :: (random) random +begin + +definition + "Quickcheck.random i = Quickcheck.random i \\ (\xs. Pair (setify xs))" + +instance .. + +end + +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) + +subsection {* Basic operations *} + +lemma is_empty_set [code]: + "Cset.is_empty (Cset.set xs) \ 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 \ 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 \ 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 \ Cset.forall A (\x. member x B)" +by descending blast + +lemma subset_subset_eq [code]: + "Cset.psubset A B \ Cset.subset A B \ \ Cset.subset B A" +by descending blast + +instantiation Cset.set :: (type) equal +begin + +definition [code]: + "HOL.equal A B \ Cset.subset A B \ 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 \ True" + by (fact equal_refl) + + +subsection {* Functorial operations *} + +lemma inter_project [code]: + "Cset.inter A (Cset.set xs) = Cset.set (List.filter (\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 (\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 (\x. \ member x A) xs)" +unfolding coset_def +apply (lifting union_set_foldr) +by descending auto + +end \ No newline at end of file diff -r fad7758421bf -r 1162191cb57c src/HOL/Quotient_Examples/ROOT.ML --- 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"]; diff -r fad7758421bf -r 1162191cb57c src/HOL/Set.thy --- 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: + "(\x\A. P x \ Q x) \ ((\x\A. P x) \ (\x\A. Q x))" + by blast + +lemma bex_disj_distrib: + "(\x\A. P x \ Q x) \ ((\x\A. P x) \ (\x\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 \ -A) = (c \ A)" - by (simp add: mem_def fun_Compl_def bool_Compl_def) + by (simp add: mem_def fun_Compl_def) lemma ComplI [intro!]: "(c \ A ==> False) ==> c \ -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 \ B = {x. x \ A \ x \ 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 \ B = {x. x \ A \ x \ 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/TPTP/ATP_Export.thy --- /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 diff -r fad7758421bf -r 1162191cb57c src/HOL/TPTP/CASC_Setup.thy --- /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 \ bool" + is_rat :: "'a \ bool" + +overloading rat_is_int \ "is_int :: rat \ bool" +begin + definition "rat_is_int (q\rat) \ (\n\int. q = of_int n)" +end + +overloading real_is_int \ "is_int :: real \ bool" +begin + definition "real_is_int (x\real) \ x \ \" +end + +overloading real_is_rat \ "is_rat :: real \ bool" +begin + definition "real_is_rat (x\real) \ x \ \" +end + +consts + to_int :: "'a \ int" + to_rat :: "'a \ rat" + to_real :: "'a \ real" + +overloading rat_to_int \ "to_int :: rat \ int" +begin + definition "rat_to_int (q\rat) = floor q" +end + +overloading real_to_int \ "to_int :: real \ int" +begin + definition "real_to_int (x\real) = floor x" +end + +overloading int_to_rat \ "to_rat :: int \ rat" +begin + definition "int_to_rat (n\int) = (of_int n\rat)" +end + +overloading real_to_rat \ "to_rat :: real \ rat" +begin + definition "real_to_rat (x\real) = (inv real x\rat)" +end + +overloading int_to_real \ "to_real :: int \ real" +begin + definition "int_to_real (n\int) = real n" +end + +overloading rat_to_real \ "to_real :: rat \ real" +begin + definition "rat_to_real (x\rat) = (of_rat x\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\int))" +by (metis int_to_rat_def rat_is_int_def) + +lemma to_real_is_int [intro, simp]: "is_int (to_real (n\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\rat))" +by (metis Rats_of_rat rat_to_real_def real_is_rat_def) + +lemma inj_of_rat [intro, simp]: "inj (of_rat\rat\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 diff -r fad7758421bf -r 1162191cb57c src/HOL/TPTP/ROOT.ML --- /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"; diff -r fad7758421bf -r 1162191cb57c src/HOL/TPTP/atp_export.ML --- /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; diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/ATP/atp_proof.ML --- 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 \ diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/ATP/atp_translate.ML --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/ATP/atp_util.ML --- 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) = diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Meson/meson.ML --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Metis/metis_tactics.ML --- 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" diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Metis/metis_translate.ML --- 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)) diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Nitpick/lib/Tools/nitrox --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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) diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Nitpick/nitpick_util.ML --- 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; diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Nitpick/nitrox.ML --- 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\8"), + [("card iota", "1\100"), + ("card", "1\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 diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/SMT/smt_translate.ML --- 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) diff -r fad7758421bf -r 1162191cb57c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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, diff -r fad7758421bf -r 1162191cb57c src/HOL/ex/ATP_Export.thy --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/ex/CASC_Setup.thy --- 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 diff -r fad7758421bf -r 1162191cb57c src/HOL/ex/Quickcheck_Examples.thy --- 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" diff -r fad7758421bf -r 1162191cb57c src/HOL/ex/ROOT.ML --- 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"; diff -r fad7758421bf -r 1162191cb57c src/HOL/ex/atp_export.ML --- 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;