Theory TransitionFeedback

(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Viorel Preoteasa
 *
 * This software is governed by the MIT licence and abiding by the rules of
 * distribution of free software. You can use, modify and/or redistribute the
 * software under the terms of the MIT licence included in this distribution.
 *)

subsection‹Feedback Operator on Predicate Transformers›

theory TransitionFeedback
  imports "../RefinementReactive/Refinement"

begin

  definition grd_update :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ bool) ⇒ 'a ⇒ bool" ("[-(_)→(_)-]") where
    "[-p→f-] = [:x ↝ y . p x ∧ y = f x:]"

  lemma "[-p→f-] = [.p.] o [-f-]"
    by (simp add: grd_update_def update_def fun_eq_iff demonic_def assume_def le_fun_def)

  lemma assert_grd_update: "(⋀ x . p x ⟹ p' x) ⟹ {.p.} o [-p'→f-] = {.p.} o [-f-]"
    by (auto simp add: fun_eq_iff grd_update_def update_def demonic_def assert_def le_fun_def)

  lemma grd_update_comp: "[-p→f-] o [-q→g-] = [-p ⊓ (q o f) → g o f-]"
    by (auto simp add: fun_eq_iff grd_update_def update_def demonic_def le_fun_def)

  lemma grd_update_assert_comp: "[-p→f-] o {.q.} = {. x . p x ⟶ q (f x).} o [-p → f-]"
    by (auto simp add: fun_eq_iff grd_update_def update_def demonic_def assert_def le_fun_def)

  lemma grd_update_update_comp: "[-p→f-] o [-g-] = [-p → g o f-]"
    by (auto simp add: fun_eq_iff grd_update_def update_def demonic_def le_fun_def)

  lemma update_grd_update_comp: "[-g-] o [-p→f-] = [-p o g → f o g-]"
    by (auto simp add: fun_eq_iff grd_update_def update_def demonic_def le_fun_def)

  lemma grd_update_update [simp]: "[-⊤→f-] = [-f-]"
    by (simp add: grd_update_def update_def)

  lemma [simp]: "(∃y. (a, y) = f (u, x)) = (a = fst (f (u, x)))"
    apply safe
    apply (metis fst_conv)
    by (rule_tac x = "snd (f (u, x))" in exI, simp)

  lemma pair_eq: "((a, b) = x) = (a = fst x ∧ b = snd x)"
    by auto

  lemma comp_exists: "(r OO r') x y = (∃ z . r x z ∧ r' z y)"
    by auto

  lemma comp_existsa: "(r OO r')  = (λ x y . ∃ z . r x z ∧ r' z y)"
    by (auto simp add: fun_eq_iff assert_true_skip)

  lemma drop_assumption: "p ⟹True"
    by simp

  lemma fun_comp_simp: "((λ(x, y). (f x, y)) ∘ (λ(a, b). (c b, d (a, b)))) = (λ (a, b) .  (((f o c) b), d (a, b)))"
    by (simp add: fun_eq_iff)

  lemma fun_comp_simp_b: "((λ(a::'c, b::'d). (c b, d (a, b))) ∘ (λ(x::'a, y::'d). (f x, y))) = (λ (x, y) .  (c y, d (f x, y)))"
    by (simp add: fun_eq_iff)

  lemma fun_comp_simp_c: "((λ((c, d), a). (a, c, d)) ∘ (λ(x, y). (case x of (a, b) ⇒ (c b, d (a, b)), f y)) ∘ (λ(a, c, b). ((a, b), c))) = (λ (u,v,w) .  (f v, c w, d (u, w)))"
    by (simp add: fun_eq_iff)

  lemma fun_comp_simp_d: "(λx. case case x of (c, b) ⇒ ((case x of (v, w) ⇒ f v, b), c) of (x, y) ⇒ p x ∧ p' y) = (λ (u,v) .  p (f u, v) ∧ p' u)"
    by (simp add: fun_eq_iff)

  lemma fun_comp_simp_e: "(λx. case x of (v, w) ⇒ (c w, d (case x of (v, w) ⇒ f v, w))) = (λ (u, v) .  (c v, d (f u, v)))"
    by (simp add: fun_eq_iff)

definition "select S = {. x . (∃ u . prec S (u, x)).} o [:x ↝ u, x' . x' = x ∧ prec S (u, x) :] o S o [:v, y ↝ v' . v' = v:]"
  

  lemma selectc_spec: "select ({. p .} o [:r:]) = {. x . (∃ u . p (u, x)).} o [:x ↝ v . ∃ u y . p (u, x) ∧ r (u,x) (v,y) :]"
    by (simp add: select_def fun_eq_iff demonic_def assert_def le_fun_def, auto)

  lemma select_sconjunctive[simp]: "sconjunctive S ⟹ sconjunctive (select S)"
    by (simp add: select_def)

  lemma sconjunctive_fusion[simp]: "sconjunctive S ⟹ sconjunctive S' ⟹ sconjunctive (S ∥ S')"
    by (simp add: fusion_prod)

  lemma sconjunctive_Skip[simp]: "sconjunctive Skip"
    by (simp add: Skip_def sconjunctive_def)

  lemma [simp]: "prec S = ⊤ ⟹ prec (select S) = ⊤"
    by (simp add: select_def top_fun_def)

definition "selectA S = {. x . (∃ u . prec S (u, x)).} o [:x ↝ u, x' . x' = x ∧ prec S (u, x) :] o (S ∥ [:u, x ↝ v, y . u = v:]) o [:v, y ↝ v' . v' = v:]"

