--- a/src/HOL/Boogie/Tools/boogie_loader.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Wed Nov 24 10:42:28 2010 +0100
@@ -191,7 +191,7 @@
| NONE => NONE)
| is_unique _ = NONE
fun mk_unique_axiom T ts =
- Const (@{const_name SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
+ Const (@{const_name 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 SMT.distinct}, HOLogic.listT T --> @{typ bool}) $
+ 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
--- a/src/HOL/SMT.thy Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/SMT.thy Wed Nov 24 10:42:28 2010 +0100
@@ -81,20 +81,6 @@
-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 {*
@@ -369,7 +355,7 @@
hide_type (open) pattern
hide_const Pattern term_eq
-hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight fun_app z3div z3mod
--- a/src/HOL/SMT_Examples/SMT_Examples.certs Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Wed Nov 24 10:42:28 2010 +0100
@@ -16193,3 +16193,101 @@
#223 := [asserted]: #31
[unit-resolution #223 #592]: false
unsat
+030f06ff279b2b609c311e25ffea5c845380fd2c 97 0
+#2 := false
+decl f1 :: S1
+#4 := f1
+decl f2 :: S1
+#5 := f2
+#9 := 3::int
+decl f3 :: int
+#8 := f3
+#46 := (>= f3 3::int)
+#51 := (ite #46 f2 f1)
+#73 := (= f1 #51)
+#58 := (ite #46 f1 f2)
+#69 := (= f1 #58)
+#115 := (iff #69 #73)
+#113 := (iff #73 #69)
+#61 := (= #51 #58)
+#12 := (<= 3::int f3)
+#13 := (ite #12 f1 f2)
+#10 := (< f3 3::int)
+#11 := (ite #10 f1 f2)
+#14 := (distinct #11 #13)
+#15 := (not #14)
+#64 := (iff #15 #61)
+#33 := (= #11 #13)
+#62 := (iff #33 #61)
+#59 := (= #13 #58)
+#56 := (iff #12 #46)
+#57 := [rewrite]: #56
+#60 := [monotonicity #57]: #59
+#54 := (= #11 #51)
+#44 := (not #46)
+#48 := (ite #44 f1 f2)
+#52 := (= #48 #51)
+#53 := [rewrite]: #52
+#49 := (= #11 #48)
+#45 := (iff #10 #44)
+#47 := [rewrite]: #45
+#50 := [monotonicity #47]: #49
+#55 := [trans #50 #53]: #54
+#63 := [monotonicity #55 #60]: #62
+#42 := (iff #15 #33)
+#34 := (not #33)
+#37 := (not #34)
+#40 := (iff #37 #33)
+#41 := [rewrite]: #40
+#38 := (iff #15 #37)
+#35 := (iff #14 #34)
+#36 := [rewrite]: #35
+#39 := [monotonicity #36]: #38
+#43 := [trans #39 #41]: #42
+#65 := [trans #43 #63]: #64
+#32 := [asserted]: #15
+#66 := [mp #32 #65]: #61
+#114 := [monotonicity #66]: #113
+#116 := [symm #114]: #115
+#109 := (not #73)
+#6 := (= f1 f2)
+#67 := (= f2 #58)
+#105 := (iff #67 #6)
+#103 := (iff #6 #67)
+#98 := (= #58 f2)
+#101 := (iff #98 #67)
+#102 := [commutativity]: #101
+#99 := (iff #6 #98)
+#96 := [hypothesis]: #73
+#97 := [trans #96 #66]: #69
+#100 := [monotonicity #97]: #99
+#104 := [trans #100 #102]: #103
+#106 := [symm #104]: #105
+#72 := (= f2 #51)
+#84 := (iff #72 #67)
+#85 := [monotonicity #66]: #84
+#80 := (not #67)
+#81 := [hypothesis]: #80
+#78 := (or #46 #67)
+#79 := [def-axiom]: #78
+#82 := [unit-resolution #79 #81]: #46
+#74 := (or #44 #72)
+#75 := [def-axiom]: #74
+#83 := [unit-resolution #75 #82]: #72
+#86 := [mp #83 #85]: #67
+#87 := [unit-resolution #81 #86]: false
+#88 := [lemma #87]: #67
+#107 := [mp #88 #106]: #6
+#7 := (not #6)
+#31 := [asserted]: #7
+#108 := [unit-resolution #31 #107]: false
+#110 := [lemma #108]: #109
+#70 := (or #46 #73)
+#71 := [def-axiom]: #70
+#111 := [unit-resolution #71 #110]: #46
+#76 := (or #44 #69)
+#77 := [def-axiom]: #76
+#112 := [unit-resolution #77 #111]: #69
+#117 := [mp #112 #116]: #73
+[unit-resolution #110 #117]: false
+unsat
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Wed Nov 24 10:42:28 2010 +0100
@@ -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 "SMT.distinct [x < (3::int), 3 \<le> x]" by smt
+lemma "distinct [x < (3::int), 3 \<le> x]" by smt
lemma
assumes "a > (0::int)"
- shows "SMT.distinct [a, a * 2, a - a]"
+ shows "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 "SMT.distinct [a + (1::nat), a * 2 + 3, a - a]" by smt
+lemma "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.certs Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs Wed Nov 24 10:42:28 2010 +0100
@@ -53701,3 +53701,42 @@
#60 := [asserted]: #10
[mp #60 #69]: false
unsat
+c4d2e4408924ee75f6b9b17e513fd22b6307bf65 38 0
+#2 := false
+decl f4 :: S2
+#9 := f4
+decl f3 :: S2
+#8 := f3
+#11 := (distinct f3 f4)
+#12 := (not #11)
+#10 := (= f3 f4)
+#13 := (implies #10 #12)
+#14 := (not #13)
+#54 := (iff #14 false)
+#1 := true
+#49 := (not true)
+#52 := (iff #49 false)
+#53 := [rewrite]: #52
+#50 := (iff #14 #49)
+#47 := (iff #13 true)
+#42 := (implies #10 #10)
+#45 := (iff #42 true)
+#46 := [rewrite]: #45
+#43 := (iff #13 #42)
+#40 := (iff #12 #10)
+#32 := (not #10)
+#35 := (not #32)
+#38 := (iff #35 #10)
+#39 := [rewrite]: #38
+#36 := (iff #12 #35)
+#33 := (iff #11 #32)
+#34 := [rewrite]: #33
+#37 := [monotonicity #34]: #36
+#41 := [trans #37 #39]: #40
+#44 := [monotonicity #41]: #43
+#48 := [trans #44 #46]: #47
+#51 := [monotonicity #48]: #50
+#55 := [trans #51 #53]: #54
+#31 := [asserted]: #14
+[mp #31 #55]: false
+unsat
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Wed Nov 24 10:42:28 2010 +0100
@@ -104,15 +104,15 @@
by smt+
lemma
- "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]"
+ "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]"
by smt+
lemma
@@ -193,7 +193,7 @@
by smt+
lemma
- "SMT.distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
+ "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"
- "SMT.distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
+ "distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
by smt+
--- a/src/HOL/Tools/SMT/smt_builtin.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Wed Nov 24 10:42:28 2010 +0100
@@ -53,7 +53,8 @@
(@{const_name If}, K true),
(@{const_name bool.bool_case}, K true),
(@{const_name Let}, K true),
- (@{const_name SMT.distinct}, K true),
+ (* (@{const_name distinct}, K true), -- not a real builtin, only when
+ applied to an explicit list *)
(* technicalities *)
(@{const_name SMT.pat}, K true),
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 24 10:42:28 2010 +0100
@@ -39,18 +39,18 @@
three elements in the argument list) *)
local
- 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."))
+ fun is_trivial_distinct (Const (@{const_name distinct}, _) $ t) =
+ (case try HOLogic.dest_list t of
+ SOME [] => true
+ | SOME [_] => true
+ | _ => false)
| is_trivial_distinct _ = false
val thms = map mk_meta_eq @{lemma
- "SMT.distinct [] = True"
- "SMT.distinct [x] = True"
- "SMT.distinct [x, y] = (x ~= y)"
- by (simp_all add: distinct_def)}
+ "distinct [] = True"
+ "distinct [x] = True"
+ "distinct [x, y] = (x ~= y)"
+ by simp_all}
fun distinct_conv _ =
U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
in
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 24 10:42:28 2010 +0100
@@ -194,6 +194,10 @@
| is_builtin_conn' (@{const_name False}, _) = false
| is_builtin_conn' c = is_builtin_conn c
+ fun is_builtin_pred' ctxt (@{const_name distinct}, _) [t] =
+ is_builtin_distinct andalso can HOLogic.dest_list t
+ | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
+
val propT = @{typ prop} and boolT = @{typ bool}
val as_propT = (fn @{typ bool} => propT | T => T)
fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
@@ -213,7 +217,7 @@
(c as Const (@{const_name If}, _), [t1, t2, t3]) =>
c $ in_form t1 $ in_term t2 $ in_term t3
| (h as Const c, ts) =>
- if is_builtin_conn' (conn c) orelse is_builtin_pred ctxt (pred c)
+ if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
then wrap_in_if (in_form t)
else Term.list_comb (h, map in_term ts)
| (h as Free _, ts) => Term.list_comb (h, map in_term ts)
@@ -237,8 +241,9 @@
(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 SMT.distinct}, T)), [t']) =>
- if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
+ | (Const (c as (@{const_name distinct}, T)), [t']) =>
+ if is_builtin_distinct andalso can HOLogic.dest_list t' then
+ Const (pred c) $ in_list T in_term t'
else as_term (in_term t)
| (Const c, ts) =>
if is_builtin_conn (conn c)
@@ -381,10 +386,10 @@
| (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 SMT.distinct}, T)), [t1]) =>
- (case builtin_fun ctxt c (HOLogic.dest_list t1) of
+ | (h as Const (c as (@{const_name distinct}, T)), ts) =>
+ (case builtin_fun ctxt c ts of
SOME (n, ts) => fold_map trans ts #>> app n
- | NONE => transs h T [t1])
+ | NONE => transs h T ts)
| (h as Const (c as (_, T)), ts) =>
(case try HOLogic.dest_number t of
SOME (T, i) =>
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Nov 24 10:42:28 2010 +0100
@@ -167,8 +167,11 @@
| conn @{const_name If} = SOME "if_then_else"
| conn _ = NONE
-fun pred @{const_name SMT.distinct} _ = SOME "distinct"
- | pred @{const_name HOL.eq} _ = SOME "="
+fun distinct_pred (@{const_name distinct}, _) [t] =
+ try HOLogic.dest_list t |> Option.map (pair "distinct")
+ | distinct_pred _ _ = NONE
+
+fun pred @{const_name HOL.eq} _ = SOME "="
| pred @{const_name term_eq} _ = SOME "="
| pred @{const_name less} T = if_int_type T "<"
| pred @{const_name less_eq} T = if_int_type T "<="
@@ -192,7 +195,10 @@
fun builtin_fun ctxt (c as (n, T)) ts =
let
val builtin_func' = chained_builtin_func (get_builtins ctxt)
- val builtin_pred' = chained_builtin_pred (get_builtins ctxt)
+ fun builtin_pred' c t =
+ (case distinct_pred c ts of
+ SOME b => SOME b
+ | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
in
if is_connT T then conn n |> Option.map (rpair ts)
else if is_predT T then
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 24 10:42:28 2010 +0100
@@ -182,7 +182,7 @@
fun mk_list cT cts =
fold_rev (Thm.mk_binop (U.instT cT cons_term)) cts (U.instT cT nil_term)
-val distinct = U.mk_const_pat @{theory} @{const_name SMT.distinct}
+val distinct = U.mk_const_pat @{theory} @{const_name distinct}
(U.destT1 o U.destT1)
fun mk_distinct [] = mk_true
| mk_distinct (cts as (ct :: _)) =
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 24 10:42:28 2010 +0100
@@ -308,14 +308,14 @@
prove disjI3 (L.negate ct2, false) (ct1, false)
| @{const HOL.disj} $ _ $ _ =>
prove disjI2 (L.negate ct1, false) (ct2, true)
- | Const (@{const_name SMT.distinct}, _) $ _ =>
+ | Const (@{const_name 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
- | @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
+ | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
fun prv cu =
@@ -481,12 +481,14 @@
(case Term.head_of (Thm.term_of cl) of
@{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
| @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
- | Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
+ | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
| _ => prove (prove_eq_safe f)) cp
in
fun monotonicity eqs ct =
let
- val lookup = AList.lookup (op aconv) (map (`Thm.prop_of o meta_eq_of) eqs)
+ fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
+ val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
+ val lookup = AList.lookup (op aconv) teqs
val cp = Thm.dest_binop (Thm.dest_arg ct)
in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
end
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 24 10:23:52 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 24 10:42:28 2010 +0100
@@ -197,7 +197,7 @@
| @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
| @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
- | Const (@{const_name SMT.distinct}, _) $ _ =>
+ | Const (@{const_name distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
else fresh_abstraction cvs ct
| Const (@{const_name If}, _) $ _ $ _ $ _ =>
@@ -258,9 +258,9 @@
(Conv.rewrs_conv [set1, set2, set3, set4] else_conv
(Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
- 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"
+ val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
+ val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
+ val dist3 = @{lemma "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