*To*: Tobias Nipkow <nipkow at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Let and commutative rewrite rules*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 7 May 2015 09:03:18 +0200*In-reply-to*: <5549E119.3080508@in.tum.de>*References*: <55477B5E.80404@inf.ethz.ch> <554783E1.2090107@in.tum.de> <55487DE5.6070305@inf.ethz.ch> <5549E119.3080508@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Dear Tobias,

let x = foo a b c in let y = bar a b c in let z = fbr a b c in f x x y y z z

let y = bar a b c in let z = fbr a b c in f (foo a b c) (foo a b c) y y z z

Andreas

lemma Let_folded2: "â f x â g x; g â g' â â Let x f â Let x g'" by (simp add: Let_def) simproc_setup let_simp ("Let x f") = {* let val (f_Let_unfold, x_Let_unfold) = let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold} in apply2 (Thm.cterm_of @{context}) (f, x) end val (f_Let_folded2, x_Let_folded2) = let val [(_ $ (f $ x) $ _), _] = Thm.prems_of @{thm Let_folded2} in apply2 (Thm.cterm_of @{context}) (f, x) end; val (g_Let_folded2, g'_Let_folded2) = let val [_, (_ $ g $ g')] = Thm.prems_of @{thm Let_folded2} in apply2 (Thm.cterm_of @{context}) (g, g') end; fun count_loose (Bound i) k = if i >= k then 1 else 0 | count_loose (s $ t) k = count_loose s k + count_loose t k | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) | count_loose _ _ = 0; fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) = (case t of Abs (_, _, t') => count_loose t' 0 <= 1 | _ => true); in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct) then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) else let (*Norbert Schirmer's case*) val t = Thm.term_of ct; val ([t'], ctxt') = Variable.import_terms false [t] ctxt; in Option.map (hd o Variable.export ctxt' ctxt o single)

if is_Free x orelse is_Bound x orelse is_Const x then SOME @{thm Let_def} else let val n = case f of (Abs (x, _, _)) => x | _ => "x"; val cx = Thm.cterm_of ctxt x; val xT = Thm.typ_of_cterm cx; val cf = Thm.cterm_of ctxt f; val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx); val (_ $ _ $ g) = Thm.prop_of fx_g; val g' = abstract_over (x, g); val abs_g'= Abs (n, xT, g'); in if g aconv g' then let val rl =

in SOME (rl OF [fx_g]) end

NONE (*avoid identity conversion*) else (* normalise the abstracted body, as the abstraction might have un-normalised the body, e.g., ordered rewriting, simprocs with syntactic checks, ... *) let val g'_normal = Simplifier.rewrite ctxt (Thm.cterm_of ctxt abs_g'); val (_ $ _ $ g'_normalised) = Thm.prop_of g'_normal; in

NONE else let val g'x = abs_g' $ x;

val rl = @{thm Let_folded2} |> cterm_instantiate [(f_Let_folded2, Thm.cterm_of ctxt f), (x_Let_folded2, cx), (g_Let_folded2, Thm.cterm_of ctxt abs_g'), (g'_Let_folded2, Thm.cterm_of ctxt g'_normalised)]; in SOME (rl OF [Thm.transitive fx_g g_g'x, g'_normal]) end end end | _ => NONE) end end *} On 06/05/15 11:38, Tobias Nipkow wrote:

Dear Andreas, Thank you for your thoughts, but I would rather not change the current setup. I don't really understand Norbert's code and I don't want to add further bits to it. Moreover, the problem seems to crop up very rarely. If we were to modify the code, I would expect one of two results: it hardly has any effect or it breaks a lot of proofs. In both cases I would want to leave well alone. Tobias PS I have recently made some similar change also in HOL and am thinking about undoing it for some of the reasons above. On 05/05/2015 10:23, Andreas Lochbihler wrote:Dear Tobias, I had another look at the implementation of let_simp. I guess that one might be able to change the let simproc fairly easily. The idea is as follows. For non-trivial lets (at least two occurrences of the bound variable and the bound term is not atomic), the let simproc inlines the bound term in the body, normalises the result with the simplifier and the current simpset, and then replaces all the remaining occurrences of the bound term in the normalised term with the bound variable. There is already a check whether the new body is alpha-beta-eta-equivalent to the old body. In that case, the simproc aborts with NONE. Now, the interaction can occur only if the abstracted body is no longer in normal form (although it is with the bound term inlined)*. Thus, it would make sense to normalise the abstracted body again and check for equivalence with the original body. When I add this additional check, the looping in my example disappears. What do you think? Best, Andreas * This may happen due to term order as in my case, but I imagine that simprocs like NO_MATCH equally cause trouble here. On 04/05/15 16:36, Tobias Nipkow wrote:Dear Andreas, I was not aware of this interaction but it does not surprise me - the let simproc is magic - but you can switch it off. I have no idea if it can be modified to avoid this interaction in the first place. That sounds like a time sink. Tobias On 04/05/2015 15:59, Andreas Lochbihler wrote:Dear experts on rewriting, I have a problem with let bindings and commutative rewrite rules. Here is an example and my understanding of what is happening. lemma "(let pb = foobar b in f pb (Îpad. g (pb * pad :: int))) = bar" apply(simp add: mult.commute) 1. mult.commute rewrites pb * pad into pad * pb, because pad seems to be smaller than pb in the term order that the simplifier uses. 2. The let simproc determines that pb occurs more than once in the body, so it does not inline the let binding. Instead, it simplifies the body with knowledge pb = foobar b. Thus, the simplifier now sees pad * foobar b. Since "foobar b" is smaller than pad in the term order, commutativity kicks in again and we get foobar b * pad. Now, the simproc abstracts the simplified body over foobar b again and replaces it with pb. So we are back to pb * pad. Thus, the simplifier goes over the whole term again and we are back at step 1. In my understanding so far, commutative rewrite rules are safe (in the sense of termination) to add to the simplifier, but the let simproc interferes with this. Is this a known problem? Can the let simproc be somehow changed to avoid this? Best, Andreas

**Follow-Ups**:**Re: [isabelle] Let and commutative rewrite rules***From:*Tobias Nipkow

**References**:**[isabelle] Let and commutative rewrite rules***From:*Andreas Lochbihler

**Re: [isabelle] Let and commutative rewrite rules***From:*Tobias Nipkow

**Re: [isabelle] Let and commutative rewrite rules***From:*Andreas Lochbihler

**Re: [isabelle] Let and commutative rewrite rules***From:*Tobias Nipkow

- Previous by Date: [isabelle] Isabelle2015-RC3 available for testing: Overzealous reprocessing
- Next by Date: Re: [isabelle] Cyclic graphs
- Previous by Thread: Re: [isabelle] Let and commutative rewrite rules
- Next by Thread: Re: [isabelle] Let and commutative rewrite rules
- Cl-isabelle-users May 2015 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