*To*: Victor Porton <porton at narod.ru>*Subject*: Re: [isabelle] The problem restated*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 16 Mar 2009 07:34:01 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <748741237116139@webmail10.yandex.ru>*References*: <748741237116139@webmail10.yandex.ru>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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 at narod.ru>:

In the following theory the theorem ret_th1 verifies well but thetheorem ret_th2 fails to verify. How this file could be changed toverify 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

**References**:**[isabelle] The problem restated***From:*Victor Porton

- Previous by Date: Re: [isabelle] Slow rule application in case of many parameters?
- Next by Date: [isabelle] Meta_impE and other tactics
- Previous by Thread: [isabelle] The problem restated
- Next by Thread: [isabelle] How do I find out via "find_theorems", for an existing theorem, whether it is marked as simp/intro/elim?
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list