A structure preserving encoding of Z in isabelle/HOL

摘要: We present a semantic representation of the core concepts specification language Z in higher-order logic. Although it is “shallow embedding” like one presented by Bowen and Gordon, our preserves structure avoids expanding schemas. The implemented logic instance generic theorem prover Isabelle. Its parser can convert concrete syntax schemas into their thus spare users from having to deal with explicitly. Our essentially conforms latest draft standard may give both clearer understanding inspire development proof calculi for Z.