:: Propositional Linear Time Temporal Logic with Initial Semantics
:: by Mariusz Giero
::
:: Received October 22, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Lm1: :: LTLAXIO5:1
for X being set
for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
proof end;

::#INSERT: LTLB with normal semantics is monotonic
theorem mon2: :: LTLAXIO5:2
for A being Element of LTLB_WFF
for F, G being Subset of LTLB_WFF st F c= G & F |- A holds
G |- A
proof end;

theorem th16: :: LTLAXIO5:3
for A, B, C being Element of LTLB_WFF holds (A => B) => ((B => C) => (A => C)) is LTL_TAUT_OF_PL
proof end;

theorem th17: :: LTLAXIO5:4
for A, B, C being Element of LTLB_WFF holds (A => (B => C)) => ((A => B) => (A => C)) is LTL_TAUT_OF_PL
proof end;

theorem th18: :: LTLAXIO5:5
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' A) => A
proof end;

theorem th19a: :: LTLAXIO5:6
for A being Element of LTLB_WFF holds {A} |= 'G' ('X' A)
proof end;

theorem th19: :: LTLAXIO5:7
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' A) => ('G' ('X' A))
proof end;

theorem th20: :: LTLAXIO5:8
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B))))
proof end;

::#INSERT: A formula A is initially valid in the temporal structure M
definition
let M be LTLModel;
let A be Element of LTLB_WFF ;
::#INSERT: A formula A is initially valid in the temporal structure M
pred M |=0 A means :: LTLAXIO5:def 1
(SAT M) . [0,A] = 1;
end;

:: deftheorem defines |=0 LTLAXIO5:def 1 :
for M being LTLModel
for A being Element of LTLB_WFF holds
( M |=0 A iff (SAT M) . [0,A] = 1 );

::#INSERT: A set F of formulas is initially valid in the temporal structure M
definition
let M be LTLModel;
let F be Subset of LTLB_WFF;
::#INSERT: A set F of formulas is initially valid in the temporal structure M
pred M |=0 F means :: LTLAXIO5:def 2
for A being Element of LTLB_WFF st A in F holds
M |=0 A;
end;

:: deftheorem defines |=0 LTLAXIO5:def 2 :
for M being LTLModel
for F being Subset of LTLB_WFF holds
( M |=0 F iff for A being Element of LTLB_WFF st A in F holds
M |=0 A );

::#INSERT: A formula A is an initial consequence of a set F of formulas
definition
let F be Subset of LTLB_WFF;
let A be Element of LTLB_WFF ;
pred F |=0 A means :: LTLAXIO5:def 3
for M being LTLModel st M |=0 F holds
M |=0 A;
end;

:: deftheorem defines |=0 LTLAXIO5:def 3 :
for F being Subset of LTLB_WFF
for A being Element of LTLB_WFF holds
( F |=0 A iff for M being LTLModel st M |=0 F holds
M |=0 A );

::#INSERT: The numbers 2.6.1-2.6.8, put in comments in the article,
::#INSERT: correspond to the ones in: Kroeger, Merz. Temporal Logic and State
::#INSERT: Systems. 2008. Springer-Verlag.
::#INSERT: 2.6.1a-trivial: M |= A implies M |=0 A
theorem Th1: :: LTLAXIO5:9
for F being Subset of LTLB_WFF
for M being LTLModel st M |= F holds
M |=0 F
proof end;

::#INSERT: 2.6.1b
theorem th261b: :: LTLAXIO5:10
for A being Element of LTLB_WFF
for M being LTLModel holds
( M |= A iff M |=0 'G' A )
proof end;

::#INSERT: 2.6.2a
theorem th262a: :: LTLAXIO5:11
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 A holds
F |= A
proof end;

definition
let F be Subset of LTLB_WFF;
func 'G' F -> Subset of LTLB_WFF equals :: LTLAXIO5:def 4
{ ('G' A) where A is Element of LTLB_WFF : A in F } ;
correctness
coherence
{ ('G' A) where A is Element of LTLB_WFF : A in F } is Subset of LTLB_WFF
;
proof end;
end;

:: deftheorem defines 'G' LTLAXIO5:def 4 :
for F being Subset of LTLB_WFF holds 'G' F = { ('G' A) where A is Element of LTLB_WFF : A in F } ;

