:: The Derivations of Temporal Logic Formulas
::  by Mariusz Giero
::
:: Received May 7, 2012
:: Copyright (c) 2012-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 FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI,
      RELAT_1, XBOOLE_0, FUNCT_1, XBOOLEAN, MODELC_2, CQC_THE1, NAT_1,
      XXREAL_0, ARYTM_1, PARTFUN1, MARGREL1, ZF_MODEL, RFINSEQ, FINSEQ_4,
      LTLAXIO1, LTLAXIO2, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, DOMAIN_1, NUMBERS, XCMPLX_0, NAT_1,
      XXREAL_0, TREES_1, TREES_2, TREES_4, TREES_9, XREAL_0, NAT_D, FUNCT_2,
      BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, AFINSQ_1, LEXBFS,
      RFINSEQ, RFINSEQ2, HILBERT1, STRUCT_0, XBOOLEAN, MARGREL1, AOFA_I00,
      LTLAXIO1, RLAFFIN3;
 constructors XXREAL_0, NAT_D, RELSET_1, AOFA_I00, HILBERT2, LTLAXIO1,
      FINSET_1, RFINSEQ, DOMAIN_1, AFINSQ_2, REAL_1, STRUCT_0, FUNCOP_1,
      XREAL_0, MATROID0, LEXBFS, MCART_1, CARD_1, RLAFFIN3, FINSEQ_4, FINSEQ_5,
      FINSEQ_2, RFINSEQ2, BINOP_2, ENUMSET1, SETFAM_1, TREES_9, TREES_2,
      TREES_4, AFINSQ_1;
 registrations ORDINAL1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1,
      XBOOLE_0, XREAL_0, HILBERT1, FINSEQ_1, LTLAXIO1, CARD_1;
 requirements NUMERALS, SUBSET, ARITHM, REAL;


begin :: Preliminaries

reserve A,B,p,q,r,s for Element of LTLB_WFF,
  i,j,k,n for Element of NAT,
  X for Subset of LTLB_WFF,
  f,f1 for FinSequence of LTLB_WFF,
  g for Function of LTLB_WFF,BOOLEAN;

registration let f be FinSequence, x be empty set;
  cluster f.x -> empty;
end;

theorem :: LTLAXIO2:1
  for f being FinSequence st len f > 0 & n > 0 holds len (f|n) > 0;

theorem :: LTLAXIO2:2
for f be FinSequence st len f = 0 holds f/^n = f;

theorem :: LTLAXIO2:3
  for f,g be FinSequence st rng f = rng g holds (len f = 0 iff len g = 0);

definition
  let A,B;
  func untn(A,B) -> Element of LTLB_WFF equals
:: LTLAXIO2:def 1
B 'or' (A '&&' (A 'U' B));
end;

theorem :: LTLAXIO2:4
(VAL g).TVERUM = 1;

theorem :: LTLAXIO2:5
(VAL g).(p 'or' q) = (VAL g).p 'or' (VAL g).q;

notation
  let p;
  synonym p is ctaut for p is LTL_TAUT_OF_PL;
end;

begin :: $n$-argument Connectives and Their Properties

definition
   let f;
   func con f -> FinSequence of LTLB_WFF means
:: LTLAXIO2:def 2
   len it = len f & it.1 = f.1 & for i being Nat st 1 <= i & i < len f holds
   it.(i+1) = it/.i '&&' f/.(i+1) if len f > 0 otherwise it = <*TVERUM*>;
end;

definition
   let f,A;
   func impg(f,A) -> FinSequence of LTLB_WFF means
:: LTLAXIO2:def 3
   len it = len f & it.1 = ('G' f/.1) => A & for i st
   1 <= i & i < len f holds it.(i+1) = ('G' f/.(i+1)) => it/.i if len f > 0
   otherwise it = <*> LTLB_WFF;
end;

definition
   let f;
   func nega f -> FinSequence of LTLB_WFF means
:: LTLAXIO2:def 4
   len it = len f & for i st 1 <= i & i <= len f holds it.i = 'not' f/.i;
 end;

