TheoremHideShift.hs revision c208973c890b8f993297720fd0247bc7481d4304
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : theorem hide shift proof rule for development graphs
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable(Logic)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maedertheorem hide shift proof rule for development graphs
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder T. Mossakowski, S. Autexier and D. Hutter:
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder Extending Development Graphs With Hiding.
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Lecture Notes in Computer Science 2029, p. 269-283,
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Springer-Verlag 2001.
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ( theoremHideShift
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder , theoremHideShiftFromList
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder (thmHideShift, getInComingGlobalUnprovenEdges)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Data.Graph.Inductive.Graph as Graph
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Map as Map
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder------------------------------------------------
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder-- Theorem hide shift and auxiliaries
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder-----------------------------------------------
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedertheoremHideShift :: LibName -> LibEnv -> Result LibEnv
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaedertheoremHideShift ln = return .
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder Map.adjust (\ dg -> theoremHideShiftAux (labNodesDG dg) dg) ln
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder-- | assume that the normal forms a commputed already.
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder-- return Nothing if nothing changed
bab2d88d650448628730ed3b65c9f99c52500e8cChristian MaedertheoremHideShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel MancetheoremHideShiftAux ns dg = let
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder nodesWHiding = map fst $ filter
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maeder (\ (_, lbl) -> labelHasHiding lbl && isJust (dgn_nf lbl)
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder && isJust (dgn_sigma lbl)) ns
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder -- all nodes with incoming hiding links
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder -- all the theorem links entering these nodes
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich -- have to replaced by theorem links with the same origin
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder -- but pointing to the normal form of the former target node
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder ingoingEdges = concatMap (getInComingGlobalUnprovenEdges dg) nodesWHiding
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder in foldl theoremHideShiftForEdge dg ingoingEdges
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedertheoremHideShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian MaedertheoremHideShiftForEdge dg edge@(source, target, edgeLab) =
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder case maybeResult $ theoremHideShiftForEdgeAux dg edge of
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder Nothing -> error "theoremHideShiftForEdgeAux"
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder Just (dg', pbasis) -> let
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder provenEdge = (source, target, edgeLab
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder { dgl_type = setProof (Proven thmHideShift pbasis) $ dgl_type edgeLab
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder , dgl_origin = DGLinkProof
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder , dgl_id = defaultEdgeId })
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder in insertDGLEdge provenEdge $ changeDGH dg' $ DeleteEdge edge
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedertheoremHideShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Result (DGraph, ProofBasis)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedertheoremHideShiftForEdgeAux dg (sn, tn, llab) = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let tlab = labDG dg tn
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Just nfNode = dgn_nf tlab
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder phi = dgl_morphism llab
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just muN = dgn_sigma tlab
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder cmor <- comp phi muN
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder let newEdge =(sn, nfNode, defDGLink cmor globalThm DGLinkProof)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case tryToGetEdge newEdge dg of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Nothing -> let
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder newGraph = changeDGH dg $ InsertEdge newEdge
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder finalEdge = case getLastChange newGraph of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder InsertEdge final_e -> final_e
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder _ -> error "Proofs.Global.globDecompForOneEdgeAux"
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder (newGraph, addEdgeId emptyProofBasis $ getEdgeId finalEdge)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just e -> return (dg, addEdgeId emptyProofBasis $ getEdgeId e)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedertheoremHideShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Result LibEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedertheoremHideShiftFromList ln ls =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return . Map.adjust (theoremHideShiftAux ls) ln