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 (, Section 6. Sharing is achieved by providing suitable locale instances. In your example, there is no sharing (Parameters x and y remain distinct.)



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