Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code



Am 16.11.2013 09:57, schrieb Florian Haftmann:
Hi Andreas,

theory Scratch imports "~~/src/HOL/BNF/BNF" begin
codatatype foo = Foo | Bar foo
code_datatype Foo Bar
code_thms foo_unfold

At code_thms, I get "Proof failed." and a huge goal state talking about
the internal BNF construction for the the foo instead of the usual list
of theorems that I would like to inspect. The same happens at
export_code and value [code].
I did not inspect the code, but I guess it happens since internal proofs
are forked, which are only forced when the code generator is invoked.
Maybe the BNF gurus can tell you more.
That would imply that with

ML {* parallel_proofs := 0 *}

the error should occur at the codatatype command already. This is not the case.

After some minimization it turns out that this has nothing to do with codatatypes at all:

consts c :: "nat ⇒ bool"
consts b :: "bool"
definition "X = {(Kl :: nat set, lab) |Kl lab. ((∀kl∈Kl. b) ∧ (∀kl. kl ∉ Kl ⟶ b)) ∧ c lab}"
code_thms X

What is code_thms actually trying to prove?

Dmitriy





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