[isabelle] Combining Locales and specializing types



I have two locales:
 locale A =
   fixes f :: "'a => 'b"

 locale B =
   fixes g :: "'b => bool"

Now I want to combine these two, so that the types 'b in A and B are the same.
The approach:
 locale C = A + B
 lemma (in C) "g (f a)"
gives a type error when trying to type the lemma.

I'm currently using the dirty-hack:
 locale C = A + B +
   assumes "False => g (f a)"

 lemma (in C) "g (f a)"

this works but looks not clean.

Is there any cleaner way to do that ?


Thanks for any help in advance Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.