Theory RefinementReactive

theory RefinementReactive
imports Temporal Refinement
section{*\label{sec_RefinementReactive}Monotonic Property Transformers*}

theory RefinementReactive
  imports Temporal Refinement
begin
  (*declare [[show_types]]*)

  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 "illegal_sts init p r x = (∃ n u y . init (u 0) ∧ (∀ i < n . r (u i, x i) (u (Suc i), y i)) ∧ (¬ p (u n, x n)))"
definition "run_sts r u x y = (∀ i . r (u i, x i) (u (Suc i), y i))"

(*todo: find better name. It is pre_sts in Algorithms*)  
definition "LocalSystem init p r q x = (¬ illegal_sts init p r x ∧ (∀ u y . (init (u 0) ∧ run_sts r u x y) ⟶ q y))"

lemma LocalSystem_not_fail_run: "LocalSystem init p r = {.- illegal_sts init p r.} o [:x ↝ y . ∃ u . init (u 0) ∧ run_sts r u x y:]"
  by (simp add: fun_eq_iff LocalSystem_def demonic_def assert_def le_fun_def, auto)
 
definition "fail_sys_delete 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_delete r u x y = (∀ i . r (u i) (u (Suc i)) (x i) (y i))"
  
definition "LocalSystem_delete init p r q x = (¬ fail_sys_delete init p r x ∧ (∀ u y . (u ∈ init ∧ run_delete r u x y) ⟶ q y))"

(*  
lemma LocalSystem_delete_simp: "LocalSystem_delete init p r = {.-fail_sys_delete init p r.} o [:x ↝ y . (∃ u ∈ init . run_delete r u x y):]"
  by (simp add: LocalSystem_delete_def fun_eq_iff demonic_def assert_def le_fun_def, auto)
*)
  
lemma "fail (LocalSystem init p r) = illegal_sts init p r"
  by (simp add: fun_eq_iff LocalSystem_def fail_def)

definition "lift_pre p = (λ (u, x) (u', y) . p (u (0::nat), x (0::nat)))"  
definition "lift_rel r = (λ (u, x) (u', y) . r (u (0::nat), x (0::nat)) (u' 0, y (0::nat)))"

definition "prec_pre_sts init p r x = (∀ u y . init (u 0) ⟶ (lift_rel r leads lift_pre p) (u, x) (u[1..], y))"
definition "rel_pre_sts init r x y = (∃ u . init (u 0) ∧ (□ lift_rel r) (u, x) (u[1..], y))"
    
lemma prec_pre_sts_simp: "prec_pre_sts init p r x =  (∀ u y . init (u 0) ⟶ (∀n . (∀ i < n . r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n)))"
  apply (simp add: prec_pre_sts_def leads_def until_def lift_rel_def lift_pre_def at_fun_def at_prod_def, safe, blast)
  by blast

lemma prec_stateless_sts_simp: "prec_pre_sts ⊤ (λ (s::unit, x) . inpt r x) (λ (s::unit, x) (s'::unit, y) . r x y :: bool)
    = (□ (λ x . inpt r (x 0)))"
proof (simp add: fun_eq_iff prec_pre_sts_simp always_def inpt_def at_fun_def, safe)
  fix x n
  assume A: "∀y n. (∀i < n. r (x i) (y i)) ⟶ Ex (r (x (n::nat)))"
  have "∃ y .(∀ i ≤ n . r (x i) (y i))"
    proof (induction n)
      case 0
      then show ?case
        using A apply (drule_tac x = "Eps ⊤" in spec, drule_tac x = 0 in spec, safe)
          by (rule_tac x = "(λ i . xa)" in exI, simp)
    next
      case (Suc n)
      from this obtain y where [simp]: "⋀ i . i ≤ n ⟹ r (x i) (y i)"
        by blast
        
      obtain y' where "r (x (Suc n)) y'"
        apply (cut_tac A)
        apply (drule_tac x = y in spec)
        apply (drule_tac x = "Suc n" in spec)
        by auto
      show ?case
        apply (rule_tac x = "λ i . if i ≤ n then y i else y'" in exI)
        apply simp
        using ‹r (x (Suc n)) y'› le_SucE by blast
    qed
    from this show " Ex (r (x n))"
      by blast
  next
    fix x n
    assume "∀f::nat. Ex (r (x f))"
    from this show "Ex (r (x n))"
      by blast
  qed

        
lemma prec_pre_sts_top[simp]: "prec_pre_sts init ⊤ r = ⊤"
  by (simp add: prec_pre_sts_simp fun_eq_iff)
  
lemma prec_pre_sts_bot[simp]: "init a ⟹ prec_pre_sts init ⊥ r = ⊥"
  apply (simp add: prec_pre_sts_simp fun_eq_iff le_fun_def, safe)
  apply (rule_tac x = "λ i . a" in exI, simp)
  apply (rule_tac x = undefined in exI)
  by (rule_tac x = 0 in exI, simp)
    
lemma rel_pre_sts_simp: "rel_pre_sts init r x y = (∃ u . init (u 0) ∧ (∀ i . r (u i, x i) (u (Suc i), y i)))"
  by (simp add: rel_pre_sts_def always_def lift_rel_def at_fun_def at_prod_def)

   
lemma LocalSystem_simp: "LocalSystem init p r  = {.prec_pre_sts init p r.} o [:rel_pre_sts init r:]"
proof -
  have [simp]: "- illegal_sts init p r = prec_pre_sts init p r"
    by (simp add: prec_pre_sts_simp fun_eq_iff illegal_sts_def, blast)
  have [simp]: "(λ x y . ∃u. init (u 0) ∧ run_sts r u x y) = rel_pre_sts init r"
    by (simp add: fun_eq_iff rel_pre_sts_simp run_sts_def)
  show ?thesis
    by (simp add: LocalSystem_not_fail_run)
qed
  

definition "local_init init S = INFIMUM init S"
  

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 nzip_def_abs: "(a || b) = (λi. (a i, b i))"  
  by (simp add: fun_eq_iff nzip_def)

  
lemma nzip_split: "(fst o u) || (snd o u) = u"
  by (simp add: fun_eq_iff nzip_def)

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)

        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)
        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, auto)
        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


definition "rel_comp_sts r r' = (λ ((u,v),x) ((u',v'), z) . (∃ y . r (u,x) (u',y) ∧ r' (v,y) (v',z)))"
definition "prec_comp_sts p r p' = (λ ((u,v),x) . p (u,x) ∧ (∀ y u' . r (u, x) (u',y) ⟶ p' (v,y)))"

