# Re: [isabelle] case_names for fun

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"'.
--------8<-----------
fun mk_inner_vertex_inj :: "inner_vertex list \<Rightarrow> inner_vertex list \<Rightarrow> (inner_vertex \<Rightarrow> inner_vertex)"
where
"mk_inner_vertex_inj [] X = id"
| "mk_inner_vertex_inj (i#I) X = (
let J = (mk_inner_vertex_inj I X) in
let j = (SOME j. j \<notin> image J (set I) \<and> j \<notin> set X) in
J (i := j))"
declare mk_inner_vertex_inj.induct[case_names name1 name2]
lemma "inj_on (mk_inner_vertex_inj I X) (set I)"
proof (intro inj_onI)
fix a b
assume "a \<in> set I"
and "b \<in> set I"
and "mk_inner_vertex_inj I X a = mk_inner_vertex_inj I X b"
thus "a=b"
proof (induct rule: mk_inner_vertex_inj.induct)
case (name1 X)
--------8<-----------
On 22 Feb 2012, at 11:19, Lars Noschinski wrote:
> On 22.02.2012 12:09, John Wickerson wrote:
>> I have a function f defined recursively using "fun". When I do induction using f.induct, the case names are "1" and "2". How can I set them to more useful names?
>
> You can do this with:
>
> declare f.induct[case_names name1 name2]
>
> -- Lars
>

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