Consolidate structure

[benkeks]

Combine existing theories and create stubs for upcoming locales and theories.

All theories should be named in Upper_Snake_Case.

Sketch of the structure.

flowchart BT
   Labeled_Transition_Systems.lts_tau -->|sublocale| Labeled_Transition_Systems.lts
   Hennessy_Milner_Logic -->|context| Labeled_Transition_Systems.lts_tau
   Behavioral_Equivalences --> Hennessy_Milner_Logic
   Spectroscopy_Game.spectroscopy_game -->|sublocale| Energy_Games.energy_game
   Spectroscopy_Game.spectroscopy_game -->|sublocale| Labeled_Transition_Systems.lts_tau
   Energy_Games.example_energy_game -->|sublocale| Energy_Games.energy_game
   Spectroscopy_Game/correctness --> Spectroscopy_Game.spectroscopy_game
   Spectroscopy_Game/correctness --> Hennessy_Milner_Logic

[TheHllm]

I think the orientation of the arrows is misleading. For example, lts_tau is a sublocale of lts, not the other way around.

Moreover I believe, that the term sublocale is misleading, as Isabelle has this as a keyword. This keyword does however not do what we would want.

[benkeks]

Arrows like X -sublocale-> Y are meant to be read “X is a sublocale of Y.” You can also read it more technically as “imports” or informally as “builds on” if you like.

In Isabelle, there are two ways of establishing a sublocale relationship: 1. By definition, using +. 2. By proving implication between assumptions, using the sublocale command. Locales created by +-definition are sublocales nonetheless I think. (I might be mistaken, but I don't see why they should be considered as something different. Do you have a reference for this?)

[TheHllm]

I was mistaken. The sublocale keyword does what we want. But then we should use this keyword or change the diagram to match. That is Labeled_Transition_Systems.lts_tau is an extension of Labeled_Transition_Systems.lts, for example denoted by Labeled_Transition_Systems.lts_tau ---locale +---> Labeled_Transition_Systems.lts. And change the code of Spectroscopy_Game.thy to use sublocale (see #59)

[benkeks]

@TheHllm Ah, cool, thanks for looking into it!

Concerning the locale structure, I think, it is conceptionally flawed to use sublocale here, which expresses that LTS can also be understood as one energy game. The reason is that there are multiple energy games that are conceivable on LTSs. In particular, there also would be different spectroscopy games—the paper alone has 2 to 4 of them, depending on how one counts.

For the scope of this class, I think it's right to focus on just the one “full spectroscopy game.” But the code base should be structured in a way, where later projects (e.g. master theses) could easily add other games. For this, the prior approach of having a dedicated locale context for the spectroscopy game is superior.

[benkeks]

I think, this Issue has sufficiently been addressed through the restructurings around energy games, for now.