Copyright	(c) Sonja Groening Christian Maeder Uni Bremen 2004-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Isabelle.IsaConsts

Contents

boolean constants strings
quantor strings
Strings of binary ops
some stuff for Isabelle
some stuff for HasCASL
strings for HOLCF lifting functions
Predefined CLASSES
predefined SORTS
predefined types
predefinded HOLCF types
term construction
binary junctors
terms for HOL-HOLCF
Boolean constants
UNTYPED terms
HOLCF
constant names
VNames of binary operators
keywords in theory files from the Isar Reference Manual 2005

Description

constants for Isabelle

Synopsis

topSort :: (a -> a -> Bool) -> [a] -> [a]
liftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool
getTypeIds :: Typ -> Set TName
deDepOn :: DomainEntry -> DomainEntry -> Bool
ordDoms :: DomainTab -> DomainTab
cTrue :: String
cFalse :: String
cNot :: String
allS :: String
exS :: String
ex1S :: String
conj :: String
disj :: String
impl :: String
eq :: String
neq :: String
plusS :: String
minusS :: String
timesS :: String
divS :: String
modS :: String
consS :: String
lconsS :: String
appendS :: String
compS :: String
pairC :: String
eqvSimS :: String
unionS :: String
membershipS :: String
imageS :: String
rangeS :: String
pcpoS :: String
prodS :: TName
sProdS :: TName
funS :: TName
cFunS :: TName
lFunS :: TName
sSumS :: TName
lProdS :: TName
lSumS :: TName
aptS :: String
appS :: String
pAppS :: String
defOpS :: String
someS :: String
lliftbinS :: String
fliftbinS :: String
flift2S :: String
pcpo :: IsaClass
isaTerm :: IsaClass
holType :: Sort
dom :: Sort
sortT :: Continuity -> Sort
mkSTypeT :: Continuity -> String -> Typ
listT :: Continuity -> Typ -> Typ
charT :: Continuity -> Typ
ratT :: Continuity -> Typ
fracT :: Continuity -> Typ
integerT :: Continuity -> Typ
boolT :: Continuity -> Typ
orderingT :: Continuity -> Typ
intT :: Continuity -> Typ
prodT :: Continuity -> Typ -> Typ -> Typ
funT :: Continuity -> Typ -> Typ -> Typ
curryFunT :: Continuity -> [Typ] -> Typ -> Typ
mkSType :: String -> Typ
noTypeT :: Typ
noType :: DTyp
noTypeC :: DTyp
hideNN :: Typ -> DTyp
hideCN :: Typ -> DTyp
dispNN :: Typ -> DTyp
dispMN :: Typ -> DTyp
boolType :: Typ
mkListType :: Typ -> Typ
mkOptionType :: Typ -> Typ
prodType :: Typ -> Typ -> Typ
mkFunType :: Typ -> Typ -> Typ
mkCurryFunType :: [Typ] -> Typ -> Typ
mkSDomType :: String -> Typ
voidDom :: Typ
flatDom :: Typ
tLift :: Typ -> Typ
mkBinDomType :: String -> Typ -> Typ -> Typ
mkContFun :: Typ -> Typ -> Typ
mkStrictProduct :: Typ -> Typ -> Typ
mkContProduct :: Typ -> Typ -> Typ
mkCurryContFun :: [Typ] -> Typ -> Typ
mkStrictSum :: Typ -> Typ -> Typ
maxPrio :: Int
lowPrio :: Int
isaEqPrio :: Int
mkConstVD :: String -> Typ -> Term
mkConstV :: String -> DTyp -> Term
mkConstD :: VName -> Typ -> Term
mkConst :: VName -> DTyp -> Term
mkFree :: String -> Term
con :: VName -> Term
conC :: VName -> Term
conDouble :: String -> Term
conDoubleC :: String -> Term
binVNameAppl :: VName -> Term -> Term -> Term
binConj :: Term -> Term -> Term
binDisj :: Term -> Term -> Term
binImpl :: Term -> Term -> Term
binEqv :: Term -> Term -> Term
binEq :: Term -> Term -> Term
binEqvSim :: Term -> Term -> Term
binUnion :: Term -> Term -> Term
binMembership :: Term -> Term -> Term
binImageOp :: Term -> Term -> Term
rangeOp :: Term -> Term
termAppl :: Term -> Term -> Term
andPT :: Continuity -> Term
orPT :: Continuity -> Term
notPT :: Continuity -> Term
bottomPT :: Continuity -> Term
nilPT :: Continuity -> Term
consPT :: Continuity -> Term
truePT :: Continuity -> Term
falsePT :: Continuity -> Term
headPT :: Continuity -> Term
tailPT :: Continuity -> Term
unitPT :: Continuity -> Term
fstPT :: Continuity -> Term
sndPT :: Continuity -> Term
pairPT :: Continuity -> Term
nothingPT :: Continuity -> Term
justPT :: Continuity -> Term
leftPT :: Continuity -> Term
rightPT :: Continuity -> Term
compPT :: Term
eqPT :: Term
neqPT :: Term
eqTPT :: Typ -> Term
neqTPT :: Typ -> Term
true :: Term
false :: Term
defOp :: Term
notOp :: Term
conSome :: Term
liftString :: Term
lpairTerm :: Term
notV :: VName
conjV :: VName
disjV :: VName
implV :: VName
eqV :: VName
neqV :: VName
plusV :: VName
minusV :: VName
divV :: VName
modV :: VName
timesV :: VName
consV :: VName
lconsV :: VName
appendV :: VName
compV :: VName
eqvSimV :: VName
unionV :: VName
membershipV :: VName
imageV :: VName
rangeV :: VName
vMap' :: Map String VName
vMap :: Map String VName
endS :: String
headerS :: String
theoryS :: String
importsS :: String
usesS :: String
beginS :: String
contextS :: String
axiomsS :: String
axiomatizationS :: String
defsS :: String
oopsS :: String
mlS :: String
mlFileS :: String
andS :: String
lemmasS :: String
lemmaS :: String
corollaryS :: String
refuteS :: String
theoremsS :: String
theoremS :: String
axclassS :: String
classesS :: String
definitionS :: String
instanceS :: String
instantiationS :: String
typedeclS :: String
typesS :: String
constsS :: String
structureS :: String
constdefsS :: String
domainS :: String
datatypeS :: String
fixrecS :: String
primrecS :: String
declareS :: String
simpS :: String
applyS :: String
backS :: String
deferS :: String
preferS :: String
byS :: String
doneS :: String
sorryS :: String
autoS :: String
inductS :: String
caseTacS :: String
insertS :: String
subgoalTacS :: String
typedefS :: String
premiseOpenS :: String
premiseCloseS :: String
metaImplS :: String
usingS :: String
whereS :: String
dotDot :: String
barS :: String
markups :: [String]
ignoredKeys :: [String]
usedTopKeys :: [String]
isaKeywords :: [String]
mkVName :: String -> VName

