Edit detail for SandBoxProp revision 1 of 1

(1) -> <spad>

)abbrev domain INEQTY InEquality
++ Author: kfp
++ Date Created: Sun Oct 26 02:21:23 CEST 2014
++ License: BSD (same as Axiom)
++ Date Last Updated:
++ Basic Operations: 
++ Related Domains: 
++ Also See:
++ AMS Classifications:
++ Keywords: 
++ Examples:
++ References:
++
++ Description:
++ 
++
InEquality(S:Comparable) : Exports == Implementation where

 OF ==> OutputForm 

 Exports == Join(Comparable , CoercibleTo OutputForm) with

 "<" : (S,S) -> %
 ++ < means lesser than

 "<=" : (S,S) -> %
 ++ <= means lesser than or equal

 ">" : (S,S) -> %
 ++ > means greater than

 ">=" : (S,S) -> %
 ++ >= means greater than or equal

 eql : (S,S) -> %
 ++ = means equal

 neq : (S,S) -> %
 ++ neq means not equal.

 lhs : % -> S
 ++ lhs returns the left hand side of the inequality

 rhs : % -> S
 ++ rhs returns the right hand side of the inequality

 rel : % -> Symbol
 ++ rel returns the inequality (relation) symbol 

 converse : % -> %
 ++ converse inequality 

 coerce : % -> OF
 ++ coerce to output form

 Implementation == add 

 Rep := Record(rel:Symbol , lhs : S, rhs : S)

 s:List(Symbol):=['<,'<=,'>,'>=,'=,'~=]

 l:S < r:S == [s.1, l, r]$Rep
 l:S <= r:S == [s.2, l, r]$Rep
 l:S > r:S == [s.3, l, r]$Rep
 l:S >= r:S == [s.4, l, r]$Rep
 eql(l:S,r:S) == [s.5, l, r]$Rep
 neq(l:S,r:S) == [s.6, l, r]$Rep

 lhs x == x.lhs
 rhs x == x.rhs
 rel x == x.rel

 converse x == 
 x.rel = s.1 => [s.3, x.rhs, x.lhs]$Rep
 x.rel = s.2 => [s.4, x.rhs, x.lhs]$Rep
 x.rel = s.3 => [s.1, x.rhs, x.lhs]$Rep
 x.rel = s.4 => [s.2, x.rhs, x.lhs]$Rep
 x.rel = s.5 => [s.5, x.rhs, x.lhs]$Rep
 x.rel = s.6 => [s.6, x.rhs, x.lhs]$Rep

 coerce(x:%):OF == 
 hconcat [x.lhs::OF," ", x.rel::OF, " ", x.rhs::OF] 

)abbrev domain PROP Prop
++ Prop is the domain of Propositions over a type T
Prop(T:Comparable) : Exports == Implementation where

 S ==> Symbol
 PI ==> PositiveInteger
 EQT ==> InEquality(T)
 TT ==> Union(S,T,PI,EQT)

 Exports == with

 assert : InEquality(T) -> %
 ++ assert an equation of type InEquality(T)
 assert : Equation(T) -> %
 ++ assert an equation of type Equation(T) (convenience) 
 And : (%,%) -> %
 ++ And means the logical connective 'and'
 Or : (%,%) -> %
 ++ Or means the logical connective 'or'
 Imp : (%,%) -> %
 ++ Imp means the logical connective 'implies'
 Eqv : (%,%) -> %
 ++ Eqv means the logical connective 'equivalent'
 Not : % -> %
 ++ Not means negation 'not'
 All : (Symbol,%) -> %
 ++ All means the universal quantifier 'forall'
 Ex : (Symbol,%) -> %
 ++ Ex means the existential quantifier 'exists'

 coerce : % -> OutputForm
 ++ coerce to output form

 qvars : % -> List(TT)
 ++ qvars lists all quantifier variables

 nnf : % -> %
 ++ nnf means negation normal form 'nnf'

 Implementation == add -- BinaryTree(TT) add 

 Rep := BinaryTree(TT)

 -- map x in TT to Rep
 iD(x:TT):% == binaryTree(x)$Rep

 rs:List(Symbol):=['<,'<=,'>,'>=,'=,'~=]

 -----------------------
 -- Op id's
 -- 1 ..... and
 -- 2 ..... or
 -- 3 ..... implies
 -- 4 ..... equivalent
 -- 5 ..... not
 -- 6 ..... forall
 -- 7 ..... exists
 -- 8,9 .... reserved
 -- 10 ..... equality
 -- 11 ..... neq
 -- 12 ..... lt
 -- 13 ..... leq
 -- 14 ..... gt
 -- 15 ..... geq
 -----------------------

 -- assert an element of type Equation(T)
 assert(s:Equation(T)):% == binaryTree(iD lhs s,10,iD rhs s)$Rep

 assert(s:EQT):% == 
 rel s = rs.1 => binaryTree(iD lhs s,12,iD rhs s)$Rep
 rel s = rs.2 => binaryTree(iD lhs s,13,iD rhs s)$Rep
 rel s = rs.3 => binaryTree(iD lhs s,14,iD rhs s)$Rep
 rel s = rs.4 => binaryTree(iD lhs s,15,iD rhs s)$Rep
 rel s = rs.5 => binaryTree(iD lhs s,10,iD rhs s)$Rep
 rel s = rs.6 => binaryTree(iD lhs s,11,iD rhs s)$Rep

 -- variable, the only nodes without left/right
 var(x:S):% == binaryTree(x)$Rep

 And(p:%,q:%):% == binaryTree(p,1,q)$Rep
 Or (p:%,q:%):% == binaryTree(p,2,q)$Rep
 Imp(p:%,q:%):% == binaryTree(p,3,q)$Rep
 Eqv(p:%,q:%):% == binaryTree(p,4,q)$Rep

 Not(p:%):% == binaryTree(p,5,empty())$Rep

 All(x:S,p:%):% == binaryTree(var x,6,p)$Rep
 Ex (x:S,p:%):% == binaryTree(var x,7,p)$Rep

 coerce(p) == 
 OF ==> OutputForm
 lp:OF:="("
 rp:OF:=")"
 lb:OF:="{"
 rb:OF:="}"
 lk:OF:="["
 rk:OF:="]"
 of:OF:=""
 s0:OF:="."
 s1:OF:=" & "
 s2:OF:=" | "
 s3:OF:=" => "
 s4:OF:=" <=> "
 s5:OF:="~"
 s6:OF:="\"
 s7:OF:="?"
 s10:OF:=" = "
 s11:OF:=" ~= "
 s12:OF:=" < "
 s13:OF:=" <= "
 s14:OF:=" > "
 s15:OF:=" >= "
 empty? p => of
 val:= value p
 val=1 => of:=hconcat [of,lp,coerce(left p),s1,coerce(right p),rp]
 val=2 => of:=hconcat [of,lp,coerce(left p),s2,coerce(right p),rp]
 val=3 => of:=hconcat [of,lp,coerce(left p),s3,coerce(right p),rp]
 val=4 => of:=hconcat [of,lp,coerce(left p),s4,coerce(right p),rp]
 val=5 => of:=hconcat [of,s5,lp,coerce(left p),rp]
 val=6 => of:=hconcat [of,s6,coerce(left p),s0,lk,coerce(right p),rk]
 val=7 => of:=hconcat [of,s7,coerce(left p),s0,lk,coerce(right p),rk]
 val=10=> of:=hconcat [of,lb,coerce(left p),s10,coerce(right p),rb] 
 val=11=> of:=hconcat [of,lb,coerce(left p),s11,coerce(right p),rb] 
 val=12=> of:=hconcat [of,lb,coerce(left p),s12,coerce(right p),rb] 
 val=13=> of:=hconcat [of,lb,coerce(left p),s13,coerce(right p),rb] 
 val=14=> of:=hconcat [of,lb,coerce(left p),s14,coerce(right p),rb] 
 val=15=> of:=hconcat [of,lb,coerce(left p),s15,coerce(right p),rb] 
 of:=hconcat[of,val::OF]
 of

 --local 
 mvNot(p:%):% ==
 val := value p
 val=1 => Or(Not(left p),Not(right p))::Rep
 val=2 => And(Not(left p),Not(right p))::Rep
 val=3 => And(left p, Not(right p))::Rep
 val=4 => Not(Or(And(left p,right p),And(Not(left p),Not(right p))))
 val=5 => (left p)::Rep
 val=6 => Ex(value(left p)::S, Not(right p))::Rep
 val=7 => All(value(left p)::S, Not(right p))::Rep
 val=10 => binaryTree(left p,11,right p)$Rep
 val=11 => binaryTree(left p,10,right p)$Rep
 val=12 => binaryTree(left p,15,right p)$Rep
 val=13 => binaryTree(left p,14,right p)$Rep
 val=14 => binaryTree(left p,13,right p)$Rep
 val=15 => binaryTree(left p,12,right p)$Rep
 p::Rep

 nnf(p:%):% ==
 empty? p => p::Rep
 val := value p
 val=1 => And(nnf(left p),nnf(right p))
 val=2 => Or(nnf(left p),nnf(right p))
 val=3 => nnf(Or(Not(left p),right p))
 val=4 => nnf(And(Or(left p,Not(right p)),Or(Not(left p),right p)))
 val=5 => nnf(mvNot(left p))
 val=6 => All(value(left p)::S, nnf(right p))
 val=7 => Ex(value(left p)::S, nnf(right p))
 p::Rep

 qvars(p:%):List(TT) == 
 L:List(TT):=[]
 empty? p => []::List(TT)
 val := value p
 if (val case S) then
 L:=append(L,[val])
 else
 L:=append(L,qvars(left p))
 L:=append(L,qvars(right p))
 L

 

)abbrev domain SUBSET SubsetOf
++ Author: kfp
++ Date Created: Mon Nov 03 20:41:24 CET 2014
++ License: BSD (same as Axiom)
++ Date Last Updated:
++ Basic Operations: 
++ Related Domains: 
++ Also See:
++ AMS Classifications:
++ Keywords: 
++ Examples:
++ References:
++
++ Description:
++ 
++
SubsetOf(T:Comparable) : Exports == Implementation where

 OF ==> OutputForm

 Exports == Join(Comparable , CoercibleTo OutputForm) with

 setOfAll : (List Symbol, Prop T ) -> %

 member? : (List T,%) -> Boolean

 coerce : % -> OutputForm

 Implementation == Prop(T) add 

 Rep := Record(s:List Symbol, p:Prop T)

 setOfAll(ls,P) == [ls,P]::Rep

 member?(t,ss) == false

 coerce(ss:%):OF ==
 r:=ss::Rep
 sym:OF:=(r.s)::OF
 prop:OF:=(r.p)::OF
 hconcat ["Set of all "::OF, sym," such that "::OF, prop]</spad>

