*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Why does "also" fail in this proof?*From*: Robin Green <greenrd at greenrd.org>*Date*: Sun, 07 May 2006 12:11:26 +0100*Organization*: Systems Research Group, University College Dublin

I'm using Isabelle 2005, and I've picked up how to do some calculational proofs in a "monkey-see, monkey-do" kind of way - i.e. not really understanding the connecting commands like "also" and "have" and "show". Can someone explain why, in the attached theory file, I get this error on the last line: *** empty result sequence -- proof command failed *** At command "also". Previously when I hit this error, I found that I could delete the previous line in the proof and the error would go away. But in this case, if I delete the previous line, the combined step is too hard for Isabelle to do in one step, as far as I can see. -- Robin

theory Functor imports Main begin constdefs const :: "'a => 'b => 'a" "const x y == x" theorem comp_id [simp]: "comp id == id" proof - have "comp id == %g x. (id o g) x" . also have "... == %g x. id (g x)" by simp also have "... == %g x. g x" by simp also have "... == id" by (simp only: id_def) finally show "comp id == id" . qed theorem comp_comp [simp]: "comp (f o g) == (comp f) o (comp g)" proof - have "comp (f o g) == %h y. ((f o g) o h) y" . also have "... == %h y. (f o g o h) y" by simp also have "... == %h y. ((comp f) ((comp g) h)) y" by simp also have "... == %h y. ((comp f) o (comp g)) h y" by simp finally show "comp (comp f g) == comp (comp f) (comp g)" . qed constdefs rpipe2 :: "['b => 'c, 'a => 'a1 => 'b, 'a, 'a1] => 'c" "rpipe2 == comp o comp" rpipe3 :: "['b => 'c, 'a => 'a1 => 'a2 => 'b, 'a, 'a1, 'a2] => 'c" "rpipe3 == rpipe2 o comp" apBoth :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" "apBoth f g x == (f x, g x)" tt :: "['c => 'a => 'b, 'c => 'a, 'c] => 'b" "tt == rpipe3 (split id) apBoth" lemma rpipe3_simp [simp]: "rpipe3 f g x y z == f (g x y z)" proof - have "rpipe3 f g x y z == (rpipe2 o comp) f g x y z" by (unfold rpipe3_def) also have "... == ((comp o comp) o comp) f g x y z" by (unfold rpipe2_def) also have "... == (comp (comp (comp f))) g x y z" by simp also have "... == f (g x y z)" by simp finally show "rpipe3 f g x y z == f (g x y z)" . qed lemma tt_simp [simp]: "tt f g x == f x (g x)" proof - have "tt f g x == rpipe3 (split id) apBoth f g x" by (unfold tt_def) also have "... == split id (apBoth f g x)" by simp also have "... == split id (f x, g x)" by (unfold apBoth_def) also have "... == f x (g x)" by simp finally show "tt f g x == f x (g x)" . qed theorem tt_o_const [simp]: "tt o const == comp" proof - have "tt o const == %f g x. (tt o const) f g x" . also have "... == %f g x. tt (const f) g x" by simp also have "... == %f g x. (const f) x (g x)" by simp also have "... == %f g x. f (g x)" by (unfold const_def) also have "... == %f g. comp f g" by (unfold o_def) finally show "tt o const == comp" . qed theorem "tt (const id) == id" proof - have "tt (const id) == (tt o const) id" by (unfold o_def) also have "... == comp id" by simp also have "... == id" by simp finally show "tt (const id) == id" . qed theorem "tt (tt (comp comp u) v) w == tt u (tt v w)" proof - have "tt (tt (comp comp u) v) w == tt (tt (comp o u) v) w" . also have "... == tt (tt (%x. comp (u x)) v) w" by (unfold o_def) also have "... == tt (%y. (%x. comp (u x)) y (v y)) w" .

**Follow-Ups**:**Re: [isabelle] Why does "also" fail in this proof?***From:*Makarius

- Previous by Date: [isabelle] Announcement and CFP: Workshop Proofs & Numbers 12-13/06 in Orsay
- Next by Date: Re: [isabelle] Why does "also" fail in this proof?
- Previous by Thread: [isabelle] Announcement and CFP: Workshop Proofs & Numbers 12-13/06 in Orsay
- Next by Thread: Re: [isabelle] Why does "also" fail in this proof?
- Cl-isabelle-users May 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list