Isar结构化证明中结合前后向推理简化i=0分支目标的方法问询

在Isar中处理i = 0这类分支时，要兼顾前后向推理，有几种实用方案：

1. 分支内直接用自动工具关联事实 #

当你通过cases i分情况后，case 0分支会自动将i = 0纳入上下文。直接用simp或auto这类工具，就能自动把该事实代入目标做简化：

proof (cases i)
  case 0
  then show ?thesis by simp
  case (Suc n)
  (* 处理i为后继数的分支逻辑 *)
qed

这里的then会把case 0给出的i = 0事实传递给simp，工具会自动匹配并简化目标中的invariant表达式。

2. 显式提取事实做自定义推导 #

如果需要更精细的控制，可以先将分支事实存为局部变量，再通过using关联到目标推导：

proof (cases i)
  case 0
  let ?zero_fact = `i = 0`
  have "invariant (smallStep fac (0, f)) a r" using ?zero_fact by (rule your_custom_rule)
  then show ?thesis .
qed

这种方式适合不依赖自动工具，需要手动控制简化步骤的场景。

3. 结合apply_end与上下文事实 #

你尝试的apply_end()可以配合上下文事实使用，直接引用分支内的条件或case_hps（分支自动生成的事实集合）：

proof (cases i)
  case 0
  apply_end (simp add: case_hps)
  (* 或者直接指定事实 *)
  apply_end (simp add: `i = 0`)
qed

case_hps会包含当前分支的所有前提事实，用它能快速将i = 0纳入简化的可用条件中。

本质上，Isar的结构化分支会自动把分支条件（如i=0）加入当前上下文，不管是用then/using做前向事实传递，还是用apply_end做后向策略调用，只要明确引用上下文里的事实，就能自然结合前后向推理。

内容的提问来源于stack exchange，提问作者cxandru