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