[isabelle-dev] AC simplification or theory merge?

[Amine Chaieb]

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.