Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski and Uni Bremen 2003-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.CFOL2IsabelleHOL

Description

The embedding comorphism from CASL to Isabelle-HOL.

Synopsis

Documentation

data CFOL2IsabelleHOL Source #

The identity of the comorphism

Constructors

CFOL2IsabelleHOL 

Instances

Show CFOL2IsabelleHOL Source # 

Methods

showsPrec :: Int -> CFOL2IsabelleHOL -> ShowS

show :: CFOL2IsabelleHOL -> String

showList :: [CFOL2IsabelleHOL] -> ShowS

Language CFOL2IsabelleHOL Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

transVar :: Set String -> VAR -> String Source #

typeToks :: Sign f e -> Set String Source #

mapSen :: FormulaTranslator f e -> Sign f e -> Set String -> FORMULA f -> Sentence Source #

type SignTranslator f e = Sign f e -> e -> IsaTheory -> IsaTheory Source #

type FormulaTranslator f e = Sign f e -> Set String -> f -> Term Source #

getAssumpsToks :: Sign f e -> Set String Source #

quantifyIsa :: String -> (String, Typ) -> Term -> Term Source #

quantify :: Set String -> QUANTIFIER -> (VAR, SORT) -> Term -> Term Source #

transFORMULA :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> FORMULA f -> Term Source #

transRecord :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> Record f Term Term Source #

transOpSymb :: Sign f e -> Set String -> OP_SYMB -> VName Source #