# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597287349 -32400
# Node ID 5d1cb6ea297715823b1805880cdcba1f3099ce6a
# Parent  8e4a4d27c621baaba3cdc58328e8c0e9b4c73ad6
...

diff -r 8e4a4d27c621 -r 5d1cb6ea2977 first-order.agda
--- a/first-order.agda	Thu Aug 13 11:22:12 2020 +0900
+++ b/first-order.agda	Thu Aug 13 11:55:49 2020 +0900
@@ -5,54 +5,62 @@
 open import Relation.Nullary hiding (¬_)
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 
-data Term : Set where
-      X : Term
-      Y : Term
-      Z : Term
-      a : Term
-      b : Term
-      c : Term
-      f : Term
-      g : Term
-      h : Term
-      p : Term
-      q : Term
-      r : Term
-      _⟨_⟩  : Term → Term → Term
-      _,_   : Term → Term → Term
-      _/\_  :  Term → Term → Term
-      _\/_  :  Term → Term → Term
-      ¬     :  Term → Term 
-      all_=>_ :  Term → Term → Term
-      ∃_=>_ :  Term → Term → Term
+module Logic (Atom : Set ) (Const Func Var Pred : Atom → Set)  where
 
-module Logic (Const Func Var Pred : Term → Set)  where
+  data Term : Set where
+      *_      : Atom → Term
+      _⟨_⟩    : Atom → Term → Term
+      _,_     : Term → Term → Term
+      _/\_    : Term → Term → Term
+      _\/_    : Term → Term → Term
+      ¬       : Term → Term 
+      all_=>_ : Atom → Term → Term
+      ∃_=>_   : Atom → Term → Term
 
   data Expr  : Term → Set  where
-     var   : {v : Term} → Var v → Expr v
-     func  : {x args : Term} → (f : Func x) → Expr args  → Expr ( x ⟨ args ⟩ )
-     const : {c : Term} → Const c → Expr c
+     var   : {v : Atom } → Var v → Expr (* v)
+     func  : {x : Atom } { args : Term} → (f : Func x) → Expr args  → Expr ( x ⟨ args ⟩ )
+     const : {c : Atom } → Const c → Expr (* c)
      args : {x y : Term} → (ex : Expr x) → (ey : Expr y) → Expr ( x , y )
 
   data Statement : Term → Set where
-     atom  :  {x : Term } → Pred x → Statement ( x )
-     predicate  :  {p args : Term } → Pred p → Expr args  → Statement ( p ⟨ args ⟩ )
+     atom  :  {x : Atom } → Pred x → Statement ( * x )
+     predicate  :  {p : Atom } {args : Term } → Pred p → Expr args  → Statement ( p ⟨ args ⟩ )
      and  :  {x y : Term } → Statement x → Statement y  → Statement ( x /\ y )
      or   :  {x y : Term } → Statement x → Statement y  → Statement ( x \/ y )
      not   :  {x : Term } → Statement x → Statement ( ¬ x  )
-     All    :  {x t : Term} → Var x → Statement t → Statement ( all x => t )
-     Exist  :  {x t : Term} → Var x → Statement t → Statement ( ∃ x => t )
+     All    :  {x : Atom } { t : Term} → Var x → Statement t → Statement ( all x => t )
+     Exist  :  {x : Atom } { t : Term} → Var x → Statement t → Statement ( ∃ x => t )
 
-  Model : ( {x : Term } → (px :  Pred x ) → Bool )
-       →  ( {p args : Term } → (px :  Pred p ) → Expr args  → Bool )
+  Model : (ampa :  {x : Atom } → (px :  Pred x ) → Bool )
+       →  (pmap : {p : Atom } { args : Term } → (px :  Pred p ) → Expr args  → Bool )
+       →  (all0   :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool )
+       →  (exist :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool )
        → {t : Term } → Statement t  → Bool
-  Model amap pmap (atom x) = amap x
-  Model amap pmap (predicate x x₁) = pmap x x₁
-  Model amap pmap (and s s₁) = Model amap pmap s  ∧ Model amap pmap s₁ 
-  Model amap pmap (or s s₁) = Model amap pmap s ∨ Model amap pmap s₁ 
-  Model amap pmap (not s) = Data.Bool.not (Model amap pmap s )
-  Model amap pmap (All x s) = {!!}
-  Model amap pmap (Exist x s) = {!!}
+  Model amap pmap all0 exist s = model s where
+      model : {t : Term} → Statement t → Bool
+      model (atom x) = amap x
+      model (predicate x x₁) = pmap x x₁
+      model (and s s₁) = model s  ∧ model s₁ 
+      model (or s s₁) = model s ∨ model s₁ 
+      model (not s) = Data.Bool.not (model s )
+      model (All x s) = all0 x s
+      model (Exist x s) = exist x s
+
+data Atom : Set where
+      X : Atom
+      Y : Atom
+      Z : Atom
+      a : Atom
+      b : Atom
+      c : Atom
+      f : Atom
+      g : Atom
+      h : Atom
+      p : Atom
+      q : Atom
+      r : Atom
+
 
 data Kind : Set where
       pred : Kind
