[isabelle] Curious failure of simp when goal equation is reoriented



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




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