| Copyright | (c) Cui Jian Till Mossakowski Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable(Logic) |
| Safe Haskell | None |
Proofs.SimpleTheoremHideShift
Description
simple version of theorem hide shift proof rule for development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual.
Synopsis
- theoremHideShift :: LibName -> LibEnv -> LibEnv
- thmHideShift :: DGRule
- getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab]
Documentation
theoremHideShift :: LibName -> LibEnv -> LibEnv Source #
to be exported function. firstly it gets all the hiding definition links out of DGraph and passes them to theoremHideShiftFromList which does the actual processing
thmHideShift :: DGRule Source #
rule name
getInComingGlobalUnprovenEdges :: DGraph -> Node -> [LEdge DGLinkLab] Source #
get all the global unproven threorem links which go into the given node in the given dgraph