(*-------------------------------------------*
            |                                           |
            |      Full Norml Form in the model F       |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                   May 2006                |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            |                                           |
            *-------------------------------------------*)

1 Introduction 

This package "FNF_F" provides a proof to transform any CSP processes
to a full normal form by applying the CSP laws given in the package
CSP_F. That means, the stable-failures equeivalence "P =F Q" can be
proven by the CSP laws and induction, without using the semantics.


2 Theory files

This directory gives theory files for the instantiated part for F.

  (1) To fully sequentialise processes

      FNF_F_sf.thy         FNF_F_sf_int.thy
      FNF_F_sf_def.thy     FNF_F_sf_par.thy
      FNF_F_sf_ext.thy     FNF_F_sf_ren.thy
      FNF_F_sf_hide.thy    FNF_F_sf_rest.thy
      FNF_F_sf_induct.thy  FNF_F_sf_seq.thy

  (2) To fully normalise sequential-processes

      FNF_F_nf_def.thy     FNF_F_nf_int.thy
      FNF_F_nf.thy      

  (3) To show full normal form is uniquely decided

      FNF_F_nf_id.thy

  (4) the main theory of FNF_F

      FNF_F.thy

  (5) A counter example for Conventional full normal form

      Counter_EX.thy

  (6) A samll exmaple of (extended) full normalisation

      DIV_Example.thy


3 How to use FNF_F.

(note: CSP_T is required for CSP_F)

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

(2) To start Isabelle with FNF_F:
    isabelle -I FNF_F
 
(3) To start ProofGeneral with FNF_F:
    Isabelle -l FNF_F

(4) To use FNF_F:
    theory [theory name] = FNF_F: