Hets - the Heterogeneous Tool Set

Copyright(c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(DevGraph)
Safe HaskellNone

Proofs.Global

Description

global proof rules for development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual.

Synopsis

Documentation

globSubsume :: LibName -> LibEnv -> LibEnv

tries to apply global subsumption to all unproven global theorem edges

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.