{- HetCATS/Proofs/Proofs.hs

$Id$

Till Mossakowski

Proofs in development graphs.

References:

T. Mossakowski, S. Autexier and D. Hutter:

Extending Development Graphs With Hiding.

H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,

Lecture Notes in Computer Science 2029, p. 269-283,

Springer-Verlag 2001.

T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

CASL Proof calculus. In: CASL reference manual, part IV.

Available from http://www.cofi.info

todo:

Integrate stuff from Saarbr�cken

Add proof status information

what should be in proof status:

- proofs of thm links according to rules

- cons, def and mono annos, and their proofs

-}

module Proofs.Proofs where

import Logic.Logic

import Logic.Prover

import Logic.Grothendieck

import Static.DevGraph

import Common.Lib.Graph

{- proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])

DG0 is the development graph resulting from the static analysis

Ri is a list of rules that transforms DGi-1 to DGi

With the list of intermediate proof states, one can easily implement

an undo operation

-}

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) -- edge in the conclusion

| LocDecompI

| LocDecompII

| GlobSubsumption (LEdge DGLinkLab)

| LocSubsumption (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 -- more detail to be added ...

{- todo: implement apply for GlobDecomp and Subsumption

the list of DGChage must be constructed in parallel to the

new DGraph -}

applyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)

applyRule = error "Proofs.hs:applyRule"

-- ---------------------

-- global decomposition

-- ---------------------

{- apply rule GlobDecomp to all global theorem links in the current DG

current DG = DGm

add to proof status the pair ([GlobDecomp e1,...,GlobDecomp en],DGm+1)

where e1...en are the global theorem links in DGm

DGm+1 results from DGm by application of GlobDecomp e1,...,GlobDecomp en -}

{- applies global decomposition to all unproven global theorem edges

if possible -}

globDecomp :: ProofStatus -> ProofStatus

globDecomp proofStatus@(globalContext,history,dgraph) =

if null (snd newHistoryElem) then proofStatus

else (globalContext, ((newHistoryElem):history), newDgraph)

where

globalThmEdges = filter isUnprovenGlobalThm (labEdges dgraph)

(newDgraph, newHistoryElem) = globDecompAux dgraph globalThmEdges ([],[])

{- auxiliary function for globDecomp (above)

actual implementation -}

globDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule],[DGChange])

-> (DGraph,([DGRule],[DGChange]))

globDecompAux dgraph [] historyElem = (dgraph, historyElem)

globDecompAux dgraph (edge:edges) historyElem =

globDecompAux newDGraph edges newHistoryElem

where

(newDGraph, newChanges) = globDecompForOneEdge dgraph edge

newHistoryElem =

if null newChanges then historyElem

else (((GlobDecomp edge):(fst historyElem)),

(newChanges++(snd historyElem)))

-- applies global decomposition to a single edge

globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph,[DGChange])

globDecompForOneEdge dgraph edge =

globDecompForOneEdgeAux dgraph edge [] paths

where

pathsToSource = getAllLocGlobDefPathsTo dgraph (getSourceNode edge) []

paths = [(node, path++(edge:[]))| (node,path) <- pathsToSource]

{- auxiliary funktion for globDecompForOneEdge (above)

actual implementation -}

globDecompForOneEdgeAux :: DGraph -> LEdge DGLinkLab -> [DGChange] ->

[(Node, [LEdge DGLinkLab])] -> (DGraph,[DGChange])

{- if the list of paths is empty from the beginning, nothing is done

otherwise the unprovenThm edge is replaced by a proven one -}

globDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes [] =

if null changes then (dgraph, [])

else ((insEdge provenEdge (delLEdge edge dgraph)),

((DeleteEdge edge):((InsertEdge provenEdge):changes)))

where

(GlobalThm _ conservativity) = (dgl_type edgeLab)

provenEdge = (source,

target,

DGLink {dgl_morphism = dgl_morphism edgeLab,

dgl_type = (GlobalThm True conservativity),

dgl_origin = DGProof}

)

-- for each path an unproven localThm edge is inserted

globDecompForOneEdgeAux dgraph edge@(source,target,edgeLab) changes

((node,path):list) =

globDecompForOneEdgeAux newGraph edge newChanges list

where

morphism = case calculateMorphismOfPath path of

