Stream: Beginner Questions

Topic: Lemmas from a definition by constructors give a contraction


view this post on Zulip Yiming Xu (Oct 19 2024 at 04:01):

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))"

view this post on Zulip Yiming Xu (Oct 19 2024 at 04:06):

Now I tried:
lemma foo:
False
sledgehammer
by (metis cform.distinct(12) cform.distinct(15) cform.distinct(5) cform.simps(24) mops_cform.cases)

view this post on Zulip Yiming Xu (Oct 19 2024 at 04:10):

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