(*-------------------------------------------*
            |                                           |
            |          << The reusable part >>          |
            |                                           |
            |        CSP-Prover on Isabelle2004         |
            |              December 2004                |
            |              February 2005  (modified)    |
            |                  June 2005  (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |              November 2005  (modified)    |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            |                                           |
            *-------------------------------------------*)

1 Introduction 

CSP-Prover [1] provides a deep encoding of the process algebra CSP
within the interactive theorem prover Isabelle. It has a generic
architecture divided into a large reusable part independent of
specific CSP models and an instantiated part for each specific CSP
model.

The reusable part contains Banach's fixpoint theorem and the metric
fixpoint induction rule based on complete metric spaces as well as
Tarski's fixpoint theorem and the standard fixpoint induction rule
based on complete partial orders. Furthermore, infinite product
constructions are provided as lifting theorems which are required for
infinite state systems. Another contribution of the model-independent
part is the definition of the CSP syntax as a recursive type.  This
means that the syntax is deeply encoded. Therefore, CSP-Prover
supports structural induction on processes.

The model dependent part is currently instantiated by the traces model
T and the stable failures model F. They define the domains T and F
together with proofs in Isabelle which establish that T and F indeed
are complete metric spaces as well as complete partial orders.
Furthermore, they define the semantic clauses of T and F. Finally, a
model-dependent proof infrastructure for each model is provided, such
as step laws as well as distributive laws, or the tactic csp_hnf_tac
that translates CSP expressions into Head Normal Form.

2 Theory files

This directory gives theory files for the Reusable part.

  (1) CSP-Prover infrastructure

      Infra.thy         Infra_list.thy   Infra_prog.thy
      Infra_common.thy  Infra_nat.thy    Infra_real.thy
      Infra_exp.thy     Infra_order.thy  Infra_set.thy
      Infra_fun.thy     Infra_pair.thy   Infra_type.thy

  (2) CPO theory

      CPO.thy  CPO_pair.thy  CPO_prod.thy CPO_set.thy

  (3) CMS theory and restriction spaces

      CMS.thy  RS.thy  RS_pair.thy  RS_prod.thy  Norm_seq.thy

  (4) CSP syntax

      CSP_syntax.thy

  (5) Trace theory

      Trace.thy  Prefix.thy
      Trace_hide.thy  Trace_par.thy  Trace_ren.thy  Trace_seq.thy 

  (6) the main theory of reusable CSP

      CSP.thy 

2 How to use CSP.

(note: Isabelle(2005)/HOL-Complex is required for CSP)

(1) To build the heap file for CSP:
    isatool usedir -b HOL-Complex CSP

(2) To start Isabelle with CSP:
    isabelle -I CSP

(3) To start ProofGeneral with CSP:
    Isabelle -l CSP

(4) To use CSP:
    theory test = CSP:

References

[1] Y.Isobe and M.Roggenbach: A Generic Theorem Prover of CSP
    Refinement, TACAS 2005 (11th International Conference on Tools and
    Algorithms for the Construction and Analysis of Systems), LNCS
    3440, pp.108-123, Edinburgh, April 2005.