Re: [isabelle] case_names for fun



Lovely. Many thanks Lars. For the benefit of future readers, the second statement should have no comma, i.e. it should read:

>  lemmas my_induct_rule
>     = mk_inner_vertex_inj.induct[case_names name1 name2]


John

On 22 Feb 2012, at 12:54, Lars Noschinski wrote:

> On 22.02.2012 12:27, John Wickerson wrote:
>> Thanks Lars. I actually tried that already, but it doesn't work. Below is a snippet of my theory file. After the last line, Isabelle says 'Unknown case: "name1"'.
> 
> Yes, you are right. The case_names attribute does not modify lemma, but returns a modified lemma. So
> 
>  (induct rule: mk_inner_vertex_inj.induct[case_names name1 name2]
> 
> will work, and
> 
>  lemmas my_induct_rule
>     = mk_inner_vertex_inj.induct[case_names name1, name2]
> 
> will work, too.
> 
>  -- Lars
> 






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