re-implemented support for datatypes (including records and typedefs);
authorboehmes
Mon Jan 03 16:22:08 2011 +0100 (2011-01-03)
changeset 4142609615ed31f04
parent 41424 7ee22760436c
child 41427 5fbad0390649
re-implemented support for datatypes (including records and typedefs);
added test cases for datatypes, records and typedefs
src/HOL/IsaMakefile
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/Datatype/datatype_selectors.ML
src/HOL/Tools/SMT/smt_datatypes.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
     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 +    fun is_decl_typ T = exists (exists (equal T o fst)) declss
    6.25 +
    6.26 +    fun add_typ' T proper =
    6.27 +      (case SMT_Builtin.dest_builtin_typ ctxt' T of
    6.28 +        SOME n => pair n
    6.29 +      | NONE => add_typ T proper)
    6.30  
    6.31 -end
    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 =