introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Oct 29 18:17:04 2010 +0200
@@ -191,7 +191,7 @@
             | NONE => NONE)
         | is_unique _ = NONE
       fun mk_unique_axiom T ts =
-        Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
+        Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
           HOLogic.mk_list T ts
     in
       map_filter is_unique fns
@@ -383,7 +383,7 @@
   fun mk_list T = HOLogic.mk_list T
 
   fun mk_distinct T ts =
-    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $
+    Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
       mk_list T ts
 
   fun quant name f = scan_line name (num -- num -- num) >> pair f

--- a/src/HOL/SMT.thy	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/SMT.thy	Fri Oct 29 18:17:04 2010 +0200
@@ -49,6 +49,20 @@
 
 
 
+subsection {* Distinctness *}
+
+text {*
+As an abbreviation for a quadratic number of inequalities, SMT solvers
+provide a built-in @{text distinct}.  To avoid confusion with the
+already defined (and more general) @{term List.distinct}, a separate
+constant is defined.
+*}
+
+definition distinct :: "'a list \<Rightarrow> bool"
+where "distinct xs = List.distinct xs"
+
+
+
 subsection {* Higher-order encoding *}
 
 text {*
@@ -314,7 +328,7 @@
 
 hide_type (open) pattern
 hide_const Pattern term_eq
-hide_const (open) trigger pat nopat fun_app z3div z3mod
+hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
 
 
 

--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Oct 29 18:17:04 2010 +0200
@@ -293,11 +293,11 @@
 
 lemma "(0 \<le> y + -1 * x \<or> \<not> 0 \<le> x \<or> 0 \<le> (x::int)) = (\<not> False)" by smt
 
-lemma "distinct [x < (3::int), 3 \<le> x]" by smt
+lemma "SMT.distinct [x < (3::int), 3 \<le> x]" by smt
 
 lemma
   assumes "a > (0::int)"
-  shows "distinct [a, a * 2, a - a]"
+  shows "SMT.distinct [a, a * 2, a - a]"
   using assms by smt
 
 lemma "
@@ -430,7 +430,7 @@
    False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
   by smt
 
-lemma "distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
+lemma "SMT.distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
 
 lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
 

--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Oct 29 18:17:04 2010 +0200
@@ -104,15 +104,15 @@
   by smt+
 
 lemma
-  "distinct []"
-  "distinct [a]"
-  "distinct [a, b, c] \<longrightarrow> a \<noteq> c"
-  "distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d"
-  "\<not> distinct [a, b, a, b]"
-  "a = b \<longrightarrow> \<not>distinct [a, b]"
-  "a = b \<and> a = c \<longrightarrow> \<not>distinct [a, b, c]"
-  "distinct [a, b, c, d] \<longrightarrow> distinct [d, b, c, a]"
-  "distinct [a, b, c, d] \<longrightarrow> distinct [a, b, c] \<and> distinct [b, c, d]"
+  "SMT.distinct []"
+  "SMT.distinct [a]"
+  "SMT.distinct [a, b, c] \<longrightarrow> a \<noteq> c"
+  "SMT.distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d"
+  "\<not> SMT.distinct [a, b, a, b]"
+  "a = b \<longrightarrow> \<not> SMT.distinct [a, b]"
+  "a = b \<and> a = c \<longrightarrow> \<not> SMT.distinct [a, b, c]"
+  "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [d, b, c, a]"
+  "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [a, b, c] \<and> SMT.distinct [b, c, d]"
   by smt+
 
 lemma
@@ -193,7 +193,7 @@
   by smt+
 
 lemma
-  "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
+  "SMT.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
@@ -636,7 +636,7 @@
   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2"
   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
-  "distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
+  "SMT.distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
   by smt+
 
 

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:04 2010 +0200
@@ -40,15 +40,18 @@
    three elements in the argument list) *)
 
 local
-  fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
-        length (HOLogic.dest_list t) <= 2
+  fun is_trivial_distinct (Const (@{const_name SMT.distinct}, _) $ t) =
+       (length (HOLogic.dest_list t) <= 2
+        handle TERM _ => error ("SMT: constant " ^
+          quote @{const_name SMT.distinct} ^ " must be applied to " ^
+          "an explicit list."))
     | is_trivial_distinct _ = false
 
   val thms = map mk_meta_eq @{lemma
-    "distinct [] = True"
-    "distinct [x] = True"
-    "distinct [x, y] = (x ~= y)"
-    by simp_all}
+    "SMT.distinct [] = True"
+    "SMT.distinct [x] = True"
+    "SMT.distinct [x, y] = (x ~= y)"
+    by (simp_all add: distinct_def)}
   fun distinct_conv _ =
     if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
 in

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

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

--- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Oct 29 18:17:04 2010 +0200
@@ -65,7 +65,7 @@
 (** interface **)
 
 local
-  val {extra_norm, translate} = SMTLIB_Interface.interface
+  val {translate, ...} = SMTLIB_Interface.interface
   val {prefixes, strict, header, builtins, serialize} = translate
   val {is_builtin_pred, ...}= the strict
   val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
@@ -189,7 +189,7 @@
 fun mk_list cT cts =
   fold_rev (Thm.mk_binop (instT cT cons_term)) cts (instT cT nil_term)
 
-val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
+val distinct = mk_inst_pair (destT1 o destT1) @{cpat SMT.distinct}
 fun mk_distinct [] = mk_true
   | mk_distinct (cts as (ct :: _)) =
       Thm.capply (instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Oct 29 18:17:04 2010 +0200
@@ -303,14 +303,14 @@
           prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
       | @{term HOL.disj} $ _ $ _ =>
           prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
-      | Const (@{const_name distinct}, _) $ _ =>
+      | Const (@{const_name SMT.distinct}, _) $ _ =>
           let
             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
             fun prv cu =
               let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
               in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
           in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
-      | @{term Not} $ (Const (@{const_name distinct}, _) $ _) =>
+      | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
           let
             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
             fun prv cu =
@@ -476,7 +476,7 @@
     (case Term.head_of (Thm.term_of cl) of
       @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
     | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
-    | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
+    | Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
     | _ => prove (prove_eq_safe f)) cp
 in
 fun monotonicity eqs ct =

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Oct 29 17:38:57 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Oct 29 18:17:04 2010 +0200
@@ -204,7 +204,7 @@
       | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
       | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
-      | Const (@{const_name distinct}, _) $ _ =>
+      | Const (@{const_name SMT.distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
           else fresh_abstraction cvs ct
       | Const (@{const_name If}, _) $ _ $ _ $ _ =>
@@ -263,10 +263,10 @@
     (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
     (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
 
-  val dist1 = @{lemma "distinct [] == ~False" by simp}
-  val dist2 = @{lemma "distinct [x] == ~False" by simp}
-  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
-    by simp}
+  val dist1 = @{lemma "SMT.distinct [] == ~False" by (simp add: distinct_def)}
+  val dist2 = @{lemma "SMT.distinct [x] == ~False" by (simp add: distinct_def)}
+  val dist3 = @{lemma "SMT.distinct (x # xs) == x ~: set xs & distinct xs"
+    by (simp add: distinct_def)}
 
   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
 in