Hets - the Heterogeneous Tool Set
Copyright(c) Till Mossakowski Uni Bremen 2002-2004
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic)
Safe HaskellNone

Isabelle.Logic_Isabelle

Description

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

Documentation

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

Syntax Isabelle () () () () Source # 
Instance details

Defined in Isabelle.Logic_Isabelle

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

Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.MonadicHasCASLTranslation

Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.HolLight2Isabelle

Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.HasCASL2IsabelleHOL

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

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

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

Orphan instances

GetRange Sentence Source # 
Instance details