Mercurial > hg > Members > kono > Proof > automaton
annotate agda/regop.agda @ 89:e919e82e95a2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Nov 2019 12:21:44 +0900 |
| parents | 9406c2571fe7 |
| children |
| rev | line source |
|---|---|
| 24 | 1 module regop where |
| 0 | 2 |
| 24 | 3 open import automaton |
| 4 | |
| 5 -- open import Level renaming ( suc to succ ; zero to Zero ) | |
| 2 | 6 open import Data.Nat |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
7 open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
8 open import Data.Maybe |
| 24 | 9 open import Data.Product |
| 10 open import Data.Bool using ( Bool ; true ; false ; _∧_ ) | |
| 3 | 11 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 9 | 12 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 0 | 13 |
| 14 | |
| 24 | 15 union : {Q1 Q2 Σ : Set } → ( M1 : Automaton Q1 Σ) ( M2 : Automaton Q2 Σ) → Automaton (Q1 × Q2) Σ |
| 16 union {Q1} {Q2} {Σ} M1 M2 = record { | |
| 17 δ = δ | |
| 18 ; astart = astart | |
| 19 ; aend = aend | |
| 20 } where | |
| 21 δ : (Q1 × Q2) → Σ → (Q1 × Q2) | |
| 22 δ = {!!} | |
| 23 astart : (Q1 × Q2) | |
| 24 astart = {!!} | |
| 25 aend : (Q1 × Q2) → Bool | |
| 26 aend = {!!} | |
| 0 | 27 |
| 24 | 28 data _∨_ (A B : Set) : Set where |
| 29 p1 : A → A ∨ B | |
| 30 p2 : B → A ∨ B | |
| 0 | 31 |
| 24 | 32 union← : {Q1 Q2 Σ : Set } → ( M1 : Automaton Q1 Σ) ( M2 : Automaton Q2 Σ) → |
| 33 ∀ ( s : List Σ ) → accept ( union M1 M2 ) s ≡ true → ( ( accept M1 s ≡ true ) ∨ ( accept M2 s ≡ true) ) | |
| 34 union← {Q1} {Q2} {Σ} M1 M2 s eq = {!!} |