# [isabelle-dev] AC simplification or theory merge?

Amine Chaieb ac638 at cam.ac.uk
Fri Jan 30 13:42:41 CET 2009

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

```