src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
 changeset 42747 f132d13fcf75 parent 42742 369dfc819056 child 42750 c8b1d9ee3758
equal inserted replaced
42746:7e227e9de779 42747:f132d13fcf75
`   353                     (0 upto length Ts - 1 ~~ Ts), t)`
`   353                     (0 upto length Ts - 1 ~~ Ts), t)`
`   354 fun reveal_bounds Ts =`
`   354 fun reveal_bounds Ts =`
`   355   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))`
`   355   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))`
`   356                     (0 upto length Ts - 1 ~~ Ts))`
`   356                     (0 upto length Ts - 1 ~~ Ts))`
`   357 `
`   357 `
`   358 (* Removes the lambdas from an equation of the form "t = (%x. u)".`
`   358 fun extensionalize_term ctxt t =`
`   359    (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)`
`   359   let val thy = Proof_Context.theory_of ctxt in`
`   360 fun extensionalize_term t =`
`   360     t |> cterm_of thy |> Meson.extensionalize_conv ctxt`
`   361   let`
`   361       |> prop_of |> Logic.dest_equals |> snd`
`   362     fun aux j (@{const Trueprop} \$ t') = @{const Trueprop} \$ aux j t'`
`   362   end`
`   363       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),`
`       `
`   364                                         Type (_, [_, res_T])]))`
`       `
`   365                     \$ t2 \$ Abs (var_s, var_T, t')) =`
`       `
`   366         if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then`
`       `
`   367           let val var_t = Var ((var_s, j), var_T) in`
`       `
`   368             Const (s, T' --> T' --> res_T)`
`       `
`   369               \$ betapply (t2, var_t) \$ subst_bound (var_t, t')`
`       `
`   370             |> aux (j + 1)`
`       `
`   371           end`
`       `
`   372         else`
`       `
`   373           t`
`       `
`   374       | aux _ t = t`
`       `
`   375   in aux (maxidx_of_term t + 1) t end`
`       `
`   376 `
`   363 `
`   377 fun introduce_combinators_in_term ctxt kind t =`
`   364 fun introduce_combinators_in_term ctxt kind t =`
`   378   let val thy = Proof_Context.theory_of ctxt in`
`   365   let val thy = Proof_Context.theory_of ctxt in`
`   379     if Meson.is_fol_term thy t then`
`   366     if Meson.is_fol_term thy t then`
`   380       t`
`   367       t`
`   434               |> Object_Logic.atomize_term thy`
`   421               |> Object_Logic.atomize_term thy`
`   435     val need_trueprop = (fastype_of t = @{typ bool})`
`   422     val need_trueprop = (fastype_of t = @{typ bool})`
`   436     val t = t |> need_trueprop ? HOLogic.mk_Trueprop`
`   423     val t = t |> need_trueprop ? HOLogic.mk_Trueprop`
`   437               |> Raw_Simplifier.rewrite_term thy`
`   424               |> Raw_Simplifier.rewrite_term thy`
`   438                      (Meson.unfold_set_const_simps ctxt) []`
`   425                      (Meson.unfold_set_const_simps ctxt) []`
`   439               |> extensionalize_term`
`   426               |> extensionalize_term ctxt`
`   440               |> presimp ? presimplify_term thy`
`   427               |> presimp ? presimplify_term thy`
`   441               |> perhaps (try (HOLogic.dest_Trueprop))`
`   428               |> perhaps (try (HOLogic.dest_Trueprop))`
`   442               |> introduce_combinators_in_term ctxt kind`
`   429               |> introduce_combinators_in_term ctxt kind`
`   443               |> kind <> Axiom ? freeze_term`
`   430               |> kind <> Axiom ? freeze_term`
`   444     val (combformula, atomic_types) =`
`   431     val (combformula, atomic_types) =`