*To*: Tobias Nipkow <nipkow at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Using Simplifier.asm_rewrite*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Thu, 4 Feb 2016 11:05:38 +0200*In-reply-to*: <56B3001A.4050702@in.tum.de>*References*: <C32D3449D568C445AB18C60817FABFE10144E5188657@ingrid.foiskola.krf> <56B1CC57.2050707@in.tum.de> <C32D3449D568C445AB18C60817FABFE10144E5188658@ingrid.foiskola.krf> <56B1E6EA.40305@in.tum.de> <56B20EDF.8020603@aalto.fi> <56B3001A.4050702@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1

Hi Tobias, Thank you for the answer. I will do as you suggest. Anyway, my starting theorem does not have schematic variables. In the process it seems that I need some schematic variables, for example to combine theorems with OF, but I will make schematic just the variables that are needed. Viorel On 02/04/2016 09:39 AM, Tobias Nipkow wrote: > This may have something to do with the fact that hypotheses in > theorems may not contain schematic variables. Or because the rewrit > step would (or appears to) require instantiation of a schematic > variable in the term to be rewritten. If it does not work it is safe > to assume that it is an inherent limitation and you have to convert > schematic to ordinary variables first. > > Tobias > > On 03/02/2016 15:29, Viorel Preoteasa wrote: >> I am trying to use asm_rewrite to simplify a term f(u,v,w) under some >> assumptions p(u,v,w). p and f are given as a pair (p,f) and p and f have >> the same domain type. For this I construct in ML the term >> "p(u,v,w) ==> Aux_Var = f(u,v,w)". >> >> In my test f(u,v,w) = ((if u + v < 10 then w else w + 1) + 2) >> and p(u,v,w) = (u + v < 10), and the goal is to simplify >> f to f(u,v,w) = w + 2 under the assumption p(u,v,w). >> >> If I define in ML >> >> val pair_a = @{term "(term for p, term for f)"}; >> >> and I apply the procedure described above all works well, >> however if instead I define the pair as the right hand >> side of a definition that contains the same term for the >> pair, the simplification does not work. The "if" term stays >> unsimplified >> >> val pair_b = Thm.term_of (Thm.rhs_of ( @{thm Test_Pair_def})); >> >> The only difference between pair_a and pair_b seems to be the >> types. In pair_a there are simple type variables, while in pair_b >> there are schematic type variables. >> >> Attached is the theory with the ML function implementing this >> simplification. At the end it defines two variables simp_a_th >> simp_b_th holding the simplifications of the two terms >> pair_a and pair_b. In pair_a "if" is simplified, while in pair_b >> "if" is not simplified. It works the same in Isabelle2015 and >> also Isabelle2016-RC3. >> >> Why is this difference? Is it possible to get the same simplification >> result also on the pair_b term? >> >> Best regards, >> >> Viorel Preoteasa >> >

**References**:**[isabelle] residual subgoals***From:*Buday Gergely

**Re: [isabelle] residual subgoals***From:*Lars Hupel

**Re: [isabelle] residual subgoals***From:*Buday Gergely

**Re: [isabelle] residual subgoals***From:*Tobias Nipkow

**[isabelle] Using Simplifier.asm_rewrite***From:*Viorel Preoteasa

**Re: [isabelle] Using Simplifier.asm_rewrite***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Isabelle2016-RC3: delayed updated of error bar in main text area
- Next by Date: Re: [isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory
- Previous by Thread: Re: [isabelle] Using Simplifier.asm_rewrite
- Next by Thread: Re: [isabelle] Using Simplifier.asm_rewrite
- Cl-isabelle-users February 2016 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