| Hi Karolis, as you certainly noticed, the embedding that you refer to is completely unrelated to TLAPS. It aims at a representation of TLA (not TLA+) in Isabelle, with higher-order logic as the underlying data language. [1] The idea is to have formulas that are interpreted over "possible worlds" as in modal logic, where worlds can be states, pairs of states or behaviors for TLA. For example, a temporal formula is represented as a function of type behavior => bool, where behavior is an infinite sequence of states. This representation is set up generically in theory Intensional [2] that attempts to introduce a syntax for expressions that hides their functional nature in many contexts, similar to the syntax used in modal logic. For example, "w |= A" is really just fancy syntax for "A w", and you can use both interchangeably, and "|- A" is a shorthand for "∀w. w |= A". Similarly, standard HOL operators can be lifted to corresponding operators over modal expressions, thus "lift2 (∧)" denotes conjunction of modal formulas and has type "('w => bool) => ('w => bool) => ('w => bool)" for some type 'w of "worlds" whereas standard conjunction is of type "bool => bool => bool". Some trickery with the Isabelle parser allows the lifting functions to be hidden in modal contexts, for example "(lift2 (∧) a b) w" can be written "w |= a ∧ b". Finally, rewrite rules for distributing lifting functions over expressions are included in the standard simplification rules applied by Isabelle, for example in order to reduce "w |= a ∧ b" to "(w |= a) ∧ (w |= b)" where the conjunction in the latter is standard (unlifted) conjunction from HOL. As you discovered, reasoning in this framework using elementary rule applications becomes tedious because rewriting needs to be applied throughout to simplify formulas. The intent was to make it possible for the user to state suitable intermediate assertions, then apply auto or simp to automate the steps that relate those assertions. The two examples provided in the AFP [3] illustrate how the embedding in Isabelle can be used, but I don't think anybody else used the theories. Since that encoding was made before the sledgehammer tool existed, I have no idea to what extent sledgehammer is useful in this context. Personally, I would recommend using TLAPS rather than that encoding of TLA in Isabelle/HOL. Best, Stephan [1] TLAPS also includes an Isabelle backend, but that backend is based on an object logic different from HOL for representing TLA+ set theory, i.e. the constant level of TLA+. TLA* formalizes state-, action-, and temporal-level reasoning.
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/AB67F8B9-2047-4CF6-AC37-A2DFFBA3B2DB%40gmail.com. |