*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Odd failure to match local statement with pending goal.*From*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*Date*: Wed, 27 Jul 2011 13:21:07 +0200*User-agent*: Mutt/1.5.21 (2010-09-15)

Dear Isabelle users, I have a theory (the full theory is attached to this mail) with the following definitions, datatype tree = LeafA | LeafB | Node "tree" "tree" fun closure :: "tree \<Rightarrow> tree set" where "closure (Node r s) = { z. \<exists> r' s'. r' \<in> closure r \<and> s' \<in> closure s \<and> z = Node r' s' }" | "closure LeafA = { LeafA }" | "closure LeafB = { LeafA, LeafB }" The failure occurs when proving the following lemma. lemma "closure (Node r (Node s t)) \<subseteq> closure (Node (Node r s) t)" unfolding closure.simps First I unfolded a couple of things, proof (rule subsetI, unfold mem_Collect_eq, elim exE conjE) and then I essentially copied the resulting goal (this explains the horrible variable names) fix x r' s' r'a s'a assume "r' \<in> closure r" and "x = Node r' s'" and "r'a \<in> closure s" and "s'a \<in> closure t" and "s' = Node r'a s'a" thus "\<exists>r' s'. (\<exists>r'a s'. r'a \<in> closure r \<and> s' \<in> closure s \<and> r' = Node r'a s') \<and> s' \<in> closure t \<and> x = Node r' s'" At this point I get a failure that I don't understand, that this statement fails to match the goal: *** Local statement will fail to refine any pending goal *** Failed attempt to solve goal by exported rule: ... The failure disappears if I rename the r'a to r'a' inside the existential quantifier of the conclusion (included as a comment in the attachment), i.e., simply by doing an alpha conversion. I find this very odd. Can anybody explain this behaviour? Thanks in advance, Bertram P.S. > isabelle version Isabelle2011: January 2011 > uname -a Linux host 2.6.39-2-amd64 #1 SMP Wed Jun 8 11:01:04 UTC 2011 x86_64 GNU/Linux

theory Test imports Main begin datatype tree = LeafA | LeafB | Node "tree" "tree" fun closure :: "tree \<Rightarrow> tree set" where "closure (Node r s) = { z. \<exists> r' s'. (r' \<in> closure r \<and> s' \<in> closure s \<and> z = Node r' s') }" | "closure LeafA = { LeafA }" | "closure LeafB = { LeafA, LeafB }" lemma "closure (Node r (Node s t)) \<subseteq> closure (Node (Node r s) t)" unfolding closure.simps proof (rule subsetI, unfold mem_Collect_eq, elim exE conjE) fix x r' s' r'a s'a (** This works -- the difference to the failing version is that *** r'a was renamed to r'a' inside the existential quantification of *** the conclusion. assume "r' \<in> closure r" and "x = Node r' s'" and "r'a \<in> closure s" and "s'a \<in> closure t" and "s' = Node r'a s'a" thus "\<exists>r' s'. (\<exists>r'a' s'. r'a' \<in> closure r \<and> s' \<in> closure s \<and> r' = Node r'a' s') \<and> s' \<in> closure t \<and> x = Node r' s'" sorry **) (** while this fails: **) assume "r' \<in> closure r" and "x = Node r' s'" and "r'a \<in> closure s" and "s'a \<in> closure t" and "s' = Node r'a s'a" thus "\<exists>r' s'. (\<exists>r'a s'. r'a \<in> closure r \<and> s' \<in> closure s \<and> r' = Node r'a s') \<and> s' \<in> closure t \<and> x = Node r' s'" sorry (** *** Local statement will fail to refine any pending goal *** Failed attempt to solve goal by exported rule: *** \<lbrakk>?r'2 \<in> closure r; ?x2 = Node ?r'2 ?s'2; ?r'a2 \<in> closure s; *** ?s'a2 \<in> closure t; ?s'2 = Node ?r'a2 ?s'a2\<rbrakk> *** \<Longrightarrow> \<exists>r' s'. *** (\<exists>r'a s'. r'a \<in> closure r \<and> s' \<in> closure s \<and> r' = Node r'a s') \<and> *** s' \<in> closure t \<and> ?x2 = Node r' s' *** At command "thus" (line 19 of ".../Bug.thy") **) end

**Follow-Ups**:**Re: [isabelle] Odd failure to match local statement with pending goal.***From:*Lawrence Paulson

**Re: [isabelle] Odd failure to match local statement with pending goal.***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Defining Union Types
- Next by Date: Re: [isabelle] Defining Union Types
- Previous by Thread: Re: [isabelle] Defining Union Types
- Next by Thread: Re: [isabelle] Odd failure to match local statement with pending goal.
- Cl-isabelle-users July 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