hide constants and types introduced by SMT,
authorboehmes
Wed May 26 15:34:47 2010 +0200 (2010-05-26)
changeset 37124fe22fc54b876
parent 37123 9cce71cd4bf0
child 37125 66b0ae11a358
hide constants and types introduced by SMT,
simplified SMT patterns syntax,
added examples for SMT patterns
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/ex/Meson_Test.thy
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed May 26 11:59:06 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Wed May 26 15:34:47 2010 +0200
     1.3 @@ -380,9 +380,11 @@
     1.4    fun mk_nary _ t [] = t
     1.5      | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts)
     1.6  
     1.7 +  fun mk_list T = HOLogic.mk_list T
     1.8 +
     1.9    fun mk_distinct T ts =
    1.10 -    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ 
    1.11 -      HOLogic.mk_list T ts
    1.12 +    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
    1.13 +      mk_list T ts
    1.14  
    1.15    fun quant name f = scan_line name (num -- num -- num) >> pair f
    1.16    val quants =
    1.17 @@ -391,20 +393,20 @@
    1.18      scan_fail "illegal quantifier kind"
    1.19    fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t)
    1.20  
    1.21 -  val patternT = @{typ pattern}
    1.22 +  val patternT = @{typ "SMT.pattern"}
    1.23    fun mk_pattern _ [] = raise TERM ("mk_pattern", [])
    1.24 -    | mk_pattern n [t] = Const (n, Term.fastype_of t --> patternT) $ t
    1.25 -    | mk_pattern n (t :: ts) =
    1.26 -        let val T = patternT --> Term.fastype_of t --> patternT
    1.27 -        in Const (@{const_name andpat}, T) $ mk_pattern n ts $ t end
    1.28 +    | mk_pattern n ts =
    1.29 +        let fun mk_pat t = Const (n, Term.fastype_of t --> patternT) $ t
    1.30 +        in mk_list patternT (map mk_pat ts) end
    1.31    fun patt n c scan =
    1.32      scan_line n num :|-- scan_count scan >> (mk_pattern c)
    1.33    fun pattern scan =
    1.34 -    patt "pat" @{const_name pat} scan ||
    1.35 -    patt "nopat" @{const_name nopat} scan ||
    1.36 +    patt "pat" @{const_name "SMT.pat"} scan ||
    1.37 +    patt "nopat" @{const_name "SMT.nopat"} scan ||
    1.38      scan_fail "illegal pattern kind"
    1.39    fun mk_trigger [] t = t
    1.40 -    | mk_trigger ps t = @{term trigger} $ HOLogic.mk_list patternT ps $ t
    1.41 +    | mk_trigger ps t =
    1.42 +        @{term "SMT.trigger"} $ mk_list @{typ "SMT.pattern list"} ps $ t
    1.43  
    1.44    fun make_label (line, col) = Free (label_name line col, @{typ bool})
    1.45    fun labelled_by kind pos t = kind $ make_label pos $ t
     2.1 --- a/src/HOL/SMT.thy	Wed May 26 11:59:06 2010 +0200
     2.2 +++ b/src/HOL/SMT.thy	Wed May 26 15:34:47 2010 +0200
     2.3 @@ -31,24 +31,22 @@
     2.4  text {*
     2.5  Some SMT solvers support triggers for quantifier instantiation.
     2.6  Each trigger consists of one ore more patterns.  A pattern may either
     2.7 -be a list of positive subterms (the first being tagged by "pat" and
     2.8 -the consecutive subterms tagged by "andpat"), or a list of negative
     2.9 -subterms (the first being tagged by "nopat" and the consecutive
    2.10 -subterms tagged by "andpat").
    2.11 +be a list of positive subterms (each being tagged by "pat"), or a
    2.12 +list of negative subterms (each being tagged by "nopat").
    2.13 +
    2.14 +When an SMT solver finds a term matching a positive pattern (a
    2.15 +pattern with positive subterms only), it instantiates the
    2.16 +corresponding quantifier accordingly.  Negative patterns inhibit
    2.17 +quantifier instantiations.  Each pattern should mention all preceding
    2.18 +bound variables.
    2.19  *}
    2.20  
    2.21  datatype pattern = Pattern
    2.22  
    2.23 -definition pat :: "'a \<Rightarrow> pattern"
    2.24 -where "pat _ = Pattern"
    2.25 +definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
    2.26 +definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
    2.27  
    2.28 -definition nopat :: "'a \<Rightarrow> pattern"
    2.29 -where "nopat _ = Pattern"
    2.30 -
    2.31 -definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
    2.32 -where "_ andpat _ = Pattern"
    2.33 -
    2.34 -definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
    2.35 +definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
    2.36  where "trigger _ P = P"
    2.37  
    2.38  
    2.39 @@ -86,8 +84,7 @@
    2.40  following term-level equation symbol.
    2.41  *}
    2.42  
    2.43 -definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
    2.44 -  where "(x term_eq y) = (x = y)"
    2.45 +definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
    2.46  
    2.47  
    2.48  
    2.49 @@ -291,4 +288,10 @@
    2.50    "x + y = y + x"
    2.51    by auto
    2.52  
    2.53 +
    2.54 +
    2.55 +hide_type (open) pattern
    2.56 +hide_const Pattern "apply" term_eq
    2.57 +hide_const (open) trigger pat nopat
    2.58 +
    2.59  end
     3.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Wed May 26 11:59:06 2010 +0200
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Wed May 26 15:34:47 2010 +0200
     3.3 @@ -395,7 +395,7 @@
     3.4  
     3.5  lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
     3.6  
     3.7 -lemma "\<forall>x::int. trigger [pat x] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
     3.8 +lemma "\<forall>x::int. SMT.trigger [[SMT.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
     3.9  
    3.10  
    3.11  subsection {* Non-linear arithmetic over integers and reals *}
     4.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed May 26 11:59:06 2010 +0200
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed May 26 15:34:47 2010 +0200
     4.3 @@ -190,6 +190,16 @@
     4.4    "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
     4.5    sorry  (* FIXME: injective function *)
     4.6  
     4.7 +lemma
     4.8 +  assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)"
     4.9 +  shows "f 1 = 1"
    4.10 +  using assms by smt
    4.11 +
    4.12 +lemma
    4.13 +  assumes "\<forall>x y. SMT.trigger [[SMT.pat (f x), SMT.pat (g y)]] (f x = g y)"
    4.14 +  shows "f 1 = g 2"
    4.15 +  using assms by smt
    4.16 +
    4.17  
    4.18  
    4.19  section {* Meta logical connectives *}
     5.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed May 26 11:59:06 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed May 26 15:34:47 2010 +0200
     5.3 @@ -119,13 +119,19 @@
     5.4        if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
     5.5    | group_quant _ Ts t = (Ts, t)
     5.6  
     5.7 -fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts))
     5.8 -  | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts))
     5.9 -  | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p
    5.10 -  | dest_pat _ t = raise TERM ("dest_pat", [t])
    5.11 +fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
    5.12 +  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
    5.13 +  | dest_pat t = raise TERM ("dest_pat", [t])
    5.14 +
    5.15 +fun dest_pats [] = I
    5.16 +  | dest_pats ts =
    5.17 +      (case map dest_pat ts |> split_list ||> distinct (op =) of
    5.18 +        (ps, [true]) => cons (SPat ps)
    5.19 +      | (ps, [false]) => cons (SNoPat ps)
    5.20 +      | _ => raise TERM ("dest_pats", ts))
    5.21  
    5.22  fun dest_trigger (@{term trigger} $ tl $ t) =
    5.23 -      (map (dest_pat []) (HOLogic.dest_list tl), t)
    5.24 +      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
    5.25    | dest_trigger t = ([], t)
    5.26  
    5.27  fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
    5.28 @@ -143,9 +149,9 @@
    5.29  
    5.30  (* enforce a strict separation between formulas and terms *)
    5.31  
    5.32 -val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)}
    5.33 +val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
    5.34  
    5.35 -val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)}
    5.36 +val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
    5.37  val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
    5.38  
    5.39  
    5.40 @@ -210,11 +216,10 @@
    5.41  
    5.42      and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
    5.43        | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
    5.44 -      | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) =
    5.45 -          c $ in_pat p $ in_term t
    5.46        | in_pat t = raise TERM ("in_pat", [t])
    5.47  
    5.48 -    and in_pats p = in_list @{typ pattern} in_pat p
    5.49 +    and in_pats ps =
    5.50 +      in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
    5.51  
    5.52      and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
    5.53        | in_trig t = in_form t
     6.1 --- a/src/HOL/ex/Meson_Test.thy	Wed May 26 11:59:06 2010 +0200
     6.2 +++ b/src/HOL/ex/Meson_Test.thy	Wed May 26 15:34:47 2010 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4    below and constants declared in HOL!
     6.5  *}
     6.6  
     6.7 -hide_const (open) subset member quotient union inter "apply"
     6.8 +hide_const (open) subset member quotient union inter
     6.9  
    6.10  text {*
    6.11    Test data for the MESON proof procedure