theorem th261bq: :: LTLAXIO5:12
for F being Subset of LTLB_WFF
for M being LTLModel holds
( M |= F iff M |=0 'G' F )
proof end;

::#INSERT: 2.6.2b
theorem th262b: :: LTLAXIO5:13
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F |= A iff 'G' F |=0 A )
proof end;

theorem th262ac1: :: LTLAXIO5:14
for n being Element of NAT holds
( {(prop n)} |= 'X' (prop n) & not {(prop n)} |=0 'X' (prop n) )
proof end;

::#INSERT: The converse of 2.6.2a does not hold in general
theorem :: LTLAXIO5:15
ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 A )
proof end;

theorem th21: :: LTLAXIO5:16
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A holds
F |= A
proof end;

theorem th21cp: :: LTLAXIO5:17
for i being Element of NAT holds
( {(prop i)} |= prop i & not {(prop i)} |=0 'G' (prop i) )
proof end;

theorem :: LTLAXIO5:18
ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 'G' A )
proof end;

theorem th263pa: :: LTLAXIO5:19
for F, G being Subset of LTLB_WFF
for M being LTLModel holds
( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )
proof end;

theorem th263pb: :: LTLAXIO5:20
for A being Element of LTLB_WFF
for M being LTLModel holds
( M |=0 A iff M |=0 {A} )
proof end;

::#INSERT: 2.6.3
::#INSERT: In compare to normal consequence (LTLAXIO1:30), the relationship
::#INSERT: between implication and initial consequence holds in the classical
::#INSERT: form
theorem th263: :: LTLAXIO5:21
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F \/ {A} |=0 B iff F |=0 A => B )
proof end;

theorem th264p: :: LTLAXIO5:22
proof end;

::#INSERT: Universal validity concepts are equaivalent as far as
::#INSERT: initial and normal semantics is concerned:
::#INSERT: 2.6.4: one line proof:
::#INSERT: {}LTLB_WFF |= A iff {}LTLB_WFF |=0 A by th262b,th264p
::#INSERT: 2.1.8
theorem th218: :: LTLAXIO5:23
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |= B ) holds
{} LTLB_WFF |= A
proof end;

::#INSERT: 2.6.5
theorem th265: :: LTLAXIO5:24
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |=0 B ) holds
{} LTLB_WFF |=0 A
proof end;

theorem :: LTLAXIO5:25
for A being Element of LTLB_WFF st {} LTLB_WFF |=0 A holds
{} LTLB_WFF |=0 'X' A
proof end;

::#INSERT: Axioms
definition
correctness
coherence ;
;
end;

:: deftheorem defines LTL0_axioms LTLAXIO5:def 5 :

::#INSERT: Derivation rules
definition
let p, q be Element of LTLB_WFF ;
pred p REFL0_rule q means :: LTLAXIO5:def 6
p = 'G' q;
pred p NEX0_rule q means :: LTLAXIO5:def 7
ex A being Element of LTLB_WFF st
( p = 'G' A & q = 'G' ('X' A) );
let r be Element of LTLB_WFF ;
pred p,q MP0_rule r means :: LTLAXIO5:def 8
ex A, B being Element of LTLB_WFF st
( p = 'G' A & q = 'G' (A => B) & r = 'G' B );
pred p,q IND0_rule r means :: LTLAXIO5:def 9
ex A, B being Element of LTLB_WFF st
( p = 'G' (A => B) & q = 'G' (A => ('X' A)) & r = 'G' (A => ('G' B)) );
end;

:: deftheorem defines REFL0_rule LTLAXIO5:def 6 :
for p, q being Element of LTLB_WFF holds
( p REFL0_rule q iff p = 'G' q );

:: deftheorem defines NEX0_rule LTLAXIO5:def 7 :
for p, q being Element of LTLB_WFF holds
( p NEX0_rule q iff ex A being Element of LTLB_WFF st
( p = 'G' A & q = 'G' ('X' A) ) );

:: deftheorem defines MP0_rule LTLAXIO5:def 8 :
for p, q, r being Element of LTLB_WFF holds
( p,q MP0_rule r iff ex A, B being Element of LTLB_WFF st
( p = 'G' A & q = 'G' (A => B) & r = 'G' B ) );