Just morph -> morph

otherwise ->

error "globDecomp: could not determine morphism of new edge"

(GlobalThm _ conservativity) = (dgl_type edgeLab)

newEdge = (node,

target,

DGLink {dgl_morphism = morphism,

dgl_type = (LocalThm False conservativity),

dgl_origin = DGProof}

)

newGraph = insEdge newEdge dgraph

newChanges = ((InsertEdge newEdge):changes)

-- -------------------

-- global subsumption

-- -------------------

-- applies global subsumption to all unproven global theorem edges if possible

globSubsume :: ProofStatus -> ProofStatus

globSubsume proofStatus@(globalContext,history,dGraph) =

if null (snd nextHistoryElem) then proofStatus

else (globalContext, nextHistoryElem:history, nextDGraph)

where

globalThmEdges = filter isUnprovenGlobalThm (labEdges dGraph)

result = globSubsumeAux dGraph ([],[]) globalThmEdges

nextDGraph = fst result

nextHistoryElem = snd result

{- auxiliary function for globSubsume (above)

the actual implementation -}

globSubsumeAux :: DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]

-> (DGraph,([DGRule],[DGChange]))

globSubsumeAux dGraph historyElement [] = (dGraph, historyElement)

globSubsumeAux dGraph (rules,changes) ((ledge@(source,target,edgeLab)):list) = if existsProvenPathOfMorphismBetween dGraph morphism source target

then

globSubsumeAux newGraph (newRules,newChanges) list

else

globSubsumeAux dGraph (rules,changes) list

where

morphism = dgl_morphism edgeLab

auxGraph = delLEdge ledge dGraph

(GlobalThm _ conservativity) = (dgl_type edgeLab)

newEdge = (source,

target,

DGLink {dgl_morphism = morphism,

dgl_type = (GlobalThm True conservativity),

dgl_origin = DGProof}

)

newGraph = insEdge newEdge auxGraph

newRules = (GlobSubsumption ledge):rules

newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)

-- ------------------

-- local subsumption

-- ------------------

{- the same as globSubsume, but for the rule LocSubsumption -}

-- applies local Subsumption to all unproven localThm edges if possible

locSubsume :: ProofStatus -> ProofStatus

locSubsume proofStatus@(globalContext,history,dGraph) =

if null (snd nextHistoryElem) then proofStatus

else (globalContext, nextHistoryElem:history, nextDGraph)

where

localThmEdges = filter isUnprovenLocalThm (labEdges dGraph)

result = locSubsumeAux dGraph ([],[]) localThmEdges

nextDGraph = fst result

nextHistoryElem = snd result

{- auxiliary function for locSubsume (above)

actual implementation -}

locSubsumeAux :: DGraph -> ([DGRule],[DGChange]) -> [LEdge DGLinkLab]

-> (DGraph,([DGRule],[DGChange]))

locSubsumeAux dgraph historyElement [] = (dgraph, historyElement)

locSubsumeAux dgraph (rules,changes) ((ledge@(source,target,edgeLab)):list) =

if existsLocGlobDefPathOfMorphismBetween dgraph morphism source target

then

globSubsumeAux newGraph (newRules,newChanges) list

else

globSubsumeAux dgraph (rules,changes) list

where

morphism = dgl_morphism edgeLab

auxGraph = delLEdge ledge dgraph

(LocalThm _ conservativity) = (dgl_type edgeLab)

newEdge = (source,

target,

DGLink {dgl_morphism = morphism,

dgl_type = (LocalThm True conservativity),

dgl_origin = DGProof}

)

newGraph = insEdge newEdge auxGraph

newRules = (LocSubsumption ledge):rules

newChanges = (DeleteEdge ledge):((InsertEdge newEdge):changes)

-- -----------------------------------------------------------------------

-- methods that check if paths of certain types exist between given nodes

-- -----------------------------------------------------------------------

{- checks if there is a path of globalDef edges or proven globalThm edges

with the given morphism between the given source and target node -}

existsProvenPathOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node

-> Bool

existsProvenPathOfMorphismBetween dgraph morphism src tgt =

-- @@@ zum Testen: not (null (concat allDefPathsBetween))

elem morphism filteredMorphismsOfProvenPaths

where

allPaths = getAllProvenPathsBetween dgraph src tgt

