[isabelle] The problem restated



In the following theory the theorem ret_th1 verifies well but the theorem ret_th2 fails to verify. How this file could be changed to verify ret_th2 also?

---

theory test
  imports Perm
begin

(*Should be replaced with actual definitions*)
consts big::i
consts newbig::i
consts move::i

theorem move_th: "move: bij(big, newbig)"
  sorry

definition ret_def: "ret == converse(move)"

theorem ret_th1: "converse(move): bij(newbig, big)"
using move_th bij_converse_bij by simp;

theorem ret_th2: "ret: bij(newbig, big)"
using move_th bij_converse_bij by simp;

end





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