:: deftheorem defines IND0_rule LTLAXIO5:def 9 :
for p, q, r being Element of LTLB_WFF holds
( p,q IND0_rule r iff ex A, B being Element of LTLB_WFF st
( p = 'G' (A => B) & q = 'G' (A => ('X' A)) & r = 'G' (A => ('G' B)) ) );

::#INSERT: Definition of derivation step
definition
let i be Nat;
let f be FinSequence of LTLB_WFF ;
let X be Subset of LTLB_WFF;
::#INSERT: Definition of derivation step
pred prc0 f,X,i means :Def29: :: LTLAXIO5:def 10
( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) );
end;

:: deftheorem Def29 defines prc0 LTLAXIO5:def 10 :
for i being Nat
for f being FinSequence of LTLB_WFF
for X being Subset of LTLB_WFF holds
( prc0 f,X,i iff ( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) );

::#INSERT: Properties of derivation step prc0 - analogue of "prc" from LTLAXIO1
theorem Th38: :: LTLAXIO5:26
for X being Subset of LTLB_WFF
for f, f2 being FinSequence of LTLB_WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds
prc0 f2,X,i + n
proof end;

theorem Th39: :: LTLAXIO5:27
for X being Subset of LTLB_WFF
for f, f1, f2 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc0 f2,X,i
proof end;

:: Derivability
definition
let X be Subset of LTLB_WFF;
let p be Element of LTLB_WFF ;
pred X |-0 p means :: LTLAXIO5:def 11
ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) );
end;

:: deftheorem defines |-0 LTLAXIO5:def 11 :
for X being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( X |-0 p iff ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) ) );

:: Properties of derivation sequences
theorem Th40: :: LTLAXIO5:28
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF
for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) & prc0 f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p )
proof end;

::#INSERT: Axioms are sound
theorem Th2: :: LTLAXIO5:29
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL0_axioms holds
F |=0 A
proof end;

::#INSERT: MP_rule is sound
theorem Th3: :: LTLAXIO5:30
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 A & F |=0 A => B holds
F |=0 B
proof end;

::#INSERT: MP0_rule is sound
theorem Th4: :: LTLAXIO5:31
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A & F |=0 'G' (A => B) holds
F |=0 'G' B
proof end;

::#INSERT: NEX0_rule is sound
theorem Th5: :: LTLAXIO5:32
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A holds
F |=0 'G' ('X' A)
proof end;

::#INSERT: REFL0_rule is sound
theorem Th6: :: LTLAXIO5:33
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A holds
F |=0 A
proof end;

::#INSERT: IND0_rule is sound
theorem Th7: :: LTLAXIO5:34
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' (A => B) & F |=0 'G' (A => ('X' A)) holds
F |=0 'G' (A => ('G' B))
proof end;

::#INSERT: 2.6.6
:: Soundness Theorem for LTLB with initial semantics.
theorem th266: :: LTLAXIO5:35
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 A holds
F |=0 A
proof end;

::#INSERT: Axioms and premises are derivable
theorem th10: :: LTLAXIO5:36
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st ( A in LTL0_axioms or A in F ) holds
F |-0 A
proof end;

::#INSERT: REFL0_rule is derivable
theorem th9: :: LTLAXIO5:37
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' A holds
F |-0 A
proof end;

::#INSERT: NEX0_rule is derivable
theorem th12: :: LTLAXIO5:38
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' A holds
F |-0 'G' ('X' A)
proof end;

::#INSERT: MP_rule is derivable
theorem th11a: :: LTLAXIO5:39
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 A & F |-0 A => B holds
F |-0 B
proof end;

::#INSERT: MP0_rule is derivable
theorem th11: :: LTLAXIO5:40
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' A & F |-0 'G' (A => B) holds
F |-0 'G' B
proof end;

::#INSERT: IND0_rule is derivable
theorem th13: :: LTLAXIO5:41
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' (A => B) & F |-0 'G' (A => ('X' A)) holds
F |-0 'G' (A => ('G' B))
proof end;

theorem th15: :: LTLAXIO5:42
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL_axioms holds
F |-0 A
proof end;

theorem :: LTLAXIO5:43
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL0_axioms holds
F |- A
proof end;

