Hi.
1. The history axiom in State.thy says:
history: "⊢ (I ∧ □[A]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∧ h$=hb]_(h,v))"
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