Re: [isabelle] Case names qualified by locale

>> I like how I can use a named case for coinduction, where P is a
>> coinductive predicate:
>> lemma "P n"
>> proof (coinduction rule: P.coinduct)
>>   case P show ?case sorry
>> qed
>> This works fine.
>> However, suppose P is inside a locale L.  Sometimes I need coinduction
>> over L.P:
>> lemma "L.P n"
>> proof (coinduction rule: L.P.coinduct)
>>   case P show ?case sorry
>> qed
> I don't know why the case names are lost here

The case names are not ÂlostÂ.  L.P is a opaque foundational constant,
and the corresponding declarations are applied only in resulting
contexts, i. e. in the context of the locale itself or due to

You might consider wrapping up you matter in something like


interpretation prefix!: L â <proof>

lemma â
proof (coinduction rule: prefix.P.coinduct)
  case P â


which will give you the full declarations from L inside a certain block.

Hope this helps.

but you should be able to
> use the names by using
>   L.P.coinduct[case_names P Q R]
> or maybe
>   L.P.coinduct[consumes 1, case_names P Q R]
> as a workaround.
>   -- Lars


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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