src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42944 9e620869a576
parent 42943 62a14c80d194
child 42951 40bf0173fbed
equal deleted inserted replaced
42943:62a14c80d194 42944:9e620869a576
   174 
   174 
   175 fun is_type_level_fairly_sound level =
   175 fun is_type_level_fairly_sound level =
   176   is_type_level_virtually_sound level orelse level = Finite_Types
   176   is_type_level_virtually_sound level orelse level = Finite_Types
   177 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   177 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
   178 
   178 
   179 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
       
   180   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
       
   181   | formula_map f (AAtom tm) = AAtom (f tm)
       
   182 
       
   183 fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
   179 fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
   184   | aconn_fold pos f (AImplies, [phi1, phi2]) =
   180   | aconn_fold pos f (AImplies, [phi1, phi2]) =
   185     f (Option.map not pos) phi1 #> f pos phi2
   181     f (Option.map not pos) phi1 #> f pos phi2
   186   | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
   182   | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
   187   | aconn_fold pos f (AOr, phis) = fold (f pos) phis
   183   | aconn_fold pos f (AOr, phis) = fold (f pos) phis
   450 (* making fact and conjecture formulas *)
   446 (* making fact and conjecture formulas *)
   451 fun make_formula ctxt eq_as_iff presimp name loc kind t =
   447 fun make_formula ctxt eq_as_iff presimp name loc kind t =
   452   let
   448   let
   453     val thy = Proof_Context.theory_of ctxt
   449     val thy = Proof_Context.theory_of ctxt
   454     val t = t |> Envir.beta_eta_contract
   450     val t = t |> Envir.beta_eta_contract
   455               |> transform_elim_term
   451               |> transform_elim_prop
   456               |> Object_Logic.atomize_term thy
   452               |> Object_Logic.atomize_term thy
   457     val need_trueprop = (fastype_of t = @{typ bool})
   453     val need_trueprop = (fastype_of t = @{typ bool})
   458     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   454     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   459               |> Raw_Simplifier.rewrite_term thy
   455               |> Raw_Simplifier.rewrite_term thy
   460                      (Meson.unfold_set_const_simps ctxt) []
   456                      (Meson.unfold_set_const_simps ctxt) []