src/HOL/Tools/SMT/smt_normalize.ML
 author haftmann Sat Aug 28 16:14:32 2010 +0200 (2010-08-28) changeset 38864 4abe644fcea5 parent 37786 4eb98849c5c0 child 39483 9f0e5684f04b permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
```     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   * simplify trivial distincts (those with less than three elements),
```
```     6   * rewrite bool case expressions as if expressions,
```
```     7   * normalize numerals (e.g. replace negative numerals by negated positive
```
```     8     numerals),
```
```     9   * embed natural numbers into integers,
```
```    10   * add extra rules specifying types and constants which occur frequently,
```
```    11   * fully translate into object logic, add universal closure,
```
```    12   * lift lambda terms,
```
```    13   * make applications explicit for functions with varying number of arguments.
```
```    14 *)
```
```    15
```
```    16 signature SMT_NORMALIZE =
```
```    17 sig
```
```    18   type extra_norm = thm list -> Proof.context -> thm list * Proof.context
```
```    19   val normalize: extra_norm -> thm list -> Proof.context ->
```
```    20     thm list * Proof.context
```
```    21   val atomize_conv: Proof.context -> conv
```
```    22   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
```
```    23 end
```
```    24
```
```    25 structure SMT_Normalize: SMT_NORMALIZE =
```
```    26 struct
```
```    27
```
```    28 infix 2 ??
```
```    29 fun (test ?? f) x = if test x then f x else x
```
```    30
```
```    31 fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
```
```    32 fun if_true_conv c cv = if_conv c cv Conv.all_conv
```
```    33
```
```    34
```
```    35
```
```    36 (* simplification of trivial distincts (distinct should have at least
```
```    37    three elements in the argument list) *)
```
```    38
```
```    39 local
```
```    40   fun is_trivial_distinct (Const (@{const_name distinct}, _) \$ t) =
```
```    41         length (HOLogic.dest_list t) <= 2
```
```    42     | is_trivial_distinct _ = false
```
```    43
```
```    44   val thms = map mk_meta_eq @{lemma
```
```    45     "distinct [] = True"
```
```    46     "distinct [x] = True"
```
```    47     "distinct [x, y] = (x ~= y)"
```
```    48     by simp_all}
```
```    49   fun distinct_conv _ =
```
```    50     if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
```
```    51 in
```
```    52 fun trivial_distinct ctxt =
```
```    53   map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
```
```    54     Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
```
```    55 end
```
```    56
```
```    57
```
```    58
```
```    59 (* rewrite bool case expressions as if expressions *)
```
```    60
```
```    61 local
```
```    62   val is_bool_case = (fn
```
```    63       Const (@{const_name "bool.bool_case"}, _) \$ _ \$ _ \$ _ => true
```
```    64     | _ => false)
```
```    65
```
```    66   val thms = map mk_meta_eq @{lemma
```
```    67     "(case P of True => x | False => y) = (if P then x else y)"
```
```    68     "(case P of False => y | True => x) = (if P then x else y)"
```
```    69     by simp_all}
```
```    70   val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
```
```    71 in
```
```    72 fun rewrite_bool_cases ctxt =
```
```    73   map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
```
```    74     Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
```
```    75 end
```
```    76
```
```    77
```
```    78
```
```    79 (* normalization of numerals: rewriting of negative integer numerals into
```
```    80    positive numerals, Numeral0 into 0, Numeral1 into 1 *)
```
```    81
```
```    82 local
```
```    83   fun is_number_sort ctxt T =
```
```    84     Sign.of_sort (ProofContext.theory_of ctxt) (T, @{sort number_ring})
```
```    85
```
```    86   fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) \$ _) =
```
```    87         (case try HOLogic.dest_number t of
```
```    88           SOME (T, i) => is_number_sort ctxt T andalso i < 2
```
```    89         | NONE => false)
```
```    90     | is_strange_number _ _ = false
```
```    91
```
```    92   val pos_numeral_ss = HOL_ss
```
```    93     addsimps [@{thm Int.number_of_minus}, @{thm Int.number_of_Min}]
```
```    94     addsimps [@{thm Int.number_of_Pls}, @{thm Int.numeral_1_eq_1}]
```
```    95     addsimps @{thms Int.pred_bin_simps}
```
```    96     addsimps @{thms Int.normalize_bin_simps}
```
```    97     addsimps @{lemma
```
```    98       "Int.Min = - Int.Bit1 Int.Pls"
```
```    99       "Int.Bit0 (- Int.Pls) = - Int.Pls"
```
```   100       "Int.Bit0 (- k) = - Int.Bit0 k"
```
```   101       "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
```
```   102       by simp_all (simp add: pred_def)}
```
```   103
```
```   104   fun pos_conv ctxt = if_conv (is_strange_number ctxt)
```
```   105     (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
```
```   106     Conv.no_conv
```
```   107 in
```
```   108 fun normalize_numerals ctxt =
```
```   109   map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
```
```   110     Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
```
```   111 end
```
```   112
```
```   113
```
```   114
```
```   115 (* embedding of standard natural number operations into integer operations *)
```
```   116
```
```   117 local
```
```   118   val nat_embedding = @{lemma
```
```   119     "nat (int n) = n"
```
```   120     "i >= 0 --> int (nat i) = i"
```
```   121     "i < 0 --> int (nat i) = 0"
```
```   122     by simp_all}
```
```   123
```
```   124   val nat_rewriting = @{lemma
```
```   125     "0 = nat 0"
```
```   126     "1 = nat 1"
```
```   127     "number_of i = nat (number_of i)"
```
```   128     "int (nat 0) = 0"
```
```   129     "int (nat 1) = 1"
```
```   130     "a < b = (int a < int b)"
```
```   131     "a <= b = (int a <= int b)"
```
```   132     "Suc a = nat (int a + 1)"
```
```   133     "a + b = nat (int a + int b)"
```
```   134     "a - b = nat (int a - int b)"
```
```   135     "a * b = nat (int a * int b)"
```
```   136     "a div b = nat (int a div int b)"
```
```   137     "a mod b = nat (int a mod int b)"
```
```   138     "min a b = nat (min (int a) (int b))"
```
```   139     "max a b = nat (max (int a) (int b))"
```
```   140     "int (nat (int a + int b)) = int a + int b"
```
```   141     "int (nat (int a * int b)) = int a * int b"
```
```   142     "int (nat (int a div int b)) = int a div int b"
```
```   143     "int (nat (int a mod int b)) = int a mod int b"
```
```   144     "int (nat (min (int a) (int b))) = min (int a) (int b)"
```
```   145     "int (nat (max (int a) (int b))) = max (int a) (int b)"
```
```   146     by (simp_all add: nat_mult_distrib nat_div_distrib nat_mod_distrib
```
```   147       int_mult[symmetric] zdiv_int[symmetric] zmod_int[symmetric])}
```
```   148
```
```   149   fun on_positive num f x =
```
```   150     (case try HOLogic.dest_number (Thm.term_of num) of
```
```   151       SOME (_, i) => if i >= 0 then SOME (f x) else NONE
```
```   152     | NONE => NONE)
```
```   153
```
```   154   val cancel_int_nat_ss = HOL_ss
```
```   155     addsimps [@{thm Nat_Numeral.nat_number_of}]
```
```   156     addsimps [@{thm Nat_Numeral.int_nat_number_of}]
```
```   157     addsimps @{thms neg_simps}
```
```   158
```
```   159   fun cancel_int_nat_simproc _ ss ct =
```
```   160     let
```
```   161       val num = Thm.dest_arg (Thm.dest_arg ct)
```
```   162       val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
```
```   163       val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
```
```   164       fun tac _ = Simplifier.simp_tac simpset 1
```
```   165     in on_positive num (Goal.prove_internal [] goal) tac end
```
```   166
```
```   167   val nat_ss = HOL_ss
```
```   168     addsimps nat_rewriting
```
```   169     addsimprocs [Simplifier.make_simproc {
```
```   170       name = "cancel_int_nat_num", lhss = [@{cpat "int (nat _)"}],
```
```   171       proc = cancel_int_nat_simproc, identifier = [] }]
```
```   172
```
```   173   fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
```
```   174
```
```   175   val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
```
```   176   val uses_nat_int =
```
```   177     Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
```
```   178 in
```
```   179 fun nat_as_int ctxt =
```
```   180   map ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt)) #>
```
```   181   exists (uses_nat_int o Thm.prop_of) ?? append nat_embedding
```
```   182 end
```
```   183
```
```   184
```
```   185
```
```   186 (* further normalizations: beta/eta, universal closure, atomize *)
```
```   187
```
```   188 val eta_expand_eq = @{lemma "f == (%x. f x)" by (rule reflexive)}
```
```   189
```
```   190 fun eta_expand_conv cv ctxt =
```
```   191   Conv.rewr_conv eta_expand_eq then_conv Conv.abs_conv (cv o snd) ctxt
```
```   192
```
```   193 local
```
```   194   val eta_conv = eta_expand_conv
```
```   195
```
```   196   fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt
```
```   197   and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt)
```
```   198   and keep_let_conv ctxt = Conv.combination_conv
```
```   199     (Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt)
```
```   200   and unfold_let_conv ctxt = Conv.combination_conv
```
```   201     (Conv.arg_conv (norm_conv ctxt)) (eta_conv norm_conv ctxt)
```
```   202   and unfold_conv thm ctxt = Conv.rewr_conv thm then_conv keep_conv ctxt
```
```   203   and unfold_ex1_conv ctxt = unfold_conv @{thm Ex1_def} ctxt
```
```   204   and unfold_ball_conv ctxt = unfold_conv (mk_meta_eq @{thm Ball_def}) ctxt
```
```   205   and unfold_bex_conv ctxt = unfold_conv (mk_meta_eq @{thm Bex_def}) ctxt
```
```   206   and norm_conv ctxt ct =
```
```   207     (case Thm.term_of ct of
```
```   208       Const (@{const_name All}, _) \$ Abs _ => keep_conv
```
```   209     | Const (@{const_name All}, _) \$ _ => eta_binder_conv
```
```   210     | Const (@{const_name All}, _) => eta_conv eta_binder_conv
```
```   211     | Const (@{const_name Ex}, _) \$ Abs _ => keep_conv
```
```   212     | Const (@{const_name Ex}, _) \$ _ => eta_binder_conv
```
```   213     | Const (@{const_name Ex}, _) => eta_conv eta_binder_conv
```
```   214     | Const (@{const_name Let}, _) \$ _ \$ Abs _ => keep_let_conv
```
```   215     | Const (@{const_name Let}, _) \$ _ \$ _ => unfold_let_conv
```
```   216     | Const (@{const_name Let}, _) \$ _ => eta_conv unfold_let_conv
```
```   217     | Const (@{const_name Let}, _) => eta_conv (eta_conv unfold_let_conv)
```
```   218     | Const (@{const_name Ex1}, _) \$ _ => unfold_ex1_conv
```
```   219     | Const (@{const_name Ex1}, _) => eta_conv unfold_ex1_conv
```
```   220     | Const (@{const_name Ball}, _) \$ _ \$ _ => unfold_ball_conv
```
```   221     | Const (@{const_name Ball}, _) \$ _ => eta_conv unfold_ball_conv
```
```   222     | Const (@{const_name Ball}, _) => eta_conv (eta_conv unfold_ball_conv)
```
```   223     | Const (@{const_name Bex}, _) \$ _ \$ _ => unfold_bex_conv
```
```   224     | Const (@{const_name Bex}, _) \$ _ => eta_conv unfold_bex_conv
```
```   225     | Const (@{const_name Bex}, _) => eta_conv (eta_conv unfold_bex_conv)
```
```   226     | Abs _ => Conv.abs_conv (norm_conv o snd)
```
```   227     | _ \$ _ => Conv.comb_conv o norm_conv
```
```   228     | _ => K Conv.all_conv) ctxt ct
```
```   229
```
```   230   fun is_normed t =
```
```   231     (case t of
```
```   232       Const (@{const_name All}, _) \$ Abs (_, _, u) => is_normed u
```
```   233     | Const (@{const_name All}, _) \$ _ => false
```
```   234     | Const (@{const_name All}, _) => false
```
```   235     | Const (@{const_name Ex}, _) \$ Abs (_, _, u) => is_normed u
```
```   236     | Const (@{const_name Ex}, _) \$ _ => false
```
```   237     | Const (@{const_name Ex}, _) => false
```
```   238     | Const (@{const_name Let}, _) \$ u1 \$ Abs (_, _, u2) =>
```
```   239         is_normed u1 andalso is_normed u2
```
```   240     | Const (@{const_name Let}, _) \$ _ \$ _ => false
```
```   241     | Const (@{const_name Let}, _) \$ _ => false
```
```   242     | Const (@{const_name Let}, _) => false
```
```   243     | Const (@{const_name Ex1}, _) => false
```
```   244     | Const (@{const_name Ball}, _) => false
```
```   245     | Const (@{const_name Bex}, _) => false
```
```   246     | Abs (_, _, u) => is_normed u
```
```   247     | u1 \$ u2 => is_normed u1 andalso is_normed u2
```
```   248     | _ => true)
```
```   249 in
```
```   250 fun norm_binder_conv ctxt = if_conv is_normed Conv.all_conv (norm_conv ctxt)
```
```   251 end
```
```   252
```
```   253 fun norm_def ctxt thm =
```
```   254   (case Thm.prop_of thm of
```
```   255     @{term Trueprop} \$ (Const (@{const_name HOL.eq}, _) \$ _ \$ Abs _) =>
```
```   256       norm_def ctxt (thm RS @{thm fun_cong})
```
```   257   | Const (@{const_name "=="}, _) \$ _ \$ Abs _ =>
```
```   258       norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
```
```   259   | _ => thm)
```
```   260
```
```   261 fun atomize_conv ctxt ct =
```
```   262   (case Thm.term_of ct of
```
```   263     @{term "op ==>"} \$ _ \$ _ =>
```
```   264       Conv.binop_conv (atomize_conv ctxt) then_conv
```
```   265       Conv.rewr_conv @{thm atomize_imp}
```
```   266   | Const (@{const_name "=="}, _) \$ _ \$ _ =>
```
```   267       Conv.binop_conv (atomize_conv ctxt) then_conv
```
```   268       Conv.rewr_conv @{thm atomize_eq}
```
```   269   | Const (@{const_name all}, _) \$ Abs _ =>
```
```   270       Conv.binder_conv (atomize_conv o snd) ctxt then_conv
```
```   271       Conv.rewr_conv @{thm atomize_all}
```
```   272   | _ => Conv.all_conv) ct
```
```   273
```
```   274 fun normalize_rule ctxt =
```
```   275   Conv.fconv_rule (
```
```   276     (* reduce lambda abstractions, except at known binders: *)
```
```   277     Thm.beta_conversion true then_conv
```
```   278     Thm.eta_conversion then_conv
```
```   279     norm_binder_conv ctxt) #>
```
```   280   norm_def ctxt #>
```
```   281   Drule.forall_intr_vars #>
```
```   282   Conv.fconv_rule (atomize_conv ctxt)
```
```   283
```
```   284
```
```   285
```
```   286 (* lift lambda terms into additional rules *)
```
```   287
```
```   288 local
```
```   289   val meta_eq = @{cpat "op =="}
```
```   290   val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
```
```   291   fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
```
```   292   fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
```
```   293
```
```   294   fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
```
```   295
```
```   296   fun used_vars cvs ct =
```
```   297     let
```
```   298       val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
```
```   299       val add = (fn SOME ct => insert (op aconvc) ct | _ => I)
```
```   300     in Term.fold_aterms (add o lookup) (Thm.term_of ct) [] end
```
```   301
```
```   302   fun apply cv thm =
```
```   303     let val thm' = Thm.combination thm (Thm.reflexive cv)
```
```   304     in Thm.transitive thm' (Thm.beta_conversion false (Thm.rhs_of thm')) end
```
```   305   fun apply_def cvs eq = Thm.symmetric (fold apply cvs eq)
```
```   306
```
```   307   fun replace_lambda cvs ct (cx as (ctxt, defs)) =
```
```   308     let
```
```   309       val cvs' = used_vars cvs ct
```
```   310       val ct' = fold_rev Thm.cabs cvs' ct
```
```   311     in
```
```   312       (case Termtab.lookup defs (Thm.term_of ct') of
```
```   313         SOME eq => (apply_def cvs' eq, cx)
```
```   314       | NONE =>
```
```   315           let
```
```   316             val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
```
```   317             val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
```
```   318             val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
```
```   319             val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
```
```   320             val defs' = Termtab.update (Thm.term_of ct', eq) defs
```
```   321           in (apply_def cvs' eq, (ctxt'', defs')) end)
```
```   322     end
```
```   323
```
```   324   fun none ct cx = (Thm.reflexive ct, cx)
```
```   325   fun in_comb f g ct cx =
```
```   326     let val (cu1, cu2) = Thm.dest_comb ct
```
```   327     in cx |> f cu1 ||>> g cu2 |>> uncurry Thm.combination end
```
```   328   fun in_arg f = in_comb none f
```
```   329   fun in_abs f cvs ct (ctxt, defs) =
```
```   330     let
```
```   331       val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
```
```   332       val (cv, cu) = Thm.dest_abs (SOME n) ct
```
```   333     in  (ctxt', defs) |> f (cv :: cvs) cu |>> Thm.abstract_rule n cv end
```
```   334
```
```   335   fun traverse cvs ct =
```
```   336     (case Thm.term_of ct of
```
```   337       Const (@{const_name All}, _) \$ Abs _ => in_arg (in_abs traverse cvs)
```
```   338     | Const (@{const_name Ex}, _) \$ Abs _ => in_arg (in_abs traverse cvs)
```
```   339     | Const (@{const_name Let}, _) \$ _ \$ Abs _ =>
```
```   340         in_comb (in_arg (traverse cvs)) (in_abs traverse cvs)
```
```   341     | Abs _ => at_lambda cvs
```
```   342     | _ \$ _ => in_comb (traverse cvs) (traverse cvs)
```
```   343     | _ => none) ct
```
```   344
```
```   345   and at_lambda cvs ct =
```
```   346     in_abs traverse cvs ct #-> (fn thm =>
```
```   347     replace_lambda cvs (Thm.rhs_of thm) #>> Thm.transitive thm)
```
```   348
```
```   349   fun has_free_lambdas t =
```
```   350     (case t of
```
```   351       Const (@{const_name All}, _) \$ Abs (_, _, u) => has_free_lambdas u
```
```   352     | Const (@{const_name Ex}, _) \$ Abs (_, _, u) => has_free_lambdas u
```
```   353     | Const (@{const_name Let}, _) \$ u1 \$ Abs (_, _, u2) =>
```
```   354         has_free_lambdas u1 orelse has_free_lambdas u2
```
```   355     | Abs _ => true
```
```   356     | u1 \$ u2 => has_free_lambdas u1 orelse has_free_lambdas u2
```
```   357     | _ => false)
```
```   358
```
```   359   fun lift_lm f thm cx =
```
```   360     if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx)
```
```   361     else cx |> f (Thm.cprop_of thm) |>> (fn thm' => Thm.equal_elim thm' thm)
```
```   362 in
```
```   363 fun lift_lambdas thms ctxt =
```
```   364   let
```
```   365     val cx = (ctxt, Termtab.empty)
```
```   366     val (thms', (ctxt', defs)) = fold_map (lift_lm (traverse [])) thms cx
```
```   367     val eqs = Termtab.fold (cons o normalize_rule ctxt' o snd) defs []
```
```   368   in (eqs @ thms', ctxt') end
```
```   369 end
```
```   370
```
```   371
```
```   372
```
```   373 (* make application explicit for functions with varying number of arguments *)
```
```   374
```
```   375 local
```
```   376   val const = prefix "c" and free = prefix "f"
```
```   377   fun min i (e as (_, j)) = if i <> j then (true, Int.min (i, j)) else e
```
```   378   fun add t i = Symtab.map_default (t, (false, i)) (min i)
```
```   379   fun traverse t =
```
```   380     (case Term.strip_comb t of
```
```   381       (Const (n, _), ts) => add (const n) (length ts) #> fold traverse ts
```
```   382     | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts
```
```   383     | (Abs (_, _, u), ts) => fold traverse (u :: ts)
```
```   384     | (_, ts) => fold traverse ts)
```
```   385   val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I)
```
```   386   fun prune_tab tab = Symtab.fold prune tab Symtab.empty
```
```   387
```
```   388   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
```
```   389   fun nary_conv conv1 conv2 ct =
```
```   390     (Conv.combination_conv (nary_conv conv1 conv2) conv2 else_conv conv1) ct
```
```   391   fun abs_conv conv tb = Conv.abs_conv (fn (cv, cx) =>
```
```   392     let val n = fst (Term.dest_Free (Thm.term_of cv))
```
```   393     in conv (Symtab.update (free n, 0) tb) cx end)
```
```   394   val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
```
```   395 in
```
```   396 fun explicit_application ctxt thms =
```
```   397   let
```
```   398     fun sub_conv tb ctxt ct =
```
```   399       (case Term.strip_comb (Thm.term_of ct) of
```
```   400         (Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt
```
```   401       | (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt
```
```   402       | (Abs _, _) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt)
```
```   403       | (_, _) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct
```
```   404     and app_conv tb n i ctxt =
```
```   405       (case Symtab.lookup tb n of
```
```   406         NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
```
```   407       | SOME j => fun_app_conv tb ctxt (i - j))
```
```   408     and fun_app_conv tb ctxt i ct = (
```
```   409       if i = 0 then nary_conv Conv.all_conv (sub_conv tb ctxt)
```
```   410       else
```
```   411         Conv.rewr_conv fun_app_rule then_conv
```
```   412         binop_conv (fun_app_conv tb ctxt (i-1)) (sub_conv tb ctxt)) ct
```
```   413
```
```   414     fun needs_exp_app tab = Term.exists_subterm (fn
```
```   415         Bound _ \$ _ => true
```
```   416       | Const (n, _) => Symtab.defined tab (const n)
```
```   417       | Free (n, _) => Symtab.defined tab (free n)
```
```   418       | _ => false)
```
```   419
```
```   420     fun rewrite tab ctxt thm =
```
```   421       if not (needs_exp_app tab (Thm.prop_of thm)) then thm
```
```   422       else Conv.fconv_rule (sub_conv tab ctxt) thm
```
```   423
```
```   424     val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty)
```
```   425   in map (rewrite tab ctxt) thms end
```
```   426 end
```
```   427
```
```   428
```
```   429
```
```   430 (* combined normalization *)
```
```   431
```
```   432 type extra_norm = thm list -> Proof.context -> thm list * Proof.context
```
```   433
```
```   434 fun with_context f thms ctxt = (f ctxt thms, ctxt)
```
```   435
```
```   436 fun normalize extra_norm thms ctxt =
```
```   437   thms
```
```   438   |> trivial_distinct ctxt
```
```   439   |> rewrite_bool_cases ctxt
```
```   440   |> normalize_numerals ctxt
```
```   441   |> nat_as_int ctxt
```
```   442   |> rpair ctxt
```
```   443   |-> extra_norm
```
```   444   |-> with_context (fn cx => map (normalize_rule cx))
```
```   445   |-> SMT_Monomorph.monomorph
```
```   446   |-> lift_lambdas
```
```   447   |-> with_context explicit_application
```
```   448
```
```   449 end
```