Search code examples
isabelletheorem-provingautomaton

Existance proofs with polymorphic types

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".

Solution

  • 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.