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.