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

Best,
Andreas


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:

   lemma
     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.,

   lemma
     assumes "A â A' â B â B'"
     obtains
       (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?

cheers

chris





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