Re: [isabelle] SMT and bound variables.



To clarify, you need to import the src/HOL/Word/WordBitwise which should probably be included by default.

Thomas.

Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote:

>Hey Lars.
>
>I'm not sure if proof reconstruction is now available for bitvectors. 
>Sascha and I looked at the problem a few years ago, and the conclusion 
>was it was doable but the performance was a tad disappointing.
>
>The tactic we implemented to help discharge the theory-lemmas appearing 
>in bitvector proofs *is* available, and should be in your context under 
>the name word_bitwise. It does the bitwise expansion of your problem and 
>some minor simplification. Together with real simplification it solves 
>both of these problems, although a bit slowly.
>
>Thomas.
>
>On 06/07/13 03:21, Lars Noschinski wrote:
>> Hi,
>>
>> I'm getting annoyed by the tediousness required to discharge seemingly 
>> trivial problems on words and thought I would try the "smt" method on 
>> them.
>>
>> (BTW: Is proof reconstruction available for Bitvectors?)
>>
>> I found a strange behaviour (in 2012, 2013 and ffc3f1659a25): Consider 
>> the two goals stated below. They are equivalent, the only difference is
>> between free and bound variables. Yet "smt" can only solve the second 
>> goal and suggests a possibly spurious counter-example for the first one.
>>
>> -------------------------------------------------------------------------- 
>>
>> theory Scratch imports "~~/src/HOL/Word/Word" begin
>>
>> lemma "⋀degree k. (degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
>>   using [[smt_oracle=true]]
>>   apply smt (* Fails, talks about possibly spurious counter-example *)
>>   oops
>>
>> lemma "(degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
>>   using [[smt_oracle=true]]
>>   apply smt (* Succeeds *)
>>   done
>> -------------------------------------------------------------------------- 
>>
>>
>> Is this some known limitation or a bug in the preprocessing?
>>
>> Best regards,
>>   Lars
>>
>


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