# Re: [isabelle] What is the error (simp)?

Your problem is in the following line:
> have c [simp]: "y:B ==> (f O g)`y = f`(g`y)" by auto
This theorem refers to y, a free variable. All the variables (y, B, f, g) in this theorem have fixed meanings. But for your final proof, you need a theorem that holds for all elements of B. You can fix your proof by changing the line as follows:
> have c [simp]: "!!y. y:B ==> (f O g)`y = f`(g`y)" by auto
Larry Paulson
On 19 Dec 2010, at 21:15, Victor Porton wrote:
> The following lemma fails to verify (in ZF). It is strange because (simp) should do the job.
>
> lemma comp_eq_id_iff2:
> "[| g: B->Ag; f: Af->C; Ag<=Af |] ==> (ALL y:B. f`(g`y) = y) <-> f O g = id(B)"
> proof -
> assume "g: B->Ag" "f: Af->C" "Ag<=Af"
> hence "f O g: B->C" by (rule comp_fun2)
> moreover
> have "id(B): B->B" by (rule id_type)
> ultimately have m: "(ALL y:B. (f O g)`y = id(B)`y) <-> f O g = id(B)" by (rule fun_extension_iff)
> from `g: B->Ag` have c [simp]: "y:B ==> (f O g)`y = f`(g`y)" by auto
> have i [simp]: "y:B ==> id(B)`y = y" by auto
> from m show "(ALL y:B. f`(g`y) = y) <-> f O g = id(B)" by simp
> qed
>
> What is my error? What is the right way to do this?

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