*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Using Simplifier.asm_rewrite*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 4 Feb 2016 08:39:06 +0100*In-reply-to*: <56B20EDF.8020603@aalto.fi>*References*: <C32D3449D568C445AB18C60817FABFE10144E5188657@ingrid.foiskola.krf> <56B1CC57.2050707@in.tum.de> <C32D3449D568C445AB18C60817FABFE10144E5188658@ingrid.foiskola.krf> <56B1E6EA.40305@in.tum.de> <56B20EDF.8020603@aalto.fi>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.5.1

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Using Simplifier.asm_rewrite***From:*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

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