Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The problem restated

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,

• Brian

Quoting Victor Porton <porton@narod.ru>:

Last updated: Nov 21 2024 at 12:39 UTC