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



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?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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