:: Defining by structural induction in the positive propositional language
:: by Andrzej Trybulec
::
:: Received April 23, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: HILBERT2:1
for Z being set
for M being ManySortedSet of Z st ( for x being set st x in Z holds
M . x is ManySortedSet of x ) holds
for f being Function st f = Union M holds
dom f = union Z
proof end;

theorem Th2: :: HILBERT2:2
for x, y being set
for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g
proof end;

theorem Th3: :: HILBERT2:3
for x, X being set st <*x*> is FinSequence of X holds
x in X
proof end;

theorem Th4: :: HILBERT2:4
for X being set
for f being FinSequence of X st f <> {} holds
ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>
proof end;

theorem Th5: :: HILBERT2:5
for x being set
for T1, T2 being Tree holds
( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )
proof end;

scheme :: HILBERT2:sch 1
InTreeInd{ F1() -> Tree, P1[ set ] } :
for f being Element of F1() holds P1[f]
provided
A1: P1[ <*> NAT] and
A2: for f being Element of F1() st P1[f] holds
for n being Element of NAT st f ^ <*n*> in F1() holds
P1[f ^ <*n*>]
proof end;

theorem Th6: :: HILBERT2:6
for x being set
for T1, T2 being DecoratedTree holds (x -tree (T1,T2)) . {} = x
proof end;

theorem Th7: :: HILBERT2:7
for x being set
for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) . <*0*> = T1 . {} & (x -tree (T1,T2)) . <*1*> = T2 . {} )
proof end;

theorem Th8: :: HILBERT2:8
for x being set
for T1, T2 being DecoratedTree holds
( (x -tree (T1,T2)) | <*0*> = T1 & (x -tree (T1,T2)) | <*1*> = T2 )
proof end;

registration
let x be set ;
let p be non empty DTree-yielding FinSequence;
cluster x -tree p -> non root ;
coherence
not x -tree p is trivial
proof end;
end;

registration
let x be set ;
let T1 be DecoratedTree;
cluster x -tree T1 -> non root ;
coherence
not x -tree T1 is trivial
proof end;
let T2 be DecoratedTree;
cluster x -tree (T1,T2) -> non root ;
coherence
not x -tree (T1,T2) is trivial
proof end;
end;

begin

definition
let n be Element of NAT ;
func prop n -> Element of HP-WFF equals :: HILBERT2:def 1
<*(3 + n)*>;
coherence
<*(3 + n)*> is Element of HP-WFF
by HILBERT1:def 4;
end;

:: deftheorem defines prop HILBERT2:def 1 :
for n being Element of NAT holds prop n = <*(3 + n)*>;

definition
let D be set ;
redefine attr D is with_VERUM means :Def2: :: HILBERT2:def 2
VERUM in D;
compatibility
( D is with_VERUM iff VERUM in D )
by HILBERT1:def 1;
redefine attr D is with_propositional_variables means :: HILBERT2:def 3
for n being Element of NAT holds prop n in D;
compatibility
( D is with_propositional_variables iff for n being Element of NAT holds prop n in D )
proof end;
end;

:: deftheorem Def2 defines with_VERUM HILBERT2:def 2 :
for D being set holds
( D is with_VERUM iff VERUM in D );

:: deftheorem defines with_propositional_variables HILBERT2:def 3 :
for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds prop n in D );

definition
let D be Subset of HP-WFF;
redefine attr D is with_implication means :: HILBERT2:def 4
for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D;
compatibility
( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D )
proof end;
redefine attr D is with_conjunction means :: HILBERT2:def 5
for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D;
compatibility
( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D )
proof end;
end;

:: deftheorem defines with_implication HILBERT2:def 4 :
for D being Subset of HP-WFF holds
( D is with_implication iff for p, q being Element of HP-WFF st p in D & q in D holds
p => q in D );

:: deftheorem defines with_conjunction HILBERT2:def 5 :
for D being Subset of HP-WFF holds
( D is with_conjunction iff for p, q being Element of HP-WFF st p in D & q in D holds
p '&' q in D );