([]::[LEdge DGLinkLab])

morphismsOfPaths = map calculateMorphismOfPath allPaths

filteredMorphismsOfProvenPaths = getFilteredMorphisms morphismsOfPaths

{- checks if a path consisting of globalDef edges only

or consisting of a localDef edge followed by any number of globalDef edges

exists between the given nodes -}

existsLocGlobDefPathOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node

-> Bool

existsLocGlobDefPathOfMorphismBetween dgraph morphism src tgt =

elem morphism filteredMorphismsOfLocGlobDefPaths

where

allPaths = getAllLocGlobDefPathsBetween dgraph src tgt

morphismsOfPaths =

map calculateMorphismOfPath allPaths

filteredMorphismsOfLocGlobDefPaths =

getFilteredMorphisms morphismsOfPaths

-- ----------------------------------------------

-- methods that calculate paths of certain types

-- ----------------------------------------------

-- @@@ this method is not used at the momen!! @@@

{- returns a list of all paths to the given node

that consist of globalDef edges or proven global theorems only

or

that consist of a localDef/proven local theorem edge followed by

any number of globalDef/proven global theorem edges -}

getAllProvenLocGlobPathsTo :: DGraph -> Node -> [LEdge DGLinkLab]

-> [(Node, [LEdge DGLinkLab])]

getAllProvenLocGlobPathsTo dgraph node path =

(node,path):(locGlobPaths ++

(concat (

[getAllProvenLocGlobPathsTo dgraph (getSourceNode edge) path|

(_, path@(edge:edges)) <- globalPaths]))

)

where

inEdges = inn dgraph node

globalEdges = (filter isGlobalDef inEdges)

++ (filter isProvenGlobalThm inEdges)

localEdges = (filter isLocalDef inEdges)

++ (filter isProvenLocalThm inEdges)

globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]

locGlobPaths = [(getSourceNode edge, (edge:path))| edge <- localEdges]

{- returns a list of all paths to the given node

that consist of globalDef edges only

or

that consist of a localDef edge followed by any number of globalDef edges -}

getAllLocGlobDefPathsTo :: DGraph -> Node -> [LEdge DGLinkLab]

-> [(Node, [LEdge DGLinkLab])]

getAllLocGlobDefPathsTo dgraph node path =

(node,path):(locGlobPaths ++

(concat (

[getAllLocGlobDefPathsTo dgraph (getSourceNode edge) path|

(_, path@(edge:edges)) <- globalPaths]))

)

where

inEdges = inn dgraph node

globalEdges = filter isGlobalDef inEdges

localEdges = filter isLocalDef inEdges

globalPaths = [(getSourceNode edge, (edge:path))| edge <- globalEdges]

locGlobPaths = [(getSourceNode edge, (edge:path))| edge <- localEdges]

{- returns all paths of globalDef edges or proven globalThm edges

between the given source and target node -}

getAllProvenPathsBetween :: DGraph -> Node -> Node -> [LEdge DGLinkLab]

-> [[LEdge DGLinkLab]]

getAllProvenPathsBetween dgraph src tgt path =

getAllPathsOfTypesBetween dgraph [isGlobalDef,isProvenGlobalThm] src tgt []

{- returns all paths of globalDef edges between the given source and

target node -}

getAllDefPathsBetween :: DGraph -> Node -> Node -> [LEdge DGLinkLab]

-> [[LEdge DGLinkLab]]

getAllDefPathsBetween dgraph src tgt path =

getAllPathsOfTypeBetween dgraph isGlobalDef src tgt

{- returns all paths consiting of edges of the given type between the

given node -}

getAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node

-> Node -> [[LEdge DGLinkLab]]

getAllPathsOfTypeBetween dgraph isType src tgt =

getAllPathsOfTypesBetween dgraph (isType:[]) src tgt []

{- returns all paths consisting of edges of the given types between

the given nodes -}

getAllPathsOfTypesBetween :: DGraph -> [LEdge DGLinkLab -> Bool] -> Node

-> Node -> [LEdge DGLinkLab]

-> [[LEdge DGLinkLab]]

getAllPathsOfTypesBetween dgraph types src tgt path =

[edge:path| edge <- edgesFromSrc]

