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 Source #

Constructors

CommonLogic2IsabelleHOL

Instances

Instances details

Show CommonLogic2IsabelleHOL Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods showsPrec :: Int -> CommonLogic2IsabelleHOL -> ShowS show :: CommonLogic2IsabelleHOL -> String showList :: [CommonLogic2IsabelleHOL] -> ShowS
Language CommonLogic2IsabelleHOL Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods language_name :: CommonLogic2IsabelleHOL -> String Source # description :: CommonLogic2IsabelleHOL -> String Source #
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic Source # sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # minSourceTheory :: CommonLogic2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CommonLogic2IsabelleHOL -> Isabelle Source # mapSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL -> Maybe () Source # map_theory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CommonLogic2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: CommonLogic2IsabelleHOL -> Sign0 -> TEXT_META -> Result Sentence Source # map_symbol :: CommonLogic2IsabelleHOL -> Sign0 -> Symbol -> Set () Source # extractModel :: CommonLogic2IsabelleHOL -> Sign0 -> () -> Result (Sign0, [Named TEXT_META]) Source # is_model_transportable :: CommonLogic2IsabelleHOL -> Bool Source # has_model_expansion :: CommonLogic2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool Source # constituents :: CommonLogic2IsabelleHOL -> [String] Source # isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool Source # rps :: CommonLogic2IsabelleHOL -> Bool Source # eps :: CommonLogic2IsabelleHOL -> Bool Source # isGTC :: CommonLogic2IsabelleHOL -> Bool Source #