Hets - the Heterogeneous Tool Set

Copyright(c) Zicheng Wang Liam O'Reilly C. Maeder Uni Bremen 2002-2009
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.CASL2PCFOL

Description

Coding out subsorting (SubPCFOL= -> PCFOL=), following Chap. III:3.1 of the CASL Reference Manual

Synopsis

Documentation

data CASL2PCFOL Source #

The identity of the comorphism

Constructors

CASL2PCFOL 

Instances

Show CASL2PCFOL Source # 

Methods

showsPrec :: Int -> CASL2PCFOL -> ShowS

show :: CASL2PCFOL -> String

showList :: [CASL2PCFOL] -> ShowS

Language CASL2PCFOL Source # 

Methods

language_name :: CASL2PCFOL -> String Source #

description :: CASL2PCFOL -> String Source #

Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 

encodeSig :: Sign f e -> Sign f e Source #

Add injection, projection and membership symbols to a signature

mkInjectivityName :: String -> SORT -> SORT -> String Source #

Make the name for the embedding or projecton injectivity axiom

mkEmbInjName :: SORT -> SORT -> String Source #

Make the name for the embedding injectivity axiom

mkProjInjName :: SORT -> SORT -> String Source #

Make the name for the projection injectivity axiom

mkInjectivity :: (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f Source #

create a quantified injectivity implication

mkInjImpl :: (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f Source #

create an injectivity implication over x and y

injectTo :: TermExtension f => SORT -> TERM f -> TERM f Source #

apply injection function

projectTo :: TermExtension f => SORT -> TERM f -> TERM f Source #

apply (a partial) projection function

mkEmbInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the embedding injectivity axiom from s to s' i.e., forall x,y:s . inj(x)=e=inj(y) => x=e=y

mkProjInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the projection injectivity axiom from s' to s i.e., forall x,y:s . pr(x)=e=pr(y) => x=e=y

mkProjName :: SORT -> SORT -> String Source #

Make the name for the projection axiom

mkXExEq :: SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f Source #

create a quantified existential equation over x of sort s

mkProjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the projection axiom from s' to s i.e., forall x:s . pr(inj(x))=e=x

mkTransAxiomName :: SORT -> SORT -> SORT -> String Source #

Make the name for the transitivity axiom from s to s' to s''

mkTransAxiom :: TermExtension f => SORT -> SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the transitivity axiom from s to s' to s'' i.e., forall x:s . inj(inj(x))=e=inj(x)

mkIdAxiomName :: SORT -> SORT -> String Source #

Make the name for the identity axiom from s to s'

mkIdAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the identity axiom from s to s' i.e., forall x:s . inj(inj(x))=e=x