Compiling FriCAS source code from file 
 /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8617047757752040298-25px001.spad
 using old system compiler.
 INEQTY abbreviates domain InEquality 
------------------------------------------------------------------------
 initializing NRLIB INEQTY for InEquality 
 compiling into NRLIB INEQTY 
 compiling exported < : (S,S) -> %
Time: 0.01 SEC.

 compiling exported <= : (S,S) -> %
Time: 0 SEC.

 compiling exported > : (S,S) -> %
Time: 0 SEC.

 compiling exported >= : (S,S) -> %
Time: 0 SEC.

 compiling exported eql : (S,S) -> %
Time: 0 SEC.

 compiling exported neq : (S,S) -> %
Time: 0 SEC.

 compiling exported lhs : % -> S
 INEQTY;lhs;%S;7 is replaced by QVELTx1 
Time: 0 SEC.

 compiling exported rhs : % -> S
 INEQTY;rhs;%S;8 is replaced by QVELTx2 
Time: 0 SEC.

 compiling exported rel : % -> Symbol
 INEQTY;rel;%S;9 is replaced by QVELTx0 
Time: 0 SEC.

 compiling exported converse : % -> %
Time: 0 SEC.

 compiling exported coerce : % -> OutputForm
****** comp fails at level 3 with expression: ******
error in function coerce 

