Email Gateway (Aug 19 2022 at 13:42): Email Gateway (Aug 19 2022 at 13:42):From: Nick Smallbone <nicsma@chalmers.se>
Hi Isabellers,
I've been playing with the list theory from the Isabelle tutorial and
bumped into something odd. After defining rev and app, and giving a
couple of simplification rules, I can prove the following lemma with
induct and simp:
lemma rev_app_1: "rev (app xs ys) = app (rev ys) (rev xs)"
But not this one:
lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
This seems rather strange to me, because all I've done is flipped the
equation around. I can understand that reorienting a simplification
rule will affect the behaviour of simp, but why does reorienting the
goal make a difference?
Code follows at the end of this message. What have I missed?
Nick (with his confused newbie hat on)
theory Lists
imports Datatype
begin
datatype 'a list = Nil | Cons 'a "'a list"
primrec app :: "'a list => 'a list => 'a list"
where
"app Nil xs = xs" |
"app (Cons x xs) ys = Cons x (app xs ys)"
primrec rev :: "'a list => 'a list"
where
"rev Nil = Nil" |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
(* Two simplification rules *)
lemma app_nil[simp]: "app xs Nil = xs"
apply (induct xs)
apply simp_all
done
lemma app_assoc[simp]: "app (app xs ys) zs = app xs (app ys zs)"
apply (induct xs)
apply simp_all
done
(* This lemma goes through... *)
lemma rev_app_1: "rev (app xs ys) = app (rev ys) (rev xs)"
apply (induct xs)
apply simp_all
done
(* ...but this one doesn't *)
lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
apply (induct xs)
apply simp_all
done
Email Gateway (Aug 19 2022 at 13:43):From: Nick Smallbone <nicsma@chalmers.se>
Thanks for the replies, all. That makes perfect sense now - it's the
orientation of the induction hypothesis that makes the difference.
Nick
Last updated: Apr 25 2024 at 08:20 UTC