src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42747 f132d13fcf75
parent 42742 369dfc819056
child 42750 c8b1d9ee3758
equal deleted 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) =