[tlaplus] On the axiomatization of state in Isabelle

[Abhishek Singh <abhishek1729@xxxxxxxxx>]

Hi.

I have a few questions about the Isabelle AFP on TLA (https://www.isa-afp.org/entries/TLA.html). If this is not the right forum to ask questions about this, please redirect me to the correct forum.

1. The history axiom in State.thy says:

history: "⊢ (I ∧ □[A]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∧ h$=hb]_(h,v))"

but this does not allow me to replace sub-actions that are more nested, as described in Th. 1 (http://lamport.azurewebsites.net/tla/auxiliary/auxiliary.html). Is it advisable to add more history axioms? e.g.

history2: "⊢ (I ∧ □[A ∨ (∃i. P i)]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∨ (∃i. P i ∧ h$=hc i)]_(h,v))"

2. Unlike history variables one-prediction prophecy variables seem to require appending either PredA(p)∧(p′ ∈Π) or (p′=p) to all sub-actions (from equations 4.4 and 4.5 in http://lamport.azurewebsites.net/tla/auxiliary/auxiliary.html) but this requirement is harder to state as an axiom. Is it possible to support prophecy variables axiomatically in the AFP? (My requirement is most likely satisfied by prophecy data structure variables.)

3. The eexE axiom says:

eexE: "⟦s ⊨ (∃∃ x. F x) ; basevars vs; (⋀ x. ⟦ basevars (x,vs); s ⊨ F x ⟧ ⟹ s ⊨ G)⟧ ⟹ (s ⊨ G)"

but basevars and vs do not seem to interact with formulas F and G; would the following simpler axiom be unsound?

eexE: "⟦s ⊨ (∃∃ x. F x); (⋀ x. s ⊨ F x ⟹ s ⊨ G)⟧ ⟹  (s ⊨ G)"

Further information: The reason for my interest in the Isabelle AFP is that I need to prove a property of the form

          "s ⊨ ∀∀ x. P x ⟶ □Q x ⟹ s ⊨ ∀∀ y. R y ⟶ □S y"

i.e. the system R is safe (S) if the system P is safe (Q) where the rigid variables in P and R satisfy some relationship. Equivalently, I need to show

           "s ⊨ ∃∃y. R y ∧ ◇¬S y ⟹ s ⊨ ∃∃ x. P x ∧ ◇¬Q x"

but this is not a standard TLA+ specification, and I felt that the Isabelle AFP might be a better system to try to formalize the proof of the above property than say TLAPS.

Any help is appreciated.

-Abhishek

-- 
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/614e6577-d96d-4db5-b950-47d651f53331n%40googlegroups.com.