0

我创建了一个小证明，目的是创建一个用于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 的风格。

4

1 回答 1

2

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。

于 2014-06-30T17:48:08.773 回答