如何在Isabelle中按自定义的r1=r2/r1≠r2分情况证明引理

规范引理定义 #

先将你的引理整理为Isabelle标准语法（替换your_type为r1/r2实际的数据类型）：

lemma lts_reachable_subset:
  fixes r1 r2 :: your_type
    v q x
  assumes sem_reg_char: "∀q∈reg2q r1 v. sem_reg q v = {w. LTS_is_reachable (fst (trans2LTS r1 v)) (snd (trans2LTS r1 v)) q w ε}"
    and q_in_reg: "q ∈ reg2q r1 v"
    and extended_reachable: "LTS_is_reachable (fst (trans2LTS r1 v) ∪ fst (trans2LTS r2 v)) 
          (insert (Alter r1 r2, r1) (insert (Alter r1 r2, r2) (snd (trans2LTS r1 v) ∪ snd (trans2LTS r2 v)))) 
          q x ε"
  shows "LTS_is_reachable (fst (trans2LTS r1 v)) (snd (trans2LTS r1 v)) q x ε"

分情况证明实现 #

直接通过cases "r1 = r2"触发排中律分情况，自由变量r2无需额外绑定，Isabelle会自动覆盖两种逻辑分支：

proof (cases "r1 = r2")
  (* 情况1：r1与r2相等 *)
  case True
  then show ?thesis
    using assms
    by (simp add: trans2LTS_same reg2q_same)  (* 替换为你已有的同构LTS简化引理，或直接simp展开 *)

  (* 情况2：r1与r2不相等 *)
  case False
  then show ?thesis
    using assms
    by (metis LTS_reachable_no_extra_states Alter_distinct sem_reg_char q_in_reg)  (* 替换为你需要的可达性、Alter性质相关规则 *)
qed

分支处理要点 #

• 相等分支：r1=r2时，trans2LTS r1 v与trans2LTS r2 v完全一致，新增的Alter状态会因r1=r2简化（若有对应等式），目标可通过simp结合已有辅助引理直接推导。
• 不等分支：r1≠r2时，需利用Alter r1 r2的唯一性（比如不属于原LTS状态集），结合前提中sem_reg的刻画，证明扩展后的LTS新增状态/转移不会影响原LTS的可达性，常用metis或auto结合可达性子集规则完成。
• 若需显式调用排中律，可替换为proof (cases rule: classical)，手动引入r1=r2和¬r1=r2的假设，但cases "r1=r2"更简洁直观。

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