Theory Temporal

theory Temporal
imports Distributive
section{*\label{sec_Temporal}Linear Temporal Logic*}

theory Temporal imports Distributive
begin
  text{*
    In this section we introduce an algebraic axiomatization of Linear Temporal Logic (LTL).
    We model LTL formulas semantically as predicates on traces. For example the LTL formula
    $\alpha = \Box\; \diamondsuit\; (x = 1)$ is modeled as a predicate 
    $\alpha : (nat \Rightarrow nat) \Rightarrow bool$, where 
    $\alpha \;x = True$ if $x\;i=1$ for infinitely many $i:nat$. In this formula $\Box$
    and $\diamondsuit$ denote the always and eventually operators, respectively. 
    Formulas with multiple variables are modeled similarly. For example a formula $\alpha$ in two 
    variables is modeled as $\alpha : (nat \Rightarrow \tv a) \Rightarrow (nat \Rightarrow \tv b) \Rightarrow bool$,
    and for example $(\Box\; \alpha) \; x\; y$ is defined as $(\forall i . \alpha \; x[i..]\; y[i..])$,
    where $x[i..]\;j = x\;(i+j)$. We would like to construct an algebraic structure (Isabelle class) 
    which has the temporal operators as operations, and which has instatiations to 
    $(nat \Rightarrow \tv a) \Rightarrow bool$, $(nat \Rightarrow \tv a) \Rightarrow (nat \Rightarrow \tv b) \Rightarrow bool$,
    and so on. Ideally our structure should be such that if we have this structure on a type $\tv a::temporal$,
    then we could extend it to $(nat \Rightarrow \tv b) \Rightarrow \tv a$ in a way similar to the
    way Boolean algebras are extended from a type $\tv a::boolean\_algebra$ to $\tv b\Rightarrow \tv a$.
    Unfortunately, if we use for example $\Box$ as primitive operation on our temporal structure,
    then we cannot extend $\Box$ from $\tv a::temporal$ to $(nat \Rightarrow \tv b) \Rightarrow \tv a$. A
    possible extension of $\Box$ could be
      $$(\Box\; \alpha)\;x = \bigwedge_{i:nat} \Box (\alpha\; x[i..]) \mbox{ and } \Box \; b = b$$
    where $\alpha: (nat \Rightarrow \tv b) \Rightarrow \tv a$ and $b:bool$. However, if we apply this
    definition to $\alpha : (nat \Rightarrow \tv a) \Rightarrow (nat \Rightarrow \tv b) \Rightarrow bool$,
    then we get
      $$(\Box\; \alpha) \; x\; y = (\forall i\;j. \alpha \; x[i..]\; y[j..])$$
    which is not correct.

    To overcome this problem we introduce as a primitive operation $!!:\tv a \Rightarrow nat \Rightarrow \tv a$,
    where $\tv a$ is the type of temporal formulas, and $\alpha !! i$ is the formula $\alpha$ at time point $i$.
    If $\alpha$ is a formula in two variables as before, then
      $$(\alpha !! i)\; x\;y = \alpha\; x[i..]\;y[i..].$$
    and we define for example the the operator always by
      $$\Box \alpha = \bigwedge_{i:nat} \alpha !! i$$
  *}
    (*
  notation
    bot ("⊥") and
    top ("⊤") and
    inf (infixl "⊓" 70)
    and sup (infixl "⊔" 65)
*)

  class temporal = complete_boolean_algebra + complete_distributive_lattice +
    fixes at :: "'a ⇒ nat ⇒ 'a" (infixl "!!" 150)
    assumes [simp]: "a !! i !! j = a !! (i + j)"
    assumes [simp]: "a !! 0 = a"
    assumes [simp]: "-(a !! i) = (-a) !! i"
    assumes Inf_at[simp]: "(Inf X) !! i = (INFIMUM X (λ x . at x i))"
    begin
      lemma [simp]: "⊤ !! i = ⊤"
        apply (cut_tac X = "{}" in Inf_at)
        by auto
          
