keep structure when calling provers

[till]

Try to keep as much development graph resp. theory structure as possible when calling a prover. There are (at least) the following types of provers:

• provers supporting all CASL constructs. Then keep all the structure
• provers supporting hiding and renaming, but not free. Then transform away free, using special dg rules
• provers supporting renaming, but neither free nor hiding. Then transform away free, using special dg rules, and hiding, using normalization (i.e. shifting hiding to one single hiding at the top level)
• provers supporting theory inclusions only. Then also renaming has to be transformed away
• prover supporting flat theories only. Then proceed as before the implementation of this ticket.

Beware that these transformations interact with comorphisms. Properties of comorphisms are required for some transformations.

Also, take care of the problem that a theory Th1 may be coded differently (just because it is simpler) than its extension Th2, resulting in coded theories CTh1 and CTh2 that are based on different comorphisms. Ensure that CTh2 is not built from scratch, but as an extension of CTh1.

See also #137 and #508.

[maeder]

Summarizing the current state:

• CASL can be transformed to theory inclusions only, qualified, and translated to VSE.
• the node menu "Prove Structured" calls VSE with the corresponding specifications and (plain) links.
• example source:/trunk/VSE/test/Imports.casl

Missing features:

• currently only the CASL2VSE comorphism is supported, it should be possible to (automatically) choose an appropriate comorphism as happens for the "Prove" node menu (i.e. for coding out subsorts or partiality)
• the menus "Prove" and "Prove Structured" should be unified by generalization. Currently only the node is updated from which the prover was called, but other nodes should be updated, too, if the structured prover proofs corresponding lemmas (i.e. of imported nodes).
• the logic VSE misses qualification methods that are needed to directly work on VSE. Since VSE is an extension of CASL this should be easier than ticket #602
• for Isabelle also a structured prover needs to be set up.
• there are a couple of bugs or missing optimizations when flattening development graphs (#508)

[maeder]

Replying to maeder:

Missing features:

[...]

* the logic VSE misses qualification methods that are needed to directly work on VSE. Since VSE is an extension of CASL this should be easier than ticket #602

This feature was implemented in changeset:11338 and changeset:11340

[maeder]

I'm waiting for theorem links to be supported by hetsvse so that

hets -g VSE/test/rll.het

works after Edit->Proofs->Flattening->Heterogeneity on the node "list_impl" using "Prove VSE Structured"