[isabelle] computation_check with "let ... in ..."



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
Description: Message signed with OpenPGP



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