I am trying to formalize business rules in Isabelle/HOL, but business rules involve the change of the values of some variables, like if x=5 => x=6. => is not the usual implication there, because x is 5 in one world (interpretation, semantic domain) and after the execution of the rule the x is 6 and it is already a different world (different interpretation, assignment function, semantic domain). So - technically is x=5 => x=6 is not the formula in First Order Logic and it is not also the formula of Higher Order Logic of Isabelle/HOL. More possible is that it is the formula in dynamic/action logic [rule1](x=5)=(x=6) (that defines that upon application of rule1 to the formula in some world yields to the truthful formula in some other world (dynamic/action logic is essentially a kind of modal logic and Kripke/possible world semantics can be applied here).
Now, back to Isabelle/HOL or Coq: FOL/HOL theory is set of formulas in all the worlds or in one particular world. If we stay at FOL/HOL then there is no change of the world, no change of the values of the variables. We should go to the modal logics if we would like to model, reasong about such changes. But can it be done in HOL? This change of world?
http://matryoshka.gforge.inria.fr/pubs/fernandez_burgos_bsc_thesis.pdf is good work about formalization of sorting algorithms in Isabelle/HOL, functional programming is used there and there is no need of variables and hence - no this change among worlds. But if we try to model Reinforcement Learning, Markov processes, impertative/object oriented programming, business rules in Isabelle/HOL, then we should express this change. How to do that?
How to express business rule if x=5 => x=6 in Isabelle/HOL?
The same approach can be used in Coq, that is why answers from the Coq community are welcome as well.
The most common solution is using a predicate of type world => world => bool representing transitions between worlds or states (for Markov processes) or memory (for program verification). It represents a transition from one place to another.
Such a predicate can typically be defined as an inductive predicate to represent non-determinism.
If you are specifically interested in logic:
For Isabelle, you could have a look at how it is done in the formalisation of dynamic logic and of modal logic in the AFP (https://www.isa-afp.org/topics.html -- search for Modal logic: on that page).
For Coq, I have found this approach, which follows the same pattern, but there many other formalisations.