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

The identity of the comorphism

Constructors

CASL2PCFOL 

Instances

encodeSig :: Sign f e -> Sign f e

Add injection, projection and membership symbols to a signature

mkInjectivityName :: String -> SORT -> SORT -> String

Make the name for the embedding or projecton injectivity axiom

mkEmbInjName :: SORT -> SORT -> String

Make the name for the embedding injectivity axiom

mkProjInjName :: SORT -> SORT -> String

Make the name for the projection injectivity axiom

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

create a quantified injectivity implication

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

create an injectivity implication over x and y

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

apply injection function

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

apply (a partial) projection function

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

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)

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

Make the name for the projection axiom

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

create a quantified existential equation over x of sort s

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

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

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

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

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

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

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

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

generateAxioms :: TermExtension f => Sign f e -> [Named (FORMULA f)]

f2Formula :: TermExtension f => FORMULA f -> FORMULA f

t2Term :: TermExtension f => TERM f -> TERM f