Theory Reactive

theory Reactive
  imports Temporal Refinement
begin
  section‹Reactive Systems›

  text‹
    In this section we introduce reactive systems which are modeled as 
    monotonic property transformers where properties are predicates on
    traces. We start with introducing some examples that uses LTL to
    specify global behaviour on traces, and later we introduce property
    transformers based on symbolic transition systems.
›

  definition "HAVOC = [:x ↝ y . True:]"
  definition "ASSERT_LIVE = {. □ ◇ (λ x . x 0).}"
  definition "GUARANTY_LIVE = [:x ↝ y . □ ◇ (λ y . y 0):]"
  definition "AE = ASSERT_LIVE o HAVOC"
  definition "SKIP = [:x ↝ y . x = y:]"

  lemma [simp]: "SKIP = id"
    by (auto simp add: fun_eq_iff SKIP_def demonic_def)

  definition "REQ_RESP = [: □(λ xs ys . xs (0::nat) ⟶ (◇ (λ ys . ys (0::nat))) ys) :]"
  definition "FAIL = ⊥"

  lemma "HAVOC o ASSERT_LIVE = FAIL"
    by (auto simp add: HAVOC_def AE_def FAIL_def ASSERT_LIVE_def fun_eq_iff assert_def demonic_def always_def at_fun_def le_fun_def eventually_def)
    

  lemma "HAVOC o AE = FAIL"
    by (auto simp add: HAVOC_def AE_def FAIL_def ASSERT_LIVE_def fun_eq_iff assert_def demonic_def always_def at_fun_def le_fun_def eventually_def)

  lemma "HAVOC o ASSERT_LIVE = FAIL"
    by (auto simp add: HAVOC_def AE_def FAIL_def ASSERT_LIVE_def fun_eq_iff assert_def demonic_def always_def  at_fun_def eventually_def)

  lemma "SKIP o AE = AE"
    by simp

  lemma "(REQ_RESP o AE) = AE"
    proof (auto simp add: fun_eq_iff HAVOC_def AE_def FAIL_def REQ_RESP_def ASSERT_LIVE_def  assert_def 
      demonic_def always_def le_fun_def eventually_def at_fun_def)
      fix x :: "'a ⇒ bool" 
      fix xa :: "nat ⇒ bool" 
      fix xb :: nat
      assume "∀xb::nat ⇒ bool . (∀x. xa x ⟶ Ex (xb[x ..])) ⟶ (∀x. ∃a. xb (x + a)) ∧ All x"
      then have "(∀x. xa x ⟶ Ex (xa[x ..])) ⟶ (∀x. ∃a. xa (x + a)) ∧ All x"
        by auto
      then show "∃x. xa (xb + x)"
        by (auto, rule_tac x = 0 in exI, simp)
    next
      fix x :: "'a ⇒ bool" 
      fix xa :: "nat ⇒ bool" 
      fix xb :: 'a
      assume "∀xb::nat ⇒ bool . (∀x. xa x ⟶ Ex (xb[x ..])) ⟶ (∀x. ∃a. xb (x + a)) ∧ All x"
      from this show "x xb"
        by (metis at_trace_def le0)
    next
      fix x :: "'a ⇒ bool" and xa :: "nat ⇒ bool" and xb :: "nat ⇒ bool" and xc :: nat
      assume A: "∀x. xa x ⟶ Ex (xb[x ..])"
      assume B: "∀x. ∃xb. xa (x + xb)"
      have "∃x1. xc ≤ AbsNat x1" by (metis (full_types) le_add2 plus_Nat_def)
      thus "∃x. xb (xc + x)" using A B by (metis AbsNat_plus add.commute at_trace_def le_Suc_ex trans_le_add2)
   qed


  subsection‹Symbolic transition systems›
  
  text‹
    In this section we introduce property transformers basend on symbolic
    transition systems. These are systems with local state. The execution
    starts in some initial state, and with some input value the system computes
    a new state and an output value. Then using the current state, and a 
    new input value the system computes a new state, and a new output, and
    so on. The system may fail if at some point the input and the current 
    state do not statisfy a required predicate.

    In the folowing definitions the variables $u$, $x$, $y$ stand for the
    state of the system, the input, and the output respectively. The $init$ 
    is the property that the initial state should satisfy. The predicate
    $p$ is the precondition of the input and the current state, and the
    relation $r$ gives the next state and the output based on the
    input and the current state.
