多态类型的存在证明

Question

我正在尝试形式化证明 DFA 在 union 下是封闭的，目前我已经证明了 "∀ ℬ. 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

如果我在主引理中添加类型或 ℬ 我得到 "Failed to refine any pending goal".

Answer 1

确实是隐式类型的问题。在你最后的陈述中，伊莎贝尔隐式地推断出三个自动机 A, B, C 的状态类型 'p, 'q, 'r，而你的 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 "

问题是，为 'q 插入 bool 类型，然后你就有了自动机最多有两个状态。然后你不能总是找到一个最多也有两个状态的联盟的自动机。

多态类型的存在证明

Existance proofs with polymorphic types

theorem-proving

automaton

isabelle