definition
let p be Element of HP-WFF ;
attr p is conjunctive means :Def6: :: HILBERT2:def 6
ex r, s being Element of HP-WFF st p = r '&' s;
attr p is conditional means :Def7: :: HILBERT2:def 7
ex r, s being Element of HP-WFF st p = r => s;
attr p is simple means :Def8: :: HILBERT2:def 8
ex n being Element of NAT st p = prop n;
end;

:: deftheorem Def6 defines conjunctive HILBERT2:def 6 :
for p being Element of HP-WFF holds
( p is conjunctive iff ex r, s being Element of HP-WFF st p = r '&' s );

:: deftheorem Def7 defines conditional HILBERT2:def 7 :
for p being Element of HP-WFF holds
( p is conditional iff ex r, s being Element of HP-WFF st p = r => s );

:: deftheorem Def8 defines simple HILBERT2:def 8 :
for p being Element of HP-WFF holds
( p is simple iff ex n being Element of NAT st p = prop n );

scheme :: HILBERT2:sch 2
HPInd{ P1[ set ] } :
for r being Element of HP-WFF holds P1[r]
provided
A1: P1[ VERUM ] and
A2: for n being Element of NAT holds P1[ prop n] and
A3: for r, s being Element of HP-WFF st P1[r] & P1[s] holds
( P1[r '&' s] & P1[r => s] )
proof end;

theorem Th9: :: HILBERT2:9
for p being Element of HP-WFF holds
( p is conjunctive or p is conditional or p is simple or p = VERUM )
proof end;

theorem Th10: :: HILBERT2:10
for p being Element of HP-WFF holds len p >= 1
proof end;

theorem Th11: :: HILBERT2:11
for p being Element of HP-WFF st p . 1 = 1 holds
p is conditional
proof end;

theorem Th12: :: HILBERT2:12
for p being Element of HP-WFF st p . 1 = 2 holds
p is conjunctive
proof end;

theorem :: HILBERT2:13
for n being Element of NAT
for p being Element of HP-WFF st p . 1 = 3 + n holds
p is simple
proof end;

theorem :: HILBERT2:14
for p being Element of HP-WFF st p . 1 = 0 holds
p = VERUM
proof end;

theorem Th15: :: HILBERT2:15
for p, q being Element of HP-WFF holds
( len p < len (p '&' q) & len q < len (p '&' q) )
proof end;

theorem Th16: :: HILBERT2:16
for p, q being Element of HP-WFF holds
( len p < len (p => q) & len q < len (p => q) )
proof end;

theorem Th17: :: HILBERT2:17
for p, q being Element of HP-WFF
for t being FinSequence st p = q ^ t holds
p = q
proof end;

theorem Th18: :: HILBERT2:18
for p, q, r, s being Element of HP-WFF st p ^ q = r ^ s holds
( p = r & q = s )
proof end;

theorem Th19: :: HILBERT2:19
for p, q, r, s being Element of HP-WFF st p '&' q = r '&' s holds
( p = r & s = q )
proof end;

theorem Th20: :: HILBERT2:20
for p, q, r, s being Element of HP-WFF st p => q = r => s holds
( p = r & s = q )
proof end;

theorem Th21: :: HILBERT2:21
for n, m being Element of NAT st prop n = prop m holds
n = m
proof end;

theorem Th22: :: HILBERT2:22
for p, q, r, s being Element of HP-WFF holds p '&' q <> r => s
proof end;

theorem Th23: :: HILBERT2:23
for p, q being Element of HP-WFF holds p '&' q <> VERUM
proof end;

theorem Th24: :: HILBERT2:24
for n being Element of NAT
for p, q being Element of HP-WFF holds p '&' q <> prop n
proof end;

theorem Th25: :: HILBERT2:25
for p, q being Element of HP-WFF holds p => q <> VERUM
proof end;

theorem Th26: :: HILBERT2:26
for n being Element of NAT
for p, q being Element of HP-WFF holds p => q <> prop n
proof end;

