**** ************************************************************************************************* **** ************************************************************************************************* **** ************************************************************************************************* *** February 2016 *** **** ************************************************************************************************* **** ************************************************************************************************* **** ************************************************************************************************* *** CORE *** **** ************************************************************************************************* **** ************************************************************************************************* **** ************************************************************************************************* --- ------------------------------------------------------------------------- fmod #LIBRARY# is inc META-LEVEL . inc CONVERSION . sort Sentence SentenceSet . subsort Sentence < SentenceSet . --- ------------------------------------------------------------------------- vars V V' : Variable . var Ct : Constant . vars T T' T1 T2 : Term . vars AS ASet AtSet : AttrSet . var A : Attr . vars St : Sort . vars TL Tl : TermList . vars NTL NTl : NeTermList . var EC : EqCondition . var Co : Condition . vars ES ESet : EquationSet . vars MS MSet : MembAxSet . vars RS RSet : RuleSet . vars SS SSet : SentenceSet . vars Sen Sen' : Sentence . vars E E' : Equation . vars Mx Mx' : MembAx . vars R R' : Rule . --- ------------------------------------------------------------------------- op eq_=_[_]; : Term Term AttrSet -> Sentence [ctor] . op ceq_=_if_[_]; : Term Term EqCondition AttrSet -> Sentence[ctor] . --- op mb_:_[_]; : Term Sort AttrSet -> Sentence[ctor]. op cmb_:_if_[_]; : Term Sort EqCondition AttrSet -> Sentence[ctor] . --- op rl_=>_[_]; : Term Term AttrSet -> Sentence [ctor]. op crl_=>_if_[_]; : Term Term Condition AttrSet -> Sentence [ctor]. --- op none : -> SentenceSet [ctor] . op __ : SentenceSet SentenceSet -> SentenceSet [ctor assoc comm id: none]. --- ------------------------------------------------------------------------- --- Equation to Sentence --- --- ------------------------------------------------------------------------- op conv : EquationSet -> SentenceSet . eq conv((none).EquationSet) = none . eq conv(eq T = T' [ASet]. ESet) = eq T = T' [ASet]; conv(ESet) . eq conv(ceq T = T' if EC[ASet]. ESet) = ceq T = T' if EC[ASet]; conv(ESet) . op conv : MembAxSet -> SentenceSet . eq conv((none).MembAxSet) = none . eq conv(mb T : St [ASet]. MSet) = mb T : St [ASet]; conv(MSet) . eq conv(cmb T : St if EC[ASet]. MSet) = cmb T : St if EC[ASet]; conv(MSet) . op conv : RuleSet -> SentenceSet . eq conv((none).RuleSet) = none . eq conv(rl T => T' [ASet]. RSet) = rl T => T' [ASet]; conv(RSet) . eq conv(crl T => T' if Co[ASet]. RSet) = crl T => T' if Co[ASet]; conv(RSet) . --- ------------------------------------------------------------------------- --- Sentence to Equation --- --- ------------------------------------------------------------------------- op convE : SentenceSet -> EquationSet . eq convE((none).SentenceSet) = (none).EquationSet . eq convE(eq T = T' [ASet]; SSet) = eq T = T' [ASet]. convE(SSet) . eq convE(ceq T = T' if EC[ASet]; SSet) = ceq T = T' if EC[ASet]. convE(SSet) . eq convE(Sen SSet) = convE(SSet) [owise]. --- ------------------------------------------------------------------------- --- Sentence to MembAx --- --- ------------------------------------------------------------------------- op convM : SentenceSet -> MembAxSet . eq convM((none).SentenceSet) = (none).MembAxSet . eq convM(mb T : St [ASet]; SSet) = mb T : St [ASet]. convM(SSet) . eq convM(cmb T : St if EC[ASet]; SSet) = cmb T : St if EC[ASet]. convM(SSet). eq convM(Sen SSet) = convM(SSet) [owise]. --- ------------------------------------------------------------------------- --- Sentence to Rule --- --- ------------------------------------------------------------------------- op convR : SentenceSet -> RuleSet . eq convR((none).SentenceSet) = (none).RuleSet . eq convR(rl T => T' [ASet]; SSet) = rl T => T' [ASet]. convR(SSet) . eq convR(crl T => T' if Co[ASet]; SSet) = crl T => T' if Co[ASet]. convR(SSet) . eq convR(Sen SSet) = convR(SSet) [owise]. --- ------------------------------------------------------------------------- --- add operations to module --- --- ------------------------------------------------------------------------- vars M M' : Module . var H : Header . var IList : ImportList . vars Q Q' : Qid . var StSet : SortSet . var SbSet : SubsortDeclSet . vars Op Od : OpDecl . vars OdSet OSet : OpDeclSet . var Tp : Type . var TpL : TypeList . var F : FindResult . var Str : String . var N : Nat . var Subst : Substitution . --- ------------------------------------------------------------------------- op addOp : Module OpDeclSet -> Module . eq addOp((fmod H is IList sorts StSet . SbSet OdSet MSet ESet endfm),OSet) = (fmod H is IList sorts StSet . SbSet overwrite(OdSet, OSet) MSet ESet endfm) . eq addOp((fth H is IList sorts StSet . SbSet OdSet MSet ESet endfth),OSet) = (fth H is IList sorts StSet . SbSet overwrite(OdSet, OSet) MSet ESet endfth) . eq addOp((mod H is IList sorts StSet . SbSet OdSet MSet ESet RSet endm),OSet) = (mod H is IList sorts StSet . SbSet overwrite(OdSet, OSet) MSet ESet RSet endm) . eq addOp((th H is IList sorts StSet . SbSet OdSet MSet ESet RSet endth),OSet) = (th H is IList sorts StSet . SbSet overwrite(OdSet, OSet) MSet ESet RSet endth) . --- op overwrite : OpDeclSet OpDeclSet -> OpDeclSet . eq overwrite( (op Q : TpL -> Tp [AtSet] .) OdSet, (op Q : TpL -> Tp [ASet] .) OSet) = overwrite(OdSet,(op Q : TpL -> Tp [ASet] .) OSet) . eq overwrite(OdSet,OSet) = OdSet OSet [owise] . --- ------------------------------------------------------------------------- --- add sentences to a module --- --- ------------------------------------------------------------------------- op addSen : Module SentenceSet -> Module . eq addSen(M,none) = M . --- Eqs --- eq addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),eq T = T' [ASet]; SSet) = if T == T' then addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),SSet) else addSen((fmod H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) ESet) endfm),SSet) fi . eq addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),eq T = T' [ASet]; SSet) = if T == T' then addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),SSet) else addSen((fth H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) ESet) endfth),SSet) fi . eq addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),eq T = T' [ASet]; SSet) = if T == T' then addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) ESet) RSet endm),SSet) fi . eq addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),eq T = T' [ASet]; SSet) = if T == T' then addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) ESet) RSet endth),SSet) fi . --- eq addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),ceq T = T' if EC [ASet]; SSet) = if T == T' then addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),SSet) else if EC == nil then addSen((fmod H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) ESet) endfm),SSet) else addSen((fmod H is IList sorts StSet . SbSet OSet MSet ((ceq T = T' if EC [ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) ESet) endfm),SSet) fi fi . eq addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),ceq T = T' if EC [ASet]; SSet) = if T == T' then addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),SSet) else if EC == nil then addSen((fth H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) ESet) endfth),SSet) else addSen((fth H is IList sorts StSet . SbSet OSet MSet ((ceq T = T' if EC[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) ESet) endfth),SSet) fi fi . eq addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),ceq T = T' if EC[ASet]; SSet) = if T == T' then addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),SSet) else if EC == nil then addSen((mod H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) ESet) RSet endm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet MSet ((ceq T = T' if EC [ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) ESet) RSet endm),SSet) fi fi . eq addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),ceq T = T' if EC [ASet]; SSet) = if T == T' then addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),SSet) else if EC == nil then addSen((th H is IList sorts StSet . SbSet OSet MSet ((eq T = T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) ESet) RSet endth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet MSet ((ceq T = T' if EC [ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) ESet) RSet endth),SSet) fi fi . --- MembAx --- eq addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),mb T : St [ASet]; SSet) = addSen((fmod H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) MSet) ESet endfm),SSet) . eq addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),mb T : St [ASet]; SSet) = addSen((fth H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) MSet) ESet endfth),SSet) . eq addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),mb T : St [ASet]; SSet) = addSen((mod H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) MSet) ESet RSet endm),SSet) . eq addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),mb T : St [ASet]; SSet) = addSen((th H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) MSet) ESet RSet endth),SSet) . --- eq addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),cmb T : St if EC[ASet]; SSet) = if EC == nil then addSen((fmod H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) MSet) ESet endfm),SSet) else addSen((fmod H is IList sorts StSet . SbSet OSet ((cmb T : St if EC[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) MSet) ESet endfm),SSet) fi . eq addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),cmb T : St if EC[ASet]; SSet) = if EC == nil then addSen((fth H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) MSet) ESet endfth),SSet) else addSen((fth H is IList sorts StSet . SbSet OSet ((cmb T : St if EC[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) MSet) ESet endfth),SSet) fi . eq addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),cmb T : St if EC[ASet]; SSet) = if EC == nil then addSen((mod H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) MSet) ESet RSet endm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet ((cmb T : St if EC[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) MSet) ESet RSet endm),SSet) fi . eq addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),cmb T : St if EC[ASet]; SSet) = if EC == nil then addSen((th H is IList sorts StSet . SbSet OSet ((mb T : St[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) MSet) ESet RSet endth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet ((cmb T : St if EC[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) MSet) ESet RSet endth),SSet) fi . --- Rule --- eq addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),rl T => T' [ASet]; SSet) = if T == T' then addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) endm),SSet) fi . eq addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),rl T => T' [ASet]; SSet) = if T == T' then addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].) endth),SSet) fi . eq addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),rl T => T' [ASet]; SSet) = if T == T' then addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) RSet endm),SSet) fi . eq addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),rl T => T' [ASet]; SSet) = if T == T' then addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) RSet endth),SSet) fi . --- eq addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),crl T => T' if Co[ASet]; SSet) = if T == T' then addSen((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),SSet) else if Co == nil then addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].)endm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet (crl T => T' if Co[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].)endm),SSet) fi fi . eq addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),crl T => T' if Co[ASet]; SSet) = if T == T' then addSen((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),SSet) else if Co == nil then addSen((th H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].)endth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet MSet ESet (crl T => T' if Co[ASet metadata(string(getLabel(conv(MSet) conv(ESet))+ 1,10))].)endth),SSet) fi fi . eq addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),crl T => T' if Co[ASet]; SSet) = if T == T' then addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),SSet) else if Co == nil then addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) RSet endm),SSet) else addSen((mod H is IList sorts StSet . SbSet OSet MSet ESet (crl T => T' if Co[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) RSet endm),SSet) fi fi . eq addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),crl T => T' if Co[ASet]; SSet) = if T == T' then addSen((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),SSet) else if Co == nil then addSen((th H is IList sorts StSet . SbSet OSet MSet ESet (rl T => T'[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) RSet endth),SSet) else addSen((th H is IList sorts StSet . SbSet OSet MSet ESet (crl T => T' if Co[ASet metadata(string(getLabel(conv(MSet) conv(ESet) conv(RSet))+ 1,10))].) RSet endth),SSet) fi fi . --- ------------------------------------------------------------------------- op getSentence : Module String -> SentenceSet . eq getSentence(M,Str)= getSentence(conv(getEqs(M))conv(getMbs(M))conv(getRls(M)),Str). --- ------------------------------------------------------------------------- op getSentence : SentenceSet String -> SentenceSet . --- ------------------------------------------------------------------------- eq getSentence((none).SentenceSet,Str) = (none).SentenceSet . eq getSentence(eq T1 = T2[metadata(Str) AS]; SS,Str) = eq T1 = T2[AS]; getSentence(SS,Str). eq getSentence(ceq T1 = T2 if EC[metadata(Str) AS]; SS,Str) = ceq T1 = T2 if EC[AS]; getSentence(SS,Str). eq getSentence(mb T : St[metadata(Str) AS]; SS,Str) = mb T : St[AS]; getSentence(SS,Str). eq getSentence(cmb T : St if EC[metadata(Str) AS]; SS,Str) = cmb T : St if EC[AS]; getSentence(SS,Str). eq getSentence(rl T1 => T2[metadata(Str) AS]; SS,Str) = rl T1 => T2[AS]; getSentence(SS,Str). eq getSentence(crl T1 => T2 if Co[metadata(Str) AS]; SS,Str) = crl T1 => T2 if Co[AS]; getSentence(SS,Str). eq getSentence(Sen SS,Str) = getSentence(SS,Str)[owise]. --- ------------------------------------------------------------------------- --- label --- --- ------------------------------------------------------------------------- op getLabel : AttrSet -> Nat . eq getLabel(AS) = getLabel(AS,0). op getLabel : AttrSet Nat -> Nat . eq getLabel((none).AttrSet,N) = N . eq getLabel(metadata(Str) AS,N) = if rat(Str,10) :: Nat then if N < rat(Str,10) then getLabel(AS,rat(Str,10)) else getLabel(AS,N) fi else getLabel(AS,N) fi . --- eq getLabel(A AS,N) = getLabel(AS,N)[owise]. --- ------------------------------------------------------------------------- op getLabel : SentenceSet -> Nat . eq getLabel(SSet) = getLabel(SSet,0). --- ------------------------------------------------------------------------- op getLabel : SentenceSet Nat -> Nat . eq getLabel((none).SentenceSet,N) = N . --- eq getLabel(eq T = T'[AS]; SSet, N) = if N < getLabel(AS) then getLabel(SSet,getLabel(AS)) else getLabel(SSet,N) fi . --- eq getLabel(ceq T = T' if EC[AS]; SSet, N) = if N < getLabel(AS) then getLabel(SSet,getLabel(AS)) else getLabel(SSet,N) fi . --- eq getLabel(mb T : St[AS]; SSet, N) = if N < getLabel(AS) then getLabel(SSet,getLabel(AS)) else getLabel(SSet,N) fi . --- eq getLabel(cmb T : St if EC[AS]; SSet, N) = if N < getLabel(AS) then getLabel(SSet,getLabel(AS)) else getLabel(SSet,N) fi . --- eq getLabel(rl T => T'[AS]; SSet, N) = if N < getLabel(AS) then getLabel(SSet,getLabel(AS)) else getLabel(SSet,N) fi . --- eq getLabel(crl T => T' if Co[AS]; SSet, N) = if N < getLabel(AS) then getLabel(SSet,getLabel(AS)) else getLabel(SSet,N) fi . --- ------------------------------------------------------------------------- op getLabel : Module -> Nat . eq getLabel(M) = getLabel(conv(getEqs(M)) conv(getMbs(M)) conv(getRls(M))). --- ------------------------------------------------------------------------- --- inc & in --- --- ------------------------------------------------------------------------- op _inc_ : SentenceSet Module -> Bool . eq SSet inc M = (convE(SSet) inc getEqs(M)) and (convM(SSet) inc getMbs(M)) and (convR(SSet) inc getRls(M)). --- ------------------------------------------------------------------------- op _inc_ : EquationSet EquationSet -> Bool . eq (none).EquationSet inc ESet = true . eq (E ES) inc ESet = (E in ESet) and (ES inc ESet). op _inc_ : MembAxSet MembAxSet -> Bool . eq (none).MembAxSet inc MSet = true . eq (Mx MS) inc MSet = (Mx in MSet) and (MS inc MSet). op _inc_ : RuleSet RuleSet -> Bool . eq (none).RuleSet inc RSet = true . eq (R RS) inc RSet = (R in RSet) and (RS inc RSet). --- ------------------------------------------------------------------------- op _in_ : Equation EquationSet -> Bool . eq (eq T = T'[AS].) in (eq T = T'[ASet].) ES = true . eq (ceq T = T' if EC[AS].) in (ceq T = T' if EC[ASet].) ES = true . eq E in ES = false [owise]. op _in_ : MembAx MembAxSet -> Bool . eq (mb T : St[AS].) in (mb T : St[ASet].) MS = true . eq (cmb T : St if EC[AS].) in (cmb T : St if EC[ASet].) MS = true . eq Mx in MS = false [owise]. op _in_ : Rule RuleSet -> Bool . eq (rl T => T'[AS].) in (rl T => T'[ASet].) RS = true . eq (crl T => T' if Co[AS].) in (crl T => T' if Co[ASet].) RS = true . eq R in RS = false [owise]. --- ------------------------------------------------------------------------- --- index --- --- ------------------------------------------------------------------------- op index : Qid -> Nat . ceq index(Q) = if F :: Nat then (if find(substr(Str, s F,length(Str)),"#",0) :: Nat then index(qid(substr(Str,s F,length(Str)))) else (if rat(substr(Str,s F,length(Str)),10) :: Nat then rat(substr(Str,s F,length(Str)),10) else 0 fi) fi) else 0 fi if Str := string(Q) /\ F := find(Str,"#",0). --- Term --- op maxIndex : Term -> Nat . eq maxIndex(Ct) = index(getName(Ct)). eq maxIndex(V) = index(getName(V)). eq maxIndex(Q[NTL]) = maxIndex(NTL). --- Term list --- op maxIndex : TermList -> Nat . eq maxIndex((empty).TermList) = 0 . eq maxIndex((T,NTL)) = if maxIndex(NTL) <= maxIndex(T) then maxIndex(T) else maxIndex(NTL) fi . --- Eqs --- op maxIndex : EquationSet -> Nat . eq maxIndex((none).EquationSet) = 0 . eq maxIndex(eq T = T'[ASet].) = if maxIndex(T) <= maxIndex(T') then maxIndex(T') else maxIndex(T) fi . --- eq maxIndex(ceq T = T' if EC[ASet].) = if maxIndex(T) <= maxIndex(T') then if maxIndex(EC) <= maxIndex(T') then maxIndex(T') else maxIndex(EC) fi else if maxIndex(EC) <= maxIndex(T) then maxIndex(T) else maxIndex(EC) fi fi . --- ceq maxIndex(E ESet) = if maxIndex(ESet) <= maxIndex(E) then maxIndex(E) else maxIndex(ESet) fi if ESet =/= (none).EquationSet . --- Mbs --- op maxIndex : MembAxSet -> Nat . eq maxIndex((none).MembAxSet) = 0 . eq maxIndex(mb T : St[ASet].) = maxIndex(T). --- eq maxIndex(cmb T : St if EC[ASet].) = if maxIndex(EC) <= maxIndex(T) then maxIndex(T) else maxIndex(EC) fi . --- ceq maxIndex(Mx MSet) = if maxIndex(MSet) <= maxIndex(Mx) then maxIndex(Mx) else maxIndex(MSet) fi if MSet =/= (none).MembAxSet . --- Rls --- op maxIndex : RuleSet -> Nat . eq maxIndex((none).RuleSet) = 0 . eq maxIndex(rl T => T'[ASet].) = if maxIndex(T) <= maxIndex(T') then maxIndex(T') else maxIndex(T) fi . --- eq maxIndex(crl T => T' if Co[ASet].) = if maxIndex(T) <= maxIndex(T') then if maxIndex(Co) <= maxIndex(T') then maxIndex(T') else maxIndex(Co) fi else if maxIndex(Co) <= maxIndex(T) then maxIndex(T) else maxIndex(Co) fi fi . --- ceq maxIndex(R RSet) = if maxIndex(RSet) <= maxIndex(R) then maxIndex(R) else maxIndex(RSet) fi if RSet =/= (none).RuleSet . --- Condition --- op maxIndex : Condition -> Nat . eq maxIndex((nil).EqCondition) = 0 . eq maxIndex(T = T' /\ Co) = if maxIndex(T) <= maxIndex(T') then if maxIndex(Co) <= maxIndex(T') then maxIndex(T') else maxIndex(Co) fi else if maxIndex(Co) <= maxIndex(T) then maxIndex(T) else maxIndex(Co) fi fi . --- eq maxIndex(T := T' /\ Co) = if maxIndex(T) <= maxIndex(T') then if maxIndex(Co) <= maxIndex(T') then maxIndex(T') else maxIndex(Co) fi else if maxIndex(Co) <= maxIndex(T) then maxIndex(T) else maxIndex(Co) fi fi . --- eq maxIndex(T : St /\ Co) = if maxIndex(T) <= maxIndex(Co) then maxIndex(Co) else maxIndex(T) fi . --- eq maxIndex(T => T' /\ Co) = if maxIndex(T) <= maxIndex(T') then if maxIndex(Co) <= maxIndex(T') then maxIndex(T') else maxIndex(Co) fi else if maxIndex(Co) <= maxIndex(T) then maxIndex(T) else maxIndex(Co) fi fi . --- Operation decl. set --- op maxIndex : OpDeclSet -> Nat . eq maxIndex((none).OpDeclSet) = 0 . eq maxIndex(op Q : TpL -> Tp [ASet].) = index(Q). eq maxIndex(Op Od OSet) = if (maxIndex(Op) <= maxIndex(Od)) then maxIndex(Od OSet) else maxIndex(Op OSet) fi . --- ------------------------------------------------------------------------- --- index of a module --- --- ------------------------------------------------------------------------- op maxIndex : Module -> Nat . eq maxIndex(M) = if maxIndex(getOps(M)) <= maxIndex(getEqs(M)) then if maxIndex(getEqs(M)) <= maxIndex(getMbs(M)) then if maxIndex(getMbs(M)) <= maxIndex(getRls(M)) then maxIndex(getRls(M)) else maxIndex(getMbs(M)) fi else if maxIndex(getEqs(M)) <= maxIndex(getRls(M)) then maxIndex(getRls(M)) else maxIndex(getEqs(M)) fi fi else if maxIndex(getOps(M)) <= maxIndex(getMbs(M)) then if maxIndex(getMbs(M)) <= maxIndex(getRls(M)) then maxIndex(getRls(M)) else maxIndex(getMbs(M)) fi else if maxIndex(getOps(M)) <= maxIndex(getRls(M)) then maxIndex(getRls(M)) else maxIndex(getOps(M)) fi fi fi . --- ------------------------------------------------------------------------- --- get variables of equation --- --- ------------------------------------------------------------------------- op _U_ : TermList TermList -> TermList [assoc]. eq Tl U (empty).TermList = Tl . eq Tl U (T,TL) = if T in Tl then Tl U TL else (Tl,T) U TL fi . --- ------------------------------------------------------------------------- op _in_ : Term TermList -> Bool . eq T in empty = false . eq T in (T',TL) = if T == T' then true else T in TL fi . --- ------------------------------------------------------------------------- op getVar : Term -> TermList . eq getVar(V) = V . eq getVar(Ct) = empty . eq getVar(Q[TL]) = getVar(TL) . --- ------------------------------------------------------------------------- op getVar : TermList -> TermList . eq getVar(empty) = empty . ceq getVar((T,TL)) = getVar(T) U getVar(TL) if TL =/= (empty).TermList . --- ------------------------------------------------------------------------- op getVar : SentenceSet -> TermList . eq getVar((none).SentenceSet) = (empty).TermList . --- Equation --- eq getVar(eq T = T'[ASet]; SSet) = getVar(T) U getVar(T') U getVar(SSet) . eq getVar(ceq T = T' if EC [ASet]; SSet) = getVar(T) U getVar(T') U getVar(EC) U getVar(SSet). --- MembAx --- eq getVar(mb T : St[ASet]; SSet) = getVar(T) U getVar(SSet). eq getVar(cmb T : St if EC [ASet]; SSet) = getVar(T) U getVar(EC) U getVar(SSet). --- Rule --- eq getVar(rl T => T'[ASet]; SSet) = getVar(T) U getVar(T') U getVar(SSet). eq getVar(crl T => T' if Co[ASet]; SSet) = getVar(T) U getVar(T') U getVar(Co) U getVar(SSet). --- ------------------------------------------------------------------------- op getVar : Condition -> TermList . eq getVar((nil).EqCondition) = (empty).TermList . eq getVar(T = T' /\ Co) = getVar(T) U getVar(T') U getVar(Co) . eq getVar(T := T' /\ Co) = getVar(T) U getVar(T') U getVar(Co) . eq getVar(T : St /\ Co) = getVar(T) U getVar(Co) . eq getVar(T => T' /\ Co) = getVar(T) U getVar(T') U getVar(Co) . --- ------------------------------------------------------------------------- op getVar : EquationSet -> TermList . eq getVar((none).EquationSet) = (empty).TermList . eq getVar(eq T = T'[ASet]. ESet) = getVar(T) U getVar(T') U getVar(ESet). eq getVar(ceq T = T' if EC [ASet]. ESet) = getVar(T) U getVar(T') U getVar(EC) U getVar(ESet). --- ------------------------------------------------------------------------- op getVar : MembAxSet -> TermList . eq getVar((none).MembAxSet) = (empty).TermList . eq getVar(mb T : St[ASet]. MSet) = getVar(T) U getVar(MSet). eq getVar(cmb T : St if EC [ASet]. MSet) = getVar(T) U getVar(EC) U getVar(MSet). --- ------------------------------------------------------------------------- op getVar : RuleSet -> TermList . eq getVar((none).RuleSet) = (empty).TermList . eq getVar(rl T => T'[ASet]. RSet) = getVar(T) U getVar(T') U getVar(RSet). eq getVar(crl T => T' if Co [ASet]. RSet) = (getVar(T) U getVar(T')) U getVar(Co) U getVar(RSet). --- ------------------------------------------------------------------------- --- add constants to module --- --- ------------------------------------------------------------------------- op addConst : Module TermList -> Module . eq addConst(M,empty) = M . eq addConst(M,(T,TL)) = if (T :: Constant) then addConst(addOp(M, op getName(T) : nil -> getType(T) [metadata("new")].),TL) else addConst(M,TL) fi . --- ------------------------------------------------------------------------- --- add variables to module --- --- ------------------------------------------------------------------------- op addVar : Module TermList Nat -> Module . eq addVar(M,empty,N) = M . eq addVar(M, (T,TL),N) = if (T :: Variable) then addVar(addOp(M, op qid(string(getName(T))+ "#" + string(N,10)) : nil -> getType(T)[metadata("added")].) ,TL,N + 1) else addVar(M,TL,N) fi . --- ------------------------------------------------------------------------- --- adding condition to module --- --- ------------------------------------------------------------------------- op addCond : Module Condition -> Module . ceq addCond(M,Co) = adCond(M',Co << Subst) if TL := getVar(Co) /\ Subst := v2s(TL,maxIndex(M)+ 1) /\ M' := addConst(M,TL << Subst) . --- op adCond : Module Condition -> Module . eq adCond(M,nil) = M . eq adCond(M,T = T' /\ Co) = adCond(addSen(M,eq metaRed(M,T) = metaRed(M,T')[none];),Co). eq adCond(M,T := T' /\ Co) = adCond(addSen(M,eq metaRed(M,T')= T[none];),Co). eq adCond(M,T : St /\ Co) = adCond(addSen(M,mb metaRed(M,T) : St [none];),Co). eq adCond(M,T => T' /\ Co) = adCond(addSen(M,rl metaRed(M,T) => metaRed(M,T')[none];),Co). --- ------------------------------------------------------------------------- --- convert variables to substitution --- --- ------------------------------------------------------------------------- op v2s : TermList Nat -> Substitution . eq v2s(empty,N) = none . eq v2s((V,TL),N) = (V <- qid(string(getName(V)) + "#" + string(N,10) + "." + string(getType(V)))); v2s(TL,N + 1). ceq v2s((T,TL),N) = v2s(TL,N) if not(T :: Variable). --- ------------------------------------------------------------------------- --- substitute constants for variables in sentences --- --- ------------------------------------------------------------------------- op v2c : SentenceSet Nat -> SentenceSet . eq v2c(SSet,N) = SSet << v2s(getVar(SSet),N). --- Condition --- op v2c : Condition Nat -> Condition . eq v2c(Co,N) = Co << v2s(getVar(Co),N). --- Equation --- op v2c : EquationSet Nat -> EquationSet . eq v2c(ESet,N) = ESet << v2s(getVar(ESet),N). --- MembAx --- op v2c : MembAxSet Nat -> MembAxSet . eq v2c(MSet,N) = MSet << v2s(getVar(MSet),N). --- Rule --- op v2c : RuleSet Nat -> RuleSet . eq v2c(RSet,N) = RSet << v2s(getVar(RSet),N). --- Term list --- op v2c : TermList Nat -> TermList . eq v2c(TL,N) = TL << v2s(getVar(TL),N). --- ------------------------------------------------------------------------- --- apply substitution --- --- ------------------------------------------------------------------------- op _<<_ : Term Substitution -> Term . eq T << none = T . eq V << ((V' <- T'); Subst) = if (V == V') then (T' << Subst) else (V << Subst) fi . eq Ct << Subst = Ct . eq Q[TL] << Subst = Q[TL << Subst]. --- Term list --- op _<<_ : TermList Substitution -> TermList . eq empty << Subst = empty . ceq (T, TL) << Subst = (T << Subst, TL << Subst) if TL =/= (empty).TermList . --- Sentence set --- op _<<_ : SentenceSet Substitution -> SentenceSet . eq (none).SentenceSet << Subst = (none).SentenceSet . --- eq (eq T = T' [ASet]; SSet) << Subst = (eq T << Subst = T' << Subst [ASet];) (SSet << Subst). eq (ceq T = T' if EC [ASet]; SSet) << Subst = (ceq T << Subst = T' << Subst if EC << Subst [ASet];) (SSet << Subst). --- eq (mb T : St [ASet]; SSet) << Subst = (mb T << Subst : St [ASet];) (SSet << Subst). eq (cmb T : St if EC [ASet]; SSet) << Subst = (cmb T << Subst : St if EC << Subst [ASet];) (SSet << Subst). --- eq (rl T => T' [ASet]; SSet) << Subst = (rl T << Subst => T' << Subst [ASet];) (SSet << Subst). eq (crl T => T' if Co [ASet]; SSet) << Subst = (crl T << Subst => T' << Subst if Co << Subst [ASet];) (SSet << Subst). --- Condition --- op _<<_ : Condition Substitution -> EqCondition . eq (nil).EqCondition << Subst = (nil).EqCondition . eq (T = T' /\ Co) << Subst = (T << Subst = T' << Subst) /\ (Co << Subst). eq (T := T' /\ Co) << Subst = (T << Subst := T' << Subst) /\ (Co << Subst). eq (T : St /\ Co) << Subst = (T << Subst : St) /\ (Co << Subst). eq (T => T' /\ Co) << Subst = (T << Subst => T' << Subst) /\ (Co << Subst). --- Eqs --- op _<<_ : EquationSet Substitution -> Equation . eq (none).EquationSet << Subst = (none).EquationSet . eq (eq T = T' [ASet]. ESet) << Subst = (eq T << Subst = T' << Subst [ASet].) (ESet << Subst). eq (ceq T = T' if EC [ASet]. ESet) << Subst = (ceq T << Subst = T' << Subst if EC << Subst [ASet].) (ESet << Subst). --- Mbs --- op _<<_ : MembAxSet Substitution -> MembAx . eq (none).MembAxSet << Subst = (none).MembAxSet . eq (mb T : St [ASet]. MSet) << Subst = (mb T << Subst : St [ASet].) (MSet << Subst). eq (cmb T : St if EC [ASet]. MSet) << Subst = (cmb T << Subst : St if EC << Subst [ASet].) (MSet << Subst). --- Rls --- op _<<_ : RuleSet Substitution -> Rule . eq (none).RuleSet << Subst = (none).RuleSet . eq (rl T => T' [ASet]. RSet) << Subst = (rl T << Subst => T' << Subst [ASet].) (RSet << Subst). eq (crl T => T' if Co [ASet]. RSet) << Subst = (crl T << Subst => T' << Subst if Co << Subst [ASet].)(RSet << Subst). --- ------------------------------------------------------------------------- --- metaRed --- --- ------------------------------------------------------------------------- op metaRed : Module Term -> Term . --- ------------------------------------------------------------------------- eq metaRed(M,T) = if metaReduce(M,T) :: ResultPair then getTerm(metaReduce(M,T)) else T fi . --- ------------------------------------------------------------------------- op metaRed : Module SentenceSet -> SentenceSet . --- ------------------------------------------------------------------------- eq metaRed(M,(none).SentenceSet) = (none).SentenceSet . eq metaRed(M,eq T = T' [ASet]; SSet) = (eq metaRed(M,T) = metaRed(M,T') [ASet];) metaRed(M,SSet). eq metaRed(M,ceq T = T' if EC [ASet]; SSet) = (ceq metaRed(M,T) = metaRed(M,T') if metaRed(M,EC) [ASet];) metaRed(M,SSet). --- eq metaRed(M,mb T : St [ASet]; SSet) = (mb metaRed(M,T) : St [ASet];) metaRed(M,SSet). eq metaRed(M,cmb T : St if EC [ASet]; SSet) = (cmb metaRed(M,T) : St if metaRed(M,EC) [ASet];) metaRed(M,SSet). --- eq metaRed(M,rl T => T' [ASet]; SSet) = (rl metaRed(M,T) => metaRed(M,T')[ASet];) metaRed(M,SSet). eq metaRed(M,crl T => T' if Co [ASet]; SSet) = (crl metaRed(M,T) => metaRed(M,T') if metaRed(M,Co)[ASet];) metaRed(M,SSet). --- Condition --- op metaRed : Module Condition -> Condition . eq metaRed(M,(nil).EqCondition) = (nil).EqCondition . eq metaRed(M,T = T' /\ Co) = if metaRed(M,T) == metaRed(M,T') then metaRed(M,Co) else metaRed(M,T) = metaRed(M,T') /\ metaRed(M,Co) fi . eq metaRed(M,T := T' /\ Co) = if metaRed(M,T) == metaRed(M,T') then metaRed(M,Co) else metaRed(M,T) := metaRed(M,T') /\ metaRed(M,Co) fi . eq metaRed(M,T : St /\ Co) = if sortLeq(M,leastSort(M,metaRed(M,T)),St) then metaRed(M,Co) else metaRed(M,T) : St /\ metaRed(M,Co) fi . --- search with bound --- eq metaRed(M,T => T' /\ Co) = if metaSearch(M,T,T',nil,'*,1000000,0) :: ResultTriple then metaRed(M,Co) else metaRed(M,T) => metaRed(M,T') /\ metaRed(M,Co) fi . --- ------------------------------------------------------------------------- --- pick the lefthand side of a sentence --- --- ------------------------------------------------------------------------- op firstTerm : SentenceSet -> Term . eq firstTerm(none) = (empty).TermList . eq firstTerm(eq T = T'[ASet]; SSet) = T . eq firstTerm(ceq T = T' if EC[ASet]; SSet) = T . eq firstTerm(mb T : St [ASet]; SSet) = T . eq firstTerm(cmb T : St if EC [ASet]; SSet) = T . eq firstTerm(rl T => T' [ASet]; SSet) = T . eq firstTerm(crl T => T' if Co[ASet]; SSet) = T . --- ------------------------------------------------------------------------- --- get identity element of an operation --- --- ------------------------------------------------------------------------- op getId : Module Qid -> TermList . eq getId(M,Q) = getId(getOps(M),Q) . --- op getId : OpDeclSet Qid -> TermList . eq getId(none,Q) = empty . eq getId((op Q : TpL -> Tp [id(T) ASet].) OSet,Q') = if (Q == Q') then T else getId(OSet,Q') fi . --- ------------------------------------------------------------------------- --- Goal --- --- ------------------------------------------------------------------------- sorts #Goal# #NeGoalList# #GoalList# . subsort #Goal# < #NeGoalList# < #GoalList# . op <_,_> : Module SentenceSet -> #Goal# [ctor]. op emptyGoalList : -> #GoalList# [ctor] . op __ : #GoalList# #GoalList# -> #GoalList# [ctor assoc id: emptyGoalList]. op __ : #GoalList# #NeGoalList# -> #NeGoalList# [ctor assoc id: emptyGoalList]. op __ : #NeGoalList# #GoalList# -> #NeGoalList# [ctor assoc id: emptyGoalList]. --- ------------------------------------------------------------------------- eq < M,(none).SentenceSet > = emptyGoalList . --- ------------------------------------------------------------------------- var G : #Goal# . var GL : #GoalList# . --- ------------------------------------------------------------------------- op noGoals : #GoalList# -> Nat . eq noGoals(emptyGoalList)= 0 . eq noGoals(G GL) = s noGoals(GL). --- ------------------------------------------------------------------------- op lastGoal : #NeGoalList# -> #Goal# . eq lastGoal(GL G) = G . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #REDUCTION# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var GL : #GoalList# . var G : #Goal# . var M : Module . var SS : SentenceSet . --- op red : #GoalList# -> #GoalList# . eq red(emptyGoalList) = emptyGoalList . eq red(< M,SS > GL) = < M,metaRed(M,SS) > red(GL). --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #IMPLICATION# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var G : #Goal# . var NGL : #NeGoalList# . var GL : #GoalList# . var M : Module . var Sen : Sentence . var SSet : SentenceSet . var EC : EqCondition . vars T T' T1 T2 : Term . var ASet : AttrSet . vars St St' : Sort . var Co : Condition . --- ------------------------------------------------------------------------- op imp : #GoalList# -> #GoalList# . --- ------------------------------------------------------------------------- eq imp(emptyGoalList) = emptyGoalList . eq imp(G NGL) = imp(G) imp(NGL). --- Eqs --- eq imp(< M,eq T = T'[ASet]; SSet >) = < M,eq T = T'[ASet]; > imp(< M,SSet >). eq imp(< M,ceq T = T' if EC [ASet]; SSet >) = if getVar((T,T')) == empty then < addCond(M,EC), eq T = T'[ASet]; > imp(< M,SSet >) else < M,ceq T = T' if EC [ASet]; > imp(< M,SSet >) fi . --- Mbs --- eq imp(< M,mb T : St [ASet]; SSet >) = < M,mb T : St [ASet]; > imp(< M,SSet >). eq imp(< M,cmb T : St if EC[ASet]; SSet >) = if getVar(T) == empty then < addCond(M,EC),mb T : St[ASet]; > imp(< M,SSet >) else < M,cmb T : St if EC[ASet]; > imp(< M,SSet >) fi . --- Rls --- eq imp(< M,rl T => T' [ASet]; SSet >) = < M,rl T => T' [ASet]; > imp(< M,SSet >). eq imp(< M,crl T => T' if Co [ASet]; SSet >) = if getVar((T,T')) == empty then < addCond(M,Co), rl T => T' [ASet]; > imp(< M,SSet >) else < M,crl T => T' if Co [ASet]; > imp(< M,SSet >) fi . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #THEOREM-OF-CONSTANTS# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var ASet : AttrSet . var Sen : Sentence . var M : Module . var SS : SentenceSet . var G : #Goal# . var NGL : #NeGoalList# . var GL : #GoalList# . var TL : TermList . var Subst : Substitution . --- ------------------------------------------------------------------------- op tc : #GoalList# -> #GoalList# . --- ------------------------------------------------------------------------- eq tc(emptyGoalList) = emptyGoalList . eq tc(G NGL) = tc(G) tc(NGL). ceq tc(< M,Sen SS >) = < addConst(M,TL << Subst),Sen << Subst > tc(< M,SS >) if TL := getVar(Sen) /\ Subst := v2s(TL,maxIndex(M)+ 1). --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #CASE-ANALYSIS# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var E : Equation . var ESet : EquationSet . var Mx : MembAx . var MxSet : MembAxSet . var R : Rule . var RSet : RuleSet . var Co : Condition . var M : Module . vars T T' T1 T2 : Term . var TL : TermList . var GT : GroundTerm . var GTL : GroundTermList . var V : Variable . var EC : EqCondition . var St : Sort . var Subst : Substitution . var ASet : AttrSet . var N : Nat . var G : #Goal# . var GL : #GoalList# . var NGL : #NeGoalList# . var Str : String . var Sen : Sentence . var SSet SeSet SnSet ScSet : SentenceSet . var MP : [MatchPair] . --- ------------------------------------------------------------------------- --- get equations for case analysis --- --- ------------------------------------------------------------------------- --- Eqs --- op CA? : Equation -> Bool . ceq CA?(eq T = T' [metadata(Str) ASet] .)= true if rfind(Str,"CA-",length(Str))=/= notFound . ceq CA?(ceq T = T' if EC [metadata(Str) ASet] .)= true if rfind(Str,"CA-",length(Str)) =/= notFound . eq CA?(E) = false [owise]. --- op getCA : EquationSet -> SentenceSet . eq getCA((none).EquationSet) = (none).SentenceSet . eq getCA(E ESet) = if CA?(E) then conv(E) getCA(ESet) else getCA(ESet) fi . --- Mbs --- op CA? : MembAx -> Bool . ceq CA?(mb T : St [metadata(Str) ASet].)= true if rfind(Str,"CA-",length(Str)) =/= notFound . ceq CA?(cmb T : St if EC [metadata(Str) ASet].)= true if rfind(Str,"CA-",length(Str)) =/= notFound . eq CA?(Mx) = false [owise]. --- op getCA : MembAxSet -> SentenceSet . eq getCA((none).MembAxSet) = (none).SentenceSet . eq getCA(Mx MxSet) = if CA?(Mx) then conv(Mx) getCA(MxSet) else getCA(MxSet) fi . --- Rls --- op CA? : Rule -> Bool . ceq CA?(rl T => T' [metadata(Str) ASet].)= true if rfind(Str,"CA-",length(Str)) =/= notFound . ceq CA?(crl T => T' if Co [metadata(Str) ASet].)= true if rfind(Str,"CA-",length(Str)) =/= notFound . eq CA?(R) = false [owise]. --- op getCA : RuleSet -> SentenceSet . eq getCA((none).RuleSet) = (none).SentenceSet . eq getCA(R RSet) = if CA?(R) then conv(R) getCA(RSet) else getCA(RSet) fi . --- Module --- op getCA : Module -> SentenceSet . eq getCA(M) = getCA(getEqs(M)) getCA(getMbs(M)) getCA(getRls(M)). --- ------------------------------------------------------------------------- --- remove sentences with a given left-hand-side --- --- ------------------------------------------------------------------------- op rmSen : SentenceSet Term -> SentenceSet . eq rmSen((none).SentenceSet,T) = (none).SentenceSet . --- Eqs eq rmSen((eq T1 = T2 [ASet];) SSet,T) = if (T1 == T) then rmSen(SSet,T) else (eq T1 = T2 [ASet];) rmSen(SSet,T) fi . eq rmSen((ceq T1 = T2 if EC[ASet];) SSet, T) = if (T1 == T) then rmSen(SSet,T) else (ceq T1 = T2 if EC[ASet];) rmSen(SSet,T) fi . --- Mbs eq rmSen((mb T1 : St[ASet];) SSet, T) = if (T1 == T) then rmSen(SSet,T) else (mb T1 : St [ASet];) rmSen(SSet,T) fi . eq rmSen((cmb T1 : St if EC[ASet];) SSet, T) = if (T1 == T) then rmSen(SSet,T) else (cmb T1 : St if EC[ASet];) rmSen(SSet,T) fi . --- Rls eq rmSen((rl T1 => T2 [ASet];) SSet,T) = if (T1 == T) then rmSen(SSet,T) else (rl T1 => T2 [ASet];) rmSen(SSet,T) fi . eq rmSen((crl T1 => T2 if Co [ASet];) SSet,T) = if (T1 == T) then rmSen(SSet,T) else (crl T1 => T2 if Co[ASet];) rmSen(SSet,T) fi . --- ------------------------------------------------------------------------- --- keep sentences with a given left-hand-side --- --- ------------------------------------------------------------------------- op getSen : SentenceSet Term -> SentenceSet . eq getSen((none).SentenceSet, T) = (none).SentenceSet . --- Eqs eq getSen(eq T1 = T2 [ASet]; SSet, T) = if (T1 == T) then eq T1 = T2 [ASet]; getSen(SSet,T) else getSen(SSet,T) fi . eq getSen(ceq T1 = T2 if EC [ASet]; SSet, T) = if (T1 == T) then ceq T1 = T2 if EC [ASet]; getSen(SSet,T) else getSen(SSet,T) fi . --- Mbs eq getSen(mb T1 : St [ASet]; SSet, T) = if (T1 == T) then mb T1 : St [ASet]; getSen(SSet,T) else getSen(SSet,T) fi . eq getSen(cmb T1 : St if EC [ASet]; SSet, T) = if (T1 == T) then cmb T1 : St if EC[ASet]; getSen(SSet,T) else getSen(SSet,T) fi . --- Rls eq getSen(rl T1 => T2 [ASet]; SSet, T) = if (T1 == T) then rl T1 => T2 [ASet]; getSen(SSet,T) else getSen(SSet,T) fi . eq getSen(crl T1 => T2 if Co [ASet]; SSet, T) = if (T1 == T) then crl T1 => T2 if Co [ASet]; getSen(SSet,T) else getSen(SSet,T) fi . --- ------------------------------------------------------------------------- --- validate substitution --- --- (second term is obtained by applying the substitution under analysis to the first term) --- ------------------------------------------------------------------------- op validate : Module Term Term -> Bool . eq validate(M,T,T') = if metaXmatch(M,T,T',nil,1,unbounded,0) :: MatchPair then false else true fi . --- op validate : Module SentenceSet Term -> Bool . eq validate(M,(none).SentenceSet,T) = true . --- Equation eq validate(M,(eq T1 = T2 [ASet];) SSet,T) = validate(M,T1,T) and validate(M,SSet,T). eq validate(M,ceq T1 = T2 if EC [ASet]; SSet,T) = validate(M,T1,T) and validate(M,SSet,T). --- Membership eq validate(M,mb T1 : St [ASet]; SSet,T) = validate(M,T1,T) and validate(M,SSet,T). eq validate(M,cmb T1 : St if EC [ASet]; SSet,T) = validate(M,T1,T) and validate(M,SSet,T). --- Rule eq validate(M,rl T1 => T2 [ASet]; SSet,T) = validate(M,T1,T) and validate(M,SSet,T). eq validate(M,crl T1 => T2 if Co [ASet]; SSet,T) = validate(M,T1,T) and validate(M,SSet,T). --- ------------------------------------------------------------------------- --- splitting the goal (case analysis) --- --- the second SentenceSet is for validation (it doesn't change) --- --- ------------------------------------------------------------------------- op split : #Goal# SentenceSet Nat GroundTerm SentenceSet -> #GoalList# . eq split(emptyGoalList,SeSet,N,GT,SnSet)= emptyGoalList . eq split(G,none,N,GT,SnSet) = G . ceq split(< M,SSet >,SeSet,N,GT,SnSet) = if MP :: MatchPair then if validate(M,SnSet,T << getSubstitution(MP)) then split-h(< M,SSet >,SeSet,N,GT,SnSet,getSen(SeSet,T)<< getSubstitution(MP)) else split(< M,SSet >,SeSet,N + 1,GT,SnSet) fi else split(< M,SSet >,rmSen(SeSet,T),0,GT,SnSet) fi if T := firstTerm(SeSet) /\ MP := metaXmatch(M,T,GT,nil,0,unbounded,N). --- ------------------------------------------------------------------------- op split-h : #Goal# SentenceSet Nat GroundTerm SentenceSet SentenceSet -> #GoalList# . eq split-h(G,SeSet,N,GT,SnSet,none) = emptyGoalList . --- Equation --- eq split-h(< M,SSet >,SeSet,N,GT,SnSet,ceq T = T' if EC [ASet]; ScSet) = split(< addCond(M,EC),SSet >,SeSet,N + 1,GT,SnSet) split-h(< M,SSet >,SeSet,N,GT,SnSet,ScSet). --- eq split-h(< M,SSet >,SeSet,N,GT,SnSet,eq T = T'[ASet]; ScSet) = split(< M,SSet >,SeSet,N + 1,GT,SnSet) split-h(< M,SSet >,SeSet,N,GT,SnSet,ScSet). --- MembAx --- eq split-h(< M,SSet >,SeSet,N,GT,SnSet,cmb T : St if EC [ASet]; ScSet) = split(< addCond(M,EC),SSet >,SeSet,N + 1,GT,SnSet) split-h(< M,SSet >,SeSet,N,GT,SnSet,ScSet). --- eq split-h(< M,SSet >,SeSet,N,GT,SnSet,mb T : St [ASet]; ScSet) = split(< M,SSet >,SeSet,N + 1,GT,SnSet) split-h(< M,SSet >,SeSet,N,GT,SnSet,ScSet). --- Rule --- eq split-h(< M,SSet >,SeSet,N,GT,SnSet,crl T => T' if Co [ASet]; ScSet) = split(< addCond(M,Co),SSet >,SeSet,N + 1,GT,SnSet) split-h(< M,SSet >,SeSet,N,GT,SnSet,ScSet). --- eq split-h(< M,SSet >,SeSet,N,GT,SnSet,rl T => T' [ASet]; ScSet) = split(< M,SSet >,SeSet,N + 1,GT,SnSet) split-h(< M,SSet >,SeSet,N,GT,SnSet,ScSet). --- ------------------------------------------------------------------------- --- get the ground terms from the sentence set in the goal --- --- ------------------------------------------------------------------------- op _@_ : GroundTermList TermList -> GroundTermList . eq GTL @ (empty).TermList = GTL . eq GTL @ (T,TL) = if T :: GroundTerm then GTL,T @ TL else GTL @ TL fi . --- op getGTerm : SentenceSet -> GroundTermList . eq getGTerm(none) = empty . eq getGTerm(SSet eq T = T' [ASet];) = getGTerm(SSet) @ (T,T') . eq getGTerm(SSet ceq T = T' if EC[ASet];) = (getGTerm(SSet) @ (T,T')) @ getGTerm(EC). eq getGTerm(SSet mb T : St [ASet];) = getGTerm(SSet) @ T . eq getGTerm(SSet cmb T : St if EC[ASet];) = (getGTerm(SSet) @ T) @ getGTerm(EC). eq getGTerm(SSet rl T => T' [ASet];) = getGTerm(SSet) @ (T,T') . eq getGTerm(SSet crl T => T' if Co [ASet];) = (getGTerm(SSet) @ (T,T')) @ getGTerm(Co). --- op getGTerm : Condition -> GroundTermList . eq getGTerm(nil) = empty . eq getGTerm(Co /\ T = T') = getGTerm(Co) @ (T,T'). eq getGTerm(Co /\ T := T') = getGTerm(Co) @ (T',T). eq getGTerm(Co /\ T : St) = getGTerm(Co) @ T . eq getGTerm(Co /\ T => T') = getGTerm(Co) @ (T,T') . --- ------------------------------------------------------------------------- --- check match --- --- ------------------------------------------------------------------------- op match? : Module SentenceSet GroundTerm -> Bool . eq match?(M,none,GT) = false . --- Equation eq match?(M,eq T = T' [ASet]; SSet,GT)= if metaXmatch(M,T,GT,nil,0,unbounded,0) :: MatchPair then true else match?(M,SSet,GT) fi . eq match?(M,ceq T = T' if EC [ASet]; SSet,GT)= if metaXmatch(M,T,GT,nil,0,unbounded,0) :: MatchPair then true else match?(M,SSet,GT) fi . --- Membership eq match?(M,mb T : St[ASet]; SSet,GT)= if metaXmatch(M,T,GT,nil,0,unbounded,0) :: MatchPair then true else match?(M,SSet,GT) fi . eq match?(M,cmb T : St if EC [ASet]; SSet,GT)= if metaXmatch(M,T,GT,nil,0,unbounded,0) :: MatchPair then true else match?(M,SSet,GT) fi . --- Rule eq match?(M,rl T => T'[ASet]; SSet,GT)= if metaXmatch(M,T,GT,nil,0,unbounded,0) :: MatchPair then true else match?(M,SSet,GT) fi . eq match?(M,crl T => T' if Co [ASet]; SSet,GT)= if metaXmatch(M,T,GT,nil,0,unbounded,0) :: MatchPair then true else match?(M,SSet,GT) fi . --- ------------------------------------------------------------------------- op ca : #GoalList# -> #GoalList# . --- ------------------------------------------------------------------------- eq ca(emptyGoalList) = emptyGoalList . eq ca(G NGL) = ca(G) ca(NGL). eq ca(< M,Sen SSet >) = ca(< M,Sen >,getGTerm(Sen)) ca(< M,SSet >). --- ------------------------------------------------------------------------- op ca : #Goal# GroundTermList -> #GoalList# . --- ------------------------------------------------------------------------- eq ca(G,empty) = G . eq ca(emptyGoalList,GTL) = emptyGoalList . eq ca(< M,Sen >,(GT,GTL)) = if match?(M,getCA(M),GT) then split(< M,Sen >,getCA(M),0,GT,getCA(M)) else ca(< M,Sen >,GTL) fi . --- ------------------------------------------------------------------------- --- get the ground terms from the sentence set in the goal (different order) --- --- ------------------------------------------------------------------------- op getGTerm-1 : SentenceSet -> GroundTermList . eq getGTerm-1(none) = empty . eq getGTerm-1(SSet eq T = T' [ASet];) = getGTerm-1(SSet) @ (T',T) . eq getGTerm-1(SSet ceq T = T' if EC[ASet];) = (getGTerm-1(SSet) @ getGTerm(EC)) @ (T',T). eq getGTerm-1(SSet mb T : St [ASet];) = getGTerm-1(SSet) @ T . eq getGTerm-1(SSet cmb T : St if EC[ASet];) = (getGTerm-1(SSet) @ getGTerm(EC)) @ T . eq getGTerm-1(SSet rl T => T' [ASet];) = getGTerm-1(SSet) @ (T',T) . eq getGTerm-1(SSet crl T => T' if Co [ASet];) = (getGTerm-1(SSet) @ getGTerm(Co)) @ (T',T). --- ------------------------------------------------------------------------- op ca-1 : #GoalList# -> #GoalList# . --- ------------------------------------------------------------------------- eq ca-1(emptyGoalList) = emptyGoalList . eq ca-1(G NGL) = ca-1(G) ca-1(NGL). eq ca-1(< M,Sen SSet >) = ca(< M,Sen >,getGTerm-1(Sen)) ca-1(< M,SSet >). --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- --- #INDUCTION# --- --- ------------------------------------------------------------------------- fmod #INDUCTION# is inc #LIBRARY# . --- ------------------------------------------------------------------------- vars M M' : Module . var ASet : AttrSet . vars Tp Tp' : Type . var TpL : TypeList . var Od : OpDecl . vars OSet OdSet : OpDeclSet . var Q : Qid . var N : Nat . vars T T' : Term . var V : Variable . var TL : TermList . var GT : GroundTerm . vars GTL GTL' : GroundTermList . var NTpL : NeTypeList . var NGTL : NeGroundTermList . var ESet : EquationSet . var EC : EqCondition . vars MSet : MembAxSet . var RSet : RuleSet . var E : Equation . var Mx : MembAx . var R : Rule . var St : Sort . var Str : String . var Co : Condition . var SSet : SentenceSet . --- ------------------------------------------------------------------------- --- get constructors for a given sort --- ------------------------------------------------------------------------- op getCons : Module Type -> OpDeclSet . eq getCons(M,Tp) = getCons(M,getOps(M),Tp). --- op getCons : Module OpDeclSet Type -> OpDeclSet . eq getCons(M,none,Tp) = none . ceq getCons(M,(op Q : TpL -> Tp [ctor ASet] .) OSet,Tp') = (op Q : TpL -> Tp [ctor ASet].) getCons(M,OSet,Tp') if sortLeq(M,Tp,Tp'). eq getCons(M,Od OSet,Tp') = getCons(M,OSet,Tp') [owise]. --- ------------------------------------------------------------------------- --- list of types ---> list of constants --- ------------------------------------------------------------------------- op Tp2C : Module Nat TypeList Type -> GroundTermList . eq Tp2C(M,N,(nil).TypeList,Tp') = (empty).GroundTermList . eq Tp2C(M,N,Tp TpL,Tp') = if sortLeq(M,Tp,Tp') then qid("x#" + string(N,10) + "." + string(Tp)), Tp2C(M,N + 1,TpL,Tp') else qid("z#" + string(N,10) + "." + string(Tp)), Tp2C(M,N + 1,TpL,Tp') fi . --- ------------------------------------------------------------------------- --- list of types ---> list of constants of types less-equal than the type of a variable --- ------------------------------------------------------------------------- op Tp2C-v : Module Nat TypeList Type -> GroundTermList . eq Tp2C-v(M,N,(nil).TypeList,Tp') = (empty).GroundTermList . eq Tp2C-v(M,N,Tp TpL,Tp') = if sortLeq(M,Tp,Tp') then qid("x#" + string(N,10) + "." + string(Tp)), Tp2C-v(M,N + 1,TpL,Tp') else Tp2C-v(M,N + 1,TpL,Tp') fi . --- ------------------------------------------------------------------------- --- list of constants ---> operation declaration set --- ------------------------------------------------------------------------- op C2ODS : GroundTermList -> OpDeclSet . eq C2ODS(empty) = none . eq C2ODS((GT,GTL)) = if GT :: Constant then (op getName(GT) : nil -> getType(GT)[metadata("induction-constant")].) C2ODS(GTL) else C2ODS(GTL) fi . --- ------------------------------------------------------------------------- --- operation ---> ground term --- ------------------------------------------------------------------------- op Op2GT : Module OpDecl Type -> GroundTerm . eq Op2GT(M,op Q : nil -> Tp [ASet].,Tp') = qid(string(Q) + "." + string(Tp)). eq Op2GT(M,op Q : NTpL -> Tp [ASet].,Tp') = Q[Tp2C(M,maxIndex(M) + 1,NTpL,Tp')]. --- ------------------------------------------------------------------------- --- make induction hypothesis --- --- ------------------------------------------------------------------------- op makeIH : SentenceSet Variable GroundTermList -> SentenceSet . eq makeIH(SSet,V,empty) = (none).SentenceSet . eq makeIH(SSet,V,(GT,GTL)) = (SSet << (V <- GT)) makeIH(SSet,V,GTL). --- op makeIH : EquationSet Variable GroundTermList -> EquationSet . eq makeIH(ESet,V,empty) = (none).EquationSet . eq makeIH(ESet,V,(GT,GTL)) = (ESet << (V <- GT)) makeIH(ESet,V,GTL). --- op makeIH : MembAxSet Variable GroundTermList -> MembAxSet . eq makeIH(MSet,V,empty) = (none).MembAxSet . eq makeIH(MSet,V,(GT,GTL)) = (MSet << (V <- GT)) makeIH(MSet,V,GTL). --- op makeIH : RuleSet Variable GroundTermList -> RuleSet . eq makeIH(RSet,V,empty) = (none).RuleSet . eq makeIH(RSet,V,(GT,GTL)) = (RSet << (V <- GT)) makeIH(RSet,V,GTL). --- ------------------------------------------------------------------------- --- substitute induction terms for induction vars --- --- ------------------------------------------------------------------------- var H : Header . var IList : ImportList . vars StSet SrSet : SortSet . var SbSet : SubsortDeclSet . var G : #Goal# . var GList : #GoalList# . var NGL : #NeGoalList# . --- ------------------------------------------------------------------------- --- Module --- op substitute : Module Variable GroundTermList -> Module . eq substitute((fmod H is IList sorts StSet . SbSet OSet MSet ESet endfm),V,GTL) = (fmod H is IList sorts StSet . SbSet OSet substitute(MSet,V,GTL) substitute(ESet,V,GTL) endfm). eq substitute((fth H is IList sorts StSet . SbSet OSet MSet ESet endfth),V,GTL) = (fth H is IList sorts StSet . SbSet OSet substitute(MSet,V,GTL) substitute(ESet,V,GTL) endfth). eq substitute((mod H is IList sorts StSet . SbSet OSet MSet ESet RSet endm),V,GTL) = (mod H is IList sorts StSet . SbSet OSet substitute(MSet,V,GTL) substitute(ESet,V,GTL) substitute(RSet,V,GTL) endm). eq substitute((th H is IList sorts StSet . SbSet OSet MSet ESet RSet endth),V,GTL) = (th H is IList sorts StSet . SbSet OSet substitute(MSet,V,GTL) substitute(ESet,V,GTL) substitute(RSet,V,GTL) endth). --- Eqs --- op substitute : EquationSet Variable GroundTermList -> EquationSet . eq substitute((none).EquationSet,V,GTL) = (none).EquationSet . ceq substitute(eq T = T' [metadata(Str) ASet]. ESet,V,GTL) = makeIH(eq T = T' [ASet].,V,GTL) substitute(ESet,V,GTL) if qid(substr(Str,length("induction-on-"),length(Str))) = V . ceq substitute(ceq T = T' if EC[metadata(Str) ASet]. ESet,V,GTL) = makeIH(ceq T = T' if EC[ASet].,V,GTL) substitute(ESet,V,GTL) if qid(substr(Str,length("induction-on-"),length(Str))) = V . eq substitute(E ESet,V,GTL) = E substitute(ESet,V,GTL) [owise]. --- Mbs --- op substitute : MembAxSet Variable GroundTermList -> MembAxSet . eq substitute((none).MembAxSet,V,GTL) = (none).MembAxSet . ceq substitute(mb T : St [metadata(Str) ASet]. MSet,V,GTL) = makeIH(mb T : St [ASet].,V,GTL) substitute(MSet,V,GTL) if qid(substr(Str,length("induction-on-"),length(Str))) = V . ceq substitute(cmb T : St if EC[metadata(Str) ASet]. MSet,V,GTL) = makeIH(cmb T : St if EC[ASet].,V,GTL) substitute(MSet,V,GTL) if qid(substr(Str,length("induction-on-"),length(Str))) = V . eq substitute(Mx MSet,V,GTL) = Mx substitute(MSet,V,GTL) [owise]. --- Rls --- op substitute : RuleSet Variable GroundTermList -> RuleSet . eq substitute((none).RuleSet,V,GTL) = (none).RuleSet . ceq substitute(rl T => T' [metadata(Str) ASet]. RSet,V,GTL) = makeIH(rl T => T' [ASet].,V,GTL) substitute(RSet,V,GTL) if qid(substr(Str,length("induction-on-"),length(Str))) = V . ceq substitute(crl T => T' if Co[metadata(Str) ASet]. RSet,V,GTL) = makeIH(crl T => T' if Co[ASet].,V,GTL) substitute(RSet,V,GTL) if qid(substr(Str,length("induction-on-"),length(Str))) = V . eq substitute(R RSet,V,GTL) = R substitute(RSet,V,GTL)[owise]. --- ------------------------------------------------------------------------- --- induction case --- --- ------------------------------------------------------------------------- op indCase : #Goal# Variable OpDeclSet -> #GoalList# . eq indCase(G,V,none) = emptyGoalList . --- ceq indCase(< M,SSet >,V,op Q : TpL -> Tp [ASet]. OSet) = ind(< addSen(M', makeIH(SSet,V,GTL')), SSet << (V <- GT) >) indCase(< M,SSet >,V,OSet) if GTL := Tp2C(M,maxIndex(M)+ 1,TpL,getType(V)) /\ GTL' := Tp2C-v(M,maxIndex(M)+ 1,TpL,getType(V)) /\ GT := Op2GT(M,op Q : TpL -> Tp [ASet].,getType(V)) /\ M' := substitute(addOp(M,C2ODS(GTL)),V,(GTL',GT)). --- ------------------------------------------------------------------------- --- induction --- --- ------------------------------------------------------------------------- op ind : #GoalList# -> #GoalList# . --- ------------------------------------------------------------------------- eq ind(emptyGoalList) = emptyGoalList . eq ind(G NGL) = ind(G) ind(NGL) . ceq ind(< M,SSet >) = if (TL :: Variable) and (getCons(M,getType(TL)) =/= none) then indCase(< M,rmIV(SSet,TL) >, TL, getCons(M,getType(TL))) else < M,SSet > fi if TL := getIV(SSet). --- ------------------------------------------------------------------------ --- get induction variables --- --- ------------------------------------------------------------------------ op getIV : SentenceSet -> Variable . ceq getIV(eq T = T' [metadata(Str) ASet]; SSet) = V if V := qid(substr(Str,length("induction-on-"),length(Str))) /\ V in getVar(eq T = T' [metadata(Str) ASet];) /\ checkIV(SSet,V). ceq getIV(ceq T = T' if EC [metadata(Str) ASet]; SSet) = V if V := qid(substr(Str,length("induction-on-"),length(Str)))/\ V in getVar(ceq T = T' if EC [metadata(Str) ASet];) /\ checkIV(SSet,V). ceq getIV(mb T : St [metadata(Str) ASet]; SSet) = V if V := qid(substr(Str,length("induction-on-"),length(Str))) /\ V in getVar(mb T : St [metadata(Str) ASet];) /\ checkIV(SSet,V). ceq getIV(cmb T : St if EC [metadata(Str) ASet]; SSet) = V if V := qid(substr(Str,length("induction-on-"),length(Str)))/\ V in getVar(cmb T : St if EC [metadata(Str) ASet];) /\ checkIV(SSet,V). ceq getIV(rl T => T' [metadata(Str) ASet]; SSet) = V if V := qid(substr(Str,length("induction-on-"),length(Str))) /\ V in getVar(rl T => T' [metadata(Str) ASet];) /\ checkIV(SSet,V). ceq getIV(crl T => T' if Co[metadata(Str) ASet]; SSet) = V if V := qid(substr(Str,length("induction-on-"),length(Str)))/\ V in getVar(crl T => T' if Co [metadata(Str) ASet];) /\ checkIV(SSet,V). eq getIV(SSet) = (empty).TermList [owise]. --- ------------------------------------------------------------------------- --- check induction variables --- --- ------------------------------------------------------------------------- op checkIV : SentenceSet Variable -> Bool . eq checkIV(none,V) = true . ceq checkIV(eq T = T' [metadata(Str) ASet]; SSet,V) = checkIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str)))/\ V in getVar(eq T = T' [metadata(Str) ASet];). ceq checkIV(ceq T = T' if EC [metadata(Str) ASet]; SSet,V) = checkIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))) /\ V in getVar(ceq T = T' if EC [metadata(Str) ASet];). ceq checkIV(mb T : St [metadata(Str) ASet]; SSet,V) = checkIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str)))/\ V in getVar(mb T : St [metadata(Str) ASet];). ceq checkIV(cmb T : St if EC [metadata(Str) ASet]; SSet,V) = checkIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))) /\ V in getVar(cmb T : St if EC [metadata(Str) ASet];). ceq checkIV(rl T => T' [metadata(Str) ASet]; SSet,V) = checkIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str)))/\ V in getVar(rl T => T' [metadata(Str) ASet];). ceq checkIV(crl T => T' if Co [metadata(Str) ASet]; SSet,V) = checkIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))) /\ V in getVar(crl T => T' if Co [metadata(Str) ASet];). eq checkIV(SSet,V) = false [owise]. --- ------------------------------------------------------------------------- --- remove induction variables --- --- ------------------------------------------------------------------------- op rmIV : SentenceSet Variable -> SentenceSet . --- Equation ceq rmIV(eq T = T' [metadata(Str) ASet]; SSet,V) = (eq T = T' [ASet];) rmIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))). ceq rmIV(ceq T = T' if EC [metadata(Str) ASet]; SSet,V) = (ceq T = T' if EC [ASet];) rmIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))) . --- Membership ceq rmIV(mb T : St [metadata(Str) ASet]; SSet,V) = (mb T : St [ASet];) rmIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))). ceq rmIV(cmb T : St if EC [metadata(Str) ASet]; SSet,V) = (cmb T : St if EC [ASet];) rmIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))) . --- Rule ceq rmIV(rl T => T' [metadata(Str) ASet]; SSet,V) = rl T => T' [ASet]; rmIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))). ceq rmIV(crl T => T' if Co [metadata(Str) ASet]; SSet,V) = crl T => T' if Co [ASet]; rmIV(SSet,V) if V = qid(substr(Str,length("induction-on-"),length(Str))) . --- owise eq rmIV(SSet,V) = SSet [owise]. --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #UNIFICATION# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var M : Module . var GL : #GoalList# . vars N P : Nat . vars T T1 T2 T1' T2' : Term . vars NTL1 NTL2 : NeTermList . vars Q Q1 Q2 : Qid . var V : Variable . var Ct : Constant . var UT : [UnificationTriple?] . var UR : [#UnifyResult?#] . var UP : UnificationProblem . var UPair : UnificandPair . vars Sn St : Sentence . var SS : SentenceSet . vars AS1 AS2 : AttrSet . vars S S1 S2 : Substitution . vars EC1 EC2 : EqCondition . vars Cx Cx1 Cx2 : Context . vars CxL CxL1 CxL2 : NeCTermList . var NTL : NeTermList . var So : Sort . vars Str1 Str2 : String . --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- op maxIndex : UnificationProblem -> Nat . eq maxIndex(T1 =? T2) = if maxIndex(T1) <= maxIndex(T2) then maxIndex(T2) else maxIndex(T1) fi . eq maxIndex(UPair /\ UP) = if maxIndex(UP) <= maxIndex(UPair) then maxIndex(UPair) else maxIndex(UP) fi . --- ------------------------------------------------------------------------- --- contexts --- --- ------------------------------------------------------------------------- sorts #UnifyResult# #UnifyResult?# . subsort #UnifyResult# < #UnifyResult?# . --- op noUnifier : -> #UnifyResult?# [ctor]. op {_,_,_} : Substitution Substitution Context -> #UnifyResult# [ctor] . op _<<_ : UnificationTriple? Context -> #UnifyResult# . eq noUnifier << Cx = noUnifier . eq {S1,S2,N} << Cx = {S1,S2,Cx} . --- ------------------------------------------------------------------------- op getContext : #UnifyResult# -> Context . eq getContext({S1,S2,Cx}) = Cx . op getSub1 : #UnifyResult# -> Substitution . eq getSub1({S1,S2,Cx}) = S1 . op getSub2 : #UnifyResult# -> Substitution . eq getSub2({S1,S2,Cx}) = S2 . --- ------------------------------------------------------------------------- op replaceContext : #UnifyResult# Context -> #UnifyResult# . eq replaceContext({S1,S2,Cx1},Cx2) = {S1,S2,Cx2} . --- ------------------------------------------------------------------------- op _<<_ : Context Context -> Context . op _<<_ : NeCTermList NeCTermList -> NeCTermList . eq [] << CxL = CxL . eq (Q1[CxL1]) << CxL2 = Q1[ CxL1 << CxL2 ] . eq (NTL,CxL1) << CxL2 = NTL,(CxL1 << CxL2) . eq (CxL1,NTL) << CxL2 = (CxL1 << CxL2),NTL . --- ------------------------------------------------------------------------- op _<<_ : Context Term -> Term . op _<<_ : NeCTermList Term -> NeTermList . eq [] << T = T . eq (Q[CxL]) << T = Q[CxL << T] . eq (NTL,CxL) << T = NTL,(CxL << T) . eq (CxL,NTL) << T = (CxL << T),NTL . --- ------------------------------------------------------------------------- op _<<_ : Context Substitution -> Context . op _<<_ : NeCTermList Substitution -> NeCTermList . eq [] << S = [] . eq (Q[CxL]) << S = Q[CxL << S] . eq (NTL,CxL) << S = (NTL << S),(CxL << S) . eq (CxL,NTL) << S = (CxL << S),(NTL << S) . --- ------------------------------------------------------------------------- --- number of solutions for unification at the top --- --- ------------------------------------------------------------------------- op nrSol : Module UnificationProblem -> Nat . eq nrSol(M,UP) = nrSol(M,UP,0). --- op nrSol : Module UnificationProblem Nat -> Nat . eq nrSol(M,UP,N) = if metaDisjointUnify(M,UP,maxIndex(UP)+ 1,N) :: UnificationTriple then nrSol(M,UP,N + 1) else N fi . --- ------------------------------------------------------------------------- --- number of solutions for left-unification --- --- ------------------------------------------------------------------------- op nrSol : Module Term Term -> Nat . eq nrSol(M,V,T2) = 0 . eq nrSol(M,T1,V) = 0 . eq nrSol(M,Ct,T) = if sameKind(M,leastSort(M,Ct),leastSort(M,T)) then nrSol(M,Ct =? T) else 0 fi . eq nrSol(M,Q1[NTL1],Ct) = if sameKind(M,leastSort(M,Q1[NTL1]),leastSort(M,Ct)) then nrSol(M,Q1[NTL1] =? Ct) + nrSol(M,NTL1,Ct) else nrSol(M,NTL1,Ct) fi . eq nrSol(M,Q1[NTL1],Q2[NTL2]) = if sameKind(M,leastSort(M,Q1[NTL1]),leastSort(M,Q2[NTL2])) then nrSol(M,Q1[NTL1] =? Q2[NTL2]) + nrSol(M,NTL1,Q2[NTL2]) else nrSol(M,NTL1,Q2[NTL2]) fi . --- op nrSol : Module NeTermList Term -> Nat . eq nrSol(M,(T1,NTL1),T2) = nrSol(M,T1,T2) + nrSol(M,NTL1,T2). --- ------------------------------------------------------------------------- --- left-unification --- --- ------------------------------------------------------------------------- op l-unify : Module Term Term Nat -> #UnifyResult?# . eq l-unify(M,T1,T2,N) = if (leastSort(M,T1) :: Type) and (leastSort(M,T2) :: Type) then if maxIndex(M) <= maxIndex(T1 =? T2) then l-unify(M,T1,T2,maxIndex(T1 =? T2),N,[]) else l-unify(M,T1,T2,maxIndex(M),N,[]) fi else noUnifier fi . --- op l-unify : Module Term Term Nat Nat Context -> #UnifyResult?# . eq l-unify(M,V,T2,P,N,Cx) = noUnifier . eq l-unify(M,T1,V,P,N,Cx) = noUnifier . eq l-unify(M,Ct,T,P,N,Cx) = if sameKind(M,leastSort(M,Ct),leastSort(M,T)) then metaDisjointUnify(M,Ct =? T,P,N) << Cx else noUnifier fi . --- eq l-unify(M,Q1[NTL1],Ct,P,N,Cx) = if sameKind(M,leastSort(M,Q1[NTL1]),leastSort(M,Ct)) then if (metaDisjointUnify(M,Q1[NTL1] =? Ct,P,N) :: UnificationTriple) then metaDisjointUnify(M,Q1[NTL1] =? Ct,P,N) << Cx else l-unify(M,NTL1,Ct,P,sd(N,nrSol(M,Q1[NTL1] =? Ct)),Cx << (Q1[[]])) fi else l-unify(M,NTL1,Ct,P,N,Cx << (Q1[[]])) fi . --- eq l-unify(M,Q1[NTL1],Q2[NTL2],P,N,Cx) = if sameKind(M,leastSort(M,Q1[NTL1]),leastSort(M,Q2[NTL2])) then if metaDisjointUnify(M,Q1[NTL1] =? Q2[NTL2],P,N) :: UnificationTriple then metaDisjointUnify(M,Q1[NTL1] =? Q2[NTL2],P,N) << Cx else l-unify(M,NTL1,Q2[NTL2],P,sd(N,nrSol(M,Q1[NTL1] =? Q2[NTL2])),Cx << (Q1[[]])) fi else l-unify(M,NTL1,Q2[NTL2],P,N,Cx << (Q1[[]])) fi . --- op l-unify : Module NeTermList Term Nat Nat Context -> #UnifyResult?# . eq l-unify(M,(T1,NTL1),T2,P,N,Cx) = if sameKind(M,leastSort(M,T1),leastSort(M,T2)) then if l-unify(M,T1,T2,P,N,[]) :: #UnifyResult# then replaceContext(l-unify(M,T1,T2,P,N,[]),(Cx << ([],NTL1))<< getContext(l-unify(M,T1,T2,P,N,[]))) else l-unify(M,NTL1,T2,P,sd(N,nrSol(M,T1,T2)),Cx << (T1,[])) fi else l-unify(M,NTL1,T2,P,sd(N,nrSol(M,T1,T2)),Cx << (T1,[])) fi . --- ------------------------------------------------------------------------- --- critical pairs left --- --- ------------------------------------------------------------------------- op CP-L : #GoalList# String String Nat -> #GoalList# . eq CP-L(emptyGoalList,Str1,Str2,N) = emptyGoalList . eq CP-L(GL < M,SS >,Str1,Str2,N)= if getSentence(M,Str1):: Sentence and getSentence(M,Str2):: Sentence then CP-L(GL < M,SS >,getSentence(M,Str1),getSentence(M,Str2),N) else GL < M,SS > fi . --- ------------------------------------------------------------------------- op CP-L : #GoalList# Sentence Sentence Nat -> #GoalList# . eq CP-L(emptyGoalList,St,Sn,N) = emptyGoalList . eq CP-L(GL < M,SS >, St,Sn,N) = GL < addSen(M,CP-L(M,St,Sn,N)),SS > . --- ------------------------------------------------------------------------- op CP-L : Module Sentence Sentence Nat -> SentenceSet . --- Eqs --- eq CP-L(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (ceq T1 = T1' if EC1[AS1]; ceq T2 = T2' if EC2[AS2];) inc M then CP-LEFT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,eq T1 = T1'[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (eq T1 = T1'[AS1]; ceq T2 = T2' if EC2[AS2];) inc M then CP-LEFT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if EC2[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,ceq T1 = T1' if EC1[AS1];,eq T2 = T2'[AS2];,N)= if (ceq T1 = T1' if EC1[AS1]; eq T2 = T2'[AS2];) inc M then CP-LEFT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if nil[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,eq T1 = T1'[AS1];,eq T2 = T2'[AS2];,N)= if (eq T1 = T1'[AS1]; eq T2 = T2'[AS2];) inc M then CP-LEFT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if nil[AS2];,N) else (none).SentenceSet fi . --- Mbs --- eq CP-L(M,cmb T1 : So if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (cmb T1 : So if EC1[AS1]; ceq T2 = T2' if EC2[AS2];) inc M then CP-LEFT(M,cmb T1 : So if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,mb T1 : So[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (mb T1 : So[AS1]; ceq T2 = T2' if EC2[AS2];) inc M then CP-LEFT(M,cmb T1 : So if nil[AS1];,ceq T2 = T2' if EC2[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,cmb T1 : So if EC1[AS1];,eq T2 = T2'[AS2];,N)= if (cmb T1 : So if EC1[AS1]; eq T2 = T2'[AS2];) inc M then CP-LEFT(M,cmb T1 : So if EC1[AS1];,ceq T2 = T2' if nil[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,mb T1 : So[AS1];,eq T2 = T2'[AS2];,N)= if (mb T1 : So[AS1]; eq T2 = T2'[AS2];) inc M then CP-LEFT(M,cmb T1 : So if nil[AS1];,ceq T2 = T2' if nil[AS2];,N) else (none).SentenceSet fi . --- eq CP-L(M,St,Sn,N) = (none).SentenceSet[owise]. --- ------------------------------------------------------------------------- op CP-LEFT : Module Sentence Sentence Nat -> SentenceSet . --- ------------------------------------------------------------------------- --- Eqs --- ceq CP-LEFT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (UR :: #UnifyResult#) and metaRed(M,EC1 << getSub1(UR)) == nil and metaRed(M,EC2 << getSub2(UR)) == nil then eq metaRed(M,T1' << getSub1(UR))= metaRed(M,(getContext(UR) << getSub1(UR)) << (T2' << getSub2(UR)))[none]; else (none).SentenceSet fi if UR := l-unify(M,T1,T2,N). --- eq CP-LEFT(M, eq T1 = T1' [AS1];,ceq T2 = T2' if EC2[AS2];,N)= CP-LEFT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if EC2[AS2];,N). eq CP-LEFT(M,ceq T1 = T1' if EC1[AS1];, eq T2 = T2' [AS2];,N)= CP-LEFT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if nil[AS2];,N). eq CP-LEFT(M, eq T1 = T1' [AS1];, eq T2 = T2' [AS2];,N)= CP-LEFT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if nil[AS2];,N). --- Mbs --- ceq CP-LEFT(M,cmb T1 : So if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (UR :: #UnifyResult#) and metaRed(M,EC1 << getSub1(UR)) == nil and metaRed(M,EC2 << getSub2(UR)) == nil then mb metaRed(M,(getContext(UR) << getSub1(UR)) << (T2' << getSub2(UR))) : So[none]; else (none).SentenceSet fi if UR := l-unify(M,T1,T2,N). --- eq CP-LEFT(M, mb T1 : So [AS1];,ceq T2 = T2' if EC2[AS2];,N)= CP-LEFT(M,cmb T1 : So if nil[AS1];,ceq T2 = T2' if EC2[AS2];,N). eq CP-LEFT(M,cmb T1 : So if EC1[AS1];, eq T2 = T2' [AS2];,N)= CP-LEFT(M,cmb T1 : So if EC1[AS1];,ceq T2 = T2' if nil[AS2];,N). eq CP-LEFT(M, mb T1 : So [AS1];, eq T2 = T2' [AS2];,N)= CP-LEFT(M,cmb T1 : So if nil[AS1];,ceq T2 = T2' if nil[AS2];,N). --- eq CP-LEFT(M,St,Sn,N) = (none).SentenceSet[owise]. --- ------------------------------------------------------------------------- --- critical pairs right -- --- ------------------------------------------------------------------------- op CP-R : #GoalList# String String Nat -> #GoalList# . eq CP-R(emptyGoalList,Str1,Str2,N) = emptyGoalList . eq CP-R(GL < M,SS >,Str1,Str2,N)= if getSentence(M,Str1):: Sentence and getSentence(M,Str2):: Sentence then CP-R(GL < M,SS >,getSentence(M,Str1),getSentence(M,Str2),N) else GL < M,SS > fi . --- ------------------------------------------------------------------------- op CP-R : #GoalList# Sentence Sentence Nat -> #GoalList# . eq CP-R(emptyGoalList,St,Sn,N) = emptyGoalList . eq CP-R(GL < M,SS >, St,Sn,N) = GL < addSen(M,CP-R(M,St,Sn,N)),SS > . --- ------------------------------------------------------------------------- op CP-R : Module Sentence Sentence Nat -> SentenceSet . eq CP-R(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (ceq T1 = T1' if EC1[AS1]; ceq T2 = T2' if EC2[AS2];) inc M then CP-RIGHT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N) else (none).SentenceSet fi . --- eq CP-R(M,eq T1 = T1'[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (eq T1 = T1'[AS1]; ceq T2 = T2' if EC2[AS2];) inc M then CP-RIGHT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if EC2[AS2];,N) else (none).SentenceSet fi . --- eq CP-R(M,ceq T1 = T1' if EC1[AS1];,eq T2 = T2'[AS2];,N)= if (ceq T1 = T1' if EC1[AS1]; eq T2 = T2'[AS2];) inc M then CP-RIGHT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if nil[AS2];,N) else (none).SentenceSet fi . --- eq CP-R(M,eq T1 = T1'[AS1];,eq T2 = T2'[AS2];,N)= if (eq T1 = T1'[AS1]; eq T2 = T2'[AS2];) inc M then CP-RIGHT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if nil[AS2];,N) else (none).SentenceSet fi . --- eq CP-R(M,St,Sn,N) = (none).SentenceSet[owise]. --- ------------------------------------------------------------------------- op CP-RIGHT : Module Sentence Sentence Nat -> SentenceSet . --- ------------------------------------------------------------------------- ceq CP-RIGHT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if EC2[AS2];,N)= if (UR :: #UnifyResult#) and metaRed(M,EC1 << getSub1(UR)) == nil and metaRed(M,EC2 << getSub2(UR)) == nil then eq metaRed(M,(getContext(UR) << getSub1(UR)) << (T2' << getSub2(UR)))= metaRed(M,T1' << getSub1(UR))[none]; else (none).SentenceSet fi if UR := l-unify(M,T1,T2,N). --- eq CP-RIGHT(M, eq T1 = T1' [AS1];,ceq T2 = T2' if EC2[AS2];,N)= CP-RIGHT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if EC2[AS2];,N). eq CP-RIGHT(M,ceq T1 = T1' if EC1[AS1];, eq T2 = T2' [AS2];,N)= CP-RIGHT(M,ceq T1 = T1' if EC1[AS1];,ceq T2 = T2' if nil[AS2];,N). eq CP-RIGHT(M, eq T1 = T1' [AS1];, eq T2 = T2' [AS2];,N)= CP-RIGHT(M,ceq T1 = T1' if nil[AS1];,ceq T2 = T2' if nil[AS2];,N). --- eq CP-RIGHT(M,St,Sn,N) = (none).SentenceSet[owise]. --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #INIT# is inc #LIBRARY# . --- ------------------------------------------------------------------------- vars GL GL1 : #GoalList# . var NGL : #NeGoalList# . var G : #Goal# . var Str : String . vars T T1 T2 : Term . var TL : TermList . var St : Sort . var AS : AttrSet . var Sen : Sentence . vars SS SS1 : SentenceSet . var EC : EqCondition . var Co : Condition . var M : Module . var Sub : Substitution . var N : Nat . --- ------------------------------------------------------------------------- op removeNonexec : SentenceSet -> SentenceSet . eq removeNonexec((none).SentenceSet)= (none).SentenceSet . eq removeNonexec( eq T1 = T2 [nonexec AS]; SS)= eq T1 = T2 [AS]; removeNonexec(SS). eq removeNonexec(ceq T1 = T2 if EC[nonexec AS]; SS)= ceq T1 = T2 if EC[AS]; removeNonexec(SS). eq removeNonexec( mb T : St [nonexec AS]; SS)= mb T : St [AS]; removeNonexec(SS). eq removeNonexec(cmb T : St if EC[nonexec AS]; SS)= cmb T : St if EC[AS]; removeNonexec(SS). eq removeNonexec( rl T1 => T2 [nonexec AS]; SS)= rl T1 => T2 [AS]; removeNonexec(SS). eq removeNonexec(crl T1 => T2 if Co[nonexec AS]; SS)= crl T1 => T2 if Co[AS]; removeNonexec(SS). eq removeNonexec(Sen SS) = Sen removeNonexec(SS)[owise]. --- ------------------------------------------------------------------------- op INIT : Module SentenceSet Substitution -> Module . eq INIT(M,SS,Sub) = addSen(M,removeNonexec(metaRed(M,SS << Sub))). op INIT : #GoalList# SentenceSet Substitution -> #GoalList# . eq INIT(emptyGoalList,SS,Sub) = emptyGoalList . eq INIT(GL < M, SS >, SS1, Sub) = GL < INIT(M,SS1,Sub),SS > . --- ------------------------------------------------------------------------- op INIT : #GoalList# String Substitution -> #GoalList# . eq INIT(emptyGoalList,Str,Sub) = emptyGoalList . eq INIT(GL < M, SS >, Str, Sub) = INIT(GL < M,SS >, getSentence(M,Str),Sub) . --- ------------------------------------------------------------------------- op select : #GoalList# Nat -> #GoalList# . eq select(emptyGoalList,N) = emptyGoalList . eq select(NGL,N) = select(NGL,N,emptyGoalList). --- op select : #NeGoalList# Nat #GoalList# -> #GoalList# . eq select(NGL ,0,GL1)= NGL GL1 . eq select(GL G,1,GL1)= GL GL1 G . ceq select(GL G,N,GL1)= select(GL,sd(N,1),G GL1) if 2 <= N . --- ------------------------------------------------------------------------- op addComment : SentenceSet String -> SentenceSet . eq addComment(none,Str) = none . eq addComment( eq T1 = T2[AS]; SS,Str)= eq T1 = T2 [AS metadata(Str)]; addComment(SS,Str). eq addComment(ceq T1 = T2 if EC[AS]; SS,Str)= ceq T1 = T2 if EC[AS metadata(Str)]; addComment(SS,Str). eq addComment( mb T : St [AS]; SS,Str)= mb T : St [AS metadata(Str)]; addComment(SS,Str). eq addComment(cmb T : St if EC[AS]; SS,Str)= cmb T : St if EC[AS metadata(Str)]; addComment(SS,Str). eq addComment( rl T1 => T2[AS]; SS,Str)= rl T1 => T2 [AS metadata(Str)]; addComment(SS,Str). eq addComment(crl T1 => T2 if Co[AS]; SS,Str)= crl T1 => T2 if Co[AS metadata(Str)]; addComment(SS,Str). --- ------------------------------------------------------------------------- op addComment : SentenceSet TermList -> SentenceSet . eq addComment(SS,empty) = SS . eq addComment(SS,(T,TL))= if not(T :: Variable) then addComment(SS,TL) else addComment(addComment(SS,"induction-on-" + string(T)),TL) fi . --- ------------------------------------------------------------------------- op addComment : #GoalList# TermList -> #GoalList# . eq addComment(emptyGoalList,TL) = emptyGoalList . eq addComment(GL < M,SS >,TL) = addComment(GL,TL) < M,addComment(SS,TL) > . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #SEQUENCE# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var G : #Goal# . var GList : #GoalList# . var NGL : #NeGoalList# . vars Sen Sen1 Sen2 : Sentence . vars SSet SS : SentenceSet . vars ECo ECd : EqCondition . vars Co Cd : Condition . var ASet : AttrSet . var M : Module . var St : Sort . vars T T' T1 T2 Bx By : Term . vars GT1 GT2 GT : GroundTerm . vars V Sx Sy Sz Sa Sb : Variable . vars GTL GTL1 GTL2 : GroundTermList . var NGTL : NeGroundTermList . --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- pair equiv --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- op r1 : SentenceSet -> SentenceSet . eq r1(none) = none . eq r1(Sen1 Sen2 SS) = r1(Sen1) r1(Sen2 SS). --- Equation --- eq r1(ceq T = T' if ECo /\ '<_`,_>[Bx,By] = '<_`,_>[GT1,GT2] /\ ECd[ASet];) = (ceq T = T' if ECo /\ Bx = GT1 /\ By = GT2 /\ ECd[ASet];). eq r1(ceq T = T' if ECo /\ '<_`,_>[Bx,By] := '<_`,_>[GT1,GT2] /\ ECd[ASet];) = (ceq T = T' if ECo /\ Bx := GT1 /\ By := GT2 /\ ECd[ASet];). --- MembAx --- eq r1(cmb T : St if ECo /\ '<_`,_>[Bx,By] = '<_`,_>[GT1,GT2] /\ ECd[ASet];) = (cmb T : St if ECo /\ Bx = GT1 /\ By = GT2 /\ ECd[ASet];). eq r1(cmb T : St if ECo /\ '<_`,_>[Bx,By] := '<_`,_>[GT1,GT2] /\ ECd[ASet];) = (cmb T : St if ECo /\ Bx := GT1 /\ By := GT2 /\ ECd[ASet];). --- Rule --- eq r1(crl T => T' if Co /\ '<_`,_>[Bx,By] = '<_`,_>[GT1,GT2] /\ Cd[ASet];) = (crl T => T' if Co /\ Bx = GT1 /\ By = GT2 /\ Cd[ASet];). eq r1(crl T => T' if Co /\ '<_`,_>[Bx,By] := '<_`,_>[GT1,GT2] /\ Cd[ASet];) = (crl T => T' if Co /\ Bx := GT1 /\ By := GT2 /\ Cd[ASet];). ---- eq r1(Sen) = Sen[owise]. --- -------------------------------------------------------------------------------------------------------------------------------------------------- op r2 : SentenceSet -> SentenceSet . eq r2(none) = none . eq r2(Sen1 Sen2 SS) = r2(Sen1) r2(Sen2 SS). --- Equation --- eq r2(ceq T = T' if ECo /\ V := Bx /\ ECd[ASet];) = (ceq T <<(V <- Bx) = T' <<(V <- Bx) if ECo <<(V <- Bx) /\ ECd <<(V <- Bx)[ASet];). --- MembAx --- eq r2(cmb T : St if ECo /\ V := Bx /\ ECd[ASet];) = (cmb T <<(V <- Bx) : St if ECo <<(V <- Bx) /\ ECd <<(V <- Bx)[ASet];). --- Rule --- eq r2(crl T => T' if Co /\ V := Bx /\ Cd[ASet];) = (crl T <<(V <- Bx) => T' <<(V <- Bx) if Co <<(V <- Bx) /\ Cd <<(V <- Bx)[ASet];). --- eq r2(Sen) = Sen[owise]. --- -------------------------------------------------------------------------------------------------------------------------------------------------- op pair : #GoalList# -> #GoalList# . eq pair(emptyGoalList) = emptyGoalList . eq pair(< M,SS > GList) = < M,r2(r1(SS))> pair(GList). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Case Analysis for sequences --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- op cs : #GoalList# -> #GoalList# . --- eq cs(emptyGoalList) = emptyGoalList . eq cs(G NGL) = cs(G) cs(NGL). --- eq cs(< M,Sen1 Sen2 SS >)= cs(< M,Sen1 >) cs(< M,Sen2 SS >). eq cs(G) = G [owise]. --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- 1) Sx,Bx,Sy := GTL --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Equation --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT,NGTL] /\ ECd [ASet];)>) = < M,(ceq T <<(Sy <- '_`,_[Sy,NGTL]) = T' <<(Sy <- '_`,_[Sy,NGTL]) if ECo <<(Sy <- '_`,_[Sy,NGTL]) /\ '_`,_[Sx,Bx,Sy] := GT /\ ECd <<(Sy <- '_`,_[Sy,NGTL])[ASet];) > cs(< M,(ceq T <<(Sx <- '_`,_[GT,Sx]) = T' <<(Sx <- '_`,_[GT,Sx]) if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT,NGTL] /\ ECd [ASet];)>) = < M,(ceq T <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL])= T' <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) if ECo <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) /\ Bx := GT /\ ECd <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL])[ASet];) > cs(< M,(ceq T <<(Sx <- '_`,_[GT,Sx]) = T' <<(Sx <- '_`,_[GT,Sx]) if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT] /\ ECd [ASet];)>) = < M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy] := GT /\ ECd [ASet];) > if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT] /\ ECd [ASet];)>)= < M,(ceq T <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence) = T' <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence) if ECo <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence)/\ Bx := GT /\ ECd <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence)[ASet];) > if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- MembAx --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT,NGTL] /\ ECd [ASet];) >) = < M,(cmb T <<(Sy <- '_`,_[Sy,NGTL]) : St if ECo <<(Sy <- '_`,_[Sy,NGTL]) /\ '_`,_[Sx,Bx,Sy] := GT /\ ECd <<(Sy <- '_`,_[Sy,NGTL])[ASet];) > cs(< M,(cmb T <<(Sx <- '_`,_[GT,Sx]) : St if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT,NGTL] /\ ECd [ASet];)>) = < M,(cmb T <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) : St if ECo <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) /\ Bx := GT /\ ECd <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL])[ASet];)> cs(< M,(cmb T <<(Sx <- '_`,_[GT,Sx]) : St if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT] /\ ECd [ASet];)>) = < M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy] := GT /\ ECd [ASet];)> if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT] /\ ECd [ASet];)>)= < M,(cmb T <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence) : St if ECo <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence)/\ Bx := GT /\ ECd <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence)[ASet];)> if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx) = leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Rule --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT,NGTL] /\ Cd [ASet];)>)= < M,(crl T <<(Sy <- '_`,_[Sy,NGTL]) => T' <<(Sy <- '_`,_[Sy,NGTL]) if Co <<(Sy <- '_`,_[Sy,NGTL]) /\ '_`,_[Sx,Bx,Sy] := GT /\ Cd <<(Sy <- '_`,_[Sy,NGTL])[ASet];)> cs(< M,(crl T <<(Sx <- '_`,_[GT,Sx]) => T' <<(Sx <- '_`,_[GT,Sx]) if Co <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy] := '_`,_[NGTL] /\ Cd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx) = leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT,NGTL] /\ Cd [ASet];)>) = < M,(crl T <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) => T' <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) if Co <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL]) /\ Bx := GT /\ Cd <<(Sx <- 'empty.Sequence ; Sy <- '_`,_[NGTL])[ASet];)> cs(< M,(crl T <<(Sx <- '_`,_[GT,Sx]) => T' <<(Sx <- '_`,_[GT,Sx]) if Co <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy] := '_`,_[NGTL] /\ Cd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx) = leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT] /\ Cd [ASet];)>) = < M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy] := GT /\ Cd [ASet];)> if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy] := '_`,_[GT] /\ Cd [ASet];)>) = < M,(crl T <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence) => T' <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence) if Co <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence)/\ Bx := GT /\ Cd <<(Sx <- 'empty.Sequence ; Sy <- 'empty.Sequence)[ASet];)> if leastSort(M,Sx)= leastSort(M,Sy)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- 2) Sx,Bx,Sy,By,Sz := GTL --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Equation --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT,NGTL] /\ ECd [ASet];)>)= < M,(ceq T <<(Sz <- '_`,_[Sz,NGTL])= T' <<(Sz <- '_`,_[Sz,NGTL]) if ECo <<(Sz <- '_`,_[Sz,NGTL])/\ '_`,_[Sx,Bx,Sy,By,Sz] := GT /\ ECd <<(Sz <- '_`,_[Sz,NGTL])[ASet];)> cs(< M,(ceq T <<(Sx <- '_`,_[GT,Sx])= T' <<(Sx <- '_`,_[GT,Sx]) if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) cs(< M,(ceq T <<(Sy <- '_`,_[Sa,Sb]) = T' <<(Sy <- '_`,_[Sa,Sb]) if ECo <<(Sy <- '_`,_[Sa,Sb]) /\ '_`,_[Sx,Bx,Sa] := GT /\ '_`,_[Sb,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sy <- '_`,_[Sa,Sb])[ASet];)>) if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Sx) = leastSort(M,GT) /\ Sa := qid(string(getName(Sy)) + "#1:" + string(getType(Sy))) /\ Sb := qid(string(getName(Sy)) + "#2:" + string(getType(Sy))). --- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT,NGTL] /\ ECd [ASet];)>) = cs(< M,(ceq T <<(Sx <- 'empty.Sequence) = T' <<(Sx <- 'empty.Sequence) if ECo <<(Sx <- 'empty.Sequence) /\ Bx := GT /\ '_`,_[Sy,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sx <- 'empty.Sequence)[ASet];)>) cs(< M,(ceq T <<(Sx <- '_`,_[GT,Sx])= T' <<(Sx <- '_`,_[GT,Sx]) if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Bx) = leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT] /\ ECd [ASet];)>) = < M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := GT /\ ECd [ASet];)> if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Sx) = leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT] /\ ECd [ASet];)>) = emptyGoalList if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Bx) = leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- MembAx --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT,NGTL] /\ ECd [ASet];)>) = < M,(cmb T <<(Sz <- '_`,_[Sz,NGTL]) : St if ECo <<(Sz <- '_`,_[Sz,NGTL])/\ '_`,_[Sx,Bx,Sy,By,Sz] := GT /\ ECd <<(Sz <- '_`,_[Sz,NGTL])[ASet];)> cs(< M,(cmb T <<(Sx <- '_`,_[GT,Sx]) : St if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) cs(< M,(cmb T <<(Sy <- '_`,_[Sa,Sb]) : St if ECo <<(Sy <- '_`,_[Sa,Sb]) /\ '_`,_[Sx,Bx,Sa] := GT /\ '_`,_[Sb,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sy <- '_`,_[Sa,Sb])[ASet];)>) if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Sx) = leastSort(M,GT) /\ Sa := qid(string(getName(Sy)) + "#1:" + string(getType(Sy))) /\ Sb := qid(string(getName(Sy)) + "#2:" + string(getType(Sy))). --- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT,NGTL] /\ ECd [ASet];)>) = cs(< M,(cmb T <<(Sx <- 'empty.Sequence) : St if ECo <<(Sx <- 'empty.Sequence) /\ Bx := GT /\ '_`,_[Sy,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sx <- 'empty.Sequence)[ASet];)>) cs(< M,(cmb T <<(Sx <- '_`,_[GT,Sx]) : St if ECo <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[NGTL] /\ ECd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Bx) = leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT] /\ ECd [ASet];)>) = < M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := GT /\ ECd [ASet];)> if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Sx) = leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT] /\ ECd [ASet];)>) = emptyGoalList if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Bx) = leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Rule --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT,NGTL] /\ Cd [ASet];)>) = < M,(crl T <<(Sz <- '_`,_[Sz,NGTL]) => T' <<(Sz <- '_`,_[Sz,NGTL]) if Co <<(Sz <- '_`,_[Sz,NGTL])/\ '_`,_[Sx,Bx,Sy,By,Sz] := GT /\ Cd <<(Sz <- '_`,_[Sz,NGTL])[ASet];)> cs(< M,(crl T <<(Sx <- '_`,_[GT,Sx]) => T' <<(Sx <- '_`,_[GT,Sx]) if Co <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[NGTL] /\ Cd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) cs(< M,(crl T <<(Sy <- '_`,_[Sa,Sb]) => T' <<(Sy <- '_`,_[Sa,Sb]) if Co <<(Sy <- '_`,_[Sa,Sb]) /\ '_`,_[Sx,Bx,Sa] := GT /\ '_`,_[Sb,By,Sz] := '_`,_[NGTL] /\ Cd <<(Sy <- '_`,_[Sa,Sb])[ASet];)>) if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Sx) = leastSort(M,GT) /\ Sa := qid(string(getName(Sy)) + "#1:" + string(getType(Sy))) /\ Sb := qid(string(getName(Sy)) + "#2:" + string(getType(Sy))). --- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT,NGTL] /\ Cd [ASet];)>) = cs(< M,(crl T <<(Sx <- 'empty.Sequence) => T' <<(Sx <- 'empty.Sequence) if Co <<(Sx <- 'empty.Sequence) /\ Bx := GT /\ '_`,_[Sy,By,Sz] := '_`,_[NGTL] /\ Cd <<(Sx <- 'empty.Sequence)[ASet];)>) cs(< M,(crl T <<(Sx <- '_`,_[GT,Sx]) => T' <<(Sx <- '_`,_[GT,Sx]) if Co <<(Sx <- '_`,_[GT,Sx]) /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[NGTL] /\ Cd <<(Sx <- '_`,_[GT,Sx])[ASet];)>) if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Bx) = leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT] /\ Cd [ASet];)>)= < M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy,By,Sz] := GT /\ Cd [ASet];)> if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Sx) = leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '_`,_[Sx,Bx,Sy,By,Sz] := '_`,_[GT] /\ Cd [ASet];) >) = emptyGoalList if leastSort(M,Sx) = leastSort(M,Sy) /\ leastSort(M,Sx) = leastSort(M,Sz) /\ leastSort(M,Bx) = leastSort(M,By) /\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx)) /\ leastSort(M,Bx) =/= leastSort(M,Sx) /\ leastSort(M,Bx) = leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Case Analysis for sets --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- 1) Bx Sx := GTL --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Equation --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,Sx] := '__[GT,NGTL] /\ ECd [ASet];)>) = < M,(ceq T <<(Sx <- '__[Sx,NGTL]) = T' <<(Sx <- '__[Sx,NGTL]) if ECo <<(Sx <- '__[Sx,NGTL]) /\ '__[Bx,Sx] := GT /\ ECd <<(Sx <- '__[Sx,NGTL])[ASet];) > cs(< M,(ceq T <<(Sx <- '__[GT,Sx]) = T' <<(Sx <- '__[GT,Sx]) if ECo <<(Sx <- '__[GT,Sx]) /\ '__[Bx,Sx] := '__[NGTL] /\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,Sx] := '__[GT,NGTL] /\ ECd [ASet];)>) = < M,(ceq T <<(Sx <- '__[NGTL])= T' <<(Sx <- '__[NGTL]) if ECo <<(Sx <- '__[NGTL]) /\ Bx := GT /\ ECd <<(Sx <- '__[NGTL])[ASet];) > cs(< M,(ceq T <<(Sx <- '__[GT,Sx]) = T' <<(Sx <- '__[GT,Sx]) if ECo <<(Sx <- '__[GT,Sx]) /\ '__[Bx,Sx] := '__[NGTL] /\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,Sx] := '__[GT] /\ ECd [ASet];)>) = < M,(ceq T = T' if ECo /\ '__[Bx,Sx] := GT /\ ECd [ASet];) > if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,Sx] := '__[GT] /\ ECd [ASet];)>)= < M,(ceq T <<(Sx <- 'empty.Set) = T' <<(Sx <- 'empty.Set) if ECo <<(Sx <- 'empty.Set)/\ Bx := GT /\ ECd <<(Sx <- 'empty.Set)[ASet];) > if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- MembAx --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,Sx] := '__[GT,NGTL] /\ ECd [ASet];)>) = < M,(cmb T <<(Sx <- '__[Sx,NGTL]) : St if ECo <<(Sx <- '__[Sx,NGTL]) /\ '__[Bx,Sx] := GT /\ ECd <<(Sx <- '__[Sx,NGTL])[ASet];) > cs(< M,(cmb T <<(Sx <- '__[GT,Sx]) : St if ECo <<(Sx <- '__[GT,Sx]) /\ '__[Bx,Sx] := '__[NGTL] /\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,Sx] := '__[GT,NGTL] /\ ECd [ASet];)>) = < M,(cmb T <<(Sx <- '__[NGTL]) : St if ECo <<(Sx <- '__[NGTL]) /\ Bx := GT /\ ECd <<(Sx <- '__[NGTL])[ASet];) > cs(< M,(cmb T <<(Sx <- '__[GT,Sx]) : St if ECo <<(Sx <- '__[GT,Sx]) /\ '__[Bx,Sx] := '__[NGTL] /\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,Sx] := '__[GT] /\ ECd [ASet];)>) = < M,(cmb T : St if ECo /\ '__[Bx,Sx] := GT /\ ECd [ASet];) > if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,Sx] := '__[GT] /\ ECd [ASet];)>)= < M,(cmb T <<(Sx <- 'empty.Set) : St if ECo <<(Sx <- 'empty.Set)/\ Bx := GT /\ ECd <<(Sx <- 'empty.Set)[ASet];) > if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Rule --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,Sx] := '__[GT,NGTL] /\ Cd [ASet];)>) = < M,(crl T <<(Sx <- '__[Sx,NGTL]) => T' <<(Sx <- '__[Sx,NGTL]) if Co <<(Sx <- '__[Sx,NGTL]) /\ '__[Bx,Sx] := GT /\ Cd <<(Sx <- '__[Sx,NGTL])[ASet];) > cs(< M,(crl T <<(Sx <- '__[GT,Sx]) => T' <<(Sx <- '__[GT,Sx]) if Co <<(Sx <- '__[GT,Sx]) /\ '__[Bx,Sx] := '__[NGTL] /\ Cd <<(Sx <- '__[GT,Sx])[ASet];)>) if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,Sx] := '__[GT,NGTL] /\ Cd [ASet];)>) = < M,(crl T <<(Sx <- '__[NGTL])=> T' <<(Sx <- '__[NGTL]) if Co <<(Sx <- '__[NGTL]) /\ Bx := GT /\ Cd <<(Sx <- '__[NGTL])[ASet];) > cs(< M,(crl T <<(Sx <- '__[GT,Sx]) => T' <<(Sx <- '__[GT,Sx]) if Co <<(Sx <- '__[GT,Sx]) /\ '__[Bx,Sx] := '__[NGTL] /\ Cd <<(Sx <- '__[GT,Sx])[ASet];)>) if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,Sx] := '__[GT] /\ Cd [ASet];)>) = < M,(crl T => T' if Co /\ '__[Bx,Sx] := GT /\ Cd [ASet];) > if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,Sx] := '__[GT] /\ Cd [ASet];)>)= < M,(crl T <<(Sx <- 'empty.Set) => T' <<(Sx <- 'empty.Set) if Co <<(Sx <- 'empty.Set)/\ Bx := GT /\ Cd <<(Sx <- 'empty.Set)[ASet];) > if sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- 1) Bx By Sx := GTL --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Equation --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,By,Sx]:= '__[GT,NGTL]/\ ECd [ASet];)>) = < M,(ceq T <<(Sx <- '__[Sx,NGTL])= T' <<(Sx <- '__[Sx,NGTL]) if ECo <<(Sx <- '__[Sx,NGTL])/\ '__[Bx,By,Sx] := GT /\ ECd <<(Sx <- '__[Sx,NGTL])[ASet];) > cs(< M,(ceq T <<(Sx <- '__[GT,Sx]) = T' <<(Sx <- '__[GT,Sx]) if ECo <<(Sx <- '__[GT,Sx])/\ '__[Bx,By,Sx] := '__[NGTL] /\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) cs(< M, ceq T <<(Sx <- '__[Sa,Sb])= T' <<(Sx <- '__[Sa,Sb]) if ECo <<(Sx <- '__[Sa,Sb])/\ '__[Bx,Sa] := GT /\ '__[By,Sb] := '__[NGTL] /\ ECd <<(Sx <- '__[Sa,Sb])[ASet]; >) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT) /\ Sa := qid(string(getName(Sx)) + "#1:" + string(getType(Sx))) /\ Sb := qid(string(getName(Sx)) + "#2:" + string(getType(Sx))) . --- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,By,Sx]:= '__[GT,NGTL]/\ ECd [ASet];)>)= cs(< M,(ceq T = T' if ECo /\ Bx := GT /\ '__[By,Sx]:= '__[NGTL] /\ ECd [ASet];)>) cs(< M,(ceq T = T' if ECo /\ By := GT /\ '__[Bx,Sx]:= '__[NGTL] /\ ECd [ASet];)>) cs(< M,(ceq T <<(Sx <- '__[GT,Sx])= T' <<(Sx <- '__[GT,Sx])if ECo <<(Sx <- '__[GT,Sx])/\ '__[Bx,By,Sx]:= '__[NGTL]/\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,By,Sx]:= '__[GT]/\ ECd [ASet];)>)= cs(< M,(ceq T = T' if ECo /\ '__[Bx,By,Sx]:= GT /\ ECd [ASet];)>) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(ceq T = T' if ECo /\ '__[Bx,By,Sx]:= '__[GT]/\ ECd [ASet];)>)= emptyGoalList if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- MembAx --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,By,Sx]:= '__[GT,NGTL]/\ ECd [ASet];)>) = < M,(cmb T <<(Sx <- '__[Sx,NGTL]) : St if ECo <<(Sx <- '__[Sx,NGTL])/\ '__[Bx,By,Sx] := GT /\ ECd <<(Sx <- '__[Sx,NGTL])[ASet];) > cs(< M,(cmb T <<(Sx <- '__[GT,Sx]) : St if ECo <<(Sx <- '__[GT,Sx])/\ '__[Bx,By,Sx] := '__[NGTL] /\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) cs(< M, cmb T <<(Sx <- '__[Sa,Sb]) : St if ECo <<(Sx <- '__[Sa,Sb])/\ '__[Bx,Sa] := GT /\ '__[By,Sb] := '__[NGTL] /\ ECd <<(Sx <- '__[Sa,Sb])[ASet]; >) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT) /\ Sa := qid(string(getName(Sx)) + "#1:" + string(getType(Sx))) /\ Sb := qid(string(getName(Sx)) + "#2:" + string(getType(Sx))) . --- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,By,Sx]:= '__[GT,NGTL]/\ ECd [ASet];)>)= cs(< M,(cmb T : St if ECo /\ Bx := GT /\ '__[By,Sx]:= '__[NGTL] /\ ECd [ASet];)>) cs(< M,(cmb T : St if ECo /\ By := GT /\ '__[Bx,Sx]:= '__[NGTL] /\ ECd [ASet];)>) cs(< M,(cmb T <<(Sx <- '__[GT,Sx]) : St if ECo <<(Sx <- '__[GT,Sx])/\ '__[Bx,By,Sx]:= '__[NGTL]/\ ECd <<(Sx <- '__[GT,Sx])[ASet];)>) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,By,Sx]:= '__[GT]/\ ECd [ASet];)>)= cs(< M,(cmb T : St if ECo /\ '__[Bx,By,Sx]:= GT /\ ECd [ASet];)>) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(cmb T : St if ECo /\ '__[Bx,By,Sx]:= '__[GT]/\ ECd [ASet];)>)= emptyGoalList if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- Rule --- --- -------------------------------------------------------------------------------------------------------------------------------------------------- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,By,Sx]:= '__[GT,NGTL]/\ Cd [ASet];)>) = < M,(crl T <<(Sx <- '__[Sx,NGTL])=> T' <<(Sx <- '__[Sx,NGTL]) if Co <<(Sx <- '__[Sx,NGTL])/\ '__[Bx,By,Sx] := GT /\ Cd <<(Sx <- '__[Sx,NGTL])[ASet];) > cs(< M,(crl T <<(Sx <- '__[GT,Sx]) => T' <<(Sx <- '__[GT,Sx]) if Co <<(Sx <- '__[GT,Sx])/\ '__[Bx,By,Sx] := '__[NGTL] /\ Cd <<(Sx <- '__[GT,Sx])[ASet];)>) cs(< M, crl T <<(Sx <- '__[Sa,Sb])=> T' <<(Sx <- '__[Sa,Sb]) if Co <<(Sx <- '__[Sa,Sb])/\ '__[Bx,Sa] := GT /\ '__[By,Sb] := '__[NGTL] /\ Cd <<(Sx <- '__[Sa,Sb])[ASet]; >) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT) /\ Sa := qid(string(getName(Sx)) + "#1:" + string(getType(Sx))) /\ Sb := qid(string(getName(Sx)) + "#2:" + string(getType(Sx))) . --- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,By,Sx]:= '__[GT,NGTL]/\ Cd [ASet];)>)= cs(< M,(crl T => T' if Co /\ Bx := GT /\ '__[By,Sx]:= '__[NGTL] /\ Cd [ASet];)>) cs(< M,(crl T => T' if Co /\ By := GT /\ '__[Bx,Sx]:= '__[NGTL] /\ Cd [ASet];)>) cs(< M,(crl T <<(Sx <- '__[GT,Sx])=> T' <<(Sx <- '__[GT,Sx])if Co <<(Sx <- '__[GT,Sx])/\ '__[Bx,By,Sx]:= '__[NGTL]/\ Cd <<(Sx <- '__[GT,Sx])[ASet];)>) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,By,Sx]:= '__[GT]/\ Cd [ASet];)>)= cs(< M,(crl T => T' if Co /\ '__[Bx,By,Sx]:= GT /\ Cd [ASet];)>) if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Sx)= leastSort(M,GT). --- ceq cs(< M,(crl T => T' if Co /\ '__[Bx,By,Sx]:= '__[GT]/\ Cd [ASet];)>)= emptyGoalList if leastSort(M,Bx)= leastSort(M,By)/\ sortLeq(M,leastSort(M,Bx),leastSort(M,Sx))/\ leastSort(M,Bx)=/= leastSort(M,Sx)/\ leastSort(M,Bx)= leastSort(M,GT). --- -------------------------------------------------------------------------------------------------------------------------------------------------- endfm --- -------------------------------------------------------------------------------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #INDUCTIONX# is inc #INDUCTION# . inc #SEQUENCE# . --- ------------------------------------------------------------------------- vars M M' : Module . var Tp : Type . var St : Sort . var Str : String . var ASet : AttrSet . var V : Variable . vars T T' Bx By : Term . var TL : TermList . vars GT GT1 GT2 : GroundTerm . vars GTL GTL' : GroundTermList . vars EC ECo ECd : EqCondition . vars Co Cd : Condition . var G : #Goal# . var GList : #GoalList# . var NGL : #NeGoalList# . vars SSet SenSet SS : SentenceSet . var Sen Sen1 Sen2 : Sentence . var MSet : MembAxSet . var ESet : EquationSet . var H : Header . var IList : ImportList . vars StSet SrSet : SortSet . var SbSet : SubsortDeclSet . var OdSet : OpDeclSet . var Subst : Substitution . --- ------------------------------------------------------------------------- --- extract constructors --- --- ------------------------------------------------------------------------- op getConsAx : Module MembAxSet Type -> MembAxSet . eq getConsAx(M,(mb T : St [metadata(Str) ASet].) MSet,Tp) = if sortLeq(M,St,Tp) and (rfind(Str,"ctor-",length(Str))=/= notFound) then (mb T : St [metadata(Str) ASet].) getConsAx(M,MSet,Tp) else getConsAx(M,MSet,Tp) fi . eq getConsAx(M,(cmb T : St if EC [metadata(Str) ASet].) MSet,Tp) = if sortLeq(M,St,Tp) and (rfind(Str,"ctor-",length(Str))=/= notFound) then (cmb T : St if EC [metadata(Str) ASet].) getConsAx(M,MSet,Tp) else getConsAx(M,MSet,Tp) fi . eq getConsAx(M,MSet,Tp) = (none).MembAxSet [owise]. --- op getConsAx : Module Type -> MembAxSet . eq getConsAx(M,Tp) = getConsAx(M,getMbs(M),Tp). --- ------------------------------------------------------------------------- --- induction --- --- ------------------------------------------------------------------------- op indx : #GoalList# -> #GoalList# . --- ------------------------------------------------------------------------- eq indx(emptyGoalList) = emptyGoalList . eq indx(G NGL) = indx(G) indx(NGL). --- ceq indx(< M,SSet >) = if (TL :: Variable) and (getConsAx(M,getType(TL)) =/= none) then indCaseAx(< M,rmIV(SSet,TL) >, TL, getConsAx(M,getType(TL))) else < M,SSet > fi if TL := getIV(SSet). --- ------------------------------------------------------------------------- --- induction case --- --- ------------------------------------------------------------------------- op indCaseAx : #Goal# Variable MembAxSet -> #GoalList# . eq indCaseAx(G,V,(none).MembAxSet) = emptyGoalList . --- ceq indCaseAx(< M,SSet >,V,cmb T : St if EC [ASet]. MSet) = ind(< addSen(M',SenSet), SSet <<(V <- GT) >) indCaseAx(< M,SSet >,V,MSet) if TL := getVar(cmb T : St if EC[ASet].) /\ Subst := v2s(TL,maxIndex(M)+ 1) /\ GTL := TL << Subst /\ GTL' := getIT(M,EC << Subst, getType(V)) /\ GT := T << Subst /\ M' := adCond(addConst(M,GTL),EC << Subst) /\ SenSet := metaRed(M',makeIHAx(SSet,V,GTL')) . --- eq indCaseAx(< M,SSet >,V,mb T : St[ASet]. MSet) = indCaseAx(< M,SSet >,V,cmb T : St if nil[ASet]. MSet). --- ------------------------------------------------------------------------- --- get induction hypothesis terms --- --- ------------------------------------------------------------------------- op getIT : Module EqCondition Type -> GroundTermList . eq getIT(M, nil,Tp) = empty . eq getIT(M,T = T' /\ EC,Tp) = getIT(M,EC,Tp) . eq getIT(M,T := T' /\ EC,Tp) = getIT(M,EC,Tp) . eq getIT(M, T : St /\ EC,Tp) = if (T :: GroundTerm) and sortLeq(M,St,Tp) then T,getIT(M,EC,Tp) else getIT(M,EC,Tp) fi . --- ------------------------------------------------------------------------- --- make induction hypothesis --- --- ------------------------------------------------------------------------- op makeIHAx : SentenceSet Variable GroundTermList -> SentenceSet . eq makeIHAx(SSet,V,empty) = (none).SentenceSet . eq makeIHAx(SSet,V,(GT,GTL)) = r2(r1(SSet << (V <- GT))) makeIHAx(SSet,V,GTL). --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #BOOL# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var M : Module . var ASet : AttrSet . var St : Sort . vars T T1 T2 : Term . var GT : GroundTerm . vars ECo ECd : EqCondition . var Co Cd : Condition . var SSet : SentenceSet . --- ------------------------------------------------------------------------- --- NOT --- --- ------------------------------------------------------------------------- --- Equation --- eq < M, ceq T1 = T2 if ECo /\ GT = 'not_[GT] /\ ECd[ASet]; > = emptyGoalList . eq < M, ceq T1 = T2 if ECo /\ 'not_[GT] = GT /\ ECd[ASet]; > = emptyGoalList . --- MembAx --- eq < M, cmb T : St if ECo /\ GT = 'not_[GT] /\ ECd[ASet]; > = emptyGoalList . eq < M, cmb T : St if ECo /\ 'not_[GT] = GT /\ ECd[ASet]; > = emptyGoalList . --- Rule --- eq < M, crl T1 => T2 if Co /\ GT = 'not_[GT] /\ Cd[ASet]; > = emptyGoalList . eq < M, crl T1 => T2 if Co /\ 'not_[GT] = GT /\ Cd[ASet]; > = emptyGoalList . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #NAT# is inc #LIBRARY# . --- ------------------------------------------------------------------------- var M : Module . vars ASet AS : AttrSet . var St : Sort . vars T T1 T2 : Term . vars GT GT1 GT2 GT3 : GroundTerm . var SSet : SentenceSet . var ESet : EquationSet . --- ------------------------------------------------------------------------- --- 1. GT1 <= GT2 <= GT3 --- --- ------------------------------------------------------------------------- ceq < M,SSet > = emptyGoalList if (eq '_<=_[GT1,GT2] = 'true.Bool [AS].) (eq '_<=_[GT2,GT3] = 'true.Bool [ASet].) ESet := getEqs(M) /\ metaRed(M,'_<_[GT3,GT1]) = 'true.Bool . --- ------------------------------------------------------------------------- --- 2. GT1 <= GT2 < GT3 --- --- ------------------------------------------------------------------------- ceq < M,SSet > = emptyGoalList if (eq '_<=_[GT1,GT2] = 'true.Bool [AS].) (eq '_<_[GT2,GT3] = 'true.Bool [ASet] .) ESet := getEqs(M) /\ metaRed(M,'_<=_[GT3,GT1]) = 'true.Bool . --- ------------------------------------------------------------------------- --- 3. GT1 < GT2 <= GT3 --- --- ------------------------------------------------------------------------- ceq < M,SSet > = emptyGoalList if (eq '_<_[GT1,GT2] = 'true.Bool [AS] .) (eq '_<=_[GT2,GT3] = 'true.Bool [ASet] .) ESet := getEqs(M) /\ metaRed(M,'_<=_[GT3,GT1]) = 'true.Bool . --- ------------------------------------------------------------------------- --- 4. GT1 < GT2 < GT3 --- --- ------------------------------------------------------------------------- ceq < M,SSet > = emptyGoalList if (eq '_<_[GT1,GT2] = 'true.Bool [AS] .) (eq '_<_[GT2,GT3] = 'true.Bool [ASet] .) ESet := getEqs(M) /\ metaRed(M,'_<=_[GT3,'s_[GT1]]) = 'true.Bool . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #TOOL# is inc #REDUCTION# . inc #IMPLICATION# . inc #THEOREM-OF-CONSTANTS# . inc #CASE-ANALYSIS# . inc #UNIFICATION# . inc #INIT# . inc #INDUCTIONX# . inc #BOOL# . inc #NAT# . --- ------------------------------------------------------------------------- var M : Module . vars T T' : Term . var St : Sort . var ASet : AttrSet . --- enhanced equality --- ceq [EN1]: < M,eq T = T' [metadata("enhanced") ASet]; > = emptyGoalList if metaSearch(M,T,T',nil,'*,1000000,0) :: ResultTriple . ceq [EN2]: < M,eq T = T' [metadata("enhanced") ASet]; > = emptyGoalList if metaSearch(M,T',T,nil,'*,1000000,0) :: ResultTriple . --- contradiction ---- ceq [CTe]: < M,eq T = T' [ASet]; > = emptyGoalList if metaSearch(M,'true.Bool,'false.Bool,nil,'*,1000000,0) :: ResultTriple . ceq [CTe]: < M,eq T = T' [ASet]; > = emptyGoalList if metaSearch(M,'false.Bool,'true.Bool,nil,'*,1000000,0) :: ResultTriple . ceq [CTm]: < M,mb T : St [ASet]; > = emptyGoalList if metaSearch(M,'true.Bool,'false.Bool,nil,'*,1000000,0) :: ResultTriple . ceq [CTm]: < M,mb T : St [ASet]; > = emptyGoalList if metaSearch(M,'false.Bool,'true.Bool,nil,'*,1000000,0) :: ResultTriple . ceq [CTr]: < M,rl T => T' [ASet]; > = emptyGoalList if metaSearch(M,'true.Bool,'false.Bool,nil,'*,1000000,0) :: ResultTriple . ceq [CTr]: < M,rl T => T' [ASet]; > = emptyGoalList if metaSearch(M,'false.Bool,'true.Bool,nil,'*,1000000,0) :: ResultTriple . --- tautology --- eq [TLe]: < M,eq T = T [ASet]; > = emptyGoalList . ceq [TLm]: < M,mb T : St [ASet]; > = emptyGoalList if sortLeq(M,leastSort(M,T),St). ceq [TLr]: < M,rl T => T'[ASet]; > = emptyGoalList if metaSearch(M,T,T',nil,'*,unbounded,0) :: ResultTriple . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- **** ************************************************************************************************* **** ************************************************************************************************* **** ************************************************************************************************* *** INTERFACE *** **** ************************************************************************************************* **** ************************************************************************************************* **** ************************************************************************************************* --- ------------------------------------------------------------------------- fmod #PRINTER# is inc #TOOL# . --- ------------------------------------------------------------------------- var H : Header . var IL : ImportList . var StS : SortSet . var SbS : SubsortDeclSet . var OPS : OpDeclSet . var OP : OpDecl . var MS : MembAxSet . var Mb : MembAx . var ES : EquationSet . var E : Equation . var RS : RuleSet . var R : Rule . var PDL : ParameterDeclList . vars MEXP MEXP1 MEXP2 : ModuleExpression . var RnS : RenamingSet . var PL : ParameterList . var TP : Type . var TPL : TypeList . vars CD CD1 CD2 : Condition . var ECD : EqCondition . vars GL GL1 GL2 : #GoalList# . var NGL : #NeGoalList# . var M : Module . var N : Nat . var ATS : AttrSet . var AT : Attr . vars QI QI1 QI2 : Qid . var QIL : QidList . var STR : String . var SS : SentenceSet . vars T T1 T2 : Term . vars ST ST1 ST2 : Sort . --- ------------------------------------------------------------------------- op goalPrint : #GoalList# -> QidList . --- print module --- op modulePrint : Module -> QidList . ceq modulePrint(M) = 'fmod headerPrint(H) 'is importPrint(IL) '\n 'sorts sortPrint(StS) '. subsortPrint(SbS) opPrint(OPS) membPrint(M,MS) eqPrint(M,ES) '\n '. '. '. '\n 'endfm if fmod H is IL sorts StS . SbS OPS MS ES endfm := M . --- ceq modulePrint(M) = 'fth headerPrint(H) 'is importPrint(IL) '\n 'sorts sortPrint(StS) '. subsortPrint(SbS) opPrint(OPS) membPrint(M,MS) eqPrint(M,ES) '\n '. '. '. '\n 'endfth if fth H is IL sorts StS . SbS OPS MS ES endfth := M . --- ceq modulePrint(M) = 'mod headerPrint(H) 'is importPrint(IL) '\n 'sorts sortPrint(StS) '. subsortPrint(SbS) opPrint(OPS) membPrint(M,MS) eqPrint(M,ES) rlPrint(M,RS) '\n '. '. '. '\n 'endm if mod H is IL sorts StS . SbS OPS MS ES RS endm := M . --- ceq modulePrint(M) = 'th headerPrint(H) 'is importPrint(IL) '\n 'sorts sortPrint(StS) '. subsortPrint(SbS) opPrint(OPS) membPrint(M,MS) eqPrint(M,ES) rlPrint(M,RS) '\n '. '. '. '\n 'endth if th H is IL sorts StS . SbS OPS MS ES RS endth := M . --- print header --- op headerPrint : Header -> QidList . eq headerPrint(QI) = '\m QI '\o . eq headerPrint(QI{PDL}) = '\m QI '\o . --- print module expression --- op mexpPrint : ModuleExpression -> QidList . eq mexpPrint(QI) = QI . eq mexpPrint(MEXP1 + MEXP2) = mexpPrint(MEXP1) '+ mexpPrint(MEXP2). eq mexpPrint(MEXP * (RnS)) = mexpPrint(MEXP). eq mexpPrint(MEXP{PL}) = mexpPrint(MEXP). --- print import list --- op importPrint : ImportList -> QidList . eq importPrint(nil) = (nil).QidList . eq importPrint(protecting MEXP . IL)= '\n 'protecting mexpPrint(MEXP) '. importPrint(IL). eq importPrint(including MEXP . IL) = '\n 'including mexpPrint(MEXP) '. importPrint(IL). eq importPrint(extending MEXP . IL) = '\n 'extending mexpPrint(MEXP) '. importPrint(IL). --- print sort set --- op sortPrint : SortSet -> QidList . eq sortPrint(none) = nil . eq sortPrint(ST) = ST . eq sortPrint(ST ; StS) = ST sortPrint(StS). --- print subsort set --- op subsortPrint : SubsortDeclSet -> QidList . eq subsortPrint(subsort ST1 < ST2 . SbS) = '\n 'subsort ST1 '< ST2 '. subsortPrint(SbS). eq subsortPrint(none) = (nil).QidList . --- print type --- op typePrint : TypeList -> QidList . eq typePrint(TP TPL) = TP typePrint(TPL) . eq typePrint(nil) = (nil).QidList . --- print operations --- op opPrint : OpDeclSet -> QidList . eq opPrint(none) = (nil).QidList . eq opPrint((op QI : TPL -> TP [metadata(STR) ATS].) OPS)= '\n 'op QI ': typePrint(TPL) '-> TP '`[ attrPrint(metadata(STR) ATS) '`] '. opPrint(OPS). eq opPrint(OP OPS) = opPrint(OPS) [owise]. --- print condition --- op condPrint : Module Condition -> QidList . eq condPrint(M,nil) = 'nil . eq condPrint(M,T1 = T2) = metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix). eq condPrint(M,T1 := T2) = metaPrettyPrint(M,T1,mixfix) ':= metaPrettyPrint(M,T2,mixfix). eq condPrint(M,T1 => T2) = metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix). eq condPrint(M,T1 : ST) = metaPrettyPrint(M,T1,mixfix) ': ST . ceq condPrint(M,CD1 /\ CD2) = condPrint(M,CD1) '/\ condPrint(M,CD2) if CD1 =/= nil /\ CD2 =/= nil . --- print membership --- op membPrint : Module MembAxSet -> QidList . eq membPrint(M,none) = (nil).QidList . ceq membPrint(M,mb T1 : ST [metadata(STR) ATS]. MS)= '\n 'mb metaPrettyPrint(M,T1,mixfix) ': ST '`[ attrPrint(metadata(STR) ATS) '`] '. membPrint(M,MS) if rat(STR,10) : Nat . ceq membPrint(M,cmb T1 : ST if ECD [metadata(STR) ATS]. MS)= '\n 'cmb metaPrettyPrint(M,T1,mixfix) ': ST 'if condPrint(M,ECD) '`[ attrPrint(metadata(STR) ATS) '`] '. membPrint(M,MS) if rat(STR,10) : Nat . eq membPrint(M,Mb MS) = membPrint(M,MS) [owise] . --- print equation --- op eqPrint : Module EquationSet -> QidList . eq eqPrint(M,none) = (nil).QidList . ceq eqPrint(M,eq T1 = T2[metadata(STR) ATS]. ES)= '\n 'eq metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix) '`[ attrPrint(metadata(STR) ATS) '`] '. eqPrint(M,ES) if rat(STR,10) : Nat . ceq eqPrint(M,ceq T1 = T2 if ECD [metadata(STR) ATS]. ES)= '\n 'ceq metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix) 'if condPrint(M,ECD) '`[ attrPrint(metadata(STR) ATS) '`] '. eqPrint(M,ES) if rat(STR,10) : Nat . eq eqPrint(M,E ES) = eqPrint(M,ES) [owise] . --- print rule --- op rlPrint : Module RuleSet -> QidList . eq rlPrint(M,none) = (nil).QidList . ceq rlPrint(M,rl T1 => T2[metadata(STR) ATS]. RS)= '\n 'rl metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix) '`[ attrPrint(metadata(STR) ATS) '`] '. rlPrint(M,RS) if rat(STR,10) : Nat . ceq rlPrint(M,crl T1 => T2 if CD [metadata(STR) ATS]. RS)= '\n 'crl metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix) 'if condPrint(M,CD) '`[ attrPrint(metadata(STR) ATS) '`] '. rlPrint(M,RS) if rat(STR,10) : Nat . eq rlPrint(M,R RS) = rlPrint(M,RS) [owise] . --- print sentence --- op senPrint : Module SentenceSet -> QidList . eq senPrint(M,none)= (nil).QidList . eq senPrint(M,mb T1 : ST [ATS]; SS)= if ATS == none then '\n 'mb metaPrettyPrint(M,T1,mixfix) ': ST '; senPrint(M,SS) else '\n 'mb metaPrettyPrint(M,T1,mixfix) ': ST '`[ attrPrint(ATS) '`] '; senPrint(M,SS) fi . eq senPrint(M,cmb T1 : ST if ECD[ATS]; SS)= if ATS == none then '\n 'cmb metaPrettyPrint(M,T1,mixfix) ': ST 'if condPrint(M,ECD) '; senPrint(M,SS) else '\n 'cmb metaPrettyPrint(M,T1,mixfix) ': ST 'if condPrint(M,ECD) '`[ attrPrint(ATS) '`] '; senPrint(M,SS) fi . --- eq senPrint(M,eq T1 = T2[ATS]; SS)= if ATS == none then '\n 'eq metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix) '; senPrint(M,SS) else '\n 'eq metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix) '`[ attrPrint(ATS) '`] '; senPrint(M,SS) fi . eq senPrint(M,ceq T1 = T2 if ECD [ATS]; SS)= if ATS == none then '\n 'ceq metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix) 'if condPrint(M,ECD) '; senPrint(M,SS) else '\n 'ceq metaPrettyPrint(M,T1,mixfix) '= metaPrettyPrint(M,T2,mixfix) 'if condPrint(M,ECD) '`[ attrPrint(ATS) '`] '; senPrint(M,SS) fi . --- eq senPrint(M,rl T1 => T2[ATS]; SS)= if ATS == none then '\n 'rl metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix) '; senPrint(M,SS) else '\n 'rl metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix) '`[ attrPrint(ATS) '`] '; senPrint(M,SS) fi . eq senPrint(M,crl T1 => T2 if CD [ATS]; SS)= if ATS == none then '\n 'crl metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix) 'if condPrint(M,CD) '; senPrint(M,SS) else '\n 'crl metaPrettyPrint(M,T1,mixfix) '=> metaPrettyPrint(M,T2,mixfix) 'if condPrint(M,CD) '`[ attrPrint(ATS) '`] '; senPrint(M,SS) fi . --- print statement attributes --- op attrPrint : AttrSet -> QidList . eq attrPrint(none) = nil . eq attrPrint(label(QI) ATS)= '\b 'label QI '\o attrPrint(ATS) . eq attrPrint(metadata(STR) ATS) = '\b 'metadata qid("\"" + STR + "\"") '\o attrPrint(ATS) . eq attrPrint(owise ATS) = '\b 'owise '\o attrPrint(ATS). eq attrPrint(nonexec ATS) = '\b 'nonexec '\o attrPrint(ATS). eq attrPrint(AT ATS) = attrPrint(ATS) [owise]. --- print operator attributes --- eq attrPrint(assoc ATS)= '\b 'assoc '\o attrPrint(ATS). eq attrPrint(comm ATS) = '\b 'com '\o attrPrint(ATS). eq attrPrint(idem ATS) = '\b 'idem '\o attrPrint(ATS). eq attrPrint(iter ATS) = '\b 'iter '\o attrPrint(ATS). eq attrPrint(memo ATS) = '\b 'memo '\o attrPrint(ATS). eq attrPrint(ctor ATS) = '\b 'ctor '\o attrPrint(ATS). eq attrPrint(msg ATS) = '\b 'msg '\o attrPrint(ATS). eq attrPrint(config ATS)= '\b 'config '\o attrPrint(ATS). eq attrPrint(object ATS)= '\b 'object '\o attrPrint(ATS). eq attrPrint(id(QI) ATS)= '\b 'id: QI '\o attrPrint(ATS). eq attrPrint(left-id(QI) ATS) = '\b 'left-id: QI '\o attrPrint(ATS). eq attrPrint(right-id(QI) ATS)= '\b 'right-id: QI '\o attrPrint(ATS). eq attrPrint(prec(N) ATS) = '\b 'prec qid(string(N,10)) '\o attrPrint(ATS). --- print goals --- op goalPrint : #GoalList# -> QidList . eq goalPrint(emptyGoalList) = nil . eq goalPrint(NGL) = '\n '==================================================== goalPrint(NGL,noGoals(NGL)) '==================================================== . op goalPrint : #GoalList# Nat -> QidList . eq goalPrint(emptyGoalList,N) = nil . eq goalPrint(< M,SS > GL,N) = if N == 1 then '\n '\y '--------------------- 'Goal: qid(string(N,10)) '--------------------- '\o '\n '< modulePrint(M) '`, senPrint(M,SS) '> '\n '\y '------------------- 'Current 'goal '------------------- '\o '\n else '\n '\y '--------------------- 'Goal: qid(string(N,10)) '--------------------- '\o '\n '< modulePrint(M) '`, senPrint(M,SS) '> '\n '\y '---------------------------------------------------- '\o '\n goalPrint(GL,sd(N,1)) fi . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #PARSER# is inc #TOOL# . --- ------------------------------------------------------------------------- vars QI QI1 QI2 : Qid . vars ST ST1 ST2 : Sort . vars QIL QIC QIA : QidList . vars NQIL NQIL1 NQIL2 NQIS : NeQidList . var M : Module . vars T T1 T2 : Term . vars SN SN1 SN2 : Sentence . vars SS SS1 : SentenceSet . vars STR STN STR1 STR2 : String . var AT : Attr . var ATS : AttrSet . var ECD : EqCondition . var N : Nat . var V : Variable . var ASG : Assignment . var SBT : Substitution . vars CD CD1 CD2 : Condition . var ET : [Term] . var ETL : [TermList] . --- ------------------------------------------------------------------------- --- parse substitution --- op substParse : Module QidList ~> Substitution . eq substParse(M,nil) = none . eq substParse(M,NQIL) = substParse(M,nil,NQIL). --- op substParse : Module QidList QidList ~> Substitution . ceq substParse(M,QIL,nil) = ASG if ASG := assignParse(M,QIL). --- substParse(M,QIL,nil) is not defined when assignParse(M,QIL):: Assignment is false --- ceq substParse(M,QIL,QI QIC) = ASG ; SBT if QI == '; /\ ASG := assignParse(M,QIL)/\ SBT := substParse(M,QIC). eq substParse(M,QIL,QI QIC) = substParse(M,QIL QI,QIC)[owise]. --- op assignParse : Module QidList ~> Assignment . ceq assignParse(M,QI '<- NQIL) = V <- T if V := getTerm(metaParse(M,QI,anyType)) /\ T := getTerm(metaParse(M,NQIL,anyType)). --- parse sentence set --- op senSetParse : Module QidList ~> SentenceSet . eq senSetParse(M,nil) = none . eq senSetParse(M,NQIL) = senSetParse(M,nil,NQIL). --- op senSetParse : Module QidList QidList ~> SentenceSet . --- senSetParse(M,QIL,nil) is not defined --- ceq senSetParse(M,QIL,QI QIC) = SN SS if SN := senParse(M,QIL QI) /\ SS := senSetParse(M,QIC). eq senSetParse(M,QIL,QI QIC)= senSetParse(M,QIL QI, QIC)[owise]. --- parse sentence --- op senParse : Module QidList ~> Sentence . --- ceq senParse(M,'eq NQIL '= NQIS ';) = eq T1 = T2[none]; if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq senParse(M,'eq NQIL '= NQIS '`[ QIA '`] ';) = eq T1 = T2[ATS]; if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType))/\ ATS := attrParse(QIA). --- ceq senParse(M,'ceq NQIL '= NQIS 'if QIC ';) = ceq T1 = T2 if condParse(M,QIC)[none]; if condParse(M,QIC): EqCondition /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq senParse(M,'ceq NQIL '= NQIS 'if QIC '`[ QIA '`] ';) = ceq T1 = T2 if condParse(M,QIC)[ATS]; if condParse(M,QIC): EqCondition /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType))/\ ATS := attrParse(QIA). --- ceq senParse(M,'mb NQIL ': ST ';) = mb T1 : ST [none]; if getKind(M,ST): Kind /\ T1 := getTerm(metaParse(M,NQIL,anyType)). ceq senParse(M,'mb NQIL ': ST '`[ QIA '`] ';) = mb T1 : ST [ATS]; if getKind(M,ST): Kind /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ ATS := attrParse(QIA). --- ceq senParse(M,'cmb NQIL ': ST 'if QIC ';) = cmb T1 : ST if ECD[none]; if getKind(M,ST) : Kind /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ ECD := condParse(M,QIC). ceq senParse(M,'cmb NQIL ': ST 'if QIC '`[ QIA '`] ';) = cmb T1 : ST if ECD[ATS]; if getKind(M,ST): Kind /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ ECD := condParse(M,QIC)/\ ATS := attrParse(QIA). --- ceq senParse(M,'rl NQIL '=> NQIS ';) = rl T1 => T2[none]; if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq senParse(M,'rl NQIL '=> NQIS '`[ QIA '`] ';) = rl T1 => T2[ATS]; if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType))/\ ATS := attrParse(QIA). --- ceq senParse(M,'crl NQIL '=> NQIS 'if QIC ';) = crl T1 => T2 if condParse(M,QIC)[none]; if condParse(M,QIC): Condition /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq senParse(M,'crl NQIL '=> NQIS 'if QIC '`[ QIA '`] ';) = crl T1 => T2 if condParse(M,QIC)[ATS]; if condParse(M,QIC): Condition /\ T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType))/\ ATS := attrParse(QIA). --- parse condition --- op condParse : Module QidList ~> Condition . eq condParse(M,nil) = (nil).EqCondition . eq condParse(M,NQIL) = condParse(M,nil,NQIL). --- op condParse : Module QidList QidList ~> Condition . ceq condParse(M,QIL,nil) = CD if CD := oneCondParse(M,QIL). --- conParse(M,QIL,nil) is not defined when oneCondParse(M,QIL) :: Condition is false ceq condParse(M,QIL,QI QIC) = CD1 /\ CD2 if (QI == '/\) /\ CD1 := oneCondParse(M,QIL)/\ CD2 := condParse(M,QIC). eq condParse(M,QIL,QI QIC) = condParse(M,QIL QI,QIC) [owise]. --- parse one condition --- op oneCondParse : Module QidList ~> Condition . ceq oneCondParse(M,NQIL '= NQIS) = (T1 = T2) if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq oneCondParse(M,NQIL ':= NQIS) = (T1 := T2) if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq oneCondParse(M,NQIL '=> NQIS) = (T1 => T2) if T1 := getTerm(metaParse(M,NQIL,anyType))/\ T2 := getTerm(metaParse(M,NQIS,anyType)). ceq oneCondParse(M,NQIL ': ST) = (T1 : ST) if getKind(M,ST): Kind /\ T1 := getTerm(metaParse(M,NQIL,anyType)). --- parse statement attributes --- op attrParse : QidList ~> AttrSet . eq attrParse(nil) = none . eq attrParse(NQIL) = attrParse(nil,NQIL). op attrParse : QidList QidList ~> AttrSet . --- attrParse(QIL,nil) is not defined --- ceq attrParse(QIL,QI QIC) = AT ATS if AT := oneAttrParse(QIL QI) /\ ATS := attrParse(QIC). eq attrParse(QIL,QI QIC)= attrParse(QIL QI, QIC)[owise]. --- parse one attribute --- op oneAttrParse : QidList ~> Attr . eq oneAttrParse('label QI) = label(QI). ceq oneAttrParse('metadata QI) = metadata(substr(STR,1, sd(length(STR),2))) if STR := string(QI). eq oneAttrParse('owise) = owise . eq oneAttrParse('nonexec) = nonexec . --- parse term list --- op termListParse : Module QidList ~> TermList . eq termListParse(M,nil) = empty . eq termListParse(M,NQIL) = termListParse(M,nil,NQIL). --- op termListParse : Module QidList QidList ~> TermList . ceq termListParse(M,QIL,QI QIC) = if ET :: Term and ETL :: TermList then ET,ETL else termListParse(M,QIL QI,QIC) fi if ET := getTerm(metaParse(M,QIL QI,anyType)) /\ ETL := termListParse(M,QIC). --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #GRAMMAR# is inc #TOOL# . --- ------------------------------------------------------------------------- sorts #Tactic# #NeTacticList# #TacticList# . subsort #Tactic# < #NeTacticList# < #TacticList# . op none : -> #TacticList# [ctor]. op __ : #TacticList# #TacticList# -> #TacticList# [ctor assoc id: none]. op __ : #NeTacticList# #TacticList# -> #NeTacticList# [ctor assoc id: none]. op __ : #TacticList# #NeTacticList# -> #NeTacticList# [ctor assoc id: none]. --- ------------------------------------------------------------------------- sort #Module# . op bModule : Qid -> #Module#[ctor] . --- ------------------------------------------------------------------------- sorts #Sentence# #SentenceSet# . subsort #Sentence# < #SentenceSet# . op bSentence : QidList -> #Sentence#[ctor]. op bSentenceSet : QidList -> #SentenceSet#[ctor]. --- ------------------------------------------------------------------------- sort #Nat# . op bNat : Qid -> #Nat#[ctor] . --- ------------------------------------------------------------------------- sorts #Term# #TermList# . subsort #Term# < #TermList# . op bTermList : QidList -> #TermList# [ctor]. op bTerm : NeQidList -> #Term# [ctor]. --- ------------------------------------------------------------------------- sorts #Assignment# #Substitution# . subsort #Assignment# < #Substitution# . op bAssignment : QidList -> #Assignment# . op bSubstitution : QidList -> #Substitution# . --- ------------------------------------------------------------------------- op goal_|-_ : #Module# #SentenceSet# -> #Tactic# [ctor]. op #select# : #Nat# -> #Tactic# [ctor]. op #.# : -> #Tactic# [ctor]. --- general proof tactics --- ops #red# #imp# #tc# #ca# #ca-1# : -> #Tactic# [ctor]. op #ind-on# : #TermList# -> #Tactic# [ctor]. op #init# : String #Substitution# -> #Tactic# [ctor]. op #init# : #Sentence# #Substitution# -> #Tactic# [ctor]. ops #cp-l# #cp-r# : String String #Nat# -> #Tactic# [ctor]. ops #cp-l# #cp-r# : #Sentence# #Sentence# #Nat# -> #Tactic# [ctor]. --- specific proof tactics -- ops #pair# #cs# : -> #Tactic# [ctor]. ops #indx-on# : #TermList# -> #Tactic# [ctor]. --- ------------------------------------------------------------------------- sort #Command# . subsort #TacticList# < #Command# . ops #rollback# #show-proof# #show-goals# #show-current-goal# : -> #Command# . op #redTerm# : #Term# -> #Command# . --- ------------------------------------------------------------------------- sorts #NeSeqTacticList# #SeqTacticList# . subsorts #TacticList# < #NeSeqTacticList# < #SeqTacticList# . op empty : -> #SeqTacticList# [ctor]. op _*_ : #NeSeqTacticList# #SeqTacticList# -> #NeSeqTacticList# [ctor assoc id: empty prec 42]. op _*_ : #SeqTacticList# #NeSeqTacticList# -> #NeSeqTacticList# [ctor assoc id: empty prec 42]. op _*_ : #SeqTacticList# #SeqTacticList# -> #SeqTacticList# [ctor assoc id: empty prec 42]. --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #COMMAND-PRINTER# is inc #GRAMMAR# . --- ------------------------------------------------------------------------- vars QI QI1 QI2 : Qid . vars NQIL NQIL1 NQIL2 : NeQidList . vars QIL QIL1 QIL2 : QidList . var CM : #Tactic# . var CML : #TacticList# . var NCML : #NeTacticList# . var STR STR1 STR2 : String . var NSCML : #NeSeqTacticList# . var N : Nat . var Nz : NzNat . --- ------------------------------------------------------------------------- op tacticPrint : #Tactic# -> QidList . --- ------------------------------------------------------------------------- eq tacticPrint(goal bModule(QI) |- bSentenceSet(NQIL)) = 'goal QI '|- bSenPrint(NQIL) . op bSenPrint : QidList -> QidList . eq bSenPrint(nil) = nil . eq bSenPrint(QI QIL) = if QI == 'eq or QI == 'ceq or QI == 'mb or QI == 'cmb or QI == 'rl or QI == 'crl then '\n QI bSenPrint(QIL) else QI bSenPrint(QIL) fi . --- eq tacticPrint(#.#) = '. . --- eq tacticPrint(#select#(bNat(QI))) = 'select QI . --- print general tactics --- eq tacticPrint(#red#) = 'red . eq tacticPrint(#imp#) = 'imp . eq tacticPrint(#tc#) = 'tc . eq tacticPrint(#ca#) = 'ca . eq tacticPrint(#ca-1#) = 'ca-1 . --- eq tacticPrint(#ind-on#(bTermList(QIL))) = 'ind 'on QIL . --- eq tacticPrint(#init#(STR,bSubstitution(QIL))) = 'init qid(STR) 'by QIL . eq tacticPrint(#init#(bSentence(QI NQIL),bSubstitution(QIL))) = 'init QI NQIL 'by QIL . --- print critical pairs --- eq tacticPrint(#cp-l#(STR1,STR2,bNat(QI))) = if QI == '0 then 'cp-l qid(STR1) '>< qid(STR2) else 'cp-l qid(STR1) '>< qid(STR2) 'skip QI fi . eq tacticPrint(#cp-r#(STR1,STR2,bNat(QI))) = if QI == '0 then 'cp-r qid(STR1) '>< qid(STR2) else 'cp-r qid(STR1) '>< qid(STR2) 'skip QI fi . eq tacticPrint(#cp-l#(bSentence(QI1 NQIL1),bSentence(QI2 NQIL2),bNat(QI))) = if QI == '0 then 'cp-l QI1 NQIL1 '>< QI2 NQIL2 else 'cp-l QI1 NQIL1 '>< QI2 NQIL2 'skip QI fi . eq tacticPrint(#cp-r#(bSentence(QI1 NQIL1),bSentence(QI2 NQIL2),bNat(QI))) = if QI == '0 then 'cp-r QI1 NQIL1 '>< QI2 NQIL2 else 'cp-r QI1 NQIL1 '>< QI2 NQIL2 'skip QI fi . --- specific tactics --- eq tacticPrint(#pair#) = 'pair . eq tacticPrint(#cs#) = 'cs . eq tacticPrint(#indx-on#(bTermList(QIL))) = 'indx 'on QIL . --- ------------------------------------------------------------------------- op tacticListPrint : #TacticList# -> QidList . --- ------------------------------------------------------------------------- eq tacticListPrint(none) = nil . eq tacticListPrint(NCML) = tacticListPrint(0,NCML) . --- ------------------------------------------------------------------------- op tacticListPrint : Nat #TacticList# -> QidList . --- ------------------------------------------------------------------------- eq tacticListPrint(0,CM) = '`( tacticPrint(CM) '`) . eq tacticListPrint(Nz,CM) = tacticPrint(CM) '`) . eq tacticListPrint(0 ,CM NCML)= '`( tacticPrint(CM) tacticListPrint(1,NCML). eq tacticListPrint(Nz,CM NCML)= tacticPrint(CM) tacticListPrint(Nz + 1,NCML). --- ------------------------------------------------------------------------- op seqTacticListPrint : #SeqTacticList# -> QidList . eq seqTacticListPrint(empty) = nil . eq seqTacticListPrint(NSCML) = seqTacticListPrint(1,NSCML). --- op seqTacticListPrint : Nat #SeqTacticList# -> QidList . eq seqTacticListPrint(N,CML)= '\n '*** qid(string(N,10)) '*** '\n tacticListPrint(CML) . eq seqTacticListPrint(N,none * NSCML) = seqTacticListPrint(N,NSCML). eq seqTacticListPrint(N,NCML * NSCML) = '\n '*** qid(string(N,10)) '*** '\n tacticListPrint(NCML) seqTacticListPrint(N + 1 ,NSCML). --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #COMMAND-PARSER# is inc #GRAMMAR# . --- ------------------------------------------------------------------------- vars QI QI1 QI2 : Qid . vars NQIL NQIL1 NQIL2 : NeQidList . vars QIL QIL1 QIL2 : QidList . var CM : #Tactic# . var CML : #TacticList# . --- ------------------------------------------------------------------------- op tacticParse : QidList ~> #Tactic# . --- ------------------------------------------------------------------------- eq tacticParse('goal QI '|- NQIL) = goal bModule(QI) |- bSentenceSet(NQIL) . eq tacticParse('.) = #.# . eq tacticParse('select QI) = #select#(bNat(QI)). --- parse general tactics --- eq tacticParse('red) = #red# . eq tacticParse('imp) = #imp# . eq tacticParse('tc) = #tc# . eq tacticParse('ca) = #ca# . eq tacticParse('ca-1)= #ca-1# . eq tacticParse('ind 'on QIL)= #ind-on#(bTermList(QIL)). --- parse init --- eq tacticParse('init QI 'by QIL) = #init#(string(QI) ,bSubstitution(QIL)). eq tacticParse('init QI NQIL 'by QIL) = #init#(bSentence(QI NQIL),bSubstitution(QIL)). --- parse critical pairs --- eq tacticParse('cp-l QI1 '>< QI2 'skip QI ) = #cp-l#(string(QI1),string(QI2),bNat(QI)). eq tacticParse('cp-r QI1 '>< QI2 'skip QI ) = #cp-r#(string(QI1),string(QI2),bNat(QI)). eq tacticParse('cp-l QI1 NQIL1 '>< QI2 NQIL2 'skip QI) = #cp-l#(bSentence(QI1 NQIL1),bSentence(QI2 NQIL2),bNat(QI)). eq tacticParse('cp-r QI1 NQIL1 '>< QI2 NQIL2 'skip QI) = #cp-r#(bSentence(QI1 NQIL1),bSentence(QI2 NQIL2),bNat(QI)). --- eq tacticParse('cp-l QI1 '>< QI2) = #cp-l#(string(QI1),string(QI2),bNat('0)). eq tacticParse('cp-r QI1 '>< QI2) = #cp-r#(string(QI1),string(QI2),bNat('0)). eq tacticParse('cp-l QI1 NQIL1 '>< QI2 NQIL2) = #cp-l#(bSentence(QI1 NQIL1),bSentence(QI2 NQIL2),bNat('0)). eq tacticParse('cp-r QI1 NQIL1 '>< QI2 NQIL2) = #cp-r#(bSentence(QI1 NQIL1),bSentence(QI2 NQIL2),bNat('0)). --- parse specific tactics --- eq tacticParse('pair) = #pair# . eq tacticParse('cs) = #cs# . eq tacticParse('indx 'on QIL) = #indx-on#(bTermList(QIL)). --- ------------------------------------------------------------------------- op tacticListParse : QidList ~> #TacticList# . --- ------------------------------------------------------------------------- eq tacticListParse(nil) = none . eq tacticListParse(NQIL)= tacticListParse(nil,NQIL). --- ------------------------------------------------------------------------- op tacticListParse : QidList QidList ~> #TacticList# . --- ceq tacticListParse(QIL,QI QIL1)= CM CML if CM := tacticParse(QIL QI) /\ CML := tacticListParse(QIL1) . eq tacticListParse(QIL,QI QIL1)= tacticListParse(QIL QI, QIL1)[owise]. --- ------------------------------------------------------------------------- op commandParse : QidList ~> #Command# . --- ------------------------------------------------------------------------- eq commandParse('redTerm NQIL) = #redTerm#(bTerm(NQIL)) . eq commandParse('rollback) = #rollback# . eq commandParse('show 'proof) = #show-proof# . eq commandParse('show 'goals) = #show-goals# . eq commandParse('show 'current 'goal)= #show-current-goal# . eq commandParse(NQIL) = tacticListParse(NQIL)[owise]. --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- fmod #COMPUTE# is inc #PARSER# . inc #GRAMMAR# . --- ------------------------------------------------------------------------- var QI : Qid . vars NQIL NQIL1 NQIL2 : NeQidList . vars QIL QIL1 QIL2 : QidList . vars GL GL1 GL2 : #GoalList# . var G : #Goal# . vars SS SS1 SS2 : SentenceSet . var M : Module . var NGL : #NeGoalList# . vars STR STR1 STR2 : String . var EGL : [#GoalList#] . var EM : [Module] . var ESS : [SentenceSet] . var EN : [Nat] . vars ESN ESN1 ESN2 : [Sentence] . var ESUB : [Substitution] . var CM : #Tactic# . var TCL : #TacticList# . var NTCL : #NeTacticList# . var N : Nat . var ETL : [TermList] . --- ------------------------------------------------------------------------- --- compute commands --- --- ------------------------------------------------------------------------- sort #Result# . op `[_`,_`] : #GoalList# QidList -> #Result# [ctor]. op compute : #TacticList# #GoalList# -> #Result# . --- ------------------------------------------------------------------------- eq compute(none,GL)= [GL,nil] . eq compute(NTCL,GL)= compute(1,NTCL,GL). --- ------------------------------------------------------------------------- op compute : Nat #TacticList# #GoalList# -> #Result# . --- ------------------------------------------------------------------------- eq compute(N,none,GL) = [GL,nil]. eq compute(N,CM TCL,emptyGoalList)= compute(N + 1, TCL,emptyGoalList)[owise]. --- goal --- ceq compute(N,(goal bModule(QI) |- bSentenceSet(NQIL)) TCL,GL)= if not(EM :: Module) then [GL, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'module 'name '\o] else if not(ESS :: SentenceSet) then [GL, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'sentence 'set '\o] else compute(N + 1,TCL,GL < EM,ESS >) fi fi if EM := upModule(QI,true) /\ ESS := senSetParse(EM,NQIL). --- select --- ceq compute(N,#select#(bNat(QI)) TCL,NGL)= if not(EN :: Nat) then [NGL,'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'number '\o] else if EN == 0 or noGoals(NGL) < EN then [NGL,'ERROR '`( qid(string(N,10)) '`) ': '\m 'select 'in ' '`[ '1 '. '. '. qid(string(noGoals(NGL),10)) '`] '\o] else compute(N + 1,TCL,EGL) fi fi if EN := rat(string(QI),10)/\ EGL := select(NGL,EN). --- current --- ceq compute(N,#.# TCL,GL G) = if QIL :: NeQidList then [GL G,QIL] else [GL GL1,QIL] fi if [GL1,QIL] := compute(N + 1,TCL,G). --- general tactics --- eq compute(N,#red# TCL,NGL) = compute(N + 1,TCL,red(NGL)). eq compute(N,#imp# TCL,NGL) = compute(N + 1,TCL,imp(NGL)). eq compute(N,#tc# TCL,NGL) = compute(N + 1,TCL,tc(NGL)). eq compute(N,#ca# TCL,NGL) = compute(N + 1,TCL,ca(NGL)). eq compute(N,#ca-1# TCL,NGL) = compute(N + 1,TCL,ca-1(NGL)). --- ind on --- ceq compute(N,#ind-on#(bTermList(QIL)),GL < M, SS >)= if not(ETL :: TermList) then [GL < M,SS >,'ERROR '`( qid(string(N,10)) '`) ': '\m 'variable 'list 'is 'invalid '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi if ETL := termListParse(M,QIL)/\ EGL := ind(addComment(< M,SS >,ETL))/\ [GL1,QIL1] := compute(N,#ind-on#(bTermList(QIL)),GL). ceq compute(N,#ind-on#(bTermList(QIL)) NTCL,NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#ind-on#(bTermList(QIL)),NGL) . --- init --- ceq compute(N,#init#(STR,bSubstitution(QIL)),GL < M,SS >)= if (SS1 == none) then [GL < M,SS >,'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'sentence 'name '\o] else if not(ESUB :: Substitution) then [GL < M,SS >,'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'substitution '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi fi if SS1 := getSentence(M,STR) /\ ESUB := substParse(M,QIL) /\ EGL := < INIT(M,SS1,ESUB),SS > /\ [GL1,QIL1] := compute(N,#init#(STR,bSubstitution(QIL)),GL). ceq compute(N,#init#(STR,bSubstitution(QIL)) NTCL,NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#init#(STR,bSubstitution(QIL)),NGL). --- ceq compute(N,#init#(bSentence(NQIL),bSubstitution(QIL)),GL < M,SS >)= if not(ESN :: Sentence) then [GL < M,SS >,'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'sentence '\o] else if not(ESUB :: Substitution and EGL :: #GoalList#) then [GL < M,SS >,'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'substitution '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi fi if ESN := senParse(M,NQIL) /\ ESUB := substParse(M,QIL) /\ EGL := < INIT(M,ESN,ESUB),SS > /\ [GL1,QIL1] := compute(N,#init#(bSentence(NQIL),bSubstitution(QIL)),GL). ceq compute(N,#init#(bSentence(NQIL),bSubstitution(QIL)) NTCL,NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#init#(bSentence(NQIL),bSubstitution(QIL)),NGL). --- critical pairs --- ceq compute(N,#cp-l#(STR1,STR2,bNat(QI)), GL < M,SS >)= if not(ESN1 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'first 'sentence 'name 'is 'invalid '\o] else if not(ESN2 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'second 'sentence 'name 'is 'invalid '\o] else if not(EN :: Nat) then [GL < M,SS > , 'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'number '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi fi fi if ESN1 := getSentence(M,STR1)/\ ESN2 := getSentence(M,STR2)/\ EN := rat(string(QI),10) /\ EGL := CP-L(< M,SS >,ESN1,ESN2,EN)/\ [GL1,QIL1] := compute(N,#cp-l#(STR1,STR2,bNat(QI)),GL) . ceq compute(N,#cp-l#(STR1,STR2,bNat(QI)) NTCL, NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#cp-l#(STR1,STR2,bNat(QI)),NGL). --- ceq compute(N,#cp-l#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)),GL < M,SS >)= if not(ESN1 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'first 'sentence 'is 'invalid '\o] else if not(ESN2 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'second 'sentence 'is 'invalid '\o] else if not(EN :: Nat) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'number '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi fi fi if ESN1 := senParse(M,NQIL1)/\ ESN2 := senParse(M,NQIL2)/\ EN := rat(string(QI),10) /\ EGL := CP-L(< M,SS >,ESN1,ESN2,EN)/\ [GL1,QIL1] := compute(N,#cp-l#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)),GL). ceq compute(N,#cp-l#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)) NTCL,NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#cp-l#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)),NGL). --- ceq compute(N,#cp-r#(STR1,STR2,bNat(QI)), GL < M,SS >)= if not(ESN1 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'first 'sentence 'name 'is 'invalid '\o] else if not(ESN2 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'second 'sentence 'name 'is 'invalid '\o] else if not(EN :: Nat) then [GL < M,SS > , 'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'number '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi fi fi if ESN1 := getSentence(M,STR1)/\ ESN2 := getSentence(M,STR2)/\ EN := rat(string(QI),10) /\ EGL := CP-R(< M,SS >,ESN1,ESN2,EN)/\ [GL1,QIL1] := compute(N,#cp-r#(STR1,STR2,bNat(QI)),GL) . ceq compute(N,#cp-r#(STR1,STR2,bNat(QI)) NTCL, NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#cp-r#(STR1,STR2,bNat(QI)),NGL). --- ceq compute(N,#cp-r#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)),GL < M,SS >)= if not(ESN1 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'first 'sentence 'is 'invalid '\o] else if not(ESN2 :: Sentence) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'second 'sentence 'is 'invalid '\o] else if not(EN :: Nat) then [GL < M,SS >, 'ERROR '`( qid(string(N,10)) '`) ': '\m 'invalid 'number '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi fi fi if ESN1 := senParse(M,NQIL1)/\ ESN2 := senParse(M,NQIL2)/\ EN := rat(string(QI),10) /\ EGL := CP-R(< M,SS >,ESN1,ESN2,EN)/\ [GL1,QIL1] := compute(N,#cp-r#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)),GL). ceq compute(N,#cp-r#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)) NTCL,NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#cp-r#(bSentence(NQIL1),bSentence(NQIL2),bNat(QI)),NGL). --- specific tactics --- eq compute(N,#pair# TCL,NGL) = compute(N + 1,TCL,pair(NGL)). eq compute(N,#cs# TCL,NGL) = compute(N + 1,TCL,cs(NGL)). ceq compute(N,#indx-on#(bTermList(QIL)),GL < M,SS >)= if not(ETL :: TermList) then [GL < M,SS >,'ERROR '`( qid(string(N,10)) '`) ': '\m 'variable 'list 'is 'invalid '\o] else if QIL1 :: NeQidList then [GL < M,SS >,QIL1] else [GL1 EGL,nil] fi fi if ETL := termListParse(M,QIL)/\ EGL := indx(addComment(< M,SS >,ETL))/\ [GL1,QIL1] := compute(N,#indx-on#(bTermList(QIL)),GL). ceq compute(N,#indx-on#(bTermList(QIL)) NTCL,NGL)= if QIL1 :: NeQidList then [NGL,QIL1] else compute(N + 1,NTCL,GL1) fi if [GL1,QIL1] := compute(N,#indx-on#(bTermList(QIL)),NGL) . --- ------------------------------------------------------------------------- endfm --- ------------------------------------------------------------------------- --- ------------------------------------------------------------------------- mod #CITP# is inc #PRINTER# . inc #COMMAND-PRINTER# . inc #COMMAND-PARSER# . inc #COMPUTE# . inc LOOP-MODE . --- ------------------------------------------------------------------------- sorts #NeSeqGoalList# #SeqGoalList# . subsorts #GoalList# < #NeSeqGoalList# < #SeqGoalList# . op empty : -> #SeqGoalList# [ctor]. op _*_ : #NeSeqGoalList# #SeqGoalList# -> #NeSeqGoalList# [ctor assoc id: empty prec 42]. op _*_ : #SeqGoalList# #NeSeqGoalList# -> #NeSeqGoalList# [ctor assoc id: empty prec 42]. op _*_ : #SeqGoalList# #SeqGoalList# -> #SeqGoalList# [ctor assoc id: empty prec 42]. --- ------------------------------------------------------------------------- op <_,_,_,_> : #Command# #SeqTacticList# #SeqGoalList# QidList -> State . op init : -> System . --- ------------------------------------------------------------------------- vars QIL QIL1 QIL2 : QidList . vars GL GL1 GL2 : #GoalList# . var NTCL : #NeTacticList# . var TCL : #TacticList# . var SS : SentenceSet . var M : Module . var NQIL : NeQidList . var SGL : #SeqGoalList# . var NSGL : #NeSeqGoalList# . var NSTCL : #NeSeqTacticList# . var STCL : #SeqTacticList# . var ET : [Term] . var ECM : [#Command#] . --- ------------------------------------------------------------------------- eq init = [nil,< none,none,emptyGoalList,nil >, '\n 'Welcome 'to 'Constructor-based 'Inductive 'Theorem 'Prover '\o '\n '\t '--- 'CITP '1.0 'built: 'February '2017 '--- '\n ] . --- in --- crl [in]: [NQIL,< none,NSTCL,NSGL,nil > ,QIL] => if ECM :: #Command# then [nil ,< ECM,NSTCL,NSGL,nil >,QIL] else [nil ,< none,NSTCL,NSGL,nil > , 'ERROR: '\m 'invalid 'command '\o] fi if ECM := commandParse(NQIL). --- out --- rl [out]: [QIL1,< none,NSTCL,NSGL,NQIL >,QIL2] => [QIL1,< none,NSTCL,NSGL,nil >,NQIL]. --- tactics --- crl < NTCL,NSTCL,SGL * GL,nil > => if QIL :: NeQidList then < none,NSTCL,SGL * GL,QIL > else if GL1 == GL then < none,NSTCL,SGL * GL, '\m 'Goal 'Unchanged '\o > else if GL1 == emptyGoalList then < none,NSTCL * NTCL,SGL * GL * GL1, '==================================================== '\n '\m 'Empty 'Goal 'List '\o '\n '==================================================== '\n '\g 'INFO: '\o 'No 'goals 'to 'prove > else < none,NSTCL * NTCL,SGL * GL * GL1, goalPrint(lastGoal(GL1)) '\n '\g 'INFO: '\o qid(string(noGoals(GL1),10)) 'goal`(s`) 'to 'prove '\n > fi fi fi if [GL1,QIL] := compute(NTCL,GL). --- commands --- rl < #rollback#,none,emptyGoalList,nil > => < none,none,emptyGoalList,'\m 'Empty 'Goal 'List '\o > . rl < #rollback#,STCL * TCL * NTCL,SGL * GL1 * GL2,nil > => if GL1 == emptyGoalList then < none,STCL * TCL,SGL * GL1, '\m 'Empty 'Goal 'List '\o > else < none,STCL * TCL,SGL * GL1, goalPrint(lastGoal(GL1)) '\n '\g 'INFO: '\o qid(string(noGoals(GL1),10)) 'goal`(s`) 'to 'prove > fi . --- rl < #show-proof#,NSTCL,NSGL, nil > => if NSTCL == none then < none, NSTCL,NSGL, '\g 'none '\o > else < none, NSTCL,NSGL, '\g seqTacticListPrint(NSTCL) '\o > fi . rl < #show-goals#,NSTCL,SGL * GL, nil > => if GL == emptyGoalList then < none, NSTCL,SGL * GL, '\m 'Empty 'Goal 'List '\o > else < none, NSTCL,SGL * GL, goalPrint(GL) > fi . --- rl < #show-current-goal#,NSTCL,SGL * emptyGoalList,nil > => < none,NSTCL,SGL * emptyGoalList,'\m 'Empty 'Goal 'List '\o > . rl < #show-current-goal#,NSTCL,SGL * GL < M,SS > ,nil > => < none,NSTCL,SGL * GL < M,SS >,goalPrint(< M,SS >) '\n '\g 'INFO: '\o qid(string(noGoals(GL)+ 1,10)) 'goal`(s`) 'to 'prove > . --- rl < #redTerm#(bTerm(NQIL)),STCL,emptyGoalList,nil > => < none,none,emptyGoalList,'\m 'Empty 'Goal 'List '\o > . crl < #redTerm#(bTerm(NQIL)),STCL,SGL * (GL < M,SS >),nil > => if ET :: Term then < none,STCL,SGL * (GL < M,SS >),'\m metaPrettyPrint(M,metaRed(M,ET),mixfix) '\o > else < none,STCL,SGL * (GL < M,SS >),'\m 'invalid 'term '\o > fi if ET := getTerm(metaParse(M,NQIL,anyType)). --- ------------------------------------------------------------------------- endm --- ------------------------------------------------------------------------- loop init .