# [isabelle] Odd failure to match local statement with pending goal.

```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?

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
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.