Edit: That is all my bad, I discovered later that I missed a case when doing an inductive definition. It really confused me for quite a while, so I keep the post here for information that "what happens if you miss a pattern in an inductive definition" But I believe my problem is solved now.
I define some formula syntax in Isabelle, and it generates a bunch of lemmas which give a contradition. I do not have any clue what is wrong now. May I please ask for hints?
I defined classical formula syntax by:
datatype ('m,'p) cform = cVAR "'p"
| cFALSE
| cDISJ "('m,'p) cform" "('m,'p) cform"
| cNOT "('m,'p) cform"
| cDIAM 'm "(('m,'p) cform) list" ("♢_ _" [0, 0])
And I defined a function "mops", collecting modal operators from formulas:
fun mops_cform :: "('m,'p) cform ⇒ 'm set" where
"mops_cform (cFALSE) = {}"
| "mops_cform (cVAR p) = {}"
| "mops_cform (cDISJ f1 f2) = mops_cform f1 ∪ mops_cform f2"
| "mops_cform (cDIAM m fl) =
{m} ∪ ⋃ (list.set (list.map mops_cform fl))"
Now I tried:
lemma foo:
False
sledgehammer
by (metis cform.distinct(12) cform.distinct(15) cform.distinct(5) cform.simps(24) mops_cform.cases)
Reason: I sorried the functionality proof and the termination proof for mops_cform, so I did not realize that I missed the negation clause for mops. It then gives an induction principle that proves truth from less cases than required, and hence the contradiction.
Last updated: Dec 21 2024 at 16:20 UTC