|
Revision 10619, 0.9 kB
(checked in by csliam, 15 months ago)
|
|
Added production of the first intergation theorem and continued work on
process translation
|
| Line | |
|---|
| 1 | {- | |
|---|
| 2 | Module : $Header$ |
|---|
| 3 | Description : Constants for the translation of processes from CspCASL |
|---|
| 4 | to IsabelleHOL (CspProver) |
|---|
| 5 | Copyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach, |
|---|
| 6 | Swansea University 2008 |
|---|
| 7 | License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt |
|---|
| 8 | |
|---|
| 9 | Maintainer : csliam@swansea.ac.uk |
|---|
| 10 | Stability : provisional |
|---|
| 11 | Portability : non-portable (imports Logic.Logic) |
|---|
| 12 | |
|---|
| 13 | Constants for the translation of processes from CspCASL to IsabelleHOL |
|---|
| 14 | (CspProver) |
|---|
| 15 | |
|---|
| 16 | -} |
|---|
| 17 | |
|---|
| 18 | module CspCASL.Trans_Consts where |
|---|
| 19 | |
|---|
| 20 | import CASL.AS_Basic_CASL |
|---|
| 21 | import Isabelle.IsaConsts |
|---|
| 22 | import Isabelle.IsaSign |
|---|
| 23 | |
|---|
| 24 | alphabetS :: String |
|---|
| 25 | alphabetS = "Alphabet" |
|---|
| 26 | |
|---|
| 27 | barExtS :: String |
|---|
| 28 | barExtS = "_Bar" |
|---|
| 29 | |
|---|
| 30 | classS :: String |
|---|
| 31 | classS = "class" |
|---|
| 32 | |
|---|
| 33 | classOp :: Term -> Term |
|---|
| 34 | classOp = termAppl (conDouble classS) |
|---|
| 35 | |
|---|
| 36 | -- Convert a SORT to a string |
|---|
| 37 | convertSort2String :: SORT -> String |
|---|
| 38 | convertSort2String s = show s |
|---|
