:: Substitution in First-Order Formulas -- Part II. {T}he Construction of
:: First-Order Formulas
::  by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-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, SUBSET_1, CQC_LANG, QC_LANG1, SUBSTUT1, MCART_1,
      MARGREL1, REALSET1, FINSEQ_1, ORDINAL4, XBOOLEAN, CARD_1, ZFMISC_1,
      RELAT_1, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, ZF_LANG, FUNCT_4, FUNCOP_1,
      CLASSES2, SUBLEMMA, PARTFUN1, CQC_SIM1, ARYTM_3, XXREAL_0, ARYTM_1,
      SUBSTUT2, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, ORDINAL1, SUBSET_1, FINSEQ_1,
      FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, PARTFUN1, NUMBERS, XCMPLX_0,
      XXREAL_0, NAT_1, CQC_LANG, FUNCOP_1, RELAT_1, FUNCT_4, FUNCT_2, CQC_SIM1,
      DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA;
 constructors PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, INT_1, QC_LANG3, CQC_SIM1,
      SUBLEMMA, RELSET_1, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      XREAL_0, NAT_1, INT_1, QC_LANG1, CQC_LANG, SUBSTUT1, SUBLEMMA, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Further Properties of Substitution

reserve Al for QC-alphabet;
reserve a,b,b1 for object,
  i,j,k,n for Nat,
  p,q,r,s for Element of CQC-WFF(Al),
  x,y,y1 for bound_QC-variable of Al,
  P for QC-pred_symbol of k,Al,
  l,ll for CQC-variable_list of k,Al,
  Sub,Sub1 for CQC_Substitution of Al,
  S,S1,S2 for Element of CQC-Sub-WFF(Al),
  P1,P2 for Element of QC-pred_symbols(Al);

theorem :: SUBSTUT2:1
  for Sub holds ex S st S`1 = VERUM(Al) & S`2 = Sub;

theorem :: SUBSTUT2:2
  for Sub holds ex S st S`1 = P!ll & S`2 = Sub;

theorem :: SUBSTUT2:3
  for k,l being Nat st P is (QC-pred_symbol of k,Al) & P is (
  QC-pred_symbol of l,Al) holds k = l;

theorem :: SUBSTUT2:4
  (for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub holds
  ex S st S`1 = 'not' p & S`2 = Sub;

theorem :: SUBSTUT2:5
  (for Sub holds ex S st S`1 = p & S`2 = Sub) & (for Sub holds ex S
st S`1 = q & S`2 = Sub) implies for Sub holds ex S st S`1 = p '&' q & S`2 = Sub
;

definition
  let Al, p, Sub;
  redefine func [p,Sub] -> Element of [:QC-WFF(Al),vSUB(Al):];
end;

theorem :: SUBSTUT2:6
  dom RestrictSub(x,All(x,p),Sub) misses {x};

theorem :: SUBSTUT2:7
  x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p),
  Sub]) = x.upVar(RestrictSub(x,All(x,p),Sub),p);

theorem :: SUBSTUT2:8
  not x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p ),Sub]) = x
;

theorem :: SUBSTUT2:9
  ExpandSub(x,p,RestrictSub(x,All(x,p),Sub)) = @RestrictSub(x,All(x
  ,p),Sub) +* (x|S_Bound([All(x,p),Sub]));

theorem :: SUBSTUT2:10
  S`2 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub])
  ) & S`1 = p implies [S,x] is quantifiable & ex S1 st S1 = [All(x,p),Sub];

theorem :: SUBSTUT2:11
  (for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub
  holds ex S st S`1 = All(x,p) & S`2 = Sub;

theorem :: SUBSTUT2:12
  for p, Sub holds ex S st S`1 = p & S`2 = Sub;

definition
  let Al,p,Sub;
  redefine func [p,Sub] -> Element of CQC-Sub-WFF(Al);
end;

notation
  let Al,x,y;
  synonym Sbst(x,y) for x .--> y;
end;

definition
  let Al,x,y;
  redefine func Sbst(x,y) -> CQC_Substitution of Al;
end;

begin :: Facts about Substitution and Quantifiers of a Formula

definition
  let Al,p,x,y;
  func p.(x,y) -> Element of CQC-WFF(Al) equals
:: SUBSTUT2:def 1
  CQC_Sub([p,Sbst(x,y)]);
end;

scheme :: SUBSTUT2:sch 1
  CQCInd1 { Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) holds P[p]
provided
 for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p] and
 for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k
holds P[p] holds for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k+1
holds P[p];

scheme :: SUBSTUT2:sch 2
  CQCInd2 {Al() -> QC-alphabet, P[set]}:
   for p being Element of CQC-WFF(Al()) holds P[p]
provided
 for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= 0 holds P[p] and
 for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= k
holds P[p] holds for p being Element of CQC-WFF(Al())
st QuantNbr(p) <= k+1 holds P[p];

theorem :: SUBSTUT2:13
  VERUM(Al).(x,y) = VERUM(Al);