theorem Th27: :: HILBERT2:27
for p, q being Element of HP-WFF holds
( p '&' q <> p & p '&' q <> q )
proof end;

theorem Th28: :: HILBERT2:28
for p, q being Element of HP-WFF holds
( p => q <> p & p => q <> q )
proof end;

theorem Th29: :: HILBERT2:29
for n being Element of NAT holds VERUM <> prop n
proof end;

begin

scheme :: HILBERT2:sch 3
HPMSSExL{ F1() -> set , F2( Element of NAT ) -> set , P1[ Element of HP-WFF , Element of HP-WFF , set , set , set ], P2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( P1[p,q,M . p,M . q,M . (p '&' q)] & P2[p,q,M . p,M . q,M . (p => q)] ) ) )
provided
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st P1[p,q,a,b,c] and
A2: for p, q being Element of HP-WFF
for a, b being set ex d being set st P2[p,q,a,b,d] and
A3: for p, q being Element of HP-WFF
for a, b, c, d being set st P1[p,q,a,b,c] & P1[p,q,a,b,d] holds
c = d and
A4: for p, q being Element of HP-WFF
for a, b, c, d being set st P2[p,q,a,b,c] & P2[p,q,a,b,d] holds
c = d
proof end;

scheme :: HILBERT2:sch 4
HPMSSLambda{ F1() -> set , F2( Element of NAT ) -> set , F3( set , set ) -> set , F4( set , set ) -> set } :
ex M being ManySortedSet of HP-WFF st
( M . VERUM = F1() & ( for n being Element of NAT holds M . (prop n) = F2(n) ) & ( for p, q being Element of HP-WFF holds
( M . (p '&' q) = F3((M . p),(M . q)) & M . (p => q) = F4((M . p),(M . q)) ) ) )
proof end;

begin

definition
func HP-Subformulae -> ManySortedSet of HP-WFF means :Def9: :: HILBERT2:def 9
( it . VERUM = root-tree VERUM & ( for n being Element of NAT holds it . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF 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) ) ) );
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) & b2 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b2 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = (p '&' q) -tree (p9,q9) & b2 . (p => q) = (p => q) -tree (p9,q9) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines HP-Subformulae HILBERT2:def 9 :
for b1 being ManySortedSet of HP-WFF holds
( b1 = HP-Subformulae iff ( b1 . VERUM = root-tree VERUM & ( for n being Element of NAT holds b1 . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = (p '&' q) -tree (p9,q9) & b1 . (p => q) = (p => q) -tree (p9,q9) ) ) ) );

definition
let p be Element of HP-WFF ;
func Subformulae p -> DecoratedTree of HP-WFF equals :: HILBERT2:def 10
HP-Subformulae . p;
correctness
coherence
HP-Subformulae . p is DecoratedTree of HP-WFF
;
proof end;
end;

:: deftheorem defines Subformulae HILBERT2:def 10 :
for p being Element of HP-WFF holds Subformulae p = HP-Subformulae . p;

theorem Th30: :: HILBERT2:30
Subformulae VERUM = root-tree VERUM by Def9;

theorem :: HILBERT2:31
for n being Element of NAT holds Subformulae (prop n) = root-tree (prop n) by Def9;

theorem Th32: :: HILBERT2:32
for p, q being Element of HP-WFF holds Subformulae (p '&' q) = (p '&' q) -tree ((Subformulae p),(Subformulae q))
proof end;

theorem Th33: :: HILBERT2:33
for p, q being Element of HP-WFF holds Subformulae (p => q) = (p => q) -tree ((Subformulae p),(Subformulae q))
proof end;

theorem Th34: :: HILBERT2:34
for p being Element of HP-WFF holds (Subformulae p) . {} = p
proof end;

theorem Th35: :: HILBERT2:35
for p being Element of HP-WFF
for f being Element of dom (Subformulae p) holds (Subformulae p) | f = Subformulae ((Subformulae p) . f)
proof end;

theorem :: HILBERT2:36
for p, q being Element of HP-WFF holds
( not p in Leaves (Subformulae q) or p = VERUM or p is simple )
proof end;