Stream: Beginner Questions

Topic: "iff" definitions with meta-equations?

Yiming Xu (Sep 12 2024 at 09:25):

I tried to write:

fun propform :: "form ⇒ bool"
  where
   "propform FALSE ≡ True"
 | "propform (VAR p) ≡ True"
 | "propform (DISJ f1 f2) ≡ (propform f1 ∧ propform f2)"
 | "propform (NOT f) ≡ propform f"
 | "propform (DIAM f) ≡ False"

And Isabelle complains. Since I have been suggested to use meta-stuff for definitions once possible, here I am attempting to define a predicate "is propositional formula" using meta-equation instead of <-->.

The error message is "Not an equation" and a colleague found out that it comes from the function package, which calls "dest_eq" in HOL level.

Therefore, the complain is because it expects HOL level equation only, not a meta one.

Yiming Xu (Sep 12 2024 at 09:26):

Therefore, what to use if I want to make the definition using meta-equality <\equiv>?

Yiming Xu (Sep 12 2024 at 09:26):

Or if there is any argument that "in such a case, it is better to using fun and HOL equality", then I am also happy to just stick with it.

Lukas Stevens (Sep 12 2024 at 09:30):

The function package expects you to use the HOL equality (=).

Lukas Stevens (Sep 12 2024 at 09:30):

You can, however, turn a HOL equality into a meta-equality with the theorem HOL.eq_reflection.

Yiming Xu (Sep 12 2024 at 09:36):

That makes sense. Thank you!

Yiming Xu (Sep 12 2024 at 09:37):

I expect the simplifier works a bit differently if it see a definition using HOL or meta equality.

Last updated: Dec 21 2024 at 16:20 UTC