Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### On Defining Functions on Trees

by
Grzegorz Bancerek, and
Piotr Rudnicki

MML identifier: DTCONSTR
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, TREES_3, RELAT_1, FUNCT_1, FINSET_1, TREES_2, BOOLE,
TREES_4, FUNCT_3, MCART_1, LANG1, TDGROUP, PROB_1, TARSKI, TREES_1,
FUNCT_6, BINOP_1, FINSOP_1, FINSEQ_2, DTCONSTR;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
RELSET_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
FINSET_1, MCART_1, PROB_1, DOMAIN_1, BINOP_1, FINSOP_1, LANG1, TREES_1,
TREES_2, TREES_3, TREES_4, FINSEQOP;
constructors NAT_1, PROB_1, DOMAIN_1, BINOP_1, FINSOP_1, LANG1, TREES_4,
MEMBERED, PARTFUN1, XBOOLE_0, FINSEQOP;
clusters SUBSET_1, LANG1, TREES_1, TREES_2, TREES_3, TREES_4, FUNCT_1,
RELSET_1, FINSEQ_1, STRUCT_0, XREAL_0, NAT_1, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
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;
:: This definition really belongs elsewhere

definition
let X be set;
cluster -> Relation-like Function-like Element of X*;
:: for x being Element of X* holds x is Function-like
end;

definition
let X be set;
cluster -> FinSequence-like Element of X*;
end;

definition
let D be non empty set, t be Element of FinTrees D;
cluster dom t -> finite;
end;

definition
let D be non empty set, T be DTree-set of D;
cluster -> DTree-yielding 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 p be FinSequence such that
p is DTree-yielding;
func roots p -> FinSequence means
:: DTCONSTR:def 1
dom it = dom p & for i being Nat st i in dom p
ex T being DecoratedTree st T = p.i & it.i = T.{};
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 f be Function;
func pr1 f -> Function means
:: DTCONSTR:def 2
dom it = dom f & for x being set st x in dom f holds it.x = (f.x)`1;
func pr2 f -> Function means
:: DTCONSTR:def 3
dom it = dom f & for x being set st x in dom f holds it.x = (f.x)`2;
end;

definition
let X, Y be set, f be FinSequence of [:X, Y:];
redefine func pr1 f -> FinSequence of X;
func pr2 f -> FinSequence of Y;
end;

theorem :: DTCONSTR:7
pr1 {} = {} & pr2 {} = {};

scheme MonoSetSeq { f() -> Function, A() -> set, H(set, set) -> set}:
for k, s being Nat holds f().k c= f().(k+s)
provided
for n being Nat holds f().(n+1) = f().n \/ H(n, f().n);

begin

definition
let A be non empty set, R be Relation of A,A*;
cluster DTConstrStr(#A,R#) -> non empty;
end;

scheme DTConstrStrEx { S() -> non empty set,
P[set, set] }:
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 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 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 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 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 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 4

(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 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 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 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 5
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 6
Terminals G <> {};
attr G is with_nonterminals means
:: DTCONSTR:def 7
NonTerminals G <> {};
attr G is with_useful_nonterminals means
:: DTCONSTR:def 8
for nt being Symbol of G st nt in NonTerminals G
ex p being FinSequence of TS(G) st nt ==> roots p;
end;

definition
cluster with_terminals with_nonterminals with_useful_nonterminals strict
(non empty DTConstrStr);
end;

definition
let G be with_terminals (non empty DTConstrStr);
redefine func Terminals G -> non empty Subset of G;
cluster TS G -> non empty;
end;

definition
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 9

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 ::::::::::::::::::::::::::::::::::::::::::::::::

definition
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 such that
x <> {};
func plus-one x -> Nat means
:: DTCONSTR:def 10
ex n being Nat st it = n+1 & x.1 = n;
end;

definition
func PN-to-NAT -> Function of TS(PeanoNat), NAT means
:: DTCONSTR:def 11
(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 12
1-tree <*x*>;
end;

definition
func NAT-to-PN -> Function of NAT, TS(PeanoNat) means
:: DTCONSTR:def 13
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 D be set, F be FinSequence of D*;
func FlattenSeq F -> Element of D* means
:: DTCONSTR:def 14
ex g being BinOp of D* st
(for p, q being Element of D* holds g.(p,q) = p^q) &
it = g "**" F;
end;

theorem :: DTCONSTR:13
for D being set, d be Element of D* holds FlattenSeq <*d*> = d;

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 15
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 16
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 17
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 18
{ 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 19
{ 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 20
{ PostTraversal tsg
where tsg is Element of FinTrees the carrier of G :
tsg in TS G & tsg.{} = nt };
end;

theorem :: DTCONSTR:14
for t being DecoratedTree of the carrier of PeanoNat
st t in TS PeanoNat holds TerminalString t = <*0*>;

theorem :: DTCONSTR:15
for nt being Symbol of PeanoNat holds
TerminalLanguage nt = {<*0*>};

theorem :: DTCONSTR:16
for t being Element of TS PeanoNat
holds PreTraversal t = ((height dom t) |-> 1)^<*0*>;

theorem :: DTCONSTR:17
for nt being Symbol of PeanoNat holds
(nt = 0 implies PreTraversalLanguage nt = {<*0*>}) &
(nt = 1 implies PreTraversalLanguage nt = { (n|->1)^<*0*>
where n is Nat : n <> 0 });

theorem :: DTCONSTR:18
for t being Element of TS PeanoNat
holds PostTraversal t = <*0*>^((height dom t) |-> 1);

theorem :: DTCONSTR:19
for nt being Symbol of PeanoNat holds
(nt = 0 implies PostTraversalLanguage nt = {<*0*>}) &
(nt = 1 implies PostTraversalLanguage nt = { <*0*>^(n|->1)
where n is Nat : n <> 0 });

:: What remains to be done, but in another article:
::
:: - partial trees (grown from the root towards the leaves)
:: - phrases

```