多态类型的存在性证明

Question

我正试图正式证明DFA在工会下是封闭的，我已经证明了这一点。"∀ 𝒜 ℬ. language 𝒜 ∪ language ℬ = language (DFA_union 𝒜 ℬ)"但我真正想证明的是... ... ∀ 𝒜 ℬ. ∃ 𝒞. language 𝒜 ∪ language ℬ = language 𝒞. 我相信这个问题与多态类型有关，但我不确定。

我的情况是这样的。

declare [[show_types]]
declare [[show_sorts]]
declare [[show_consts]]

record ('q, 'a)DFA =
  Q0 :: 'q
  F :: "'q set"
  δ :: "'q ⇒ 'a ⇒ 'q"

primrec δ_iter :: "('q, 'a)DFA ⇒ 'a list ⇒ 'q ⇒ 'q" where
  "δ_iter 𝒜 [] q = q" |
  "δ_iter 𝒜 (a # as) q = δ_iter 𝒜 as (δ 𝒜 q a)"

definition δ0_iter :: "('q, 'a)DFA ⇒ 'a list ⇒ 'q" where
  "δ0_iter 𝒜 as = δ_iter 𝒜 as (Q0 𝒜)"

definition language :: "('q, 'a)DFA ⇒ ('a list) set" where
  "language 𝒜 = {w . δ0_iter 𝒜 w ∈ (F 𝒜)}"

fun DFA_union :: "('p, 'a)DFA ⇒ ('q, 'a)DFA ⇒ ('p × 'q, 'a)DFA" where
  "DFA_union 𝒜 ℬ = 
    ⦇ Q0 = (Q0 𝒜, Q0 ℬ)
    , F = {(q, r) . q ∈ F 𝒜 ∨ r ∈ F ℬ}
    , δ = λ (q, r). λ a. (δ 𝒜 q a, δ ℬ r a) 
    ⦈"

lemma extract_fst: "∀ 𝒜 ℬ p q. fst (δ_iter (DFA_union 𝒜 ℬ) ws (p, q)) = δ_iter 𝒜 ws p" 
  by (induct ws; simp)

lemma extract_snd: "∀ 𝒜 ℬ p q. snd (δ_iter (DFA_union 𝒜 ℬ) ws (p, q)) = δ_iter ℬ ws q" 
  by (induct ws; simp)

lemma "∀ 𝒜 ℬ. language 𝒜 ∪ language ℬ = language (DFA_union 𝒜 ℬ)"
proof((rule allI)+)
  fix 𝒜 ℬ
  let ?𝒞 = "DFA_union 𝒜 ℬ"
  have "language ?𝒞 = {w . δ0_iter ?𝒞 w ∈ F ?𝒞}" 
    by (simp add: language_def)
  also have "... = {w . fst (δ0_iter ?𝒞 w) ∈ (F 𝒜) ∨ snd (δ0_iter ?𝒞 w) ∈ (F ℬ)}" 
    by auto 
  also have "... = {w . δ0_iter 𝒜 w ∈ F 𝒜 ∨ δ0_iter ℬ w ∈ F ℬ}"
    using DFA.select_convs(1) DFA_union.simps δ0_iter_def extract_fst extract_snd
    by (metis (no_types, lifting)) 
  also have "... = {w . δ0_iter 𝒜 w ∈ F 𝒜} ∪ {w. δ0_iter ℬ w ∈ F ℬ}"
    by blast
  also have "... = language 𝒜 ∪ language ℬ"
    by (simp add: language_def)
  finally show "language 𝒜 ∪ language ℬ = language ?𝒞"
    by simp
qed

lemma DFA_union_closed: "∀ 𝒜 ℬ. ∃ 𝒞. language 𝒜 ∪ language ℬ = language 𝒞"
  sorry

如果我在主外稃中给𝒜或ℬ添加类型，我得到 "未能完善任何待定目标 "的结果。

Answer 1

问题确实是因为隐式类型。在你的最后一句话中，Isabelle隐式推导了状态类型 'p, 'q, 'r 对于三个自动机 A, B, C而你的 DFA_union 的状态类型。C 到 'p * 'q. 因此，如果你必须明确地提供类型注释。此外，通常不需要用显式的 ∀-量词。

所以，你可以继续这样做。

lemma DFA_union: "language 𝒜 ∪ language ℬ = language (DFA_union 𝒜 ℬ)" 
  (is "_ = language ?𝒞")
proof -
   have "language ?𝒞 = {w . δ0_iter ?𝒞 w ∈ F ?𝒞}" 
   ...
qed

lemma DFA_union_closed: fixes 𝒜 :: "('q,'a)DFA" and ℬ :: "('p,'a)DFA"
  shows "∃ 𝒞 :: ('q × 'p, 'a)DFA. language 𝒜 ∪ language ℬ = language 𝒞"
  by (intro exI, rule DFA_union)

请注意，这些类型注解在下面的意义上也是必不可少的. 像下面这样的定理（所有的状态类型都是一样的）是不正确的.

lemma fixes 𝒜 :: "('q,'a)DFA" and ℬ :: "('q,'a)DFA"
  shows "∃ 𝒞 :: ('q, 'a)DFA. language 𝒜 ∪ language ℬ = language 𝒞"

问题是，插入 bool-类型为 'q那么你的自动机最多只有两种状态。然后你不可能总是找到一个自动机的结合体，也有最多两个状态。