# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597290397 -32400
# Node ID abb61bee093aa1813c08f9282b3cbe1de5d7cb2a
# Parent  d4a148a4809f9c2fa20186cb5a4d983752e5685c
remove Atom

diff -r d4a148a4809f -r abb61bee093a first-order.agda
--- a/first-order.agda	Thu Aug 13 12:42:25 2020 +0900
+++ b/first-order.agda	Thu Aug 13 12:46:37 2020 +0900
@@ -44,19 +44,26 @@
           model-exist [] vx s = false
           model-exist (x ∷ t) vx s = model (sbst s vx x ) ∨ model-exist t vx 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 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
 
 
 data Kind : Set where
@@ -68,7 +75,7 @@
       arg  : Kind
       args : Kind
 
-data Kinds : Atom → Kind → Set where
+data Kinds : Term → Kind → Set where
       kX : Kinds X var
       kY : Kinds Y var
       kZ : Kinds Z var
@@ -82,40 +89,30 @@
       kq : Kinds q pred
       kr : Kinds r pred
 
-Const : Atom → Set
+Const : Term → Set
 Const x = Kinds x const
 
-Func : Atom → Set
+Func : Term → Set
 Func x = Kinds x func
 
-Var : Atom → Set
+Var : Term → Set
 Var x = Kinds x var
 
-Pred : Atom → Set
+Pred : Term → Set
 Pred x = Kinds x pred
 
-open Logic Atom Const Func Var Pred 
-
-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
+open Logic Term Const Func Var Pred 
 
 ex1 : Term
-ex1 = ¬ ( (* p ) /\ ( all X => ( p ⟨ f ⟨ * X ⟩ ⟩ )))
+ex1 = ¬ ( p  /\ ( all X => ( p ⟨ f ⟨ X ⟩ ⟩ )))
 
 parse-arg : (t : Term ) → Maybe Expr 
-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
@@ -132,9 +129,9 @@
 parse-arg _ = nothing
 
 parse : (t : Term ) → Maybe Statement 
-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
@@ -176,7 +173,7 @@
 
 ex2 = parse ex1
 
-subst-expr :  { x : Atom } → Expr  → Var x → (value : Expr ) → Expr 
+subst-expr :  { x : Term } → Expr  → Var x → (value : Expr ) → Expr 
 subst-expr  (var kX) kX v = v
 subst-expr  (var kY) kX v = var kY
 subst-expr  (var kZ) kX v = var kZ
@@ -190,7 +187,7 @@
 subst-expr  (const x₁) xv v = (const x₁)
 subst-expr  (args e e₁) xv v = args ( subst-expr e xv v ) ( subst-expr e₁ xv v ) 
 
-subst-prop :  {x : Atom } (e : Statement  ) → Var x → (value : Expr ) → Statement 
+subst-prop :  {x : Term } (e : Statement  ) → Var x → (value : Expr ) → Statement 
 subst-prop (atom x) xv v = atom x
 subst-prop (predicate x x₁) xv v = predicate x ( subst-expr x₁ xv v )
 subst-prop (and e e₁) xv v = and ( subst-prop e xv v ) ( subst-prop e₁ xv v )
@@ -199,11 +196,11 @@
 subst-prop (All x e) xv v = All x ( subst-prop e xv v )
 subst-prop (Exist x e) xv v = Exist x ( subst-prop e xv v )
 
-amap :  {x : Atom } → (px :  Pred x ) → Bool 
+amap :  {x : Term } → (px :  Pred x ) → Bool 
 amap {p} px = false
 amap {q} px = true
 amap {r} px = false
-pmap : {p : Atom } → (px :  Pred p ) → Expr → Bool 
+pmap : {p : Term } → (px :  Pred p ) → Expr → Bool 
 pmap {p} px (Logic.const kc) = true
 pmap {p}  px _ = false
 pmap {q}  px _ = false
@@ -213,7 +210,7 @@
 all0 =  const ka ∷ const kb ∷ const kc ∷ []
 
 test003 : Bool 
-test003 with parse ( ∃ X => ( p  ⟨ * X ⟩ ) )
+test003 with parse ( ∃ X => ( p  ⟨  X ⟩ ) )
 test003 | just x = Model amap pmap all0 subst-prop x
 test003 | nothing = false