definition "selectB S = {:x ↝ u, x' . x = x':} o S o [:v, y ↝ v' . v' = v:]"

definition "selectC S = {:x ↝ u, x' . x = x':} o (S ∥ [:u, x ↝ v, y . u = v:]) o [:v, y ↝ v' . v' = v:]"
  
definition "feedback S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((select S) ** Skip) o (S ∥ [:u, x ↝ v, y . u = v:]) o [:u,y ↝ y' . y' = y:]"
  
definition "feedbackA S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((selectA S) ** Skip) o (S ∥ [:u, x ↝ v, y . u = v:]) o [:u,y ↝ y' . y' = y:]"

definition "feedbackB S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((selectB S) ** Skip) o (S ∥ [:u, x ↝ v, y . u = v:]) o [:u,y ↝ y' . y' = y:]"

definition "feedbackC S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((selectC S) ** Skip) o (S ∥ [:u, x ↝ v, y . u = v:]) o [:u,y ↝ y' . y' = y:]"
  
lemma selectA_spec: "selectA ({. p .} o [:r:]) = {. x . (∃ u . p (u, x)).} o [:x ↝ u . ∃  y . p (u, x) ∧ r (u,x) (u,y) :]"
  apply (simp add: selectA_def fusion_spec_demonic)
  by (simp add: selectA_def fun_eq_iff demonic_def assert_def le_fun_def fusion_spec_demonic, auto)
    
thm Prod_angelic_demonic_Skip

