first, a disclaimer: the Isabelle theories that you mention are unrelated to TLAPS (as you say) and even TLA+, and as such are probably irrelevant to the audience of the mailing list. I'll answer your questions but suggest that we take any follow-up discussion offline in order to avoid confusion.
Also, as far as I know these Isabelle theories have not been used for any serious verification attempt. In particular, the part about quantification over state variables that you refer to is really experimental, and I expect changes to be necessary.--
I would expect that you'd rather like to have
⊢ (I ∧ □[A ∨ (∃i. P i)]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[(A /\ h$ = $h) ∨ (∃i. P i ∧ h$=hc i)]_(h,v))
so that h is not left unconstrained for A action. Can't you get this from the above by instantiating hb by something along the lines of
if A then $h else (CHOOSE i : P i /\ hc i)
Not having had any significant experience with prophecy variables, I didn't dare write an axiom for them in Isabelle. You'll want to experiment to see what works for you.
This is sound but weaker. The "basevars" predicate is a hack in order to distinguish state variables from other state functions. The predicate is used for reasoning about ENABLED, and the above axiom allows you to treat the bound variable x as any other state variable in that context.
Indeed, if you need history or prophecy variables in these reductions, TLAPS won't be able to help you at this point. If the relationship between the variables can be expressed as a refinement mapping, you can instantiate the specification of R in the module that defines system P.
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/A26534F8-A203-4FC1-9A64-FE827155F010%40gmail.com.