++ (concat

[getAllPathsOfTypesBetween dgraph types src nextTgt (edge:path)|

(edge,nextTgt) <- nextStep] )

where

inGoingEdges = inn dgraph tgt

edgesOfTypes = filterByTypes types inGoingEdges

edgesFromSrc =

[edge| edge@(source,_,_) <- edgesOfTypes, source == src]

nextStep =

[(edge, source)| edge@(source,_,_) <- edgesOfTypes, source /= src]

{- returns a list of all paths between the given nodes

that consist only of globalDef edges

or

that consist of a localDef edge followed by any number of globalDef edges -}

getAllLocGlobDefPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]]

getAllLocGlobDefPathsBetween dgraph src tgt = globDefPaths ++ locGlobDefPaths

where

globDefPaths = getAllDefPathsBetween dgraph src tgt ([]::[LEdge DGLinkLab])

outEdges = out dgraph src

nextStep = [(edge,getTargetNode edge) | edge <- outEdges]

pathEnds =

[(edge,getAllDefPathsBetween dgraph node tgt ([]::[LEdge DGLinkLab]))|

(edge, node) <- nextStep]

locGlobDefPaths =

concat [addToAll edge paths | (edge, paths) <- pathEnds]

-- adds the given element at the front of all lists in the given list

addToAll :: a -> [[a]] -> [[a]]

addToAll _ [] = []

addToAll element (list:lists) = (element:list):(addToAll element lists)

-- removes all edges that are not of the given types

filterByTypes :: [LEdge DGLinkLab -> Bool] -> [LEdge DGLinkLab]

-> [LEdge DGLinkLab]

filterByTypes [] edges = edges

filterByTypes (isType:typeChecks) edges =

(filter isType edges)++(filterByTypes typeChecks edges)

-- --------------------------------------

-- methods to determine or get morphisms

-- --------------------------------------

-- determines the morphism of a given path

calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism

calculateMorphismOfPath [] = error "getMorphismOfPath: empty path"

calculateMorphismOfPath path@((src,tgt,edgeLab):furtherPath) =

case maybeMorphismOfFurtherPath of

Nothing -> Nothing

Just morphismOfFurtherPath ->

comp Grothendieck morphism morphismOfFurtherPath

where

morphism = dgl_morphism edgeLab

maybeMorphismOfFurtherPath = calculateMorphismOfPath furtherPath

{- removes the "Nothing"s from a list of Maybe GMorphism

returns the remaining elements as plain GMorphisms -}

getFilteredMorphisms :: [Maybe GMorphism] -> [GMorphism]

getFilteredMorphisms morphisms =

[morph| (Just morph) <- filter isValidMorphism morphisms]

-- returns True if the given Maybe GMorphisms is not "Nothing"

isValidMorphism :: Maybe GMorphism -> Bool

isValidMorphism morphism =

case morphism of

Nothing -> False

otherwise -> True

-- ------------------------------------

-- methods to get the nodes of an edge

-- ------------------------------------

getSourceNode :: LEdge DGLinkLab -> Node

getSourceNode (source,_,_) = source

getTargetNode :: LEdge DGLinkLab -> Node

getTargetNode (_,target,_) = target

-- -------------------------------------

-- methods to check the type of an edge

-- -------------------------------------

isProvenGlobalThm :: LEdge DGLinkLab -> Bool

isProvenGlobalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(GlobalThm True _) -> True

otherwise -> False

isUnprovenGlobalThm :: LEdge DGLinkLab -> Bool

isUnprovenGlobalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(GlobalThm False _) -> True

otherwise -> False

isProvenLocalThm :: LEdge DGLinkLab -> Bool

isProvenLocalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(LocalThm True _) -> True

otherwise -> False

isUnprovenLocalThm :: LEdge DGLinkLab -> Bool

isUnprovenLocalThm (_,_,edgeLab) =

case dgl_type edgeLab of

(LocalThm False _) -> True

otherwise -> False

isGlobalDef :: LEdge DGLinkLab -> Bool

isGlobalDef (_,_,edgeLab) =

case dgl_type edgeLab of

GlobalDef -> True

otherwise -> False

isLocalDef :: LEdge DGLinkLab -> Bool

isLocalDef (_,_,edgeLab) =

case dgl_type edgeLab of

LocalDef -> True

otherwise -> False