src/HOL/SMT.thy
 changeset 37124 fe22fc54b876 parent 36902 c6bae4456741 child 37151 3e9e8dfb3c98
```     1.1 --- a/src/HOL/SMT.thy	Wed May 26 11:59:06 2010 +0200
1.2 +++ b/src/HOL/SMT.thy	Wed May 26 15:34:47 2010 +0200
1.3 @@ -31,24 +31,22 @@
1.4  text {*
1.5  Some SMT solvers support triggers for quantifier instantiation.
1.6  Each trigger consists of one ore more patterns.  A pattern may either
1.7 -be a list of positive subterms (the first being tagged by "pat" and
1.8 -the consecutive subterms tagged by "andpat"), or a list of negative
1.9 -subterms (the first being tagged by "nopat" and the consecutive
1.10 -subterms tagged by "andpat").
1.11 +be a list of positive subterms (each being tagged by "pat"), or a
1.12 +list of negative subterms (each being tagged by "nopat").
1.13 +
1.14 +When an SMT solver finds a term matching a positive pattern (a
1.15 +pattern with positive subterms only), it instantiates the
1.16 +corresponding quantifier accordingly.  Negative patterns inhibit
1.17 +quantifier instantiations.  Each pattern should mention all preceding
1.18 +bound variables.
1.19  *}
1.20
1.21  datatype pattern = Pattern
1.22
1.23 -definition pat :: "'a \<Rightarrow> pattern"
1.24 -where "pat _ = Pattern"
1.25 +definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
1.26 +definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
1.27
1.28 -definition nopat :: "'a \<Rightarrow> pattern"
1.29 -where "nopat _ = Pattern"
1.30 -
1.31 -definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
1.32 -where "_ andpat _ = Pattern"
1.33 -
1.34 -definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
1.35 +definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
1.36  where "trigger _ P = P"
1.37
1.38
1.39 @@ -86,8 +84,7 @@
1.40  following term-level equation symbol.
1.41  *}
1.42
1.43 -definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
1.44 -  where "(x term_eq y) = (x = y)"
1.45 +definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
1.46
1.47
1.48
1.49 @@ -291,4 +288,10 @@
1.50    "x + y = y + x"
1.51    by auto
1.52
1.53 +
1.54 +
1.55 +hide_type (open) pattern
1.56 +hide_const Pattern "apply" term_eq
1.57 +hide_const (open) trigger pat nopat
1.58 +
1.59  end
```