*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] computation_check with "let ... in ..."*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Tue, 20 Feb 2018 21:00:45 +0000

Dear code generation experts, I was wondering how can we computation_check a term with the form “let … in …”. Here is a small example: given a proposition that can be proved by evalutaion (i.e., by eval or by by code_simp), lemma "let x ::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]” I want to solve it using the computation_check mechanic. If I unfold the “let” constant first, the proposition can be proved like the following: ML ‹ val holds = @{computation_check terms: Trueprop "times::int poly ⇒ _" "HOL.equal ::int poly ⇒ _" "0 :: int poly" "pCons :: int ⇒ _" "0 :: int" "1 :: int" Code_Target_Int.positive datatypes:num }; › lemma "let x::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]" unfolding Let_def apply (tactic ‹ CONVERSION (holds @{context}) 1 ›) by (rule TrueI) However, without the unfolding (i.e., remove “unfolding Let_def”), "apply (tactic ‹CONVERSION (holds@{context}) 1›)” will get stuck. I am not sure if there is any other constant I should add to “@{computation_check terms: ... };" to make the CONVERSION work. Thanks in advance, Wenda

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] computation_check with "let ... in ..."***From:*Thiemann, Rene

- Previous by Date: Re: [isabelle] Proof of concept: BNF-based records
- Next by Date: Re: [isabelle] computation_check with "let ... in ..."
- Previous by Thread: [isabelle] CfP: 4PAD 2018 - 5th International Symposium on Formal Approaches to Parallel and Distributed Systems
- Next by Thread: Re: [isabelle] computation_check with "let ... in ..."
- Cl-isabelle-users February 2018 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