Documentation

topSort :: (a -> a -> Bool) -> [a] -> [a] Source #

a topological sort with a uses predicate

liftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool Source #

extends a dependency relation to lists using any

getTypeIds :: Typ -> Set TName Source #

deDepOn :: DomainEntry -> DomainEntry -> Bool Source #

ordDoms :: DomainTab -> DomainTab Source #

boolean constants strings

cTrue :: String Source #

cFalse :: String Source #

cNot :: String Source #

Not string

quantor strings

allS :: String Source #

exS :: String Source #

ex1S :: String Source #

Strings of binary ops

conj :: String Source #

disj :: String Source #

impl :: String Source #

eq :: String Source #

neq :: String Source #

plusS :: String Source #

minusS :: String Source #

timesS :: String Source #

divS :: String Source #

modS :: String Source #

consS :: String Source #

lconsS :: String Source #

appendS :: String Source #

compS :: String Source #

pairC :: String Source #

lower case pair

eqvSimS :: String Source #

unionS :: String Source #

membershipS :: String Source #

imageS :: String Source #

Imange of functions

rangeS :: String Source #

some stuff for Isabelle

pcpoS :: String Source #

prodS :: TName Source #

sProdS :: TName Source #

funS :: TName Source #

cFunS :: TName Source #

lFunS :: TName Source #

