1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Oct 29 17:38:57 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Oct 29 18:17:04 2010 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4              | NONE => NONE)
     1.5          | is_unique _ = NONE
     1.6        fun mk_unique_axiom T ts =
     1.7 -        Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
     1.8 +        Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
     1.9            HOLogic.mk_list T ts
    1.10      in
    1.11        map_filter is_unique fns
    1.12 @@ -383,7 +383,7 @@
    1.13    fun mk_list T = HOLogic.mk_list T
    1.14  
    1.15    fun mk_distinct T ts =
    1.16 -    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
    1.17 +    Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
    1.18        mk_list T ts
    1.19  
    1.20    fun quant name f = scan_line name (num -- num -- num) >> pair f

     2.1 --- a/src/HOL/SMT.thy	Fri Oct 29 17:38:57 2010 +0200
     2.2 +++ b/src/HOL/SMT.thy	Fri Oct 29 18:17:04 2010 +0200
     2.3 @@ -49,6 +49,20 @@
     2.4  
     2.5  
     2.6  
     2.7 +subsection {* Distinctness *}
     2.8 +
     2.9 +text {*
    2.10 +As an abbreviation for a quadratic number of inequalities, SMT solvers
    2.11 +provide a built-in @{text distinct}.  To avoid confusion with the
    2.12 +already defined (and more general) @{term List.distinct}, a separate
    2.13 +constant is defined.
    2.14 +*}
    2.15 +
    2.16 +definition distinct :: "'a list \<Rightarrow> bool"
    2.17 +where "distinct xs = List.distinct xs"
    2.18 +
    2.19 +
    2.20 +
    2.21  subsection {* Higher-order encoding *}
    2.22  
    2.23  text {*
    2.24 @@ -314,7 +328,7 @@
    2.25  
    2.26  hide_type (open) pattern
    2.27  hide_const Pattern term_eq
    2.28 -hide_const (open) trigger pat nopat fun_app z3div z3mod
    2.29 +hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
    2.30  
    2.31  
    2.32  

     3.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Oct 29 17:38:57 2010 +0200
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Oct 29 18:17:04 2010 +0200
     3.3 @@ -293,11 +293,11 @@
     3.4  
     3.5  lemma "(0 \<le> y + -1 * x \<or> \<not> 0 \<le> x \<or> 0 \<le> (x::int)) = (\<not> False)" by smt
     3.6  
     3.7 -lemma "distinct [x < (3::int), 3 \<le> x]" by smt
     3.8 +lemma "SMT.distinct [x < (3::int), 3 \<le> x]" by smt
     3.9  
    3.10  lemma
    3.11    assumes "a > (0::int)"
    3.12 -  shows "distinct [a, a * 2, a - a]"
    3.13 +  shows "SMT.distinct [a, a * 2, a - a]"
    3.14    using assms by smt
    3.15  
    3.16  lemma "
    3.17 @@ -430,7 +430,7 @@
    3.18     False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
    3.19    by smt
    3.20  
    3.21 -lemma "distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
    3.22 +lemma "SMT.distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
    3.23  
    3.24  lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
    3.25  

     4.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 29 17:38:57 2010 +0200
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 29 18:17:04 2010 +0200
     4.3 @@ -104,15 +104,15 @@
     4.4    by smt+
     4.5  
     4.6  lemma
     4.7 -  "distinct []"
     4.8 -  "distinct [a]"
     4.9 -  "distinct [a, b, c] \<longrightarrow> a \<noteq> c"
    4.10 -  "distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d"
    4.11 -  "\<not> distinct [a, b, a, b]"
    4.12 -  "a = b \<longrightarrow> \<not>distinct [a, b]"
    4.13 -  "a = b \<and> a = c \<longrightarrow> \<not>distinct [a, b, c]"
    4.14 -  "distinct [a, b, c, d] \<longrightarrow> distinct [d, b, c, a]"
    4.15 -  "distinct [a, b, c, d] \<longrightarrow> distinct [a, b, c] \<and> distinct [b, c, d]"
    4.16 +  "SMT.distinct []"
    4.17 +  "SMT.distinct [a]"
    4.18 +  "SMT.distinct [a, b, c] \<longrightarrow> a \<noteq> c"
    4.19 +  "SMT.distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d"
    4.20 +  "\<not> SMT.distinct [a, b, a, b]"
    4.21 +  "a = b \<longrightarrow> \<not> SMT.distinct [a, b]"
    4.22 +  "a = b \<and> a = c \<longrightarrow> \<not> SMT.distinct [a, b, c]"
    4.23 +  "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [d, b, c, a]"
    4.24 +  "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [a, b, c] \<and> SMT.distinct [b, c, d]"
    4.25    by smt+
    4.26  
    4.27  lemma
    4.28 @@ -193,7 +193,7 @@
    4.29    by smt+
    4.30  
    4.31  lemma
    4.32 -  "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
    4.33 +  "SMT.distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
    4.34    sorry  (* FIXME: injective function *)
    4.35  
    4.36  lemma
    4.37 @@ -636,7 +636,7 @@
    4.38    "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2"
    4.39    "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
    4.40    "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
    4.41 -  "distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
    4.42 +  "SMT.distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
    4.43    by smt+
    4.44  
    4.45  

     5.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 17:38:57 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:04 2010 +0200
     5.3 @@ -40,15 +40,18 @@
     5.4     three elements in the argument list) *)
     5.5  
     5.6  local
     5.7 -  fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
     5.8 -        length (HOLogic.dest_list t) <= 2
     5.9 +  fun is_trivial_distinct (Const (@{const_name SMT.distinct}, _) $ t) =
    5.10 +       (length (HOLogic.dest_list t) <= 2
    5.11 +        handle TERM _ => error ("SMT: constant " ^
    5.12 +          quote @{const_name SMT.distinct} ^ " must be applied to " ^
    5.13 +          "an explicit list."))
    5.14      | is_trivial_distinct _ = false
    5.15  
    5.16    val thms = map mk_meta_eq @{lemma
    5.17 -    "distinct [] = True"
    5.18 -    "distinct [x] = True"
    5.19 -    "distinct [x, y] = (x ~= y)"
    5.20 -    by simp_all}
    5.21 +    "SMT.distinct [] = True"
    5.22 +    "SMT.distinct [x] = True"
    5.23 +    "SMT.distinct [x, y] = (x ~= y)"
    5.24 +    by (simp_all add: distinct_def)}
    5.25    fun distinct_conv _ =
    5.26      if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    5.27  in

     6.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Oct 29 17:38:57 2010 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Oct 29 18:17:04 2010 +0200
     6.3 @@ -233,7 +233,7 @@
     6.4          (q as Const (qn, _), [Abs (n, T, t')]) =>
     6.5            if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
     6.6            else as_term (in_term t)
     6.7 -      | (Const (c as (@{const_name distinct}, T)), [t']) =>
     6.8 +      | (Const (c as (@{const_name SMT.distinct}, T)), [t']) =>
     6.9            if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
    6.10            else as_term (in_term t)
    6.11        | (Const c, ts) =>
    6.12 @@ -377,7 +377,7 @@
    6.13        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    6.14            transT T ##>> trans t1 ##>> trans t2 #>>
    6.15            (fn ((U, u1), u2) => SLet (U, u1, u2))
    6.16 -      | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
    6.17 +      | (h as Const (c as (@{const_name SMT.distinct}, T)), [t1]) =>
    6.18            (case builtin_fun ctxt c (HOLogic.dest_list t1) of
    6.19              SOME (n, ts) => fold_map trans ts #>> app n
    6.20            | NONE => transs h T [t1])

     7.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Oct 29 17:38:57 2010 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Oct 29 18:17:04 2010 +0200
     7.3 @@ -167,7 +167,7 @@
     7.4    | conn @{const_name If} = SOME "if_then_else"
     7.5    | conn _ = NONE
     7.6  
     7.7 -fun pred @{const_name distinct} _ = SOME "distinct"
     7.8 +fun pred @{const_name SMT.distinct} _ = SOME "distinct"
     7.9    | pred @{const_name HOL.eq} _ = SOME "="
    7.10    | pred @{const_name term_eq} _ = SOME "="
    7.11    | pred @{const_name less} T = if_int_type T "<"

     8.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Oct 29 17:38:57 2010 +0200
     8.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Oct 29 18:17:04 2010 +0200
     8.3 @@ -65,7 +65,7 @@
     8.4  (** interface **)
     8.5  
     8.6  local
     8.7 -  val {extra_norm, translate} = SMTLIB_Interface.interface
     8.8 +  val {translate, ...} = SMTLIB_Interface.interface
     8.9    val {prefixes, strict, header, builtins, serialize} = translate
    8.10    val {is_builtin_pred, ...}= the strict
    8.11    val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
    8.12 @@ -189,7 +189,7 @@
    8.13  fun mk_list cT cts =
    8.14    fold_rev (Thm.mk_binop (instT cT cons_term)) cts (instT cT nil_term)
    8.15  
    8.16 -val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
    8.17 +val distinct = mk_inst_pair (destT1 o destT1) @{cpat SMT.distinct}
    8.18  fun mk_distinct [] = mk_true
    8.19    | mk_distinct (cts as (ct :: _)) =
    8.20        Thm.capply (instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)

     9.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 29 17:38:57 2010 +0200
     9.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 29 18:17:04 2010 +0200
     9.3 @@ -303,14 +303,14 @@
     9.4            prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
     9.5        | @{term HOL.disj} $ _ $ _ =>
     9.6            prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
     9.7 -      | Const (@{const_name distinct}, _) $ _ =>
     9.8 +      | Const (@{const_name SMT.distinct}, _) $ _ =>
     9.9            let
    9.10              fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
    9.11              fun prv cu =
    9.12                let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
    9.13                in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
    9.14            in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
    9.15 -      | @{term Not} $ (Const (@{const_name distinct}, _) $ _) =>
    9.16 +      | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
    9.17            let
    9.18              fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
    9.19              fun prv cu =
    9.20 @@ -476,7 +476,7 @@
    9.21      (case Term.head_of (Thm.term_of cl) of
    9.22        @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
    9.23      | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
    9.24 -    | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
    9.25 +    | Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
    9.26      | _ => prove (prove_eq_safe f)) cp
    9.27  in
    9.28  fun monotonicity eqs ct =

    10.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Oct 29 17:38:57 2010 +0200
    10.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Oct 29 18:17:04 2010 +0200
    10.3 @@ -204,7 +204,7 @@
    10.4        | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
    10.5        | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
    10.6        | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
    10.7 -      | Const (@{const_name distinct}, _) $ _ =>
    10.8 +      | Const (@{const_name SMT.distinct}, _) $ _ =>
    10.9            if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
   10.10            else fresh_abstraction cvs ct
   10.11        | Const (@{const_name If}, _) $ _ $ _ $ _ =>
   10.12 @@ -263,10 +263,10 @@
   10.13      (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
   10.14      (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
   10.15  
   10.16 -  val dist1 = @{lemma "distinct [] == ~False" by simp}
   10.17 -  val dist2 = @{lemma "distinct [x] == ~False" by simp}
   10.18 -  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
   10.19 -    by simp}
   10.20 +  val dist1 = @{lemma "SMT.distinct [] == ~False" by (simp add: distinct_def)}
   10.21 +  val dist2 = @{lemma "SMT.distinct [x] == ~False" by (simp add: distinct_def)}
   10.22 +  val dist3 = @{lemma "SMT.distinct (x # xs) == x ~: set xs & distinct xs"
   10.23 +    by (simp add: distinct_def)}
   10.24  
   10.25    fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   10.26  in