(*-------------------------------------------*
            |                                           |
            |   The instantiated part for the mode T    |
            |                                           |
            |        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 instantiated part for T.

  (1) Domain theory for the traces model T

      Domain_T.thy  Domain_T_cms.thy  Domain_T_cpo.thy

  (2) Semantics

      CSP_T_semantics.thy
      CSP_T_op_alpha_par.thy
      CSP_T_op_index_par.thy
      CSP_T_traces.thy
      CSP_T_tracesfun.thy
      CSP_T_full_abs.thy

  (3) Properties for operators

      CSP_T_continuous.thy
      CSP_T_contraction.thy
      CSP_T_mono.thy

  (4) CSP laws

      CSP_T_law.thy            CSP_T_law_dist.thy
      CSP_T_law_SKIP.thy       CSP_T_law_fp.thy
      CSP_T_law_alpha_par.thy  CSP_T_law_index_par.thy
      CSP_T_law_commut.thy     CSP_T_law_ref.thy
      CSP_T_law_decompo.thy    CSP_T_law_step.thy

  (5) CSP tactic for T

      CSP_T_tactic.thy

  (6) the main theory of CSP_T

      CSP_T.thy 

3 How to use CSP_T.

(note: CSP is required for CSP_T)

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

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

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

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

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.