src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 50967 00d87ade2294
parent 50965 7a7d1418301e
child 50969 4179fa5c79fe
equal deleted inserted replaced
50966:b85cb3049df9 50967:00d87ade2294
    44       -> string list * (string * real) list * string list -> string list
    44       -> string list * (string * real) list * string list -> string list
    45   end
    45   end
    46 
    46 
    47   val mash_unlearn : Proof.context -> unit
    47   val mash_unlearn : Proof.context -> unit
    48   val nickname_of_thm : thm -> string
    48   val nickname_of_thm : thm -> string
    49   val find_suggested_facts : string list -> ('b * thm) list -> ('b * thm) list
    49   val find_suggested_facts : ('b * thm) list -> string list -> ('b * thm) list
    50   val mesh_facts :
    50   val mesh_facts :
    51     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
    51     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
    52     -> 'a list
    52     -> 'a list
    53   val theory_ord : theory * theory -> order
    53   val theory_ord : theory * theory -> order
    54   val thm_ord : thm * thm -> order
    54   val thm_ord : thm * thm -> order
   431       | NONE => hint
   431       | NONE => hint
   432     end
   432     end
   433   else
   433   else
   434     elided_backquote_thm 200 th
   434     elided_backquote_thm 200 th
   435 
   435 
   436 fun find_suggested_facts suggs facts =
   436 fun find_suggested_facts facts =
   437   let
   437   let
   438     fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
   438     fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
   439     val tab = fold add_fact facts Symtab.empty
   439     val tab = fold add_fact facts Symtab.empty
   440   in map_filter (Symtab.lookup tab) suggs end
   440   in map_filter (Symtab.lookup tab) end
   441 
   441 
   442 fun scaled_avg [] = 0
   442 fun scaled_avg [] = 0
   443   | scaled_avg xs =
   443   | scaled_avg xs =
   444     Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
   444     Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
   445 
   445 
   772 val max_proximity_facts = 100
   772 val max_proximity_facts = 100
   773 
   773 
   774 fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
   774 fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
   775   | find_mash_suggestions max_facts suggs facts chained raw_unknown =
   775   | find_mash_suggestions max_facts suggs facts chained raw_unknown =
   776     let
   776     let
   777       val raw_mash = find_suggested_facts suggs facts
   777       val raw_mash = find_suggested_facts facts suggs
   778       val unknown_chained =
   778       val unknown_chained =
   779         inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
   779         inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
   780       val proximity =
   780       val proximity =
   781         facts |> sort (thm_ord o pairself snd o swap)
   781         facts |> sort (thm_ord o pairself snd o swap)
   782               |> take max_proximity_facts
   782               |> take max_proximity_facts