*To*: Konrad Slind <slind at cs.utah.edu>*Subject*: Re: [isabelle] pushing let environments to the top level*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 27 Apr 2009 09:40:00 -0700*Cc*: Ewaryst Schulz <ewaryst.schulz at dfki.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <D7C2A3F3-DEF2-414E-AD25-CE1213F3FEFF@cs.utah.edu>*References*: <49F18DB9.3000802@dfki.de> <D7C2A3F3-DEF2-414E-AD25-CE1213F3FEFF@cs.utah.edu>*Sender*: huffman.brian.c at gmail.com

On Sat, Apr 25, 2009 at 4:43 PM, Konrad Slind <slind at cs.utah.edu> wrote: > Michael Norrish and I tackled exactly this sort of thing in > > http://www.cs.utah.edu/~slind/papers/tphols05.pearl.pdf<http://www.cs.utah.edu/%7Eslind/papers/tphols05.pearl.pdf> > > The ideas in the paper are worked out in HOL4, and may > need to be modified a bit for Isabelle/HOL. > I just tried out the rules from the paper in Isabelle/HOL. Indeed, the unmodified rules don't work quite the same in Isabelle. Here's what I tried: definition flip_def [simp]: "flip f x y = f y x" definition compose_def [simp]: "compose f g x = f (g x)" lemma Let_simps: "!!f m g. f (Let m g) = Let m (compose f g)" "!!m f n. (Let m f) n = Let m (flip f n)" "!!f g. compose f (%x. g x) = (%x. f (g x))" "!!f y. flip (%x. f x) y = (%x. f x y)" "!!f g. compose f (split g) = split (compose (compose f) g)" "!!f x. flip (split f) x = split (flip (compose flip f) x)" unfolding Let_def expand_fun_eq by simp_all Next I applied these as rewrites to the example term from the paper: lemma "perm (h # t) (let (l1, l2) = part (%y. ord y h) t in qsort ord l1 @ [h] @ qsort ord l2)" apply (simp only: Let_simps) Here's the resulting term I hoped to get: let (l1, l2) = part (%y. ord y h) t in perm (h # t) (qsort ord l1 @ [h] @ qsort ord l2)" But here's what I got: goal (1 subgoal): 1. let x = part (%y. ord y h) t in perm (h # t) ((%(l1, l2). qsort ord l1 @ [h] @ qsort ord l2) x) It sort of worked. At least the let binding was lifted to the outside of the term. But the tuple binding was replaced with a single variable binding. Also, the simplifier invented a new bound variable name, while the rules in the paper are specifically designed to preserve bound variable names. It appears that the Isabelle's simplifier behaves differently than HOL4. In HOL4, the LHS patterns of the following two rules are non-overlapping: "compose f (%x. g x) = (%x. f (g x))" "compose f (split g) = split (compose (compose f) g)" In Isabelle, I think the simplifier treats the first rule as equivalent to the eta-contracted form: "compose f g = (%x. f (g x))" So it matches more often than the same rule in HOL4. As a workaround, you could call the simplifier twice, using the split-specific rules first, and the more general rules afterward: lemma "perm (h # t) (let (l1, l2) = part (%y. ord y h) t in qsort ord l1 @ [h] @ qsort ord l2)" apply (simp only: Let_simps(1,2,5,6), simp only: Let_simps(3,4)) goal (1 subgoal): 1. let (xa, x) = part (%y. ord y h) t in perm (h # t) (qsort ord xa @ [h] @ qsort ord x) This at least gets the tuple binding in the right place, but the variable names are still wrong. It just seems that the preservation of bound variable names is a feature of the HOL4 simplifier that was never implemented in Isabelle. Instead, Isabelle's simplifier replaces the old bound variable name for whatever name was used on the RHS of the original rewrite rule. For example: lemma foo: "!!f g. compose f (%a. (g a, h a)) = (%a. f (g a, h a))" unfolding expand_fun_eq by simp lemma "P (compose f (%y. (y, y)))" apply (simp only: foo) goal (1 subgoal): 1. P (%a. f (a, a)) Anyway, I guess my conclusion is that to lift let-bindings in Isabelle, we will need more than just a set of rewrite rules. A special proof tactic that preserves variable names probably wouldn't be too hard to implement though. - Brian

**References**:**[isabelle] pushing let environments to the top level***From:*Ewaryst Schulz

**Re: [isabelle] pushing let environments to the top level***From:*Konrad Slind

- Previous by Date: [isabelle] Termination Proof ``fun'' ;)
- Next by Date: Re: [isabelle] Termination Proof ``fun'' ;)
- Previous by Thread: Re: [isabelle] pushing let environments to the top level
- Next by Thread: [isabelle] PhD positions in ICT on Formal Verification via SMT available in Trento
- Cl-isabelle-users April 2009 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