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




On 03/02/2014 16:29, Nick Smallbone wrote:
> 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?

Because you are doing an induction, and the IH is your original goal, and the IH
is used as a rewrite rule in your proof.

Tobias

> 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.