src/HOL/Tools/SMT/smt_normalize.ML
author wenzelm
Fri Sep 25 20:37:59 2015 +0200 (2015-09-25)
changeset 61268 abe08fb15a12
parent 61033 fd7fe96ca7b9
child 66298 5ff9fe3fee66
permissions -rw-r--r--
moved remaining display.ML to more_thm.ML;
     1 (*  Title:      HOL/Tools/SMT/smt_normalize.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Normalization steps on theorems required by SMT solvers.
     5 *)
     6 
     7 signature SMT_NORMALIZE =
     8 sig
     9   val drop_fact_warning: Proof.context -> thm -> unit
    10   val atomize_conv: Proof.context -> conv
    11 
    12   val special_quant_table: (string * thm) list
    13   val case_bool_entry: string * thm
    14   val abs_min_max_table: (string * thm) list
    15 
    16   type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    17   val add_extra_norm: SMT_Util.class * extra_norm -> Context.generic -> Context.generic
    18   val normalize: Proof.context -> thm list -> (int * thm) list
    19 end;
    20 
    21 structure SMT_Normalize: SMT_NORMALIZE =
    22 struct
    23 
    24 fun drop_fact_warning ctxt =
    25   SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
    26     Thm.string_of_thm ctxt)
    27 
    28 
    29 (* general theorem normalizations *)
    30 
    31 (** instantiate elimination rules **)
    32 
    33 local
    34   val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of @{context} @{const False})
    35 
    36   fun inst f ct thm =
    37     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    38     in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
    39 in
    40 
    41 fun instantiate_elim thm =
    42   (case Thm.concl_of thm of
    43     @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
    44   | Var _ => inst I cpfalse thm
    45   | _ => thm)
    46 
    47 end
    48 
    49 
    50 (** normalize definitions **)
    51 
    52 fun norm_def thm =
    53   (case Thm.prop_of thm of
    54     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
    55       norm_def (thm RS @{thm fun_cong})
    56   | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
    57   | _ => thm)
    58 
    59 
    60 (** atomization **)
    61 
    62 fun atomize_conv ctxt ct =
    63   (case Thm.term_of ct of
    64     @{const Pure.imp} $ _ $ _ =>
    65       Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
    66   | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
    67       Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
    68   | Const (@{const_name Pure.all}, _) $ Abs _ =>
    69       Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
    70   | _ => Conv.all_conv) ct
    71   handle CTERM _ => Conv.all_conv ct
    72 
    73 val setup_atomize =
    74   fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
    75     @{const_name Pure.all}, @{const_name Trueprop}]
    76 
    77 
    78 (** unfold special quantifiers **)
    79 
    80 val special_quant_table = [
    81   (@{const_name Ex1}, @{thm Ex1_def_raw}),
    82   (@{const_name Ball}, @{thm Ball_def_raw}),
    83   (@{const_name Bex}, @{thm Bex_def_raw})]
    84 
    85 local
    86   fun special_quant (Const (n, _)) = AList.lookup (op =) special_quant_table n
    87     | special_quant _ = NONE
    88 
    89   fun special_quant_conv _ ct =
    90     (case special_quant (Thm.term_of ct) of
    91       SOME thm => Conv.rewr_conv thm
    92     | NONE => Conv.all_conv) ct
    93 in
    94 
    95 fun unfold_special_quants_conv ctxt =
    96   SMT_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    97 
    98 val setup_unfolded_quants = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quant_table
    99 
   100 end
   101 
   102 
   103 (** trigger inference **)
   104 
   105 local
   106   (*** check trigger syntax ***)
   107 
   108   fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true
   109     | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false
   110     | dest_trigger _ = NONE
   111 
   112   fun eq_list [] = false
   113     | eq_list (b :: bs) = forall (equal b) bs
   114 
   115   fun proper_trigger t =
   116     t
   117     |> these o try SMT_Util.dest_symb_list
   118     |> map (map_filter dest_trigger o these o try SMT_Util.dest_symb_list)
   119     |> (fn [] => false | bss => forall eq_list bss)
   120 
   121   fun proper_quant inside f t =
   122     (case t of
   123       Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u
   124     | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u
   125     | @{const trigger} $ p $ u =>
   126         (if inside then f p else false) andalso proper_quant false f u
   127     | Abs (_, _, u) => proper_quant false f u
   128     | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
   129     | _ => true)
   130 
   131   fun check_trigger_error ctxt t =
   132     error ("SMT triggers must only occur under quantifier and multipatterns " ^
   133       "must have the same kind: " ^ Syntax.string_of_term ctxt t)
   134 
   135   fun check_trigger_conv ctxt ct =
   136     if proper_quant false proper_trigger (SMT_Util.term_of ct) then Conv.all_conv ct
   137     else check_trigger_error ctxt (Thm.term_of ct)
   138 
   139 
   140   (*** infer simple triggers ***)
   141 
   142   fun dest_cond_eq ct =
   143     (case Thm.term_of ct of
   144       Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
   145     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
   146     | _ => raise CTERM ("no equation", [ct]))
   147 
   148   fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
   149     | get_constrs _ _ = []
   150 
   151   fun is_constr thy (n, T) =
   152     let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
   153     in can (the o find_first match o get_constrs thy o Term.body_type) T end
   154 
   155   fun is_constr_pat thy t =
   156     (case Term.strip_comb t of
   157       (Free _, []) => true
   158     | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts
   159     | _ => false)
   160 
   161   fun is_simp_lhs ctxt t =
   162     (case Term.strip_comb t of
   163       (Const c, ts as _ :: _) =>
   164         not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
   165         forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts
   166     | _ => false)
   167 
   168   fun has_all_vars vs t =
   169     subset (op aconv) (vs, map Free (Term.add_frees t []))
   170 
   171   fun minimal_pats vs ct =
   172     if has_all_vars vs (Thm.term_of ct) then
   173       (case Thm.term_of ct of
   174         _ $ _ =>
   175           (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of
   176             ([], []) => [[ct]]
   177           | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
   178       | _ => [])
   179     else []
   180 
   181   fun proper_mpat _ _ _ [] = false
   182     | proper_mpat thy gen u cts =
   183         let
   184           val tps = (op ~~) (`gen (map Thm.term_of cts))
   185           fun some_match u = tps |> exists (fn (t', t) =>
   186             Pattern.matches thy (t', u) andalso not (t aconv u))
   187         in not (Term.exists_subterm some_match u) end
   188 
   189   val pat = SMT_Util.mk_const_pat @{theory} @{const_name pat} SMT_Util.destT1
   190   fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
   191 
   192   fun mk_clist T =
   193     apply2 (Thm.cterm_of @{context}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
   194   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   195   val mk_pat_list = mk_list (mk_clist @{typ pattern})
   196   val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
   197   fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
   198 
   199   val trigger_eq = mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
   200 
   201   fun insert_trigger_conv [] ct = Conv.all_conv ct
   202     | insert_trigger_conv ctss ct =
   203         let
   204           val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
   205           val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]
   206         in Thm.instantiate ([], inst) trigger_eq end
   207 
   208   fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
   209     let
   210       val (lhs, rhs) = dest_cond_eq ct
   211 
   212       val vs = map Thm.term_of cvs
   213       val thy = Proof_Context.theory_of ctxt
   214 
   215       fun get_mpats ct =
   216         if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct
   217         else []
   218       val gen = Variable.export_terms ctxt outer_ctxt
   219       val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs))
   220 
   221     in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
   222 
   223   fun has_trigger (@{const trigger} $ _ $ _) = true
   224     | has_trigger _ = false
   225 
   226   fun try_trigger_conv cv ct =
   227     if SMT_Util.under_quant has_trigger (SMT_Util.term_of ct) then Conv.all_conv ct
   228     else Conv.try_conv cv ct
   229 
   230   fun infer_trigger_conv ctxt =
   231     if Config.get ctxt SMT_Config.infer_triggers then
   232       try_trigger_conv (SMT_Util.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
   233     else Conv.all_conv
   234 in
   235 
   236 fun trigger_conv ctxt =
   237   SMT_Util.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
   238 
   239 val setup_trigger =
   240   fold SMT_Builtin.add_builtin_fun_ext''
   241     [@{const_name pat}, @{const_name nopat}, @{const_name trigger}]
   242 
   243 end
   244 
   245 
   246 (** combined general normalizations **)
   247 
   248 fun gen_normalize1_conv ctxt =
   249   atomize_conv ctxt then_conv
   250   unfold_special_quants_conv ctxt then_conv
   251   Thm.beta_conversion true then_conv
   252   trigger_conv ctxt
   253 
   254 fun gen_normalize1 ctxt =
   255   instantiate_elim #>
   256   norm_def #>
   257   Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
   258   Drule.forall_intr_vars #>
   259   Conv.fconv_rule (gen_normalize1_conv ctxt) #>
   260   (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
   261   Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
   262 
   263 fun gen_norm1_safe ctxt (i, thm) =
   264   (case try (gen_normalize1 ctxt) thm of
   265     SOME thm' => SOME (i, thm')
   266   | NONE => (drop_fact_warning ctxt thm; NONE))
   267 
   268 fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
   269 
   270 
   271 (* unfolding of definitions and theory-specific rewritings *)
   272 
   273 fun expand_head_conv cv ct =
   274   (case Thm.term_of ct of
   275     _ $ _ =>
   276       Conv.fun_conv (expand_head_conv cv) then_conv
   277       Conv.try_conv (Thm.beta_conversion false)
   278   | _ => cv) ct
   279 
   280 
   281 (** rewrite bool case expressions as if expressions **)
   282 
   283 val case_bool_entry = (@{const_name "bool.case_bool"}, @{thm case_bool_if})
   284 
   285 local
   286   fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
   287     | is_case_bool _ = false
   288 
   289   fun unfold_conv _ =
   290     SMT_Util.if_true_conv (is_case_bool o Term.head_of)
   291       (expand_head_conv (Conv.rewr_conv @{thm case_bool_if}))
   292 in
   293 
   294 fun rewrite_case_bool_conv ctxt =
   295   SMT_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   296 
   297 val setup_case_bool = SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   298 
   299 end
   300 
   301 
   302 (** unfold abs, min and max **)
   303 
   304 val abs_min_max_table = [
   305   (@{const_name min}, @{thm min_def_raw}),
   306   (@{const_name max}, @{thm max_def_raw}),
   307   (@{const_name abs}, @{thm abs_if_raw})]
   308 
   309 local
   310   fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
   311         (case AList.lookup (op =) abs_min_max_table n of
   312           NONE => NONE
   313         | SOME thm => if SMT_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE)
   314     | abs_min_max _ _ = NONE
   315 
   316   fun unfold_amm_conv ctxt ct =
   317     (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of
   318       SOME thm => expand_head_conv (Conv.rewr_conv thm)
   319     | NONE => Conv.all_conv) ct
   320 in
   321 
   322 fun unfold_abs_min_max_conv ctxt =
   323   SMT_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
   324 
   325 val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
   326 
   327 end
   328 
   329 
   330 (** normalize numerals **)
   331 
   332 local
   333   (*
   334     rewrite Numeral1 into 1
   335     rewrite - 0 into 0
   336   *)
   337 
   338   fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
   339         true
   340     | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
   341         true
   342     | is_irregular_number _ = false
   343 
   344   fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t
   345 
   346   val proper_num_ss =
   347     simpset_of (put_simpset HOL_ss @{context} addsimps @{thms Num.numeral_One minus_zero})
   348 
   349   fun norm_num_conv ctxt =
   350     SMT_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
   351       Conv.no_conv
   352 in
   353 
   354 fun normalize_numerals_conv ctxt =
   355   SMT_Util.if_exists_conv (is_strange_number ctxt) (Conv.top_sweep_conv norm_num_conv ctxt)
   356 
   357 end
   358 
   359 
   360 (** combined unfoldings and rewritings **)
   361 
   362 fun unfold_conv ctxt =
   363   rewrite_case_bool_conv ctxt then_conv
   364   unfold_abs_min_max_conv ctxt then_conv
   365   Thm.beta_conversion true
   366 
   367 fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
   368 fun unfold_monomorph ctxt = map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   369 
   370 
   371 (* overall normalization *)
   372 
   373 fun burrow_ids f ithms =
   374   let
   375     val (is, thms) = split_list ithms
   376     val (thms', extra_thms) = f thms
   377   in (is ~~ thms') @ map (pair ~1) extra_thms end
   378 
   379 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   380 
   381 structure Extra_Norms = Generic_Data
   382 (
   383   type T = extra_norm SMT_Util.dict
   384   val empty = []
   385   val extend = I
   386   fun merge data = SMT_Util.dict_merge fst data
   387 )
   388 
   389 fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT_Util.dict_update (cs, norm))
   390 
   391 fun apply_extra_norms ctxt ithms =
   392   let
   393     val cs = SMT_Config.solver_class_of ctxt
   394     val es = SMT_Util.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   395   in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
   396 
   397 local
   398   val ignored = member (op =) [@{const_name All}, @{const_name Ex},
   399     @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
   400 
   401   val schematic_consts_of =
   402     let
   403       fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
   404         | collect (t $ u) = collect t #> collect u
   405         | collect (Abs (_, _, t)) = collect t
   406         | collect (t as Const (n, _)) =
   407             if not (ignored n) then Monomorph.add_schematic_consts_of t else I
   408         | collect _ = I
   409       and collect_trigger t =
   410         let val dest = these o try SMT_Util.dest_symb_list
   411         in fold (fold collect_pat o dest) (dest t) end
   412       and collect_pat (Const (@{const_name pat}, _) $ t) = collect t
   413         | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t
   414         | collect_pat _ = I
   415     in (fn t => collect t Symtab.empty) end
   416 in
   417 
   418 fun monomorph ctxt xthms =
   419   let val (xs, thms) = split_list xthms
   420   in
   421     map (pair 1) thms
   422     |> Monomorph.monomorph schematic_consts_of ctxt
   423     |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
   424   end
   425 
   426 end
   427 
   428 fun normalize ctxt wthms =
   429   wthms
   430   |> map_index I
   431   |> gen_normalize ctxt
   432   |> unfold_polymorph ctxt
   433   |> monomorph ctxt
   434   |> unfold_monomorph ctxt
   435   |> apply_extra_norms ctxt
   436 
   437 val _ = Theory.setup (Context.theory_map (
   438   setup_atomize #>
   439   setup_unfolded_quants #>
   440   setup_trigger #>
   441   setup_case_bool #>
   442   setup_abs_min_max))
   443 
   444 end;