Mercurial > hg > Members > kono > Proof > FirstOrder
annotate Logic.agda @ 11:17cd0e70e931
add clausal form transformation
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Aug 2020 10:18:55 +0900 |
| parents | edf4a816abff |
| children | 1e3ebb348a54 |
| rev | line source |
|---|---|
| 9 | 1 module Logic (Const Func Var Pred : Set) where |
| 1 | 2 open import Data.List hiding (all ; and ; or ) |
| 2 | 3 open import Data.Bool hiding ( not ) |
| 5 | 4 |
| 9 | 5 data Expr : Set where |
| 6 var : Var → Expr | |
| 10 | 7 func : Func → Expr → Expr |
| 9 | 8 const : Const → Expr |
|
11
17cd0e70e931
add clausal form transformation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
9 _,_ : Expr → Expr → Expr |
| 0 | 10 |
| 9 | 11 data Statement : Set where |
| 10 | 12 pred : Pred → Statement |
| 13 predx : Pred → Expr → Statement | |
| 14 _/\_ : Statement → Statement → Statement | |
| 15 _\/_ : Statement → Statement → Statement | |
| 16 ¬_ : Statement → Statement | |
| 17 All_=>_ : Var → Statement → Statement | |
| 18 Exist_=>_ : Var → Statement → Statement | |
| 19 | |
| 20 subst-prop : (e : Statement ) → (sbst : Expr → Var → Expr → Expr ) → Var → Expr → Statement | |
| 21 subst-prop (pred x) sbst xv v = pred x | |
| 22 subst-prop (predx x x₁) sbst xv v = predx x ( sbst x₁ xv v ) | |
| 23 subst-prop (e /\ e₁) sbst xv v = ( subst-prop e sbst xv v ) /\ ( subst-prop e₁ sbst xv v ) | |
| 24 subst-prop (e \/ e₁) sbst xv v = ( subst-prop e sbst xv v ) \/ ( subst-prop e₁ sbst xv v ) | |
| 25 subst-prop (¬ e) sbst xv v = ¬ ( subst-prop e sbst xv v ) | |
| 26 subst-prop (All x => e) sbst xv v = All x => ( subst-prop e sbst xv v ) | |
| 27 subst-prop (Exist x => e) sbst xv v = Exist x => ( subst-prop e sbst xv v ) | |
| 0 | 28 |
| 9 | 29 {-# TERMINATING #-} |
| 30 M : (amap : Pred → Bool ) (pmap : Pred → Expr → Bool ) | |
| 31 → (all-const : List Expr ) | |
| 10 | 32 → (subst-prop : Expr → Var → Expr → Expr ) |
| 9 | 33 → Statement → Bool |
| 34 M amap pmap all0 sbst s = m s where | |
| 35 m : Statement → Bool | |
| 10 | 36 m (pred x) = amap x |
| 37 m (predx x x₁) = pmap x x₁ | |
| 38 m (s /\ s₁) = m s ∧ m s₁ | |
| 39 m (s \/ s₁) = m s ∨ m s₁ | |
| 40 m (¬ s) = Data.Bool.not (m s ) | |
| 41 m (All x => s) = m-all all0 x s where | |
| 9 | 42 m-all : List Expr → Var → Statement → Bool |
| 43 m-all [] vx s = true | |
| 10 | 44 m-all (x ∷ t) vx s = m (subst-prop s sbst vx x ) ∧ m-all t vx s |
| 45 m (Exist x => s) = m-exist all0 x s where | |
| 9 | 46 m-exist : List Expr → Var → Statement → Bool |
| 47 m-exist [] vx s = false | |
| 10 | 48 m-exist (x ∷ t) vx s = m (subst-prop s sbst vx x ) ∨ m-exist t vx s |
| 1 | 49 |