# [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.
{"ft_lang_label":"__label__en","ft_lang_prob":0.72911406,"math_prob":0.7782173,"size":3576,"snap":"2021-43-2021-49","text_gpt3_token_len":1157,"char_repetition_ratio":0.22424412,"word_repetition_ratio":0.4977029,"special_character_ratio":0.3649329,"punctuation_ratio":0.105726875,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9880304,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-11-27T17:21:52Z\",\"WARC-Record-ID\":\"<urn:uuid:c1471d0b-31a6-4220-b68a-e61eac262bcf>\",\"Content-Length\":\"8442\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:a733680b-5c49-4128-9897-a47cb56f2478>\",\"WARC-Concurrent-To\":\"<urn:uuid:217c4a09-1f54-4758-8a1e-dc21af3a3fee>\",\"WARC-IP-Address\":\"131.111.8.15\",\"WARC-Target-URI\":\"https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-July/msg00130.html\",\"WARC-Payload-Digest\":\"sha1:TW5H75STX55O4DUBDS63ZWESEMEO5LT6\",\"WARC-Block-Digest\":\"sha1:64V3EBUFGG4G4NJVLVZDQFPQWOJQ3KBN\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-49/CC-MAIN-2021-49_segments_1637964358208.31_warc_CC-MAIN-20211127163427-20211127193427-00566.warc.gz\"}"}