:: On Defining Functions on Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 12, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, XBOOLE_0, FINSEQ_1, TREES_3, SUBSET_1, RELAT_1,
FUNCT_1, TARSKI, TREES_2, TREES_4, ZFMISC_1, MCART_1, LANG1, STRUCT_0,
TDGROUP, CARD_3, ARYTM_3, NAT_1, XXREAL_0, FINSET_1, TREES_1, TREES_A,
FUNCT_6, PRE_POLY, ORDINAL4, FINSEQ_2, DTCONSTR;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
FINSET_1, XTUPLE_0, MCART_1, CARD_3, DOMAIN_1, LANG1, TREES_1, TREES_2,
FINSEQ_4, TREES_3, TREES_4, FINSEQOP, XXREAL_0, NAT_1, PRE_POLY;
constructors PARTFUN1, BINOP_1, DOMAIN_1, SETWISEO, XXREAL_0, XREAL_0, NAT_1,
CARD_3, FINSEQOP, FINSEQ_4, FINSOP_1, TREES_4, LANG1, RELSET_1, PRE_POLY,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1,
FINSEQ_1, TREES_1, TREES_2, TREES_3, STRUCT_0, LANG1, FINSET_1, CARD_1,
FINSEQ_2, TREES_4, VALUED_0, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
theorem :: DTCONSTR:1 :: This really belongs elsewhere
for D being non empty set, p being FinSequence of FinTrees D holds
p is FinSequence of Trees D;
theorem :: DTCONSTR:2
for x,y being set, p being FinSequence of x st y in dom p holds p.y in x;
registration
let D be non empty set, T be DTree-set of D;
cluster -> DTree-yielding for FinSequence of T;
end;
definition
let D be non empty set;
let F be non empty DTree-set of D;
let Tset be non empty Subset of F;
redefine mode Element of Tset -> Element of F;
end;
definition
let D be non empty set, T be DTree-set of D;
let p be FinSequence of T;
redefine func roots p -> FinSequence of D;
end;
theorem :: DTCONSTR:3
roots {} = {};
theorem :: DTCONSTR:4
for T being DecoratedTree holds roots <*T*> = <*T.{}*>;
theorem :: DTCONSTR:5
for D being non empty set, F being (Subset of FinTrees D),
p being FinSequence of F st len roots p = 1
ex x being Element of FinTrees D st p = <*x*> & x in F;
theorem :: DTCONSTR:6
for T1, T2 being DecoratedTree holds roots <*T1, T2*> = <*T1.{}, T2.{}*>;
definition
let X, Y be set, f be FinSequence of [:X, Y:];
redefine func pr1 f -> FinSequence of X;
redefine func pr2 f -> FinSequence of Y;
end;
theorem :: DTCONSTR:7
pr1 {} = {} & pr2 {} = {};
begin
registration
let A be non empty set, R be Relation of A,A*;
cluster DTConstrStr(#A,R#) -> non empty;
end;
scheme :: DTCONSTR:sch 1
DTConstrStrEx { S() -> non empty set, P[object,object] }:
ex G be strict non empty DTConstrStr st the carrier of G = S() &
for x being Symbol of G, p being FinSequence of the carrier of G
holds x ==> p iff P[x, p];
scheme :: DTCONSTR:sch 2
DTConstrStrUniq { S() -> non empty set, P[set, set] }:
for G1, G2 being strict non empty DTConstrStr st (the carrier of G1 = S() &
for x being Symbol of G1, p being FinSequence of the carrier of G1
holds x ==> p iff P[x, p]) & (the carrier of G2 = S() &
for x being Symbol of G2, p being FinSequence of the carrier of G2
holds x ==> p iff P[x, p]) holds G1 = G2;
theorem :: DTCONSTR:8
for G being non empty DTConstrStr holds Terminals G misses NonTerminals G;
scheme :: DTCONSTR:sch 3
DTCMin { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
ex X being Subset of FinTrees [:the carrier of G(), D():] st X = Union f() &
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, TermVal(d)] in X) & (for o being Symbol of G(),
p being FinSequence of X st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in X ) &
for F being Subset of FinTrees [:the carrier of G(), D():] st
(for d being Symbol of G() st d in Terminals G()
holds root-tree [d, TermVal(d)] in F ) & (for o being Symbol of G(),
p being FinSequence of F st o ==> pr1 roots p
holds [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p in F) holds X c= F
provided
dom f() = NAT and
f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q };
scheme :: DTCONSTR:sch 4
DTCSymbols { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
ex X1 being Subset of FinTrees(the carrier of G()) st
X1 = { t`1 where t is Element of FinTrees [:(the carrier of G()), D():] :
t in Union f() } &
(for d being Symbol of G() st d in Terminals G() holds root-tree d in X1) &
(for o being Symbol of G(), p being FinSequence of X1 st o ==> roots p
holds o-tree p in X1) & for F being Subset of FinTrees the carrier of G() st
(for d being Symbol of G() st d in Terminals G() holds root-tree d in F) &
(for o being Symbol of G(), p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds X1 c= F
provided
dom f() = NAT and
f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q };
scheme :: DTCONSTR:sch 5
DTCHeight { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
for n being Nat, dt being Element of FinTrees [:the carrier of G(), D():]
st dt in Union f() holds dt in f().n iff height dom dt <= n
provided
dom f() = NAT and
f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q };
scheme :: DTCONSTR:sch 6
DTCUniq { f() -> Function,
G() -> non empty DTConstrStr, D() -> non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D()}:
for dt1, dt2 being DecoratedTree of [:(the carrier of G()), D():]
st dt1 in Union f() & dt2 in Union f() & dt1`1 = dt2`1 holds dt1 = dt2
provided
dom f() = NAT and
f().0 = { root-tree [t, d] where t is Symbol of G(), d is Element of D() :
t in Terminals G() & d = TermVal(t) or t ==> {} & d = NTermVal(t, {}, {}) } and
for n being Nat holds f().(n+1) =
f().n \/ { [o, NTermVal(o, pr1 roots p, pr2 roots p)]-tree p
where o is Symbol of G(), p is Element of (f().n)* :
ex q being FinSequence of FinTrees [:the carrier of G(), D():] st
p = q & o ==> pr1 roots q };
definition
let G be non empty DTConstrStr;
func TS(G) -> Subset of FinTrees(the carrier of G) means
:: DTCONSTR:def 1
(for d being Symbol of G st d in Terminals G holds root-tree d in it) &
(for o being Symbol of G, p being FinSequence of it st o ==> roots p
holds o-tree p in it) & for F being Subset of FinTrees the carrier of G st
(for d being Symbol of G st d in Terminals G holds root-tree d in F) &
(for o being Symbol of G, p being FinSequence of F st o ==> roots p
holds o-tree p in F) holds it c= F;
end;
scheme :: DTCONSTR:sch 7
DTConstrInd{ G()->non empty DTConstrStr, P[set] }:
for t being DecoratedTree of the carrier of G() st t in TS(G()) holds P[t]
provided
for s being Symbol of G() st s in Terminals G() holds P[root-tree s] and
for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts &
for t being DecoratedTree of the carrier of G() st t in rng ts holds P[t]
holds P[nt-tree ts];
scheme :: DTCONSTR:sch 8
DTConstrIndDef{G()->non empty DTConstrStr, D()->non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D() }:
ex f being Function of TS(G()), D() st
(for t being Symbol of G() st t in Terminals G()
holds f.(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f.(nt-tree ts) = NTermVal(nt, roots ts, f * ts);
scheme :: DTCONSTR:sch 9
DTConstrUniqDef{G()->non empty DTConstrStr, D()->non empty set,
TermVal(set) -> Element of D(), NTermVal(set, set, set) -> Element of D(),
f1, f2() -> Function of TS(G()), D() }: f1() = f2()
provided
(for t being Symbol of G() st t in Terminals G()
holds f1().(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f1().(nt-tree ts) = NTermVal(nt, roots ts, f1() * ts) and
(for t being Symbol of G() st t in Terminals G()
holds f2().(root-tree t) = TermVal(t)) & for nt being Symbol of G(),
ts being FinSequence of TS(G()) st nt ==> roots ts
holds f2().(nt-tree ts) = NTermVal(nt, roots ts, f2() * ts);
begin
definition
func PeanoNat -> strict non empty DTConstrStr means
:: DTCONSTR:def 2
the carrier of it = {0, 1} &
for x being Symbol of it, y being FinSequence of the carrier of it
holds x ==> y iff x=1 & (y=<*0*> or y=<*1*>);
end;
begin
:: Some properties of decorated tree constructions
definition
let G be non empty DTConstrStr;
attr G is with_terminals means
:: DTCONSTR:def 3
Terminals G <> {};
attr G is with_nonterminals means
:: DTCONSTR:def 4
NonTerminals G <> {};
attr G is with_useful_nonterminals means
:: DTCONSTR:def 5
for nt being Symbol of G st nt in NonTerminals G
ex p being FinSequence of TS(G) st nt ==> roots p;
end;
registration
cluster with_terminals with_nonterminals with_useful_nonterminals strict
for non empty DTConstrStr;
end;
definition
let G be with_terminals non empty DTConstrStr;
redefine func Terminals G -> non empty Subset of G;
end;
registration
let G be with_terminals non empty DTConstrStr;
cluster TS G -> non empty;
end;
registration
let G be with_useful_nonterminals non empty DTConstrStr;
cluster TS G -> non empty;
end;
definition
let G be with_nonterminals non empty DTConstrStr;
redefine func NonTerminals G -> non empty Subset of G;
end;
definition
let G be with_terminals non empty DTConstrStr;
mode Terminal of G is Element of Terminals G;
end;
definition
let G be with_nonterminals non empty DTConstrStr;
mode NonTerminal of G is Element of NonTerminals G;
end;
definition
let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;
let nt be NonTerminal of G;
mode SubtreeSeq of nt -> FinSequence of TS(G) means
:: DTCONSTR:def 6
nt ==> roots it;
end;
definition
let G be with_terminals non empty DTConstrStr;
let t be Terminal of G;
redefine func root-tree t -> Element of TS(G);
end;
definition
let G be with_nonterminals with_useful_nonterminals non empty DTConstrStr;
let nt be NonTerminal of G;
let p be SubtreeSeq of nt;
redefine func nt-tree p -> Element of TS(G);
end;
theorem :: DTCONSTR:9
for G being with_terminals non empty DTConstrStr,
tsg being Element of TS G, s being Terminal of G
st tsg.{} = s holds tsg = root-tree s;
theorem :: DTCONSTR:10
for G being with_terminals with_nonterminals non empty DTConstrStr,
tsg being Element of TS G, nt being NonTerminal of G st tsg.{} = nt
ex ts being FinSequence of TS G st tsg = nt-tree ts & nt ==> roots ts;
begin
:: Peano naturals continued
registration
cluster PeanoNat ->
with_terminals with_nonterminals with_useful_nonterminals;
end;
definition
let nt be NonTerminal of PeanoNat, t be Element of TS PeanoNat;
redefine func nt-tree t -> Element of TS PeanoNat;
end;
definition
let x be FinSequence of NAT;
func plus-one x -> Element of NAT equals
:: DTCONSTR:def 7
(x.1) + 1;
end;
definition
func PN-to-NAT -> Function of TS(PeanoNat), NAT means
:: DTCONSTR:def 8
(for t being Symbol of PeanoNat st t in Terminals PeanoNat
holds it.(root-tree t) = 0) & for nt being Symbol of PeanoNat,
ts being FinSequence of TS(PeanoNat) st nt ==> roots ts
holds it.(nt-tree ts) = plus-one(it * ts);
end;
definition
let x be Element of TS(PeanoNat);
func PNsucc x -> Element of TS(PeanoNat) equals
:: DTCONSTR:def 9
1-tree <*x*>;
end;
definition
func NAT-to-PN -> sequence of TS(PeanoNat) means
:: DTCONSTR:def 10
it.0 = root-tree 0 & for n being Nat holds it.(n+1) = PNsucc it.n;
end;
theorem :: DTCONSTR:11
for pn being Element of TS(PeanoNat) holds pn = NAT-to-PN.(PN-to-NAT.pn);
theorem :: DTCONSTR:12
for n being Nat holds n = PN-to-NAT.(NAT-to-PN.n);
begin
:: Tree traversals and terminal language
definition
let G be non empty DTConstrStr, tsg be DecoratedTree of the carrier of G;
assume
tsg in TS G;
func TerminalString tsg -> FinSequence of Terminals G means
:: DTCONSTR:def 11
ex f being Function of (TS G), (Terminals G)* st it = f.tsg &
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts
holds f.(nt-tree ts) = FlattenSeq(f * ts);
func PreTraversal tsg -> FinSequence of the carrier of G means
:: DTCONSTR:def 12
ex f being Function of (TS G), (the carrier of G)* st it = f.tsg &
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
ts being FinSequence of TS(G),
rts being FinSequence st rts = roots ts & nt ==> rts
for x being FinSequence of (the carrier of G)* st x = f * ts
holds f.(nt-tree ts) = <*nt*>^FlattenSeq(x);
func PostTraversal tsg -> FinSequence of the carrier of G means
:: DTCONSTR:def 13
ex f being Function of (TS G), (the carrier of G)* st it = f.tsg &
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = <*t*>) & for nt being Symbol of G,
ts being FinSequence of TS(G),
rts being FinSequence st rts = roots ts & nt ==> rts
for x being FinSequence of (the carrier of G)* st x = f * ts
holds f.(nt-tree ts) = FlattenSeq(x)^<*nt*>;
end;
definition
let G be with_nonterminals non empty non empty DTConstrStr,
nt be Symbol of G;
func TerminalLanguage nt -> Subset of (Terminals G)* equals
:: DTCONSTR:def 14
{ TerminalString tsg where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
func PreTraversalLanguage nt -> Subset of (the carrier of G)* equals
:: DTCONSTR:def 15
{ PreTraversal tsg where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
func PostTraversalLanguage nt -> Subset of (the carrier of G)* equals
:: DTCONSTR:def 16
{ PostTraversal tsg where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
end;
theorem :: DTCONSTR:13
for t being DecoratedTree of the carrier of PeanoNat
st t in TS PeanoNat holds TerminalString t = <*0*>;
theorem :: DTCONSTR:14
for nt being Symbol of PeanoNat holds TerminalLanguage nt = {<*0*>};
theorem :: DTCONSTR:15
for t being Element of TS PeanoNat
holds PreTraversal t = ((height dom t) |-> 1)^<*0*>;
theorem :: DTCONSTR:16
for nt being Symbol of PeanoNat holds
(nt = 0 implies PreTraversalLanguage nt = {<*0*>}) &
(nt = 1 implies PreTraversalLanguage nt = { (n|->1)^<*0*>
where n is Element of NAT : n <> 0 });
theorem :: DTCONSTR:17
for t being Element of TS PeanoNat
holds PostTraversal t = <*0*>^((height dom t) |-> 1);
theorem :: DTCONSTR:18
for nt being Symbol of PeanoNat holds
(nt = 0 implies PostTraversalLanguage nt = {<*0*>}) &
(nt = 1 implies PostTraversalLanguage nt = { <*0*>^(n|->1)
where n is Element of NAT : n <> 0 });
:: What remains to be done, but in another article:
::
:: - partial trees (grown from the root towards the leaves)
:: - phrases