--- a/CONTRIBUTORS Wed Feb 11 15:05:26 2009 +0100
+++ b/CONTRIBUTORS Wed Feb 11 15:05:40 2009 +0100
@@ -7,6 +7,9 @@
Contributions to this Isabelle version
--------------------------------------
+* February 2008: Timothy Bourke, NICTA
+ "solves" criterion for find_theorems and auto_solve option
+
* December 2008: Clemens Ballarin, TUM
New locale implementation.
--- a/NEWS Wed Feb 11 15:05:26 2009 +0100
+++ b/NEWS Wed Feb 11 15:05:40 2009 +0100
@@ -183,6 +183,16 @@
* The 'axiomatization' command now only works within a global theory
context. INCOMPATIBILITY.
+* New find_theorems criterion "solves" matching theorems that
+ directly solve the current goal. Try "find_theorems solves".
+
+* Added an auto solve option, which can be enabled through the
+ ProofGeneral Isabelle settings menu (disabled by default).
+
+ When enabled, find_theorems solves is called whenever a new lemma
+ is stated. Any theorems that could solve the lemma directly are
+ listed underneath the goal.
+
*** Document preparation ***
--- a/src/HOL/HOL.thy Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/HOL.thy Wed Feb 11 15:05:40 2009 +0100
@@ -932,7 +932,7 @@
structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
-structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP");
+structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP");
*}
text {*ResBlacklist holds theorems blacklisted to sledgehammer.
@@ -1701,6 +1701,29 @@
*}
+subsection {* Nitpick theorem store *}
+
+ML {*
+structure Nitpick_Const_Simp_Thms = NamedThmsFun
+(
+ val name = "nitpick_const_simp"
+ val description = "equational specification of constants as needed by Nitpick"
+)
+structure Nitpick_Const_Psimp_Thms = NamedThmsFun
+(
+ val name = "nitpick_const_psimp"
+ val description = "partial equational specification of constants as needed by Nitpick"
+)
+structure Nitpick_Ind_Intro_Thms = NamedThmsFun
+(
+ val name = "nitpick_ind_intro"
+ val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
+)
+*}
+setup {* Nitpick_Const_Simp_Thms.setup
+ #> Nitpick_Const_Psimp_Thms.setup
+ #> Nitpick_Ind_Intro_Thms.setup *}
+
subsection {* Legacy tactics and ML bindings *}
ML {*
--- a/src/HOL/IsaMakefile Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 11 15:05:40 2009 +0100
@@ -285,7 +285,6 @@
Taylor.thy \
Transcendental.thy \
GCD.thy \
- Order_Relation.thy \
Parity.thy \
Lubs.thy \
Polynomial.thy \
@@ -322,7 +321,7 @@
Library/Multiset.thy Library/Permutation.thy \
Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \
Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
- Library/README.html Library/Continuity.thy \
+ Library/README.html Library/Continuity.thy Library/Order_Relation.thy \
Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
Library/Library/ROOT.ML Library/Library/document/root.tex \
Library/Library/document/root.bib Library/While_Combinator.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Order_Relation.thy Wed Feb 11 15:05:40 2009 +0100
@@ -0,0 +1,101 @@
+(* ID : $Id$
+ Author : Tobias Nipkow
+*)
+
+header {* Orders as Relations *}
+
+theory Order_Relation
+imports Main
+begin
+
+subsection{* Orders on a set *}
+
+definition "preorder_on A r \<equiv> refl A r \<and> trans r"
+
+definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
+
+definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
+
+definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
+
+definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
+
+lemmas order_on_defs =
+ preorder_on_def partial_order_on_def linear_order_on_def
+ strict_linear_order_on_def well_order_on_def
+
+
+lemma preorder_on_empty[simp]: "preorder_on {} {}"
+by(simp add:preorder_on_def trans_def)
+
+lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
+by(simp add:partial_order_on_def)
+
+lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
+by(simp add:linear_order_on_def)
+
+lemma well_order_on_empty[simp]: "well_order_on {} {}"
+by(simp add:well_order_on_def)
+
+
+lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
+by (simp add:preorder_on_def)
+
+lemma partial_order_on_converse[simp]:
+ "partial_order_on A (r^-1) = partial_order_on A r"
+by (simp add: partial_order_on_def)
+
+lemma linear_order_on_converse[simp]:
+ "linear_order_on A (r^-1) = linear_order_on A r"
+by (simp add: linear_order_on_def)
+
+
+lemma strict_linear_order_on_diff_Id:
+ "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
+by(simp add: order_on_defs trans_diff_Id)
+
+
+subsection{* Orders on the field *}
+
+abbreviation "Refl r \<equiv> refl (Field r) r"
+
+abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
+
+abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
+
+abbreviation "Total r \<equiv> total_on (Field r) r"
+
+abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
+
+abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
+
+
+lemma subset_Image_Image_iff:
+ "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
+ r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
+apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
+apply metis
+by(metis trans_def)
+
+lemma subset_Image1_Image1_iff:
+ "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
+by(simp add:subset_Image_Image_iff)
+
+lemma Refl_antisym_eq_Image1_Image1_iff:
+ "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
+by(simp add: expand_set_eq antisym_def refl_def) metis
+
+lemma Partial_order_eq_Image1_Image1_iff:
+ "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
+by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
+
+
+subsection{* Orders on a type *}
+
+abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
+
+abbreviation "linear_order \<equiv> linear_order_on UNIV"
+
+abbreviation "well_order r \<equiv> well_order_on UNIV"
+
+end
--- a/src/HOL/Order_Relation.thy Wed Feb 11 15:05:26 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(* ID : $Id$
- Author : Tobias Nipkow
-*)
-
-header {* Orders as Relations *}
-
-theory Order_Relation
-imports Plain "~~/src/HOL/Hilbert_Choice" "~~/src/HOL/ATP_Linkup"
-begin
-
-text{* This prelude could be moved to theory Relation: *}
-
-definition "irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
-
-definition "total_on A r \<equiv> \<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
-
-abbreviation "total \<equiv> total_on UNIV"
-
-
-lemma total_on_empty[simp]: "total_on {} r"
-by(simp add:total_on_def)
-
-lemma refl_on_converse[simp]: "refl A (r^-1) = refl A r"
-by(auto simp add:refl_def)
-
-lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
-by (auto simp: total_on_def)
-
-lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
-by(simp add:irrefl_def)
-
-declare [[simp_depth_limit = 2]]
-lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
-by(simp add: antisym_def trans_def) blast
-declare [[simp_depth_limit = 50]]
-
-lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
-by(simp add: total_on_def)
-
-
-subsection{* Orders on a set *}
-
-definition "preorder_on A r \<equiv> refl A r \<and> trans r"
-
-definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
-
-definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
-
-definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
-
-definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
-
-lemmas order_on_defs =
- preorder_on_def partial_order_on_def linear_order_on_def
- strict_linear_order_on_def well_order_on_def
-
-
-lemma preorder_on_empty[simp]: "preorder_on {} {}"
-by(simp add:preorder_on_def trans_def)
-
-lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
-by(simp add:partial_order_on_def)
-
-lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
-by(simp add:linear_order_on_def)
-
-lemma well_order_on_empty[simp]: "well_order_on {} {}"
-by(simp add:well_order_on_def)
-
-
-lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
-by (simp add:preorder_on_def)
-
-lemma partial_order_on_converse[simp]:
- "partial_order_on A (r^-1) = partial_order_on A r"
-by (simp add: partial_order_on_def)
-
-lemma linear_order_on_converse[simp]:
- "linear_order_on A (r^-1) = linear_order_on A r"
-by (simp add: linear_order_on_def)
-
-
-lemma strict_linear_order_on_diff_Id:
- "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
-by(simp add: order_on_defs trans_diff_Id)
-
-
-subsection{* Orders on the field *}
-
-abbreviation "Refl r \<equiv> refl (Field r) r"
-
-abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
-
-abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
-
-abbreviation "Total r \<equiv> total_on (Field r) r"
-
-abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
-
-abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
-
-
-lemma subset_Image_Image_iff:
- "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
- r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
-apply metis
-by(metis trans_def)
-
-lemma subset_Image1_Image1_iff:
- "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
-by(simp add:subset_Image_Image_iff)
-
-lemma Refl_antisym_eq_Image1_Image1_iff:
- "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
-by(simp add: expand_set_eq antisym_def refl_def) metis
-
-lemma Partial_order_eq_Image1_Image1_iff:
- "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
-by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
-
-
-subsection{* Orders on a type *}
-
-abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
-
-abbreviation "linear_order \<equiv> linear_order_on UNIV"
-
-abbreviation "well_order r \<equiv> well_order_on UNIV"
-
-end
--- a/src/HOL/Relation.thy Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Relation.thy Wed Feb 11 15:05:40 2009 +0100
@@ -70,6 +70,16 @@
"trans r == (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
definition
+irrefl :: "('a * 'a) set => bool" where
+"irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
+
+definition
+total_on :: "'a set => ('a * 'a) set => bool" where
+"total_on A r \<equiv> \<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
+
+abbreviation "total \<equiv> total_on UNIV"
+
+definition
single_valued :: "('a * 'b) set => bool" where
"single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)"
@@ -268,6 +278,21 @@
lemma trans_diag [simp]: "trans (diag A)"
by (fast intro: transI elim: transD)
+lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
+unfolding antisym_def trans_def by blast
+
+subsection {* Irreflexivity *}
+
+lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
+by(simp add:irrefl_def)
+
+subsection {* Totality *}
+
+lemma total_on_empty[simp]: "total_on {} r"
+by(simp add:total_on_def)
+
+lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
+by(simp add: total_on_def)
subsection {* Converse *}
@@ -330,6 +355,9 @@
lemma sym_Int_converse: "sym (r \<inter> r^-1)"
by (unfold sym_def) blast
+lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
+by (auto simp: total_on_def)
+
subsection {* Domain *}
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Feb 11 15:05:40 2009 +0100
@@ -333,9 +333,10 @@
val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
(fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
(DatatypeProp.make_cases new_type_names descr sorts thy2)
-
in
thy2
+ |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
+ o Context.Theory
|> parent_path flat_names
|> store_thmss "cases" new_type_names case_thms
|-> (fn thmss => pair (thmss, case_names))
--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Feb 11 15:05:40 2009 +0100
@@ -71,8 +71,9 @@
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
- ||> fold_option (snd oo addsmps I "simps" []) trsimps
+ |> addsmps (NameSpace.qualified "partial") "psimps"
+ [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
+ ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
||>> note_theorem ((qualify "pinduct",
[Attrib.internal (K (RuleCases.case_names cnames)),
Attrib.internal (K (RuleCases.consumes 1)),
@@ -127,7 +128,8 @@
val tinduct = map remove_domain_condition pinducts
val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
- val allatts = if has_guards then [] else [Code.add_default_eqn_attrib]
+ val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
+ [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
val qualify = NameSpace.qualified defname;
in
--- a/src/HOL/Tools/function_package/size.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Wed Feb 11 15:05:40 2009 +0100
@@ -209,8 +209,9 @@
val ([size_thms], thy'') = PureThy.add_thmss
[((Binding.name "size", size_eqns),
- [Simplifier.simp_add, Thm.declaration_attribute
- (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ Thm.declaration_attribute
+ (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
in
SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
@@ -238,4 +239,4 @@
val setup = DatatypePackage.interpretation add_size_thms;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Tools/inductive_package.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Feb 11 15:05:40 2009 +0100
@@ -691,7 +691,8 @@
ctxt |>
LocalTheory.notes kind
(map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
- [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
+ [Attrib.internal (K (ContextRules.intro_query NONE)),
+ Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>
--- a/src/HOL/Tools/old_primrec_package.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML Wed Feb 11 15:05:40 2009 +0100
@@ -283,7 +283,8 @@
val simps'' = maps snd simps';
in
thy''
- |> note (("simps", [Simplifier.simp_add, Code.add_default_eqn_attribute]), simps'')
+ |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ Code.add_default_eqn_attribute]), simps'')
|> snd
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd
--- a/src/HOL/Tools/primrec_package.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Feb 11 15:05:40 2009 +0100
@@ -251,7 +251,8 @@
val qualify = Binding.qualify prefix;
val spec' = (map o apfst)
(fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
- val simp_att = (Attrib.internal o K) Simplifier.simp_add;
+ val simp_atts = map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
in
lthy
|> set_group ? LocalTheory.set_group (serial_string ())
@@ -259,7 +260,7 @@
|-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
|-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
|-> (fn simps' => LocalTheory.note Thm.theoremK
- ((qualify (Binding.name "simps"), [simp_att]), maps snd simps'))
+ ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
|>> snd
end handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
--- a/src/HOL/Tools/recdef_package.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Wed Feb 11 15:05:40 2009 +0100
@@ -207,7 +207,8 @@
tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
congs wfs name R eqs;
val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
- val simp_att = if null tcs then [Simplifier.simp_add, Code.add_default_eqn_attribute] else [];
+ val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
+ Code.add_default_eqn_attribute] else [];
val ((simps' :: rules', [induct']), thy) =
thy
--- a/src/HOL/Tools/record_package.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Wed Feb 11 15:05:40 2009 +0100
@@ -2188,7 +2188,8 @@
val final_thy =
thms_thy
|> (snd oo PureThy.add_thmss)
- [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
+ [((Binding.name "simps", sel_upd_simps),
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
((Binding.name "iffs", iffs), [iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
--- a/src/HOL/Tools/sat_solver.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML Wed Feb 11 15:05:40 2009 +0100
@@ -569,9 +569,10 @@
fun minisat_with_proofs fm =
let
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
- val proofpath = File.tmp_path (Path.explode "result.prf")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
+ val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
@@ -754,8 +755,9 @@
fun minisat fm =
let
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
@@ -916,8 +918,9 @@
(getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
(* both versions of zChaff appear to have the same interface, so we do *)
(* not actually need to distinguish between them in the following code *)
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
@@ -941,8 +944,9 @@
fun berkmin fm =
let
val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!")
@@ -966,8 +970,9 @@
fun jerusat fm =
let
val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
- val inpath = File.tmp_path (Path.explode "isabelle.cnf")
- val outpath = File.tmp_path (Path.explode "result")
+ val serial_str = serial_string ()
+ val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
+ val outpath = File.tmp_path (Path.explode ("result" ^ serial_str))
val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
--- a/src/Pure/General/seq.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/General/seq.ML Wed Feb 11 15:05:40 2009 +0100
@@ -19,6 +19,7 @@
val hd: 'a seq -> 'a
val tl: 'a seq -> 'a seq
val chop: int -> 'a seq -> 'a list * 'a seq
+ val take: int -> 'a seq -> 'a seq
val list_of: 'a seq -> 'a list
val of_list: 'a list -> 'a seq
val append: 'a seq -> 'a seq -> 'a seq
@@ -94,6 +95,12 @@
NONE => ([], xq)
| SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq'));
+(* truncate the sequence after n elements *)
+fun take n s = let
+ fun f 0 _ () = NONE
+ | f n ss () = Option.map (apsnd (make o f (n - 1))) (pull ss);
+ in make (f n s) end;
+
(*conversion from sequence to list*)
fun list_of xq =
(case pull xq of
--- a/src/Pure/IsaMakefile Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/IsaMakefile Wed Feb 11 15:05:40 2009 +0100
@@ -85,7 +85,7 @@
pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML \
subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML \
theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML \
- ../Tools/quickcheck.ML
+ ../Tools/quickcheck.ML ../Tools/auto_solve.ML
@./mk
--- a/src/Pure/Isar/find_theorems.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/Isar/find_theorems.ML Wed Feb 11 15:05:40 2009 +0100
@@ -7,9 +7,16 @@
signature FIND_THEOREMS =
sig
val limit: int ref
+ val tac_limit: int ref
+
datatype 'term criterion =
- Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
- val print_theorems: Proof.context -> term option -> int option -> bool ->
+ Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
+ Pattern of 'term
+
+ val find_theorems: Proof.context -> thm option -> bool ->
+ (bool * string criterion) list -> (Facts.ref * thm) list
+
+ val print_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> unit
end;
@@ -19,12 +26,14 @@
(** search criteria **)
datatype 'term criterion =
- Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term;
+ Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
+ Pattern of 'term;
fun read_criterion _ (Name name) = Name name
| read_criterion _ Intro = Intro
| read_criterion _ Elim = Elim
| read_criterion _ Dest = Dest
+ | read_criterion _ Solves = Solves
| read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str)
| read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str);
@@ -37,6 +46,7 @@
| Intro => Pretty.str (prfx "intro")
| Elim => Pretty.str (prfx "elim")
| Dest => Pretty.str (prfx "dest")
+ | Solves => Pretty.str (prfx "solves")
| Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
| Pattern pat => Pretty.enclose (prfx " \"") "\""
@@ -108,7 +118,7 @@
then SOME (0, 0) else NONE;
-(* filter intro/elim/dest rules *)
+(* filter intro/elim/dest/solves rules *)
fun filter_dest ctxt goal (_, thm) =
let
@@ -159,6 +169,20 @@
end
else NONE
+val tac_limit = ref 5;
+
+fun filter_solves ctxt goal = let
+ val baregoal = Logic.get_goal (prop_of goal) 1;
+
+ fun etacn thm i = Seq.take (!tac_limit) o etac thm i;
+ fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal
+ else (etacn thm THEN_ALL_NEW
+ (Goal.norm_hhf_tac THEN'
+ Method.assumption_tac ctxt)) 1 goal;
+ in
+ fn (_, thm) => if (is_some o Seq.pull o try_thm) thm
+ then SOME (Thm.nprems_of thm, 0) else NONE
+ end;
(* filter_simp *)
@@ -176,26 +200,23 @@
(* filter_pattern *)
-fun get_names (_, thm) =
- fold_aterms (fn Const (c, _) => insert (op =) c | Free (x, _) => insert (op =) x | _ => I)
- (Thm.full_prop_of thm) [];
-
-fun add_pat_names (t, cs) =
- case strip_comb t of
- (Const (c, _), args) => foldl add_pat_names (insert (op =) c cs) args
- | (Free (c, _), args) => foldl add_pat_names (insert (op =) c cs) args
- | (Abs (_, _, t), _) => add_pat_names (t, cs)
- | _ => cs;
- (* Only include constants and frees that cannot be thrown away.
- for example, from "(% x y z. y + 1) 7 8 9" give [1].
- The result [1, 8] would be more accurate, but only a
- sound approximation is required and variables must
- be ignored: e.g. "_ 7 8 9". *)
+fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []);
+fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
+ (* Including all constants and frees is only sound because
+ matching uses higher-order patterns. If full matching
+ were used, then constants that may be subject to
+ beta-reduction after substitution of frees should
+ not be included for LHS set because they could be
+ thrown away by the substituted function.
+ e.g. for (?F 1 2) do not include 1 or 2, if it were
+ possible for ?F to be (% x y. 3)
+ The largest possible set should always be included on
+ the RHS. *)
fun filter_pattern ctxt pat = let
- val pat_consts = add_pat_names (pat, []);
+ val pat_consts = get_names pat;
- fun check (t, NONE) = check (t, SOME (get_names t))
+ fun check (t, NONE) = check (t, SOME (get_thm_names t))
| check ((_, thm), c as SOME thm_consts) =
(if pat_consts subset_string thm_consts
andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt)
@@ -210,13 +231,21 @@
fun err_no_goal c =
error ("Current goal required for " ^ c ^ " search criterion");
+val fix_goal = Thm.prop_of;
+val fix_goalo = Option.map fix_goal;
+
fun filter_crit _ _ (Name name) = apfst (filter_name name)
| filter_crit _ NONE Intro = err_no_goal "intro"
| filter_crit _ NONE Elim = err_no_goal "elim"
| filter_crit _ NONE Dest = err_no_goal "dest"
- | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt goal)
- | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt goal)
- | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt goal)
+ | filter_crit _ NONE Solves = err_no_goal "solves"
+ | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt
+ (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt
+ (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt
+ (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
@@ -314,11 +343,14 @@
val limit = ref 40;
-fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun find_theorems ctxt opt_goal rem_dups raw_criteria =
let
- val start = start_timing ();
+ val add_prems = Seq.hd o (TRY (Method.insert_tac
+ (Assumption.prems_of ctxt) 1));
+ val opt_goal' = Option.map add_prems opt_goal;
+
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val filters = map (filter_criterion ctxt opt_goal) criteria;
+ val filters = map (filter_criterion ctxt opt_goal') criteria;
val raw_matches = all_filters filters (all_facts_of ctxt);
@@ -326,6 +358,13 @@
if rem_dups
then rem_thm_dups (nicer_shortest ctxt) raw_matches
else raw_matches;
+ in matches end;
+
+fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let
+ val start = start_timing ();
+
+ val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
+ val matches = find_theorems ctxt opt_goal rem_dups raw_criteria;
val len = length matches;
val lim = the_default (! limit) opt_limit;
@@ -334,21 +373,17 @@
val end_msg = " in " ^
(List.nth (String.tokens Char.isSpace (end_timing start), 3))
^ " secs"
-
- fun prt_fact (thmref, thm) = Pretty.block
- [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- ProofContext.pretty_thm ctxt thm];
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
- :: Pretty.str "" ::
+ :: Pretty.str "" ::
(if null thms then [Pretty.str ("nothing found" ^ end_msg)]
else
[Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
(if len <= lim then ""
else " (" ^ string_of_int lim ^ " displayed)")
^ end_msg ^ ":"), Pretty.str ""] @
- map prt_fact thms)
+ map Display.pretty_fact thms)
|> Pretty.chunks |> Pretty.writeln
- end;
+ end
end;
--- a/src/Pure/Isar/isar_cmd.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Feb 11 15:05:40 2009 +0100
@@ -412,7 +412,7 @@
let
val proof_state = Toplevel.enter_proof_body state;
val ctxt = Proof.context_of proof_state;
- val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
+ val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
--- a/src/Pure/Isar/isar_syn.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Feb 11 15:05:40 2009 +0100
@@ -860,6 +860,7 @@
P.reserved "intro" >> K FindTheorems.Intro ||
P.reserved "elim" >> K FindTheorems.Elim ||
P.reserved "dest" >> K FindTheorems.Dest ||
+ P.reserved "solves" >> K FindTheorems.Solves ||
P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
P.term >> FindTheorems.Pattern;
--- a/src/Pure/Isar/method.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/Isar/method.ML Wed Feb 11 15:05:40 2009 +0100
@@ -38,6 +38,7 @@
val atomize: bool -> method
val this: method
val fact: thm list -> Proof.context -> method
+ val assumption_tac: Proof.context -> int -> tactic
val assumption: Proof.context -> method
val close: bool -> Proof.context -> method
val trace: Proof.context -> thm list -> unit
@@ -222,22 +223,22 @@
if cond (Logic.strip_assums_concl prop)
then Tactic.rtac rule i else no_tac);
-fun assm_tac ctxt =
+in
+
+fun assumption_tac ctxt =
assume_tac APPEND'
Goal.assume_rule_tac ctxt APPEND'
cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
cond_rtac (can Logic.dest_term) Drule.termI;
-in
-
fun assumption ctxt = METHOD (HEADGOAL o
- (fn [] => assm_tac ctxt
+ (fn [] => assumption_tac ctxt
| [fact] => solve_tac [fact]
| _ => K no_tac));
fun close immed ctxt = METHOD (K
(FILTER Thm.no_prems
- ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
+ ((if immed then ALLGOALS (assumption_tac ctxt) else all_tac) THEN flexflex_tac)));
end;
--- a/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/ProofGeneral/ROOT.ML Wed Feb 11 15:05:40 2009 +0100
@@ -17,7 +17,8 @@
(use
|> setmp Proofterm.proofs 1
|> setmp quick_and_dirty true
- |> setmp auto_quickcheck true) "preferences.ML";
+ |> setmp auto_quickcheck true
+ |> setmp auto_solve false) "preferences.ML";
use "pgip_parser.ML";
--- a/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Wed Feb 11 15:05:40 2009 +0100
@@ -151,6 +151,12 @@
nat_pref Quickcheck.auto_time_limit
"auto-quickcheck-time-limit"
"Time limit for automatic quickcheck (in milliseconds).",
+ bool_pref AutoSolve.auto
+ "auto-solve"
+ "Try to solve newly declared lemmas with existing theorems.",
+ nat_pref AutoSolve.auto_time_limit
+ "auto-solve-time-limit"
+ "Time limit for seeking automatic solutions (in milliseconds).",
thm_deps_pref];
val proof_preferences =
--- a/src/Pure/Tools/ROOT.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/Tools/ROOT.ML Wed Feb 11 15:05:40 2009 +0100
@@ -9,5 +9,6 @@
(*basic XML support*)
use "xml_syntax.ML";
-(*quickcheck needed here because of pg preferences*)
-use "../../Tools/quickcheck.ML"
+(*quickcheck/autosolve needed here because of pg preferences*)
+use "../../Tools/quickcheck.ML";
+use "../../Tools/auto_solve.ML";
--- a/src/Pure/display.ML Wed Feb 11 15:05:26 2009 +0100
+++ b/src/Pure/display.ML Wed Feb 11 15:05:40 2009 +0100
@@ -20,6 +20,7 @@
val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
val pretty_thm: thm -> Pretty.T
val string_of_thm: thm -> string
+ val pretty_fact: Facts.ref * thm -> Pretty.T
val pretty_thms: thm list -> Pretty.T
val pretty_thm_sg: theory -> thm -> Pretty.T
val pretty_thms_sg: theory -> thm list -> Pretty.T
@@ -92,6 +93,10 @@
val string_of_thm = Pretty.string_of o pretty_thm;
+fun pretty_fact (thmref, thm) = Pretty.block
+ [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+ pretty_thm thm];
+
fun pretty_thms [th] = pretty_thm th
| pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_solve.ML Wed Feb 11 15:05:40 2009 +0100
@@ -0,0 +1,93 @@
+(* Title: auto_solve.ML
+ Author: Timothy Bourke and Gerwin Klein, NICTA
+
+ Check whether a newly stated theorem can be solved directly
+ by an existing theorem. Duplicate lemmas can be detected in
+ this way.
+
+ The implemenation is based in part on Berghofer and
+ Haftmann's Pure/codegen.ML. It relies critically on
+ the FindTheorems solves feature.
+*)
+
+signature AUTO_SOLVE =
+sig
+ val auto : bool ref;
+ val auto_time_limit : int ref;
+
+ val seek_solution : bool -> Proof.state -> Proof.state;
+end;
+
+structure AutoSolve : AUTO_SOLVE =
+struct
+ structure FT = FindTheorems;
+
+ val auto = ref false;
+ val auto_time_limit = ref 5000;
+
+ fun seek_solution int state = let
+ val ctxt = Proof.context_of state;
+
+ fun conj_to_list [] = []
+ | conj_to_list (t::ts) =
+ (Conjunction.dest_conjunction t
+ |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
+ handle TERM _ => t::conj_to_list ts;
+
+ val crits = [(true, FT.Solves)];
+ fun find g = (NONE, FT.find_theorems ctxt g true crits);
+ fun find_cterm g = (SOME g, FT.find_theorems ctxt
+ (SOME (Goal.init g)) true crits);
+
+ fun prt_result (goal, results) = let
+ val msg = case goal of
+ NONE => "The current goal"
+ | SOME g => Syntax.string_of_term ctxt (term_of g);
+ in
+ Pretty.big_list (msg ^ " could be solved directly with:")
+ (map Display.pretty_fact results)
+ end;
+
+ fun seek_against_goal () = let
+ val goal = try Proof.get_goal state
+ |> Option.map (#2 o #2);
+
+ val goals = goal
+ |> Option.map (fn g => cprem_of g 1)
+ |> the_list
+ |> conj_to_list;
+
+ val rs = if length goals = 1
+ then [find goal]
+ else map find_cterm goals;
+ val frs = filter_out (null o snd) rs;
+
+ in if null frs then NONE else SOME frs end;
+
+ fun go () = let
+ val res = TimeLimit.timeLimit
+ (Time.fromMilliseconds (!auto_time_limit))
+ (try seek_against_goal) ();
+ in
+ case Option.join res of
+ NONE => state
+ | SOME results => (Proof.goal_message
+ (fn () => Pretty.chunks [Pretty.str "",
+ Pretty.markup Markup.hilite
+ (Library.separate (Pretty.brk 0)
+ (map prt_result results))])
+ state)
+ end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
+ in
+ if int andalso !auto andalso not (!Toplevel.quiet)
+ then go ()
+ else state
+ end;
+
+end;
+
+val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
+
+val auto_solve = AutoSolve.auto;
+val auto_solve_time_limit = AutoSolve.auto_time_limit;
+