definition "sts_comp S S' = [-(u,v),x ↝ (u,x),v -] o (S ** Skip) o [-(u,y),v ↝ (v,y),u-] o (S' ** Skip) o [-(v,z),u ↝ (u,v),z-]"

lemma sts_comp_prec_rel: "sts_comp ({.p.} o [:r:]) ({.p'.} o [:r':]) = {.prec_comp_sts p r p'.} o [:rel_comp_sts r r':]"
  apply (simp add: sts_comp_def Prod_spec_Skip update_def)
  apply (simp add: comp_assoc [THEN sym] assert_demonic_comp demonic_demonic demonic_assert_comp)
  apply (simp add: comp_assoc demonic_demonic)
  apply (simp add: comp_assoc [THEN sym] assert_demonic_comp demonic_demonic demonic_assert_comp assert_assert_comp)
  apply (simp add: comp_assoc demonic_demonic)
  apply (rule prec_rel_eq)
  by (simp_all add: fun_eq_iff prec_comp_sts_def rel_comp_sts_def OO_def)

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 = True"
definition "precS = (λ (u, x) . True)"
definition "relS = (λ (u::nat, x::nat) (u'::nat, y::nat) . u = 0 ∧ u' = 1)"

definition "initS' v = True"
definition "precS' = (λ (u, x) . False)"
definition "relS' = (λ (v::nat, x) (v'::nat, y::nat) . True)"

definition "symbS = LocalSystem initS precS relS"
definition "symbS' = LocalSystem initS' precS' relS'"
definition "symbS'' = LocalSystem (prod_pred initS initS') (prec_comp_sts precS relS precS') (rel_comp_sts relS relS')"

lemma [simp]: "symbS = Magic"
proof (simp add: symbS_def LocalSystem_simp)
  have [simp]: "prec_pre_sts initS precS relS = ⊤"
    by (simp add: prec_pre_sts_simp fun_eq_iff precS_def)
  have [simp]: "rel_pre_sts initS relS  = ⊥"
    apply (simp add: rel_pre_sts_simp fun_eq_iff relS_def initS_def, safe)
    by (metis One_nat_def less_numeral_extra(1))
  show " {. prec_pre_sts initS precS relS .} ∘ [: rel_pre_sts initS relS :] = Magic"
    by (simp add: assert_true_skip Magic_def)
qed

