Isabelle/HOL正则表达式转LTS自反引理证明求助

我在Isabelle/HOL中完成了正则表达式相关定义，尝试证明一个直观成立的引理，具体定义如下：

datatype 'v regexp = ESet 
                   | LChr 'v
                   | Concat "'v regexp" "'v regexp"
                   | Alter "'v regexp" "'v regexp"
                   | Dot
                   | Star "'v regexp" 
                   | Plus "'v regexp" 
                   | Ques "'v regexp" 
                   | ε         

fun ConcatRegexp :: "'v regexp ⇒ 'v regexp ⇒ 'v regexp" where
  "ConcatRegexp r1 r2 = Concat r2 r1"

fun ConcatRegexp2 :: "'v regexp ⇒ 'v regexp ⇒ 'v regexp" where
  "ConcatRegexp2 r1 r2 = Concat (Concat r2 r1) r1"

fun renameDelta1 :: "('v regexp * 'v set * 'v regexp) set ⇒ ('v regexp ⇒ 'v regexp) ⇒ ('v regexp * 'v set * 'v regexp) set" where 
  "renameDelta1 ss f = {(f q, v, f q') | q v q' . (q, v, q') ∈ ss}"

fun renameDelta2 :: "('v regexp * 'v regexp) set ⇒ ('v regexp ⇒ 'v regexp) ⇒ ('v regexp * 'v regexp) set" where  
  "renameDelta2 ss f = {(f q, f q') | q q' . (q, q') ∈ ss}"

primrec trans2LTS :: "'v regexp ⇒ 'v set ⇒ (('v regexp × 'v set × 'v regexp) set * ('v regexp * 'v regexp) set)" where 
  "trans2LTS (LChr v) alp_set = ({(LChr v, {v}, ε)}, {})" |
  "trans2LTS ESet alp_set = ({(ESet, {}, ε)}, {})" |
  "trans2LTS ε alp_set = ({(ε, {}, ε)}, {})" |
  "trans2LTS Dot alp_set = ({(Dot, alp_set, ε)}, {})" |
  "trans2LTS (Concat r1 r2) alp_set = (
    renameDelta1 (fst (trans2LTS r1 alp_set)) (ConcatRegexp r2) ∪ fst (trans2LTS r2 alp_set),
    renameDelta2 (snd (trans2LTS r1 alp_set)) (ConcatRegexp r2) ∪ {(Concat ε r2, r2)} ∪ snd (trans2LTS r2 alp_set)
  )" |
  "trans2LTS (Alter r1 r2) alp_set = (
    fst (trans2LTS r1 alp_set) ∪ fst (trans2LTS r2 alp_set), 
    snd (trans2LTS r1 alp_set) ∪ snd (trans2LTS r2 alp_set) ∪ {(Alter r1 r2, r1), (Alter r1 r2, r2)}
  )" |
  "trans2LTS (Star r) alp_set = (
    renameDelta1 (fst (trans2LTS r alp_set)) (ConcatRegexp (Star r)), 
    renameDelta2 (snd (trans2LTS r alp_set)) (ConcatRegexp (Star r)) ∪ {(Star r, ε), (Star r, Concat r (Star r)), (Concat ε (Star r), Star r)}
  )" |
  "trans2LTS (Plus r) alp_set = (
    (renameDelta1 (fst (trans2LTS r alp_set)) (ConcatRegexp2 (Star r))) ∪ (renameDelta1 (fst (trans2LTS r alp_set)) (ConcatRegexp (Star r))), 
    {(Plus r, Concat (Concat r (Star r)) (Star r)), (Concat (Concat ε (Star r)) (Star r), Concat (Star r) (Star r)), (Concat (Star r) (Star r), ε), (Concat (Star r) (Star r), Concat r (Star r)), (Concat ε (Star r), Concat (Star r) (Star r))}
    ∪ (renameDelta2 (snd (trans2LTS r alp_set)) (ConcatRegexp2 (Star r))) ∪ (renameDelta2 (snd (trans2LTS r alp_set)) (ConcatRegexp (Star r)))
  )" |
  "trans2LTS (Ques r) alp_set = (
    fst (trans2LTS r alp_set),
    {(Ques r, ε), (Ques r, r)} ∪ snd (trans2LTS r alp_set)
  )"

待证明的reflexNotHold引理定义如下：

lemma reflexNotHold: "(r, r) ∈ snd (trans2LTS r v) ⟹ False"
  apply(induction r)
  sorry

最初采用结构归纳法对正则表达式结构进行归纳证明该引理，但受函数递归定义影响，共有4个子目标无法完成，以下是可行的证明思路： #

证明卡壳的核心原因 #

直接对正则表达式做结构归纳时，命题强度不足，没有覆盖renameDelta2引入的上下文映射性质，也没有利用Isabelle数据类型自带的构造子互斥、单射、子项结构严格更小的内置定理，导致Concat、Alter、Star、Plus四个复合构造子分支无法闭合。

具体证明步骤 #

1 先证明两个前置小引理 #

这两个引理可以直接用simp策略自动证明，不需要手动推导：

• 上下文函数单射性：定义的ConcatRegexp、ConcatRegexp2都是正则表达式构造子的部分应用，由于datatype的构造子是单射的，这两个函数也都是单射函数：

  lemma ConcatRegexp_inj: "inj (ConcatRegexp x)"
    by (simp add: inj_def ConcatRegexp.simps)
  
  lemma ConcatRegexp2_inj: "inj (ConcatRegexp2 x)"
    by (simp add: inj_def ConcatRegexp2.simps)
  

• 子项结构严格更小：Isabelle自动为datatype生成了子项size严格小于父项的定理，任意正则表达式的子表达式结构大小一定小于表达式本身，不可能和父项相等。

2 归纳时拆分集合成员关系 #

对r做结构归纳时，每个复合构造子分支的ε边集合都是三个部分的并集，逐个拆解矛盾即可：

• renameDelta2生成的边集合：展开renameDelta2定义可知，集合里的元素都是(f q, f q')形式，其中(q,q')是子表达式的ε边。如果存在(f q, f q)属于该集合，由f的单射性可得q=q'，直接和归纳假设（子表达式q不存在自环）矛盾；另外这部分边的节点都是f作用的结果，f是Concat开头的上下文，和当前根构造子（比如Star/Plus/Alter）不同，语法上不可能等于当前根r。
• 子表达式自带的ε边集合：这部分边的节点都是子表达式内部的节点，根据归纳假设，子表达式自身不存在自环；且子表达式要么是当前根的子项（size更小，不可能等于根），要么构造子和根不同，不可能等于根r。
• 手动添加的显式ε边集合：这部分边直接用simp即可证明不存在自环：
  • 边的左值如果是当前根r，右值要么是ε（基础构造子，和根构造子不同），要么是r的子表达式（size更小，不可能等于r），要么是其他构造子生成的项（比如Star r的边右值是Concat开头的项，和Star构造子互斥，不可能相等）
  • 边的左值如果不是当前根r，自然不可能构成(r,r)的边对

3 基础分支自动证明 #

ESet、LChr、Dot、ε四个基础构造子的ε边集合是空集，直接用simp即可证明不存在任何边，自然不存在自环。 #

按上述步骤，给归纳过程加上对应的单射引理、构造子互斥定理、子项size定理，所有子目标都可以自动解出，不需要手动编写复杂的证明步骤。

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