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

Dear Christian,

This seems to be a deficiency of the cases method (just like it not binding ?case to the conclusion). If you use induct instead, it works, but you have to qualify the hypothesis by the case name:

    proof (induct rule: foo)
      case a
      thm a.a1


On 02/07/15 11:44, Christian Sternagel wrote:
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.