Email Gateway (Aug 18 2022 at 13:09): Email Gateway (Aug 18 2022 at 13:09):From: Victor Porton <porton@narod.ru>
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
Email Gateway (Aug 18 2022 at 13:10):From: Brian Huffman <brianh@cs.pdx.edu>
I think the problem is that you need to unfold the definition of "ret":
theorem ret_th2: "ret: bij(newbig, big)"
unfolding ret_def
using move_th bij_converse_bij by simp
Hope this helps,
Quoting Victor Porton <porton@narod.ru>:
Last updated: May 03 2024 at 12:27 UTC