# Theory TL

Up to index of Isabelle/HOLCF/IOA

theory TL
imports Pred Sequence
uses [TL.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
        ID:         $Id: TL.thy,v 1.10 2005/09/02 15:24:03 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* A General Temporal Logic *}

    theory TL
    imports Pred Sequence
    begin

    defaultsort type

    types
      'a temporal = "'a Seq predicate"

    consts
    suffix     :: "'a Seq => 'a Seq => bool"
    tsuffix    :: "'a Seq => 'a Seq => bool"

    validT     :: "'a Seq predicate => bool"

    unlift     ::  "'a lift => 'a"

    Init         ::"'a predicate => 'a temporal"          ("<_>" [0] 1000)

    Box          ::"'a temporal => 'a temporal"   ("[] (_)" [80] 80)
    Diamond      ::"'a temporal => 'a temporal"   ("<> (_)" [80] 80)
    Next         ::"'a temporal => 'a temporal"
    Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)

    syntax (xsymbols)
       "Box"        ::"'a temporal => 'a temporal"   ("\<box> (_)" [80] 80)
       "Diamond"    ::"'a temporal => 'a temporal"   ("\<diamond> (_)" [80] 80)
       "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\<leadsto>" 22)

    defs

    unlift_def:
      "unlift x == (case x of
                     UU   => arbitrary
                   | Def y   => y)"

    (* this means that for nil and UU the effect is unpredictable *)
    Init_def:
      "Init P s ==  (P (unlift (HD$s)))"

    suffix_def:
      "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)"

    tsuffix_def:
      "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"

    Box_def:
      "([] P) s == ! s2. tsuffix s2 s --> P s2"

    Next_def:
      "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"

    Diamond_def:
      "<> P == .~ ([] (.~ P))"

    Leadsto_def:
       "P ~> Q == ([] (P .--> (<> Q)))"

    validT_def:
      "validT P == ! s. s~=UU & s~=nil --> (s |= P)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem simple:

      [] <> (¬ P) = (¬ <> [] P)

theorem Boxnil:

      nil |= [] P

theorem Diamondnil:

      ¬ (nil |= <> P)

theorem Diamond_def2:

      (<> F) s = (∃s2. tsuffix s2 s ∧ F s2)

## TLA Axiomatization by Merz

theorem suffix_refl:

      suffix s s

theorem reflT:

      s ≠ UU ∧ s ≠ nil --> (s |= [] F --> F)

theorem suffix_trans:

      [| suffix y x; suffix z y |] ==> suffix z x

theorem transT:

      s |= [] F --> [] [] F

theorem normalT:

      s |= [] (F --> G) --> [] F --> [] G

## TLA Rules by Lamport

theorem STL1a:

      validT P ==> validT ([] P)

theorem STL1b:

      valid P ==> validT <P>

theorem STL1:

      valid P ==> validT ([] <P>)

theorem STL4:

      valid (P --> Q) ==> validT ([] <P> --> [] <Q>)

## LTL Axioms by Manna/Pnueli

theorem tsuffix_TL:

      [| s ≠ UU ∧ s ≠ nil; tsuffix s2.0 (TL·s) |] ==> tsuffix s2.0 s

theorem LTL1:

      s ≠ UU ∧ s ≠ nil --> (s |= [] F --> F ∧ Next ([] F))

theorem LTL2a:

      s |= ¬ Next F --> Next (¬ F)

theorem LTL2b:

      s |= Next (¬ F) --> ¬ Next F

theorem LTL3:

      ex |= Next (F --> G) --> Next F --> Next G

theorem ModusPonens:

      [| validT (P --> Q); validT P |] ==> validT Q