1.1 --- a/src/HOL/IsaMakefile Fri Dec 31 00:11:24 2010 +0100
1.2 +++ b/src/HOL/IsaMakefile Mon Jan 03 16:22:08 2011 +0100
1.3 @@ -297,7 +297,6 @@
1.4 Tools/ATP/atp_systems.ML \
1.5 Tools/choice_specification.ML \
1.6 Tools/code_evaluation.ML \
1.7 - Tools/Datatype/datatype_selectors.ML \
1.8 Tools/int_arith.ML \
1.9 Tools/groebner.ML \
1.10 Tools/list_code.ML \
1.11 @@ -356,6 +355,7 @@
1.12 Tools/SMT/smtlib_interface.ML \
1.13 Tools/SMT/smt_builtin.ML \
1.14 Tools/SMT/smt_config.ML \
1.15 + Tools/SMT/smt_datatypes.ML \
1.16 Tools/SMT/smt_failure.ML \
1.17 Tools/SMT/smt_monomorph.ML \
1.18 Tools/SMT/smt_normalize.ML \
2.1 --- a/src/HOL/SMT.thy Fri Dec 31 00:11:24 2010 +0100
2.2 +++ b/src/HOL/SMT.thy Mon Jan 03 16:22:08 2011 +0100
2.3 @@ -5,14 +5,14 @@
2.4 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
2.5
2.6 theory SMT
2.7 -imports List
2.8 +imports Record
2.9 uses
2.10 - "Tools/Datatype/datatype_selectors.ML"
2.11 "Tools/SMT/smt_utils.ML"
2.12 "Tools/SMT/smt_failure.ML"
2.13 "Tools/SMT/smt_config.ML"
2.14 ("Tools/SMT/smt_monomorph.ML")
2.15 ("Tools/SMT/smt_builtin.ML")
2.16 + ("Tools/SMT/smt_datatypes.ML")
2.17 ("Tools/SMT/smt_normalize.ML")
2.18 ("Tools/SMT/smt_translate.ML")
2.19 ("Tools/SMT/smt_solver.ML")
2.20 @@ -123,7 +123,6 @@
2.21
2.22
2.23
2.24 -
2.25 subsection {* Integer division and modulo for Z3 *}
2.26
2.27 definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
2.28 @@ -138,6 +137,7 @@
2.29
2.30 use "Tools/SMT/smt_monomorph.ML"
2.31 use "Tools/SMT/smt_builtin.ML"
2.32 +use "Tools/SMT/smt_datatypes.ML"
2.33 use "Tools/SMT/smt_normalize.ML"
2.34 use "Tools/SMT/smt_translate.ML"
2.35 use "Tools/SMT/smt_solver.ML"
2.36 @@ -380,13 +380,4 @@
2.37 hide_const Pattern fun_app term_true term_false z3div z3mod
2.38 hide_const (open) trigger pat nopat weight
2.39
2.40 -
2.41 -
2.42 -subsection {* Selectors for datatypes *}
2.43 -
2.44 -setup {* Datatype_Selectors.setup *}
2.45 -
2.46 -declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
2.47 -declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
2.48 -
2.49 end
3.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy Fri Dec 31 00:11:24 2010 +0100
3.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Mon Jan 03 16:22:08 2011 +0100
3.3 @@ -607,7 +607,11 @@
3.4
3.5
3.6
3.7 -section {* Pairs *} (* FIXME: tests for datatypes and records *)
3.8 +section {* Datatypes, Records, and Typedefs *}
3.9 +
3.10 +subsection {* Without support by the SMT solver *}
3.11 +
3.12 +subsubsection {* Algebraic datatypes *}
3.13
3.14 lemma
3.15 "x = fst (x, y)"
3.16 @@ -625,6 +629,252 @@
3.17 using fst_conv snd_conv pair_collapse
3.18 by smt+
3.19
3.20 +lemma
3.21 + "[x] \<noteq> Nil"
3.22 + "[x, y] \<noteq> Nil"
3.23 + "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]"
3.24 + "hd (x # xs) = x"
3.25 + "tl (x # xs) = xs"
3.26 + "hd [x, y, z] = x"
3.27 + "tl [x, y, z] = [y, z]"
3.28 + "hd (tl [x, y, z]) = y"
3.29 + "tl (tl [x, y, z]) = [z]"
3.30 + using hd.simps tl.simps(2) list.simps
3.31 + by smt+
3.32 +
3.33 +lemma
3.34 + "fst (hd [(a, b)]) = a"
3.35 + "snd (hd [(a, b)]) = b"
3.36 + using fst_conv snd_conv pair_collapse hd.simps tl.simps(2) list.simps
3.37 + by smt+
3.38 +
3.39 +
3.40 +subsubsection {* Records *}
3.41 +
3.42 +record point =
3.43 + x :: int
3.44 + y :: int
3.45 +
3.46 +record bw_point = point +
3.47 + black :: bool
3.48 +
3.49 +lemma
3.50 + "p1 = p2 \<longrightarrow> x p1 = x p2"
3.51 + "p1 = p2 \<longrightarrow> y p1 = y p2"
3.52 + "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2"
3.53 + "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2"
3.54 + using point.simps
3.55 + by smt+
3.56 +
3.57 +lemma
3.58 + "x \<lparr> x = 3, y = 4 \<rparr> = 3"
3.59 + "y \<lparr> x = 3, y = 4 \<rparr> = 4"
3.60 + "x \<lparr> x = 3, y = 4 \<rparr> \<noteq> y \<lparr> x = 3, y = 4 \<rparr>"
3.61 + "\<lparr> x = 3, y = 4 \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4 \<rparr>"
3.62 + "\<lparr> x = 3, y = 4 \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6 \<rparr>"
3.63 + "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p"
3.64 + "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr> = p"
3.65 + using point.simps
3.66 + using [[z3_options="AUTO_CONFIG=false"]]
3.67 + by smt+
3.68 +
3.69 +lemma
3.70 + "y (p \<lparr> x := a \<rparr>) = y p"
3.71 + "x (p \<lparr> y := a \<rparr>) = x p"
3.72 + "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>"
3.73 + sorry
3.74 +
3.75 +lemma
3.76 + "p1 = p2 \<longrightarrow> x p1 = x p2"
3.77 + "p1 = p2 \<longrightarrow> y p1 = y p2"
3.78 + "p1 = p2 \<longrightarrow> black p1 = black p2"
3.79 + "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2"
3.80 + "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2"
3.81 + "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
3.82 + using point.simps bw_point.simps
3.83 + by smt+
3.84 +
3.85 +lemma
3.86 + "x \<lparr> x = 3, y = 4, black = b \<rparr> = 3"
3.87 + "y \<lparr> x = 3, y = 4, black = b \<rparr> = 4"
3.88 + "black \<lparr> x = 3, y = 4, black = b \<rparr> = b"
3.89 + "x \<lparr> x = 3, y = 4, black = b \<rparr> \<noteq> y \<lparr> x = 3, y = 4, black = b \<rparr>"
3.90 + "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4, black = b \<rparr>"
3.91 + "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6, black = b \<rparr>"
3.92 + "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> x = 3, y = 4, black = w \<rparr>"
3.93 + "\<lparr> x = 3, y = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
3.94 + \<lparr> x = 3, y = 4, black = False \<rparr>"
3.95 + "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow>
3.96 + p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> = p"
3.97 + "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow>
3.98 + p \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> = p"
3.99 + "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow>
3.100 + p \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p"
3.101 + using point.simps bw_point.simps
3.102 + using [[z3_options="AUTO_CONFIG=false"]]
3.103 + by smt+
3.104 +
3.105 +lemma
3.106 + "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> =
3.107 + p \<lparr> black := True \<rparr> \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>"
3.108 + sorry
3.109 +
3.110 +
3.111 +subsubsection {* Type definitions *}
3.112 +
3.113 +typedef three = "{1, 2, 3::int}" by auto
3.114 +
3.115 +definition n1 where "n1 = Abs_three 1"
3.116 +definition n2 where "n2 = Abs_three 2"
3.117 +definition n3 where "n3 = Abs_three 3"
3.118 +definition nplus where "nplus n m = Abs_three (Rep_three n + Rep_three m)"
3.119 +
3.120 +lemma three_def': "(x \<in> three) = (x = 1 \<or> x = 2 \<or> x = 3)"
3.121 + by (auto simp add: three_def)
3.122 +
3.123 +lemma
3.124 + "n1 = n1"
3.125 + "n2 = n2"
3.126 + "n1 \<noteq> n2"
3.127 + "nplus n1 n1 = n2"
3.128 + "nplus n1 n2 = n3"
3.129 + using n1_def n2_def n3_def nplus_def
3.130 + using three_def' Rep_three Abs_three_inverse
3.131 + using [[z3_options="AUTO_CONFIG=false"]]
3.132 + by smt+
3.133 +
3.134 +
3.135 +subsection {* With support by the SMT solver (but without proofs) *}
3.136 +
3.137 +subsubsection {* Algebraic datatypes *}
3.138 +
3.139 +lemma
3.140 + "x = fst (x, y)"
3.141 + "y = snd (x, y)"
3.142 + "((x, y) = (y, x)) = (x = y)"
3.143 + "((x, y) = (u, v)) = (x = u \<and> y = v)"
3.144 + "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
3.145 + "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)"
3.146 + "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
3.147 + "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
3.148 + "(fst (x, y) = snd (x, y)) = (x = y)"
3.149 + "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
3.150 + "(fst (x, y) = snd (x, y)) = (x = y)"
3.151 + "(fst p = snd p) = (p = (snd p, fst p))"
3.152 + using fst_conv snd_conv pair_collapse
3.153 + using [[smt_datatypes, smt_oracle]]
3.154 + by smt+
3.155 +
3.156 +lemma
3.157 + "[x] \<noteq> Nil"
3.158 + "[x, y] \<noteq> Nil"
3.159 + "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]"
3.160 + "hd (x # xs) = x"
3.161 + "tl (x # xs) = xs"
3.162 + "hd [x, y, z] = x"
3.163 + "tl [x, y, z] = [y, z]"
3.164 + "hd (tl [x, y, z]) = y"
3.165 + "tl (tl [x, y, z]) = [z]"
3.166 + using hd.simps tl.simps(2)
3.167 + using [[smt_datatypes, smt_oracle]]
3.168 + by smt+
3.169 +
3.170 +lemma
3.171 + "fst (hd [(a, b)]) = a"
3.172 + "snd (hd [(a, b)]) = b"
3.173 + using fst_conv snd_conv pair_collapse hd.simps tl.simps(2)
3.174 + using [[smt_datatypes, smt_oracle]]
3.175 + by smt+
3.176 +
3.177 +
3.178 +subsubsection {* Records *}
3.179 +
3.180 +lemma
3.181 + "p1 = p2 \<longrightarrow> x p1 = x p2"
3.182 + "p1 = p2 \<longrightarrow> y p1 = y p2"
3.183 + "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2"
3.184 + "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2"
3.185 + using point.simps
3.186 + using [[smt_datatypes, smt_oracle]]
3.187 + using [[z3_options="AUTO_CONFIG=false"]]
3.188 + by smt+
3.189 +
3.190 +lemma
3.191 + "x \<lparr> x = 3, y = 4 \<rparr> = 3"
3.192 + "y \<lparr> x = 3, y = 4 \<rparr> = 4"
3.193 + "x \<lparr> x = 3, y = 4 \<rparr> \<noteq> y \<lparr> x = 3, y = 4 \<rparr>"
3.194 + "\<lparr> x = 3, y = 4 \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4 \<rparr>"
3.195 + "\<lparr> x = 3, y = 4 \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6 \<rparr>"
3.196 + "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p"
3.197 + "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr> = p"
3.198 + using point.simps
3.199 + using [[smt_datatypes, smt_oracle]]
3.200 + using [[z3_options="AUTO_CONFIG=false"]]
3.201 + by smt+
3.202 +
3.203 +lemma
3.204 + "y (p \<lparr> x := a \<rparr>) = y p"
3.205 + "x (p \<lparr> y := a \<rparr>) = x p"
3.206 + "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>"
3.207 + using point.simps
3.208 + using [[smt_datatypes, smt_oracle]]
3.209 + using [[z3_options="AUTO_CONFIG=false"]]
3.210 + by smt+
3.211 +
3.212 +lemma
3.213 + "p1 = p2 \<longrightarrow> x p1 = x p2"
3.214 + "p1 = p2 \<longrightarrow> y p1 = y p2"
3.215 + "p1 = p2 \<longrightarrow> black p1 = black p2"
3.216 + "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2"
3.217 + "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2"
3.218 + "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
3.219 + using point.simps bw_point.simps
3.220 + using [[smt_datatypes, smt_oracle]]
3.221 + by smt+
3.222 +
3.223 +lemma
3.224 + "x \<lparr> x = 3, y = 4, black = b \<rparr> = 3"
3.225 + "y \<lparr> x = 3, y = 4, black = b \<rparr> = 4"
3.226 + "black \<lparr> x = 3, y = 4, black = b \<rparr> = b"
3.227 + "x \<lparr> x = 3, y = 4, black = b \<rparr> \<noteq> y \<lparr> x = 3, y = 4, black = b \<rparr>"
3.228 + "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4, black = b \<rparr>"
3.229 + "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6, black = b \<rparr>"
3.230 + "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> x = 3, y = 4, black = w \<rparr>"
3.231 + "\<lparr> x = 3, y = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
3.232 + \<lparr> x = 3, y = 4, black = False \<rparr>"
3.233 + "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow>
3.234 + p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> = p"
3.235 + "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow>
3.236 + p \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> = p"
3.237 + "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow>
3.238 + p \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p"
3.239 + using point.simps bw_point.simps
3.240 + using [[smt_datatypes, smt_oracle]]
3.241 + using [[z3_options="AUTO_CONFIG=false"]]
3.242 + by smt+
3.243 +
3.244 +lemma
3.245 + "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> =
3.246 + p \<lparr> black := True \<rparr> \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>"
3.247 + using point.simps bw_point.simps
3.248 + using [[smt_datatypes, smt_oracle]]
3.249 + using [[z3_options="AUTO_CONFIG=false"]]
3.250 + by smt
3.251 +
3.252 +
3.253 +subsubsection {* Type definitions *}
3.254 +
3.255 +lemma
3.256 + "n1 = n1"
3.257 + "n2 = n2"
3.258 + "n1 \<noteq> n2"
3.259 + "nplus n1 n1 = n2"
3.260 + "nplus n1 n2 = n3"
3.261 + using n1_def n2_def n3_def nplus_def
3.262 + using [[smt_datatypes, smt_oracle]]
3.263 + using [[z3_options="AUTO_CONFIG=false"]]
3.264 + by smt+
3.265 +
3.266
3.267
3.268 section {* Function updates *}
4.1 --- a/src/HOL/Tools/Datatype/datatype_selectors.ML Fri Dec 31 00:11:24 2010 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,83 +0,0 @@
4.4 -(* Title: HOL/Tools/Datatype/datatype_selectors.ML
4.5 - Author: Sascha Boehme, TU Muenchen
4.6 -
4.7 -Selector functions for datatype constructor arguments.
4.8 -*)
4.9 -
4.10 -signature DATATYPE_SELECTORS =
4.11 -sig
4.12 - val add_selector: ((string * typ) * int) * (string * typ) ->
4.13 - Context.generic -> Context.generic
4.14 - val lookup_selector: Proof.context -> string * int -> string option
4.15 - val setup: theory -> theory
4.16 -end
4.17 -
4.18 -structure Datatype_Selectors: DATATYPE_SELECTORS =
4.19 -struct
4.20 -
4.21 -structure Stringinttab = Table
4.22 -(
4.23 - type key = string * int
4.24 - val ord = prod_ord fast_string_ord int_ord
4.25 -)
4.26 -
4.27 -structure Data = Generic_Data
4.28 -(
4.29 - type T = string Stringinttab.table
4.30 - val empty = Stringinttab.empty
4.31 - val extend = I
4.32 - fun merge data : T = Stringinttab.merge (K true) data
4.33 -)
4.34 -
4.35 -fun pretty_term context = Syntax.pretty_term (Context.proof_of context)
4.36 -
4.37 -fun sanity_check context (((con as (n, _), i), sel as (m, _))) =
4.38 - let
4.39 - val thy = Context.theory_of context
4.40 - val varify_const =
4.41 - Const #> Type.varify_global [] #> snd #> Term.dest_Const #>
4.42 - snd #> Term.strip_type
4.43 -
4.44 - val (Ts, T) = varify_const con
4.45 - val (Us, U) = varify_const sel
4.46 - val _ = (0 < i andalso i <= length Ts) orelse
4.47 - error (Pretty.string_of (Pretty.block [
4.48 - Pretty.str "The constructor ",
4.49 - Pretty.quote (pretty_term context (Const con)),
4.50 - Pretty.str " has no argument position ",
4.51 - Pretty.str (string_of_int i),
4.52 - Pretty.str "."]))
4.53 - val _ = length Us = 1 orelse
4.54 - error (Pretty.string_of (Pretty.block [
4.55 - Pretty.str "The term ", Pretty.quote (pretty_term context (Const sel)),
4.56 - Pretty.str " might not be a selector ",
4.57 - Pretty.str "(it accepts more than one argument)."]))
4.58 - val _ =
4.59 - (Sign.typ_equiv thy (T, hd Us) andalso
4.60 - Sign.typ_equiv thy (nth Ts (i-1), U)) orelse
4.61 - error (Pretty.string_of (Pretty.block [
4.62 - Pretty.str "The types of the constructor ",
4.63 - Pretty.quote (pretty_term context (Const con)),
4.64 - Pretty.str " and of the selector ",
4.65 - Pretty.quote (pretty_term context (Const sel)),
4.66 - Pretty.str " do not fit to each other."]))
4.67 - in ((n, i), m) end
4.68 -
4.69 -fun add_selector (entry as ((con as (n, _), i), (_, T))) context =
4.70 - (case Stringinttab.lookup (Data.get context) (n, i) of
4.71 - NONE => Data.map (Stringinttab.update (sanity_check context entry)) context
4.72 - | SOME c => error (Pretty.string_of (Pretty.block [
4.73 - Pretty.str "There is already a selector assigned to constructor ",
4.74 - Pretty.quote (pretty_term context (Const con)), Pretty.str ", namely ",
4.75 - Pretty.quote (pretty_term context (Const (c, T))), Pretty.str "."])))
4.76 -
4.77 -fun lookup_selector ctxt = Stringinttab.lookup (Data.get (Context.Proof ctxt))
4.78 -
4.79 -val setup =
4.80 - Attrib.setup @{binding selector}
4.81 - ((Args.term >> Term.dest_Const) -- Scan.lift (Parse.nat) --|
4.82 - Scan.lift (Parse.$$$ "=") -- (Args.term >> Term.dest_Const) >>
4.83 - (Thm.declaration_attribute o K o add_selector))
4.84 - "assign a selector function to a datatype constructor argument"
4.85 -
4.86 -end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Mon Jan 03 16:22:08 2011 +0100
5.3 @@ -0,0 +1,126 @@
5.4 +(* Title: HOL/Tools/SMT/smt_datatypes.ML
5.5 + Author: Sascha Boehme, TU Muenchen
5.6 +
5.7 +Collector functions for common type declarations and their representation
5.8 +as algebraic datatypes.
5.9 +*)
5.10 +
5.11 +signature SMT_DATATYPES =
5.12 +sig
5.13 + val add_decls: typ ->
5.14 + (typ * (term * term list) list) list list * Proof.context ->
5.15 + (typ * (term * term list) list) list list * Proof.context
5.16 +end
5.17 +
5.18 +structure SMT_Datatypes: SMT_DATATYPES =
5.19 +struct
5.20 +
5.21 +val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of
5.22 +
5.23 +fun mk_selectors T Ts ctxt =
5.24 + let
5.25 + val (sels, ctxt') =
5.26 + Variable.variant_fixes (replicate (length Ts) "select") ctxt
5.27 + in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
5.28 +
5.29 +
5.30 +(* datatype declarations *)
5.31 +
5.32 +fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt =
5.33 + let
5.34 + fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE
5.35 + val vars = the (get_first get_vars descr) ~~ Ts
5.36 + val lookup_var = the o AList.lookup (op =) vars
5.37 +
5.38 + val dTs = map (apsnd (fn (m, vs, _) => Type (m, map lookup_var vs))) descr
5.39 + val lookup_typ = the o AList.lookup (op =) dTs
5.40 +
5.41 + fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
5.42 + | typ_of (Datatype.DtType (n, dts)) = Type (n, map typ_of dts)
5.43 + | typ_of (Datatype.DtRec i) = lookup_typ i
5.44 +
5.45 + fun mk_constr T (m, dts) ctxt =
5.46 + let
5.47 + val Ts = map typ_of dts
5.48 + val constr = Const (m, Ts ---> T)
5.49 + val (selects, ctxt') = mk_selectors T Ts ctxt
5.50 + in ((constr, selects), ctxt') end
5.51 +
5.52 + fun mk_decl (i, (_, _, constrs)) ctxt =
5.53 + let
5.54 + val T = lookup_typ i
5.55 + val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
5.56 + in ((T, css), ctxt') end
5.57 +
5.58 + in fold_map mk_decl descr ctxt end
5.59 +
5.60 +
5.61 +(* record declarations *)
5.62 +
5.63 +val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode
5.64 +
5.65 +fun get_record_decl ({ext_def, ...} : Record.info) T ctxt =
5.66 + let
5.67 + val (con, _) = Term.dest_Const (lhs_head_of ext_def)
5.68 + val (fields, more) = Record.get_extT_fields (ProofContext.theory_of ctxt) T
5.69 + val fieldTs = map snd fields @ [snd more]
5.70 +
5.71 + val constr = Const (con, fieldTs ---> T)
5.72 + val (selects, ctxt') = mk_selectors T fieldTs ctxt
5.73 + in ((T, [(constr, selects)]), ctxt') end
5.74 +
5.75 +
5.76 +(* typedef declarations *)
5.77 +
5.78 +fun get_typedef_decl (info : Typedef.info) T Ts =
5.79 + let
5.80 + val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info
5.81 +
5.82 + val env = snd (Term.dest_Type abs_type) ~~ Ts
5.83 + val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
5.84 +
5.85 + val constr = Const (Abs_name, instT (rep_type --> abs_type))
5.86 + val select = Const (Rep_name, instT (abs_type --> rep_type))
5.87 + in (T, [(constr, [select])]) end
5.88 +
5.89 +
5.90 +(* collection of declarations *)
5.91 +
5.92 +fun declared declss T = exists (exists (equal T o fst)) declss
5.93 +
5.94 +fun get_decls T n Ts ctxt =
5.95 + let val thy = ProofContext.theory_of ctxt
5.96 + in
5.97 + (case Datatype.get_info thy n of
5.98 + SOME info => get_datatype_decl info n Ts ctxt
5.99 + | NONE =>
5.100 + (case Record.get_info thy (record_name_of n) of
5.101 + SOME info => get_record_decl info T ctxt |>> single
5.102 + | NONE =>
5.103 + (case Typedef.get_info ctxt n of
5.104 + [] => ([], ctxt)
5.105 + | info :: _ => ([get_typedef_decl info T Ts], ctxt))))
5.106 + end
5.107 +
5.108 +fun add_decls T (declss, ctxt) =
5.109 + let
5.110 + fun add (TFree _) = I
5.111 + | add (TVar _) = I
5.112 + | add (T as Type (@{type_name fun}, _)) =
5.113 + fold add (Term.body_type T :: Term.binder_types T)
5.114 + | add @{typ bool} = I
5.115 + | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
5.116 + if declared declss T orelse declared dss T then (dss, ctxt1)
5.117 + else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
5.118 + else
5.119 + (case get_decls T n Ts ctxt1 of
5.120 + ([], _) => (dss, ctxt1)
5.121 + | (ds, ctxt2) =>
5.122 + let
5.123 + val constrTs =
5.124 + maps (map (snd o Term.dest_Const o fst) o snd) ds
5.125 + val Us = fold (union (op =) o Term.binder_types) constrTs []
5.126 + in fold add Us (ds :: dss, ctxt2) end))
5.127 + in add T ([], ctxt) |>> append declss end
5.128 +
5.129 +end
6.1 --- a/src/HOL/Tools/SMT/smt_translate.ML Fri Dec 31 00:11:24 2010 +0100
6.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Jan 03 16:22:08 2011 +0100
6.3 @@ -134,20 +134,35 @@
6.4
6.5 (* preprocessing *)
6.6
6.7 -(** FIXME **)
6.8 -
6.9 -local
6.10 - (*
6.11 - force eta-expansion for constructors and selectors,
6.12 - add missing datatype selectors via hypothetical definitions,
6.13 - also return necessary datatype and record theorems
6.14 - *)
6.15 -in
6.16 +(** datatype declarations **)
6.17
6.18 fun collect_datatypes_and_records (tr_context, ctxt) ts =
6.19 - (([], tr_context, ctxt), ts)
6.20 + let
6.21 + val (declss, ctxt') =
6.22 + fold (Term.fold_types SMT_Datatypes.add_decls) ts ([], ctxt)
6.23
6.24 -end
6.25 + fun is_decl_typ T = exists (exists (equal T o fst)) declss
6.26 +
6.27 + fun add_typ' T proper =
6.28 + (case SMT_Builtin.dest_builtin_typ ctxt' T of
6.29 + SOME n => pair n
6.30 + | NONE => add_typ T proper)
6.31 +
6.32 + fun tr_select sel =
6.33 + let val T = Term.range_type (Term.fastype_of sel)
6.34 + in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end
6.35 + fun tr_constr (constr, selects) =
6.36 + add_fun constr NONE ##>> fold_map tr_select selects
6.37 + fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases
6.38 + val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context
6.39 +
6.40 + fun add (constr, selects) =
6.41 + Termtab.update (constr, length selects) #>
6.42 + fold (Termtab.update o rpair 1) selects
6.43 + val funcs = fold (fold (fold add o snd)) declss Termtab.empty
6.44 +
6.45 + in ((funcs, declss', tr_context', ctxt'), ts) end
6.46 + (* FIXME: also return necessary datatype and record theorems *)
6.47
6.48
6.49 (** eta-expand quantifiers, let expressions and built-ins *)
6.50 @@ -174,8 +189,15 @@
6.51 end
6.52 in
6.53
6.54 -fun eta_expand ctxt =
6.55 +fun eta_expand ctxt funcs =
6.56 let
6.57 + fun exp_func t T ts =
6.58 + (case Termtab.lookup funcs t of
6.59 + SOME k =>
6.60 + Term.list_comb (t, ts)
6.61 + |> k <> length ts ? expf k (length ts) T
6.62 + | NONE => Term.list_comb (t, ts))
6.63 +
6.64 fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
6.65 | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
6.66 | expand (q as Const (@{const_name All}, T)) = exp2 T q
6.67 @@ -196,7 +218,8 @@
6.68 SOME (_, k, us, mk) =>
6.69 if k = length us then mk (map expand us)
6.70 else expf k (length ts) T (mk (map expand us))
6.71 - | NONE => Term.list_comb (u, map expand ts))
6.72 + | NONE => exp_func u T (map expand ts))
6.73 + | (u as Free (_, T), ts) => exp_func u T (map expand ts)
6.74 | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts)
6.75 | (u, ts) => Term.list_comb (u, map expand ts))
6.76
6.77 @@ -530,17 +553,18 @@
6.78 val with_datatypes =
6.79 has_datatypes andalso Config.get ctxt SMT_Config.datatypes
6.80
6.81 - fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts)
6.82 + fun no_dtyps (tr_context, ctxt) ts =
6.83 + ((Termtab.empty, [], tr_context, ctxt), ts)
6.84
6.85 val ts1 = map (Envir.beta_eta_contract o SMT_Utils.prop_of o snd) ithms
6.86
6.87 - val ((dtyps, tr_context, ctxt1), ts2) =
6.88 + val ((funcs, dtyps, tr_context, ctxt1), ts2) =
6.89 ((make_tr_context prefixes, ctxt), ts1)
6.90 |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps)
6.91
6.92 val (ctxt2, ts3) =
6.93 ts2
6.94 - |> eta_expand ctxt1
6.95 + |> eta_expand ctxt1 funcs
6.96 |> lift_lambdas ctxt1
6.97 ||> intro_explicit_application
6.98
7.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Dec 31 00:11:24 2010 +0100
7.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Jan 03 16:22:08 2011 +0100
7.3 @@ -130,10 +130,10 @@
7.4
7.5 fun sdatatypes decls =
7.6 let
7.7 - fun con (n, []) = add n
7.8 + fun con (n, []) = sep (add n)
7.9 | con (n, sels) = par (add n #>
7.10 - fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
7.11 - fun dtyp (n, decl) = add n #> fold (sep o con) decl
7.12 + fold (fn (n, s) => par (add n #> sep (add s))) sels)
7.13 + fun dtyp (n, decl) = add n #> fold con decl
7.14 in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
7.15
7.16 fun serialize comments {header, sorts, dtyps, funcs} ts =
8.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Dec 31 00:11:24 2010 +0100
8.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Jan 03 16:22:08 2011 +0100
8.3 @@ -851,7 +851,8 @@
8.4 |> tap (check_after idx r ps prop)
8.5 in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
8.6
8.7 - val disch_rules = [@{thm allI}, @{thm refl}, @{thm reflexive}]
8.8 + val disch_rules = [@{thm allI}, @{thm refl}, @{thm reflexive},
8.9 + Z3_Proof_Literals.true_thm]
8.10 fun all_disch_rules rules = map (pair false) (disch_rules @ rules)
8.11
8.12 fun disch_assm rules thm =