added option to enable trigger inference;
better documentation of triggers and SMT available options

--- a/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
+++ b/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
@@ -32,16 +32,18 @@
 subsection {* Triggers for quantifier instantiation *}
 
 text {*
-Some SMT solvers support triggers for quantifier instantiation.
-Each trigger consists of one ore more patterns.  A pattern may either
-be a list of positive subterms (each being tagged by "pat"), or a
-list of negative subterms (each being tagged by "nopat").
-
-When an SMT solver finds a term matching a positive pattern (a
-pattern with positive subterms only), it instantiates the
-corresponding quantifier accordingly.  Negative patterns inhibit
-quantifier instantiations.  Each pattern should mention all preceding
-bound variables.
+Some SMT solvers support patterns as a quantifier instantiation
+heuristics.  Patterns may either be positive terms (tagged by "pat")
+triggering quantifier instantiations -- when the solver finds a
+term matching a positive pattern, it instantiates the corresponding
+quantifier accordingly -- or negative terms (tagged by "nopat")
+inhibiting quantifier instantiations.  A list of patterns
+of the same kind is called a multipattern, and all patterns in a
+multipattern are considered conjunctively for quantifier instantiation.
+A list of multipatterns is called a trigger, and their multipatterns
+act disjunctively during quantifier instantiation.  Each multipattern
+should mention at least all quantified variables of the preceding
+quantifier block.
 *}
 
 datatype pattern = Pattern
@@ -236,6 +238,24 @@
 
 declare [[ smt_datatypes = false ]]
 
+text {*
+The SMT method provides an inference mechanism to detect simple triggers
+in quantified formulas, which might increase the number of problems
+solvable by SMT solvers (note: triggers guide quantifier instantiations
+in the SMT solver).  To turn it on, set the following option.
+*}
+
+declare [[ smt_infer_triggers = false ]]
+
+text {*
+The SMT method monomorphizes the given facts, that is, it tries to
+instantiate all schematic type variables with fixed types occurring
+in the problem.  This is a (possibly nonterminating) fixed-point
+construction whose cycles are limited by the following option.
+*}
+
+declare [[ smt_monomorph_limit = 10 ]]
+
 
 
 subsection {* Certificates *}

--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Dec 15 08:39:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Dec 15 08:39:24 2010 +0100
@@ -26,6 +26,7 @@
   val trace: bool Config.T
   val trace_used_facts: bool Config.T
   val monomorph_limit: int Config.T
+  val infer_triggers: bool Config.T
   val drop_bad_facts: bool Config.T
   val filter_only_facts: bool Config.T
   val debug_files: string Config.T
@@ -135,6 +136,10 @@
 val (monomorph_limit, setup_monomorph_limit) =
   Attrib.config_int monomorph_limitN (K 10)
 
+val infer_triggersN = "smt_infer_triggers"
+val (infer_triggers, setup_infer_triggers) =
+  Attrib.config_bool infer_triggersN (K false)
+
 val drop_bad_factsN = "smt_drop_bad_facts"
 val (drop_bad_facts, setup_drop_bad_facts) =
   Attrib.config_bool drop_bad_factsN (K false)
@@ -156,6 +161,7 @@
   setup_trace #>
   setup_verbose #>
   setup_monomorph_limit #>
+  setup_infer_triggers #>
   setup_drop_bad_facts #>
   setup_filter_only_facts #>
   setup_trace_used_facts #>