Theory EgHighBranchRevC
theory EgHighBranchRevC
imports Dependent_SIFUM_Type_Systems.Compositionality
Dependent_SIFUM_Type_Systems.Language
"HOL-Eisbach.Eisbach_Tools"
"../CompositionalRefinement"
begin
text ‹
Theory for exploring refinement of a program that branches on a high variable.
The purpose of this particular example is to demonstrate that in order to prove any branching
on a High-classified variable remains safe when refined to a concrete implementation, it is
necessary to ensure that the two concrete branches of execution take the same number of steps,
possibly by skip-padding the one with less steps in it, and provide an appropriate coupling
invariant to link the corresponding concrete steps of the two branches of the if-statement.
›
type_synonym 'var addr = 'var
type_synonym val = nat
type_synonym 'var mem = "'var addr ⇒ val"