Treat logical equivalences on hml srbb

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

Treat logical equivalences on hml srbb #70

Closed betawave closed 10 months ago

betawave commented 10 months ago

This PR provides

Regarding HML Formulas:
- Definitions for Implication and Equivalence
- Congruence and Precongruence Properties
- Some Proofs for specific Equivalences and Implications
- Proof for Distinguishing Conjunction Thinning
Regarding HML SRBB Formulas:
- Definitions for Implication and Equivalence
- Some Congruence Properties
- Some Proofs for specific Equivalences and Implications
- Proofs for Distinguishing Conjunction Thinning for all Conjunction Types

betawave commented 10 months ago

I've reworked the statement of all lemmata to explicitly mention the assumptions and conclusions for simpler parsing.

betawave commented 10 months ago

I'm fine with the important proofs, and think that we could merge. Our rule was that another person from the team (not @benkeks, in this case @ekeln) must give the green light before merging. Tbh, I'm unsure if a 1.8k line prove review that inspects the contents, not only the form is "zumutbar"... I'm very sorry that this sprawled so much :(

betawave commented 10 months ago

I've removed all greek letter suffixes I could find and have moved the naming from conjuction to inner. The only remaining topic is the renaming of dist and distFrom in HML.thy, then I believe this is ready for merging.

betawave commented 10 months ago

I've aligned the naming of distinguishes and distinguishes_from predicates in HML.thy and HML_SRBB.thy. Given this, and our discussions in the team meeting I'll now merge this.