theorem :: SUBSTUT2:14
  (P!l).(x,y) = P!CQC_Subst(l,Sbst(x,y)) & QuantNbr(P!l) = QuantNbr((P!l
  ).(x,y));

theorem :: SUBSTUT2:15
  QuantNbr(P!l) = QuantNbr(CQC_Sub([P!l,Sub]));

definition
  let Al;
  let S be Element of QC-Sub-WFF(Al);
  redefine func S`2 -> CQC_Substitution of Al;
end;

theorem :: SUBSTUT2:16
  ['not' p,Sub] = Sub_not [p,Sub];

theorem :: SUBSTUT2:17
  'not' p.(x,y) = 'not' (p.(x,y)) & (QuantNbr(p) = QuantNbr(p.(x,y))
  implies QuantNbr('not' p) = QuantNbr('not' p.(x,y)));

theorem :: SUBSTUT2:18
  (for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
  for Sub holds QuantNbr('not' p) = QuantNbr(CQC_Sub(['not' p,Sub]));

theorem :: SUBSTUT2:19
  [p '&' q,Sub] = CQCSub_&([p,Sub],[q,Sub]);

theorem :: SUBSTUT2:20
  (p '&' q).(x,y) = (p.(x,y)) '&' (q.(x,y)) & ( QuantNbr(p) = QuantNbr(p
.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y)) implies QuantNbr(p '&'q) = QuantNbr((
  p '&' q).(x,y)));

theorem :: SUBSTUT2:21
  (for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) & (for
  Sub holds QuantNbr(q) = QuantNbr(CQC_Sub([q,Sub]))) implies for Sub holds
  QuantNbr(p '&' q) = QuantNbr(CQC_Sub[p '&' q,Sub]);

definition
  let Al;
  func CFQ(Al) -> Function of CQC-Sub-WFF(Al),vSUB(Al) equals
:: SUBSTUT2:def 2
  (QSub(Al))|CQC-Sub-WFF(Al);
end;

definition
  let Al,p,x,Sub;
  func QScope(p,x,Sub) -> CQC-WFF-like Element of [:QC-Sub-WFF(Al),
  bound_QC-variables(Al):] equals
:: SUBSTUT2:def 3
  [[p,(CFQ(Al)).[All(x,p),Sub]],x];
end;

definition
  let Al,p,x,Sub;
  func Qsc(p,x,Sub) -> second_Q_comp of QScope(p,x,Sub) equals
:: SUBSTUT2:def 4
  Sub;
end;

theorem :: SUBSTUT2:22
  [All(x,p),Sub] = CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) &
  QScope(p,x,Sub) is quantifiable;

theorem :: SUBSTUT2:23
  (for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
  for Sub holds QuantNbr(All(x,p)) = QuantNbr(CQC_Sub([All(x,p),Sub]));

theorem :: SUBSTUT2:24
  QuantNbr(VERUM(Al)) = QuantNbr(CQC_Sub([VERUM(Al),Sub]));

theorem :: SUBSTUT2:25
  for p, Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]));

theorem :: SUBSTUT2:26
  p is atomic implies ex k,P,ll st p = P!ll;

scheme :: SUBSTUT2:sch 3
  CQCInd3 {Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p]
provided
 for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k,Al()
for P being QC-pred_symbol of k,Al()
holds P[VERUM(Al())] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]);

begin :: Results about the Construction of Formulas

reserve F1,F2,F3 for QC-formula of Al,
  L for FinSequence;

definition
  let Al;
  let G,H be QC-formula of Al;
  assume
 G is_subformula_of H;
  mode PATH of G,H -> FinSequence means
:: SUBSTUT2:def 5

    1 <= len it & it.1 = G & it.(
len it) = H & for k st 1 <= k & k < len it ex G1,H1
being Element of QC-WFF(Al) st it.k = G1 & it.(k+1) = H1 &
G1 is_immediate_constituent_of H1;
end;

theorem :: SUBSTUT2:27
  for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <=
  len L holds ex F3 st F3 = L.i & F3 is_subformula_of F2;

theorem :: SUBSTUT2:28
  for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i
  <= len L holds L.i is Element of CQC-WFF(Al);

theorem :: SUBSTUT2:29
  for L being PATH of q,p st QuantNbr(p) <= n & q is_subformula_of
  p & 1 <= i & i <= len L holds ex r st r = L.i & QuantNbr(r) <= n;

theorem :: SUBSTUT2:30
  QuantNbr(p) = n & q is_subformula_of p implies QuantNbr(q) <= n;

theorem :: SUBSTUT2:31
  for n,p st (for q st q is_subformula_of p holds QuantNbr(q) = n) holds n = 0;

theorem :: SUBSTUT2:32
  for p st (for q st q is_subformula_of p holds for x,r holds q <> All(x
  ,r)) holds QuantNbr(p) = 0;

theorem :: SUBSTUT2:33
  for p st for q st q is_subformula_of p holds QuantNbr(q) <> 1
  holds QuantNbr(p) = 0;

theorem :: SUBSTUT2:34
  1 <= QuantNbr(p) implies ex q st q is_subformula_of p & QuantNbr(q)=1;