lemma Sup_at: "(Sup X) !! i = (SUPREMUM X (λ x . x !! i))"
  by (subst compl_eq_compl_iff [THEN sym], simp add: uminus_Sup)

      lemma [simp]: "(a ⊓ b) !! i = (a !! i) ⊓ (b !! i)"
        apply (cut_tac X = "{a,b}" in Inf_at)
        by auto

      lemma [simp]: "(INF x:X. f x) !! i = (INF x:X. f x !! i)"
        apply (unfold Inf_at)
        by simp

      definition always :: "'a ⇒ 'a"  ("□ (_)" [900] 900) where
        "□ p = (INF i . p !! i)"

      definition eventually_bounded :: "nat set ⇒ 'a ⇒ 'a"  ("♢b (_) (_)" [900,900] 900) where
         "♢b b p = (SUP i: b . p !! i)"

      definition always_bounded :: "nat set ⇒ 'a ⇒ 'a"  ("□b (_) (_)" [900,900] 900) where
         "□b b p = (INF i: b . p !! i)"

      lemma "(□b b p) ⊓ (□b b' p) = (□b (b ∪ b') p)"
        apply (simp add: always_bounded_def)
        apply (rule antisym, simp_all, auto)
        apply (rule_tac INF_greatest, safe)
        apply (rule_tac y = "(INF i:b. p !! i)" in order_trans, simp_all)
        apply (rule INF_lower, simp)
        apply (rule_tac y = "(INF i:b'. p !! i)" in order_trans, simp_all)
        apply (rule INF_lower, simp)
        apply (rule_tac INF_greatest)
        apply (rule INF_lower, simp)
        apply (rule_tac INF_greatest)
        by (rule INF_lower, simp)

      definition eventually :: "'a ⇒ 'a"  ("♢ (_)" [900] 900) where
        "♢ p = (SUP i . p !! i)"

      definition "next" :: "'a ⇒ 'a"  ("⨀ (_)" [900] 900) where
        "⨀ p = p !! (Suc 0)"

      definition until :: "'a ⇒ 'a ⇒ 'a" (infix "until" 65) where 
        "(p until q) = (SUP n . (INFIMUM {i . i < n}  (at p)) ⊓ (q !! n))"

      definition leads :: "'a ⇒ 'a ⇒ 'a" (infix "leads" 65) where 
        "(p leads q) = -(p until -q)"
        
      lemma iterate_next: "(next ^^ n) p = p !! n"
        proof (induction n)
          show "(next ^^ 0) p = p !! 0" by simp
        next
          fix n
          assume [simp]: "(next ^^ n) p = p !! n" 
          show "(next ^^ Suc n) p = p !! Suc n"
            by (simp add: next_def)
        qed

      lemma always_next: "□ p = p ⊓ (□ (⨀ p))"
        apply (simp add: always_def next_def)
        apply (rule antisym, simp_all, safe)
        apply (rule_tac x = "p" in Inf_lower)
        apply (simp add: image_def, rule_tac x = 0 in exI, simp)
        apply (rule INF_greatest, simp)
        apply (rule_tac x = "p !! Suc x" in Inf_lower)
        apply (simp add: image_def, auto)[1]
        apply (rule INF_greatest, simp)
        apply (case_tac i, simp_all)
        apply (rule_tac y = "(INF x. p !! Suc x)" in order_trans, simp_all)
        apply (rule_tac x = "p !! Suc nat" in Inf_lower)
        by (auto simp add: image_def)
    end

text{*
Next lemma, in the context of complete boolean algebras, will be used 
to prove $-(p\ until\ -p) = \Box\; p$.
*}
  context complete_boolean_algebra
    begin
      lemma until_always: "(INF n. (SUP i : {i. i < n} . - p i) ⊔ ((p :: nat ⇒ 'a) n)) ≤ p n"
        proof -
          have "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i:{i. i ≤ n}. p i)"
            proof (induction n)
              have "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (SUP i:{i. i < 0}. - p i) ⊔ p 0"
                by (rule INF_lower, simp)
              also have "... ≤ (INF i:{i. i ≤ 0}. p i)"
                by simp
              finally show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i:{i. i ≤ 0}. p i)"
                by simp
            next
              fix n::nat assume "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i : {i. i ≤ n}. p i)"
              also have "⋀ i . i ≤ n ⟹ ... ≤ p i" by (rule INF_lower, simp)
              finally have [simp]: "⋀ i . i ≤ n ⟹ (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ p i"
                by simp
              show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i : {i. i ≤ Suc n}. p i)"
                proof (rule INF_greatest, safe, cases)
                  fix i::nat
                    assume "i ≤ n" from this show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ p i" by simp
                next
                  fix i::nat
                    have A: "{i. i ≤ n} = {i . i < Suc n}" by auto
                    have B: "(SUP i:{i. i ≤ n}. - p i) ≤ - (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n)"
                      by (metis (lifting, mono_tags) `(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i:{i. i ≤ n}. p i)` compl_mono uminus_INF)
                    assume "i ≤ Suc n" and "¬ i ≤ n"
                    from this have [simp]: "i = Suc n" by simp
                    have "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ⊓ ((SUP i:{i. i ≤ n}. - p i) ⊔ p (Suc n))"
                      by (simp add: A, rule INF_lower, simp)
                    also have "... ≤ ((INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ⊓ ((- (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n)) ⊔ p (Suc n)))"
                      by (rule inf_mono, simp_all, rule_tac y = "- (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n)" in order_trans, simp_all add: B)
                    also have "... ≤ p i"
                      by (simp add: inf_sup_distrib1)
                    finally show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ p i" by simp
                qed
            qed
        also have "(INF i:{i. i ≤ n}. p i) ≤ p n" by (rule INF_lower, auto)
        finally show "(INF n. (SUP i : {i. i < n} . - p i) ⊔ ((p :: nat ⇒ 'a) n)) ≤ p n" by simp
        qed

     end

