如何为Isabelle中类star的range正则定义类似in_star_iff_concat的引理？

核心思路 #

Range正则（r^m到r^n的重复）的本质是有限次数的可控重复，完全可以类比Star的in_star_iff_concat引理，通过列表分解+正则操作封闭性来完成证明：

1. 先将Range的成员资格转化为「m到n个原正则匹配子串的连接」；
2. 用已有的正则构造（重复、连接、并）组合出Range对应的正则表达式；
3. 基于列表分解引理证明构造出的表达式与Range语义等价。

步骤1：定义Range的语义 #

先明确Range的核心语义：字符串w属于range r m n，当且仅当它能被拆分为k个（m ≤ k ≤ n）属于r语言的子串的连接。

definition in_range :: "'a regex ⇒ nat ⇒ nat ⇒ 'a list ⇒ bool" where
  "in_range r m n w = (∃k. m ≤ k ∧ k ≤ n ∧ ∃ws. length ws = k ∧ (∀i<k. ws ! i ∈ language r) ∧ w = concat ws)"

步骤2：证明Range的列表分解引理 #

类比in_star_iff_concat，先把Range的成员资格和列表分解绑定，这是后续证明的核心桥梁：

lemma in_range_iff_concat:
  "in_range r m n w ⟷ (∃k∈{m..n}. ∃ws. length ws = k ∧ (∀i<k. ws ! i ∈ language r) ∧ w = concat ws)"
  unfolding in_range_def using CollectI by auto

证明逻辑：

• 左→右：直接根据in_range的定义提取对应的k和子串列表；
• 右→左：对k在[m,n]范围内的情况，结合子串的语言成员资格，直接推导w满足in_range的条件。

步骤3：构造Range对应的正则表达式 #

利用正则语言在连接、并、有限重复下的封闭性，构造range_regex：

• 若m > n，直接返回空语言（Zero）；
• 否则，先构造r重复m次的表达式，再并上r重复0到n-m次的所有表达式，最后将两部分连接。

(* 先定义正则表达式的有限重复：repeat r k 表示r重复k次 *)
fun repeat :: "'a regex ⇒ nat ⇒ 'a regex" where
  "repeat r 0 = One"  (* One对应空串语言 *)
| "repeat r (Suc k) = repeat r k @> r"  (* @>表示正则表达式的连接 *)

(* 构造Range正则表达式 *)
fun range_regex :: "'a regex ⇒ nat ⇒ nat ⇒ 'a regex" where
  "range_regex r m n = (if m > n then Zero else repeat r m @> foldr (<|>) (map (repeat r) [0..n-m]) Zero)"

注：<|>是正则表达式的并操作，Zero对应空语言。

步骤4：证明语义等价性 #

基于前面的列表分解引理，证明构造出的range_regex的语言恰好是in_range定义的集合：

lemma language_range_regex:
  "language (range_regex r m n) = {w. in_range r m n w}"
proof (cases "m > n")
  case True
  then show ?thesis unfolding range_regex_def language_Zero by auto
next
  case False
  let ?R = "foldr (<|>) (map (repeat r) [0..n-m]) Zero"
  (* 先证明?R的语言是r重复0到n-m次的所有字符串 *)
  have "language ?R = {w. ∃k≤n-m. w ∈ language (repeat r k)}"
    by (induction "map (repeat r) [0..n-m]" rule: foldr_induct)
       (auto simp: language_Union language_Zero)
  (* 再推导连接后的语言 *)
  have "language (repeat r m @> ?R) = {w. ∃u v. u ∈ language (repeat r m) ∧ v ∈ language ?R ∧ w = u@v}"
    unfolding language_Concat by auto
  (* 结合列表分解引理，转化为Range的语义 *)
  also have "... = {w. ∃k∈{m..n}. ∃ws. length ws=k ∧ (∀i<k. ws!i∈language r) ∧ w=concat ws}"
  proof (intro set_eqI iffI)
    fix w assume "w ∈ ?thesis"
    then obtain k₁ k₂ ws₁ ws₂ where k₁=m and k₂≤n-m 
      and len1: "length ws₁=k₁" and len2: "length ws₂=k₂"
      and mem1: "∀i<k₁. ws₁!i∈language r" and mem2: "∀i<k₂. ws₂!i∈language r"
      and w_eq: "w=concat ws₁@concat ws₂" by auto
    let ?k = k₁ + k₂; let ?ws = ws₁ @ ws₂
    show "w ∈ {w. ∃k∈{m..n}. ∃ws. length ws=k ∧ (∀i<k. ws!i∈language r) ∧ w=concat ws}"
      using k₁=m k₂≤n-m False len1 len2 mem1 mem2 w_eq concat_append by auto
  next
    fix w assume "w ∈ {w. ∃k∈{m..n}. ∃ws. length ws=k ∧ (∀i<k. ws!i∈language r) ∧ w=concat ws}"
    then obtain k ws where k_range: "m ≤k ≤n" and len: "length ws=k"
      and mem: "∀i<k. ws!i∈language r" and w_eq: "w=concat ws" by auto
    let ?k₂ = k - m; let ?ws₁ = take m ws; let ?ws₂ = drop m ws
    show "w ∈ language (repeat r m @> ?R)"
      using k_range len mem w_eq concat_take_drop language_repeat language_Union language_Concat by auto
  qed
  finally show ?thesis unfolding range_regex_def False in_range_iff_concat by auto
qed

关键说明 #

• 如果AFP库中已有现成的有限重复/范围操作，可以直接复用，无需自己定义repeat；
• 当m=0时，range r 0 n就是Star的有限版本（最多n次重复），此时构造可以简化为foldr (<|>) (map (repeat r) [0..n]) Zero；
• 整个证明的核心是用列表分解将Range的语义转化为已知正则操作的组合，完全对齐in_star_iff_concat的证明思路。

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