hets -- a heterogenous Specification (CASL) tool setContentsIndex
Proofs.Proofs
Portability non-portable(Logic)
Stability provisional
Maintainer hets@tzi.de
Description
Proofs in development graphs.
Synopsis
type ProofStatus = (GlobalContext, [([DGRule], [DGChange])], DGraph)
data DGRule
= TheoremHideShift
| HideTheoremShift
| Borrowing
| ConsShift
| DefShift
| MonoShift
| ConsComp
| DefComp
| MonoComp
| DefToMono
| MonoToCons
| FreeIsMono
| MonoIsFree
| Composition
| GlobDecomp (LEdge DGLinkLab)
| LocDecomp (LEdge DGLinkLab)
| GlobSubsumption (LEdge DGLinkLab)
| LocalInference
| BasicInference Edge BasicProof
| BasicConsInference Edge BasicConsProof
data DGChange
= InsertNode (LNode DGNodeLab)
| DeleteNode Node
| InsertEdge (LEdge DGLinkLab)
| DeleteEdge (LEdge DGLinkLab)
data BasicProof
= forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => BasicProof lid (Proof_status sentence proof_tree)
| Guessed
| Conjectured
| Handwritten
data BasicConsProof = BasicConsProof
applyRule :: DGRule -> DGraph -> Maybe ([DGChange], DGraph)
globDecomp :: ProofStatus -> ProofStatus
globDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule], [DGChange]) -> (DGraph, ([DGRule], [DGChange]))
globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph, [DGChange])
globDecompForOneEdgeAux :: DGraph -> LEdge DGLinkLab -> [DGChange] -> [(Node, [LEdge DGLinkLab])] -> (DGraph, [DGChange])
globSubsume :: ProofStatus -> ProofStatus
globSubsumeAux :: DGraph -> ([DGRule], [DGChange]) -> [LEdge DGLinkLab] -> (DGraph, ([DGRule], [DGChange]))
getLabelOfEdge :: LEdge b -> b
locDecomp :: ProofStatus -> ProofStatus
locDecompAux :: DGraph -> ([DGRule], [DGChange]) -> [LEdge DGLinkLab] -> (DGraph, ([DGRule], [DGChange]))
getAllGlobPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node -> [[LEdge DGLinkLab]]
filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
getAllLocGlobDefPathsTo :: DGraph -> Node -> [LEdge DGLinkLab] -> [(Node, [LEdge DGLinkLab])]
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllThmDefPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node -> [[LEdge DGLinkLab]]
getAllGlobDefPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]]
getAllPathsOfTypesBetween :: DGraph -> [LEdge DGLinkLab -> Bool] -> Node -> Node -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]]
filterByTypes :: [LEdge DGLinkLab -> Bool] -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism
getSourceNode :: LEdge DGLinkLab -> Node
isProven :: LEdge DGLinkLab -> Bool
isGlobalThm :: LEdge DGLinkLab -> Bool
isProvenGlobalThm :: LEdge DGLinkLab -> Bool
isUnprovenGlobalThm :: LEdge DGLinkLab -> Bool
isProvenLocalThm :: LEdge DGLinkLab -> Bool
isUnprovenLocalThm :: LEdge DGLinkLab -> Bool
isGlobalDef :: LEdge DGLinkLab -> Bool
isLocalDef :: LEdge DGLinkLab -> Bool
getLabelOfAnyInsertedEdge :: [DGChange] -> Maybe DGLinkLab
getInsertedEdges :: [DGChange] -> [LEdge DGLinkLab]
selectProofBasis :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab]
selectProofBasisAux :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab]
calculateProofBasis :: [LEdge DGLinkLab] -> [DGLinkLab]
getProofBasis :: DGLinkLab -> [DGLinkLab]
filterProvenPaths :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
notProofCycle :: DGLinkLab -> [LEdge DGLinkLab] -> Bool
isProofCycle :: DGLinkLab -> [LEdge DGLinkLab] -> Bool
elemOfProofBasis :: DGLinkLab -> LEdge DGLinkLab -> Bool
Produced by Haddock version 0.6