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.