Copyright	(c) Till Mossakowski Uni Bremen 2002-2004
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic)
Safe Haskell	None

Isabelle.Logic_Isabelle

Contents

Orphan instances

Description

Instance of class Logic for Isabelle (including Pure, HOL etc.).

Documentation

type IsabelleMorphism = DefaultMorphism Sign Source #

data Isabelle Source #

Constructors

Isabelle

Instances

Instances details

Show Isabelle Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods showsPrec :: Int -> Isabelle -> ShowS show :: Isabelle -> String showList :: [Isabelle] -> ShowS
Language Isabelle Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods language_name :: Isabelle -> String Source # description :: Isabelle -> String Source #
Sentences Isabelle Sentence Sign IsabelleMorphism () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods map_sen :: Isabelle -> IsabelleMorphism -> Sentence -> Result Sentence Source # simplify_sen :: Isabelle -> Sign -> Sentence -> Sentence Source # negation :: Isabelle -> Sentence -> Maybe Sentence Source # print_sign :: Isabelle -> Sign -> Doc Source # print_named :: Isabelle -> Named Sentence -> Doc Source # sym_of :: Isabelle -> Sign -> [Set ()] Source # mostSymsOf :: Isabelle -> Sign -> [()] Source # symmap_of :: Isabelle -> IsabelleMorphism -> EndoMap () Source # sym_name :: Isabelle -> () -> Id Source # sym_label :: Isabelle -> () -> Maybe String Source # fullSymName :: Isabelle -> () -> String Source # symKind :: Isabelle -> () -> String Source # symsOfSen :: Isabelle -> Sign -> Sentence -> [()] Source # pair_symbols :: Isabelle -> () -> () -> Result () Source #
Syntax Isabelle () () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods parsersAndPrinters :: Isabelle -> Map String (PrefixMap -> AParser st (), () -> Doc) Source # parse_basic_spec :: Isabelle -> Maybe (PrefixMap -> AParser st ()) Source # parseSingleSymbItem :: Isabelle -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: Isabelle -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: Isabelle -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: Isabelle -> () -> Item Source # symb_items_name :: Isabelle -> () -> [String] Source #
StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods basic_analysis :: Isabelle -> Maybe (((), Sign, GlobalAnnos) -> Result ((), ExtSign Sign (), [Named Sentence])) Source # sen_analysis :: Isabelle -> Maybe (((), Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: Isabelle -> IRI -> LibName -> () -> Sign -> GlobalAnnos -> Result ((), ExtSign Sign (), [Named Sentence]) Source # stat_symb_map_items :: Isabelle -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Isabelle -> Sign -> [()] -> Result [()] Source # convertTheory :: Isabelle -> Maybe ((Sign, [Named Sentence]) -> ()) Source # ensures_amalgamability :: Isabelle -> ([CASLAmalgOpt], Gr Sign (Int, IsabelleMorphism), [(Int, IsabelleMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Isabelle -> IsabelleMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: Isabelle -> Gr Sign (Int, IsabelleMorphism) -> Result (Sign, Map Int IsabelleMorphism) Source # qualify :: Isabelle -> SIMPLE_ID -> LibName -> IsabelleMorphism -> Sign -> Result (IsabelleMorphism, [Named Sentence]) Source # symbol_to_raw :: Isabelle -> () -> () Source # id_to_raw :: Isabelle -> Id -> () Source # matches :: Isabelle -> () -> () -> Bool Source # empty_signature :: Isabelle -> Sign Source # add_symb_to_sign :: Isabelle -> Sign -> () -> Result Sign Source # signature_union :: Isabelle -> Sign -> Sign -> Result Sign Source # signatureDiff :: Isabelle -> Sign -> Sign -> Result Sign Source # intersection :: Isabelle -> Sign -> Sign -> Result Sign Source # final_union :: Isabelle -> Sign -> Sign -> Result Sign Source # morphism_union :: Isabelle -> IsabelleMorphism -> IsabelleMorphism -> Result IsabelleMorphism Source # is_subsig :: Isabelle -> Sign -> Sign -> Bool Source # subsig_inclusion :: Isabelle -> Sign -> Sign -> Result IsabelleMorphism Source # generated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # cogenerated_sign :: Isabelle -> Set () -> Sign -> Result IsabelleMorphism Source # induced_from_morphism :: Isabelle -> EndoMap () -> Sign -> Result IsabelleMorphism Source # induced_from_to_morphism :: Isabelle -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result IsabelleMorphism Source # is_transportable :: Isabelle -> IsabelleMorphism -> Bool Source # is_injective :: Isabelle -> IsabelleMorphism -> Bool Source # theory_to_taxonomy :: Isabelle -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: Isabelle -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: Isabelle -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: Isabelle -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
LogicalFramework Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods base_sig :: Isabelle -> Sign Source # write_logic :: Isabelle -> String -> String Source # write_syntax :: Isabelle -> String -> IsabelleMorphism -> String Source # write_proof :: Isabelle -> String -> IsabelleMorphism -> String Source # write_model :: Isabelle -> String -> IsabelleMorphism -> String Source # read_morphism :: Isabelle -> FilePath -> IsabelleMorphism Source # write_comorphism :: Isabelle -> String -> String -> String -> IsabelleMorphism -> IsabelleMorphism -> IsabelleMorphism -> String Source #
Logic Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Isabelle.Logic_Isabelle Methods parse_basic_sen :: Isabelle -> Maybe (() -> AParser st Sentence) Source # stability :: Isabelle -> Stability Source # data_logic :: Isabelle -> Maybe AnyLogic Source # top_sublogic :: Isabelle -> () Source # all_sublogics :: Isabelle -> [()] Source # bottomSublogic :: Isabelle -> Maybe () Source # sublogicDimensions :: Isabelle -> [[()]] Source # parseSublogic :: Isabelle -> String -> Maybe () Source # proj_sublogic_epsilon :: Isabelle -> () -> Sign -> IsabelleMorphism Source # provers :: Isabelle -> [Prover Sign Sentence IsabelleMorphism () ()] Source # default_prover :: Isabelle -> String Source # cons_checkers :: Isabelle -> [ConsChecker Sign Sentence () IsabelleMorphism ()] Source # conservativityCheck :: Isabelle -> [ConservativityChecker Sign Sentence IsabelleMorphism] Source # empty_proof_tree :: Isabelle -> () Source # syntaxTable :: Isabelle -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: Isabelle -> Maybe OMCD Source # export_symToOmdoc :: Isabelle -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: Isabelle -> NameMap () -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: Isabelle -> SigMap () -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: Isabelle -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: Isabelle -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: Isabelle -> SigMapI () -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: Isabelle -> (Sign, [Sentence]) -> () Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HolLight2Isabelle Methods sourceLogic :: HolLight2Isabelle -> HolLight Source # sourceSublogic :: HolLight2Isabelle -> HolLightSL Source # sourceSublogicLossy :: HolLight2Isabelle -> HolLightSL Source # minSourceTheory :: HolLight2Isabelle -> Maybe (LibName, String) Source # targetLogic :: HolLight2Isabelle -> Isabelle Source # mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe () Source # map_theory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HolLight2Isabelle -> (Sign0, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HolLight2Isabelle -> HolLightMorphism -> Result IsabelleMorphism Source # map_sentence :: HolLight2Isabelle -> Sign0 -> Sentence0 -> Result Sentence Source # map_symbol :: HolLight2Isabelle -> Sign0 -> () -> Set () Source # extractModel :: HolLight2Isabelle -> Sign0 -> () -> Result (Sign0, [Named Sentence0]) Source # is_model_transportable :: HolLight2Isabelle -> Bool Source # has_model_expansion :: HolLight2Isabelle -> Bool Source # is_weakly_amalgamable :: HolLight2Isabelle -> Bool Source # constituents :: HolLight2Isabelle -> [String] Source # isInclusionComorphism :: HolLight2Isabelle -> Bool Source # rps :: HolLight2Isabelle -> Bool Source # eps :: HolLight2Isabelle -> Bool Source # isGTC :: HolLight2Isabelle -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool 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 #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool 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 #

Orphan instances

GetRange Sentence Source #
Instance details Methods getRange :: Sentence -> Range Source # rangeSpan :: Sentence -> [Pos] Source #