I am trying to construct the complement regexp.

First, I construct the NFA automaton, the definition of neg1 automaton takes an automaton and changes its accepts states. I thought it's a straightforward idea.

However, I was stuck by the last lemma, `accepts_neg1`

. Any help would be appreciated.

```
type_synonym ('a,'s) na = "'s * 'a set * ('a ⇒'s ⇒ 's set) * ('s ⇒ bool)"
primrec delta :: "('a,'s)na ⇒ 'a list ⇒ 's ⇒ 's set" where
"delta A [] p = {p}" |
"delta A (a#w) p = Union(delta A w ` next A a p)"
definition
accepts :: "('a,'s)na ⇒ 'a list ⇒ bool" where
"accepts A w = (∃q ∈ delta A w (start A). fin A q)"
definition
step :: "('a,'s)na ⇒ 'a ⇒ ('s * 's)set" where
"step A a = {(p,q) . q : next A a p}"
primrec steps :: "('a,'s)na ⇒ 'a list ⇒ ('s * 's)set" where
"steps A [] = Id" |
"steps A (a#w) = step A a O steps A w"
lemma steps_append[simp]:
"steps A (v@w) = steps A v O steps A w"
by(induct v, simp_all add:O_assoc)
lemma in_steps_append[iff]:
"(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
apply(rule steps_append[THEN equalityE])
apply blast
done
lemma delta_conv_steps: "⋀p. delta A w p = {q. (p,q) : steps A w}"
by(induct w)(auto simp:step_def)
lemma accepts_conv_steps:
"accepts A w = (∃q. (start A,q) ∈ steps A w ∧ fin A q)"
by(simp add: delta_conv_steps accepts_def)
type_synonym 'a bitsNA = "('a, nat list)na"
definition
neg1 :: "'a bitsNA ⇒ 'a bitsNA" where
"neg1 = (λ(ql,vl1,dl,fl). (ql, vl1, dl, λs. ¬ fl s))"
lemma fin_neg1[iff]:
"⋀L. fin (neg1 L) q = (¬ fin L q)"
apply(simp add:neg1_def)
done
lemma start_neg1[iff]:
"⋀L. start (neg1 L) = start L"
apply (simp add:neg1_def)
done
lemma step_neg1[iff]:
"⋀L p. (p, q)∈ step (neg1 L) a = ((p, q) ∈ step L a)"
apply(simp add:neg1_def step_def)
done
lemma steps_neg1[iff]:
"⋀L p. (p, q)∈ steps (neg1 L) w = ((p, q) ∈ steps L w)"
apply(induct w)
apply simp
apply simp
apply force
done
lemma accepts_neg1: accepts (neg1 L) w ⟹ (¬ accepts L w)"
apply (simp add: accepts_conv_steps)
apply(induct w)
apply simp
sorry
```

I just think the way is to universal parameter in the state q, but I don't know how to solve it.

What is you definition of `next`

?

```
definition start :: "'a * 'b * 'c * 'd ⇒ 'a" where "start A = fst A"
definition alp :: "'a * 'b * 'c * 'd ⇒ 'b" where "alp A = fst(snd(A))"
definition "next" :: "'a * 'b * 'c * 'd ⇒ 'c" where "next A = fst(snd(snd(A)))"
definition fin :: "'a * 'b * 'c * 'd ⇒ 'd" where "fin A = snd(snd(snd(A)))"
```

Please remove the useless `⋀L p.`

~~And the proof goes through once you realize that you have to generalize over ~~`p`

and `q`

wrong lemma

Once remove the L and p, the steps lemma couldn't pass easily

I though a little bit more about it and it is unclear to me if this holds because NFA means that you could have two paths one reaching a final a state and one reaching a non-final state. So negation would still accept the word.

```
lemma "accepts (neg1 L) [w] ⟹ (¬ accepts L [w])"
(*
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
L = ([], {}, λx xa. {[0], []}, UNIV - {[]})
w = a⇩1
*)
```

Not sure if the counter-example is correct

My NFA includes the initial state, alphabet, transition states and accept states.

The transition rules take one alphabet and one state, the state is denoted in a list, then return a list set, like the atom automaton below,

```
definition
"atom" :: "'a ⇒ 'a set ⇒ 'a bitsNA" where
"atom a vs = ([2],vs,
λb s. if s=[2] ∧ b=a ∧ a : vs then {[3]} else {[1]},
λs. case s of [] ⇒ False | left#s ⇒ (left#s) = [3])"
```

There is no counterexample in my script.

```
Testing conjecture with Quickcheck-exhaustive...
Quickcheck ran out of time
Quickcheck found no counterexample.
```

I don't know exactly.

I replace the path w by a path of length 1 `[w]`

Ahh, I see. From the counterexample, the negation of L cound just accept empty list. That's the inital state and any input character.

Last updated: Feb 27 2024 at 08:17 UTC