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