Adrián Doña Mateo (Jul 28 2022 at 08:50): Adrián Doña Mateo (Jul 28 2022 at 08:50):Hi, how do I properly use a case a of b statement given as an assumption in the proof state? Here is the example I am having trouble with:
lemma assumes "seq (Suc m) (Suc n) (Node ts) (Node us)"
shows "∀(t, u) ∈ set (zip ts us). seq m n t u"
proof
fix p assume "p ∈ set (zip ts us)" (*something to deal with "case p of (t, u)" here*)
then show "seq m n (fst p) (snd p)"
qed
Inside the proof..qed block, the proof state is:
⋀x. x ∈ set (zip ts us) ⟹
case x of
(t, u) ⇒ seq m n t u
Hi Adrián, in this particular case you can consider using fst and snd to extract elements from a pair. For example, if you can show have "seq m n (fst x) (snd x)" if "x ∈ set (zip ts us)" for x then your target should follow:
notepad
begin
have "seq m n (fst x) (snd x)" if "x ∈ set (zip ts us)" for x
sorry
then have "⋀x. x ∈ set (zip ts us) ⟹
case x of
(t, u) ⇒ seq m n t u"
by auto
end
Last updated: Apr 26 2024 at 08:19 UTC