Yiming Xu (Sep 29 2024 at 04:16): Yiming Xu (Sep 29 2024 at 04:16):As an abridged version:
My original goal looks like (A /\ B ==> C). Such a subgoal is generated by a proof method application. I want to refer to "A" and "B" separately, so I typed:
assume "A /\ B" show "C" proof (elim conjI)
The goal turns to "A ==>B ==> C", as I expected.
However, I then typed "from B obtain ..."
Isabelle complains and gives me: "Failed to retrieve literal fact: B"
Why is that?
Concrete version of the problem:
My goal originally looks like this:
goal (1 subgoal):
1. w ∈ elts (world M) ∧
(∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl) ⟹
∃vl. rel Mf m (sEqc M Σ w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate Mf) (valt Mf) v
f)
fl)
vl
I typed:
assume a: "w ∈ elts (world M) ∧
(∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl)"
then show "∃vl. rel Mf m (sEqc M Σ w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate Mf) (valt Mf) v
f)
fl)
vl"
proof (elim conjE)
to turn it into:
w ∈ elts (world M) ⟹
∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl ⟹
∃vl. rel Mf m (sEqc M Σ w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate Mf) (valt Mf) v
f)
fl)
vl
I hope I can then refer to "w ∈ elts (world M) " and "∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl " separately.
However, after the "proof (elim conjE)", when I type:
from ‹ (∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl)›
obtain vl
where "rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl"
it complains:
Failed to retrieve literal fact⌂:
∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f) fl)
vl
How can I split and refer to the long conjunct separately?
Mathias Fleury (Sep 29 2024 at 06:39):You need to assume it
Mathias Fleury (Sep 29 2024 at 06:40):When you type B it is looking at a fact in the Isar proof. This is the entire point of Isar: the proof text is sufficient
Mathias Fleury (Sep 29 2024 at 06:40):and only show and qed look at the concrete proof goal
Yiming Xu (Sep 29 2024 at 07:16):I see, thanks! I forgot (again) that assume is for and only for the things that are generated during the proof.
Mathias Fleury (Sep 29 2024 at 07:28):BTW you can also decompose the assumptions directly with
assume "A /\ B"
then have A and B
by fast+
avoiding a nesting of proof (and hence indentation and so on)
Mathias Fleury (Sep 29 2024 at 07:31):Or the version with term naming to avoid repeating terms:
assume "A /\ B" (is "?w_in_word /\ ?succs")
then have ?w_in_word and ?succs
by fast+
As usual in naming during programming: ?A is a cool name for examples, but not a good one for proof maintainability.
Yiming Xu (Sep 29 2024 at 07:34):Sorry, what does the name with "?" break for sack of maintainability?
Mathias Fleury (Sep 29 2024 at 07:43):I do not manage to come up with a good example, but if you use ?A and by accident it starts referring to another term, it is much harder to remember what it should point to
Mathias Fleury (Sep 29 2024 at 07:48):In your example you have two assumptions:w ∈ elts (world M) and
∃vl. rel M m (w # vl) ∧
Truel
(map (λf v. adSts (Gframe.truncate M) (valt M) v f)
fl)
vl . Which one is more naturally an ?A and which one a ?B?
Yiming Xu (Sep 29 2024 at 07:53):I think I will just call the first conjunct ?A and the second conjunct ?B, so in my case ?A is w ∈ elts (world M) and ∃vl. rel M m (w # vl) ∧ Truel (map (λf v. adSts (Gframe.truncate M) (valt M) v f) fl) vl is ?B.
Yiming Xu (Sep 29 2024 at 07:55):I think one possible thing to do is not to use sth like "A" but a longer thing to keep all of them distinguished. Say, call the first one ?w_wd and the second one ?exvl.
Last updated: Dec 21 2024 at 16:20 UTC