lib: README.md files for the new sessions

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Basics/README.md

@@ -0,0 +1,16 @@
+<!--
+  Copyright 2023, Proofcraft Pty Ltd
+  SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# Basic Library Theories
+
+This session contains basic library theories that are needed in other sessions
+of this repository, such as [Monads] or [CParser], but that we do not want to
+put into these sessions to avoid circular session dependencies.
+
+Dependencies on `Word_Lib` and the Isabelle distribution (e.g. `HOL-Libary`) are
+fine, but avoid introducing any further session dependencies.
+
+[Monads]: ../Monads/
+[CParser]: ../../tools/c-parser

lib/Eisbach_Tools/README.md

@@ -0,0 +1,19 @@
+<!--
+  Copyright 2023, Proofcraft Pty Ltd
+  SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# Eisbach and Tactic Tools
+
+This session contains tools and tactics for defining Isabelle [Eisbach] methods.
+
+Some of the theories in this session are not strictly speaking Eisbach-related,
+but are mostly used from Eisbach methods, so we collect them here as well.
+
+We only include theories that are needed in the [Monads], [CParser], and
+[AutoCorres] sessions.
+
+[Eisbach]: https://isabelle.in.tum.de/dist//doc/eisbach.pdf
+[Monads]: ../Monads/
+[CParser]: ../../tools/c-parser/
+[AutoCorres]: ../../tools/autocorres/

lib/ML_Utils/README.md

@@ -0,0 +1,15 @@
+<!--
+  Copyright 2023, Proofcraft Pty Ltd
+  SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# Isabelle/ML Utilities
+
+`ML_Utils` is a collection of 'basic' ML utilities (similar to
+`~~/src/Pure/library.ML`}). If you find yourself implementing:
+
+- a simple data-structure-shuffling task,
+- something that shows up in the standard library of other functional languages, or
+- something that's "missing" from the general pattern of an Isabelle ML library,
+
+consider adding it here.

lib/Monads/README.md

@@ -0,0 +1,38 @@
+<!--
+  Copyright 2023, Proofcraft Pty Ltd
+  SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# Monad Definitions and Tactics
+
+This session contains definitions of various monads useful in [AutoCorres] and
+the [seL4 verification][l4v] for the verification of C programs.
+
+In particular, this session defines:
+
+- a [nondeterministic state monad][nondet] with failure to express stateful
+  computation. There is a variation of this monad that also allows computation
+  with exceptions (throw/catch).
+
+- a [reader option monad][option] to express computation that can depend on
+  state and can fail, but does not change state. It can also be used to express
+  projections from the state in preconditions and other state assertions.
+
+- a [trace monad][trace] that stores a set of traces for expressing concurrent
+  computation.
+
+- for each of these monads, weakest-precondition lemmas and corresponding tool
+  setup.
+
+- for the nondeterministic state monad, additional concepts such as
+  wellformedness with respect to failure (`empty_fail`), absence of failure
+  (`no_fail`), absence of exceptions (`no_throw`). See the respective theories
+  for more details.
+
+The directory [`wp/`](./wp/) contains proof methods to reason about these monads
+in weakest-precondition style.
+
+[l4v]: https://github.com/seL4/l4v/
+[nondet]: ./NonDetMonad.thy
+[option]: ./OptionMonad.thy
+[trace]: ./TraceMonad.thy