*To*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*Subject*: Re: [isabelle] Odd failure to match local statement with pending goal.*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Wed, 10 Aug 2011 00:58:31 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20110802211001.GA2459@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*References*: <20110727112106.GA2460@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <4E3165D3.9080306@in.tum.de> <20110802211001.GA2459@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*User-agent*: Thunderbird 2.0.0.6 (X11/20070801)

Bertram Felgenhauer wrote: > So do we know whether this is an obscure feature or possibly a bug? > (If it's a feature I'd love to hear the underlying story.) Hi, this problem has now been fixed in the repository version of Isabelle (476a239d3e0e). It was caused by some rather old code in Isabelle's theorem module that renamed "all bound variables and some unknowns" in a rule during resolution, in order to preserve as many of the variable names in the goal as possible. For example, when resolving the rule ?P ?x ==> \<exists>x. P x with the proof state \<exists>foo. P foo this will result in the new proof state ?P ?foo because the schematic variable ?x in the rule has been renamed to match that of the bound variable foo in the goal. Unfortunately, such a renaming of schematic variables can cause two kinds of name clashes, neither of which were detected by the old code: 1. If two bound variables in the goal happen to have the same name, this may cause two schematic variables in the rule to be mapped to the same variable: lemma R1: "P x ==> Q y ==> (\<exists>x. P x) \<and> (\<exists>y. Q y)" by auto lemma "(\<exists>z. P z) \<and> (\<exists>z. Q z)" apply (rule R1) oops 2. If a bound variable in the goal happens to have the same name as a schematic variable in the rule, it may clash with another schematic variable in the rule after the renaming. lemma R2: "P y ==> x = y ==> \<exists>x. P x" by auto lemma "\<exists>y. P y" apply (rule R2) oops I have now introduced a check that filters out such problematic renamings. Greetings, Stefan

**References**:**Re: [isabelle] Odd failure to match local statement with pending goal.***From:*Bertram Felgenhauer

- Previous by Date: [isabelle] Question regarding sequent calculi in Isabelle
- Next by Date: Re: [isabelle] schematic variables
- Previous by Thread: Re: [isabelle] Odd failure to match local statement with pending goal.
- Next by Thread: [isabelle] Get an ML value from a theory context
- Cl-isabelle-users August 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