text{*
  We prove now a number of results of the temporal class.
*}
  context temporal
    begin   
      lemma [simp]: "(a ⊔ b) !! i = (a !! i) ⊔ (b !! i)"
        by (subst compl_eq_compl_iff [THEN sym], simp)

      lemma always_less [simp]: "□ p ≤ p"
        proof -
          have "□ p ≤ p !! 0"
            by (unfold always_def, rule INF_lower, simp)
          also have "p !! 0 = p" by simp
          finally show "□ p ≤ p" by simp
        qed

      lemma always_always: "□ □ x = □ x" 
        apply (rule antisym, simp_all)
        apply (auto simp add: le_fun_def always_def)
        apply (rule INF_greatest, simp)
        apply (rule INF_greatest, simp)
        by (rule INF_lower, simp)

      lemma always_and: "□ (p ⊓ q) = (□ p) ⊓ (□ q)"
        by (simp add: always_def INF_inf_distrib)

      lemma eventually_or: "♢ (p ⊔ q) = (♢ p) ⊔ (♢ q)"
        by (simp add: eventually_def SUP_sup_distrib)

      lemma neg_until_always: "-(p until -p) = □ p"
        proof (rule antisym)
          show "- (p until - p) ≤ □ p"
           by (simp add: until_def always_def uminus_SUP uminus_INF, rule INF_greatest, cut_tac p = "λ n . p !! n" in until_always, simp)
        next
          have "⋀ n . □ p ≤ p !! n"
            by (simp add: always_def INF_lower)
          also have "⋀ n . p !! n ≤ (SUP x:{i. i < n}. (- p) !! x) ⊔ p !! n"
            by simp
          finally show "□ p ≤ -(p until -p)"
            apply (simp add: until_def uminus_SUP uminus_INF)
            by (rule INF_greatest, simp)
        qed

lemma leads_always: "p leads p = □ p"
  by (simp add: neg_until_always leads_def)

      lemma neg_always_eventually: "□ p = - ♢ (- p)"
        by (simp add: fun_eq_iff always_def eventually_def until_def uminus_SUP)
        
      lemma neg_true_until_always: "-(⊤ until -p) = □ p"
        by (simp add: fun_eq_iff always_def until_def uminus_SUP uminus_INF)

lemma top_leads_always: "⊤ leads p = □ p"
  by (simp add: neg_true_until_always leads_def)


      lemma neg_until_true: "-(p until -⊤) = ⊤"
        by (simp add: fun_eq_iff always_def until_def uminus_SUP uminus_INF)

lemma leads_top: "p leads ⊤ = ⊤"
  using neg_until_true by (simp add:  leads_def)

      lemma neg_until_false: "-(p until -⊥) = ⊥"
        proof (simp add: fun_eq_iff always_def until_def uminus_SUP uminus_INF)
          have "⋀f. (⊥::'a) ∈ range (λn. SUPREMUM {na. (na::nat) < n} f)"
            by auto
          then have "⋀f. (INF n. SUPREMUM {na. (na::nat) < n} f) ≤ (⊥::'a)"
            by (meson local.Inf_lower)
          then show "(INF n. SUPREMUM {na. na < n} (op !! (- p))) = ⊥"
            by (simp add: local.le_iff_inf)
        qed

lemma leads_bot: "p leads ⊥ = ⊥"
  using neg_until_false by (simp add:  leads_def)

      lemma true_until_eventually: "(⊤ until p) = ♢ p"
        by (cut_tac p = "-p" in neg_always_eventually, cut_tac p = "-p" in neg_true_until_always, simp)

end

text{*
  Boolean algebras with $b!!i = b$ form a temporal class.
*}

  instantiation bool :: temporal
    begin
      definition at_bool_def [simp]: "(p::bool) !! i = p"
    instance proof 
      qed (auto)
    end

  type_synonym 'a trace = "nat ⇒ 'a"

text{*
  Asumming that $\tv a::temporal$ is a type of class $temporal$, and $\tv b$ is an arbitrary type,
  we would like to create the instantiation of $\tv b\ trace \Rightarrow \tv a$ as a temporal
  class. However Isabelle allows only instatiations of functions from a class to another 
  class. To solve this problem we introduce a new class called trace with an operation
  $\mathit{suffix}::\tv a \Rightarrow nat \Rightarrow \tv a$ where 
  $\mathit{suffix}\;a\;i\;j = (a[i..])\; j = a\;(i+j)$ when
  $a$ is a trace with elements of some type $\tv b$ ($\tv a = nat \Rightarrow \tv b$). 
*}


  class trace =
    fixes suffix :: "'a ⇒ nat ⇒ 'a" ("_[_ ..]" [80, 15] 80)
    fixes eqtop :: "nat ⇒ 'a ⇒ 'a ⇒ bool" 
    fixes cat :: "nat ⇒ 'a ⇒ 'a ⇒ 'a" 
    fixes Cat :: "(nat ⇒ 'a) ⇒ 'a"
    assumes suffix_suffix[simp]: "a[i..][j..] = a[i + j..]"
    assumes [simp]: "a[0..] = a"
    assumes [simp]: "eqtop 0 a b = True"
    assumes [simp]: "eqtop n a a = True"
    assumes all_eqtop[simp]: "∀ n . eqtop n a b ⟹ a = b"
    assumes eqtop_sym: "eqtop n a b =  eqtop n b a"
    assumes eqtop_tran: "eqtop n a b ⟹  eqtop n b c ⟹ eqtop n a c"
    assumes [simp]: "eqtop n (cat n x y) z = eqtop n x z"
    assumes cat_at_eq[simp]: "(cat n x y)[n..] = y"
    assumes eqtop_Suc: "eqtop (Suc n) x y = (eqtop n x y ∧ eqtop (Suc 0) (x[n..]) (y[n..]))"
    assumes Cat_Suc: "Cat u = cat (Suc 0) (u 0) (Cat (λ i . u (Suc i)))"
  assumes cat_Suc: "cat (Suc n) x y = cat (Suc 0) x (cat n (x[Suc 0..]) y)"
  assumes cat_Zero[simp]: "cat 0 x y = y"

    begin
      definition "next_trace" :: "'a ⇒ 'a"  ("⊙ (_)" [900] 900) where
        "⊙ p = p[Suc 0..]"

     lemma  eq_le[simp]: "⋀ a b . n ≤ m ⟹ eqtop m a b ⟹ eqtop n a b"
      apply (induction m, simp)
      apply (case_tac "n = Suc m", simp)
      apply (subst (asm) eqtop_Suc)
       by auto
         
