(*-----------------------------------------------*
            |                                               |
            |    The Dining Mathematicians in CSP-Prover    |
            |                                               |
            |                  June 2004                    |
            |              December 2004 (modified)         |
            |              November 2005 (modified)         |
            |                  July 2009 (modified)         |
            |                                               |
            |         Yoshinao Isobe    (AIST, Japan)       |
            |         Markus Roggenbach (UWS, UK)           |
            |                                               |
            *-----------------------------------------------*)

1 Introduction 

These 5 theory files (DM1_Sys_def.thy - DM5_Spc_Seq.thy) verify that
(Imp n) refines Spc (i.e. Spc <=F (Imp n)). (Imp n) expresses a
concurrent behavior between two mathematicians and a shared variable,
where n is the initial value of the shared variable. On the other
hand, Spc requires that the mathematicians exclusively eat and they
have no deadlock. Please also see the following URL:

  http://staff.aist.go.jp/y-isobe/CSP-Prover/ex_dm/dining_mathematicians.html

2 Theory files

  DM1_Imp_def.thy  : defines Imp
  DM2_para.thy     : expands parallel operators in Imp
  DM3_hide.thy     : expands hiding operators in Imp
  DM4_Spc_def.thy  : defines Spc
  DM5_Spc_Imp.thy  : proves Spc <=F Imp


3 How to use these theory files

(1) Execute Proof General (2005) as follows:

       Isabelle -l CSP_F

    (the heap for CSP_F should be built before)

(2) Load the theory file "DM5_Spc_Imp.thy" by C-x C-f.

(3) Prove the lemmas by C-c C-n until the bottom.
   (or Finish the proof by C-c C-b at one step *)


References for The Dining Mathematicians

   E.M.Clarke and B.H.Schlingloff "Model Checking", Chapter 24 in
   Handbook of Automated Reasoning, Elsevier Science Publishers, 2001