[isabelle-dev] AC simplification or theory merge?

[Amine Chaieb]

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