Copyright	(c) Till Mossakowski and Uni Bremen 2003-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	hausmann@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.CoCFOL2IsabelleHOL

Description

The embedding comorphism from CoCASL to Isabelle-HOL.

Synopsis

data CoCFOL2IsabelleHOL = CoCFOL2IsabelleHOL

Documentation

data CoCFOL2IsabelleHOL Source #

The identity of the comorphism

Constructors

CoCFOL2IsabelleHOL

Instances

Instances details

Show CoCFOL2IsabelleHOL Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods showsPrec :: Int -> CoCFOL2IsabelleHOL -> ShowS show :: CoCFOL2IsabelleHOL -> String showList :: [CoCFOL2IsabelleHOL] -> ShowS
Language CoCFOL2IsabelleHOL Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods language_name :: CoCFOL2IsabelleHOL -> String Source # description :: CoCFOL2IsabelleHOL -> String Source #
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CoCFOL2IsabelleHOL Methods sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL Source # sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # sourceSublogicLossy :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics Source # minSourceTheory :: CoCFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CoCFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe () Source # map_theory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CoCFOL2IsabelleHOL -> (CSign, [Named CoCASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CoCFOL2IsabelleHOL -> CoCASLMor -> Result IsabelleMorphism Source # map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence Source # map_symbol :: CoCFOL2IsabelleHOL -> CSign -> Symbol -> Set () Source # extractModel :: CoCFOL2IsabelleHOL -> CSign -> () -> Result (CSign, [Named CoCASLFORMULA]) Source # is_model_transportable :: CoCFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CoCFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool Source # constituents :: CoCFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CoCFOL2IsabelleHOL -> Bool Source # rps :: CoCFOL2IsabelleHOL -> Bool Source # eps :: CoCFOL2IsabelleHOL -> Bool Source # isGTC :: CoCFOL2IsabelleHOL -> Bool Source #