Email Gateway (Aug 18 2022 at 19:13): Email Gateway (Aug 18 2022 at 19:13):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
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?
Thank you,
John
Email Gateway (Aug 18 2022 at 19:13):From: Lars Noschinski <noschinl@in.tum.de>
You can do this with:
declare f.induct[case_names name1 name2]
-- Lars
Email Gateway (Aug 18 2022 at 19:13):From: John Wickerson <jpw48@cam.ac.uk>
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<-----------
Email Gateway (Aug 18 2022 at 19:13):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:14):From: John Wickerson <jpw48@cam.ac.uk>
Lovely. Many thanks Lars. For the benefit of future readers, the second statement should have no comma, i.e. it should read:
Last updated: Apr 25 2024 at 12:23 UTC