[isabelle] What is the error (simp)?



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?

-- 
Victor Porton - http://portonvictor.org





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