lemma eqtop_Suc_Cat: "⋀ u . eqtop (Suc 0) ((Cat u)[n..]) (u n)"
  proof (induction n)
    case 0
    then show ?case
      apply simp
      apply (subst Cat_Suc)
        by simp
  next
    case (Suc n)
      
    have "(cat (Suc 0) (u 0) (Cat (λi. u (Suc i)))[Suc n ..]) =  (cat (Suc 0) (u 0) (Cat (λi. u (Suc i)))[Suc 0 ..][n..])"
      by (simp del: cat_at_eq)
    also have "... = Cat (λi. u (Suc i))[n ..]"
      by simp
    finally have [simp]: "(cat (Suc 0) (u 0) (Cat (λi. u (Suc i)))[Suc n ..]) =  Cat (λi. u (Suc i))[n ..]"
      by simp
    show ?case
      apply (subst Cat_Suc, simp)
      by (rule Suc)
  qed

     lemma eqtop_tail_eqtop: "eqtop n x y ⟹ x[n ..] = y[n ..] ⟹ eqtop na x y"
       apply (case_tac "na ≤ n", simp_all)
       apply (induction na, simp_all)
       apply (subst eqtop_Suc)
       apply (case_tac "n = na", simp_all)
       apply (cut_tac i = n and j = "na - n" and a = x in suffix_suffix)
       apply (simp del: suffix_suffix)
       by simp

     lemma [simp]: "eqtop n z (cat n x y) = eqtop n z x"
       by (subst eqtop_sym, simp, subst eqtop_sym, simp)
         
        

     lemma eqtop_tail: "eqtop n x y ⟹ x[n..] = y[n..] ⟹ x = y"
      apply (rule all_eqtop, safe)
      by (rule eqtop_tail_eqtop, simp_all)

     definition "cons x = cat (Suc 0) x x"
     
     lemma [simp]: "(cons a)[Suc 0..] = a"
      by (simp add: cons_def)

     lemma [simp]: "eqtop 0 = ⊤"
      by (simp add: fun_eq_iff)

     lemma [simp]: "eqtop n x (cat n x y)"
       by (subst eqtop_sym, simp)

     lemma [simp]: "∃y. x = y[Suc 0 ..]"
       by (rule_tac x = "cons x" in exI, simp)

     lemma eqtop_plus: "⋀ x y . (eqtop n x y ∧ (eqtop m (x[n..]) (y[n..]))) = eqtop (n + m) x y"
       apply (induction m, simp)
       apply (subst eqtop_Suc)
       apply simp
       apply (subst (2) eqtop_Suc)
       by auto

     lemma [simp]: "cat n (cat n x y) z = cat n x z"
      by (rule_tac n = n in eqtop_tail, simp_all)

     lemma [simp]: "cat n x (x[n..]) = x"
       by (rule_tac n = n in eqtop_tail, simp_all)
         

     lemma eqtop_Suc_a: "eqtop (Suc n) x y = (eqtop (Suc 0) x y ∧ eqtop n (x[Suc 0 ..]) (y[Suc 0 ..]))"
       by (cut_tac n = "Suc 0" and m = "n" in eqtop_plus, auto)
         
    
lemma cat_Suc_b: "⋀ x y . cat (Suc n) x y = cat n x (cat (Suc 0) (x[n..]) y)"
  apply (induction n, simp_all)
  apply (subst cat_Suc)
  apply simp
  apply (subst cat_Suc[THEN sym])
    by simp

         
