summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Tools/auto_solve.ML

changeset 33301 | 1fe9fc908ec3 |

parent 33290 | 6dcb0a970783 |

child 33889 | 4328de748fb2 |

equal
deleted
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 |