diff r 9cce71cd4bf0 r fe22fc54b876 src/HOL/SMT.thy
 a/src/HOL/SMT.thy Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/SMT.thy Wed May 26 15:34:47 2010 +0200
@@ 31,24 +31,22 @@
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 (the first being tagged by "pat" and
the consecutive subterms tagged by "andpat"), or a list of negative
subterms (the first being tagged by "nopat" and the consecutive
subterms tagged by "andpat").
+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.
*}
datatype pattern = Pattern
definition pat :: "'a \ pattern"
where "pat _ = Pattern"
+definition pat :: "'a \ pattern" where "pat _ = Pattern"
+definition nopat :: "'a \ pattern" where "nopat _ = Pattern"
definition nopat :: "'a \ pattern"
where "nopat _ = Pattern"

definition andpat :: "pattern \ 'a \ pattern" (infixl "andpat" 60)
where "_ andpat _ = Pattern"

definition trigger :: "pattern list \ bool \ bool"
+definition trigger :: "pattern list list \ bool \ bool"
where "trigger _ P = P"
@@ 86,8 +84,7 @@
following termlevel equation symbol.
*}
definition term_eq :: "bool \ bool \ bool" (infix "term'_eq" 50)
 where "(x term_eq y) = (x = y)"
+definition term_eq :: "bool \ bool \ bool" where "term_eq x y = (x = y)"
@@ 291,4 +288,10 @@
"x + y = y + x"
by auto
+
+
+hide_type (open) pattern
+hide_const Pattern "apply" term_eq
+hide_const (open) trigger pat nopat
+
end