@@ -63,7 +71,7 @@
       arg  : Kind
       args : Kind
 
-data Kinds : Term → Kind → Set where
+data Kinds : Atom → Kind → Set where
       kX : Kinds X var
       kY : Kinds Y var
       kZ : Kinds Z var
@@ -76,38 +84,31 @@
       kp : Kinds p pred
       kq : Kinds q pred
       kr : Kinds r pred
-      karg  : (x y : Term ) → Kinds (x ⟨ y  ⟩ ) arg
-      kargs : (x y : Term ) → Kinds (x , y )  args
-      kand  : (x y : Term ) → Kinds (x /\ y )  conn
-      kor   : (x y : Term ) → Kinds (x \/ y ) conn
-      knot  : (x : Term ) → Kinds  (¬ x ) conn
-      kall_ : (x y : Term ) → Kinds (all x => y ) conn
-      kexit : (x y : Term ) → Kinds (∃ x => y ) conn
 
-Const : Term → Set
+Const : Atom → Set
 Const x = Kinds x const
 
-Func : Term → Set
+Func : Atom → Set
 Func x = Kinds x func
 
-Var : Term → Set
+Var : Atom → Set
 Var x = Kinds x var
 
-Pred : Term → Set
+Pred : Atom → Set
 Pred x = Kinds x pred
 
+open Logic Atom Const Func Var Pred 
+
 ex1 : Term
-ex1 = ¬ ( p /\ ( all X => ( p ⟨ f ⟨ X ⟩ ⟩ )))
-
-open Logic Const Func Var Pred 
+ex1 = ¬ ( (* p ) /\ ( all X => ( p ⟨ f ⟨ * X ⟩ ⟩ )))
 
 parse-arg : (t : Term ) → Maybe (Expr t )
-parse-arg X = just (var kX)
-parse-arg Y = just (var kY)
-parse-arg Z = just (var kZ)
-parse-arg a = just (const ka)
-parse-arg b = just (const kb)
-parse-arg c = just (const kc)
+parse-arg (* X) = just (var kX)
+parse-arg (* Y) = just (var kY)
+parse-arg (* Z) = just (var kZ)
+parse-arg (* a) = just (const ka)
+parse-arg (* b) = just (const kb)
+parse-arg (* c) = just (const kc)
 parse-arg (f ⟨ x ⟩) with parse-arg x
 parse-arg (f ⟨ x ⟩) | just pt = just ( func kf pt )
 parse-arg (f ⟨ x ⟩) | nothing = nothing
@@ -124,9 +125,9 @@
 parse-arg _ = nothing
 
 parse : (t : Term ) → Maybe (Statement t )
-parse p = just ( atom kp )
-parse q = just ( atom kq )
-parse r = just ( atom kr )
+parse (* p) = just ( atom kp )
+parse (* q) = just ( atom kq )
+parse (* r) = just ( atom kr )
 parse (p ⟨ x ⟩) with parse-arg x
 parse (p ⟨ x ⟩) | just y = just ( predicate kp y )
 parse (p ⟨ x ⟩) | nothing = nothing
@@ -167,3 +168,24 @@
 parse _ = nothing
 
 ex2 = parse ex1
+
+subst-expr : {e xv : Term } { x : Atom } → Expr e → Var x → (value : Expr xv ) → Expr {!!}
+subst-expr = {!!}
+
+subst-prop : {xv t : Term } {x : Atom } (orig : Statement t ) → Var x → (value : Expr xv ) → Statement {!!}
+subst-prop = {!!}
+
+ampa :  {x : Atom } → (px :  Pred x ) → Bool 
+ampa {p} px = false
+ampa {q} px = true
+ampa {r} px = false
+pmap : {p : Atom } { args : Term } → (px :  Pred p ) → Expr args  → Bool 
+pmap {p} px (Logic.func kf (Logic.const x)) = true
+pmap {p} px (Logic.func kf _) = false
+pmap {p}  px _ = false
+pmap {q} {y} px _ = false
+pmap {r} {y} px _ = false
+all0   :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool 
+all0   = {!!}
+exist :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool 
+exist = {!!}