[isabelle-dev] AC simplification or theory merge?
Amine Chaieb
ac638 at cam.ac.uk
Fri Jan 30 12:54:49 CET 2009
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.
More information about the isabelle-dev
mailing list