[isabelle-dev] AC simplification or theory merge?

[Brian Huffman]

Hi Amine,

In the interest of making your proof scripts more robust, I think it  
is best to avoid relying on the term ordering whenever possible.  
Specifically, if you have a tactic like (simp add: mult_ac) that does  
not completely solve the subgoal, and the following tactic relies on  
the resulting terms being in a specific order, then this is a problem.

In this situation you should break up your proof using the  
transitivity reasoner, so that AC rewriting is only used in situations  
where it completely solves the subgoal it is given.

Hope this helps,

- Brian

Quoting Amine Chaieb <ac638 at cam.ac.uk>:

> I managed now to get all the proofs done. Apparently the term ordering
> changes if I don't merge...
>
> Amine.
>
> Amine Chaieb wrote:
>> Dear all,
>> I am trying to integrate some development about generalized   
>> factorials and generalized binomial coefficients. The theory alone   
>> is working fine.
>> Then I decided to put all the lemmas in Binomial.thy since in this   
>> case a new file is not really necessary.
>> It roughly looks like this:
>>
>> Binomial imports Plain "~~/src/HOL/SetInterval"
>>
>> and
>>
>> Pochhammer imports Fact Binomial Presburger
>>
>> Fact imports Nat
>>
>> *In this configuration all my proofs go through!!*
>>
>> So I replaced the import section by the union of these two, added   
>> my proofs at the end of the old file: My proofs broke down.
>>
>>
>> It roughly looks like:
>>
>> Binomial imports Plain "~~/src/HOL/SetInterval" Fact Presburger
>> Content of old Binomial
>> Content of Pochhammer
>> end
>>
>> *In this configuration many of my proofs are broken!!*
>>
>> I suspected the order in which theories are loaded, so I tried the   
>> several combinations (4!) but this does not help. Investigating   
>> more closely, it seems that rewriting with commutativity does not   
>> work properly (I am sure of this). I have e.g. proved a statement   
>> "x*y = z" and then want the other version "y*x = z", the proof text  
>>  by (simp only: mult_commute my_theorem) does not work, I had to  
>> use  subst. This is a very simple instance, but there are proofs  
>> wich  involve many many factors, so I can not afford to do these by  
>> hand.
>>
>> Why does this happen? Is this the merge again? Some other   
>> mechanism? I also replaced ring_simps/field_simps by algebra_simps   
>> but this does not help. I think something is wrong with the   
>> term_ordering when I don't merge???
>>
>> Best wishes,
>> Amine.
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev