--- a/src/HOL/IsaMakefile Wed May 12 23:53:54 2010 +0200
+++ b/src/HOL/IsaMakefile Wed May 12 23:53:55 2010 +0200
@@ -1249,7 +1249,8 @@
SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \
SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \
SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \
- SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
+ SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML \
+ SMT/Tools/smt_additional_facts.ML
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
--- a/src/HOL/SMT/SMT_Base.thy Wed May 12 23:53:54 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy Wed May 12 23:53:55 2010 +0200
@@ -8,6 +8,7 @@
imports Real "~~/src/HOL/Word/Word"
uses
"~~/src/Tools/cache_io.ML"
+ ("Tools/smt_additional_facts.ML")
("Tools/smt_normalize.ML")
("Tools/smt_monomorph.ML")
("Tools/smt_translate.ML")
@@ -130,6 +131,7 @@
section {* Setup *}
+use "Tools/smt_additional_facts.ML"
use "Tools/smt_normalize.ML"
use "Tools/smt_monomorph.ML"
use "Tools/smt_translate.ML"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/smt_additional_facts.ML Wed May 12 23:53:55 2010 +0200
@@ -0,0 +1,45 @@
+(* Title: HOL/SMT/Tools/smt_additional_facts.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Include additional facts.
+*)
+
+signature SMT_ADDITIONAL_FACTS =
+sig
+ val add_facts: thm list -> thm list
+end
+
+structure SMT_Additional_Facts: SMT_ADDITIONAL_FACTS =
+struct
+
+infix 2 ??
+fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms
+
+
+
+(* pairs *)
+
+val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
+
+val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
+val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
+
+val add_pair_rules = exists_pair_type ?? append pair_rules
+
+
+
+(* function update *)
+
+val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
+
+val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
+val exists_fun_upd = Term.exists_subterm is_fun_upd
+
+val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules
+
+
+(* include additional facts *)
+
+val add_facts = add_pair_rules #> add_fun_upd_rules
+
+end
--- a/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:54 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:55 2010 +0200
@@ -217,31 +217,6 @@
-(* include additional rules *)
-
-local
- val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
-
- val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
- val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
-
- val add_pair_rules =
- exists (exists_pair_type o Thm.prop_of) ?? append pair_rules
-
-
- val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
-
- val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
- val exists_fun_upd = Term.exists_subterm is_fun_upd
-
- val add_fun_upd_rules =
- exists (exists_fun_upd o Thm.prop_of) ?? append fun_upd_rules
-in
-val add_rules = add_pair_rules #> add_fun_upd_rules
-end
-
-
-
(* unfold definitions of specific constants *)
local
@@ -537,7 +512,6 @@
|> rewrite_bool_cases ctxt
|> normalize_numerals ctxt
|> nat_as_int ctxt
- |> add_rules
|> map (unfold_defs ctxt #> normalize_rule ctxt)
|> lift_lambdas ctxt
|> apsnd (explicit_application ctxt)
--- a/src/HOL/SMT/Tools/smt_solver.ML Wed May 12 23:53:54 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Wed May 12 23:53:55 2010 +0200
@@ -70,6 +70,7 @@
reconstruct: proof_data -> thm }
+
(* SMT options *)
val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
@@ -84,6 +85,7 @@
if Config.get ctxt trace then tracing (f x) else ()
+
(* SMT certificates *)
val (fixed_certificates, setup_fixed_certificates) =
@@ -102,6 +104,7 @@
else SOME (Cache_IO.make (Path.explode name)))
+
(* interface to external solvers *)
local
@@ -173,7 +176,8 @@
val tc = interface comments
val thy = ProofContext.theory_of ctxt
in
- SMT_Normalize.normalize ctxt prems
+ SMT_Additional_Facts.add_facts prems
+ |> SMT_Normalize.normalize ctxt
||> SMT_Translate.translate tc thy
||> apfst (run_solver ctxt command arguments)
||> reconstruct o make_proof_data ctxt
@@ -181,6 +185,7 @@
end
+
(* solver store *)
type solver = Proof.context -> thm list -> thm
@@ -202,6 +207,7 @@
fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i)))
+
(* selected solver *)
structure Selected_Solver = Generic_Data
@@ -229,6 +235,7 @@
in gen_solver name (raw_solver_of context name) end
+
(* SMT tactic *)
local
@@ -277,6 +284,7 @@
HEADGOAL (smt_tac ctxt (thms @ facts))))
+
(* setup *)
val setup =