# HG changeset patch # User boehmes # Date 1274880887 -7200 # Node ID fe22fc54b8760ce120829090c7ed27c1b135f206 # Parent 9cce71cd4bf0812e132a39581c91fa14120eccb4 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns diff -r 9cce71cd4bf0 -r fe22fc54b876 src/HOL/Boogie/Tools/boogie_loader.ML --- 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 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 term-level 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 diff -r 9cce71cd4bf0 -r fe22fc54b876 src/HOL/SMT_Examples/SMT_Examples.thy --- 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 "\x::int. (\y. y \ x \ y > 0) \ x > 0" by smt -lemma "\x::int. trigger [pat x] (x < a \ 2 * x < 2 * a)" by smt +lemma "\x::int. SMT.trigger [[SMT.pat x]] (x < a \ 2 * x < 2 * a)" by smt subsection {* Non-linear arithmetic over integers and reals *} diff -r 9cce71cd4bf0 -r fe22fc54b876 src/HOL/SMT_Examples/SMT_Tests.thy --- 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] \ (\x y. f x = f y \ y = x) \ f a \ f b" sorry (* FIXME: injective function *) +lemma + assumes "\x. SMT.trigger [[SMT.pat (f x)]] (f x = x)" + shows "f 1 = 1" + using assms by smt + +lemma + assumes "\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 *} diff -r 9cce71cd4bf0 -r fe22fc54b876 src/HOL/Tools/SMT/smt_translate.ML --- 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 diff -r 9cce71cd4bf0 -r fe22fc54b876 src/HOL/ex/Meson_Test.thy --- 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