::#INSERT: 2.6.7
::#INSERT: auxilliary theorem to prove completeness theorem
theorem th267: :: LTLAXIO5:44
for A being Element of LTLB_WFF st {} LTLB_WFF |- A holds
{} LTLB_WFF |-0 A
proof end;

::#INSERT: Generalized theorem 2.6.7 does not hold, i.e.,
::#INSERT: not for F,A holds (F |- A implies F |-0 A);
theorem th14: :: LTLAXIO5:45
for i being Element of NAT holds
( {(prop i)} |- 'X' (prop i) & not {(prop i)} |-0 'X' (prop i) )
proof end;

::#INSERT: LTLB with initial semantics is monotonic
theorem mon: :: LTLAXIO5:46
for A being Element of LTLB_WFF
for F, G being Subset of LTLB_WFF st F c= G & F |-0 A holds
G |-0 A
proof end;

definition
let f be FinSequence of LTLB_WFF ;
let A be Element of LTLB_WFF ;
func implications (f,A) -> FinSequence of LTLB_WFF means :imps: :: LTLAXIO5:def 12
( len it = len f & it . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
it . (i + 1) = (f /. (i + 1)) => (it /. i) ) ) if len f > 0
otherwise it = <*> LTLB_WFF;
existence
( ( len f > 0 implies ex b1 being FinSequence of LTLB_WFF st
( len b1 = len f & b1 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b1 . (i + 1) = (f /. (i + 1)) => (b1 /. i) ) ) ) & ( not len f > 0 implies ex b1 being FinSequence of LTLB_WFF st b1 = <*> LTLB_WFF ) )
proof end;
uniqueness
for b1, b2 being FinSequence of LTLB_WFF holds
( ( len f > 0 & len b1 = len f & b1 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b1 . (i + 1) = (f /. (i + 1)) => (b1 /. i) ) & len b2 = len f & b2 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b2 . (i + 1) = (f /. (i + 1)) => (b2 /. i) ) implies b1 = b2 ) & ( not len f > 0 & b1 = <*> LTLB_WFF & b2 = <*> LTLB_WFF implies b1 = b2 ) )
proof end;
consistency
for b1 being FinSequence of LTLB_WFF holds verum
;
end;

:: deftheorem imps defines implications LTLAXIO5:def 12 :
for f being FinSequence of LTLB_WFF
for A being Element of LTLB_WFF
for b3 being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b3 = implications (f,A) iff ( len b3 = len f & b3 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b3 . (i + 1) = (f /. (i + 1)) => (b3 /. i) ) ) ) ) & ( not len f > 0 implies ( b3 = implications (f,A) iff b3 = <*> LTLB_WFF ) ) );

::#INSERT: 2.6.8
:: Weak Completeness Theorem for LTLB with initial semantics
theorem th268: :: LTLAXIO5:47
for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF st F |=0 A holds
F |-0 A
proof end;

::#INSERT: Deduction theorem holds in the classical form compared with
::#INSERT: Deduction theorem for LTLB with normal semantics (see LTLAXIO1:57)
theorem :: LTLAXIO5:48
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F \/ {A} |-0 B holds
F |-0 A => B
proof end;

:: Converse of Deduction Theorem
theorem :: LTLAXIO5:49
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 A => B holds
F \/ {A} |-0 B
proof end;

registration
let F be finite Subset of LTLB_WFF;
cluster 'G' F -> finite ;
coherence
'G' F is finite
proof end;
end;

theorem :: LTLAXIO5:50
for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF holds
( F |- A iff 'G' F |-0 A )
proof end;

theorem :: LTLAXIO5:51
for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF st F |-0 A holds
F |- A
proof end;

::#INSERT: The counterexample that "for F,A holds (F |- A implies F |-0 A)"
::#INSERT: is not true. Another counterexample see above for theorem "th14".
theorem :: LTLAXIO5:52
for i being Element of NAT holds
( {(prop i)} |- 'G' (prop i) & not {(prop i)} |-0 'G' (prop i) )
proof end;

theorem :: LTLAXIO5:53
for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF st F |-0 'G' A holds
F |- A
proof end;

::#INSERT: The converse of the above theorem does not hold
theorem :: LTLAXIO5:54
for i being Element of NAT holds
( {(prop i)} |- prop i & not {(prop i)} |-0 'G' (prop i) )
proof end;