Email Gateway (Aug 18 2022 at 18:18): Email Gateway (Aug 18 2022 at 18:18):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
In the following simple script, the Isar proof only works if I fix the types
of
both subtrees, like I did. If I let their types unspecified (like in: fix
x0 and lt0 and rt0) it
gives a type unification error. From the proof state, one can see that it
happens
because the two induction hypothesis are assigned different type variables.
Could anyone elaborate a bit more on that for me?
Many Thanks!
theory newbies_tree_demo
imports Main
begin
datatype 'a Tree = Leaf | Br 'a "'a Tree" "'a Tree"
primrec reflect::"'a Tree => 'a Tree"
where
ref01:"reflect Leaf = Leaf" |
rev02:"reflect (Br label lt rt) = Br label (reflect rt) (reflect lt)"
theorem th_refl01isA: "reflect (reflect t) = t"
proof (induct t)
show "reflect (reflect Leaf) = Leaf" by simp
next
fix x0 and lt0::"'a Tree" and rt0::"'a Tree"
assume IH1: "reflect (reflect lt0) = lt0"
assume IH2: "reflect (reflect rt0) = rt0"
show "reflect (reflect (Br x0 lt0 rt0)) = Br x0 lt0 rt0" by (simp
add:IH1 IH2)
qed
Email Gateway (Aug 18 2022 at 18:18):From: Lawrence Paulson <lp15@cam.ac.uk>
The problem is that the function reflect is polymorphic, and when you simply state the induction hypotheses as you do, there is no reason to assume that the variables have the same types. To eliminate this difficulty, the Isar language includes abbreviations letting you refer to the various inductive cases. Then types are assigned correctly. I suggest writing your proof as follows:
theorem th_refl01isA: "reflect (reflect t) = t"
proof (induct t)
case Leaf
show ?case by simp
next
case (Br x0 lt0 rt0)
thus ?case by simp
qed
Larry Paulson
Email Gateway (Aug 18 2022 at 18:18):From: Alfio Martini <alfio.martini@acm.org>
Dear Lawrence,
Many thanks for the quick and helpful reply!
Best!
Last updated: Apr 24 2024 at 16:18 UTC