*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] natural number arithmetic normalisation*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 14 Nov 2011 10:32:40 +0100*In-reply-to*: <CAAMXsiZjTgm0Z=sk9grbhFBsEB7=bFSY=ekYDX8sTxdDL9j1VQ@mail.gmail.com>*References*: <4EC0541C.1090406@nicta.com.au> <CAAMXsiZjTgm0Z=sk9grbhFBsEB7=bFSY=ekYDX8sTxdDL9j1VQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0

It would certainly be nice to get rid of these rewrites, but the task is daunting. Tobias Am 14/11/2011 07:23, schrieb Brian Huffman: > On Mon, Nov 14, 2011 at 12:34 AM, Michael Norrish > <Michael.Norrish at nicta.com.au> wrote: >> The following term arose inside a side-condition that the simplifier was attempting to discharge: >> >> (2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) >> >> The simp tactic being used included field_simps as a rewrite. >> >> The result was an apparent "hang" as Isabelle attempted to calculate 2 ^ 32 in unary arithmetic. >> >> You can see the behaviour by doing >> >> lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X" >> apply (simp add: field_simps) > > This is a very interesting puzzle, especially since, as you say, > field_simps doesn't even mention Suc! > > After looking at the simp trace to see which rules were involved I > realized that you can get the same blowup using "simp only" with a > small set of rules, none of which are in field_simps, and all of which > are in the default simpset: > > lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X" > apply (simp only: One_nat_def mult_Suc_right mult_0_right add_2_eq_Suc) > > Yet simply writing "apply simp" on the same goal reduces everything to > just a numeral. > > The weirdness involves these rewrite rules: > > lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" > lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" > > These rules originate quite a while ago: > http://isabelle.in.tum.de/repos/isabelle/rev/9d6514fcd584 > > Now, what happens if we simplify a term like "2 + 0" or "0 + 2", where > more than one possible simp rule can apply? It turns out that the > simplifier will rewrite "2 + 0" to "2" (using the additive zero law), > but in the other order, "0 + 2" rewrites to "Suc (Suc 0)" (using rule > add_2_eq_Suc'). So the presence of the add_commute rule really makes a > difference here: > > lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X" > apply (simp add: add_commute) (* blows up with Suc *) > > >> It seems to me that this is yet more evidence that using 1 = Suc 0 as a rewrite is a bad idea. > > I agree. I think that a good guideline for the Isabelle simpset should > be that no simp rule should ever insert a Suc into a subgoal that > didn't already contain one. > > We have discussed removing "1 = Suc 0" as a simp rule on the dev > mailing list before: > https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-February/000484.html > > My conclusion back then was that the only reason we have "1 = Suc 0" > [simp] is historical, since "1" used to be a mere abbreviation for > "Suc 0". It would be nice to finally get rid of it (along with > add_2_eq_Suc and friends). > > - Brian

**References**:**[isabelle] natural number arithmetic normalisation***From:*Michael Norrish

**Re: [isabelle] natural number arithmetic normalisation***From:*Brian Huffman

- Previous by Date: Re: [isabelle] natural number arithmetic normalisation
- Next by Date: [isabelle] Combining locales?
- Previous by Thread: Re: [isabelle] natural number arithmetic normalisation
- Next by Thread: [isabelle] Combining locales?
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list