[isabelle-dev] Issue in AFP

[Tobias Nipkow]

I added two useful simp rules that broke (= mostly shortened) a number of 
proofs. I'll fix the slow sessions over the next few days - they are a bit of a 
challenge.

Tobias

On 18/06/2017 20:38, Florian Haftmann wrote:
>> isabelle: 20304512a33b tip
>> afp: 644957b424ee tip
>> JinjaThreads FAILED
>> (see also /srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
>> ***                            (\<forall>T.
>> ***                                typeof\<^bsub>h\<^esub> v =
>> ***                                \<lfloor>T\<rfloor> \<longrightarrow>
>> ***                                (\<forall>C.
>> ***                                    class_type_of' T =
>> ***                                    \<lfloor>C\<rfloor> \<longrightarrow>
>> ***                                    (\<forall>Ts Tr D.
>> ***  P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow>
>> ***  \<tau>external_defs D M))))
>> ***                        then (\<tau>red0t (extTA2J0 P) P t h
>> ***                               (Val v\<bullet>M(es), xs)
>> ***                               (Val v\<bullet>M(es'), xs') \<or>
>> ***                              countInitBlock (Val v\<bullet>M(es1'))
>> ***                              < countInitBlock (Val v\<bullet>M(es1)) \<and>
>> ***                              Val v\<bullet>M(es') =
>> ***                              Val v\<bullet>M(es) \<and>
>> ***                              xs' = xs) \<and>
>> ***                             h' = h \<and>
>> ***                             ta1 = \<lbrace>\<rbrace> \<and>
>> ***                             ta = \<lbrace>\<rbrace>
>> ***                        else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and>
>> ***                             (if call (Val v\<bullet>M(es)) = None \<or>
>> ***                                 call1 (Val v\<bullet>M(es1)) = None
>> ***                              then \<exists>e'' xs''.
>> ***                                      \<tau>red0r (extTA2J0 P) P t h
>> *** (Val v\<bullet>M(es), xs) (e'', xs'') \<and>
>> ***                                      extTA2J0
>> *** P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow>
>> ***                    \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and>
>> ***                                      no_call P h e'' \<and>
>> ***                                      \<not> \<tau>move0 P h e''
>> ***                              else extTA2J0
>> ***                                    P,P,t \<turnstile> \<langle>Val
>> ***                           v\<bullet>M(es),
>> ***                  (h, xs)\<rangle> -ta\<rightarrow>
>> ***                 \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and>
>> ***                                   no_call P h (Val v\<bullet>M(es)) \<and>
>> ***                                   \<not> \<tau>move0 P h
>> ***     (Val v\<bullet>M(es))))
>> *** At command "apply" (line 911 of "/srv/data/tum/afp/master/thys/JinjaThreads/Compiler/Correctness1.thy")
> 
> Any hint what is going on?
> 
> Cheers,
> 	Florian
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170618/f39641cd/attachment.bin>