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

```Am 16.11.2013 17:32, schrieb Florian Haftmann:
```
```On 16.11.2013 13:14, Dmitriy Traytel wrote:
```
```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?
```
```Interesting.  The code generator internally only does rewriting and
instantiation, no backward proofs, except for case certificates
(Pure/Isar/code.ML):

```
```fun case_cong thy case_const (num_args, (pos, _)) =
let
val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
val Ts = binder_types T;
val T_cong = nth Ts pos;
fun mk_prem z = Free (z, T_cong);
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end;
```
```But this should hold regardless of the logical properties of the case
combinator.

Have you tried to obtain a traceback?

```
I tried to do it now (see below). It points to the set_comprehension_simproc that is installed as a code preprocessor in Product_Type:
```
setup {*
Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
```
[Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [ at {cpat "Collect ?P"}],
```    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
*}

Dmitriy

Exception trace - Proof failed.
```
1. \<And>a ba aa baa. (aa, baa) \<in> (\<lambda>Kl. Kl) ` (\<lambda>Kl. Kl) ` {Kl. \<forall>kl\<in>Kl. b} \<times> UNIV \<inter> (\<lambda>Kl. Kl) ` (\<lambda>Kl. Kl) ` {Kl. \<forall>kl. kl \<notin> Kl \<longrightarrow> b} \<times> UNIV \<inter> UNIV \<times> (\<lambda>lab. lab) ` Collect c \<Longrightarrow> c baa
```The error(s) above occurred for the goal statement:
```
{(Kl, lab) |Kl lab. ((\<forall>kl\<in>Kl. b) \<and> (\<forall>kl. kl \<notin> Kl \<longrightarrow> b)) \<and> c lab} = (\<lambda>(Kl, lab). (Kl, lab)) ` ((\<lambda>Kl. Kl) ` (\<lambda>Kl. Kl) ` {Kl. \<forall>kl\<in>Kl. b} \<times> UNIV \<inter> (\<lambda>Kl. Kl) ` (\<lambda>Kl. Kl) ` {Kl. \<forall>kl. kl \<notin> Kl \<longrightarrow> b} \<times> UNIV \<inter> UNIV \<times> (\<lambda>lab. lab) ` {lab. c lab})
``` (line 10 of "/home/traytel/Scratch3.thy")
Goal.prove_common(7)result(1)
Goal.prove_common(7)
Set_Comprehension_Pointfree.conv(2)
Set_Comprehension_Pointfree.code_simproc(2)
Raw_Simplifier.rewritec(4)proc_rews(1)
Raw_Simplifier.rewritec(4)
Raw_Simplifier.bottomc(3)botc(3)
Raw_Simplifier.bottomc(3)try_botc(1)(1)
Code.eqn_conv(2)
Conv.fconv_rule(2)
List.map(2)()
Library.singleton(1)(1)
List.map(2)()
Basics.#>(1)(1)
Code_Preproc.obtain_eqns(3)
Code_Preproc.ensure_fun(5)
Code_Preproc.extend_arities_eqngr(5)
Code_Thingol.code_depgr(2)
Code_Thingol.code_thms(1)
Toplevel.apply_tr(3)(1)

```

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