1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed May 12 23:54:02 2010 +0200
1.3 @@ -0,0 +1,368 @@
1.4 +(* Title: HOL/Tools/SMT/z3_proof_tools.ML
1.5 + Author: Sascha Boehme, TU Muenchen
1.6 +
1.7 +Helper functions required for Z3 proof reconstruction.
1.8 +*)
1.9 +
1.10 +signature Z3_PROOF_TOOLS =
1.11 +sig
1.12 + (* accessing and modifying terms *)
1.13 + val term_of: cterm -> term
1.14 + val prop_of: thm -> term
1.15 + val mk_prop: cterm -> cterm
1.16 + val as_meta_eq: cterm -> cterm
1.17 +
1.18 + (* theorem nets *)
1.19 + val thm_net_of: thm list -> thm Net.net
1.20 + val net_instance: thm Net.net -> cterm -> thm option
1.21 +
1.22 + (* proof combinators *)
1.23 + val under_assumption: (thm -> thm) -> cterm -> thm
1.24 + val with_conv: conv -> (cterm -> thm) -> cterm -> thm
1.25 + val discharge: thm -> thm -> thm
1.26 + val varify: string list -> thm -> thm
1.27 + val unfold_eqs: Proof.context -> thm list -> conv
1.28 + val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
1.29 + val by_tac: (int -> tactic) -> cterm -> thm
1.30 + val make_hyp_def: thm -> Proof.context -> thm * Proof.context
1.31 + val by_abstraction: Proof.context -> thm list -> (Proof.context -> cterm ->
1.32 + thm) -> cterm -> thm
1.33 +
1.34 + (* a faster COMP *)
1.35 + type compose_data
1.36 + val precompose: (cterm -> cterm list) -> thm -> compose_data
1.37 + val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
1.38 + val compose: compose_data -> thm -> thm
1.39 +
1.40 + (* unfolding of 'distinct' *)
1.41 + val unfold_distinct_conv: conv
1.42 +
1.43 + (* simpset *)
1.44 + val make_simpset: Proof.context -> thm list -> simpset
1.45 +end
1.46 +
1.47 +structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
1.48 +struct
1.49 +
1.50 +
1.51 +
1.52 +(* accessing terms *)
1.53 +
1.54 +val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
1.55 +
1.56 +fun term_of ct = dest_prop (Thm.term_of ct)
1.57 +fun prop_of thm = dest_prop (Thm.prop_of thm)
1.58 +
1.59 +val mk_prop = Thm.capply @{cterm Trueprop}
1.60 +
1.61 +val (eqT, eq) = `(hd o Thm.dest_ctyp o Thm.ctyp_of_term) @{cpat "op =="}
1.62 +fun mk_meta_eq_cterm ct cu =
1.63 + let val inst = ([(eqT, Thm.ctyp_of_term ct)], [])
1.64 + in Thm.mk_binop (Thm.instantiate_cterm inst eq) ct cu end
1.65 +
1.66 +fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
1.67 +
1.68 +
1.69 +
1.70 +(* theorem nets *)
1.71 +
1.72 +fun thm_net_of thms =
1.73 + let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
1.74 + in fold insert thms Net.empty end
1.75 +
1.76 +fun maybe_instantiate ct thm =
1.77 + try Thm.first_order_match (Thm.cprop_of thm, ct)
1.78 + |> Option.map (fn inst => Thm.instantiate inst thm)
1.79 +
1.80 +fun first_of thms ct = get_first (maybe_instantiate ct) thms
1.81 +fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
1.82 +
1.83 +
1.84 +
1.85 +(* proof combinators *)
1.86 +
1.87 +fun under_assumption f ct =
1.88 + let val ct' = mk_prop ct
1.89 + in Thm.implies_intr ct' (f (Thm.assume ct')) end
1.90 +
1.91 +fun with_conv conv prove ct =
1.92 + let val eq = Thm.symmetric (conv ct)
1.93 + in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
1.94 +
1.95 +fun discharge p pq = Thm.implies_elim pq p
1.96 +
1.97 +fun varify vars = Drule.generalize ([], vars)
1.98 +
1.99 +fun unfold_eqs _ [] = Conv.all_conv
1.100 + | unfold_eqs ctxt eqs =
1.101 + More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
1.102 +
1.103 +fun match_instantiate f ct thm =
1.104 + Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
1.105 +
1.106 +fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
1.107 +
1.108 +(* |- c x == t x ==> P (c x) ~~> c == t |- P (c x) *)
1.109 +fun make_hyp_def thm ctxt =
1.110 + let
1.111 + val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
1.112 + val (cf, cvs) = Drule.strip_comb lhs
1.113 + val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
1.114 + fun apply cv th =
1.115 + Thm.combination th (Thm.reflexive cv)
1.116 + |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
1.117 + in
1.118 + yield_singleton Assumption.add_assumes eq ctxt
1.119 + |>> Thm.implies_elim thm o fold apply cvs
1.120 + end
1.121 +
1.122 +
1.123 +
1.124 +(* abstraction *)
1.125 +
1.126 +local
1.127 +
1.128 +fun typ_of ct = #T (Thm.rep_cterm ct)
1.129 +fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
1.130 +
1.131 +fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
1.132 +
1.133 +fun context_of (ctxt, _, _, _) = ctxt
1.134 +
1.135 +fun replace (cv, ct) = Thm.forall_elim ct o Thm.forall_intr cv
1.136 +
1.137 +fun abs_instantiate (_, tab, _, beta_norm) =
1.138 + fold replace (map snd (Termtab.dest tab)) #>
1.139 + beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
1.140 +
1.141 +fun generalize cvs =
1.142 + let
1.143 + val no_name = ""
1.144 +
1.145 + fun dest (Free (n, _)) = n
1.146 + | dest _ = no_name
1.147 +
1.148 + fun gen vs (t as Free (n, _)) =
1.149 + let val i = find_index (equal n) vs
1.150 + in
1.151 + if i >= 0 then insert (op aconvc) (nth cvs i) #> pair (Bound i)
1.152 + else pair t
1.153 + end
1.154 + | gen vs (t $ u) = gen vs t ##>> gen vs u #>> (op $)
1.155 + | gen vs (Abs (n, T, t)) =
1.156 + gen (no_name :: vs) t #>> (fn u => Abs (n, T, u))
1.157 + | gen _ t = pair t
1.158 +
1.159 + in (fn ct => gen (map (dest o Thm.term_of) cvs) (Thm.term_of ct) []) end
1.160 +
1.161 +fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) =
1.162 + let val (t, cvs') = generalize cvs ct
1.163 + in
1.164 + (case Termtab.lookup tab t of
1.165 + SOME (cv, _) => (cv, cx)
1.166 + | NONE =>
1.167 + let
1.168 + val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
1.169 + val cv = certify ctxt (Free (n, map typ_of cvs' ---> typ_of ct))
1.170 + val cv' = Drule.list_comb (cv, cvs')
1.171 + val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
1.172 + val beta_norm' = beta_norm orelse not (null cvs')
1.173 + in (cv', (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
1.174 + end
1.175 +
1.176 +fun abs_arg f cvs ct =
1.177 + let val (cf, cu) = Thm.dest_comb ct
1.178 + in f cvs cu #>> Thm.capply cf end
1.179 +
1.180 +fun abs_comb f g cvs ct =
1.181 + let val (cf, cu) = Thm.dest_comb ct
1.182 + in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
1.183 +
1.184 +fun abs_list f g cvs ct =
1.185 + (case Thm.term_of ct of
1.186 + Const (@{const_name Nil}, _) => pair ct
1.187 + | Const (@{const_name Cons}, _) $ _ $ _ =>
1.188 + abs_comb (abs_arg f) (abs_list f g) cvs ct
1.189 + | _ => g cvs ct)
1.190 +
1.191 +fun abs_abs f cvs ct =
1.192 + let val (cv, cu) = Thm.dest_abs NONE ct
1.193 + in f (cv :: cvs) cu #>> Thm.cabs cv end
1.194 +
1.195 +val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
1.196 +val is_arithT = (fn @{typ int} => true | @{typ real} => true | _ => false)
1.197 +fun is_number t =
1.198 + (case try HOLogic.dest_number t of
1.199 + SOME (T, _) => is_arithT T
1.200 + | NONE => false)
1.201 +
1.202 +fun abstract (ext_logic, with_theories) =
1.203 + let
1.204 + fun abstr1 cvs ct = abs_arg abstr cvs ct
1.205 + and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
1.206 + and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
1.207 + and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
1.208 +
1.209 + and abstr cvs ct =
1.210 + (case Thm.term_of ct of
1.211 + @{term Trueprop} $ _ => abstr1 cvs ct
1.212 + | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
1.213 + | @{term True} => pair ct
1.214 + | @{term False} => pair ct
1.215 + | @{term Not} $ _ => abstr1 cvs ct
1.216 + | @{term "op &"} $ _ $ _ => abstr2 cvs ct
1.217 + | @{term "op |"} $ _ $ _ => abstr2 cvs ct
1.218 + | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
1.219 + | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
1.220 + | Const (@{const_name distinct}, _) $ _ =>
1.221 + if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
1.222 + else fresh_abstraction cvs ct
1.223 + | Const (@{const_name If}, _) $ _ $ _ $ _ =>
1.224 + if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
1.225 + | Const (@{const_name All}, _) $ _ =>
1.226 + if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
1.227 + | Const (@{const_name Ex}, _) $ _ =>
1.228 + if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
1.229 + | @{term "uminus :: int => _"} $ _ => abstr1 cvs ct
1.230 + | @{term "uminus :: real => _"} $ _ => abstr1 cvs ct
1.231 + | @{term "op + :: int => _"} $ _ $ _ => abstr2 cvs ct
1.232 + | @{term "op + :: real => _"} $ _ $ _ => abstr2 cvs ct
1.233 + | @{term "op - :: int => _"} $ _ $ _ => abstr2 cvs ct
1.234 + | @{term "op - :: real => _"} $ _ $ _ => abstr2 cvs ct
1.235 + | @{term "op * :: int => _"} $ _ $ _ => abstr2 cvs ct
1.236 + | @{term "op * :: real => _"} $ _ $ _ => abstr2 cvs ct
1.237 + | @{term "op div :: int => _"} $ _ $ _ => abstr2 cvs ct
1.238 + | @{term "op mod :: int => _"} $ _ $ _ => abstr2 cvs ct
1.239 + | @{term "op / :: real => _"} $ _ $ _ => abstr2 cvs ct
1.240 + | @{term "op < :: int => _"} $ _ $ _ => abstr2 cvs ct
1.241 + | @{term "op < :: real => _"} $ _ $ _ => abstr2 cvs ct
1.242 + | @{term "op <= :: int => _"} $ _ $ _ => abstr2 cvs ct
1.243 + | @{term "op <= :: real => _"} $ _ $ _ => abstr2 cvs ct
1.244 + | Const (@{const_name apply}, _) $ _ $ _ => abstr2 cvs ct
1.245 + | Const (@{const_name fun_upd}, _) $ _ $ _ $ _ => abstr3 cvs ct
1.246 + | t =>
1.247 + if is_atomic t orelse is_number t then pair ct
1.248 + else fresh_abstraction cvs ct)
1.249 + in abstr [] end
1.250 +
1.251 +fun with_prems thms f ct =
1.252 + fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
1.253 + |> f
1.254 + |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
1.255 +
1.256 +in
1.257 +
1.258 +fun by_abstraction ctxt thms prove = with_prems thms (fn ct =>
1.259 + let val (cu, cx) = abstract (true, true) ct (abs_context ctxt)
1.260 + in abs_instantiate cx (prove (context_of cx) cu) end)
1.261 +
1.262 +end
1.263 +
1.264 +
1.265 +
1.266 +(* a faster COMP *)
1.267 +
1.268 +type compose_data = cterm list * (cterm -> cterm list) * thm
1.269 +
1.270 +fun list2 (x, y) = [x, y]
1.271 +
1.272 +fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
1.273 +fun precompose2 f rule = precompose (list2 o f) rule
1.274 +
1.275 +fun compose (cvs, f, rule) thm =
1.276 + discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
1.277 +
1.278 +
1.279 +
1.280 +(* unfolding of 'distinct' *)
1.281 +
1.282 +local
1.283 + val set1 = @{lemma "x ~: set [] == ~False" by simp}
1.284 + val set2 = @{lemma "x ~: set [x] == False" by simp}
1.285 + val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
1.286 + val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
1.287 + val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
1.288 +
1.289 + fun set_conv ct =
1.290 + (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
1.291 + (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
1.292 +
1.293 + val dist1 = @{lemma "distinct [] == ~False" by simp}
1.294 + val dist2 = @{lemma "distinct [x] == ~False" by simp}
1.295 + val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
1.296 + by simp}
1.297 +
1.298 + fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
1.299 +in
1.300 +fun unfold_distinct_conv ct =
1.301 + (More_Conv.rewrs_conv [dist1, dist2] else_conv
1.302 + (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
1.303 +end
1.304 +
1.305 +
1.306 +
1.307 +(* simpset *)
1.308 +
1.309 +local
1.310 + val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
1.311 + val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
1.312 + val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
1.313 + val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
1.314 +
1.315 + fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
1.316 + fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
1.317 + | dest_binop t = raise TERM ("dest_binop", [t])
1.318 +
1.319 + fun prove_antisym_le ss t =
1.320 + let
1.321 + val (le, r, s) = dest_binop t
1.322 + val less = Const (@{const_name less}, Term.fastype_of le)
1.323 + val prems = Simplifier.prems_of_ss ss
1.324 + in
1.325 + (case find_first (eq_prop (le $ s $ r)) prems of
1.326 + NONE =>
1.327 + find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
1.328 + |> Option.map (fn thm => thm RS antisym_less1)
1.329 + | SOME thm => SOME (thm RS antisym_le1))
1.330 + end
1.331 + handle THM _ => NONE
1.332 +
1.333 + fun prove_antisym_less ss t =
1.334 + let
1.335 + val (less, r, s) = dest_binop (HOLogic.dest_not t)
1.336 + val le = Const (@{const_name less_eq}, Term.fastype_of less)
1.337 + val prems = prems_of_ss ss
1.338 + in
1.339 + (case find_first (eq_prop (le $ r $ s)) prems of
1.340 + NONE =>
1.341 + find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
1.342 + |> Option.map (fn thm => thm RS antisym_less2)
1.343 + | SOME thm => SOME (thm RS antisym_le2))
1.344 + end
1.345 + handle THM _ => NONE
1.346 +in
1.347 +
1.348 +fun make_simpset ctxt rules = Simplifier.context ctxt (HOL_ss
1.349 + addsimps @{thms field_simps}
1.350 + addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
1.351 + addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
1.352 + addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
1.353 + addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
1.354 + addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
1.355 + addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
1.356 + addsimps @{thms array_rules}
1.357 + addsimprocs [
1.358 + Simplifier.simproc @{theory} "fast_int_arith" [
1.359 + "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
1.360 + Simplifier.simproc @{theory} "fast_real_arith" [
1.361 + "(m::real) < n", "(m::real) <= n", "(m::real) = n"]
1.362 + (K Lin_Arith.simproc),
1.363 + Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
1.364 + (K prove_antisym_le),
1.365 + Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
1.366 + (K prove_antisym_less)]
1.367 + addsimps rules)
1.368 +
1.369 +end
1.370 +
1.371 +end