[isabelle] case_names, obtains (par_name), and named local hypotheses

Dear list,

according to the documentation of the "case_names" attribute it is possible to name (sub)hypothesis of cases. Maybe I'm misunderstanding the description in isar-ref (page 139). But I thought that after

  lemma foo [consumes 1, case_names a [a1 a2] b [b1 b2]]:
    "A â A' â B â B' â (A â A' â P) â (B â B' â P) â P"
  by blast

it would be possible to refer to "a1", "a2", "b1", and "b2" in subsequent proofs as follows:

    assumes "A â A' â B â B'"
    shows "A â B'"
    using assms
    proof (cases rule: foo)
      case a
      thm a1 -- "this doesn't seem to work"

Could someone please clarify?

On a related note, it would be nice to be able to introduce names for subhypothesis also for "obtains". E.g.,

    assumes "A â A' â B â B'"
      (a [a_1 a2]) "A" and "A'" |
      (b [b_1 b2]) "B" and "B'"
    using assms by blast

Or maybe this is already possible and I just couldn't figure out how?



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