sSumS :: TName Source #

lProdS :: TName Source #

lSumS :: TName Source #

some stuff for HasCASL

aptS :: String Source #

appS :: String Source #

pAppS :: String Source #

defOpS :: String Source #

someS :: String Source #

Some string

strings for HOLCF lifting functions

lliftbinS :: String Source #

fliftbinS :: String Source #

flift2S :: String Source #

Predefined CLASSES

pcpo :: IsaClass Source #

isaTerm :: IsaClass Source #

predefined SORTS

holType :: Sort Source #

dom :: Sort Source #

sortT :: Continuity -> Sort Source #

mkSTypeT :: Continuity -> String -> Typ Source #

listT :: Continuity -> Typ -> Typ Source #

charT :: Continuity -> Typ Source #

ratT :: Continuity -> Typ Source #

fracT :: Continuity -> Typ Source #

integerT :: Continuity -> Typ Source #

boolT :: Continuity -> Typ Source #

orderingT :: Continuity -> Typ Source #

intT :: Continuity -> Typ Source #

prodT :: Continuity -> Typ -> Typ -> Typ Source #

funT :: Continuity -> Typ -> Typ -> Typ Source #

curryFunT :: Continuity -> [Typ] -> Typ -> Typ Source #

predefined types

mkSType :: String -> Typ Source #

noTypeT :: Typ Source #

noType :: DTyp Source #

noTypeC :: DTyp Source #

hideNN :: Typ -> DTyp Source #

hideCN :: Typ -> DTyp Source #

dispNN :: Typ -> DTyp Source #

dispMN :: Typ -> DTyp Source #

boolType :: Typ Source #

mkListType :: Typ -> Typ Source #

mkOptionType :: Typ -> Typ Source #

prodType :: Typ -> Typ -> Typ Source #

mkFunType :: Typ -> Typ -> Typ Source #

mkCurryFunType :: [Typ] -> Typ -> Typ Source #

predefinded HOLCF types

mkSDomType :: String -> Typ Source #

voidDom :: Typ Source #

flatDom :: Typ Source #

tLift :: Typ -> Typ Source #

mkBinDomType :: String -> Typ -> Typ -> Typ Source #

mkContFun :: Typ -> Typ -> Typ Source #

mkStrictProduct :: Typ -> Typ -> Typ Source #

mkContProduct :: Typ -> Typ -> Typ Source #

mkCurryContFun :: [Typ] -> Typ -> Typ Source #

mkStrictSum :: Typ -> Typ -> Typ Source #

term construction

maxPrio :: Int Source #

1000

lowPrio :: Int Source #

10

isaEqPrio :: Int Source #

2

mkConstVD :: String -> Typ -> Term Source #

construct constants and variables

mkConstV :: String -> DTyp -> Term Source #

mkConstD :: VName -> Typ -> Term Source #

mkConst :: VName -> DTyp -> Term Source #

mkFree :: String -> Term Source #

con :: VName -> Term Source #

construct a constant with no type

conC :: VName -> Term Source #

conDouble :: String -> Term Source #

conDoubleC :: String -> Term Source #

binVNameAppl :: VName -> Term -> Term -> Term Source #

apply VName operator to two term

binary junctors

binConj :: Term -> Term -> Term Source #

binDisj :: Term -> Term -> Term Source #

binImpl :: Term -> Term -> Term Source #

binEqv :: Term -> Term -> Term Source #

binEq :: Term -> Term -> Term Source #

binEqvSim :: Term -> Term -> Term Source #

binUnion :: Term -> Term -> Term Source #

binMembership :: Term -> Term -> Term Source #

binImageOp :: Term -> Term -> Term Source #

