src/Tools/auto_solve.ML
 changeset 33301 1fe9fc908ec3 parent 33290 6dcb0a970783 child 33889 4328de748fb2
equal inserted replaced
33300:939ca97f5a11 33301:1fe9fc908ec3
`     3 `
`     3 `
`     4 Check whether a newly stated theorem can be solved directly by an`
`     4 Check whether a newly stated theorem can be solved directly by an`
`     5 existing theorem.  Duplicate lemmas can be detected in this way.`
`     5 existing theorem.  Duplicate lemmas can be detected in this way.`
`     6 `
`     6 `
`     7 The implementation is based in part on Berghofer and Haftmann's`
`     7 The implementation is based in part on Berghofer and Haftmann's`
`     8 quickcheck.ML.  It relies critically on the FindTheorems solves`
`     8 quickcheck.ML.  It relies critically on the Find_Theorems solves`
`     9 feature.`
`     9 feature.`
`    10 *)`
`    10 *)`
`    11 `
`    11 `
`    12 signature AUTO_SOLVE =`
`    12 signature AUTO_SOLVE =`
`    13 sig`
`    13 sig`
`    43 `
`    43 `
`    44 val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>`
`    44 val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>`
`    45   let`
`    45   let`
`    46     val ctxt = Proof.context_of state;`
`    46     val ctxt = Proof.context_of state;`
`    47 `
`    47 `
`    48     val crits = [(true, FindTheorems.Solves)];`
`    48     val crits = [(true, Find_Theorems.Solves)];`
`    49     fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);`
`    49     fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);`
`    50 `
`    50 `
`    51     fun prt_result (goal, results) =`
`    51     fun prt_result (goal, results) =`
`    52       let`
`    52       let`
`    53         val msg =`
`    53         val msg =`
`    54           (case goal of`
`    54           (case goal of`
`    55             NONE => "The current goal"`
`    55             NONE => "The current goal"`
`    56           | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));`
`    56           | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));`
`    57       in`
`    57       in`
`    58         Pretty.big_list`
`    58         Pretty.big_list`
`    59           (msg ^ " could be solved directly with:")`
`    59           (msg ^ " could be solved directly with:")`
`    60           (map (FindTheorems.pretty_thm ctxt) results)`
`    60           (map (Find_Theorems.pretty_thm ctxt) results)`
`    61       end;`
`    61       end;`
`    62 `
`    62 `
`    63     fun seek_against_goal () =`
`    63     fun seek_against_goal () =`
`    64       (case try Proof.simple_goal state of`
`    64       (case try Proof.simple_goal state of`
`    65         NONE => NONE`
`    65         NONE => NONE`