[isabelle] Custom case distinction rules with consider (Isabelle2016-RC3)



Dear Isar wizards,

I try to use the new "consider" statement to prove custom case distinction rules inside my lemmas. (I will only need them inside this particular lemma, so it makes sense to prove them there). However, I have not found a nice way to provide an eigen-context with its own fixed variables to consider. Here's a minimal example which works with Isabelle:

  { fix x :: "('v + 'v) option"
    consider "x = None" | y where "x = Some (Inl y)" | y where "x = Some (Inr y)"
      by pat_completeness }
  note Î_cases = this[case_names None Inl Inr]

Is there any way write this more nicely? I'd like to (in increasing importance)
(i) using note to give a name to the rule andblock
(ii) avoid the boilerplate with opening a proof
(iii) declaring the case names with the cases in consider.

Thanks in advance for any suggestions,
Andreas




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