try to eliminate datatype acost

[maxhaslbeck]

Type ('a, 'b) acost is introduced ...

isabelle_llvm_time/thys/basic/kernel/LLVM_Shallow.thy

Line 9 in 55a7e86

datatype ('a, 'b) acost = acostC (the_acost: "'a \<Rightarrow> 'b")

... to wrap functions in order to enable type class lifting of addition for functions in monoid_add ...

isabelle_llvm_time/thys/basic/kernel/LLVM_Shallow.thy

Line 36 in 55a7e86

instantiation acost :: (type, monoid_add) monoid_add

... to not clash with the lifting addition for functions in sep_algebra.

By defining a type class capturing resources which are always disjoint (i.e. x ## y := True), sep_algebra's addition definition can be reused without a clash.
That means monoid_add + "resource algebra" might be sublocale of separation_algebra?