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

  (1) Domain theory for the stable failures model F

      Domain_F.thy   Domain_F_cms.thy   Domain_F_cpo.thy
      Set_F.thy      Set_F_cms.thy      Set_F_cpo.thy

  (2) Semantics

      CSP_F_semantics.thy
      CSP_F_op_alpha_par.thy
      CSP_F_op_index_par.thy
      CSP_F_failures.thy
      CSP_F_failuresfun.thy
      CSP_F_domain.thy
      CSP_F_full_abs.thy

  (3) Properties for operators

      CSP_F_continuous.thy
      CSP_F_contraction.thy
      CSP_F_mono.thy

  (4) CSP laws

      CSP_F_law.thy            CSP_F_law_dist.thy
      CSP_F_law_SKIP.thy       CSP_F_law_fp.thy
      CSP_F_law_alpha_par.thy  CSP_F_law_index_par.thy
      CSP_F_law_commut.thy     CSP_F_law_ref.thy
      CSP_F_law_decompo.thy    CSP_F_law_step.thy

  (5) CSP tactic for F

      CSP_F_tactic.thy

  (6) the main theory of CSP_F

      CSP_F.thy 

3 How to use CSP_F.

(note: CSP_T is required for CSP_F)

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

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

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

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

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.