Yiming Xu (Sep 14 2024 at 08:31): Yiming Xu (Sep 14 2024 at 08:31):definition is_NML_def :
"is_NML s ≡
(⋀ A B p q f form.
ptaut form ⟶ form ∈ s ∧
(IMP (BOX (IMP p q)) (IMP (BOX p) (BOX q))) ∈ s ∧
(IMP (DIAM p) (NOT (BOX (NOT p)))) ∈ s ∧
(IMP (NOT (BOX (NOT p))) (DIAM p)) ∈ s ∧
(A ∈ s ⟶ (subst f A) ∈ s) ∧
(A ∈ s ⟶ (BOX A) ∈ s) ∧
((IMP A B) ∈ s ∧ A ∈ s ⟶ B ∈ s))"
definition NMLG_def:
"NMLG Γ ≡ ⋂ {A | is_NML A ∧ Γ subset A}"
definition NMLG_def is not accepted, with the following error message:
image.png
Yiming Xu (Sep 14 2024 at 08:33):It infers the type of A to be bool. Why it is doing that and how can I avoid it?
Yiming Xu (Sep 14 2024 at 08:33):I checked subset predicate takes two sets.
Yiming Xu (Sep 14 2024 at 08:33):And is_NML takes a term of type form => set.
Mathias Fleury (Sep 14 2024 at 08:39):None of the things are writing type in a meaningful way
is_NML A ∧ Γ subset A is not a bool{A | P (is_NML A)} is not a _ set set as required by ⋂Γ subset A does not mean what you think it does and Γ does not appear anywhere else Mathias Fleury (Sep 14 2024 at 08:41):So I suggest looking at other examples (find_theorems "‹{_| _. _}› " and ‹{_. _}› ) to see how it is supposed to be used
Yiming Xu (Sep 14 2024 at 08:41):P (is_NML A) seems to make the wrong sense. is_NML A should be of type bool. Here it should be P A.
Mathias Fleury (Sep 14 2024 at 08:42):I put P because all the stuff after | does not make sense and I have no clue what you intended to write
Yiming Xu (Sep 14 2024 at 08:43):Mathias Fleury said:
So I suggest looking at other examples (
find_theorems "‹{_| _. _}› "and‹{_. _}›) to see how it is supposed to be used
Let me try and see, maybe I should use schematic variables somewhere.
Yiming Xu (Sep 14 2024 at 08:49):I intend to write a set comprehension to define "NMLG Gamma" to be "the modal logic generated by Gamma". So both Gamma and "NMLG Gamma" should be of type "form set".
Yiming Xu (Sep 14 2024 at 08:49):I think I understand the following error message: It complains is_NML s is a prop, not bool.
Yiming Xu (Sep 14 2024 at 08:50):This is because I wrote meta-equality for defining it. Maybe it is not a good idea if I want to use it in a comprehension later... Let me try to edit it into HOL equality...
Mathias Fleury (Sep 14 2024 at 08:51):No isabelle has infered types, concluded that A must be of type bool and then complains that A cannot be an argument of is_NML
Mathias Fleury (Sep 14 2024 at 08:51):Sometimes (like here) the types are so completely messed up, that the error message is not helping you at all
Yiming Xu (Sep 14 2024 at 08:51):
Yiming Xu (Sep 14 2024 at 08:52):Oh I forgot the screenshot.
Mathias Fleury (Sep 14 2024 at 08:52):Okay then you are right.
Mathias Fleury (Sep 14 2024 at 08:52):Remark that \Gamma appears only in the condition (and is not a set)
Yiming Xu (Sep 14 2024 at 08:53):Ah? Why Gamma is not a set? It is a form set.
Yiming Xu (Sep 14 2024 at 08:54):Yiming Xu said:
Ah? Why Gamma is not a set? It should be a form set.
Yiming Xu (Sep 14 2024 at 08:55):And okay it is indeed because it does not like the prop. Now it works.
image.png
Yiming Xu (Sep 16 2024 at 08:08):Mathias Fleury said:
Remark that \Gamma appears only in the condition (and is not a set)
So you mean \Gamma does not appear on the RHS of the definition? Maybe that is correct, because I just found that my definition of NMLG is wrong.
image.png
Yiming Xu (Sep 16 2024 at 08:10):I would like it to be form set => form set! Maybe it is because it does not think the Gamma on the LHS and RHS are the same. HOL4 has the same problem, and can be resolved by adding some bars in the comprehension.
Yiming Xu (Sep 16 2024 at 08:11):Any clue on how should I deal with that?
Yiming Xu (Sep 16 2024 at 08:12):Oh maybe I know. The definition of subset.
Yiming Xu (Sep 16 2024 at 08:13):
Yiming Xu (Sep 16 2024 at 08:13):Fixed. My stupid.
Last updated: Dec 21 2024 at 16:20 UTC