Stream: Beginner Questions

Topic: Why is this syntax error have ... by have ...by

Yiming Xu (Sep 17 2024 at 07:20):

image.png

Yiming Xu (Sep 17 2024 at 07:21):

I believe the first "show" is already killed by the "by". Why it is still complaining.

Yiming Xu (Sep 17 2024 at 07:22):

If the above is problematic, why is this case fine?
image.png

Yiming Xu (Sep 17 2024 at 09:15):

The error goes away if I replace the second "show" with "have". Does it indicate the first "show" is not finished?

Yiming Xu (Sep 17 2024 at 09:15):

image.png

Yiming Xu (Sep 17 2024 at 09:17):

I see. It is unhappy with the fact that I only quantify over p and q.

Yiming Xu (Sep 17 2024 at 09:18):

It wants me to write

(⋀A B p q f form. BOX (p → q) → (BOX p → BOX q) ∈ P)

Even if only p and q actually appears.

Yiming Xu (Sep 17 2024 at 09:31):

Another question: Can we name subgoals? Are they referred as something like ?thesis by default? (If no, then I can understand, because the order of generated subgoals can be easily broken, nevertheless, can we say something like
show "a pattern matching a generated subgoal" by ...
instad?
)

Yiming Xu (Sep 17 2024 at 09:32):

They are so long to copy and past. I do not quite want to write like this in long term:

show "⋀A B p q f form. ptaut form ⟹ form ∈ P" using "1" by blast
    show "(⋀A B p q f form. BOX (p → q) → (BOX p → BOX q) ∈ P)"  using "2" by blast
    show "⋀A B p q f form. A ∈ P ⟹ subst f A ∈ P" using "s" by blast
    show "⋀A B p q f form. DIAM p → NOT (BOX (NOT p)) ∈ P" using 3 by blast
    show "⋀A B p q f form. NOT (BOX (NOT p)) → DIAM p ∈ P" using s1 by blast
    show " ⋀A B p q f form. A ∈ P ⟹ BOX A ∈ P" using 4 by blast
    show "⋀A B p q f form. A → B ∈ P ⟹ A ∈ P ⟹ B ∈ P " using 5 by blast

Yiming Xu (Sep 17 2024 at 10:07):

And why is this complaining?
image.png

Yiming Xu (Sep 17 2024 at 10:08):

I have just learnt a few days ago that meta-connectives are right assoc, so I think even with out the "()", the following should parse.

⋀p2. KGproof Γ p2 ⟹ ⋀p1. KGproof Γ p1 ⟹ KGproof Γ (p1 @ p2)

Yiming Xu (Sep 17 2024 at 10:08):

It is happy if I write:

⋀p2. KGproof Γ p2 ⟹ (⋀p1. (KGproof Γ p1 ⟹ KGproof Γ (p1 @ p2)))

though.

Yiming Xu (Sep 17 2024 at 11:34):

Another question: what to write between a "proof" and "qed" to skip a proof? I know there are sorry and oops. But I want something to be filled between proof and qed so I do not need to comment out a block of partial proof.

My life will also be better if there is a key-binding for both comment and undo the comment.

Yiming Xu (Sep 17 2024 at 11:40):

Yiming Xu said:

Another question: what to write between a "proof" and "qed" to skip a proof? I know there are sorry and oops. But I want something to be filled between proof and qed so I do not need to comment out a block of partial proof.

My life will also be better if there is a key-binding for both comment and undo the comment.

I am aware of this post. https://stackoverflow.com/questions/65711558/how-to-abort-a-proof-in-isabelle but this does not solve my problem.

Last updated: Dec 21 2024 at 16:20 UTC