{- 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

-}

import Logic.Logic

import Logic.Prover

import Static.DevGraph

{- 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

-}

data 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 = undefined

{- 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 -}

globDecomp :: ProofStatus -> ProofStatus

globDecomp = undefined

{- try to apply rules GlobSubsumption

to all global theorem links in the current DG

current DG = DGm

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

where e1...en are those global theorem links in DGm for which the

rule subsumption can be applied

if n=0, then just return the original proof status

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

globSubsume :: ProofStatus -> ProofStatus

globSubsume = undefined

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

locSubsume :: ProofStatus -> ProofStatus

locSubsume = undefined