definition
  let f;
  func nex f -> FinSequence of LTLB_WFF means
:: LTLAXIO2:def 5
  len it = len f & for i st 1 <= i & i <= len f holds it.i = 'X' f/.i;
end;

theorem :: LTLAXIO2:6
len f > 0 implies (con f)/.1 = f/.1;

theorem :: LTLAXIO2:7
  for i be Nat st 1 <= i & i < len f holds
  (con f)/.(i+1) = (con f)/.i '&&' f/.(i+1);

theorem :: LTLAXIO2:8
for i be Nat st i in dom f holds (nega f)/.i = 'not' (f/.i);

theorem :: LTLAXIO2:9
for i be Nat st i in dom f holds (nex f)/.i = 'X' (f/.i);

theorem :: LTLAXIO2:10
(con <*>LTLB_WFF)/.(len con <*>LTLB_WFF) = TVERUM;

theorem :: LTLAXIO2:11
(con <*A*>)/.(len con <*A*>) = A;

theorem :: LTLAXIO2:12
for k,n being Nat holds n <= k implies (con f).n = (con (f|k)).n;

theorem :: LTLAXIO2:13
  for k,n being Nat holds
  (n <= k & 1 <= n & n <= len f implies (con f)/.n = (con (f|k))/.n);

theorem :: LTLAXIO2:14
nega <*A*> = <*'not' A*>;

theorem :: LTLAXIO2:15
nega (f^<*A*>) = (nega f)^<*'not' A*>;

theorem :: LTLAXIO2:16
nega (f^f1) = (nega f)^(nega f1);

theorem :: LTLAXIO2:17
(VAL g).((con (f^f1))/.(len con (f^f1))) =
  (VAL g).((con f)/.(len con f)) '&' (VAL g).((con f1)/.(len con f1));

theorem :: LTLAXIO2:18
n in dom f implies (VAL g).((con f)/.len con f) =
  (VAL g).((con (f|(n -' 1)))/.(len con (f|(n -' 1)))) '&' (VAL g).(f/.n) '&'
  (VAL g).((con (f/^n))/.(len con (f/^n)));

theorem :: LTLAXIO2:19
(VAL g).((con f)/.(len con f)) = 1 iff
  for i be Nat st i in dom f holds (VAL g).(f/.i) = 1;

theorem :: LTLAXIO2:20
(VAL g).('not' ((con nega f)/.(len con nega f))) = 0 iff
  for i be Nat st i in dom f holds (VAL g).(f/.i) = 0;

theorem :: LTLAXIO2:21
rng f = rng f1 implies
   (VAL g).((con f)/.(len con f)) = (VAL g).((con f1)/.(len con f1));

begin :: Classical Tautologies of Temporal Language

theorem :: LTLAXIO2:22
p => TVERUM is ctaut;

theorem :: LTLAXIO2:23
'not' TVERUM => p is ctaut;

theorem :: LTLAXIO2:24
p => p is ctaut;

theorem :: LTLAXIO2:25
('not' 'not' p) => p is ctaut;

theorem :: LTLAXIO2:26
p => ('not' 'not' p) is ctaut;

theorem :: LTLAXIO2:27
(p '&&' q) => p is ctaut;

theorem :: LTLAXIO2:28
(p '&&' q) => q is ctaut;

theorem :: LTLAXIO2:29
for k be Nat st k in dom f holds
  f/.k => 'not' ((con nega f)/.(len con nega f)) is ctaut;

theorem :: LTLAXIO2:30
  rng f c= rng f1 implies ('not' ((con (nega f)) /. (len (con (nega f))))) =>
  ('not' ((con (nega f1)) /. (len (con (nega f1))))) is ctaut;

theorem :: LTLAXIO2:31
('not' (p => q)) => p is ctaut;

theorem :: LTLAXIO2:32
('not' (p => q)) => ('not' q) is ctaut;

theorem :: LTLAXIO2:33
p => (q => p) is ctaut;

theorem :: LTLAXIO2:34
p => (q => (p => q)) is ctaut;

