search

equivio / silent-step-spectroscopy

Isabelle formalization of linear-time–branching-time spectroscopy accounting for silent steps
https://equivio.github.io/silent-step-spectroscopy/AFP/LinearTimeBranchingTimeSpectroscopyAccountingForSilentSteps/index.html
Other
0 stars 0 forks source link

Unify semantics #171

Closed benkeks closed 5 months ago

benkeks commented 6 months ago

The purpose of this PR is to use one set of definitions of equivalence, distinction etc. for all semantics functions. To this end, a new locale lts_semantics is introduced and used. The simplifier is set up so that a lot of proofs become shorter.

Also, the PR drops the “bonus” theories HML_Context and LTS_Prime. (In order to reduce the burden of maintaining unused lemmas and proofs.)