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



On 28.07.2011 12:45, Lawrence Paulson wrote:
I'm afraid I can't. In general, the name of a bound variable should be irrelevant. I considered the possibility of a hidden effect on type inference, but all variables have the same type, namely tree.

Strange.

Indeed. When I tried to find a minimal example, I found that it goes away, when I try to remove the initial proof steps:

-----------------
lemma "⋀x. x ∈ {z. ∃r' s'. r' ∈ closure r ∧ s' ∈ {z. ∃r' s'. r' ∈
      closure s ∧ s' ∈ closure t ∧ z = Node r' s'} ∧ z = Node r' s'} ⟹
    x ∈ {z. ∃r' s'. r' ∈ {z. ∃r' s'. r' ∈ closure r ∧ s' ∈ closure
      s ∧ z = Node r' s'} ∧ s' ∈ closure t ∧ z = Node r' s'}"
  apply (unfold mem_Collect_eq)
  apply (elim exE conjE)
proof -
  fix x r' s' r'a

  assume "x = Node r' s'" and "r'a ∈ closure s"
  then show "∃r' s'.
    (∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s
      ∧ r' = Node r'a s') ∧
    s' ∈ closure t ∧ x = Node r' s'"
oops
-----------------

still exhibits this behabiour, but if I remove the unfold too, it goes away. The show statement in the following snippet works just fine:

-----------------
lemma "⋀x. ∃r' s'. r' ∈ closure r ∧ (∃r' s'a. r' ∈ closure s ∧ s'a ∈
      closure t ∧ s' = Node r' s'a) ∧ x = Node r' s' ⟹
    ∃r' s'. (∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s ∧ r' = Node r'a
      s') ∧ s' ∈ closure t ∧ x = Node r' s'"
  apply (elim exE conjE)
proof -
  fix x r' s' r'a

  assume "x = Node r' s'" and "r'a ∈ closure s"
  then show "∃r' s'.
    (∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s
      ∧ r' = Node r'a s') ∧
    s' ∈ closure t ∧ x = Node r' s'"
    sorry
oops
-----------------





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