:: Defining by structural induction in the positive propositional language
::  by Andrzej Trybulec
::
:: Received April 23, 1999
:: Copyright (c) 1999-2021 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;