:: Defining by structural induction in the positive propositional language
:: by Andrzej Trybulec
::
:: Received April 23, 1999
:: Copyright (c) 1999-2019 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, PBOOLE, FUNCT_1, CARD_3, RELAT_1, TARSKI, FINSEQ_1,
ORDINAL4, XBOOLE_0, SUBSET_1, HILBERT1, TREES_1, TREES_A, CARD_1,
ARYTM_3, TREES_2, TREES_4, TREES_3, TREES_9, FUNCT_6, QC_LANG1, XBOOLEAN,
ZF_LANG, GLIB_000, XXREAL_0, NAT_1, ORDINAL1, ZFMISC_1, PARTFUN1,
FUNCT_4, FUNCOP_1, HILBERT2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_3,
RELAT_1, FUNCT_1, PARTFUN1, XCMPLX_0, NAT_1, FINSEQ_1, FUNCOP_1, FUNCT_4,
FUNCT_6, PBOOLE, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9, HILBERT1,
XXREAL_0;
constructors FUNCT_4, XREAL_0, NAT_1, CARD_3, TREES_4, HILBERT1, RELSET_1,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
XREAL_0, NAT_1, FINSEQ_1, TREES_2, TREES_3, HILBERT1, TREES_4;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve X,x for set;
theorem :: HILBERT2:1
for Z being set, M being ManySortedSet of Z st for x being set st
x in Z holds M.x is ManySortedSet of x for f being Function st f = Union M
holds dom f = union Z;
theorem :: HILBERT2:2
for x,y being set, f,g being FinSequence st <*x*>^f = <*y*>^g holds f = g;
theorem :: HILBERT2:3
for x being object holds <*x*> is FinSequence of X implies x in X;
theorem :: HILBERT2:4
for X for f being FinSequence of X st f <> {} ex g being
FinSequence of X, d being Element of X st f = g^<*d*>;
reserve k,m,n for Element of NAT,
p,q,r,s,r9,s9 for Element of HP-WFF,
T1,T2 for Tree;
theorem :: HILBERT2:5
<*x*> in tree(T1,T2) iff x=0 or x=1;
scheme :: HILBERT2:sch 1
InTreeInd{T() -> Tree, P[set] }: for f being Element of T() holds P[f]
provided
P[<*>NAT] and
for f being Element of T() st P[f] for n st f^<*n*> in T() holds P[f
^<*n*>];
reserve T1,T2 for DecoratedTree;
theorem :: HILBERT2:6
for x being set, T1, T2 holds (x-tree (T1,T2)).{} = x;
theorem :: HILBERT2:7
x-tree(T1,T2).<*0*> = T1.{} & x-tree(T1,T2).<*1*> = T2.{};
theorem :: HILBERT2:8
x-tree(T1,T2)|<*0*> = T1 & x-tree(T1,T2)|<*1*> = T2;
registration
let x;
let p be DTree-yielding non empty FinSequence;
cluster x-tree p -> non root;
end;
registration
let x;
let T1 be DecoratedTree;
cluster x-tree T1 -> non root;
let T2 be DecoratedTree;
cluster x-tree (T1,T2) -> non root;
end;
begin :: About the language
definition
let n;
func prop n -> Element of HP-WFF equals
:: HILBERT2:def 1
<*3+n*>;
end;
definition
let D be set;
redefine attr D is with_VERUM means
:: HILBERT2:def 2
VERUM in D;
redefine attr D is with_propositional_variables means
:: HILBERT2:def 3
for n holds prop n in D;
end;
definition
let D be Subset of HP-WFF;
redefine attr D is with_implication means
:: HILBERT2:def 4
for p, q st p in D & q in D holds p => q in D;
redefine attr D is with_conjunction means
:: HILBERT2:def 5
for p, q st p in D & q in D holds p '&' q in D;
end;
reserve t,t1 for FinSequence;
definition
let p;
attr p is conjunctive means
:: HILBERT2:def 6
ex r,s st p = r '&' s;
attr p is conditional means
:: HILBERT2:def 7
ex r,s st p = r => s;
attr p is simple means
:: HILBERT2:def 8
ex n st p = prop n;
end;
scheme :: HILBERT2:sch 2
HPInd { P[set] }: for r holds P[r]
provided
P[VERUM] and
for n holds P[prop n] and
for r,s st P[r] & P[s] holds P[r '&' s] & P[r => s];
theorem :: HILBERT2:9
p is conjunctive or p is conditional or p is simple or p = VERUM;
theorem :: HILBERT2:10
len p >= 1;
theorem :: HILBERT2:11
p.1 = 1 implies p is conditional;
theorem :: HILBERT2:12
p.1 = 2 implies p is conjunctive;
theorem :: HILBERT2:13
p.1 = 3+n implies p is simple;
theorem :: HILBERT2:14
p.1 = 0 implies p = VERUM;
theorem :: HILBERT2:15
len p < len(p '&' q) & len q < len(p '&' q);
theorem :: HILBERT2:16
len p < len(p => q) & len q < len(p => q);
theorem :: HILBERT2:17
p = q^t implies p = q;
theorem :: HILBERT2:18
p^q = r^s implies p = r & q = s;
theorem :: HILBERT2:19
p '&' q = r '&' s implies p = r & s = q;
theorem :: HILBERT2:20
p => q = r => s implies p = r & s = q;
theorem :: HILBERT2:21
prop n = prop m implies n = m;
theorem :: HILBERT2:22
p '&' q <> r => s;
theorem :: HILBERT2:23
p '&' q <> VERUM;
theorem :: HILBERT2:24
p '&' q <> prop n;
theorem :: HILBERT2:25
p => q <> VERUM;
theorem :: HILBERT2:26
p => q <> prop n;
theorem :: HILBERT2:27
p '&' q <> p & p '&' q <> q;
theorem :: HILBERT2:28
p => q <> p & p => q <> q;
theorem :: HILBERT2:29
VERUM <> prop n;
begin :: Defining by structural induction
scheme :: HILBERT2:sch 3
HPMSSExL{V()->set,P(Element of NAT)->set, C,I[Element of HP-WFF,Element of
HP-WFF,set,set,set]}: ex M being ManySortedSet of HP-WFF st M.VERUM = V() & (
for n holds M.prop n = P(n)) & for p,q holds C[p,q,M.p,M.q,M.(p '&' q)] & I[p,q
,M.p,M.q,M.(p => q)]
provided
for p,q for a,b being set ex c being set st C[p,q,a,b,c] and
for p,q for a,b being set ex d being set st I[p,q,a,b,d] and
for p,q for a,b,c,d being set st C[p,q,a,b,c] & C[p,q,a,b,d] holds c
= d and
for p,q for a,b,c,d being set st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d;
scheme :: HILBERT2:sch 4
HPMSSLambda{V()->set,P(Element of NAT)->set,C,I(set,set)->set}: ex M being
ManySortedSet of HP-WFF st M.VERUM = V() & (for n holds M.prop n = P(n)) & for
p,q holds M.(p '&' q) = C(M.p,M.q) & M.(p => q) = I(M.p,M.q);
begin :: The tree of the subformulae
definition
func HP-Subformulae -> ManySortedSet of HP-WFF means
:: HILBERT2:def 9
it.VERUM =
root-tree VERUM & (for n holds it.prop n = root-tree prop n) & for p,q ex p9,q9
being DecoratedTree of HP-WFF st p9 = it.p & q9 = it.q & it.(p '&' q) = (p '&'
q)-tree(p9,q9) & it.(p => q) = (p => q)-tree(p9,q9);
end;
definition
let p;
func Subformulae p -> DecoratedTree of HP-WFF equals
:: HILBERT2:def 10
HP-Subformulae.p;
end;
theorem :: HILBERT2:30
Subformulae VERUM = root-tree VERUM;
theorem :: HILBERT2:31
Subformulae prop n = root-tree prop n;
theorem :: HILBERT2:32
Subformulae(p '&' q) = (p '&' q)-tree(Subformulae p,Subformulae q);
theorem :: HILBERT2:33
Subformulae(p => q) = (p => q)-tree(Subformulae p,Subformulae q);
theorem :: HILBERT2:34
(Subformulae p).{} = p;
theorem :: HILBERT2:35
for f being Element of dom Subformulae p holds (Subformulae p)|f
= Subformulae((Subformulae p).f);
theorem :: HILBERT2:36
p in Leaves Subformulae q implies p = VERUM or p is simple;