src/HOL/Tools/SMT/smt_normalize.ML
changeset 58061 3d060f43accb
parent 57996 ca917ea6969c
child 58112 8081087096ad
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -0,0 +1,441 @@
     1.4 +(*  Title:      HOL/Tools/SMT/smt_normalize.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Normalization steps on theorems required by SMT solvers.
     1.8 +*)
     1.9 +
    1.10 +signature SMT_NORMALIZE =
    1.11 +sig
    1.12 +  val drop_fact_warning: Proof.context -> thm -> unit
    1.13 +  val atomize_conv: Proof.context -> conv
    1.14 +
    1.15 +  val special_quant_table: (string * thm) list
    1.16 +  val case_bool_entry: string * thm
    1.17 +  val abs_min_max_table: (string * thm) list
    1.18 +
    1.19 +  type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    1.20 +  val add_extra_norm: SMT_Util.class * extra_norm -> Context.generic -> Context.generic
    1.21 +  val normalize: Proof.context -> thm list -> (int * thm) list
    1.22 +end;
    1.23 +
    1.24 +structure SMT_Normalize: SMT_NORMALIZE =
    1.25 +struct
    1.26 +
    1.27 +fun drop_fact_warning ctxt =
    1.28 +  SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
    1.29 +    Display.string_of_thm ctxt)
    1.30 +
    1.31 +
    1.32 +(* general theorem normalizations *)
    1.33 +
    1.34 +(** instantiate elimination rules **)
    1.35 +
    1.36 +local
    1.37 +  val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.38 +
    1.39 +  fun inst f ct thm =
    1.40 +    let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.41 +    in Thm.instantiate ([], [(cv, ct)]) thm end
    1.42 +in
    1.43 +
    1.44 +fun instantiate_elim thm =
    1.45 +  (case Thm.concl_of thm of
    1.46 +    @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
    1.47 +  | Var _ => inst I cpfalse thm
    1.48 +  | _ => thm)
    1.49 +
    1.50 +end
    1.51 +
    1.52 +
    1.53 +(** normalize definitions **)
    1.54 +
    1.55 +fun norm_def thm =
    1.56 +  (case Thm.prop_of thm of
    1.57 +    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    1.58 +      norm_def (thm RS @{thm fun_cong})
    1.59 +  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    1.60 +  | _ => thm)
    1.61 +
    1.62 +
    1.63 +(** atomization **)
    1.64 +
    1.65 +fun atomize_conv ctxt ct =
    1.66 +  (case Thm.term_of ct of
    1.67 +    @{const Pure.imp} $ _ $ _ =>
    1.68 +      Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
    1.69 +  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
    1.70 +      Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
    1.71 +  | Const (@{const_name Pure.all}, _) $ Abs _ =>
    1.72 +      Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
    1.73 +  | _ => Conv.all_conv) ct
    1.74 +
    1.75 +val setup_atomize =
    1.76 +  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
    1.77 +    @{const_name Pure.all}, @{const_name Trueprop}]
    1.78 +
    1.79 +
    1.80 +(** unfold special quantifiers **)
    1.81 +
    1.82 +val special_quant_table = [
    1.83 +  (@{const_name Ex1}, @{thm Ex1_def_raw}),
    1.84 +  (@{const_name Ball}, @{thm Ball_def_raw}),
    1.85 +  (@{const_name Bex}, @{thm Bex_def_raw})]
    1.86 +
    1.87 +local
    1.88 +  fun special_quant (Const (n, _)) = AList.lookup (op =) special_quant_table n
    1.89 +    | special_quant _ = NONE
    1.90 +
    1.91 +  fun special_quant_conv _ ct =
    1.92 +    (case special_quant (Thm.term_of ct) of
    1.93 +      SOME thm => Conv.rewr_conv thm
    1.94 +    | NONE => Conv.all_conv) ct
    1.95 +in
    1.96 +
    1.97 +fun unfold_special_quants_conv ctxt =
    1.98 +  SMT_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    1.99 +
   1.100 +val setup_unfolded_quants = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quant_table
   1.101 +
   1.102 +end
   1.103 +
   1.104 +
   1.105 +(** trigger inference **)
   1.106 +
   1.107 +local
   1.108 +  (*** check trigger syntax ***)
   1.109 +
   1.110 +  fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true
   1.111 +    | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false
   1.112 +    | dest_trigger _ = NONE
   1.113 +
   1.114 +  fun eq_list [] = false
   1.115 +    | eq_list (b :: bs) = forall (equal b) bs
   1.116 +
   1.117 +  fun proper_trigger t =
   1.118 +    t
   1.119 +    |> these o try SMT_Util.dest_symb_list
   1.120 +    |> map (map_filter dest_trigger o these o try SMT_Util.dest_symb_list)
   1.121 +    |> (fn [] => false | bss => forall eq_list bss)
   1.122 +
   1.123 +  fun proper_quant inside f t =
   1.124 +    (case t of
   1.125 +      Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u
   1.126 +    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u
   1.127 +    | @{const trigger} $ p $ u =>
   1.128 +        (if inside then f p else false) andalso proper_quant false f u
   1.129 +    | Abs (_, _, u) => proper_quant false f u
   1.130 +    | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
   1.131 +    | _ => true)
   1.132 +
   1.133 +  fun check_trigger_error ctxt t =
   1.134 +    error ("SMT triggers must only occur under quantifier and multipatterns " ^
   1.135 +      "must have the same kind: " ^ Syntax.string_of_term ctxt t)
   1.136 +
   1.137 +  fun check_trigger_conv ctxt ct =
   1.138 +    if proper_quant false proper_trigger (SMT_Util.term_of ct) then Conv.all_conv ct
   1.139 +    else check_trigger_error ctxt (Thm.term_of ct)
   1.140 +
   1.141 +
   1.142 +  (*** infer simple triggers ***)
   1.143 +
   1.144 +  fun dest_cond_eq ct =
   1.145 +    (case Thm.term_of ct of
   1.146 +      Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
   1.147 +    | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
   1.148 +    | _ => raise CTERM ("no equation", [ct]))
   1.149 +
   1.150 +  fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
   1.151 +    | get_constrs _ _ = []
   1.152 +
   1.153 +  fun is_constr thy (n, T) =
   1.154 +    let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
   1.155 +    in can (the o find_first match o get_constrs thy o Term.body_type) T end
   1.156 +
   1.157 +  fun is_constr_pat thy t =
   1.158 +    (case Term.strip_comb t of
   1.159 +      (Free _, []) => true
   1.160 +    | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts
   1.161 +    | _ => false)
   1.162 +
   1.163 +  fun is_simp_lhs ctxt t =
   1.164 +    (case Term.strip_comb t of
   1.165 +      (Const c, ts as _ :: _) =>
   1.166 +        not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
   1.167 +        forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts
   1.168 +    | _ => false)
   1.169 +
   1.170 +  fun has_all_vars vs t =
   1.171 +    subset (op aconv) (vs, map Free (Term.add_frees t []))
   1.172 +
   1.173 +  fun minimal_pats vs ct =
   1.174 +    if has_all_vars vs (Thm.term_of ct) then
   1.175 +      (case Thm.term_of ct of
   1.176 +        _ $ _ =>
   1.177 +          (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
   1.178 +            ([], []) => [[ct]]
   1.179 +          | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
   1.180 +      | _ => [])
   1.181 +    else []
   1.182 +
   1.183 +  fun proper_mpat _ _ _ [] = false
   1.184 +    | proper_mpat thy gen u cts =
   1.185 +        let
   1.186 +          val tps = (op ~~) (`gen (map Thm.term_of cts))
   1.187 +          fun some_match u = tps |> exists (fn (t', t) =>
   1.188 +            Pattern.matches thy (t', u) andalso not (t aconv u))
   1.189 +        in not (Term.exists_subterm some_match u) end
   1.190 +
   1.191 +  val pat = SMT_Util.mk_const_pat @{theory} @{const_name pat} SMT_Util.destT1
   1.192 +  fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
   1.193 +
   1.194 +  fun mk_clist T =
   1.195 +    pairself (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
   1.196 +  fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   1.197 +  val mk_pat_list = mk_list (mk_clist @{typ pattern})
   1.198 +  val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
   1.199 +  fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
   1.200 +
   1.201 +  val trigger_eq = mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
   1.202 +
   1.203 +  fun insert_trigger_conv [] ct = Conv.all_conv ct
   1.204 +    | insert_trigger_conv ctss ct =
   1.205 +        let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
   1.206 +        in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
   1.207 +
   1.208 +  fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
   1.209 +    let
   1.210 +      val (lhs, rhs) = dest_cond_eq ct
   1.211 +
   1.212 +      val vs = map Thm.term_of cvs
   1.213 +      val thy = Proof_Context.theory_of ctxt
   1.214 +
   1.215 +      fun get_mpats ct =
   1.216 +        if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct
   1.217 +        else []
   1.218 +      val gen = Variable.export_terms ctxt outer_ctxt
   1.219 +      val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs))
   1.220 +
   1.221 +    in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
   1.222 +
   1.223 +  fun has_trigger (@{const trigger} $ _ $ _) = true
   1.224 +    | has_trigger _ = false
   1.225 +
   1.226 +  fun try_trigger_conv cv ct =
   1.227 +    if SMT_Util.under_quant has_trigger (SMT_Util.term_of ct) then Conv.all_conv ct
   1.228 +    else Conv.try_conv cv ct
   1.229 +
   1.230 +  fun infer_trigger_conv ctxt =
   1.231 +    if Config.get ctxt SMT_Config.infer_triggers then
   1.232 +      try_trigger_conv (SMT_Util.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
   1.233 +    else Conv.all_conv
   1.234 +in
   1.235 +
   1.236 +fun trigger_conv ctxt =
   1.237 +  SMT_Util.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
   1.238 +
   1.239 +val setup_trigger =
   1.240 +  fold SMT_Builtin.add_builtin_fun_ext''
   1.241 +    [@{const_name pat}, @{const_name nopat}, @{const_name trigger}]
   1.242 +
   1.243 +end
   1.244 +
   1.245 +
   1.246 +(** combined general normalizations **)
   1.247 +
   1.248 +fun gen_normalize1_conv ctxt =
   1.249 +  atomize_conv ctxt then_conv
   1.250 +  unfold_special_quants_conv ctxt then_conv
   1.251 +  Thm.beta_conversion true then_conv
   1.252 +  trigger_conv ctxt
   1.253 +
   1.254 +fun gen_normalize1 ctxt =
   1.255 +  instantiate_elim #>
   1.256 +  norm_def #>
   1.257 +  Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
   1.258 +  Drule.forall_intr_vars #>
   1.259 +  Conv.fconv_rule (gen_normalize1_conv ctxt) #>
   1.260 +  (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
   1.261 +  Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
   1.262 +
   1.263 +fun gen_norm1_safe ctxt (i, thm) =
   1.264 +  (case try (gen_normalize1 ctxt) thm of
   1.265 +    SOME thm' => SOME (i, thm')
   1.266 +  | NONE => (drop_fact_warning ctxt thm; NONE))
   1.267 +
   1.268 +fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
   1.269 +
   1.270 +
   1.271 +(* unfolding of definitions and theory-specific rewritings *)
   1.272 +
   1.273 +fun expand_head_conv cv ct =
   1.274 +  (case Thm.term_of ct of
   1.275 +    _ $ _ =>
   1.276 +      Conv.fun_conv (expand_head_conv cv) then_conv
   1.277 +      Conv.try_conv (Thm.beta_conversion false)
   1.278 +  | _ => cv) ct
   1.279 +
   1.280 +
   1.281 +(** rewrite bool case expressions as if expressions **)
   1.282 +
   1.283 +val case_bool_entry = (@{const_name "bool.case_bool"}, @{thm case_bool_if})
   1.284 +
   1.285 +local
   1.286 +  fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
   1.287 +    | is_case_bool _ = false
   1.288 +
   1.289 +  fun unfold_conv _ =
   1.290 +    SMT_Util.if_true_conv (is_case_bool o Term.head_of)
   1.291 +      (expand_head_conv (Conv.rewr_conv @{thm case_bool_if}))
   1.292 +in
   1.293 +
   1.294 +fun rewrite_case_bool_conv ctxt =
   1.295 +  SMT_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   1.296 +
   1.297 +val setup_case_bool = SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   1.298 +
   1.299 +end
   1.300 +
   1.301 +
   1.302 +(** unfold abs, min and max **)
   1.303 +
   1.304 +val abs_min_max_table = [
   1.305 +  (@{const_name min}, @{thm min_def_raw}),
   1.306 +  (@{const_name max}, @{thm max_def_raw}),
   1.307 +  (@{const_name abs}, @{thm abs_if_raw})]
   1.308 +
   1.309 +local
   1.310 +  fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
   1.311 +        (case AList.lookup (op =) abs_min_max_table n of
   1.312 +          NONE => NONE
   1.313 +        | SOME thm => if SMT_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE)
   1.314 +    | abs_min_max _ _ = NONE
   1.315 +
   1.316 +  fun unfold_amm_conv ctxt ct =
   1.317 +    (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of
   1.318 +      SOME thm => expand_head_conv (Conv.rewr_conv thm)
   1.319 +    | NONE => Conv.all_conv) ct
   1.320 +in
   1.321 +
   1.322 +fun unfold_abs_min_max_conv ctxt =
   1.323 +  SMT_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
   1.324 +
   1.325 +val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
   1.326 +
   1.327 +end
   1.328 +
   1.329 +
   1.330 +(** normalize numerals **)
   1.331 +
   1.332 +local
   1.333 +  (*
   1.334 +    rewrite Numeral1 into 1
   1.335 +    rewrite - 0 into 0
   1.336 +  *)
   1.337 +
   1.338 +  fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
   1.339 +        true
   1.340 +    | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
   1.341 +        true
   1.342 +    | is_irregular_number _ = false
   1.343 +
   1.344 +  fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t
   1.345 +
   1.346 +  val proper_num_ss =
   1.347 +    simpset_of (put_simpset HOL_ss @{context} addsimps @{thms Num.numeral_One minus_zero})
   1.348 +
   1.349 +  fun norm_num_conv ctxt =
   1.350 +    SMT_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
   1.351 +      Conv.no_conv
   1.352 +in
   1.353 +
   1.354 +fun normalize_numerals_conv ctxt =
   1.355 +  SMT_Util.if_exists_conv (is_strange_number ctxt) (Conv.top_sweep_conv norm_num_conv ctxt)
   1.356 +
   1.357 +end
   1.358 +
   1.359 +
   1.360 +(** combined unfoldings and rewritings **)
   1.361 +
   1.362 +fun unfold_conv ctxt =
   1.363 +  rewrite_case_bool_conv ctxt then_conv
   1.364 +  unfold_abs_min_max_conv ctxt then_conv
   1.365 +  Thm.beta_conversion true
   1.366 +
   1.367 +fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
   1.368 +fun unfold_monomorph ctxt = map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   1.369 +
   1.370 +
   1.371 +(* overall normalization *)
   1.372 +
   1.373 +fun burrow_ids f ithms =
   1.374 +  let
   1.375 +    val (is, thms) = split_list ithms
   1.376 +    val (thms', extra_thms) = f thms
   1.377 +  in (is ~~ thms') @ map (pair ~1) extra_thms end
   1.378 +
   1.379 +type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   1.380 +
   1.381 +structure Extra_Norms = Generic_Data
   1.382 +(
   1.383 +  type T = extra_norm SMT_Util.dict
   1.384 +  val empty = []
   1.385 +  val extend = I
   1.386 +  fun merge data = SMT_Util.dict_merge fst data
   1.387 +)
   1.388 +
   1.389 +fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT_Util.dict_update (cs, norm))
   1.390 +
   1.391 +fun apply_extra_norms ctxt ithms =
   1.392 +  let
   1.393 +    val cs = SMT_Config.solver_class_of ctxt
   1.394 +    val es = SMT_Util.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   1.395 +  in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
   1.396 +
   1.397 +local
   1.398 +  val ignored = member (op =) [@{const_name All}, @{const_name Ex},
   1.399 +    @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
   1.400 +
   1.401 +  val schematic_consts_of =
   1.402 +    let
   1.403 +      fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
   1.404 +        | collect (t $ u) = collect t #> collect u
   1.405 +        | collect (Abs (_, _, t)) = collect t
   1.406 +        | collect (t as Const (n, _)) =
   1.407 +            if not (ignored n) then Monomorph.add_schematic_consts_of t else I
   1.408 +        | collect _ = I
   1.409 +      and collect_trigger t =
   1.410 +        let val dest = these o try SMT_Util.dest_symb_list
   1.411 +        in fold (fold collect_pat o dest) (dest t) end
   1.412 +      and collect_pat (Const (@{const_name pat}, _) $ t) = collect t
   1.413 +        | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t
   1.414 +        | collect_pat _ = I
   1.415 +    in (fn t => collect t Symtab.empty) end
   1.416 +in
   1.417 +
   1.418 +fun monomorph ctxt xthms =
   1.419 +  let val (xs, thms) = split_list xthms
   1.420 +  in
   1.421 +    map (pair 1) thms
   1.422 +    |> Monomorph.monomorph schematic_consts_of ctxt
   1.423 +    |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
   1.424 +  end
   1.425 +
   1.426 +end
   1.427 +
   1.428 +fun normalize ctxt wthms =
   1.429 +  wthms
   1.430 +  |> map_index I
   1.431 +  |> gen_normalize ctxt
   1.432 +  |> unfold_polymorph ctxt
   1.433 +  |> monomorph ctxt
   1.434 +  |> unfold_monomorph ctxt
   1.435 +  |> apply_extra_norms ctxt
   1.436 +
   1.437 +val _ = Theory.setup (Context.theory_map (
   1.438 +  setup_atomize #>
   1.439 +  setup_unfolded_quants #>
   1.440 +  setup_trigger #>
   1.441 +  setup_case_bool #>
   1.442 +  setup_abs_min_max))
   1.443 +
   1.444 +end;