lemma cat_at: "⋀ i x y . i ≤ n ⟹ (cat n x y[i..]) = cat (n - i) (x[i..]) y"
  proof (induction n)
    case 0
    then show ?case 
      by simp
  next
    case (Suc n)
    then show ?case 
      apply (case_tac "i = Suc n", simp_all)
      apply (subst cat_Suc_b)
      apply (case_tac "i ≤ n", simp_all)
      apply (subgoal_tac "x[n ..] = x[i..][n-i..]")
       apply (simp del: suffix_suffix add: cat_Suc_b[THEN sym])
       apply simp_all
      apply (subgoal_tac "(Suc (n - i)) = Suc n - i")
        by auto
  qed
    
lemma eqtop_cat_le: "⋀ m x y z . m ≤ n ⟹ eqtop m (cat n x y) z = eqtop m x z"
  proof (induction n)
    case 0
    then show ?case
      by simp
  next
    case (Suc n)
    then show ?case 
      apply (case_tac "m = Suc n")
       apply simp
      apply (subst cat_Suc_b)
        by (subst Suc, simp_all)
        
  qed
         
lemma eqtop_cat_aux: "i < n ⟹ eqtop (Suc 0) (cat n x y[i..]) (x[i..])"
  by (simp add: cat_at eqtop_cat_le)


    end

  instantiation "prod" :: (trace, trace) trace
    begin
      definition at_prod_def: "x[i..] ≡ ((fst x)[i..], (snd x)[i..])"
      definition eqtop_prod_def: "eqtop n x y ≡ eqtop n (fst x) (fst y) ∧ eqtop n (snd x) (snd y)"
      definition cat_prod_def: "cat n x y ≡ (cat n (fst x) (fst y), cat n (snd x) (snd y))"
      definition Cat_prod_def: "Cat u ≡ (Cat (fst o u), Cat (snd o u))"

      instance proof
        fix n:: nat fix a b c:: "'a × 'b"
        assume "eqtop n a b" and " eqtop n b c"
        from this show "eqtop n a c"
          apply (simp add: eqtop_prod_def, safe)
          apply (rule_tac b = "fst b" in eqtop_tran, simp_all)
          by (rule_tac b = "snd b" in eqtop_tran, simp_all)
        next
        fix n:: nat fix x y:: "'a × 'b"
          show "cat (Suc n) x y = cat (Suc 0) x (cat n (x[Suc 0..]) y)"
            apply (simp add: cat_prod_def at_prod_def)
            apply (subst cat_Suc)
              apply simp
            apply (subst cat_Suc)
              by simp

        next
        qed (auto simp add: at_prod_def  eqtop_prod_def all_conj_distrib cat_prod_def Cat_prod_def, simp_all add: eqtop_sym eqtop_tail,
          metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, 
          subst Cat_Suc, simp add: comp_def, subst Cat_Suc, simp add: comp_def)

    end

  instantiation "fun" :: (trace, temporal) temporal
    begin
      definition at_fun_def: "(P:: 'a ⇒ 'b) !! i = (λ x . (P (x[i..])) !! i)"
      instance proof qed  (simp_all add: at_fun_def add.commute fun_eq_iff le_fun_def)
end
  

lemma SUP_Suc: "(SUP x:{i. i < Suc n}. p x) = (SUP x:{i. i < n}. p x) ⊔ ((p n)::'a::complete_lattice)"
  apply (rule antisym)
   apply (rule SUP_least, safe)
    apply (case_tac "x = n", simp_all)
   apply (simp add: SUP_upper le_supI1)
    apply auto
   apply (rule SUP_least, auto)
  by (simp_all add: SUP_upper)

  
definition "top_dep p = (∀ x x' . eqtop (Suc 0) x x' ⟶ p x = p x')"

lemma INF_distrib: "(INF x y. p x ⊔ ((q y)::'a::complete_distrib_lattice)) = (INF x . p x) ⊔ (INF y . q y)"
  apply (simp add: sup_INF Inf_sup)
    by (subst INF_commute, simp)
  
lemma top_dep_INF_SUP: "top_dep p ⟹  (INF x. (SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p (x[n ..])) !! n) = 
   (INF x y. (SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p y) !! n)"
  apply (rule antisym)
  apply (rule INF_greatest,simp)
   apply (rule INF_greatest,simp)
   apply (rule_tac y = "(SUP xa:{i. i < n}. (- p ((cat n x y)[xa ..])) !! xa) ⊔ (- p ((cat n x y)[n ..])) !! n" in order_trans)
  apply(rule_tac i = "(cat n x y)" in INF_lower, simp_all)

   apply (subgoal_tac "⋀ xa . xa < n ⟹ p (cat n x y[xa ..])  = p (x[xa ..])")
    apply simp
    
   apply (simp add: top_dep_def)
   apply (drule_tac x = "(cat n x y[xa ..])" in spec)
   apply (drule_tac x = "(x[xa ..])" in spec)
   apply auto
    apply (simp add: eqtop_cat_aux)
    
  apply (rule INF_greatest,simp)
  apply (rule_tac y = " (INF y. (SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p y) !! n) " in order_trans)
    apply(rule_tac i = "x" in INF_lower, simp_all)
  apply (rule_tac y = "(SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p (x[n ..])) !! n " in order_trans)
  by(rule_tac i = "x[n ..]" in INF_lower, simp_all)      
    

      
