(*-------------------------------------------*
            |                                           |
            |   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)    |
            |                   May 2006  (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2009         |
            |                   June 2009  (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.

This package "CSP_T" provides the instantiated part for the traces
model T. It defines the domain "domT" together with proofs in Isabelle
which establish that domT indeed are complete metric spaces as well as
complete partial orders. Furthermore, it define the semantic clauses
of the model T. Finally, a model-dependent proof infrastructure for
the model T is provided, thus CSP-laws such as step laws as well as
distributive laws, or tactics such as cspT_hsf_tac that translates CSP
expressions into Head Sequential 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_surj.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_etc.thy
      CSP_T_law_DIV.thy        CSP_T_law_fp.thy
      CSP_T_law_SKIP.thy       CSP_T_law_norm.thy
      CSP_T_law_SKIP_DIV.thy   CSP_T_law_ref.thy
      CSP_T_law_alpha_par.thy  CSP_T_law_rep_par.thy
      CSP_T_law_aux.thy        CSP_T_law_step.thy
      CSP_T_law_basic.thy      CSP_T_law_step_ext.thy
      CSP_T_law_decompo.thy    CSP_T_law_ufp.thy
      CSP_T_law_dist.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:
    isabelle usedir -b CSP CSP_T

(2) To start ProofGeneral with CSP_T:
    isabelle emacs -l CSP_T

(3) To use CSP_T:
    theory [theory name] = 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.