Как упростить доказательство свойства функции для типа данных?

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 приветствуется.

Answer 1

Мой опыт показывает, что такие низкоуровневые (и специальные) правила, как ваши disj_not а также redgreen вряд ли когда-нибудь пригодятся. Если они действительно необходимы, это, скорее всего, может быть связано с некоторой нехваткой автоматизации (через соответствующие simp, intro, elim, а также dest правила). К счастью, в вашем примере эти "промежуточные леммы" вообще не нужны (и я не думаю, что они имеют особую образовательную ценность). Подходя к вашему вопросу об обтекаемой версии. Я думаю, что один канонический способ сделать это будет следующим:

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

Где автоматически сгенерированный факт color.exhaust используется для доказательства случаями по переменной x типа color,