I have created a small proof with the intention of creating an example for using next on proof cases:
theory RedGreen
imports Main
begin
datatype color = RED | GREEN
fun green :: "color => color"
where
"green RED = GREEN"
| "green GREEN = GREEN"
lemma disj_not: "P \<or> Q \<Longrightarrow> \<not>P \<longrightarrow> Q"
proof
assume disj: "P \<or> Q"
assume "\<not>P"
from this show "Q" using `P \<or> Q` by (simp)
qed
lemma redgreen: "x \<noteq> RED \<longrightarrow> x = GREEN"
proof
assume notred: "x \<noteq> RED"
have "x = RED \<or> x = GREEN" by (simp only: color.nchotomy)
from this show "x = GREEN" using notred by (simp add: disj_not)
qed
lemma "green x = GREEN"
proof cases
assume "x = RED"
from this show "green x = GREEN" by (simp)
next
assume "x \<noteq> RED"
from this have "x = GREEN" by (simp add: redgreen)
from this show "green x = GREEN" by (simp)
qed
Can this be streamlined without losing the details? Using some magical tricks would not be the thing I wish for. Improving the style of using Isar is welcome.
My experience is that such low-level (and ad-hoc) rules like your disj_not and redgreen are hardly ever useful. If they are really necessary this can most likely be attributed to some lack of automation (via appropriate simp, intro, elim, and dest rules). Gladly, in your example these "intermediate lemmas" are not necessary at all (and I do not think that they are of special educational value). Coming to your question of a streamlined version. I think one canonical way of doing so would be the following:
lemma "green x = GREEN"
proof (cases x)
case RED
then show "green x = GREEN" by simp
next
case GREEN
then show "green x = GREEN" by simp
qed
Where the automatically generated fact color.exhaust is used for a proof by cases on the variable x of type color.