Hets - the Heterogeneous Tool Set

Copyright	(c) Soeren Schulze, Uni Bremen 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	s.schulze@uni-bremen.de
Stability	experimental
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.CommonLogic2IsabelleHOL

Description

A direct comorphism from CommonLogic to Isabelle-HOL, passing arguments as native Isabelle lists.

Documentation

data CommonLogic2IsabelleHOL

Constructors

CommonLogic2IsabelleHOL

mapSentence :: Sign -> TEXT_META -> Result Sentence

mapTheory :: (Sign, [Named TEXT_META]) -> Result (Sign, [Named Sentence])

individualS :: String

individualT :: Typ

ax_that :: Named Sentence

type RENAMES = Map String VName

mkIndName :: String -> VName

addRenames :: RENAMES -> [String] -> RENAMES

makeRenames :: [String] -> RENAMES

basicRenames :: Sign -> RENAMES

rename :: RENAMES -> String -> VName

mapSig :: Sign -> Sign

relSymb :: VName

thatSymb :: VName

funSymb :: VName

quantify :: RENAMES -> QUANT -> String -> Term -> Term

transTextMeta :: Sign -> TEXT_META -> Term

transNamed :: Sign -> Named TEXT_META -> Named Sentence

transText :: RENAMES -> TEXT -> Term

transPhrase :: RENAMES -> PHRASE -> Term

transTerm :: RENAMES -> TERM -> Term

transNameOrSeqmark :: NAME_OR_SEQMARK -> String

transTermSeq :: RENAMES -> TERM_SEQ -> Term

transArgsSimple :: RENAMES -> [TERM_SEQ] -> Maybe Term

transArgs :: RENAMES -> [TERM_SEQ] -> Term

applyTermSeq :: VName -> RENAMES -> TERM -> [TERM_SEQ] -> Term

transSen :: RENAMES -> SENTENCE -> Term