src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42549 b9754f26c7bc
parent 42548 ea2a28b1938f
child 42551 cd99d6d3027a
equal deleted inserted replaced
42548:ea2a28b1938f 42549:b9754f26c7bc
    21 
    21 
    22   val fact_prefix : string
    22   val fact_prefix : string
    23   val conjecture_prefix : string
    23   val conjecture_prefix : string
    24   val boolify_base : string
    24   val boolify_base : string
    25   val explicit_app_base : string
    25   val explicit_app_base : string
       
    26   val type_pred_base : string
    26   val is_type_system_sound : type_system -> bool
    27   val is_type_system_sound : type_system -> bool
    27   val type_system_types_dangerous_types : type_system -> bool
    28   val type_system_types_dangerous_types : type_system -> bool
    28   val num_atp_type_args : theory -> type_system -> string -> int
    29   val num_atp_type_args : theory -> type_system -> string -> int
    29   val unmangled_const : string -> string * string fo_term list
    30   val unmangled_const : string -> string * string fo_term list
    30   val translate_atp_fact :
    31   val translate_atp_fact :
   512   case combtyp_from_typ @{typ "unit => bool"} of
   513   case combtyp_from_typ @{typ "unit => bool"} of
   513     CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
   514     CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
   514   | _ => raise Fail "expected two-argument type constructor"
   515   | _ => raise Fail "expected two-argument type constructor"
   515 
   516 
   516 fun type_pred_combatom type_sys ty tm =
   517 fun type_pred_combatom type_sys ty tm =
   517   CombApp (CombConst ((const_prefix ^ type_pred_base, type_pred_base),
   518   CombApp (CombConst (`make_fixed_const type_pred_base, pred_combtyp ty, [ty]),
   518                       pred_combtyp ty, [ty]), tm)
   519            tm)
   519   |> repair_combterm_consts type_sys
   520   |> repair_combterm_consts type_sys
   520   |> AAtom
   521   |> AAtom
   521 
   522 
   522 fun formula_for_combformula ctxt type_sys =
   523 fun formula_for_combformula ctxt type_sys =
   523   let
   524   let