lemma feedbackB_spec: "feedbackB ({.p.} o [:r:]) = {:x ↝ u, x' . p (u,x) ∧ (∀ v y . r (u,x) (v, y) ⟶ p (v,x)) ∧ x = x':} o [:u,x ↝ y . ∃ v y' . r (u,x) (v, y') ∧ r (v, x) (v, y):]"
  apply (simp add: feedbackB_def selectB_def Prod_spec_Skip fusion_spec_demonic)
  apply (subgoal_tac "{:x ↝ (u, x').x = x':} ∘ ({. p .} ∘ [: r :]) ∘ [:(v, y)↝v' . v' = v:] 
      = {:x ↝ (u, x'). p (u, x) ∧ x = x':} ∘ [:u,x ↝ v . ∃ y . r (u,x) (v, y):]")
   apply (simp add: Prod_angelic_demonic_Skip)
   apply (simp add: fun_eq_iff demonic_def angelic_def assert_def le_fun_def, auto)
    apply (rule_tac x = a in exI, simp_all, auto)
   by (simp add: fun_eq_iff demonic_def angelic_def assert_def le_fun_def)
    
lemma feedbackC_spec: "feedbackC ({.p.} o [:r:]) = {:x ↝ u, x' . p (u,x) ∧ (∀ y . r (u,x) (u, y) ⟶ p (u,x)) ∧ x = x':} o [:u,x ↝ y . r (u, x) (u, y):]"
  apply (simp add: feedbackC_def selectC_def Prod_spec_Skip fusion_spec_demonic)
  apply (subgoal_tac "({:x ↝ (u, x').x = x':} ∘ ({. p .} ∘ [: r ⊓ (λ(u, x) (v, y). u = v) :]) ∘ [:(v, y)↝v'. v' = v:])  
      = {:x ↝ (u, x'). p (u, x) ∧ x = x':} ∘ [:u,x ↝ v . ∃ y . r (u,x) (u, y) ∧ v = u:]")
   apply (simp add: Prod_angelic_demonic_Skip)
   apply (simp add: fun_eq_iff demonic_def angelic_def assert_def le_fun_def, auto)
  by (simp add: fun_eq_iff demonic_def angelic_def assert_def le_fun_def)

    
  lemma feedbackB_decomp: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ 
      feedbackB ( {. u, x . p (u, x) ∧ p' x.} o [:u, x ↝ v, y . r (u, x) y ∧ r' x v:])
       = {. x . p' x ∧ (∀b. r' x b ⟶ p (b,x)).} o [:x ↝ y . ∃ v . r' x v ∧ r (v, x) y:]"
    apply (unfold feedbackB_spec, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec angelic_def)
    apply auto
    by metis

  lemma [simp]: "prec S = ⊤ ⟹ prec (feedback S) = ⊤"
    by (simp add: feedback_def)

  lemma feedback_simp_a: "feedback ({.p.} o [:r:]) = 
    {. λx. (∃u. p (u, x)) ∧ (∀a. (∃u. p (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ p (a, x)) .} ∘
    [:x ↝ y  . (∃ v .(∃u. p (u, x) ∧ (∃y. r (u, x) (v, y))) ∧  r (v, x) (v, y)):]"
    apply (simp add: feedback_def selectc_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: comp_assoc [THEN sym]  comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def)
    by (simp add: inf_fun_def)
      
lemma feedbackA_simp_a: "feedbackA ({.p.} o [:r:]) = 
    {. x. ∃u. p (u, x) .} ∘ [:x ↝ z. ∃a. p (a, x) ∧ r (a, x) (a, z):]"
    apply (simp add: feedbackA_def selectA_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
  apply (simp add: comp_assoc [THEN sym]  comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def)
    by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, blast)


  lemma feedback_simp_b: "feedback ({.p.} o [-q→f-]) = 
    {. λx. (∃u. p (u, x)) ∧ (∀u. p (u, x) ∧ q (u, x) ⟶ p (fst (f (u, x)), x)) .} ∘
    [:x ↝ y  . (∃ u . p (u, x) ∧ q (u, x) ∧ q (fst (f (u, x)), x) ∧ fst (f (u, x)) = fst (f (fst (f (u, x)), x)) ∧ y = snd (f (fst (f (u, x)), x))):]"
    by (simp add: feedback_simp_a grd_update_def fun_eq_iff demonic_def assert_def le_fun_def pair_eq, auto)

  lemma feedback_simp_c: "feedback ({.p.} o [-f-]) = 
    {. x. (∃u. p (u, x)) ∧ (∀u. p (u, x) ⟶ p (fst (f (u, x)), x)) .} ∘
    [:x ↝ y  . (∃ u . p (u, x) ∧ fst (f (u, x)) = fst (f (fst (f (u, x)), x)) ∧ y = snd (f (fst (f (u, x)), x))):]"
    by (cut_tac p = p and f = f and q = ⊤ in feedback_simp_b, simp)

  lemma feedback_simp_cc: "feedback ([-f-]) = 
    [:x ↝ y  . (∃ u . fst (f (u, x)) = fst (f (fst (f (u, x)), x)) ∧ y = snd (f (fst (f (u, x)), x))):]"
    by (cut_tac p = ⊤ and f = f in feedback_simp_c, simp add: assert_true_skip_a assert_true_skip)


  lemma feedback_test: "feedback ([-(λ (u,x) . (u , u))-]) = [:⊤:]"
    by (simp add: feedback_simp_cc fun_eq_iff demonic_def le_fun_def)

  lemma feedback_simp_d: "feedback [:r:] = [: x ↝ y . ∃ v . r (v, x) (v, y):]"
    apply (cut_tac p = ⊤ and r = r in feedback_simp_a)
    apply simp
    apply (subgoal_tac "(λx y. ∃v. (∃u y. r (u, x) (v, y)) ∧ r (v, x) (v, y)) = (λx y. ∃v. r (v, x) (v, y))")
    by (auto simp add: fun_eq_iff assert_true_skip assert_true_skip_a )

  lemma feedback_update_simp: "feedback ( {.p.} o [- λ (u, x) . (f x, g (u, x))-])
       = {. x . p (f x, x).} o [-λ x . g (f x, x)-]"
    apply (unfold feedback_simp_c, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec update_def)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis

  lemma feedback_update_simp_x: "feedback ( {. p.} o [- λ ux . (f (snd ux), g ux)-])
       = {. x . p (f x, x).} o [-λ x . g (f x, x)-]"
    apply (unfold feedback_simp_c, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec update_def)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis

  lemma feedback_update_simp_a: "feedback ( {.p.} o [- λ (u, s, x) . (f (s, x), g (u, s, x), h (u, s, x)) -])
       = {. s, x . p ((f (s, x)), s, x).} o [-λ (s, x) . (g ((f (s, x)), s, x), h ((f (s, x)), s, x))-]"
    apply (cut_tac p = p and f = f and g = "λ (u, s, x) . (g (u, s, x), h (u, s, x))" in feedback_update_simp_x)
    apply (unfold feedback_simp_c, simp)
    by (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec update_def)

  lemma feedback_update_simp_b: "feedback ( {.p.} o [- λ (u, s, x) . (f (s, x), g (u, s, x), h (u, s, x)) -])
       = {. s, x . p ((f (s, x)), s, x).} o [-λ (s, x) . (g ((f (s, x)), s, x), h ((f (s, x)), s, x))-]"
    apply (cut_tac p = p and f = f and g = "λ (u, s, x) . (g (u, s, x), h (u, s, x))" in feedback_update_simp)
    apply (simp add: feedback_update_simp)
    apply (unfold feedback_simp_c, simp)
    by (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec update_def)

  lemma feedback_update_simp_c: "feedback ( {. (u, s, x) . p u s x .} o [- λ (u, s, x) . (f s x, g u s x, h u s x) -])
       = {. s, x . p (f s x) s x.} o [-λ (s, x) . (g (f s x) s x, h (f s x) s x)-]"
    apply (unfold feedback_simp_c, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec update_def)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis

  lemma feedback_simp_bot: "feedback (⊥::(('a × 'b) ⇒ bool) ⇒ ('a × 'c) ⇒ bool) = ⊥"
    proof -
      have [simp]: "((⊥::(('a × 'b) ⇒ bool) ⇒ ('a × 'c) ⇒ bool)) =  ({.⊥::'a × 'c ⇒ bool.} o [:⊥ :: 'a ×'c ⇒ 'a × 'b ⇒ bool:])"
        by (simp add: feedback_simp_a fun_eq_iff assert_def)
      show "feedback (⊥::(('a × 'b) ⇒ bool) ⇒ ('a × 'c) ⇒ bool) = ⊥"
        by (simp add: feedback_simp_a fun_eq_iff assert_def)
    qed

  lemma "A = {.p.} o [-λ (a, b) . (c b, d (a, b))-] ⟹ B = {.p'.} o [-f-] ⟹ feedback (A o (B ** Skip)) 
          =  {. x . p (f (c x), x) ∧ p' (c x) .} ∘ [-λx . d (f (c x), x)-]"
    apply (simp add: prod_assert_update_skip comp_update_update comp_update_assert update_assert_comp assert_assert_comp comp_assoc [THEN sym])
    apply (simp add: fun_comp_simp)
    apply (cut_tac p = "p ⊓ ((λ(x, y). p' x) ∘ (λ(a, b). (c b, d (a, b))))" and f = "f o c" and g = d in feedback_update_simp)
    by simp

  lemma AAA: "p = p' ⟹ (⋀ x . p x ⟹ r x = r' x) ⟹ {.p.} o [:r:] = {.p'.} o [:r':]"
    by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, auto)

  thm feedback_simp_a
    

    
  lemma "A = {.p.} o [-λ (a, b) . (c b, d (a, b))-] ⟹ B = {.p'.} o [-f-] ⟹ feedback ((B ** Skip) o A) 
          =  {. x . p (f (c x), x) ∧ p' (c x) .} ∘ [-λx . d (f (c x), x)-]"
    apply (simp add: prod_assert_update_skip comp_update_update comp_update_assert update_assert_comp assert_assert_comp comp_assoc [THEN sym])
    apply (simp add: fun_comp_simp_b)
    apply (cut_tac p = " (λ(x, y). p' x) ⊓ (p ∘ (λ(x, y). (f x, y)))" and f = "c" and g = "λ (x, y) . d (f x, y)" in feedback_update_simp)
    by (simp add: update_def demonic_def fun_eq_iff assert_def le_fun_def, auto)
 

  lemma "A = {.p.} o [-λ (a, b) . (c b, d (a, b))-] ⟹ B = {.p'.} o [-f-] ⟹ 
        feedback (feedback ([-λ (a,c,b) . ((a,b), c)-] o (A ** B) o [-λ ((c, d), a) . (a,c,d)-] )) =  {. x . p (f (c x), x) ∧ p' (c x) .} ∘ [-λx . d (f (c x), x)-]"
    apply (simp add: prod_assert_update comp_update_update comp_update_assert update_assert_comp assert_assert_comp comp_assoc [THEN sym])
    apply (simp add: fun_comp_simp_c)
    apply (cut_tac p = "(λ(x, y). p x ∧ p' y) ∘ (λ(a, c, b). ((a, b), c)) " and f = "λ (v, w) . f v" and g = "λ(u, v, w) . (c w, d (u, w))" in feedback_update_simp)
    apply (subgoal_tac "(λ(u, x). (case x of (v, w) ⇒ f v, case (u, x) of (u, v, w) ⇒ (c w, d (u, w)))) = (λ(u, v, w). (f v, c w, d (u, w)))")
    apply simp
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply simp
    apply (simp add: fun_comp_simp_d fun_comp_simp_e)
    apply (cut_tac p = "  λ(u, v). p (f u, v) ∧ p' u " and f = "c" and g = "λ (x, y) . d (f x, y)" in feedback_update_simp)
    apply (simp add: update_def demonic_def fun_eq_iff assert_def le_fun_def)
    by (simp_all add: fun_eq_iff)
  lemma feedback_simp_aa: "feedback ({.inpt r.} o [:r:]) = 
    {. λx. (∃u. inpt r (u, x)) ∧ (∀a. (∃u. inpt r (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ inpt r (a, x)).} ∘
    [:x ↝ y  . (∃ v .(∃u.  (∃y. r (u, x) (v, y))) ∧  r (v, x) (v, y)):]"
    apply (simp add: feedback_def selectc_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: comp_assoc [THEN sym] comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def)
    apply (simp add: inf_fun_def)
    apply (simp add: fun_eq_iff demonic_def assert_def inpt_def le_fun_def, auto)
    apply (drule_tac x = xb in spec, safe, simp)
    apply metis
    by metis


  lemma feedback_in_simp_aux: "((∃u. inpt r (u, x)) ∧ (∀a. (∃u. inpt r (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ inpt r (a, x))) 
          = ((∃u. inpt r (u, x)) ∧ (∀a. (∃u y. r (u, x) (a, y)) ⟶ inpt r (a, x)))"
    apply (simp add: fun_eq_iff inpt_def)
    apply auto
    apply metis
    by metis

  lemma feedback_simp_aaa: "feedback ({.inpt r.} o [:r:]) = 
    {. λx. (∃u. inpt r (u, x)) ∧ (∀a. (∃u. inpt r (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ inpt r (a, x)).} ∘
    [:x ↝ y  . (∃ v .  r (v, x) (v, y)):]"
    apply (simp add: feedback_def selectc_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: comp_assoc [THEN sym] comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def)
    apply (simp add: inf_fun_def)
    apply (simp add: fun_eq_iff demonic_def assert_def inpt_def le_fun_def, auto)
    apply (drule_tac x = xb in spec, safe, simp)
    by metis
      
  lemma feedbackB_simp_aaaa: "feedbackB ({.inpt r.} o [:r:]) = 
   {:x ↝ (u, x').inpt r (u, x) ∧ (∀v. (∃y. r (u, x) (v, y)) ⟶ inpt r (v, x)) ∧ x = x':} ∘ [:(u, x)↝y.∃v. (∃y'. r (u, x) (v, y')) ∧ r (v, x) (v, y):]"
    by (simp add: feedbackB_spec)

  lemma feedbackB_simp_aaaaa: "p ≤ inpt r ⟹ feedbackB ({.p.} o [:r:]) = 
   {:x ↝ (u, x'). p (u, x) ∧ (∀v. (∃y. r (u, x) (v, y)) ⟶ p (v, x)) ∧ x = x':} ∘ [:(u, x)↝y.∃v. (∃y'. r (u, x) (v, y')) ∧ r (v, x) (v, y):]"
    by (simp add: feedbackB_spec)
      
      
  lemma feedback_simp_aaaa: "feedback ({.inpt r.} o [:r:]) = 
    {. λx.((∃u. inpt r (u, x)) ∧ (∀a. (∃u y. r (u, x) (a, y)) ⟶ inpt r (a, x))).} ∘
    [:x ↝ y  . (∃ v .  r (v, x) (v, y)):]"
    by (simp add: feedback_simp_aaa feedback_in_simp_aux)
 
  lemma feedback_simp_aaaaa: "p ≤ inpt r ⟹ feedback ({.p.} o [:r:]) = 
    {. λx.((∃u. p (u, x)) ∧ (∀a. (∃u y. p (u, x) ∧ r (u, x) (a, y)) ⟶ p (a, x))).} ∘
    [:x ↝ y  . (∃ v .  p (v, x) ∧ r (v, x) (v, y)):]"
    apply (cut_tac r = "λ x y . p x ∧ r x y" in  feedback_simp_aaaa)
    by (simp add: prec_rel)


  lemma "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ feedback ([- λ (x, y, z) . ((x, y), z) -] o (({.p.} o [:r:]) ** ({.p'.} o [:r':])) o [- λ ((x, y), z) . (x, y, z) -]) = 
    (feedback ({.p.} o [:r:])) ** ({.p'.} o [:r':])"
    apply (simp add: Prod_spec update_def comp_assoc[THEN sym] demonic_demonic OO_def demonic_assert_comp)
    apply (simp add: comp_assoc demonic_demonic OO_def)
    apply (simp add: feedback_simp_aaaaa)
    apply (simp add:  Prod_spec)
    apply (subst feedback_simp_aaaaa)
    apply (simp add: inpt_def le_fun_def)
    apply (rule AAA)
    apply (simp_all add: fun_eq_iff)
    apply safe
    apply blast
    apply (drule_tac x = aa in spec, safe)
    apply simp
    apply (drule_tac x = ua in spec, simp_all, safe)
    apply blast
    apply (simp add: le_fun_def inpt_def,blast)
    apply blast
    apply blast
    apply blast
    by blast

  lemma feedback_in_simp_a: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ 
      feedback ( {. u, x . p (u, x) ∧ p' x.} o [:u, x ↝ v, y . r (u, x) y ∧ r' x v:])
       = {. x . p' x ∧ (∀b. r' x b ⟶ p (b,x)).} o [:x ↝ y . ∃ v . r' x v ∧ r (v, x) y:]"
    apply (unfold feedback_simp_a, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis

  lemma feedback_in_simp_b: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ 
      feedback ( {. u, x . p (u, x) ∧ p' x.} o [:u, x ↝ v, y . r (u, x) y ∧ r' x v:])
       = {. x . p' x ∧ (∀b. r' x b ⟶ p (b,x)).} o [:x ↝ y . ∃ v . r' x v ∧ r (v, x) y:]"
    apply (unfold feedback_simp_a, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis
  lemma "p ≤ inpt r ⟹ p'' ≤ inpt r'' ⟹ feedback ( (Skip ** ({.p.} o [:r:])) o ([-λ(x,y) . (y,x)-]) o (Skip ** ({.p''.} o [:r'':])) ) 
      = ({.p.} o [:r:]) o ({.p''.} o [:r'':])"
    apply (simp add: Prod_spec update_def comp_assoc[THEN sym] demonic_demonic OO_def demonic_assert_comp Prod_Skip_spec)
    apply (simp add: comp_assoc demonic_demonic OO_def)
    apply (simp add: Prod_spec update_def comp_assoc[THEN sym] demonic_demonic OO_def demonic_assert_comp Prod_Skip_spec assert_assert_comp)
    apply (simp add: comp_assoc demonic_demonic OO_def)
    apply (simp add: feedback_simp_a)
    apply (simp add: inpt_def le_fun_def)
    apply (rule AAA, safe)
    apply (simp add: fun_eq_iff le_fun_def, safe)
    by blast+

  lemma feedback_update_simp_aaa: "(⋀ u x. fst(f(u,x)) = fst(f(undefined,x))) ⟹
    feedback({.p.} o [-f-]) = {.x. p(fst(f(undefined, x)), x).} ∘ [- λx. snd(f(fst(f(undefined,x)),x))-] "
    apply (cut_tac f = "(λx. fst(f(undefined, x)))" and g = "(λ(u,x). snd(f(u, x)))" in feedback_update_simp)
    apply (subgoal_tac "f = (λ(u, x). (fst(f(undefined,x)), snd(f(u,x))))")
    apply (simp_all add:fun_eq_iff)
    apply (drule drop_assumption)
    apply (simp)
    by (metis pair_eq)

  lemma feedback_update_simp_bbb: "(⋀ u x. fst(f(u,x)) = fst(f(undefined,x))) ⟹
    feedback([-f-]) = [- λx. snd(f(fst(f(undefined,x)),x))-] "
    apply (cut_tac p = "(λ(x, s).True)" and f = f in feedback_update_simp_aaa)
    by (simp_all add: Refinement.assert_true_skip_a )

  thm feedback_def

  thm feedback_in_simp_a
   
  definition "feedbackless S = (SOME T . ∃ p f . S = {.p.} o [-f-] ∧ T = {.x. p(fst(f(Eps (λ u . p (u, x)), x)), x).} ∘ [- λx. snd(f(fst(f(Eps (λ u . p (u, x)),x)),x))-]) "

  definition "fstsome p x = Eps (λ u . p (u, x))"

  definition "fbv p f x = fst(f(fstsome p x, x))"

  definition "fb_prec p f x = p(fbv p f x, x)"
  definition "fb_func p f x = snd(f(fbv p f x, x))"

  lemma fb_prec_simp: "fb_prec p f = (λ x . p(fbv p f x, x))"
    by (simp add: fun_eq_iff fb_prec_def)

  lemma fb_func_simp: "fb_func p f = (λ x . snd(f(fbv p f x, x)))"
    by (simp add: fun_eq_iff fb_func_def)

  lemma feedbackless_update_simp_aaa: "feedbackless({.p.} o [-f-]) = {.fb_prec p f.} ∘ [- fb_func p f -] "
      apply (simp add: feedbackless_def fbv_def fstsome_def fb_prec_simp fb_func_simp)
      apply (rule some_equality)
      apply auto [1]
      apply safe
      apply (simp add: assert_update_eq, safe)
      apply (simp add: fun_eq_iff, safe)
      apply (metis someI)
      apply (metis someI)
      by (metis someI)

  lemma "(⋀ u x. fst(f(u,x)) = fst(f(undefined,x))) ⟹ feedback({.p.} o [-f-]) = feedbackless({.p.} o [-f-])"
    apply (simp add: feedback_update_simp_aaa feedbackless_update_simp_aaa)
    apply (subgoal_tac "(λ x. p (fst (f (undefined, x)), x)) = fb_prec p f")
    apply (subgoal_tac "(λx. snd (f (fst (f (undefined, x)), x))) = fb_func p f")
    apply simp
    apply (simp add: fun_eq_iff fb_func_def fbv_def, auto)
    apply metis
    apply (simp add: fun_eq_iff fb_prec_def fbv_def, auto)
    apply metis
    by metis

      
  lemma feedbackless_update_simp_bbb: "feedbackless([-f-]) = [- fb_func ⊤ f -] "
    apply (cut_tac p = "λ (u,x) . True" and f = f in feedbackless_update_simp_aaa)
    apply (simp_all add: Refinement.assert_true_skip_a update_eq top_fun_def fb_prec_simp fb_func_simp)
    by (simp add: split_def)

  lemma feedback_update_simp_ccc: "feedback( {.⊥.} o [-f-]) = ⊥"
    apply (subgoal_tac "{.⊥.} o [-f-] = ⊥")
    apply (simp add: feedback_simp_bot)
    by (simp add: assert_false_fail)



  subsubsection‹Different Feedback Attempts›

  definition "select'' S = [:x ↝ u, x' . x' = x ∧ prec S (u, x) :] o S o [:v, y ↝ v' . v' = v:]"

  definition "selectb S = {: x ↝ u, x'. x = x' ∧ prec S (u, x):} o S o [:v, y ↝ v' . v' = v:]"

  definition "selectd S = [:x ↝ u, x' . x' = x ∧ prec S (u, x) :] o S o [:v, y ↝ v' . v' = v:]"

  definition "selecte S = [:x ↝ u, x' . x' = x ∧ grd S (u, x) :] o S o [:v, y ↝ v' . v' = v:]"

  definition "feedbackf S = {. x . (∃ u . prec S (u, x)).} o [:x ↝ (u, x'), u' . x' = x ∧ u' = u ∧ prec S (u, x) :] 
        o (S ** Skip) o [:(v, y), u ↝ (v', y') . v = u ∧ v' = v ∧ y' = y:]"

  definition "feedbackg S = [:x ↝ (u, x'), u' . x' = x ∧ u' = u ∧ grd S (u, x) :] o (S ** Skip) o [:(v, y), u ↝ v', y' . v = u ∧ y' = y ∧ v' = v:]"
  
  lemma selectc''_spec: "select'' ({. p .} o [:r:]) = [:x ↝ v . ∃ u y . p (u, x) ∧ r (u,x) (v,y) :]"
    by (simp add: select''_def fun_eq_iff demonic_def assert_def le_fun_def, auto)

  lemma selectcb_spec: "selectb ({. p .} o [:r:]) = {: x ↝ u,x'. x = x' ∧  p (u, x):} o [:u, x ↝ v . ∃ y . p (u, x) ∧ r (u,x) (v,y) :]"
    by (simp add: selectb_def fun_eq_iff demonic_def assert_def le_fun_def inf_fun_def angelic_def)

 lemma feedbackf_spec: "feedbackf ({. p .} o [:r:]) = {. x . (∃ u . p (u, x)).} o [:x ↝ u, y . p (u, x) ∧ r (u,x) (u,y) :]"
    by (simp add: feedbackf_def fun_eq_iff demonic_def assert_def le_fun_def Prod_spec_Skip, auto)

  lemma feedbackg_spec: "feedbackg ({. p .} o [:r:]) = {. x . (∀ u . p (u, x)).} o [:x ↝ u, y .r (u,x) (u,y) :]"
    by (simp add: feedbackg_def fun_eq_iff demonic_def assert_def le_fun_def Prod_spec_Skip grd_def, auto)

  lemma selectd_spec: "selectd ({. p .} o [:r:]) = [:x ↝ u, x' . x' = x ∧ p (u, x) :] o [:r:] o [:v, y ↝ v' . v' = v:]"
    by (simp add: selectd_def fun_eq_iff demonic_def assert_def le_fun_def)

  lemma selecte_spec: "selecte ({. p .} o [:r:]) = {.x . ∀ u . p (u, x).} o [:x ↝ v . ∃ u y . r (u, x) (v, y):]"
    by (simp add: selecte_def fun_eq_iff demonic_def assert_def le_fun_def grd_def, auto)

 
  definition "feedback' S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((select S) ** Skip) o S o [:u,y ↝ y' . y' = y:]"
  definition "feedback'' S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((select'' S) ** Skip) o S o [:u,y ↝ y' . y' = y:]"


  definition "feedbacka S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((select S) ** Skip) o (S ∥ [:u, x ↝ v, y . u = v:])"
  definition "feedbackb S = [:x ↝ x', x'' . x' = x ∧ x'' = x:] o ((selectb S) ** Skip) o (S ∥ [:u, x ↝ v, y . u = v:]) o [:u,y ↝ y' . y' = y:]"

  lemma feedback_simp_a_a: "feedback' ({.p.} o [:r:]) = 
    {. x. (∃u. p (u, x)) ∧  (∀a. (∃u. p (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ p (a, x)) .} ∘
    [: λx y. ∃a aa. (∃u. p (u, x) ∧ (∃y. r (u, x) (aa, y))) ∧ r (aa, x) (a, y) :]"
    apply (simp add: feedback'_def selectc_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: demonic_def assert_def le_fun_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert comp_existsa)
    by (simp add: inf_fun_def)

  lemma feedback_simp_a_b: "feedback'' ({.p.} o [:r:]) = 
   {. λx. ∀a. (∃u. p (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ p (a, x) .} ∘ [: λx y. ∃a aa. (∃u. p (u, x) ∧ (∃y. r (u, x) (aa, y))) ∧ r (aa, x) (a, y) :]"
    apply (simp add: feedback''_def selectc''_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    by (simp add: demonic_def assert_def le_fun_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert comp_existsa)

  lemma feedbackb_simp_a: "feedbackb ({.p.} o [:r:]) = 
    {:x ↝ u, x' . x = x' ∧ p (u, x) ∧ (∀a. ((∃y. r (u, x) (a, y))) ⟶ p (a, x)) :} ∘
    [:u, x ↝ y  . (∃ v .( (∃y. r (u, x) (v, y))) ∧  r (v, x) (v, y)):]"
    apply (simp add: feedbackb_def selectcb_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: demonic_def assert_def le_fun_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert comp_existsa)
    apply (simp add: inf_fun_def fun_eq_iff Prod_angelic_demonic_Skip assert_def demonic_def le_fun_def angelic_def, auto)
    by metis
    
  lemma feedbackb_simp_aa: "feedbackb ({.inpt r.} o [:r:]) = 
    {:x ↝ u, x' . x = x' ∧ inpt r (u, x) ∧ (∀a. ((∃y. r (u, x) (a, y))) ⟶ inpt r (a, x)) :} ∘
    [:u, x ↝ y  . (∃ v .( (∃y. r (u, x) (v, y))) ∧  r (v, x) (v, y)):]"
    apply (simp add: feedbackb_def selectcb_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: demonic_def assert_def le_fun_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert comp_existsa)
    apply (simp add: inf_fun_def fun_eq_iff Prod_angelic_demonic_Skip assert_def demonic_def le_fun_def angelic_def inpt_def, auto)
    apply metis
    by metis

  lemma feedbacka_simp_a: "feedbacka ({.p.} o [:r:]) = 
    {. λx. (∃u. p (u, x)) ∧ (∀a. (∃u. p (u, x) ∧ (∃y. r (u, x) (a, y))) ⟶ p (a, x)) .} ∘
    [: λx (v, y) . (∃u. p (u, x) ∧ (∃y. r (u, x) (v, y))) ∧ r (v, x) (v, y):]"
    apply (simp add: feedbacka_def selectc_spec Prod_spec_Skip comp_demonic_demonic comp_existsa  fusion_spec_demonic)
    apply (simp add: demonic_def assert_def le_fun_def Prod_spec_Skip Prod_Skip_spec Prod_demonic_skip Prod_skip_demonic Prod_demonic Prod_spec_demonic Prod_demonic_spec
     comp_assoc [THEN sym] demonic_demonic comp_demonic_demonic assert_assert_comp comp_demonic_assert demonic_assert_comp OO_def Prod_spec Fail_assert comp_existsa)
    apply (simp add: inf_fun_def)
    by (auto simp add: le_fun_def demonic_def fun_eq_iff assert_def)

  lemma feedback_in_simp_a_a: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ 
      feedback' ( {. u, x . p (u, x) ∧ p' x.} o [:u, x ↝ v, y . r (u, x) y ∧ r' x v:])
       = {. x . p' x ∧ (∀b. r' x b ⟶ p (b,x)).} o [:x ↝ y . ∃ v . r' x v ∧ r (v, x) y:]"
    apply (unfold feedback_simp_a_a, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis

  lemma feedbacka_in_simp_a: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ 
      feedbacka ( {. u, x . p (u, x) ∧ p' x.} o [:u, x ↝ v, y . r (u, x) y ∧ r' x v:])
       = {. x . p' x ∧ (∀b. r' x b ⟶ p (b,x)).} o [:x ↝ v, y . r' x v ∧ r (v, x) y:]"
    apply (unfold feedbacka_simp_a, simp)
    apply (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec)
    apply safe
    apply metis
    apply metis
    apply metis
    apply metis
    by metis


  lemma feedbacka_simp_b: "feedbacka [:r:] = [: x ↝ v, y . r (v, x) (v, y):]"
    apply (cut_tac p = ⊤ and r = r in feedbacka_simp_a)
    apply simp
    apply (subgoal_tac "(λx (v, y). (∃u y. r (u, x) (v, y)) ∧ r (v, x) (v, y)) = ( λx (v, y). r (v, x) (v, y))")
    by (auto simp add: assert_true_skip assert_true_skip_a )

  subsubsection‹Feedback of Decomposable Components›
definition "decomposable r r' r'' = (∀ u x v y . r (u, x) (v, y) = ((r' x v) ∧ r'' (u, x) y))"
  
lemma decomposabel_iff: "(∃ r' r'' . decomposable r r' r'') = ((∀ u x v y . r (u, x) (v, y) = ((∃ u y . r (u, x) (v, y)) ∧ (∃ v . r (u, x) (v, y))) ))"
  apply safe
     apply blast
    apply blast
   apply (simp add: decomposable_def)
  apply (rule_tac x = "(λ x v . (∃ y u' . r (u', x) (v, y)))" in exI)
  apply (rule_tac x = "(λ (u,x) y . (∃ v . r (u,x) (v, y)))" in exI)
    by (unfold decomposable_def, blast)

lemma decomposable_calc: "(∃ r' r'' . decomposable r r' r'') ⟹ decomposable r (λ x v . (∃ y u' . r (u', x) (v, y))) (λ (u,x) y . (∃ v . r (u,x) (v, y)))"
  by (simp add: decomposable_def, blast)

    
lemma decomposable_inpt: "decomposable r r' r'' ⟹ inpt r (u, x) = (inpt r' x ∧ inpt r'' (u, x))"
  by (simp add: decomposable_def inpt_def)
  

lemma decomposable_feedback_trs: "decomposable r r' r'' ⟹ feedback (trs r) 
  = {. x . inpt r' x ∧ (∀b. r' x b ⟶ inpt r'' (b, x)).} ∘ [:x↝y.∃v. r' x v ∧ r'' (v, x) y:]"
proof -
  assume [simp]: "decomposable r r' r''"
  from this have A: "r = (λ (u, x) (v, y) . (r'' (u, x) y ∧ (r' x v)))"
    by (unfold decomposable_def, auto simp add: fun_eq_iff)
  have "feedback (trs r) = feedback ({. u, x . inpt r (u, x).} ∘ [: r :])"
    by (simp add: trs_def)
  also have "... = feedback ({.(u, x).inpt r' x ∧ inpt r'' (u, x).} ∘ [: r :])"
    by (subst decomposable_inpt [of r r' r''], simp_all)
  also have "... = feedback ({.(u, x). inpt r'' (u, x) ∧ inpt r' x.} ∘ [: (u, x)↝(v, y). r'' (u, x) y ∧ r' x v :])"
    apply (subst A)
    apply (subgoal_tac "(λ (u, x).inpt r' x ∧ inpt r'' (u, x)) = (λ (u, x).inpt r'' (u, x) ∧ inpt r' x)")
    by auto
  also have "... = {. x . inpt r' x ∧ (∀b. r' x b ⟶ inpt r'' (b, x)).} ∘ [:x↝y.∃v. r' x v ∧ r'' (v, x) y:]"
    by (subst feedback_in_simp_a, simp_all)
  finally show "feedback (trs r) = {. x . inpt r' x ∧ (∀b. r' x b ⟶ inpt r'' (b, x)).} ∘ [:x ↝ y.∃v. r' x v ∧ r'' (v, x) y:]"
    by simp
qed

lemma spec_eq: "(⋀ x . p x = p' x) ⟹ (⋀ x y . p x ⟹ r x y = r' x y) ⟹ {.p.} o [:r:] = {.p'.} o [:r':]"
  by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, auto)

theorem "decomposable r r' r'' ⟹  feedback (trs r) 
    = trs (λ x y . (∀v. r' x v ⟶ inpt r'' (v, x)) ∧ (∃v. r' x v ∧ r'' (v, x) y))"
  apply (simp add: decomposable_feedback_trs )
  apply (simp add: trs_def)
  apply (rule spec_eq)
   apply (auto simp add: inpt_def)
  by blast

  
lemma [simp]: "((∃u. p u x) ∧ (∃v. Ex (r v)) ∧ (∀a. (∃u. p u x) ∧ (∃v. Ex (r v)) ∧ Ex (r a) ⟶ p a x)) 
  = (((∃v. Ex (r v)) ∧ (∀ a . Ex (r a) ⟶ p a x)))"
  by auto

definition "Decomposable r = (∃ r' r'' . decomposable r r' r'')"
  
definition "fst_dec r = (λ x v . ∃ u y . r (u, x) (v, y))"
definition "snd_dec r = (λ (u, x) y . ∃ v . r (u, x) (v, y))"
  
lemma decomosable_fst_snd: "Decomposable r = (decomposable r (fst_dec r) (snd_dec r))"
  apply (simp add: Decomposable_def decomposable_def fst_dec_def snd_dec_def, safe)
     apply blast
    apply blast
   apply blast
  apply (rule_tac x = "fst_dec r" in exI)
  apply (rule_tac x = "snd_dec r" in exI)
  by (unfold fst_dec_def snd_dec_def, blast) 

definition "state_determ r = (∀ x y y' s s' s'' . r (s, x) (s', y) ∧ r (s, x) (s'', y') ⟶ s' = s'')"
    
lemma decomposable_and: "decomposable r r' r'' ⟹ decomposable (λ (u, x) (v, y) . p(u, x) ∧ r (u,x) (v, y)) r' (λ (u,x) y . p (u, x) ∧ r'' (u, x) y)"
  by (simp add: decomposable_def, auto)

end