Re: [isabelle] Variable sharing



Hi John,

locale loc1 =
fixes x::real
assumes "x < 2"

locale loc2 =
fixes y::real
assumes "y < 3"

is there a way to define a proof goal for showing EX x. x < 2 in loc1 *and* EX x. x < y in loc2 (as one proof goal)? Does this require some form of variable sharing?

You need to define a context (ie locale) that inherits from both. This can be achieved with locale expressions. I recommend reading the tutorial (http://isabelle.in.tum.de/dist/Isabelle/doc/locales.pdf), Section 6. Sharing is achieved by providing suitable locale instances. In your example, there is no sharing (Parameters x and y remain distinct.)

Cheers,

Clemens






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