Re: [isabelle] Case names qualified by locale



On 03.09.2015 12:20, Christoph Dittmann wrote:
> Hi,
> 
> 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, 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




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