theorem :: LTLAXIO2:35
'not' (p '&&' q) => (('not' p) 'or' ('not' q)) is ctaut;

theorem :: LTLAXIO2:36
'not' (p 'or' q) => (('not' p) '&&' ('not' q)) is ctaut;

theorem :: LTLAXIO2:37
'not' (p '&&' q) => (p => 'not' q)is ctaut;

theorem :: LTLAXIO2:38
('not' (TVERUM '&&' 'not' A)) => A is ctaut;

theorem :: LTLAXIO2:39
'not' (s '&&' q) => (p => q => (p => 'not' s)) is ctaut;

theorem :: LTLAXIO2:40
p => r => (p => s => (p => (r '&&' s))) is ctaut;

theorem :: LTLAXIO2:41
'not' (p '&&' s) => 'not' ((r '&&' s) '&&' (p '&&' q)) is ctaut;

theorem :: LTLAXIO2:42
'not' (p '&&' s) => 'not' ((p '&&' q) '&&' (r '&&' s)) is ctaut;

theorem :: LTLAXIO2:43
(p => (q '&&' ('not' q))) => ('not' p) is ctaut;

theorem :: LTLAXIO2:44
(q => (p '&&' r)) => ((p => s) => (q => (s '&&' r))) is ctaut;

theorem :: LTLAXIO2:45
(p => q) => ((r => s) => ((p '&&' r) => (q '&&' s))) is ctaut;

theorem :: LTLAXIO2:46
(p => q) => (p => r => (r => p => (r => q))) is ctaut;

theorem :: LTLAXIO2:47
p => q => (p => ('not' r) => (p => ('not' (q => r)))) is ctaut;

theorem :: LTLAXIO2:48
p => (q 'or' r) => (r => s => (p => (q 'or' s))) is ctaut;

theorem :: LTLAXIO2:49
p => r => (q => r => ((p 'or' q) => r)) is ctaut;

theorem :: LTLAXIO2:50
  r => untn(p,q) => (r => (('not' p) '&&' ('not' q)) => ('not' r)) is ctaut;

theorem :: LTLAXIO2:51
r => untn(p,q) => (r => (('not' q) '&&'
  ('not' (p 'U' q))) => ('not' r)) is ctaut;

begin :: The Derivations of Temporal Logic Formulas within Classical Logic

theorem :: LTLAXIO2:52
X |- p => q & X |- p => r implies X |- p => (q '&&' r);

theorem :: LTLAXIO2:53
X |- p => q & X |- r => s implies X |- (p '&&' r) => (q '&&' s);

theorem :: LTLAXIO2:54
X |- p => q & X |- p => r & X |- r => p implies X |- r => q;

theorem :: LTLAXIO2:55
X |- p => (q '&&' ('not' q)) implies X |- 'not' p;

theorem :: LTLAXIO2:56
(for i be Nat st i in dom f holds {}LTLB_WFF |- p => f/.i) implies
  {} LTLB_WFF |- p => (con f)/.(len con f);

theorem :: LTLAXIO2:57
(for i be Nat st i in dom f holds {}LTLB_WFF |- (f/.i) => p) implies
   {}LTLB_WFF |- ('not' (con nega f)/.(len con nega f)) => p;

begin :: The Derivations of Temporal Logic Formulas

theorem :: LTLAXIO2:58
X |- (('X' p) => ('X' q)) => ('X' (p => q));

theorem :: LTLAXIO2:59
X |- ('X' (p '&&' q)) => (('X' p) '&&' ('X' q));

theorem :: LTLAXIO2:60
{}LTLB_WFF |- (con nex f)/.(len con nex f)=>('X' (con f)/.(len con f));

theorem :: LTLAXIO2:61
X |- (('X' p) 'or' ('X' q)) => 'X' (p 'or' q);

theorem :: LTLAXIO2:62
X |- ('X' (p 'or' q)) => (('X' p) 'or' ('X' q));

theorem :: LTLAXIO2:63
X |- ('not' (A 'U' B)) => ('X' 'not' untn(A,B));