| Copyright | (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable(DevGraph) |
| Safe Haskell | None |
Proofs.Global
Description
global proof rules for development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual.
- globSubsume :: LibName -> LibEnv -> LibEnv
- globDecomp :: LibName -> LibEnv -> LibEnv
- globDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph
- globDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
- globSubsumeFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
Documentation
globSubsume :: LibName -> LibEnv -> LibEnv
tries to apply global subsumption to all unproven global theorem edges
globDecomp :: LibName -> LibEnv -> LibEnv
globDecompAux :: DGraph -> LEdge DGLinkLab -> DGraph
globDecompFromList :: LibName -> [LEdge DGLinkLab] -> LibEnv -> LibEnv
applies global decomposition to the list of edges given (global theorem edges) if possible, if empty list is given then to all unproven global theorems. Notice: (for ticket 5, which solves the problem across library border) 1. before the actual global decomposition is applied, the whole DGraph is updated firstly by calling the function updateDGraph. 2. The changes of the update action should be added as the head of the history.