›
 
  definition "fail_sys init p r x = (∃ n u y . u ∈ init ∧ (∀ i < n . r (u i) (u (Suc i)) (x i) (y i)) ∧ (¬ p (u n) (u (Suc n)) (x n)))"
  definition "run r u x y = (∀ i . r (u i) (u (Suc i)) (x i) (y i))"
  definition "LocalSystem init p r q x = (¬ fail_sys init p r x ∧ (∀ u y . (u ∈ init ∧ run r u x y) ⟶ q y))"

  lemma "fail (LocalSystem init p r) = fail_sys init p r"
    by (simp add: fun_eq_iff LocalSystem_def fail_def fail_sys_def run_def)

  definition "inpt_st r u u' x =  (∃ y . r u u' x y)"

  definition "lft_pred_st p u x = p (u (0::nat)) (u 1) (x (0::nat))"

  definition "lft_pred_loc_st p u x = p (u (0::nat)) (x (0::nat))"

  definition "lft_rel_st r u x y = r (u (0::nat)) (u 1) (x (0::nat)) (y (0::nat))"

  definition "prec_st p r = -((lft_pred_st (inpt_st r)) until -(lft_pred_st p))"

  lemma prec_st_simp: "prec_st p r u x = (∀ n . (∀ i < n . inpt_st r (u i) (u (Suc i)) (x i)) ⟶ p (u n) (u (Suc n)) (x n))"
    by (simp add: prec_st_def until_def lft_pred_st_def inpt_st_def at_fun_def, metis)

  definition "SymSystem init p r = [:z ↝  u, x . u ∈ init ∧ z = x:] o {.u, x . prec_st p r u x.} o 
      [:u, x ↝ y . (□ (lft_rel_st r)) u x y :]"

  lemma SymSystem_rel: "SymSystem init p r = {. x . ∀u. u ∈ init ⟶ prec_st p r u x .} ∘ 
    [: x ↝ y . ∃ u . u ∈ init ∧ (□ lft_rel_st r) u x y :] "
    proof -
      have [simp]:  "((λz (u, x). u ∈ init ∧ z = x) OO (λ(x, y). (□ lft_rel_st r) x y)) = (λx y. ∃u. u ∈ init ∧ (□ lft_rel_st r) u x y)"
        by auto
      show ?thesis by  (simp add: SymSystem_def demonic_assert_comp comp_assoc demonic_demonic)
    qed

  theorem "SymSystem init p r q x = LocalSystem init p r q x"
    proof
      assume "SymSystem init p r q x"
      then show "LocalSystem init p r q x"
        apply (auto simp add: SymSystem_def LocalSystem_def assert_def 
          demonic_def prec_st_simp lft_rel_st_def lft_pred_st_def inpt_st_def
          always_def  le_fun_def fail_sys_def run_def at_fun_def)
        by metis
    next
      assume "LocalSystem init p r q x"
      then show "SymSystem init p r q x"
        apply (auto simp add: SymSystem_def LocalSystem_def assert_def 
          demonic_def prec_st_simp lft_rel_st_def lft_pred_st_def inpt_st_def
          always_def  le_fun_def fail_sys_def run_def at_fun_def)
        by metis
    qed

  definition "local_init init S = Inf (S ` init)"

  definition "zip_set A B = {u . ((fst o u) ∈ A) ∧ ((snd o u) ∈ B)}"
  definition nzip:: "('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ ('a×'b)" (infixl "||" 65) where "(xs || ys) i = (xs i, ys i)"

  lemma [simp]: "fst ∘ x || y = x"
    by (simp add: fun_eq_iff nzip_def)

  lemma [simp]: "snd ∘ x || y = y"
    by (simp add: fun_eq_iff nzip_def)

  lemma [simp]: "x ∈ A ⟹ y ∈ B ⟹ (x || y) ∈ zip_set A B"
    by (simp add: zip_set_def)

  lemma local_demonic_init: "local_init init (λ u . {. x . p u x.} o [:x ↝ y . r u x y :]) = 
        [:z ↝ u, x . u ∈ init ∧ z = x:] o {.u, x . p u x.} o [:u, x ↝ y . r u x y :]"
    by (auto simp add: fun_eq_iff demonic_def assert_def local_init_def le_fun_def)

  lemma local_init_comp: "u' ∈ init' ⟹ (∀ u. sconjunctive (S u)) ⟹ (local_init init S) o (local_init init' S') 
                       = local_init (zip_set init init') (λ u . (S (fst o u)) o (S' (snd o u)))"
      proof (subst fun_eq_iff, auto)
        fix x :: 'f
        assume A: "u' ∈ init'"
        assume "∀ u . sconjunctive (S u)"
        from this have [simp]: "⋀ u . sconjunctive (S u)" by simp
        from A have [simp]: "⋀ y . S y (INF y' ∈ init'. S' y' x) =  (INF y' ∈ init' . S y (S' y' x))"
          by (simp add: sconjunctive_INF_simp image_comp)

        have [simp]: "(INF y ∈ init . (INF y' ∈ init' . S y (S' y' x))) ≤ (INF u ∈ zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x))"
          proof (rule INF_greatest, auto simp add: zip_set_def)
            fix u :: "'a ⇒ 'c × 'b"
            assume [simp]: "fst ∘ u ∈ init"
            assume [simp]: "snd ∘ u ∈ init'"
            have "(INF y ∈ init. INF y' ∈ init'. S y (S' y' x)) ≤ (INF y' ∈ init'. S (fst o u) (S' y' x))"
              by (rule INF_lower, simp)
            also have "... ≤ S (fst o u) (S' (snd o u) x)"
              by (rule INF_lower, simp)
            finally show "(INF y ∈ init. INF y' ∈ init'. S y (S' y' x)) ≤ S (fst o u) (S' (snd o u) x)"
              by simp
          qed
        have [simp]: "(INF u ∈ zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x)) ≤ (INF y ∈ init . (INF y' ∈ init' . S y (S' y' x)))"
          proof (rule INF_greatest, rule INF_greatest)
            fix y :: "'a ⇒ 'c" and y':: "'a ⇒ 'b"
            assume [simp]: "y ∈ init"
            assume [simp]: "y' ∈ init'"
            have "(INF u ∈ zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x)) ≤ S (fst o (y || y')) (S' (snd o (y || y')) x)"
              by (rule INF_lower, simp)
            also have "... ≤  S y (S' y' x)"
              by simp
            finally show "(INF u :: 'a ⇒ 'c × 'b ∈ zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x)) ≤ S y (S' y' x)"
              by simp
          qed
        have "local_init init S (local_init init' S' x) = (INF y ∈ init. S y (INF y' ∈ init'. S' y' x)) "
          by (simp add: local_init_def image_comp)
        also have "... = (INF y ∈ init . (INF y' ∈ init' . S y (S' y' x)))"
          by simp
        also have "... = (INF u ∈ zip_set init init'. S (fst ∘ u) ∘ S' (snd ∘ u)) x"
         by (rule antisym) (simp_all add: image_comp)
        also have "... = local_init (zip_set init init') (λ u . (S (fst o u)) o (S' (snd o u))) x"
          by (simp add: local_init_def)
        finally show "local_init init S (local_init init' S' x) = local_init (zip_set init init') (λu::'a ⇒ 'c × 'b. S (fst ∘ u) ∘ S' (snd ∘ u)) x"
          by simp
      qed

  lemma init_state: "[:z ↝ u, x . u ∈ init ∧ z = x:] o {.u, x . p u x.} o [:u, x ↝ y . r u x y :] 
      = [:z ↝ u, x . z = x:] o {.u, x . u ∈ init ⟶ p u x.} o [:u, x ↝ y . u ∈ init ∧ r u x y :]"
    by (auto simp add: fun_eq_iff demonic_def assert_def local_init_def le_fun_def)

  lemma always_lft_rel_comp: "(□ lft_rel_st r) (fst ∘ u) OO (□ lft_rel_st r') (snd ∘ u) 
              = (□ lft_rel_st (λ (u, v) (u', v') . ((r u u') OO (r' v v')))) u"
    proof (auto simp add: fun_eq_iff lft_rel_st_def always_def at_fun_def relcompp_exists)
      fix x::"nat ⇒'a" and
          y::"nat ⇒ 'b" and
          v::"nat ⇒ 'c" and
          n:: nat
      assume "∀i . r (fst (u i)) (fst (u (Suc i))) (x i) (v i)"
      and "∀i . r' (snd (u i)) (snd (u (Suc i))) (v i) (y i)"
      from this show "(case u n of (u, v) ⇒ λ(u', v'). r u u' OO r' v v') (u (Suc n)) (x n) (y n)"
        by (metis (mono_tags, lifting)  prod.case_eq_if relcompp.relcompI)
    next
      fix x::"nat ⇒'a" and
          z::"nat ⇒ 'b"
      define a where "a n = (SOME y . r (fst (u n)) (fst (u (Suc n))) (x n) y ∧ r' (snd (u n)) (snd (u (Suc n))) y (z n))"
        for n
      assume "∀i . (case u i of (u, v) ⇒ λ(u', v'). r u u' OO r' v v') (u (Suc i)) (x i) (z i)"
      from this and a_def have "(∀i :: nat. r (fst (u i)) (fst (u (Suc i))) (x i) (a i)) ∧ (∀i :: nat. r' (snd (u i)) (snd (u (Suc i))) (a i) (z i))"
        apply auto
          apply (metis (mono_tags, lifting) pick_middlep prod.collapse split_conv tfl_some)
          by (metis (mono_tags, lifting) pick_middlep prod.collapse split_conv tfl_some)
     from this show "∃ a . (∀i . r (fst (u i)) (fst (u (Suc i))) (x i) (a i)) ∧ (∀i . r' (snd (u i)) (snd (u (Suc i))) (a i) (z i))"
      by blast
    qed

 theorem SymSystem_comp: "u' ∈ init' ⟹ SymSystem init p r o SymSystem init' p' r' 
                   = [:z ↝ u, x . fst o u ∈ init ∧ snd o u ∈ init' ∧ z = x:] 
                   o {. u, x . prec_st p r (fst ∘ u) x ∧ (∀y. (□ lft_rel_st r) (fst ∘ u) x y ⟶ prec_st p' r' (snd ∘ u) y) .} 
                   o [: u, x ↝ y . (□ lft_rel_st (λ(u, v) (u', v'). r u u' OO r' v v')) u x y :]"
                   (is "?p ⟹ ?S  = ?T")
    proof -
      assume A: "?p"
      have "?S = 
        [: z ↝ (u, x) . u ∈ init ∧ z = x :] ∘ {.x, y. prec_st p r x y.} ∘
        [: id (λ(u, x). id ((□ lft_rel_st r) u x)) :] ∘
        ([: z ↝ u, x . u ∈ init' ∧ z = x :] ∘ {.x, y. prec_st p' r' x y.} ∘
        [: id (λ(u, x). id ((□ lft_rel_st r') u x)) :])"
        by (unfold SymSystem_def, simp)
      also have "... =  local_init init (λu::nat ⇒ 'e. {. id (prec_st p r u) .} ∘ [: id (λx. id ((□ lft_rel_st r) u x)) :]) ∘
          local_init init' (λu. {. id (prec_st p' r' u) .} ∘ [: id (λx::nat ⇒ 'd. id ((□ lft_rel_st r') u x)) :])"
        by (unfold local_demonic_init [THEN sym], simp)
      also from A have "... = local_init (zip_set init init')
            (λu. {. prec_st p r (fst ∘ u) .} ∘ [: (□ lft_rel_st r) (fst ∘ u) :] ∘ ({. prec_st p' r' (snd ∘ u) .} ∘ [: (□ lft_rel_st r') (snd ∘ u) :]))"
              by (simp add: local_init_comp)
      also have " ... = local_init (zip_set init init')
         (λu. {. prec_st p r (fst ∘ u) .} ∘ [: (□ lft_rel_st r) (fst ∘ u) :] ∘ {. prec_st p' r' (snd ∘ u) .} ∘ [: (□ lft_rel_st r') (snd ∘ u) :])"
      by (simp add: comp_assoc [THEN sym])
      also have "... =  local_init (zip_set init init')
        (λu.{. x . prec_st p r (fst ∘ u) x ∧ (∀y. (□ lft_rel_st r) (fst ∘ u) x y ⟶ prec_st p' r' (snd ∘ u) y) .} ∘
            [: (□ lft_rel_st (λ(u, v) (u', v'). r u u' OO r' v v')) u :]) "
         by (simp add: assert_demonic_comp always_lft_rel_comp)
    also have "... = local_init (zip_set init init')
     (λu.{.x. prec_st p r (fst ∘ u) x ∧ (∀y::nat ⇒ 'd. (□ lft_rel_st r) (fst ∘ u) x y ⟶ prec_st p' r' (snd ∘ u) y).} ∘
         [: id (λx::nat ⇒ 'c. id ((□ lft_rel_st (λ(u, v) (u', v'). r u u' OO r' v v')) u x)) :])"
       by simp
    also have "... = ?T"
     by (unfold local_demonic_init, simp add: zip_set_def)
   finally show ?thesis by simp
   qed

  lemma always_lft_rel_comp_a: "(□ lft_rel_st r) u OO (□ lft_rel_st r') v 
              = (□ lft_rel_st (λ (u, v) (u', v') . ((r u u') OO (r' v v')))) (u || v)"
      by (unfold always_lft_rel_comp [THEN sym], auto)


  theorem SymSystem_comp_a: "u' ∈ init' ⟹ SymSystem init p r o SymSystem init' p' r' 
                   = {.x . ∀ u v . u ∈ init ∧ v ∈ init' ⟶ (prec_st p r u x ∧ (∀y. (□ lft_rel_st r) u x y ⟶ prec_st p' r' v y)) .} 
                   o [: x ↝ y . ∃ u v . u ∈ init ∧ v ∈ init' ∧ (□ lft_rel_st (λ(u, v) (u', v'). r u u' OO r' v v')) (u || v) x y :]"
                   (is "?p ⟹ ?S = ?T")
    proof -
      assume A: "u' ∈ init'"
      from A have [simp]: "(λx. (∀u. u ∈ init ⟶ prec_st p r u x) ∧ (∀y. (∃u. u ∈ init ∧ (□ lft_rel_st r) u x y) ⟶ (∀u. u ∈ init' ⟶ prec_st p' r' u y)))
          = (λx. ∀u v. u ∈ init ∧ v ∈ init' ⟶ prec_st p r u x ∧ (∀y. (□ lft_rel_st r) u x y ⟶ prec_st p' r' v y))"
          by (auto simp add: fun_eq_iff)
      have [simp]: "(λx y. ∃u. u ∈ init ∧ (□ lft_rel_st r) u x y) OO (λx y. ∃u. u ∈ init' ∧ (□ lft_rel_st r') u x y) 
        = (λ x y . ∃ u v . u ∈ init ∧ v ∈ init' ∧ (((□ lft_rel_st r) u) OO ((□ lft_rel_st r') v)) x y)"
        by (auto simp add: fun_eq_iff)

      from A have "?S = {.x . ∀u . u ∈ init ⟶ prec_st p r u x.} ∘ 
            [: x ↝ y . ∃u::nat ⇒ 'e. u ∈ init ∧ (□ lft_rel_st r) u x y :] ∘
            ({.x. ∀u . u ∈ init' ⟶ prec_st p' r' u x.} ∘ [: x ↝ y . ∃u . u ∈ init' ∧ (□ lft_rel_st r') u x y :])"
        by (simp add: SymSystem_rel)
       also have "... = {. λx . ∀u . u ∈ init ⟶ prec_st p r u x .} ∘ [: x ↝ y . ∃u . u ∈ init ∧ (□ lft_rel_st r) u x y :] ∘ 
          {. x . ∀u . u ∈ init' ⟶ prec_st p' r' u x .} ∘ [: x ↝ y . ∃u . u ∈ init' ∧ (□ lft_rel_st r') u x y :]"
          by (simp add: comp_assoc [THEN sym])
       also have "... = ?T"
          by (simp add: assert_demonic_comp always_lft_rel_comp_a)
      finally show ?thesis
        by simp
     qed

  text‹We show next that the composition of two SymSystem $S$ and $S'$ is not equal to the SymSystem of the 
  compostion of local transitions of $S$ and $S'$›

  definition "initS = {u . fst (u (0::nat)) = (0::nat)}"
  definition "localPrecS = (⊤:: nat × nat  ⇒ nat × nat ⇒ nat ⇒ bool)"
  definition "localRelS = (λ (u::nat, v) (u', v'::nat) (x::nat) (y::nat) . u = 0 ∧ u' = 1 ∧ v = v')"

  definition "initS' = (⊤::(nat ⇒ (nat × nat)) set)"
  definition "localPrecS' = (⊥:: nat × nat  ⇒ nat × nat ⇒ nat ⇒ bool)"
  definition "localRelS' = (λ (u::nat, v) (u', v'::nat) (x::nat) (y::nat) . u = u')"

  definition "symbS = SymSystem initS localPrecS localRelS"
  definition "symbS' = SymSystem initS' localPrecS' localRelS'"

  definition "localPrecSS' = (λ(u::nat, v::nat) (u', v') (x::nat) . 0 < u)"
  definition "localRelSS' = (λ (u, v::nat) (u'::nat, v'::nat) (x::nat) (z::nat) . (u::nat) = 0 ∧ u' = 1)"

  lemma localSS'_aux: "( λx. ∀ (a::nat) (aa::nat) (b::nat). ¬ (case x of (x::nat, u::nat, v::nat) ⇒ λab. u = 0 ∧ 
    (case ab of (y, u', v') ⇒ u' = Suc 0 ∧ v = v')) (a, aa, b)) 
    = (λ (x, u, v) . u > 0)"
    by (auto simp add: fun_eq_iff)


  lemma localSS'_aux_b: "((λ(x, u, v) ab. u = 0 ∧ (case ab of (y, u', v') ⇒ u' = Suc 0 ∧ v = v')) OO (λ(x, u, v) (y, u', v'). u = u')) 
    = (λ (x, u, v) (y, u', v') . u = 0 ∧ u' = 1)"
    by (simp add: fun_eq_iff relcompp_exists)

  lemma "{.x, (u, v) . localPrecS (u, v) (a,b) x.} o [:x, (u,v) ↝ y, (u',v') . localRelS (u,v) (u',v') x y:] o 
         {.x, (u, v) . localPrecS' (u, v) (c, d) x.} o [:x, (u,v) ↝ y, (u',v') . localRelS' (u,v) (u',v') x y:]
       = {.x, (u, v) . localPrecSS' (u, v) (e, f) x.} o [:x, (u,v) ↝ y, (u',v') . localRelSS' (u,v) (u',v') x y:]"
    by (simp add: assert_demonic_comp localPrecS'_def localPrecS_def localRelS_def localRelS'_def 
      relcompp_exists localPrecSS'_def localRelSS'_def localSS'_aux localSS'_aux_b)

  lemma [simp]: "[: ⊥::('a ⇒ 'b => ('c::boolean_algebra)) :] = ⊤"
    by (simp add: fun_eq_iff demonic_def)

  definition "symbSS' = SymSystem initS localPrecSS' localRelSS'"

  lemma symbSS'_aux: "( λx. ∀u. fst (u 0) = 0 ⟶
                (∀n. (∀i<n. Ex ((case u i of (u, v) ⇒ λ(u', v'::nat) x z. u = 0 ∧ u' = Suc 0) (u (Suc i)) (x i))) 
                ⟶ (case u n of (u, v) ⇒ λ(u', v') x. 0 < u) (u (Suc n)) (x n)) ) = ⊥"
    apply (auto simp add: fun_eq_iff)
    by (rule_tac x = "λ i . (i::nat, i)" in exI, simp)

  lemma symbSS': "symbSS' = ⊥"
    by (simp add: symbSS'_def SymSystem_rel initS_def localPrecSS'_def localRelSS'_def prec_st_simp inpt_st_def symbSS'_aux)

  lemma symbS: "symbS = ⊤"
    proof (simp add: symbS_def SymSystem_rel initS_def localPrecS_def localRelS_def)
      have [simp]: "(λx. ∀u. fst (u 0) = 0 ⟶ prec_st ⊤ (λ (u, v) (u', v') x y . u = 0 ∧ u' = Suc 0 ∧ v = v') u x) = ⊤"
        by (simp_all add: fun_eq_iff prec_st_def always_def lft_rel_st_def at_fun_def lft_pred_st_def inpt_st_def until_def)
  
    have [simp]: "(λx y. ∃u. fst (u 0) = 0 ∧ (□ lft_rel_st (λ (u, v) (u', v') (x) (y). u = 0 ∧ u' = Suc 0 ∧ v = v')) u x y) = ⊥"
      proof (auto simp add: fun_eq_iff always_def lft_rel_st_def at_fun_def)
      fix x::"nat ⇒ 'a" and xa :: "nat ⇒ 'b" and u::"nat ⇒ nat × 'c"
      assume A: "∀a . (case u a of (e, f) ⇒ λ(u', v') x y. e = 0 ∧ u' = Suc 0 ∧ f = v') (u (Suc a)) (x a) (xa a)" 
      {fix n:: nat
        from A have "fst (u n) = 0 ∧ fst (u (Suc n)) = Suc 0"
          by (drule_tac x = n in spec, case_tac "u n", case_tac "u (Suc n)", auto)
      }
      note B = this
      then have "fst (u (Suc 0)) =  0" by auto
      moreover have "fst (u (Suc 0)) =  Suc 0" using B [of 0] by auto
      ultimately show "(0) < fst (u (0))" by auto
    qed

    show "{. λx. ∀u. fst (u 0) = 0 ⟶ prec_st ⊤ (λ(u, v) (u', v') x y. u = 0 ∧ u' = Suc 0 ∧ v = v') u x .} ∘
            [: λ x y . ∃u . fst (u 0) = 0 ∧ (□ lft_rel_st (λ(u, v) (u', v') x y. u = 0 ∧ u' = Suc 0 ∧ v = v')) u x y :] =
            ⊤"
      by simp
    qed

  lemma "symbS o symbS' ≠ symbSS'"
    by (simp add: symbSS' symbS fun_eq_iff)

  lemma prec_st_inpt: "prec_st (inpt_st r) r = (□ (lft_pred_st (inpt_st r)))"
    by (simp add: prec_st_def neg_until_always)

  lemma "grd (SymSystem init p r) = Sup ((- prec_st p r ⊔ (□ (lft_pred_st (inpt_st r)))) ` init)"
    proof (unfold fun_eq_iff, auto simp add: grd_def SymSystem_rel demonic_def assert_def)
      fix x :: "nat ⇒ 'a" and  xa :: "nat ⇒ 'b" and  u :: "nat ⇒ 'c"
      assume "∀xa::nat ⇒ 'c∈init. prec_st p r xa x ∧ ¬ (□ lft_pred_st (inpt_st r)) xa x"
      and "u ∈ init"
      and "(□ lft_rel_st r) u x xa"
      then show "False"
        by (auto simp add: always_def lft_pred_st_def inpt_st_def at_fun_def lft_rel_st_def)
    next
      fix x :: "nat ⇒ 'a" and  xa :: "nat ⇒ 'c"
      assume B: "xa ∈ init"
      assume "(λy . ∃u . u ∈ init ∧ (□ lft_rel_st r) u x y) ≤ ⊥"
      then have A: "∀ y u . u ∉ init ∨ ¬ (□ lft_rel_st r) u x y"
        by auto
      let ?y = "λ n . (SOME z . r (xa n) (xa (Suc n)) (x n) z)"
      from B and A have "¬ (□ lft_rel_st r) xa x ?y" by simp
      moreover assume "(□ lft_pred_st (inpt_st r)) xa x"
      ultimately show "False"
        apply (simp add: always_def lft_pred_st_def inpt_st_def at_fun_def lft_rel_st_def)
        by (metis (full_types) tfl_some)
   qed

 
  definition "guard S = {.((grd S)::'a⇒bool).} o S"

  lemma "((grd (local_init init S))::'a⇒bool) = Sup ((grd o S) ` init)"
    by (simp add: fun_eq_iff local_init_def assert_def grd_def)

  lemma "u ∈ init ⟹ guard ([:z ↝ u, x . u ∈ init ∧ z = x:] o {.u, x . p u x.} o [:u, x ↝ y . r u x y :])
      = [:z ↝ u, x . u ∈ init ∧ z = x:] o {.u, x . u ∈ init ∧ (∃a. a ∈ init ∧ (p a x ⟶ Ex (r a x))) ∧ p u x.} o [:u, x ↝ y . ((r u x y)::bool) :]"
    by (auto simp add: fun_eq_iff local_init_def guard_def grd_def assert_def demonic_def le_fun_def)

  lemma inpt_str_comp_aux: "(∀n. (∀i<n. inpt_st (λ(u, v) (u', v'). r u u' OO r' v v') (u i) (u (Suc i)) (x i)) ⟶
        inpt_st r (fst (u n)) (fst (u (Suc n))) (x n) ∧ (∀y. r (fst (u n)) (fst (u (Suc n))) (x n) y ⟶ inpt_st r' (snd (u n)) (snd (u (Suc n))) y)) ⟶
        (∀ i < n . inpt_st r ((fst o u) i) ((fst o u) (Suc i)) (x i) ∧ (∀y. r (fst (u i)) (fst (u (Suc i))) (x i) y ⟶ inpt_st r' (snd (u i)) (snd (u (Suc i))) y))"
        (is "(∀ n . ?p n) ⟶ ?q n")
    proof (induction n)
      case 0
      show ?case by auto
    next
      case (Suc n)
      show ?case
        proof auto
          fix i::nat
          assume B: "∀ n . ?p n"
          then have A: "?p n" (is "?A ⟶ ?B")
               by simp
          from Suc and B have C: "?q n"
            by simp
          assume "i < Suc n"
          then show "inpt_st r (fst (u i)) (fst (u (Suc i))) (x i)"
            proof cases
              assume "i < n"
              then show ?thesis
                by (metis Suc.IH B comp_apply)
           next
             assume "¬ i < n"
             from this and ‹i < Suc n› have [simp]: "i = n" by simp
             show ?thesis
               proof cases
                assume "?A"
                from this and A have D: "?B" by simp
                from D show ?thesis
                  by (metis ‹i = n›)
              next
                assume "¬ ?A"
                then obtain j where j: "j < n ∧ ¬ inpt_st (λ (u, v) . λ (u', v') . r u u' OO r' v v') (u j) (u (Suc j)) (x j)"
                  by auto
                with C have "inpt_st r (fst (u j)) (fst (u (Suc j))) (x j) ∧ (∀y. r (fst (u j)) (fst (u (Suc j))) (x j) y ⟶ inpt_st r' (snd (u j)) (snd (u (Suc j))) y)"
                  by auto
                with j show ?thesis
                  apply (case_tac "u j")
                  apply (case_tac "u (Suc j)")
                  apply (simp add: inpt_st_def)
                  by (metis relcompp.relcompI)
              qed
         qed
     next
          fix i::nat fix y :: 'e
          assume B: "∀ n . ?p n"
          then have A: "?p n" (is "?A ⟶ ?B")
               by simp
          from Suc and B have C: "∀i<n. inpt_st r (fst (u i)) (fst (u (Suc i))) (x i) ∧ (∀y. r (fst (u i)) (fst (u (Suc i))) (x i) y ⟶ inpt_st r' (snd (u i)) (snd (u (Suc i))) y)"
            by simp
          assume E: "r (fst (u i)) (fst (u (Suc i))) (x i) y"
          assume "i < Suc n"
          then show "inpt_st r' (snd (u i)) (snd (u (Suc i))) y"
            proof cases
              assume "i < n"
              from this and E and C show ?thesis
                by simp
           next
             assume "¬ i < n"
             from this and ‹i < Suc n› have [simp]: "i = n" by simp
             show ?thesis
               proof (cases ?A)
                case True
                with A have D: "?B" by simp
                from D and E show ?thesis
                  by (metis ‹i = n›)
              next
                case False
                then obtain j where j: "j < n ∧ ¬ inpt_st (λ (u, v) . λ (u', v') . r u u' OO r' v v') (u j) (u (Suc j)) (x j)"
                  by auto
                with C have "inpt_st r (fst (u j)) (fst (u (Suc j))) (x j) ∧ (∀y. r (fst (u j)) (fst (u (Suc j))) (x j) y ⟶ inpt_st r' (snd (u j)) (snd (u (Suc j))) y)"
                  by auto
                with j show ?thesis
                  by (case_tac "u j", case_tac "u (Suc j)", simp add: inpt_st_def, metis relcompp.relcompI)
              qed
         qed
     qed
  qed
                     
  lemma inpt_str_comp_aux_a: "(∀n. (∀i<n. inpt_st (λ(u, v) (u', v'). r u u' OO r' v v') (u i) (u (Suc i)) (x i)) ⟶
        inpt_st r (fst (u n)) (fst (u (Suc n))) (x n) ∧ (∀y. r (fst (u n)) (fst (u (Suc n))) (x n) y ⟶ inpt_st r' (snd (u n)) (snd (u (Suc n))) y)) ⟹
        inpt_st r ((fst o u) n) ((fst o u) (Suc n)) (x n) ∧ (∀y. r (fst (u n)) (fst (u (Suc n))) (x n) y ⟶ inpt_st r' (snd (u n)) (snd (u (Suc n))) y)"
    by (cut_tac n = "Suc n" and r = r and r' = r' and u = u and x = x in inpt_str_comp_aux, simp)

  definition "rel_st r r' = (λ (u, v) (u', v') x z . inpt_st r u u' x ∧ (∀ y . r u u' x y ⟶ inpt_st r' v v' y) ∧ (r u u' OO r' v v') x z)"

  lemma inpt_str_comp_a: "(prec_st (inpt_st r) r (fst ∘ u) x ∧ (∀y. (□ lft_rel_st r) (fst ∘ u) x y ⟶ prec_st (inpt_st r') r' (snd ∘ u) y)) = 
    prec_st (λ u u' x . inpt_st r (fst u) (fst u') x ∧ (∀ y . r (fst u) (fst u') x y ⟶ (inpt_st r' (snd u) (snd u') y))) (λ(u, v) (u', v'). r u u' OO r' v v') u x"
    proof (auto simp add: prec_st_inpt prec_st_simp)
      fix n:: nat
      assume "(□ lft_pred_st (inpt_st r)) (fst ∘ u) x"
      then show "inpt_st r (fst (u n)) (fst (u (Suc n))) (x n)"
        by (simp add: always_def lft_pred_st_def at_fun_def)
    next
      fix n:: nat and y :: 'c
      assume A: "(□ lft_pred_st (inpt_st r)) (fst ∘ u) x"
      assume B: "r (fst (u n)) (fst (u (Suc n))) (x n) y"
      assume C: "∀i<n. inpt_st (λ(u::'a, v::'d) (u'::'a, v'::'d). r u u' OO r' v v') (u i) (u (Suc i)) (x i)"
      let ?y = "λ i . (if i = n then y else (SOME y . r ((fst o u) i) ((fst o u) (Suc i)) (x i) y))"
      assume "∀y . (□ lft_rel_st r) (fst ∘ u) x y ⟶ (□ lft_pred_st (inpt_st r')) (snd ∘ u) y"
      then have D: "(□ lft_rel_st r) (fst ∘ u) x ?y ⟶ (□ lft_pred_st (inpt_st r')) (snd ∘ u) ?y"
        by simp
      from A and B have E: "(□ lft_rel_st r) (fst ∘ u) x ?y"
        apply (auto simp add: always_def at_fun_def lft_rel_st_def lft_pred_st_def inpt_st_def)
        by (metis tfl_some)
      from D and E have "(□ lft_pred_st (inpt_st r')) (snd ∘ u) ?y" by simp

      from A and E and this show "inpt_st r' (snd (u n)) (snd (u (Suc n))) y"
        apply (simp add: always_def lft_pred_st_def at_fun_def)
        apply (drule_tac x = n in spec)
        apply (drule_tac x = n in spec)
        by (drule_tac x = n in spec, simp)
    next
      assume "∀ n . (∀i<n. inpt_st (λ(u::'a, v::'d) (u'::'a, v'::'d). r u u' OO r' v v') (u i) (u (Suc i)) (x i)) ⟶
            inpt_st r (fst (u n)) (fst (u (Suc n))) (x n) ∧ (∀y::'c. r (fst (u n)) (fst (u (Suc n))) (x n) y ⟶ inpt_st r' (snd (u n)) (snd (u (Suc n))) y)"
      then show "(□ lft_pred_st (inpt_st r)) (fst ∘ u) x"
        apply (auto simp add: always_def lft_pred_st_def at_fun_def)
        apply (drule inpt_str_comp_aux_a)
        by auto
   next
      fix y::"nat ⇒ 'c"
      assume "∀ n . (∀i<n. inpt_st (λ(u::'a, v::'d) (u'::'a, v'::'d). r u u' OO r' v v') (u i) (u (Suc i)) (x i)) ⟶
            inpt_st r (fst (u n)) (fst (u (Suc n))) (x n) ∧ (∀y::'c. r (fst (u n)) (fst (u (Suc n))) (x n) y ⟶ inpt_st r' (snd (u n)) (snd (u (Suc n))) y)"
      moreover assume " (□ lft_rel_st r) (fst ∘ u) x y"
      ultimately show "(□ lft_pred_st (inpt_st r')) (snd ∘ u) y"
        apply (auto simp add: always_def lft_pred_st_def at_fun_def)
        apply (drule inpt_str_comp_aux_a)
        by (auto simp add:  lft_rel_st_def)
   qed

  lemma inpt_str_comp_b: "prec_st (λ u u' x . inpt_st r (fst u) (fst u') x ∧ 
    (∀ y . r (fst u) (fst u') x y ⟶ (inpt_st r' (snd u) (snd u') y))) (λ(u, v) (u', v'). r u u' OO r' v v') u x
    =  (□ (lft_pred_st (inpt_st (rel_st r r')))) u x"
    proof (auto simp add: prec_st_simp always_def lft_pred_st_def at_fun_def rel_st_def)
      fix m::nat
      assume A: "∀n . (∀i<n. inpt_st (λ(u, v) (u', v'). r u u' OO r' v v') (u i) (u (Suc i)) (x i)) ⟶
                      inpt_st r (fst (u n)) (fst (u (Suc n))) (x n) 
                      ∧ (∀y. r (fst (u n)) (fst (u (Suc n))) (x n) y ⟶ inpt_st r' (snd (u n)) (snd (u (Suc n))) y)" (is "∀ n . ?p n ⟶ ?q n ∧ ?r n")
      then have "?q m" 
        by (drule_tac n = m in inpt_str_comp_aux_a, simp)
      then obtain y where B: "r ((fst ∘ u) m) ((fst ∘ u) (Suc m)) (x m) y" by (auto simp add: inpt_st_def)
      from A have "?r m"
        by (drule_tac n = m in inpt_str_comp_aux_a, simp)
      from this B show "inpt_st (λ(u, v) (u', v') (x::'c) z. inpt_st r u u' x ∧ (∀y. r u u' x y 
          ⟶ inpt_st r' v v' y) ∧ (r u u' OO r' v v') x z) (u m) (u (Suc m)) (x m)"
      apply (case_tac "u m")
      apply (case_tac "u (Suc m)")     
      apply (simp add: inpt_st_def)
      by (metis relcompp.relcompI)
    next
      fix m::nat
      assume " ∀ m. inpt_st (λ(u, v) (u', v') (x) z. inpt_st r u u' x ∧ (∀y. r u u' x y ⟶ inpt_st r' v v' y) 
          ∧ (r u u' OO r' v v') x z) (u m) (u (Suc m)) (x m)" (is "∀ m . ?p m")
      then have "?p m" by simp
      then show " inpt_st r (fst (u m)) (fst (u (Suc m))) (x m)"
        apply (simp add: inpt_st_def)
        by (case_tac "u m", case_tac "u (Suc m)", simp)
    next
      fix m::nat and y :: 'e
      assume " ∀ m. inpt_st (λ(u, v) (u', v') (x) z. inpt_st r u u' x ∧ (∀y. r u u' x y ⟶ inpt_st r' v v' y) 
          ∧ (r u u' OO r' v v') x z) (u m) (u (Suc m)) (x m)" (is "∀ m . ?p m")
      then have "?p m" by simp
      moreover assume "r (fst (u m)) (fst (u (Suc m))) (x m) y"
      ultimately show " inpt_st r' (snd (u m)) (snd (u (Suc m))) y"
        apply (simp add: inpt_st_def)
        by (case_tac "u m", case_tac "u (Suc m)", simp)
    qed

  lemma inpt_str_comp: "(prec_st (inpt_st r) r (fst ∘ u) x ∧ (∀y. (□ lft_rel_st r) (fst ∘ u) x y ⟶ prec_st (inpt_st r') r' (snd ∘ u) y)) 
               = (□ (lft_pred_st (inpt_st (rel_st r r')))) u x"
    by (simp add: inpt_str_comp_a inpt_str_comp_b)

  lemma RSysTmp_inpt_comp: "u' ∈ init' ⟹ SymSystem init (inpt_st r) r o SymSystem init'(inpt_st r') r' 
      =  SymSystem (zip_set init init') (inpt_st (rel_st r r')) (rel_st r r')"
    proof -
      assume A : "u' ∈ init'"
      have [simp]: "( λx y. (case x of (x, xa) ⇒ (□ lft_pred_st (inpt_st (rel_st r r'))) x xa) ∧ 
        (case x of (x, xa) ⇒ (□ lft_rel_st (λ(u, v) (u', v'). r u u' OO r' v v')) x xa) y)
        =  (λ(x, y). (□ lft_rel_st (rel_st r r')) x y)" (is "?a = ?b")
        proof (auto simp add: fun_eq_iff always_def at_fun_def lft_pred_st_def lft_rel_st_def rel_st_def inpt_st_def)
          fix a :: "nat ⇒ 'e × 'a" and  b :: "nat ⇒ 'c" and  x :: "nat ⇒ 'b" and  xa :: nat
          assume "∀xa::nat. (case a xa of (u::'e, v::'a) ⇒ λ(u'::'e, v'::'a). r u u' OO r' v v') (a (Suc xa)) (b xa) (x xa)" (is "∀ xa . ?P xa")
          then have A: "?P xa" by simp
          assume "∀x . Ex ((case a x of (u, v) ⇒ λ(u', v') (x) z. Ex (r u u' x) ∧ (∀y. r u u' x y ⟶ Ex (r' v v' y)) ∧ (r u u' OO r' v v') x z) (a (Suc x)) (b x))" (is "∀ xa . ?Q xa")
          then have "?Q xa" by simp
          from this and A show "(case a xa of (u, v) ⇒ λ(u', v') (x) z. Ex (r u u' x) ∧ (∀y. r u u' x y ⟶ Ex (r' v v' y)) ∧ (r u u' OO r' v v') x z) (a (Suc xa)) (b xa) (x xa)"
            by (case_tac "a xa", case_tac "a (Suc xa)", simp)
        next
          fix a :: "nat ⇒ 'e × 'a" and  b :: "nat ⇒ 'c" and  x :: "nat ⇒ 'b" and xa :: nat
          assume "∀xa . (case a xa of (u::'e, v::'a) ⇒ λ(u'::'e, v'::'a) (x::'c) z::'b. Ex (r u u' x) ∧ (∀y::'d. r u u' x y ⟶ Ex (r' v v' y)) ∧ (r u u' OO r' v v') x z) (a (Suc xa)) (b xa) (x xa)" (is "∀ xa . ?Q xa")
          then have "?Q xa" by simp
          then show "(case a xa of (u::'e, v::'a) ⇒ λ(u'::'e, v'::'a). r u u' OO r' v v') (a (Suc xa)) (b xa) (x xa)"
          by (case_tac "a xa", case_tac "a (Suc xa)", simp)
        qed
      
     from A have "SymSystem init (inpt_st r) r o SymSystem init'(inpt_st r') r' = [: z ↝ u, x . fst ∘ u ∈ init ∧ snd ∘ u ∈ init' ∧ z = x :] ∘
      ({.u, x . prec_st (inpt_st r) r (fst ∘ u) x ∧ (∀y::nat ⇒ 'd. (□ lft_rel_st r) (fst ∘ u) x y ⟶ prec_st (inpt_st r') r' (snd ∘ u) y).} ∘
      [:  (λ(u, x).  ((□ lft_rel_st (λ(u, v) (u', v'). r u u' OO r' v v')) u x)) :])"
      by (unfold SymSystem_comp, simp add: comp_assoc)
      also have "... = [: z ↝ u, x . fst ∘ u ∈ init ∧ snd ∘ u ∈ init' ∧ z = x :] ∘ ({. x, y . (□ lft_pred_st (inpt_st (rel_st r r'))) x y .} ∘ [: ?b :])"
          by (subst assert_demonic, simp add: inpt_str_comp)
      also have "... = SymSystem (zip_set init init') (inpt_st (rel_st r r')) (rel_st r r')"
        by (simp add: SymSystem_def prec_st_inpt comp_assoc zip_set_def)
      finally show ?thesis by simp
    qed

  definition "GrdSymSystem init r = [:z ↝ u, x . u ∈ init ∧ z = x:] o trs (λ (u, x) y . (□(lft_rel_st r)) u x y)"

  lemma inpt_always: "inpt (λ(x, y). (□ lft_rel_st r) x y) = (λ(x, y). (□ lft_pred_st (inpt_st r)) x y)"
    proof (auto simp add: fun_eq_iff)
    fix a :: "nat ⇒ 'a" and  b :: "nat ⇒ 'b"
    assume "inpt (λ(x, y).(□ lft_rel_st r) x y) (a, b)"
    then show "(□ lft_pred_st (inpt_st r)) a b"
      by (auto simp add: inpt_def lft_pred_st_def inpt_st_def always_def at_fun_def lft_rel_st_def)
    next
      fix a :: "nat ⇒ 'a" and  b :: "nat ⇒ 'b"
      let ?y = "λ n . (SOME y . r (a n) (a (Suc n)) (b n) y)"
      assume "(□ lft_pred_st (inpt_st r)) a b"
      then have "(□ lft_rel_st r) a b ?y"
        apply (auto simp add: always_def at_fun_def lft_rel_st_def inpt_st_def lft_pred_st_def)
        by (metis tfl_some)
      then show "inpt (λ(x, y). (□ lft_rel_st r) x y) (a, b)"
        by (auto simp add: inpt_def)
    qed

  lemma "GrdSymSystem init r = SymSystem init (inpt_st r) r"
    by (simp add: GrdSymSystem_def SymSystem_def trs_def  prec_st_inpt comp_assoc inpt_always)

  subsection‹Example: COUNTER›
  text‹
    In this section we introduce an example counter that counts how many times
    the input variable $x$ is true. The input is a sequence of boolen values
    and the output is a sequence of natural numbers. The output at some moment in 
    time is the number of true values seen so far in the input.

    We defined the system counter in two different ways and we show that the
    two definitions are equivalent. The first definition takes the entire 
    input sequence and it computes the corresponding output sequence. We introduce
    the second version of the counter as a reactive system based on a symbolic
    transition system. We use a local variable to record the number of true
    values seen so far, and initially the local variable is zero. At every step
    we increase the local variable if the input is true. The output of the
    system at every step is equal to the local variable.
›

  primrec count :: "bool trace ⇒ nat trace" where
    "count x 0 = (if x 0 then 1 else 0)" |
    "count x (Suc n) = (if x (Suc n) then count x n + 1 else count x n)"

  definition "Counter_global n = {.x . (∀ k . count x k ≤ n).} o [:x ↝ y . y = count x:]"

  definition "prec_count M u u' x = (u ≤ M)"
  definition "rel_count u u' x y = ((x ⟶ u' = Suc u) ∧ (¬ x ⟶ u' = u) ∧ y = u')"

  lemma counter_a_aux: "u 0 = 0 ⟹ ∀i < n. (x i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ x i ⟶ u (Suc i) = u i) ⟹ (∀ i < n . count x i = u (Suc i))"
      proof (induction n)
        case 0
        show ?case by simp
      next
        case (Suc n)
        {fix j::nat
          assume "∀i<Suc n. (x i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ x i ⟶ u (Suc i) = u i)"
          and "j < Suc n"
          and "u (0::nat) = (0::nat)"
          from this and Suc have "count x j = u (Suc j)"
            by (case_tac j, auto)
        }
        from Suc and this show ?case 
          by auto
      qed

  lemma counter_b_aux: "u 0 = 0 ⟹ ∀n. (xa n ⟶ u (Suc n) = Suc (u n)) ∧ (¬ xa n ⟶ u (Suc n) = u n) ∧ xb n = u (Suc n) 
                ⟹ count xa n = u (Suc n)"
    by (induction n, simp_all)

  definition "COUNTER M = SymSystem {u . u 0 = 0} (prec_count M) rel_count"

  lemma "COUNTER = Counter_global"
    proof -
      have A:"(λx y . ∃u::nat ⇒ nat. u (0::nat) = (0::nat) ∧ (□ lft_rel_st rel_count) u x y)
        = (λ x y . y = count x)"
        proof (simp add: fun_eq_iff lft_rel_st_def rel_count_def always_def at_fun_def, safe)
          fix x :: "nat ⇒ bool" and  xa :: "nat ⇒ nat" and u:: "nat ⇒ nat" and xb :: nat
          assume A: "u 0 = 0"
          assume B: "∀xb . (x xb ⟶ u (Suc xb) = Suc (u xb)) ∧ (¬ x xb ⟶ u (Suc xb) = u xb) ∧ xa xb = u (Suc xb)"
          from A and this have "count x xb = xa xb"
             by (drule_tac counter_b_aux, auto)
          then show "xa xb = count x xb" by simp
        next
          fix x::"nat ⇒ bool" and xa::"nat ⇒ nat"
          define u where "u i = (if i = 0 then 0 else count x (i - 1))" for i
          assume B: "∀xb::nat. xa xb = count x xb"
          {fix xb::nat
          from u_def and B have "u 0 = 0 ∧ ( (x xb ⟶ u (Suc xb) = Suc (u xb)) ∧ (¬ x xb ⟶ u (Suc xb) = u xb) ∧ xa xb = u (Suc xb))"
            by (case_tac xb, auto)
          }
          then show "∃u::nat ⇒ nat. u 0 = 0 ∧ (∀xb. (x xb ⟶ u (Suc xb) = Suc (u xb)) ∧ (¬ x xb ⟶ u (Suc xb) = u xb) ∧ 
              xa xb = u (Suc xb))"
          by auto
       qed
      {fix x :: nat
        have "(λxa . ∀u . u (0::nat) = (0::nat) ⟶ prec_st (prec_count x) rel_count u xa) = 
          (λxa::nat ⇒ bool. ∀k::nat. count xa k ≤ x)"
        proof (simp add: fun_eq_iff lft_rel_st_def  prec_st_def until_def 
            lft_pred_st_def prec_count_def at_fun_def inpt_st_def rel_count_def, safe)
          fix xa::"nat ⇒ bool" and k:: nat
          define uu where "uu i = (if i = 0 then 0 else count xa (i - 1))" for i
          assume "(∀u . u 0 = 0 ⟶ (∀xb . (∃x<xb. xa x ∧ u (Suc x) ≠ Suc (u x) ∨ ¬ xa x ∧ u (Suc x) ≠ u x) ∨ u xb ≤ x))" (is "∀ u . ?s u")
          then have "?s uu" (is "?p ⟶ (∀xb . (∃ x < xb . ?q xb x) ∨ ?r xb)")
            by auto
          from this and uu_def  have "(∀xb . (∃ x < xb . ?q xb x) ∨ ?r xb)"
            by simp
          then have "(∃ x < (Suc k) . ?q (Suc k) x) ∨ ?r (Suc k)"
            by simp
          then obtain xb where "xb < (Suc k) ∧ (?q (Suc k) xb ∨ ?r (Suc k))"
            by auto
          from this and uu_def show "count xa k ≤ x"
             by (case_tac xb, auto)
        next 
          fix xa:: "nat ⇒ bool" and  u::"nat ⇒ nat" and xaa::nat
          assume C: "∀k::nat. count xa k ≤ x"
          assume A: "u (0::nat) = (0::nat)"
          assume B: "¬ u xaa ≤ x"
          from A and B have D: "xaa > 0"
            by (metis le0 neq0_conv)
          from this and B and C have "count xa (xaa - 1) ≠ u xaa"
            by metis
          from this and D have E: "∃i < xaa. count xa i ≠ u (Suc i)"
            by (metis One_nat_def Suc_diff_1 diff_Suc_less)
          have "u 0 = 0 ⟹ ∀i<xaa. (xa i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ xa i ⟶ u (Suc i) = u i) ⟹ ∀i<xaa. count xa i = u (Suc i)"
            by (rule counter_a_aux, simp)
          from this and A and E show "(∃x<xaa. xa x ∧ u (Suc x) ≠ Suc (u x) ∨ ¬ xa x ∧ u (Suc x) ≠ u x)"
            by auto
        qed
        }
      note B = this
     show ?thesis
      by (simp add: fun_eq_iff COUNTER_def SymSystem_rel Counter_global_def A B)

   qed
 

  subsection‹Example: LIVE›

  text‹
    The last example of this formalization introduces a system which does some
    local computation, and ensures some global liveness property.
    We show that this example is the fusion of a symbolic transition system and a demonic
    choice which ensures the liveness property of the output sequence.
    We also show that asumming some liveness property for the input, we can refine
    the example into an executable system that does not ensure the liveness
    property of the output on its own, but relies on the liveness of the input.
›

  definition "rel_ex u u' x y = (((x ∧ u' = u + (1::int)) ∨ (¬ x ∧ u' = u - 1) ∨ u' = 0) ∧ (y = (u' = 0)))"
  definition "prec_ex u u' x = (-1 ≤ u ∧ u ≤ 3)"

  definition "LIVE = [:x ↝ u, x' . u (0::nat) = 0 ∧ x = x':] o {.u, x . prec_st prec_ex rel_ex u x.} 
    o [:u, x ↝ y . (□(λ u x y . rel_ex (u 0) (u 1) (x 0) (y 0))) u x y  ∧ (□ (◇ (λ y . y 0))) y :]"

  lemma LIVE_fusion: "LIVE = (SymSystem {u . u 0 = 0} prec_ex rel_ex) ∥ [:x ↝ y . (□ (◇ (λ y . y 0))) y:]"
    proof -
      define init where "init = {u . u (0::nat) = (0::int)}"
      then have A: "(λ i::nat . 0::int) ∈ init"
        by simp
      then have "([: x ↝ (u, y). u ∈ init ∧ x = y :] ∘ {.(x, y). prec_st prec_ex rel_ex x y .} ∘ [: λ(x, y). (□ lft_rel_st rel_ex) x y :]) ∥
          [: λx. □ ◇ (λy. y 0) :] =
          [: x ↝ (u, y). u ∈ init ∧ x = y :] ∘ {. (x, y). prec_st prec_ex rel_ex x y .} ∘
          [: (u, x) ↝ y. (□ lft_rel_st rel_ex) u x y ∧ (□ ◇ (λy. y 0)) y :]"
        by (unfold fusion_spec_local_a, auto)
      then show ?thesis 
        by (simp add: init_def SymSystem_def)
          (auto simp add: LIVE_def lft_rel_st_def always_def at_fun_def)
   qed

  definition "preca_ex x = (x 1 = (¬x 0))"

  lemma monotonic_SymSystem[simp]: "mono (SymSystem init p r)"
    by (simp add: SymSystem_def)

  lemma event_ex_aux_a: "a 0 = (0::int) ⟹ ∀n. xa (Suc n) = (¬ xa n) ⟹ 
        ∀n. (xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0) ⟹ 
        (a n = -1 ⟶ xa n) ∧ (a n = 1 ⟶ ¬ xa n) ∧ -1 ≤ a n ∧ a n ≤ 1"
    proof (induction n)
      case 0
      show ?case
        by (metis "0.prems"(1) le_minus_one_simps(1) minus_zero zero_le_one zero_neq_neg_one)
    next
      case (Suc n)
      {assume "a (Suc n) = - (1::int)" from this and Suc have "xa (Suc n)"
        by (metis add.commute add_le_same_cancel2 not_one_le_zero zero_neq_neg_one)}
      note A = this
      {assume "a (Suc n) = (1::int)" and "xa (Suc n)" from this and Suc have "False"
        by (metis eq_iff le_iff_diff_le_0 not_one_le_zero)}
      note B = this
      {assume "a n ≠ - (1::int)" from this and Suc have " - (1::int) ≤ a (Suc n)" 
         by (metis add.commute monoid_add_class.add.left_neutral le_less not_le right_minus uminus_add_conv_diff zle_add1_eq_le)}
      note C = this
      {assume "a n = - (1::int)" from this and Suc have " - (1::int) ≤ a (Suc n)"
        by (metis add.commute le_minus_one_simps(4) monoid_add_class.add.right_neutral not_le right_minus zle_add1_eq_le)}
      note D = this
      from C and D and Suc have  E: " - (1::int) ≤ a (Suc n)" by auto
      from Suc have F: "a (Suc n) ≤ (1::int)"
        by (metis eq_iff int_one_le_iff_zero_less le_iff_diff_le_0 le_less not_le zle_add1_eq_le)
      from A B E F show ?case by auto
    qed

  lemma event_ex_aux: "a 0 = (0::int) ⟹ ∀n. xa (Suc n) = (¬ xa n) ⟹ 
         ∀n. (xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0) ⟹ 
        (∀ n . (a n = -1 ⟶ xa n) ∧ (a n = 1 ⟶ ¬ xa n) ∧ -1 ≤ a n ∧ a n ≤ 1)"
    by (clarify, drule event_ex_aux_a, auto)

  lemma "{.□ preca_ex.} o LIVE ≤ SymSystem {u . u 0 = 0} prec_ex rel_ex"
    proof (unfold LIVE_fusion SymSystem_def, rule fusion_local_refinement, simp_all)
      fix z::"nat ⇒ bool" and u :: "nat ⇒ int" and x::"nat ⇒ bool"
      assume A: "u 0 = 0"
      assume "(□ preca_ex) z"
      then have B: "∀x::nat. z (Suc x) = (¬ z x)"  
        by (auto simp add: preca_ex_def lft_rel_st_def rel_ex_def always_def at_fun_def)
      assume "(□ lft_rel_st rel_ex) u z x"
      then have C: "∀xa . (z xa ∧ u (Suc xa) = u xa + 1 ∨ ¬ z xa ∧ u (Suc xa) = u xa - 1 ∨ u (Suc xa) = 0) ∧ x xa = (u (Suc xa) = 0)"
        by (auto simp add: preca_ex_def lft_rel_st_def rel_ex_def always_def at_fun_def)
      have D: "(∀ n . (u n = -1 ⟶ z n) ∧ (u n = 1 ⟶ ¬ z n) ∧ -1 ≤ u n ∧ u n ≤ 1)"
        by (cut_tac A B C, rule event_ex_aux, auto)
      {
          fix a::nat
          {assume "u (Suc a) = 0" from this A B C have "∃b . u (Suc (a + b)) = 0"
            by (metis monoid_add_class.add.right_neutral)}
          note 1 = this
          {assume "u (Suc a) = -1" from this A B C D have "∃b . u (Suc (a + b)) = 0" 
            by (metis add_Suc_right diff_minus_eq_add diff_self monoid_add_class.add.right_neutral)}
          note 2 = this
          {assume "u (Suc a) = 1" from this A B C D have "∃b . u (Suc (a + b)) = 0" 
            by (metis add_Suc_right diff_self monoid_add_class.add.right_neutral)}
          note 3 = this
          from 1 2 3 A B C D have "∃b . x (a + b)"
            by (simp, metis diff_0 int_one_le_iff_zero_less le_less not_le zle_diff1_eq)
      }
      then show "(□ ◇ (λy . y 0)) x"
        by (simp add: always_def eventually_def preca_ex_def at_fun_def rel_ex_def lft_rel_st_def)
   qed
  end