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

Contents

Description

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

Documentation

data Isabelle Source #

Constructors

Isabelle 

Instances

Show Isabelle Source # 

Methods

showsPrec :: Int -> Isabelle -> ShowS

show :: Isabelle -> String

showList :: [Isabelle] -> ShowS

Language Isabelle Source # 

Methods

language_name :: Isabelle -> String Source #

description :: Isabelle -> String Source #

Sentences Isabelle Sentence Sign IsabelleMorphism () Source # 
Syntax Isabelle () () () () Source # 

Methods

parsersAndPrinters :: Isabelle -> Map String (PrefixMap -> AParser st (), () -> Doc) Source #

parse_basic_spec :: Isabelle -> Maybe (PrefixMap -> AParser st ()) Source #

parseSingleSymbItem :: Isabelle -> Maybe (AParser st ()) Source #

parse_symb_items :: Isabelle -> Maybe (AParser st ()) Source #

parse_symb_map_items :: Isabelle -> Maybe (AParser st ()) Source #

toItem :: Isabelle -> () -> Item Source #

symb_items_name :: Isabelle -> () -> [String] Source #

StaticAnalysis Isabelle () Sentence () () Sign IsabelleMorphism () () Source # 

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 # 

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 # 

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 #

Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Orphan instances