[isabelle-dev] AC simplification or theory merge?
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 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"
> 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
> *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
> Best wishes,
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev