Existance proofs with polymorphic types

Question

I am trying to formalize the proof that DFA are closed under union, and I have got so far as proving "∀ ℬ. language ∪ language ℬ = language (DFA_union ℬ)", but what I would actually like to prove is ∀ ℬ. ∃ . language ∪ language ℬ = language . I belive the issue has something to do with polymorphic types, but I am not sure.

Here is what I have:

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

If I add types to or ℬ in the main lemma I get "Failed to refine any pending goal".

Answer 1

the problem is indeed because of implicit types. In your last statement Isabelle implicitly infers state-types 'p, 'q, 'r for the three automata A, B, C, whereas your DFA_union lemma fixes the state type of C to 'p * 'q. Therefore, if you have to explicitly provide type-annotations. Moreover, it is usually not required to state your lemmas with explicit ∀-quantifiers.

So, you can continue like this:

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)

Note that these type-annotations are also essential in the following sense. A lemma like the following (where all state-types are the same) is just not true.

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

The problem is, plug in the bool-type for 'q, then you have automata which have at most two states. And then you cannot always find an automaton for the union that also has at most two states.