lemma [simp]: "symbS''= Fail"
proof (simp add: symbS''_def LocalSystem_simp)
  have A[simp]: "prod_pred initS initS' = ⊤"
    by (simp add: prod_pred_def initS_def initS'_def fun_eq_iff)
  have B[simp]: "prec_comp_sts precS relS precS' = (λ ((u, v), x). (0 < u))"
    apply (simp add: prec_comp_sts_def)
    by (simp add: prec_comp_sts_def precS'_def fun_eq_iff precS_def relS_def)
    
  have [simp]: "prec_pre_sts (prod_pred initS initS') (prec_comp_sts precS relS precS') (rel_comp_sts relS relS') = ⊥"
    apply (simp add: prec_pre_sts_simp fun_eq_iff)
    apply (simp add:  rel_comp_sts_def relS_def relS'_def, safe)
    by (rule_tac x = "λ i . if i = 0 then (0,0) else (1,1)" in exI, simp)
      
  show " {. prec_pre_sts (prod_pred initS initS') (prec_comp_sts precS relS precS') (rel_comp_sts relS relS') .} 
    ∘ [: rel_pre_sts (prod_pred initS initS') (rel_comp_sts relS relS') :] = Fail"
    by (simp add: assert_false_fail Fail_def del: A B)
qed
  
theorem "symbS o symbS' ≠ symbS''"
  by simp
    
lemma rel_pre_sts_comp: "rel_pre_sts init r OO rel_pre_sts init' r' = rel_pre_sts (prod_pred init init') (rel_comp_sts r r')"
  apply (simp add: rel_pre_sts_simp fun_eq_iff OO_def prod_pred_def rel_comp_sts_def, safe)
   apply (rule_tac x = "u || ua" in exI)
   apply (simp add: nzip_def, blast)
proof -
  fix x xa u xb y
  assume A: "∀i. (case u i of (u, v) ⇒ λx ((u', v'), z). ∃y. r (u, x) (u', y) ∧ r' (v, y) (v', z)) (x i) (u (Suc i), xa i) "
  from A have "∀i. ∃y. r (fst (u i), x i) (fst (u (Suc i)), y) ∧ r' (snd (u i), y) (snd (u (Suc i)), xa i)"
    apply safe
    apply (drule_tac x = i in spec)
      apply (case_tac "u i", simp)
    by (case_tac "u (Suc i)", simp)
  from this have "∃ y . ∀ i . r (fst (u i), x i) (fst (u (Suc i)), y i) ∧ r' (snd (u i), y i) (snd (u (Suc i)), xa i)"
    by (simp add: choice_iff)
  from this obtain yy where [simp]: "⋀ i . r (fst (u i), x i) (fst (u (Suc i)), yy i)" and [simp]: "⋀ i . r' (snd (u i), yy i) (snd (u (Suc i)), xa i)"
    by blast
  assume [simp]: "init xb"
  assume [simp]: "init' y"
  assume [simp]: "u 0 = (xb, y)"
    
  show "∃ yy . (∃ua. init (ua 0) ∧ (∀i. r (ua i, x i) (ua (Suc i), yy i))) ∧ (∃ua. init' (ua 0) ∧ (∀i. r' (ua i, yy i) (ua (Suc i), xa i)))"
    apply (rule_tac x = yy in exI, safe)
     apply (rule_tac x = "fst o u" in exI, simp)
    by (rule_tac x = "snd o u" in exI, simp)
qed
  

  
theorem LocalSystem_comp: "init' a ⟹ LocalSystem init p r o LocalSystem init' p' r' = 
   {.x.(∀u. init (u 0) ⟶ (∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))) ∧
        (∀y. (∃u. init (u 0) ∧ (∀i. r (u i, x i) (u (Suc i), y i))) ⟶ (∀u. init' (u 0) ⟶ (∀ya n. (∀i<n. r' (u i, y i) (u (Suc i), ya i)) ⟶ p' (u n, y n)))).} ∘
    [: rel_pre_sts init r OO rel_pre_sts init' r' :]"
  apply (simp add: LocalSystem_simp comp_assoc [symmetric] assert_demonic_comp)
    by (simp add: prec_pre_sts_simp rel_pre_sts_simp)

      
lemma sts_comp_prec_aux_a: "p' ≤ inpt r' ⟹ 
    (⋀ v y n .v 0 = b ⟹ (∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), y i)) ⟹  prec_comp_sts p r p' ((u n, v n), x n)) ⟹
    ∀i < n. r (u i, x i) (u (Suc i), y i) ⟹ p (u n, x n) ∧ (∃ z v . v 0 = b ∧ (∀ i < n . r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
    proof (induction n)
      case 0
      assume A: "(⋀v y n. v 0 = b ⟹ ∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), y i) ⟹ prec_comp_sts p r p' ((u n, v n), x n))"
      have "prec_comp_sts p r p' ((u 0, (λ i . b) 0), x 0)"
        by (rule A, simp_all)
      from this have [simp]: "p (u 0, x 0)"
        by (simp add: prec_comp_sts_def)
      show ?case
        apply simp
        by (rule_tac x = "λ i . b" in exI, simp)
          
    next
      case (Suc n)
      thm Suc(1)
        
      have "p (u n, x n) ∧ (∃z v. v 0 = b ∧ (∀i<n. r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
        apply (rule Suc(1))
          apply (rule Suc(2))
         apply (rule Suc(3), simp_all)
        by (cut_tac Suc(4), simp)
          
      from this obtain z v where "p (u n, x n)" and [simp]: "v 0 = b" and [simp]: "⋀ i . i < n ⟹ r' (v i, y i) (v (Suc i), z i)" and "⋀ i .  i < n ⟹ p' (v i, y i)"
        by blast
          
      have "⋀ i . i < n ⟹ rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), z i)"
        apply (simp add: rel_comp_sts_def)
          apply (rule_tac x = "y i" in exI, simp)
        by (cut_tac Suc(4), simp)
          
          thm Suc(2)

      from this have A: "(prec_comp_sts p r p' ((u (n), v (n)), x (n)))"
        by (rule_tac Suc(3), auto)
          
      from this have " p (u n, x n) ∧ p' (v n, y n)"
        apply (simp add: prec_comp_sts_def)
        apply safe
        apply (drule_tac x = "y n" in spec, safe, simp)
        by (cut_tac Suc(4), blast)
      from this have "p' (v n, y n)"
        by simp
      from Suc(2) obtain b' a where [simp]: "r' (v n, y n) (b', a)"
        using ‹p' (v n, y n)› by (simp add: le_fun_def inpt_def, blast)
      define v' where "v' = (λ i . if i ≤ n then v i else b')"
      define z' where "z' = (λ i . if i < n then z i else a)"
        
      have [simp]: "v' 0 = b"
        by(simp add: v'_def)
            
      have A': "∀i < Suc n. rel_comp_sts r r' ((u i, v' i), x i) ((u (Suc i), v' (Suc i)), z' i) 
      ⟹ prec_comp_sts p r p' ((u (Suc n), v' (Suc n)), x (Suc n))"
        by (rule Suc(3), simp_all)
            
      have "∀i < Suc n. rel_comp_sts r r' ((u i, v' i), x i) ((u (Suc i), v' (Suc i)), z' i) "
        apply (simp add: rel_comp_sts_def)
        apply safe
        apply (rule_tac x = "y i" in exI)
        apply safe
        using Suc.prems(3) apply auto[1]
        apply (simp add: v'_def z'_def)
        by (case_tac "i = n", simp_all)
          
          
      from this have "prec_comp_sts p r p' ((u (Suc n), v' (Suc n)), x (Suc n))"
        by (rule A')

      from this have [simp]: " p (u (Suc n), x (Suc n))"
        by (simp add: prec_comp_sts_def)
          
      have [simp]: "(∃z v. v 0 = b ∧ (∀i<Suc n. r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
        apply (rule_tac x = z' in exI)
        apply (rule_tac x = v' in exI, simp)
        apply (simp add: v'_def z'_def, safe)
          apply (simp add: ‹⋀i. i < n ⟹ p' (v i, y i)›)
        using ‹r' (v n, y n) (b', a)› less_antisym apply blast
          using ‹p' (v n, y n)› less_antisym by blast
        
        
      show ?case
        by simp
    qed

      
lemma sts_comp_prec_b: "p' ≤ inpt r' ⟹ init' b ⟹ prec_pre_sts (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r') x ⟹
    (prec_pre_sts init p r x ∧ (∀y. rel_pre_sts init r x y ⟶ prec_pre_sts init' p' r' y))" 
   proof (simp add: prec_pre_sts_simp rel_pre_sts_simp, safe)
    fix u
    fix y n
    assume [simp]: "init (u (0::nat))"
    assume [simp]: "init' b"
    assume A: "∀u. prod_pred init init' (u 0) ⟶ (∀y n. (∀i<n. rel_comp_sts r r' (u i, x i) (u (Suc i), y i)) ⟶ prec_comp_sts p r p' (u n, x n))"
    from this have [simp]: "⋀ v y n .v 0 = b ⟹ (∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), y i)) ⟹  prec_comp_sts p r p' ((u n, v n), x n)"
      apply (drule_tac x = "u || v" in spec)
      by (simp add: nzip_def prod_pred_def)
    assume [simp]: "∀i<n. r (u i, x i) (u (Suc i), y i)"
      
    thm sts_comp_prec_aux_a
      assume [simp]: "p' ≤ inpt r'"
      
    from this have "p (u n, x n) ∧ (∃ z v . v 0 = b ∧ (∀ i < n . r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
      apply (cut_tac p = p  and b = b and r = r and p' = p' and r' = r' and u = u and n = n and x = x in  sts_comp_prec_aux_a)
      by simp_all
    from this show "p (u n, x n)"
      by simp
  next
    fix v ya n y u
    assume [simp]: "init' (v (0::nat))"
    assume [simp]: "∀i<n. r' (v i, y i) (v (Suc i), ya i)"
    assume [simp]: "∀i. r (u i, x i) (u (Suc i), y i)"
    assume [simp]: "init (u (0::nat))"
    assume A: "∀u. prod_pred init init' (u 0) ⟶ (∀y n. (∀i<n. rel_comp_sts r r' (u i, x i) (u (Suc i), y i)) ⟶ prec_comp_sts p r p' (u n, x n))"
    from this have B: "(∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), ya i)) ⟹  prec_comp_sts p r p' ((u n, v n), x n)"
      apply (drule_tac x = "u || v" in spec)
      by (simp add: nzip_def prod_pred_def)
      
    have [simp]: "(∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), ya i))"
      apply (simp add: rel_comp_sts_def, safe)
      by (rule_tac x = "y i" in exI, simp)
    
    have C: "prec_comp_sts p r p' ((u n, v n), x n) ⟹  p' (v n, y n)"
      apply (simp add: prec_comp_sts_def, safe)
      apply (drule_tac x = "y n" in spec, safe, simp)
      by (drule_tac x = "u (Suc n)" in spec, auto)
    show " p' (v n, y n)"
      by (rule C, rule B, simp)
  qed
    
primrec u_y :: "('a × 'b ⇒ 'a × 'c ⇒ bool) ⇒ 'a ⇒ (nat ⇒ 'b) ⇒ nat ⇒ 'a ×'c" where
    "u_y r a x 0 = (SOME (u,y) . r (a, x 0) (u, y))" |
    "u_y r a x (Suc n) = (SOME (u, y) . r (fst (u_y r a x n), x (Suc n)) (u, y))"

definition "uu r a x i = (case i of 0 ⇒ a | Suc n ⇒ fst (u_y r a x n))"
definition "yy r a x = snd o (u_y r a x)"

  lemma sts_exists_aux:  "p ≤ inpt r ⟹   prec_pre_sts init p r x ⟹  
        init a ⟹ (∀ i ≤ n . r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i))"
    apply (simp add: prec_pre_sts_simp)
    apply (induction n)
     apply (simp add: uu_def yy_def inpt_def le_fun_def)
     apply (rule someI_ex)
      apply (drule_tac x = "λ i . a" in spec, simp)
    apply simp
    apply safe
    apply (case_tac "i < Suc n")
    apply (drule_tac x = i in spec)
    apply simp
    apply simp
    apply (drule_tac x = "uu r a x" in spec, safe)
    apply (simp add: uu_def)
    apply (drule_tac x = "yy r a x" in spec)
    proof -
      fix n
      assume "∀n. (∀i<n. r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i)) ⟶ p (uu r a x n, x n)"
      from this have A: "(∀i<Suc n. r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i)) ⟶ p (uu r a x (Suc n), x (Suc n))"
        by simp  
      assume "∀i≤n. r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i)"
      from this and A have B: "p (uu r a x (Suc n), x (Suc n))"
        by auto
      assume "p ≤ inpt r"
      from this and B have "inpt r (uu r a x (Suc n), x (Suc n))"
        by (simp add: le_fun_def)
      from this obtain b z where "r (uu r a x (Suc n), x (Suc n)) (b, z)"
        by (simp add: inpt_def, blast)
      from this show "r (uu r a x (Suc n), x (Suc n)) (uu r a x (Suc (Suc n)), yy r a x (Suc n))"
        apply (simp add: uu_def yy_def)
        by (simp add: tfl_some)
    qed
(*todo: create a single lemma with sts_exists_aux*)
lemma sts_exists:  "p ≤ inpt r ⟹   prec_pre_sts init p r x ⟹  init a ⟹  r (uu r a x n, x n) (uu r a x (Suc n), yy r a x n)" 
  by (drule_tac p = p and init = init and n = "Suc n" in sts_exists_aux, auto)

lemma sts_prec:  "p ≤ inpt r ⟹  prec_pre_sts init p r x ⟹  init a ⟹  p (uu r a x n, x n)"
proof -
  assume [simp]: "init a"
  assume [simp]: "p ≤ inpt r"
  assume [simp]: "prec_pre_sts init p r x"
  from this have A: "⋀ u y n . init (u 0) ⟹ ∀i<n. r (u i, x i) (u (Suc i), y i) ⟹ p (u n, x n)"
    by (simp add: prec_pre_sts_simp)
  show "p (uu r a x n, x n)"
    apply (rule A)
     apply (simp add: uu_def)
    apply safe
    by (rule_tac p = p and init = init in sts_exists, simp_all)
qed
  
lemma sts_exists_prec:  "p ≤ inpt r ⟹   prec_pre_sts init p r x ⟹  init a ⟹   p (uu r a x n, x n) ∧ r (uu r a x n, x n) (uu r a x (Suc n), yy r a x n)"
  by (simp add: sts_exists sts_prec)
    
lemma sts_comp_prec_a: "p ≤ inpt r ⟹ prec_pre_sts init p r x ⟹ (⋀ y. rel_pre_sts init r x y ⟹ prec_pre_sts init' p' r' y) 
    ⟹ prec_pre_sts (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r') x"
proof (subst prec_pre_sts_simp, safe)
  fix u y n 
  assume Z: "p ≤ inpt r"
  assume init: "prod_pred init init' (u (0::nat))"
    
  define a where "a = fst o u"
  define b where "b = snd o u"
   
  have [simp]: "⋀i . u i = (a i, b i)"
    by (simp add: a_def b_def)
      
  thm choice_iff
    
    
  assume A: "prec_pre_sts init p r x"
  assume T: "(⋀ y. rel_pre_sts init r x y ⟹ prec_pre_sts init' p' r' y)"
  assume "∀i<n. rel_comp_sts r r' (u i, x i) (u (Suc i), y i)"
 
  from this obtain z where  U: "⋀ i . i < n ⟹ r (a i, x i) (a (Suc i), z i)" and G: "⋀ i . i < n ⟹ r' (b i, z i) (b (Suc i), y i)"
    by (simp add: rel_comp_sts_def choice_iff', blast)

  from init have [simp]: "init (a 0)" and [simp]: "init' (b 0)"
    by (simp_all add: prod_pred_def)

  from A have H: "⋀ y n . (∀i<n. r (a i, x i) (a (Suc i), y i)) ⟹ p (a n, x n)"
    by (simp add: prec_pre_sts_simp)
      
  have [simp]: "p(a n, x n)"
    apply (rule H)
    using U by auto     
     
  show "prec_comp_sts p r p' (u n, x n)"
  proof (simp add: prec_comp_sts_def, safe)
    fix ya u'
    assume [simp]: "r (a n, x n) (u', ya)"
    define a' where "a' = (λ i . if i ≤ n then a i else u')"
    define y' where "y' = (λ i . if i < n then z i else ya)"

    define N where "N = Suc n"
      
    have V: "⋀ i . i < N ⟹ r (a' i, x i) (a' (Suc i), y' i)"
      apply (simp add: a'_def y'_def N_def, safe)
      using U apply simp
      using ‹r (a n, x n) (u', ya)› less_antisym by blast
      
  have B: "prec_pre_sts (λ c . c = a' N) p r (x[N..])"
    using A apply (simp add: prec_pre_sts_simp)
    apply safe
    apply (drule_tac x = "λ i . if i ≤ N then a' i else u (i - N)" in spec)
    apply safe
     apply simp_all
      apply (simp add: a'_def)
    apply (drule_tac x = "(λ i . if i < N then y' i else y (i - N))" in spec)
  proof -
    fix u y m
    define na where "na = N + m"
      
    assume [simp]: "u (0::nat) = a' N"  
    assume "∀na. (∀i<na. r (if i ≤ N then a' i else u (i - N), x i) (if Suc i ≤ N then a' (Suc i) else u (Suc i - N), if i < N then y' i else y (i - N))) ⟶
                 p (if na ≤ N then a' na else u (na - N), x na)"
      
    from this have C: " (∀i<na. r (if i ≤ N then a' i else u (i - N), x i) (if Suc i ≤ N then a' (Suc i) else u (Suc i - N), if i < N then y' i else y (i - N))) ⟶
                 p (if na ≤ N then a' na else u (na - N), x na)"
      by simp
        

    assume B: " ∀i<m. r (u i, x (N + i)) (u (Suc i), y i)"
      
    have [simp]: "(∀i<na. r (if i ≤ N then a' i else u (i - N), x i) (if Suc i ≤ N then a' (Suc i) else u (Suc i - N), if i < N then y' i else y (i - N)))"
      apply safe
      apply (case_tac "i ≤ N", simp_all add: na_def, safe)
      using V apply auto [1]
       apply (cut_tac B)
        apply (drule_tac x = 0 in spec, simp)
       apply (cut_tac B)
      apply (drule_tac x = "i - N" in spec, auto)
      by (simp add: Suc_diff_le)
        
    from C have D: " p (if na ≤ N then a' na else u (na - N), x na)"
      by simp
      
    show "p (u m, x (N + m))"
      using D apply (simp add: na_def)
      apply (case_tac "m = 0", simp_all)
      by (simp_all add: na_def)
  qed

  have S: "⋀ k . r (uu r (a' N)  (x[N..]) k, (x[N..]) k) (uu r (a' N) (x[N..]) (Suc k), yy r (a' N) (x[N..]) k)"
    apply (rule_tac p = p and r = r and init = "(λc. c = a' N)" in sts_exists)
      apply (rule Z)
     apply (rule B)
    by simp
        
  define u' where "u' = (λ i . if i ≤ N then a' i else uu r (a' N)  (x[N..]) (i - N))" 
  define z' where "z' = (λ i . if i < N then y' i else yy r (a' N)  (x[N..]) (i - N))" 

  have "rel_pre_sts init r x z'"
    apply (simp add: rel_pre_sts_simp)
    apply (rule_tac x = u' in exI)
    apply (simp add: u'_def z'_def, safe)
      apply (simp add: a'_def)
    using S [of 0]  apply (simp add: uu_def)
    using V apply simp
    apply (cut_tac k = "i - N" in S, auto)
    by (subgoal_tac "Suc (i - N) = Suc i - N", simp_all)
      

      
    from this T have "prec_pre_sts init' p' r' z'"
      by simp
    
    from this show "p' (b n, ya)"
      apply (simp add: prec_pre_sts_simp)
      apply (drule_tac x = b in spec, simp)
      apply (drule_tac x = y in spec)
      apply (drule_tac x = n in spec, safe)
       apply (simp add: G z'_def N_def y'_def)
        by (simp add: z'_def N_def y'_def)
qed
  
qed       
      
lemma prec_pre_sts_comp: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init' b ⟹ 
    (prec_pre_sts init p r x ∧ (∀y. rel_pre_sts init r x y ⟶ prec_pre_sts init' p' r' y))
      = prec_pre_sts (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r') x"
  apply safe
    apply (simp_all add: sts_comp_prec_b)
    by (rule sts_comp_prec_a, simp_all)


lemma sts_comp: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init' b ⟹ 
           LocalSystem init p r o LocalSystem init' p' r' = LocalSystem (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r')"
  apply (simp add: LocalSystem_simp)
  by (simp add: comp_assoc [THEN sym] assert_demonic_comp rel_pre_sts_comp prec_pre_sts_comp)
    
    
subsection{*Parallel Composition of STSs*}

definition "rel_prod_sts r r' = (λ ((u,v), (x, y)) ((u', v'), (x', y')) . r (u,x) (u',x') ∧ r' (v, y) (v', y'))"
definition "prec_prod_sts p p' = (λ ((u,v), (x, y)) . p (u,x) ∧ p' (v,y))"

lemma "(prec_prod_sts (inpt r)  (inpt r')) ≤ inpt (rel_prod_sts r r')"
  by (simp add: prec_prod_sts_def rel_prod_sts_def inpt_def le_fun_def)

lemma "(prec_prod_sts (inpt r)  (inpt r')) = inpt (rel_prod_sts r r')"
  by (simp add: prec_prod_sts_def rel_prod_sts_def inpt_def fun_eq_iff)

definition "distrib_state = [:(u,v), (x, y) ↝ (u', x'), (v', y'). u'=u ∧ v'=v ∧ x'=x ∧ y'=y:]"
definition "merge_state = [:(u, x), (v, y) ↝ (u', v'), (x', y'). u'=u ∧ v'=v ∧ x'=x ∧ y'=y:]"


lemma "distrib_state o merge_state = Skip"
  apply (simp add: distrib_state_def merge_state_def demonic_demonic demonic_eq_skip[THEN sym])
  apply (rule_tac f = demonic in arg_cong)
  apply (simp add: fun_eq_iff OO_def)
  by auto


lemma "merge_state o distrib_state = Skip"
  apply (simp add: distrib_state_def merge_state_def demonic_demonic demonic_eq_skip[THEN sym])
  apply (rule_tac f = demonic in arg_cong)
  apply (simp add: fun_eq_iff OO_def)
  by auto

definition "prod_sts S S' = (distrib_state o (S ** S') o merge_state)"

lemma prod_sts: "prod_sts ({.p.} o [:r:]) ({.p'.}o[:r':]) = {.prec_prod_sts p p'.} o [:rel_prod_sts r r':]"
  apply (simp add: prod_sts_def Prod_spec merge_state_def distrib_state_def)
  apply (simp add: comp_assoc [THEN sym] demonic_assert_comp)
  apply (simp add: comp_assoc demonic_demonic)
  apply (rule prec_rel_eq)
  apply (simp add: fun_eq_iff prec_prod_sts_def)
  by (simp add: fun_eq_iff rel_prod_sts_def OO_def)
    
lemma update_demonic_update: "[-f-] o [:r:] o [-g-] = [:x ↝ y . ∃ z . r (f x) z ∧ y = g z:]"
  by (simp add: demonic_def fun_eq_iff update_def le_fun_def, auto)
    
lemma sts_prod_prec: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init a ⟹ init' b ⟹ 
   prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') (x || y)
  = (prec_pre_sts init p r x ∧ prec_pre_sts init' p' r' y)"
proof (safe)
  assume initA[simp]: "init a"
  assume initB[simp]: "init' b"
  assume "p' ≤ inpt r'" and "p ≤ inpt r"
  from this have [simp]: "prec_prod_sts p p' ≤ inpt (rel_prod_sts r r')"
    by (simp add: prec_prod_sts_def le_fun_def rel_prod_sts_def inpt_def)
    
  assume A: "prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') (x || y)"
  from this have C: "⋀ n . prec_prod_sts p p' (uu (rel_prod_sts r r') (a,b) (x || y) n, (x || y) n) ∧ rel_prod_sts r r' (uu (rel_prod_sts r r') (a,b) (x || y) n, (x || y) n) 
        (uu (rel_prod_sts r r') (a, b) (x || y) (Suc n), yy (rel_prod_sts r r') (a, b) (x || y) n)"
    apply (cut_tac r = "(rel_prod_sts r r')" and p = "prec_prod_sts p p'" and init = "prod_pred init init'" 
        and a = "(a,b)" and x = "x || y" and n = n in sts_exists_prec)
       apply simp_all
    by (simp add: prod_pred_def)
      
  obtain u' v' where U[simp]: "uu (rel_prod_sts r r') (a,b) (x || y) = u' || v'"
    using nzip_split [symmetric] by auto 

  obtain s' t' where [simp]: "yy (rel_prod_sts r r') (a,b) (x || y) = s' || t'"
    using nzip_split [symmetric] by auto
      
  have [simp]: "init (u' 0)"
    by (cut_tac U, simp add: fun_eq_iff del: U, drule_tac x= 0 in spec, 
        cut_tac initA, simp add: uu_def nzip_def del: U initA)

  have [simp]: "init' (v' 0)"
    by (cut_tac U, simp add: fun_eq_iff del: U, drule_tac x= 0 in spec, cut_tac initB, 
        simp add: uu_def nzip_def del: U initB)
      
  from C have [simp]: "⋀ n . r (u' n, x n) (u' (Suc n), s' n)" and [simp]: "⋀ n . r' (v' n, y n) (v' (Suc n), t' n)"
    by (simp_all, simp_all add: rel_prod_sts_def nzip_def)
      
  from A have B: "⋀ u v s t n . init (u 0) ⟹ init' (v 0) ⟹ ∀i < n. r (u i, x i) (u (Suc i), s i) ⟹  ∀i<n. r' (v i, y i) (v (Suc i), t i) ⟹ p (u n, x n) ∧ p' (v n, y n)"
    apply (simp add: prec_pre_sts_simp)
    apply (drule_tac x = "u || v" in spec)
    apply (simp add: prod_pred_def nzip_def)
    apply (drule_tac x = "s || t" in spec) 
    by (simp add: prec_prod_sts_def rel_prod_sts_def nzip_def)
    
  show "prec_pre_sts init p r x"
    apply (simp add: prec_pre_sts_simp, safe)
    by (cut_tac n = n and u = u and v = v' and s = y and t = t' in B, simp_all) 
  
  show "prec_pre_sts init' p' r' y"
    apply (simp add: prec_pre_sts_simp, safe)
    by (cut_tac n = n and u = u' and v = u and s = s' and t = ya in B, simp_all)
      
next
  assume U: "prec_pre_sts init p r x"
  assume V: "prec_pre_sts init' p' r' y"
  show "prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') (x || y)"
  proof (simp add: prec_pre_sts_simp prod_pred_def rel_prod_sts_def prec_prod_sts_def nzip_def, clarify)
    fix u xa ya yaa n ua v
    assume A: "∀i<n. (case u i of (u, v) ⇒ λ(x, y) ((u', v'), x', y'). r (u, x) (u', x') ∧ r' (v, y) (v', y')) (x i, y i) (u (Suc i), yaa i)"
    define a where "a = fst o u"
    define b where "b = snd o u"
    define s where "s = fst o yaa"
    define t where "t = snd o yaa"
      
    assume "u 0 = (xa, ya) "
    assume "init xa"
    assume "init' ya"
    assume "(ua, v) = u n"
    have [simp]: "init (a 0)"
      by (simp add: ‹init xa› ‹u 0 = (xa, ya)› a_def)
    have [simp]: "init' (b 0)"
      by (simp add: ‹b ≡ snd ∘ u› ‹init' ya› ‹u 0 = (xa, ya)›)
      
    have [simp]: "⋀ i . i < n ⟹ r (a i, x i) (a (Suc i), s i)" and [simp]: "⋀ i . i < n ⟹ r' (b i, y i) (b (Suc i), t i)"
      using A apply (drule_tac x = i in spec)
      apply (case_tac "u i", case_tac "yaa i", case_tac "u (Suc i)", simp add: a_def s_def)
      using A apply (drule_tac x = i in spec)
      by (case_tac "u i", case_tac "yaa i", case_tac "u (Suc i)", simp add: b_def t_def)
        
    from U have [simp]: "p (a n, x n)"
      apply (simp add: prec_pre_sts_simp)
      apply (drule_tac x = a in spec, simp)
      by (drule_tac x = s in spec, simp)

    from V have [simp]: "p' (b n, y n)"
      apply (simp add: prec_pre_sts_simp)
      apply (drule_tac x = b in spec, simp)
      by (drule_tac x = t in spec, simp)
        
    have [simp]: "ua = a n"
      by (metis ‹(ua, v) = u n› ‹a ≡ fst ∘ u› comp_def fst_conv)

    have [simp]: "v = b n"
      by (metis ‹(ua, v) = u n› b_def comp_apply snd_conv)
      
    show "p (ua, x n) ∧ p' (v, y n)"
      by simp
  qed
qed
  
lemma sts_prod_rel: "(λ x y . ∃z. rel_pre_sts (prod_pred init init') (rel_prod_sts r r') (case x of (x, xa) ⇒ x || xa) z ∧ y = (fst ∘ z, snd ∘ z))
  = (λ (x, y) (u, v) . rel_pre_sts init r x u ∧ rel_pre_sts init' r' y v)"
  apply (subst fun_eq_iff)
  apply (subst fun_eq_iff)
  apply(simp add: rel_pre_sts_simp nzip_def prod_pred_def rel_prod_sts_def, safe)
    apply (rule_tac x = "fst o u" in exI)
    apply clarsimp
    apply (drule_tac x = i in spec)
    apply (case_tac "u i", simp)
    apply (case_tac "u (Suc i)", simp)
    apply (case_tac "z i", simp)
    apply (rule_tac x = "snd o u" in exI)
    apply clarsimp
    apply (drule_tac x = i in spec)
    apply (case_tac "u i", simp)
    apply (case_tac "u (Suc i)", simp)
   apply (case_tac "z i", simp)
  apply (rule_tac x = "aa || ba" in exI, safe)
    apply (rule_tac x = "u || ua" in exI, safe)
    by (simp_all add: nzip_def)
  
    
theorem sts_prod: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init a ⟹ init' b ⟹ 
    LocalSystem init p r ** LocalSystem init' p' r' = 
    [-x, x' ↝ x || x'-] o LocalSystem (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') o [-y ↝ fst o y, snd o y-]"
proof -
  assume [simp]: "p ≤ inpt r"
  assume [simp]: "p' ≤ inpt r'"
  assume [simp]: "init a"
  assume [simp]: "init' b"
    
    thm sts_prod_prec
    
  have [simp]: "prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y)
    = (λ (x, y) . prec_pre_sts init p r x ∧ prec_pre_sts init' p' r' y)"
    apply (simp add: fun_eq_iff)
      by (subst sts_prod_prec [of _ _ _ _ _ a _ b], simp_all)
    
      
  have "[-x, x' ↝ x || x'-] o LocalSystem (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') o [-y ↝ fst o y, snd o y-] = 
     [- (x, y) ↝ x || y -] ∘ {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') .} 
      ∘ [: rel_pre_sts (prod_pred init init') (rel_prod_sts r r') :] ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]"
    by (simp add: LocalSystem_simp comp_assoc [symmetric])
      
 also have "... = {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y) .} ∘ [- (x, y) ↝ x || y -] ∘
    [: rel_pre_sts (prod_pred init init') (rel_prod_sts r r') :] ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]"
   by (simp add: update_assert_comp)
 also have "... =  {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y) .} ∘ ([- (x, y) ↝ x || y -] ∘
    [: rel_pre_sts (prod_pred init init') (rel_prod_sts r r') :] ∘ [- y ↝ (fst ∘ y, snd ∘ y) -])"
   by (simp add: comp_assoc)
     
  also have "... = {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y) .} ∘
    [:x↝y.∃z. rel_pre_sts (prod_pred init init') (rel_prod_sts r r') (case x of (x, xa) ⇒ x || xa) z ∧ y = (fst ∘ z, snd ∘ z):]"
    by (simp add: update_demonic_update)
      
  also have "... =  {.(x, y).prec_pre_sts init p r x ∧ prec_pre_sts init' p' r' y.} ∘ [:(x, y)↝(u, v).rel_pre_sts init r x u ∧ rel_pre_sts init' r' y v:]"
    by (simp add: sts_prod_rel)
  also have "... = LocalSystem init p r ** LocalSystem init' p' r'"
    by (simp add: LocalSystem_simp Prod_spec)
  finally show ?thesis
    by simp
qed


  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, x) . u ≤ M)"
  definition "rel_count = (λ (u,x) (u', 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 = LocalSystem (λ a . a = 0) (prec_count M) rel_count"

  lemma "COUNTER = Counter_global"
    proof -
      have A:"rel_pre_sts (λ a . a = 0) rel_count = (λ x y . y = count x)"
        proof (simp add: rel_pre_sts_simp rel_count_def fun_eq_iff, 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 A: "u == (λ i . if i = 0 then 0 else count x (i - 1))"
          assume B: "∀xb::nat. xa xb = count x xb"
          {fix xb::nat
          from A 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 "(prec_pre_sts (λ a . a = 0) (prec_count x) rel_count) = (λxa::nat ⇒ bool. ∀k::nat. count xa k ≤ x)"
        proof (simp add: fun_eq_iff  prec_pre_sts_simp   prec_count_def at_fun_def rel_count_def, safe)
          fix xa::"nat ⇒ bool" and k:: nat
          define uu where A: "uu == (λ i . if i = 0 then 0 else count xa (i - 1))"
          assume "∀u. u 0 = 0 ⟶ (∀y n. (∀i<n. (xa i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ xa i ⟶ u (Suc i) = u i) ∧ y i = u (Suc i)) ⟶ u n ≤ x) " (is "∀ u . ?p u ⟶ ?s u")
          then have "?p uu ⟶ ?s uu"
            by blast
          from this and A  have "?s uu"
            by simp
          then have "∀ n. (∀i<n. (xa i ⟶ uu (Suc i) = Suc (uu i)) ∧ (¬ xa i ⟶ uu (Suc i) = uu i)) ⟶ uu n ≤ x"
            apply auto
            by (drule_tac x = "λ i . uu (Suc i)" in spec, simp)
          from this have "(∀i < (Suc k). (xa i ⟶ uu (Suc i) = Suc (uu i)) ∧ (¬ xa i ⟶ uu (Suc i) = uu i)) ⟶ uu (Suc k)≤ x"
            by simp
          from this and A show "count xa k ≤ x"
            apply (auto)
              apply (metis (no_types, lifting) Suc_eq_plus1_left Suc_pred add.commute count.simps(2))
            using not_gr_zero apply fastforce
               apply (metis (no_types, lifting) Suc_eq_plus1_left Suc_pred add.commute count.simps(2))
            using not_gr_zero apply fastforce
             apply (metis Suc_pred count.simps(2))
            by (metis Suc_pred count.simps(2))
              

        next 
          fix xa:: "nat ⇒ bool" and  u::"nat ⇒ nat" and n::nat
          fix y
          assume C: "∀k::nat. count xa k ≤ x"
          assume A: "u (0::nat) = (0::nat)"
          assume B: "∀i<n. (xa i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ xa i ⟶ u (Suc i) = u i) ∧ y i = u (Suc i)"
            
          have D: "∀i < n. count xa i = u (Suc i)"
            apply (rule counter_a_aux)
             apply (simp add: A)
            by (simp add: B)
              
            
            
          show "u n ≤ x"
            apply (case_tac n, simp add: A)
            apply simp
              apply (cut_tac D)
            apply (drule_tac x = nat in spec, simp)
            apply (cut_tac C)
            by (drule_tac x = "nat" in spec, simp)
        qed
        }
      note B = this
     show ?thesis
      by (simp add: fun_eq_iff COUNTER_def LocalSystem_simp 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, x) (u', y) . ((x ∧ u' = u + (1::int)) ∨ (¬ x ∧ u' = u - 1) ∨ u' = 0) ∧ (y = (u' = 0)))"
  definition "prec_ex = (λ (u, x) . -1 ≤ u ∧ u ≤ 3)"

  definition "LIVE = {. prec_pre_sts (λ a . a = 0) prec_ex rel_ex.} 
    o [:x ↝ y . ∃ u . u (0::nat) = 0 ∧ (□(λ u x y . rel_ex (u (0::nat), x (0::nat)) (u 1, y (0::nat)))) u x y  ∧ (□ (♢ (λ y . y 0))) y :]"

thm fusion_spec_local_a
                                    
lemma LIVE_fusion: "LIVE = (LocalSystem (λ a . a = 0) prec_ex rel_ex) ∥ [:x ↝ y . (□ (♢ (λ y . y 0))) y:]"
proof-
  have [simp]: "⋀ x y . rel_pre_sts (λa. a = 0) rel_ex x y = ( ∃u. u 0 = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u (Suc 0), y 0))) u x y)"
    by (simp add: rel_pre_sts_simp always_def at_fun_def)
    have [simp]: "rel_pre_sts (λa. a = 0) rel_ex ⊓ (λx. □ ♢ (λy. y 0)) = (λ x y . ∃u. u 0 = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u (Suc 0), y 0))) u x y ∧ (□ ♢ (λy. y 0)) y)"
      by (simp add: fun_eq_iff, blast)
show "LIVE = (LocalSystem (λ a . a = 0) prec_ex rel_ex) ∥ [:x ↝ y . (□ (♢ (λ y . y 0))) y:]"
        apply (simp add: LocalSystem_simp)
    apply (auto simp add: LIVE_def  fusion_spec_local_a at_fun_def)
    apply (cut_tac p = "prec_pre_sts (λa. a = 0) prec_ex rel_ex" and p' =  
        and r = "rel_pre_sts (λa. a = 0) rel_ex" and r' = "λx. □ ♢ (λy. y 0)" in fusion_spec)
    by (simp add: assert_true_skip)
      
   qed

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

lemma monotonic_SymSystem[simp]: "mono (LocalSystem init p r)"
  
    by (simp add: LocalSystem_simp)

  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)" 
        proof -
          have f1: "∀x0. a x0 - 1 = - 1 + a x0"
            by simp
          have f2: "∀x0. a x0 + 1 = 1 + a x0"
            by auto
          have "∀n. (xa n ∧ a (Suc n) = 1 + a n ∨ ¬ xa n ∧ a (Suc n) = - 1 + a n ∨ a (Suc n) = 0) = (xa n ∧ a (Suc n) + - 1 * a n = 1 ∨ ¬ xa n ∧ a (Suc n) + - 1 * a n = - 1 ∨ a (Suc n) = 0)"
            by force
          hence f3: "(∀n. xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0) = (∀n. xa n ∧ a (Suc n) + - 1 * a n = 1 ∨ ¬ xa n ∧ a (Suc n) + - 1 * a n = - 1 ∨ a (Suc n) = 0)"
        using f2 f1 by presburger
        have "a (Suc n) + - 1 * a n = 1 ∨ a (Suc n) + - 1 * a n = - 1 ∨ (¬ xa n ∨ a (Suc n) + - 1 * a n ≠ 1) ∧ (xa n ∨ a (Suc n) + - 1 * a n ≠ - 1)"
        by meson
        thus ?thesis
        using f3 Suc.IH `∀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 0 = 0` `a n ≠ - 1` by auto
        qed
      }
      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)

  thm fusion_local_refinement
    
  lemma "{.□ preca_ex.} o LIVE ≤ LocalSystem (λ a . a = (0::int)) prec_ex rel_ex"
  proof (unfold LIVE_def LocalSystem_simp comp_assoc [symmetric] assert_assert_comp)
    show " {. □ preca_ex ⊓ prec_pre_sts (λa. a = 0) prec_ex rel_ex .} 
    ∘ [:x↝y.∃u. u (0::nat) = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u 1, y 0))) u x y ∧ (□ ♢ (λy. y 0)) y:]
    ≤ {. prec_pre_sts (λa. a = 0) prec_ex rel_ex .} ∘ [: rel_pre_sts (λa. a = (0::int)) rel_ex :]"
    proof (unfold assert_demonic_refinement, safe)
      fix x xa
      assume "(□ preca_ex) x"
      then have B: "∀i::nat. x (Suc i) = (¬ x i)"
        by (auto simp add: preca_ex_def always_def at_fun_def)
      assume "prec_pre_sts (λa. a = 0) prec_ex rel_ex x"
      assume "rel_pre_sts (λa. a = 0) rel_ex x xa"
      from this obtain u where  [simp]: "u 0 = 0" and [simp]: "⋀ i . rel_ex (u i, x i) (u (Suc i), xa i)"
        by (simp add: rel_pre_sts_simp, blast)

      then have C: "∀i . (x i ∧ u (Suc i) = u i + 1 ∨ ¬ x i ∧ u (Suc i) = u i - 1 ∨ u (Suc i) = 0) ∧ xa i = (u (Suc i) = 0)"
        by (simp add:   rel_ex_def)

      have D: "(∀ n . (u n = -1 ⟶ x n) ∧ (u n = 1 ⟶ ¬ x n) ∧ -1 ≤ u n ∧ u n ≤ 1)"
        by (cut_tac B C, rule event_ex_aux, auto)
          
      have [simp]: "(□ (λu x y. rel_ex (u 0, x 0) (u (Suc 0), y 0))) u x xa "
        by (simp add: always_def at_fun_def)
      thm rel_ex_def
      thm preca_ex_def
     {
          fix a::nat
          {assume "u (Suc a) = 0" from this 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 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 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 B C D have X: "∃b . xa (a + b)"
            by (simp, metis diff_0 int_one_le_iff_zero_less le_less not_le zle_diff1_eq)
      }
      then have [simp]: "(□ ♢ (λy. y 0)) xa"
        by (simp add: always_def eventually_def preca_ex_def at_fun_def)
      show "∃u. u (0::nat) = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u 1, y 0))) u x xa ∧ (□ ♢ (λy. y 0)) xa"
        by (rule_tac x = u in exI, simp)
    qed
  qed
end