(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