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
interpretation.

You might consider wrapping up you matter in something like

context
begin

interpretation prefix!: L â <proof>

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

end

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

Hope this helps.
	Florian

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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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