isabelle - データ型の関数プロパティの証明を合理化する方法は?

Question

next証明ケースで使用する例を作成する目的で、小さな証明を作成しました。

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 

詳細を失うことなく、これを合理化できますか? 魔法のトリックを使用することは、私が望んでいることではありません。Isar の使用スタイルの改善は大歓迎です。