Adapt the Ouroboros Praos implementation to Isabelle2022

[javierdiaz72]

This resolves #20.

[jeltsch]

It seems a bit strange to me that such changes should be necessary. In the past, I had an experience where many of my simplifier invocations broke after an Isabelle update. The problem was, if I remember correctly, that the most fundamental theory of my development (probably Transition_Systems-Foundations) imported Eisbach before Main. This can lead to problems with configurations, like the one of the simplifier. As you perhaps know, some things in Isabelle are designed with linear processing of code in mind, which creates issues when a theory imports several other theories: in particular, configurations have to be merged and in some cases this leads to suboptimal results.

The bottom line back then was that you should never import certain low-level theories of Isabelle/HOL without having imported Main first: Main is the official entry point for any Isabelle/HOL development. If you don’t respect this rule, you might face breakage in some versions in Isabelle, which you might not see in others. I’m not completely sure about the details, though; I guess the rule is that all theories of the HOL session that come before Main as well as some other sessions like Eisbach shouldn’t be imported directly, while you can rely on the HOL sessions that come after Main and the sessions of, for example, HOL-Library taking care to import Main first.

The theory Ouroboros_Praos_Implementation doesn’t explicitly import Main. I checked the chain of theories imported first and found that it is Ouroboros_Praos_Implementation → Finite_Map_Extras → Finite_Map → FSet → Main; so Main actually is imported first (except if you have a different local version of Finite_Map_Extras perhaps; I’m a bit puzzled about you being able to import it without qualifying with a session name). Therefore, it seems that not importing Main first isn’t the problem here.

[jeltsch]

At the moment, the theory Ouroboros_Praos_Implementation is not mentioned in the ROOT file. If I add it and run make qnd afterwards, I get the following error messages:

*** Cannot load theory file "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Finite_Map_Extras.thy"
*** The error(s) above occurred for theory "Ouroboros.Finite_Map_Extras"
*** (required by "Ouroboros.Ouroboros_Praos_Implementation") (line 5 of "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Ouroboros_Praos_Implementation.thy")
*** Cannot load theory "HOL-Library.BNF_Corec"
*** The error(s) above occurred for theory "HOL-Library.BNF_Corec"
*** (required by "Ouroboros.Ouroboros_Praos_Implementation") (line 6 of "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Ouroboros_Praos_Implementation.thy")
*** Cannot load theory "HOL-Library.Sublist"
*** The error(s) above occurred for theory "HOL-Library.Sublist"
*** (required by "Ouroboros.Ouroboros_Praos_Implementation") (line 7 of "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Ouroboros_Praos_Implementation.thy")
*** Cannot load theory "Chi_Calculus.Typed_Basic_Transition_System"
*** The error(s) above occurred for theory "Chi_Calculus.Typed_Basic_Transition_System"
*** (required by "Ouroboros.Ouroboros_Praos_Implementation") (line 8 of "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Ouroboros_Praos_Implementation.thy")
*** Cannot load theory file "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Finite_Map_Extras.thy"
*** Bad import of theory "HOL-Library.BNF_Corec": need to include sessions "HOL-Library" in ROOT
*** Bad import of theory "HOL-Library.Sublist": need to include sessions "HOL-Library" in ROOT
*** Bad import of theory "Chi_Calculus.Typed_Basic_Transition_System": need to include sessions "Chi_Calculus" in ROOT
*** No such file: "/home/wolfgang/Dokumente/Beruf/IOG/ouroboros-high-assurance/src/Finite_Map_Extras.thy"
*** No such file: "HOL-Library.BNF_Corec"
*** No such file: "HOL-Library.Sublist"
*** No such file: "Chi_Calculus.Typed_Basic_Transition_System"

I guess this has partly to do with lack of porting to the Þ-calculus and partly with some more additions to the ROOT file missing. I’ll accept this pull request nevertheless, but we must fix these issues.