lemma top_dep_all_leadsto_aux: "top_dep p ⟹ (INF b. SUP x:{i. i < n}. (- p (b[x ..])) !! x) ≤ (SUP x:{i. i < n}. INF xa. (- p xa) !! x)"
  proof (induction n)
    case 0
    then show ?case 
      by simp
  next
    case (Suc n)
    then show ?case 
      apply (simp add: SUP_Suc)
      apply (rule_tac y = "(INF b. SUP x:{i. i < n}. (- p (b[x ..])) !! x) ⊔ (INF xa. (- p xa) !! n)" in order_trans)
       apply simp_all
       apply (simp add: top_dep_INF_SUP)
        apply (simp add: INF_distrib)
        by (rule_tac y = "(SUP x:{i. i < n}. INF xa. (- p xa) !! x)" in order_trans, simp_all)
  qed
 
  
(*change the proof using INF_SUP*)
theorem top_dep_all_leadsto: "top_dep p ⟹ INFIMUM UNIV (p leads (λ y . q)) = ((SUPREMUM UNIV p) leads q)"
  apply (simp add: until_def leads_def)
  apply (simp add:   until_def uminus_SUP uminus_INF at_fun_def)
  apply (rule antisym)
   apply (rule INF_greatest, simp_all)

   prefer 2
   apply (rule INF_greatest, simp_all)
   apply (rule INF_greatest, simp_all)
   apply (rule_tac y = " (SUP x:{i. i < xa}. INF xa. (- p xa) !! x) ⊔ q !! xa" in order_trans)
    apply (rule INF_lower, simp_all)
   apply (rule_tac y = "(SUP xa:{i. i < xa}. (- p (x[xa ..])) !! xa)" in order_trans)
    apply simp_all
    apply (rule_tac SUP_least, simp)
   apply (rule_tac y = "(- p (x[xb ..])) !! xb" in order_trans)
    apply (meson INF_lower2 UNIV_I order_refl)
   apply (simp add: SUP_upper2)
  apply (subst INF_commute)
    
  apply (rule_tac y = "(INF z. (SUP x:{i. i < x}. (- p (z[x ..])) !! x) ⊔ q !! x)" in order_trans)
   apply (rule INF_lower, simp)
  apply (subst INF_sup [THEN sym], simp)
  apply (rule_tac y = "(SUP x:{i. i < x}. INF xa. (- p xa) !! x)" in order_trans, simp_all)
  by (simp add: top_dep_all_leadsto_aux)
    

  
theorem SUP_Always: "top_dep p ⟹ SUPREMUM UNIV (□ p) = □ (SUPREMUM UNIV  (p::('b::trace) ⇒ 'a::temporal))"
proof (simp add: always_def Sup_at at_fun_def INF_SUP)
  assume A: "top_dep p"
  have "⋀x. (INF n. p (x[n ..]) !! n) ≤ (SUP x. INF n. p (x n) !! n)"
    by (rule_tac i = "(λ i . x[i ..])" in SUP_upper2, simp_all)
  from this have [simp]: "(SUP x. INF n. p (x[n ..]) !! n) ≤ (SUP x. INF n. p (x n) !! n)"
   by (rule SUP_least)
  have "⋀x. (INF n. p (x n) !! n) ≤ (SUP x. INF n. p (x[n ..]) !! n)"
    apply (rule_tac y =  "INF n. p ((Cat x)[n ..]) !! n" in order_trans)
     apply (rule INF_greatest, simp)
     apply (rule_tac y = "p (x n) !! n" in order_trans)
      apply (rule INF_lower, simp)
    using A apply (simp add: top_dep_def)
     apply (drule_tac x = "Cat x[n ..]" in spec)
     apply (drule_tac x = "x n" in spec)
    apply (simp add: eqtop_Suc_Cat)
    by (rule SUP_upper, simp)
  from this have [simp]: "(SUP x. INF n. p (x n) !! n) ≤ (SUP x. INF n. p (x[n ..]) !! n)"
    by (rule SUP_least)
  show "(SUP x. INF xa. p (x[xa ..]) !! xa) = (SUP x. INF xa. p (x xa) !! xa)"
    by (rule antisym, simp_all)
qed

