(*-------------------------------------------*
            |                CSP-Prover                 |
            |              December 2004                |
            |              February 2005  (modified)    |
            |                  June 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 stable failures
model F.  It defines the domain F together with proofs in Isabelle
which establish that F indeed is a complete metric space as well as a
complete partial order. Furthermore, it defines the semantic clauses
of F. Finally, model-dependent proof infrastructure is provided, such
as step laws as well as distributive laws holding in F, or the tactic
csp_hnf_tac that translates CSP expressions into Head Normal Form.

2 Theory files

[Reusable part]

  (1) CSP-Prover infrastructure

    Infra.thy

  (2) CPO theory

    CPO.thy  CPO_pair.thy  CPO_prod.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 

[Instantiated part]

  (1) Domain theory for the Stable Failures model (SF)

    Domain_T.thy        Domain_T_cms.thy        Domain_T_cpo.thy
    Domain_F.thy        Domain_F_cms.thy        Domain_F_cpo.thy
    Domain_SF.thy       Domain_SF_cms.thy       Domain_SF_cpo.thy
    Domain_SF_prod.thy  Domain_SF_prod_cms.thy  Domain_SF_prod_cpo.thy

  (2) Semantic clauses 

    CSP_semantics.thy   CSP_semantics_exp.thy

  (3) Proofs of correctness of semantics, contractiveness on cms, and
      continuity on cpo for each operators and process expressions.

    SKIP.thy   STOP.thy  DIV.thy  Constant_cms.thy  Constant_cpo.thy
    Act_prefix.thy  Act_prefix_cms.thy  Act_prefix_cpo.thy
    Ext_choice.thy  Ext_choice_cms.thy  Ext_choice_cpo.thy
    Ext_pre_choice.thy  Ext_pre_choice_cms.thy  Ext_pre_choice_cpo.thy
    Int_choice.thy  Int_choice_cms.thy  Int_choice_cpo.thy
    Rep_int_choice.thy  Rep_int_choice_cms.thy  Rep_int_choice_cpo.thy
    Parallel.thy  Parallel_cms.thy  Parallel_cpo.thy
    Hiding.thy  Hiding_cpo.thy
    Renaming.thy  Renaming_cms.thy  Renaming_cpo.thy
    Conditional.thy  Conditional_cms.thy  Conditional_cpo.thy
    Seq_compo.thy  Seq_compo_cms.thy  Seq_compo_cpo.thy
    Proc_name.thy  Proc_name_cms.thy  Proc_name_cpo.thy

    CSP_proc.thy  CSP_proc_cms.thy  CSP_proc_cpo.thy

  (4) Replicated alphabetized parallel (as a syntactic sugar)

    Alpha_parallel.thy  Rep_parallel.thy  Index_parallel.thy

  (5) CSP laws

    CSP_law_SKIP.thy  CSP_law_commut.thy  CSP_law_decompo.thy
    CSP_law_dist.thy  CSP_law_etc.thy  CSP_law_fp.thy
    CSP_law_par1.thy  CSP_law_par2.thy  CSP_law_ref.thy
    CSP_law_step1.thy  CSP_law_step2.thy  

  (6) Proof rules and tactics for CSP

    CSP_rule_rw.thy  CSP_tactic.thy  CSP.thy

3 How to use CSP.

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

(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.