[isabelle] Use of simp add:

I would appreciate some kind of strategy to determine what to write after simp add: when proving a simple fact. This first came up for me when I was trying to prove "floor (9.5::real) = (9::int)" and "ceiling (9.5::real) = (10::int)". Here try0 was no help; it tried simp, auto, fast, fastforce, force, blast, metis, linarith, and presburger, and then reported no proof found. Quite by accident, I found out how to do these; you type simp add: floor_unique or simp add: ceiling_unique . I'd like to know how to find rules like floor_unique and ceiling_unique in other cases. The one I'm concerned about now is "(2::nat)*x ~= 3", which arose for me as an unproved subgoal. Yes, I know I can prove this one by presburger, because try0 told me so, but that seems like using an elephant to crush a flea; presburger took forever to find a proof. I've also tried find_theorems, but that said it found over 18,000 theorems and none of the first few looked promising. I'm sure there's a much simpler way of proving that "(2::nat)*x ~= 3", and I'm sure that many people on the mailing list know what it is, but what I'd really appreciate is some hints on how to find something like this. -Douglas
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.