*To*: cl-isabelle-users at lists.cam.ac.uk, Dmitriy Traytel <traytel at in.tum.de>*Subject*: Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 16 Nov 2013 17:32:05 +0100*Cc*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <528761A5.8070406@in.tum.de>*Organization*: TU Munich*References*: <52861E13.7090503@inf.ethz.ch> <5287337F.5080402@informatik.tu-muenchen.de> <528761A5.8070406@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

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**

**Follow-Ups**:**Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code***From:*Dmitriy Traytel

**References**:**[isabelle] Proof failed for BNF iterators at code_thms and export_code***From:*Andreas Lochbihler

**Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code***From:*Florian Haftmann

**Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code
- Next by Date: [isabelle] AFP 2013-1 released
- Previous by Thread: Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code
- Next by Thread: Re: [isabelle] Proof failed for BNF iterators at code_thms and export_code
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list