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.