search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

Axioms from unit, assoc, comm annotations are not exported from HasCASL specs to Isabelle #692

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by ewaryst and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/692

Consider the spec

logic HasCASL

spec Monoid = 
     sort Elem
     ops  e:Elem;
          __ * __: Elem * Elem -> Elem, comm, assoc, unit e
end

spec Group =
     Monoid
then
     op inv:Elem->Elem

     forall x: Elem
     . inv(x) * x = e   %(inv_Group)%
then %implies
     forall x: Elem
     . x * inv(x) = e   %(rinv_Group)%
end

When the proof-obligation is tackled in Isabelle, the axioms following from the annotations of the *-op in the spec Monoid are missing in the thy-file.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/692#comment:1

It's not a translation problem. No sentences are generated within the HasCASL static analysis