X-symbols
This version of CSP-Prover is available on Isabelle 2008. The previous
version (i.e CSP-Prover on Isabelle 2007) caused several errors and
many warnings in Isabelle 2008. The errors were easily solved, but some
warnings still remain.
Most of the warnings were "Currently parsed expression could be
extremely ambiguous." We have not found the clear solution for the
warnings, but most of them could be removed by invalidating the
X-symbols of CSP-Processes. Therefore, we separated the definitions of
X-symbols from the main definitions and theorems, and collected them
into new files "CSP_*_xsymbols". If you do not use X-symbols of
CSP-Processes, it is recommended to use the theories
CSP_Main, CSP_T_Main, and CSP_F_Main,
instead of
CSP, CSP_T, and CSP_F.
CSP_*_Main contains all the definitions and theorems of previous
CSP-Prover except the definitions on X-symbols, and CSP_* imports
CSP_*_Main and CSP_*_xsymbols (e.g. see dependency-graph).
If you use "CSP_F", then you will frequently meet with warnings,
especially on sets. For example, even the following simple equation
causes "Currently parsed expression could be extremely ambiguous."
lemma "{a,a}={a}"
By using "CSP_F_Main" instead of "CSP_F", most of such warnings
disappear. The warnings which still remain in CSP_F_Main are caused by
the syntactical ambiguity on the remaining operator "P[[r]]", which did
not happen in Isabelle 2005. The warnings would be easily removed by
changing the syntax, but we did not it to keep the compatibility with
old CSP-Provers as much as possible. We continue working to solve this
problems.