# HG changeset patch
# User boehmes
# Date 1273701235 -7200
# Node ID e0d295cb8bfdfffff43f268df9a5bbf52a9a27fe
# Parent  0ab4217a07b1171173f5da689e400a544d880161
move the addition of extra facts into a separate module

diff -r 0ab4217a07b1 -r e0d295cb8bfd src/HOL/IsaMakefile
--- 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
 
 
diff -r 0ab4217a07b1 -r e0d295cb8bfd src/HOL/SMT/SMT_Base.thy
--- 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"
diff -r 0ab4217a07b1 -r e0d295cb8bfd src/HOL/SMT/Tools/smt_additional_facts.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
diff -r 0ab4217a07b1 -r e0d295cb8bfd src/HOL/SMT/Tools/smt_normalize.ML
--- 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)
diff -r 0ab4217a07b1 -r e0d295cb8bfd src/HOL/SMT/Tools/smt_solver.ML
--- 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 =