fricas
(1) -> <spad>
fricas
)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]
fricas
)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
fricas
)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>
fricas
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?
fricas
)set output tex off
fricas
)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
fricas
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
fricas
m1:=assert(m>1::R)
R is not a valid type.
SUBSETS
fricas
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