[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Trying to understand lifting in Isabelle/HOL TLA*

Hello,

I'm trying to use TLA*, a generalization of TLA formalized in Isabelle/HOL (https://www.isa-afp.org/entries/TLA.html). The main confusion, I believe, is how to work with the lifted expressions.

In TLAPS, it is clear how to decompose a proof based on the connectives. But it is unclear to me how to approach the same in TLA*. I took the following as a trivial example:

lemma
fixes a and b
assumes a1: "⊢ a"
and a2: "⊢ b"
shows "⊢ a ∧ b"
using a1 a2 by auto

This lemma is proved by auto, but there is no direct rule for that. To understand what's happening here, I tried to decompose the proof into atomic steps:

lemma
fixes a and b
assumes a1: "⊢ a"
and a2: "⊢ b"
shows "⊢ a ∧ b"
proof
fix w
show "w ⊨ a ∧ b"
proof -
have "a w" using a1 by rule
moreover have "b w" using a2 by rule
ultimately have "a w ∧ b w" by rule
hence "(∧) (a w) (b w)" by simp
hence "(lift2 (∧) a b) w" using unl_lift2 by simp
hence "w ⊨ lift2 (∧) a b" by simp
thus "w ⊨ a ∧ b" by simp
qed
qed

Is this reasoning the one (approximately) the auto tactic should be used internally?
I don't know if those steps are atomic. I tried to use rule tactics only but failed to find the actual rules. Maybe it's because a lot is done by macro rewriting. My knowledge here is limited.

Maybe you know of good pointers (apart from the theory document) on how to prove things in this theory? I manage to prove simple invariants with the help of the sledgehammer, but I feel quite lost, only having random events of success.

Karolis

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFteovKyRWofbZ%3DDroh57HC8jDYbw_OSFJKL9EStQ-HOJ4Nseg%40mail.gmail.com.