text{*
  In the last part of our formalization, we need to instantiate the functions
  from $nat$ to some arbitrary type $\tv a$ as a trace class. However, this again is not
  possible using the instatiation mechanism of Isabelle. We solve this problem
  by creating another class called $nat$, and then we instatiate the functions
  from $\tv a::nat$ to $\tv b$ as traces. The class $nat$ is defined such that if we
  have a type $\tv a::nat$, then $\tv a$ is isomorphic to the type $nat$. 
*}

  class nat = zero + plus + minus + one +
    fixes RepNat :: "'a ⇒ nat"
    fixes AbsNat :: "nat ⇒ 'a"
    assumes RepAbsNat[simp]: "RepNat (AbsNat n) = n"
    and AbsRepNat[simp]: "AbsNat (RepNat x) = x"
    and zero_Nat_def: "0 = AbsNat 0"
    and one_Nat_def: "1 = AbsNat 1"
    and plus_Nat_def: "a + b = AbsNat (RepNat a + RepNat b)"
    and minus_Nat_def: "a - b = AbsNat (RepNat a - RepNat b)"
  begin
    lemma AbsNat_plus: "AbsNat (i + j) = AbsNat i + AbsNat j"
      by (simp add: plus_Nat_def)
    lemma AbsNat_minus: "AbsNat (i - j) = AbsNat i - AbsNat j"
      by (simp add: minus_Nat_def)
    lemma AbsNat_zero [simp]: "AbsNat 0 + i = i"
      by (simp add: plus_Nat_def)
    lemma [simp]: "(AbsNat (Suc 0) + x = 0) = False"
      apply (simp add: plus_Nat_def zero_Nat_def)
      apply (rule notI)
      apply (subgoal_tac "RepNat (AbsNat (Suc (RepNat x))) = RepNat (AbsNat 0)")
      apply (unfold RepAbsNat) [1]
      by simp_all

    subclass comm_monoid_diff 
      apply (unfold_locales)
        apply (simp_all add: plus_Nat_def zero_Nat_def minus_Nat_def add.assoc)
        by (simp add: add.commute)
  end

text{*
  The type natural numbers is an instantiation of the class $nat$.
*}

  instantiation nat :: nat
    begin
      definition RepNat_nat_def [simp]: "(RepNat:: nat ⇒ nat) = id"
      definition AbsNat_nat_def [simp]: "(AbsNat:: nat ⇒ nat) = id"
      instance proof 
        qed auto
    end

text{*
  Finally, functions from $\tv a::nat$ to some arbitrary type $\tv b$ are instatiated
  as a trace class. 
*}

  instantiation "fun" :: (nat, type) trace
    begin
      definition at_trace_def [simp]: "((t :: 'a ⇒ 'b)[i..]) j = (t  (AbsNat i + j))"
      definition eqtop_trace_def [simp]: "eqtop n a b = (∀ i < n . a (AbsNat i) = b (AbsNat i))"
      definition cat_trace_def [simp]: "cat n a b i = (if RepNat i < n then a i else b (i - AbsNat n))"
      definition Cat_trace_def [simp]: "Cat y i = (y (RepNat i) 0)"
      lemma  eqtop_trace_eq: "∀n i. i < n ⟶ (a::'a⇒'b) (AbsNat i) = b (AbsNat i) ⟹ a = b"
        proof (simp add: fun_eq_iff, safe)
          fix x:: "'a"
          assume " ∀n i. i < n ⟶ a (AbsNat i) = b (AbsNat i)"
          from this have "∀ i < Suc (RepNat x) .  a (AbsNat i) = b (AbsNat i)" by blast
          from this have "a (AbsNat (RepNat x)) = b (AbsNat (RepNat x))" by blast
          from this show "a x = b x" by simp
        qed

    lemma [simp]: "(RepNat (AbsNat n + xa) < n) = False"
      by (subst plus_Nat_def, simp)

    lemma [simp]: "AbsNat n + AbsNat 0 = AbsNat n"
      by (subst plus_Nat_def, simp)

    lemma trace_eqtop_tail: "∀i<n. x (AbsNat i) = y (AbsNat i) ⟹ ∀xa. x (AbsNat n + xa) = y (AbsNat n + xa) ⟹ x xa = y xa"
      by (metis AbsNat_plus AbsRepNat add_diff_inverse)
 
    lemma trace_eqtop_Suc: "∀i<n. x (AbsNat i) = y (AbsNat i) ⟹ x (AbsNat n) = y (AbsNat n) ⟹ i < Suc n ⟹ x (AbsNat i) = y (AbsNat i)"
      by (metis less_antisym)

    lemma RepNat_is_zero: "RepNat x = 0 ⟹ x = 0"
      proof -
      assume "RepNat x = 0"
      from this have "AbsNat (RepNat x) = AbsNat(0)" by simp
      from this show "x = 0" apply (subst zero_Nat_def)
        by (subst (asm) AbsRepNat, simp)
    qed

    lemma RepNat_zero: "RepNat x = 0 ⟹ u 0 x = u 0 0"
      by (drule RepNat_is_zero, simp)

    lemma [simp]: "0 < RepNat x ⟹ (Suc (RepNat (x - AbsNat (Suc 0)))) = RepNat x"
      by (subst minus_Nat_def, simp)
        
    

instance proof
  fix n::nat fix x y :: "'a ⇒ 'b"
          show "cat (Suc n) x y = cat (Suc 0) x (cat n (x[Suc 0..]) y)"
            apply (simp add:   fun_eq_iff)
              apply auto
               apply (metis (no_types, lifting) AbsRepNat RepAbsNat Suc_pred add.left_neutral add_Suc_shift minus_Nat_def plus_Nat_def)
            using not_less_eq apply auto[1]
            using less_Suc_eq_0_disj apply auto[1]
            by (metis (no_types, lifting) One_nat_def RepAbsNat diff_Suc_eq_diff_pred minus_Nat_def)
        next
          fix x y :: "'a ⇒ 'b"
       
          show "cat 0 x y = y"
            apply (auto simp add:   fun_eq_iff)
            by (metis diff_zero zero_Nat_def)
       next
      qed (auto simp add: fun_eq_iff AbsNat_plus add.assoc AbsNat_minus one_Nat_def RepNat_zero, drule eqtop_trace_eq, 
           simp_all, drule trace_eqtop_Suc)
    end

