src/HOL/TLA/README.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/README.thy	Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,48 @@
+theory README imports Main
+begin
+
+section \<open>TLA: Lamport's Temporal Logic of Actions\<close>
+
+text \<open>
+  TLA \<^url>\<open>http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html\<close>
+  is a linear-time temporal logic introduced by Leslie Lamport in \<^emph>\<open>The
+  Temporal Logic of Actions\<close> (ACM TOPLAS 16(3), 1994, 872-923). Unlike other
+  temporal logics, both systems and properties are represented as logical
+  formulas, and logical connectives such as implication, conjunction, and
+  existential quantification represent structural relations such as
+  refinement, parallel composition, and hiding. TLA has been applied to
+  numerous case studies.
+
+  This directory formalizes TLA in Isabelle/HOL, as follows:
+
+    \<^item> \<^file>\<open>Intensional.thy\<close> prepares the ground by introducing basic syntax for
+      "lifted", possible-world based logics.
+
+    \<^item> \<^file>\<open>Stfun.thy\<close> and \<^file>\<open>Action.thy\<close> represent the state and transition
+      level formulas of TLA, evaluated over single states and pairs of states.
+
+    \<^item> \<^file>\<open>Init.thy\<close> introduces temporal logic and defines conversion functions
+      from nontemporal to temporal formulas.
+
+    \<^item> \<^file>\<open>TLA.thy\<close> axiomatizes proper temporal logic.
+
+
+  Please consult the \<^emph>\<open>design notes\<close>
+  \<^url>\<open>http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps\<close>
+  for further information regarding the setup and use of this encoding of TLA.
+
+  The theories are accompanied by a small number of examples:
+
+    \<^item> \<^dir>\<open>Inc\<close>: Lamport's \<^emph>\<open>increment\<close> example, a standard TLA benchmark,
+      illustrates an elementary TLA proof.
+
+    \<^item> \<^dir>\<open>Buffer\<close>: a proof that two buffers in a row implement a single buffer,
+      uses a simple refinement mapping.
+
+    \<^item> \<^dir>\<open>Memory\<close>: a verification of (the untimed part of) Broy and Lamport's
+    \<^emph>\<open>RPC-Memory\<close> case study, more fully explained in LNCS 1169 (the \<^emph>\<open>TLA
+    solution\<close> is available separately from
+    \<^url>\<open>http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html\<close>).
+\<close>
+
+end