[isabelle] Isar-Level cases command



Dear Isabelle-users,

we (rightfully) pride ourselves with how natural nicely written Isar
proofs are. But things are (always) not perfect, and there is always
room for careful improvements.

Consider this rather idiomatic proof:

lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  show ?case
  proof(cases "P x")
    case True with Cons
    have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
    also note Cons.IH
    also have "Suc (length xs) = length (x#xs)" by simp
    finally show ?thesis by this simp
  next
    case False with Cons
    have "length (filter P (x#xs)) = length (filter P xs)" by simp
    also note Cons.IH
    also have "length xs ≤ length (x#xs)" by simp
    finally show ?thesis .
 qed
qed
    
It is a nicely written structural proof and easy to follow. But there is
a wart: The case distinction!

      * I have to write "show ?case" to initiate a case distinction. But
        this is not natural: At this point, the final result is not what
        is on my mind. And in a manually written proof, I would not
        re-state the current goal at this point.
      * If I had not used the "case" command I would actually have to
        copy’n’paste the current goal here; obviously not very nice.
        Especially if there are multiple case distinction, each
        requiring me to copy that.
      * The goal was conveniently named ?case, but suddenly I have to
        write ?thesis. I (believe I) understand the techical reasons,
        but again, this is a violation of the principle of least
        surprise.

What I would like to be able to write is something like

lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  
  cases("P x")
    case True with Cons
    have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
    also note Cons.IH
    also have "Suc (length xs) = length (x#xs)" by simp
    finally show ?case by this simp
  next
    case False with Cons
    have "length (filter P (x#xs)) = length (filter P xs)" by simp
    also note Cons.IH
    also have "length xs ≤ length (x#xs)" by simp
    finally show ?case .
  qed
qed


No seemingly redundant statement of the subgoals, the ability to simply
use ?case and the conventional flow of thoughts and facts in such a
proof.


This would also open the way to conveniently discharge multiple subgoals
in one case distinction:

lemma "A" and "B"
proof-
  have "C" sorry

  cases ("D")
    case True
    from `C` show A using True sorry
    thus B using True sorry
  next
    case False
    from `C` show B using False sorry
    thus A using False sorry
  qed
qed

(Note that in this case, no ?thesis is available, and
        show A and B proof (cases "D") 
 does not do the right thing, as it apply the cases rule only to the
first subgoal, so it becomes messy to do this proof right now.)


This is the users mailing list, so I’ll refrain from making wild
assumptions about if and how this could be implemented, and whether
there is a similarity to the obtains command, but instead ask you for
feedback on the user-facing design of this feature:

Is it something you’d want as well?
Is the syntax nice?
What could be the closing keyword, if not qed?


Greetings,
Joachim
-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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