rangeOp :: Term -> Term Source #

termAppl :: Term -> Term -> Term Source #

HOL function application

terms for HOL-HOLCF

andPT :: Continuity -> Term Source #

orPT :: Continuity -> Term Source #

notPT :: Continuity -> Term Source #

bottomPT :: Continuity -> Term Source #

nilPT :: Continuity -> Term Source #

consPT :: Continuity -> Term Source #

truePT :: Continuity -> Term Source #

falsePT :: Continuity -> Term Source #

headPT :: Continuity -> Term Source #

tailPT :: Continuity -> Term Source #

unitPT :: Continuity -> Term Source #

fstPT :: Continuity -> Term Source #

sndPT :: Continuity -> Term Source #

pairPT :: Continuity -> Term Source #

nothingPT :: Continuity -> Term Source #

justPT :: Continuity -> Term Source #

leftPT :: Continuity -> Term Source #

rightPT :: Continuity -> Term Source #

compPT :: Term Source #

eqPT :: Term Source #

neqPT :: Term Source #

eqTPT :: Typ -> Term Source #

neqTPT :: Typ -> Term Source #

Boolean constants

true :: Term Source #

false :: Term Source #

UNTYPED terms

defOp :: Term Source #

defOp constant

notOp :: Term Source #

Not constant

conSome :: Term Source #

some constant

HOLCF

liftString :: Term Source #

lpairTerm :: Term Source #

constant names

notV :: VName Source #

Not VName

VNames of binary operators

conjV :: VName Source #

disjV :: VName Source #

implV :: VName Source #

eqV :: VName Source #

neqV :: VName Source #

plusV :: VName Source #

minusV :: VName Source #

divV :: VName Source #

modV :: VName Source #

timesV :: VName Source #

consV :: VName Source #

lconsV :: VName Source #

appendV :: VName Source #

compV :: VName Source #

eqvSimV :: VName Source #

unionV :: VName Source #

membershipV :: VName Source #

imageV :: VName Source #

rangeV :: VName Source #

vMap' :: Map String VName Source #

vMap :: Map String VName Source #

keywords in theory files from the Isar Reference Manual 2005

endS :: String Source #

headerS :: String Source #

theoryS :: String Source #

importsS :: String Source #

usesS :: String Source #

beginS :: String Source #

contextS :: String Source #

axiomsS :: String Source #

axiomatizationS :: String Source #

defsS :: String Source #

oopsS :: String Source #

mlS :: String Source #

mlFileS :: String Source #

andS :: String Source #

lemmasS :: String Source #

lemmaS :: String Source #

corollaryS :: String Source #

refuteS :: String Source #

theoremsS :: String Source #

theoremS :: String Source #

axclassS :: String Source #

classesS :: String Source #

definitionS :: String Source #

instanceS :: String Source #

instantiationS :: String Source #

typedeclS :: String Source #

typesS :: String Source #

constsS :: String Source #

structureS :: String Source #

constdefsS :: String Source #

domainS :: String Source #

datatypeS :: String Source #

fixrecS :: String Source #

primrecS :: String Source #

declareS :: String Source #

simpS :: String Source #

applyS :: String Source #

backS :: String Source #

deferS :: String Source #

preferS :: String Source #

byS :: String Source #

doneS :: String Source #

sorryS :: String Source #

autoS :: String Source #

inductS :: String Source #

caseTacS :: String Source #

insertS :: String Source #

subgoalTacS :: String Source #

typedefS :: String Source #

premiseOpenS :: String Source #

premiseCloseS :: String Source #

metaImplS :: String Source #

usingS :: String Source #

whereS :: String Source #

dotDot :: String Source #

barS :: String Source #

markups :: [String] Source #

ignoredKeys :: [String] Source #

toplevel keys that are currently ignored

usedTopKeys :: [String] Source #

toplevel keywords currently recognized by IsaParse

isaKeywords :: [String] Source #

all Isabelle keywords

mkVName :: String -> VName Source #