(|hconcat|
 (|construct| | << | (|::| (|x| |lhs|) (|OutputForm|)) | >> | " "
 (|::| (|x| |rel|) (|OutputForm|)) " "
 (|::| (|x| |rhs|) (|OutputForm|))))
****** level 3 ******
$x:= (:: (x lhs) (OutputForm))
$m:= (Symbol)
$f:=
((((|x| # #) (|s| # #) (|#| #) (< #) ...)))

 >> Apparent user error:
 Cannot coerce (call (ELT % 24) (call (XLAM (1ドル 2ドル) (RECORDELT 1ドル 1 3)) x (QUOTE lhs))) 
 of mode (OutputForm) 
 to mode (Symbol)

InEq?

)set output tex off
 

)set output algebra on

x>0

 There are 1 exposed and 2 unexposed library operations named > 
 having 2 argument(s) but none was determined to be applicable. 
 Use HyperDoc Browse, or issue
 )display op >
 to learn more about the available operations. Perhaps 
 package-calling the operation or using coercions on the arguments
 will allow you to apply the operation.

 Cannot find a definition or applicable library operation named > 
 with argument type(s) 
 Variable(x)
 NonNegativeInteger

 Perhaps you should use "@" to indicate the required return type, 
 or "$" to specify which version of the function you need.

Propositions

assert(P1)

 There are no library operations named assert having 1 argument(s) 
 though there are 1 exposed operation(s) and 0 unexposed 
 operation(s) having a different number of arguments. Use HyperDoc
 Browse, or issue
 )what op assert
 to learn what operations contain " assert " in their names, or 
 issue
 )display op assert
 to learn more about the available operations.

 Cannot find a definition or applicable library operation named 
 assert with argument type(s) 
 Variable(P1)

 Perhaps you should use "@" to indicate the required return type, 
 or "$" to specify which version of the function you need.

NNF

m1:=assert(m>1::R)

 R is not a valid type.

SUBSETS

setOfAll([x,y,z],assert(x^2+y^2+z^2<=1))

 There are 2 exposed and 1 unexposed library operations named <= 
 having 2 argument(s) but none was determined to be applicable. 
 Use HyperDoc Browse, or issue
 )display op <=
 to learn more about the available operations. Perhaps 
 package-calling the operation or using coercions on the arguments
 will allow you to apply the operation.

 Cannot find a definition or applicable library operation named <= 
 with argument type(s) 
 Polynomial(Integer)
 PositiveInteger

 Perhaps you should use "@" to indicate the required return type, 
 or "$" to specify which version of the function you need.

-- continue with NatDed?/Solve/RSPACE/Cell/Interval/Surface(k) , requires: CAD