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

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


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