made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
authorboehmes
Sun Jun 05 15:00:17 2011 +0200 (2011-06-05)
changeset 4315472e4753a6677
parent 43153 cbb748ccf81b
child 43155 f4f27123daef
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Jun 03 19:37:26 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Jun 05 15:00:17 2011 +0200
     1.3 @@ -321,15 +321,19 @@
     1.4      Make application explicit for functions with varying number of arguments.
     1.5    *)
     1.6  
     1.7 -  fun add t i = Termtab.map_default (t, i) (Integer.min i)
     1.8 +  fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i))
     1.9 +  fun add_type T = apsnd (Typtab.update (T, ()))
    1.10  
    1.11    fun min_arities t =
    1.12      (case Term.strip_comb t of
    1.13        (u as Const _, ts) => add u (length ts) #> fold min_arities ts
    1.14      | (u as Free _, ts) => add u (length ts) #> fold min_arities ts
    1.15 -    | (Abs (_, _, u), ts) => min_arities u #> fold min_arities ts
    1.16 +    | (Abs (_, T, u), ts) => add_type T #> min_arities u #> fold min_arities ts
    1.17      | (_, ts) => fold min_arities ts)
    1.18  
    1.19 +  fun minimize types t i =
    1.20 +    if i = 0 orelse Typtab.defined types (Term.type_of t) then 0 else i
    1.21 +
    1.22    fun app u (t, T) =
    1.23      (Const (@{const_name SMT.fun_app}, T --> T) $ t $ u, Term.range_type T)
    1.24  
    1.25 @@ -340,14 +344,22 @@
    1.26      in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
    1.27  in
    1.28  
    1.29 -fun intro_explicit_application ts =
    1.30 +fun intro_explicit_application ctxt ts =
    1.31    let
    1.32 -    val arities = fold min_arities ts Termtab.empty
    1.33 -    fun apply' t = apply (the (Termtab.lookup arities t)) t
    1.34 +    val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
    1.35 +    val arities' = Termtab.map (minimize types) arities
    1.36 +    fun apply' t = apply (the (Termtab.lookup arities' t)) t
    1.37  
    1.38      fun traverse Ts t =
    1.39        (case Term.strip_comb t of
    1.40 -        (u as Const (_, T), ts) => apply' u T (map (traverse Ts) ts)
    1.41 +        (q as Const (@{const_name All}, _), [u as Abs _]) => q $ traverse Ts u
    1.42 +      | (q as Const (@{const_name Ex}, _), [u as Abs _]) => q $ traverse Ts u
    1.43 +      | (q as Const (@{const_name Ex}, _), [u1 as Abs _, u2]) =>
    1.44 +          q $ traverse Ts u1 $ traverse Ts u2
    1.45 +      | (u as Const (c as (_, T)), ts) =>
    1.46 +          (case SMT_Builtin.dest_builtin ctxt c ts of
    1.47 +            SOME (_, _, us, mk) => mk (map (traverse Ts) us)
    1.48 +          | NONE => apply' u T (map (traverse Ts) ts))
    1.49        | (u as Free (_, T), ts) => apply' u T (map (traverse Ts) ts)
    1.50        | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
    1.51        | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
    1.52 @@ -574,7 +586,7 @@
    1.53        ts2
    1.54        |> eta_expand ctxt1 is_fol funcs
    1.55        |> lift_lambdas ctxt1
    1.56 -      ||> intro_explicit_application
    1.57 +      |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1)
    1.58  
    1.59      val ((rewrite_rules, extra_thms, builtin), ts4) =
    1.60        (if is_fol then folify ctxt2 else pair ([], [], I)) ts3