Stream: Beginner Questions

Topic: Why Pure.conjunctionI is an "ill-formed introduction rule"?

Qiyuan Xu (Jun 15 2021 at 07:55):

This Isar code triggers an error "Ill-formed introduction rule",

declare Pure.conjunctionI[intro]

where the Pure.conjunctionI is PROP ?A ⟹ PROP ?B ⟹ PROP ?A &&& PROP ?B
Why? Isn't it an introduction rule??

The same problem is actually hindering me. I have defined a constant for certain purpose, let's say MyConj :: prop => prop => prop where MyConj = (&&&) , and the same error "Ill-formed introduction rule" occurs when I'm trying to declare the introduction rule for it, that PROP P ⟹ PROP Q ⟹ PROP MyConj (RPOP P) (PROP Q).

Mathias Fleury (Jun 15 2021 at 07:57):

why don't you use standard HOL conjunction instead of Pure conjuction?

Mathias Fleury (Jun 15 2021 at 08:00):

Anyway given that intro is defined in HOL.thy, I don't expect it to work on &&&…

Qiyuan Xu (Jun 15 2021 at 08:09):

Mathias Fleury said:

why don't you use standard HOL conjunction instead of Pure conjuction?

for some purpose it's better to be defined in the meta logic (the Pure logic) I think. Let's just talk about the situation for &&&, and it's interesting and unexpected, right?

Mathias Fleury (Jun 15 2021 at 08:13):

Interesting? Maybe.
Unexpected? Not really, since intro is HOL specific…

Qiyuan Xu (Jun 15 2021 at 08:14):

Mathias Fleury said:

Anyway given that intro is defined in HOL.thy, I don't expect it to work on &&&…

The intro attribute is defined in src/Provers/classical.ML... Is it really restricted to HOL?

Mathias Fleury (Jun 15 2021 at 08:19):

$ grep -r "classical.ML" *
src/HOL/HOL.thy:ML_file \<open>~~/src/Provers/classical.ML\<close>
src/FOL/FOL.thy:ML_file \<open>~~/src/Provers/classical.ML\<close>

Mathias Fleury (Jun 15 2021 at 08:20):

so not limited to HOL, but only used in _instantiations_ not in Pure

Qiyuan Xu (Jun 15 2021 at 08:20):

Okay... fine

Last updated: Dec 21 2024 at 16:20 UTC