hide constants and types introduced by SMT,
simplified SMT patterns syntax,
added examples for SMT patterns

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Wed May 26 15:34:47 2010 +0200
@@ -380,9 +380,11 @@
   fun mk_nary _ t [] = t
     | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
 
+  fun mk_list T = HOLogic.mk_list T
+
   fun mk_distinct T ts =
-    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ 
-      HOLogic.mk_list T ts
+    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
+      mk_list T ts
 
   fun quant name f = scan_line name (num -- num -- num) >> pair f
   val quants =
@@ -391,20 +393,20 @@
     scan_fail "illegal quantifier kind"
   fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t)
 
-  val patternT = @{typ pattern}
+  val patternT = @{typ "SMT.pattern"}
   fun mk_pattern _ [] = raise TERM ("mk_pattern", [])
-    | mk_pattern n [t] = Const (n, Term.fastype_of t --> patternT) $ t
-    | mk_pattern n (t :: ts) =
-        let val T = patternT --> Term.fastype_of t --> patternT
-        in Const (@{const_name andpat}, T) $ mk_pattern n ts $ t end
+    | mk_pattern n ts =
+        let fun mk_pat t = Const (n, Term.fastype_of t --> patternT) $ t
+        in mk_list patternT (map mk_pat ts) end
   fun patt n c scan =
     scan_line n num :|-- scan_count scan >> (mk_pattern c)
   fun pattern scan =
-    patt "pat" @{const_name pat} scan ||
-    patt "nopat" @{const_name nopat} scan ||
+    patt "pat" @{const_name "SMT.pat"} scan ||
+    patt "nopat" @{const_name "SMT.nopat"} scan ||
     scan_fail "illegal pattern kind"
   fun mk_trigger [] t = t
-    | mk_trigger ps t = @{term trigger} $ HOLogic.mk_list patternT ps $ t
+    | mk_trigger ps t =
+        @{term "SMT.trigger"} $ mk_list @{typ "SMT.pattern list"} ps $ t
 
   fun make_label (line, col) = Free (label_name line col, @{typ bool})
   fun labelled_by kind pos t = kind $ make_label pos $ t

--- 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 \<Rightarrow> pattern"
-where "pat _ = Pattern"
+definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
+definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
 
-definition nopat :: "'a \<Rightarrow> pattern"
-where "nopat _ = Pattern"
-
-definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
-where "_ andpat _ = Pattern"
-
-definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
+definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
 where "trigger _ P = P"
 
 
@@ -86,8 +84,7 @@
 following term-level equation symbol.
 *}
 
-definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
-  where "(x term_eq y) = (x = y)"
+definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> 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

--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Wed May 26 15:34:47 2010 +0200
@@ -395,7 +395,7 @@
 
 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
 
-lemma "\<forall>x::int. trigger [pat x] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
+lemma "\<forall>x::int. SMT.trigger [[SMT.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
 
 
 subsection {* Non-linear arithmetic over integers and reals *}

--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed May 26 15:34:47 2010 +0200
@@ -190,6 +190,16 @@
   "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
   sorry  (* FIXME: injective function *)
 
+lemma
+  assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)"
+  shows "f 1 = 1"
+  using assms by smt
+
+lemma
+  assumes "\<forall>x y. SMT.trigger [[SMT.pat (f x), SMT.pat (g y)]] (f x = g y)"
+  shows "f 1 = g 2"
+  using assms by smt
+
 
 
 section {* Meta logical connectives *}

--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed May 26 15:34:47 2010 +0200
@@ -119,13 +119,19 @@
       if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
   | group_quant _ Ts t = (Ts, t)
 
-fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts))
-  | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts))
-  | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p
-  | dest_pat _ t = raise TERM ("dest_pat", [t])
+fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
+  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
+  | dest_pat t = raise TERM ("dest_pat", [t])
+
+fun dest_pats [] = I
+  | dest_pats ts =
+      (case map dest_pat ts |> split_list ||> distinct (op =) of
+        (ps, [true]) => cons (SPat ps)
+      | (ps, [false]) => cons (SNoPat ps)
+      | _ => raise TERM ("dest_pats", ts))
 
 fun dest_trigger (@{term trigger} $ tl $ t) =
-      (map (dest_pat []) (HOLogic.dest_list tl), t)
+      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
   | dest_trigger t = ([], t)
 
 fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
@@ -143,9 +149,9 @@
 
 (* enforce a strict separation between formulas and terms *)
 
-val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)}
+val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
 
-val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)}
+val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
 val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
 
 
@@ -210,11 +216,10 @@
 
     and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
       | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
-      | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) =
-          c $ in_pat p $ in_term t
       | in_pat t = raise TERM ("in_pat", [t])
 
-    and in_pats p = in_list @{typ pattern} in_pat p
+    and in_pats ps =
+      in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
 
     and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
       | in_trig t = in_form t

--- a/src/HOL/ex/Meson_Test.thy	Wed May 26 11:59:06 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Wed May 26 15:34:47 2010 +0200
@@ -16,7 +16,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) subset member quotient union inter "apply"
+hide_const (open) subset member quotient union inter
 
 text {*
   Test data for the MESON proof procedure