text{*
  By putting together all class definitions and instatiations introduced so far, we obtain the
  temporal class structure for predicates on traces with arbitrary number of parameters.

  For example in the next lemma $r$ and $r'$ are predicate relations, and the operator
  always is available for them as a consequence of the above construction.
*}

  lemma "(□ r) OO (□ r') ≤ (□ (r OO r'))"
    by (simp add: le_fun_def always_def at_fun_def, auto)

  lemma [simp]: "(next ^^ n) ⊤ = ⊤"
    apply (induction n, simp)
    by (simp add: next_def)

 (*some tests for next of a variable*)

  lemma "r (u[1..]) = (∃ y . (⨀ (λ v . v = y ∧ r y)) u)"
    apply safe
    apply (rule_tac x = "u[1..]" in exI)
    apply (simp add: next_def at_fun_def)
    by (simp add: next_def at_fun_def)

  lemma "r (u[1..]) = ( (⨀ (λ v . ∃ y . v = y ∧ r y)) u)"
    apply safe
    apply (simp add: next_def at_fun_def)
    by (simp add: next_def at_fun_def)

  lemma "(r (u[1..])::bool) = ( (⨀ r) u)"
    apply safe
    apply (simp add: next_def at_fun_def)
    by (simp add: next_def at_fun_def)

  lemma "((□ r) u (u[1..]) x y ::bool) = ( (⨀ (λ u' . (□ r) u u' x y)) u)"
    apply safe
    apply (simp add: next_def at_fun_def)
    by (simp add: next_def at_fun_def)


  lemma "r (u[1..]) = (∃ y . (⨀ (λ v y . v = y ∧ r  y)) u y)"
    apply safe
    apply (rule_tac x = "u" in exI)
    apply (simp add: next_def at_fun_def)
    by (simp add: next_def at_fun_def)

subsection{*Propositional Temporal Logic*}

  (*P is the name of a propositional variable*)
definition "prop P σ = (P ∈ σ (0::nat))"

(*Existential quantification for a propositional variable*)
  
definition "Exists P f σ = (∃ σ' . (∀ i . σ i - {P} = σ' i - {P}) ∧ f σ')"
definition "Forall P f σ = (∀ σ' . (∀ i . σ i - {P} = σ' i - {P}) ⟶ f σ')"
definition impl:: "'a ⇒ 'a ⇒ ('a::boolean_algebra)"  (infixl "→" 60)
  where "x → y = ((-x) ⊔ y)"


lemma "x ≠ y ⟹ (Exists y ((□ (prop x → (♢ prop y))) ⊓ □ ♢ prop y)) = ⊤"
  apply (auto simp add: fun_eq_iff)
  apply (simp add: Exists_def)
  apply (rule_tac x = "λ i . xa i ∪ {y}" in exI, simp, safe)
   apply (simp add: always_def at_fun_def impl_def, safe)
   apply (simp add: eventually_def at_fun_def)
   apply (rule_tac x = 0 in exI)
   apply (simp add: prop_def)
    
   apply (simp add: always_def at_fun_def impl_def eventually_def, safe)
   apply (rule_tac x = 0 in exI)
  by (simp add: prop_def)
    
lemma "x ≠ y ⟹ (Forall y ((□ (prop x → (♢ prop y))) → □ ♢ prop y)) = (□ ♢ (prop x))"
  apply (auto simp add: fun_eq_iff)
   apply (simp add: Forall_def impl_def sup_fun_def)
   apply (subst always_def)
   apply (subst eventually_def)
   apply (simp add: at_fun_def, safe)
   apply (subst prop_def, simp)
   apply (drule_tac x = "λ i . if i < f then xa i ∪ {y} else xa i - {y}" in spec)
   apply safe
      apply auto [1]
    apply (case_tac "i < f") 
      apply auto [2]
    apply (simp add: always_def eventually_def at_fun_def prop_def, safe)
    apply (case_tac "fa < f", simp_all)
     apply (drule_tac x = 0 in spec, simp)
    apply (rule_tac x = "fa - f" in exI, simp)
    apply (simp add: always_def eventually_def at_fun_def prop_def)
   apply (drule_tac x = f in spec, simp)
    apply (simp add: Forall_def impl_def, safe)
  apply (simp add: always_def eventually_def at_fun_def prop_def, safe)
  apply (drule_tac x = f in spec, safe)
    apply (drule_tac x = "f + fa" in spec)
  apply (drule_tac x = "f + fa" in spec, safe)
   apply auto[1]
  apply (rule_tac x = "fa + fb" in exI)
  by (simp add: add.assoc)


  end