[isabelle-dev] AC simplification or theory merge?
brianh at cs.pdx.edu
Fri Jan 30 15:57:15 CET 2009
In the interest of making your proof scripts more robust, I think it
is best to avoid relying on the term ordering whenever possible.
Specifically, if you have a tactic like (simp add: mult_ac) that does
not completely solve the subgoal, and the following tactic relies on
the resulting terms being in a specific order, then this is a problem.
In this situation you should break up your proof using the
transitivity reasoner, so that AC rewriting is only used in situations
where it completely solves the subgoal it is given.
Hope this helps,
Quoting Amine Chaieb <ac638 at cam.ac.uk>:
> 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
>> 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,
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev