All of the lemmas involved are either arihmetic or logical inference
rules and make sense. Presburger is a generic and complex decision
procedure. I am not surprised and would not want to optimize presburger
to use fewer lemmas.
Tobias
Am 28/06/2011 00:08, schrieb Jasmin Blanchette:
Hi all,
Quick question: Josef Urban noticed that the proof terms for some lemmas proved directly by
"presburger" can refer to lots of other lemmas; for example, the proof of
"Parity.even_mult_two_ex" directly refers to 206 lemmas.
ML {* Thm.proof_body_of @{thm Parity.even_mult_two_ex} *}
(I've attached the list.) Is that normal? Does this have anything to do with
"presburger"?
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
