Theory ReactiveFeedback

(**-----------------------------------------------------------------------------
 * © [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‹\label{ReactiveFeedback}Reactive Feedback›

theory ReactiveFeedback
  imports TransitionFeedback IterateOperators

begin

definition "Feedback S = {:x ↝ (u, y), x' . (x = x'):} o IterateOmegaA ([-λ ((u, y), x) . ((u, x), x)-] o (S ** Skip)) o [-λ ((u,y), x) . y -]"


lemma Feedback_refin: "S ≤ T ⟹ Feedback S ≤ Feedback T"
  apply (simp add: Feedback_def)
  apply (rule refin_comp_right)
  apply (rule refin_comp_left, simp_all)
  apply (rule IterateOmegaA_refin)
   apply (rule mono_comp_a)
    apply simp_all
  apply (rule refin_comp_left, simp_all)
  by (rule prod_mono1, simp)

(*Feedback attempt for property transformers. Not good for input incomplete systems*)
definition "FeedbackX Init S = [:x ↝ (u, y), x' . (u = ()) ∧ (x = x'):] o ((Init ** Skip) ** Skip) o IterateOmega ([-λ ((u, y), x) . ((u, x), x)-] o (S ** Skip)) o [-λ ((u,y), x) . y -]"

(*Similar to FeedbackX but using IterateOmegaA instead of IterateOmega*)
definition "FeedbackA Init S = [:x ↝ (x'', y), x' . (x'' = x) ∧ (x = x'):] o ((Init ** Skip) ** Skip) o IterateOmegaA ([-λ ((u, y), x) . ((u, x), x)-] o (S ** Skip)) o [-λ ((u,y), x) . y -]"

lemma feedback_update_simp_e: "feedback ([- λ (u, s, x) . (f s x, g u s x, h u s x) -])
     = [-λ (s, x) . (g (f s x) s x, h (f s x) s x)-]"
  apply (unfold feedback_simp_cc, simp)
  by (simp add: fun_eq_iff assert_def demonic_def le_fun_def inpt_def rel_spec update_def)

definition "InitDF init = [: s ↝ s'. (□(λs. init (s (0::nat)))) s' :]"

definition "Add = [- λ(x,y). x+y-]"
definition "UD = [-λ(x,s). (s,x) -]"
definition "Split = [-λx. (x,x)-]"

definition "RT1 = [- λ(u, (s,x)). ((u,x),s)-]"
definition "RT2 = [- λ((v,y),s). (v, (s,y)) -]"
definition "RT3 = [- λ(x,s). (s,x)-]"

definition "Res  = [-λx. Summ x-]"

definition "init_ExFb = (λ u . u = (0::nat))" 
definition "ExFb = RT1 o (Add ** Skip) o UD o (Split ** Skip) o RT2"

lemma ExFb_simp : "ExFb = [- λ(u, (s,x)). (s, (u+x,s))-]"
  apply (simp add: ExFb_def Add_def UD_def Split_def RT1_def RT2_def update_comp prod_update_skip)
  apply (rule_tac f = "update" in arg_cong)
  by (simp add: fun_eq_iff)

 
definition "ExFb_transfb = feedback ExFb"

lemma ExFb_transfb_simp: "ExFb_transfb = [- λ(s,x). (s+x,s)-]"
  by (simp add: ExFb_transfb_def ExFb_simp feedback_update_simp_e)

definition "ExFb_genfb = DelayFeedback init_ExFb ExFb_transfb"

lemma DelayFeedback_example: "ExFb_genfb = Res"
  apply (simp add: ExFb_genfb_def ExFb_transfb_simp Res_def init_ExFb_def update_def split_def)
  apply (cut_tac init="(λ u . u = (0::nat))" and p="⊤" and r="(λx y. y=(fst x + snd x, fst x))" in DelayFeedback_simp )
  apply (simp add: prec_pre_sts_simp assert_true_skip_a  assert_true_skip)
  apply (drule drop_assumption, simp)
  apply (rule_tac f="demonic" in arg_cong)
  apply (simp add: fun_eq_iff)
  apply safe
    apply (simp_all add: rel_pre_sts_simp)
   apply (metis Nat.add_0_right sum_suc)
    using Summ.simps(1) Summ.simps(2) by blast


  definition "RT4 = [- λ(s, (u, x)). (u, (s, x)) -]"
  definition "RT5 = [- λ(v, (s, y)). (s, (v, y)) -]"

  definition "Res_aux = [-λ(u, x). ((λi. if i = 0 then 0 else u (i-1) + x (i-1)),(λi. if i = 0 then 0 else u (i-1) + x (i-1)))-]"

  definition "ExFb_delayfb_aux = RT4 o ExFb o RT5"

  lemma ExFb_delayfb_aux_simp: "ExFb_delayfb_aux = [-λ(s, (u, x)). (u+x, (s, s))-]"
    apply (simp add: ExFb_delayfb_aux_def ExFb_simp RT4_def RT5_def update_comp)
    apply (rule_tac f = "update" in arg_cong)
    by (simp add: fun_eq_iff)
 
  definition "ExFb_delayfb = [-λ(u,x). nzip u x-] o (DelayFeedback (λ u . u = (0::nat)) ExFb_delayfb_aux) o [-λx. (fst o x, snd o x)-]"


  lemma aaa_ind:"∀x. (x = 0 ⟶ aa 0 = 0) ∧ (0 < x ⟶ aa x = a (x - Suc 0) + b (x - Suc 0)) ⟹
                 ∀x. (x = 0 ⟶ ba 0 = 0) ∧ (0 < x ⟶ ba x = a (x - Suc 0) + b (x - Suc 0)) ⟹ (aa x = ba x)"
    apply (induction x)
    by simp_all

  lemma ExFb_delayfb_simp: "ExFb_delayfb = Res_aux"
    apply (simp add: ExFb_delayfb_def ExFb_delayfb_aux_simp Res_aux_def update_def split_def)
    apply (simp add: DelayFeedback_b_simp)
    apply (simp add: demonic_demonic)
    apply (rule_tac f="demonic" in arg_cong)
    apply (simp add: fun_eq_iff)
    apply safe
    apply simp_all
        apply (simp_all add: rel_pre_sts_def nzip_def always_def at_fun_def at_prod_def lift_rel_def)
      apply auto [1]
    apply (metis Suc_pred fst_conv)
      apply (metis snd_conv)
      
      apply (metis Suc_pred snd_conv)
      
    apply (simp add: OO_def nzip_def rel_pre_sts_simp)
      
    apply (rule_tac x = "nzip aa ba" in exI, simp)
    apply (rule_tac x = "nzip a b" in exI)
    apply (unfold nzip_def, simp)
    apply (rule_tac x = aa in exI, simp_all, safe)
    by (drule_tac aa = aa and ba = ba and x = i in aaa_ind, simp_all)

   
  definition "Init_ExFb = InitDF init_ExFb"


  lemma Res_aux_simp: "[-λ((u, y), x). ((u, x), x)-] ∘ Res_aux ** Skip =  [- λ((u, y), x). (((λi. if i = 0 then 0 else u (i-1) + x (i-1)),(λi. if i = 0 then 0 else u (i-1) + x (i-1))), x) -]"
    apply (simp add: Res_aux_def prod_update_skip update_comp )
    apply(rule_tac f=update in arg_cong)
    apply (simp add: o_def )
    by (subst fun_eq_iff, safe)


  definition "Res_aux_fun =  (λ((u::nat⇒nat, y::nat⇒nat), x::nat⇒nat). (((λ(i::nat). if i = (0::nat) then (0::nat) else u (i-(1::nat)) + x (i-(1::nat))), (λ(i::nat). if i = (0::nat) then (0::nat) else u (i-(1::nat)) + x (i-(1::nat)))), x))"


lemma Res_aux_fun_aux_a: "⋀ a b c . (Res_aux_fun ^^ (n::nat)) z = ((a,b), c) 
        ⟹ (∀ i < n . a i = ( Summ c (i::nat))  ∧ b i = ( Summ c (i::nat))) ∧ c = (snd z)"
    apply (induction n, simp_all)
    apply (subst (asm) (2)  Res_aux_fun_def)
    apply (case_tac "(Res_aux_fun ^^ n) z", simp)
    apply (case_tac aa, simp)
    apply safe
    apply (case_tac i, simp_all)
    by (case_tac i, simp_all)

  lemma Res_aux_fun_aux_b:  "(i < n  ⟹  apply (((Res_aux_fun )^^ n) z) i = apply ((Res_aux_fun ^^ (Suc i)) z) i)"
    apply (case_tac "(Res_aux_fun ^^ Suc i) z")
    apply (case_tac "a", simp)
    apply (cut_tac a = aa and b = ba and c = b and n = "Suc i" and z = z in Res_aux_fun_aux_a, simp_all)
    apply (case_tac "(Res_aux_fun ^^ n) z")
    apply (case_tac "ab", simp)
    apply (drule Res_aux_fun_aux_a)
    by (simp add: apply_def)


lemma Res_aux_fun_aux_c: "(λx. let z = λi. apply (Res_aux_fun ((Res_aux_fun ^^ i) x)) i in ((fst ∘ fst ∘ z, snd ∘ fst ∘ z), snd ∘ z)) 
                = (λ x . ((Summ (snd x), Summ (snd x)), snd x) )"
    apply (simp add: fun_eq_iff Let_def, safe)
    apply (case_tac " (Res_aux_fun ((Res_aux_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Res_aux_fun_aux_a, simp_all)
    apply (simp add: apply_def)
    apply (case_tac " (Res_aux_fun ((Res_aux_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Res_aux_fun_aux_a, simp_all)
    apply (simp add: apply_def)
    apply (case_tac " (Res_aux_fun ((Res_aux_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Res_aux_fun_aux_a, simp_all)
  by (simp add: apply_def)
    

(*Examples*)

(* Example of a delayed counter system adding 1 and 2 *)

  definition "Init_adder3 = [- λx. (λ (i::nat). (2::nat))-]"
  definition "S_adder3    = [- λ (x, (x'::nat ⇒ unit)) . x-] o [- λx . (λ (i::nat). (x i) + 1)-] o [- λx . (λ (i::nat). if i = 0 then (0::nat) else x (i-1)) -] o 
                              [- λx. (λ (i::nat) . x i + 2) -] o [- λx. (x, x) -]"
  definition "Res_adder3  = [- λx . (λ (i::nat) . 3 * i + 2) -]"


  definition "S_simp_adder3 = [- λ (x,  (x'::nat ⇒ unit)). ((λi. if i = 0 then 2 else x(i-1) + 3), (λi. if i = 0 then 2 else x(i-1) + 3))-]"

  lemma S_adder3_simp: "S_adder3 = S_simp_adder3"
    apply (simp add: S_adder3_def S_simp_adder3_def)
    apply (simp add: update_comp)
    apply (rule_tac f = update in arg_cong)
    by (simp add: fun_eq_iff)

  lemma Adder3_inner_simp: "[-λ((u, y), x). ((u, x), x)-] ∘ S_simp_adder3 ** Skip =  [- λ((u, y), x). (((λi. if i = 0 then 2 else u(i-1) + 3), (λi. if i = 0 then 2 else u(i-1) + 3)), x) -]"
    apply (simp add: S_simp_adder3_def prod_update_skip update_comp )
    apply(rule_tac f=update in arg_cong)
    apply (simp add: o_def )
    by (subst fun_eq_iff, safe)


  definition "Adder3_iter_fun =  (λ((u::nat ⇒ nat, y::nat ⇒ nat), x::nat ⇒ unit). ((λi::nat. if i = (0::nat) then 2::nat else u (i - (1::nat)) + (3::nat), λi::nat. if i = (0::nat) then 2::nat else u (i - (1::nat)) + (3::nat)), x))"

  lemma Adder3_iter_aux_a: "⋀ a b c . (Adder3_iter_fun ^^ (n::nat)) z = ((a,b), c) ⟹ (∀ i < n . a i = 3 * i + 2 ∧ b i = 3 * i + 2) ∧ c = (snd z)"
    apply (induction n, simp_all)
    apply (case_tac "(Adder3_iter_fun ^^ n) z")
    apply (case_tac aa, simp)
    apply safe
    apply simp_all
    apply (subst (asm) (1) Adder3_iter_fun_def, simp)
    apply (subgoal_tac " a i = (if i = 0 then 2 else ab (i - 1) + 3)", simp)
    apply (case_tac "i", simp)
    apply simp
    apply (simp add: fun_eq_iff)
    apply (subst (asm) (1) Adder3_iter_fun_def, simp, safe)
    apply (case_tac "i", simp)
    by simp


  lemma Adder3_iter_aux_b[simp]: "i < n ⟹ apply ((Adder3_iter_fun ^^ n) z) i = apply ((Adder3_iter_fun ^^ Suc i) z) i"
    apply (case_tac "(Adder3_iter_fun ^^ Suc i) z")
    apply (case_tac "a", simp)
    apply (cut_tac a = aa and b = ba and c = b and n = "Suc i" and z = z in Adder3_iter_aux_a, simp_all)
    apply (case_tac "(Adder3_iter_fun ^^ n) z")
    apply (case_tac "ab", simp)
    apply (drule Adder3_iter_aux_a)
    by (simp add: apply_def)

  lemma Adder3_iter_aux_c: "(λx. let z = λi. apply (Adder3_iter_fun ((Adder3_iter_fun ^^ i) x)) i in ((fst ∘ fst ∘ z, snd ∘ fst ∘ z), snd ∘ z)) = (λ x . (((λ i . 3 * i + 2), (λ i . 3 * i + 2)), snd x) )"
    apply (simp add: fun_eq_iff Let_def, safe)
    apply (case_tac " (Adder3_iter_fun ((Adder3_iter_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Adder3_iter_aux_a, simp_all)
    apply (simp add: apply_def)
    apply (case_tac " (Adder3_iter_fun ((Adder3_iter_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Adder3_iter_aux_a, simp_all)
    by (simp add: apply_def)


  lemma "FeedbackX Init_adder3 S_adder3 = Res_adder3"
    apply (simp add: FeedbackX_def)
    apply (simp add: Init_adder3_def Res_adder3_def S_adder3_simp Adder3_inner_simp)
    apply (simp add: Adder3_iter_fun_def [THEN sym])
    apply (simp add: IterateOmega_func_bb Adder3_iter_aux_c)
    apply (simp add: update_comp comp_assoc prod_update_skip)
    apply(simp add: update_def demonic_demonic)
    apply (rule_tac f = demonic in arg_cong)
    by (simp add: OO_def fun_eq_iff)


  (* Example of a system computing the delayed sum of its inputs *)

  definition "Init_sum = [-λx. (λ (i::nat). (0::nat))-]"
  definition "S_sum    = [-λ(x, x'). (λi. x i + x' i) -] o [- λx . (λ (i::nat). if i = 0 then (0::nat) else x (i-1)) -] o [- λx. (x, x) -]"
  definition "Res_sum  = [-λx. Summ x-]"

  definition "S_simp_sum = [-λ(x, x'). ((λi. if i = 0 then 0 else x (i-1) + x' (i-1)),(λi. if i = 0 then 0 else x (i-1) + x' (i-1))) -]"

  lemma S_sum_simp: "S_sum = S_simp_sum" 
    apply (simp add: S_sum_def S_simp_sum_def update_comp)
    apply (rule_tac f = update in arg_cong)
    by (simp add: fun_eq_iff)


  lemma Sum_inner_simp: "[-λ((u, y), x). ((u, x), x)-] ∘ S_simp_sum ** Skip =  [- λ((u, y), x). (((λi. if i = 0 then 0 else u (i-1) + x (i-1)),(λi. if i = 0 then 0 else u (i-1) + x (i-1))), x) -]"
    apply (simp add: S_simp_sum_def prod_update_skip update_comp )
    apply(rule_tac f=update in arg_cong)
    apply (simp add: o_def )
    by (subst fun_eq_iff, safe)


  definition "Sum_iter_fun =  (λ((u::nat⇒nat, y::nat⇒nat), x::nat⇒nat). (((λ(i::nat). if i = (0::nat) then (0::nat) else u (i-(1::nat)) + x (i-(1::nat))), (λ(i::nat). if i = (0::nat) then (0::nat) else u (i-(1::nat)) + x (i-(1::nat)))), x))"


  lemma Sum_iter_aux_a: "⋀ a b c . (Sum_iter_fun ^^ (n::nat)) z = ((a,b), c) ⟹ (∀ i < n . a i = ( Summ c (i::nat))  ∧ b i = ( Summ c (i::nat))) ∧ c = (snd z)"
    apply (induction n, simp_all)
    apply (subst (asm) (2)  Sum_iter_fun_def)
    apply (case_tac "(Sum_iter_fun ^^ n) z", simp)
    apply (case_tac aa, simp)
    apply safe
    apply (case_tac i, simp_all)
    by (case_tac i, simp_all)

  lemma Sum_iter_aux_b:  "(i < n  ⟹  apply (((Sum_iter_fun )^^ n) z) i = apply ((Sum_iter_fun ^^ (Suc i)) z) i)"
    apply (case_tac "(Sum_iter_fun ^^ Suc i) z")
    apply (case_tac "a", simp)
    apply (cut_tac a = aa and b = ba and c = b and n = "Suc i" and z = z in Sum_iter_aux_a, simp_all)
    apply (case_tac "(Sum_iter_fun ^^ n) z")
    apply (case_tac "ab", simp)
    apply (drule Sum_iter_aux_a)
    by (simp add: apply_def)


lemma Sum_iter_aux_c: "(λx. let z = λi. apply (Sum_iter_fun ((Sum_iter_fun ^^ i) x)) i in ((fst ∘ fst ∘ z, snd ∘ fst ∘ z), snd ∘ z)) 
    = (λ x . ((Summ (snd x), Summ (snd x)), snd x) )"
    apply (simp add: fun_eq_iff Let_def, safe)
    apply (case_tac " (Sum_iter_fun ((Sum_iter_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Sum_iter_aux_a, simp_all)
    apply (simp add: apply_def)
    apply (case_tac " (Sum_iter_fun ((Sum_iter_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Sum_iter_aux_a, simp_all)
    apply (simp add: apply_def)
    apply (case_tac " (Sum_iter_fun ((Sum_iter_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Sum_iter_aux_a, simp_all)
    by (simp add: apply_def)


  lemma "FeedbackX Init_sum S_sum = Res_sum"
    apply (simp add: FeedbackX_def)
    apply (simp add: Init_sum_def Res_sum_def S_sum_simp Sum_inner_simp)
    apply (simp add: Sum_iter_fun_def [THEN sym])
    apply (simp add: IterateOmega_func_bb Sum_iter_aux_b Sum_iter_aux_c)
    apply (simp add: update_comp comp_assoc prod_update_skip)
    apply(simp add: update_def demonic_demonic)
    apply (rule_tac f = demonic in arg_cong)
    by (simp add: OO_def)

  (* Example of a delayed counter system with precondition adding 1 and 2 *)

  definition "Init_adder3_wp = [- λx. (λ (i::nat). (2::nat))-]"
  definition "S_adder3_wp    = [- λ (x, (x'::nat ⇒ unit)) . x-] o {.□ (λx. x 0 ≠ 0).} o [- λx . (λ (i::nat). (x i) + 1)-] o [- λx . (λ (i::nat). if i = 0 then (0::nat) else x (i-1)) -] o 
                              [- λx. (λ (i::nat) . x i + 2) -] o [- λx. (x, x) -]"
  definition "Res_adder3_wp  = {. x. True.} o [- λx . (λ (i::nat) . 3 * i + 2) -]"


  definition "S_simp_adder3_wp = {. □ (λ (x, (x'::nat ⇒ unit)). x 0 ≠ 0) .} o[- λ (x,  (x'::nat ⇒ unit)). ((λi. if i = 0 then 2 else x(i-1) + 3), (λi. if i = 0 then 2 else x(i-1) + 3))-]"


  lemma S_adder3_wp_simp: "S_adder3_wp = S_simp_adder3_wp"
    apply (simp add: S_adder3_wp_def S_simp_adder3_wp_def)
    apply (simp add: update_comp update_assert_comp comp_assoc)
    apply (rule spec_eq_iff)
    by (simp_all add: fun_eq_iff always_def at_fun_def at_prod_def)


  lemma Adder3_wp_inner_simp: "[-λ((u, y), x). ((u, x), x)-] ∘ S_simp_adder3_wp ** Skip =  {. □ (λ ((u, y), x). u 0 ≠ 0).} o [-λ((u, y), x). (((λi. if i = 0 then 2 else u(i-1) + 3), (λi. if i = 0 then 2 else u(i-1) + 3)), x)-]"
    apply (simp add: S_simp_adder3_wp_def prod_assert_update_skip update_comp)
    apply (simp add: update_assert_comp comp_assoc[THEN sym])
    apply (simp add: update_comp comp_assoc)
    apply (rule spec_eq_iff)
    by (simp_all add: fun_eq_iff always_def at_fun_def at_prod_def)


  definition "Adder3_iter_wp_fun =  (λ((u::nat ⇒ nat, y::nat ⇒ nat), x::nat ⇒ unit). ((λi::nat. if i = (0::nat) then 2::nat else u (i - (1::nat)) + (3::nat), λi::nat. if i = (0::nat) then 2::nat else u (i - (1::nat)) + (3::nat)), x))"
  definition "Adder3_iter_wp_prec = (□ (λ ((u, y), x). u 0 ≠ 0))"

  lemma Adder3_iter_wp_aux_a: "⋀ a b c . (Adder3_iter_wp_fun ^^ (n::nat)) z = ((a,b), c) ⟹ (∀ i < n . a i = 3 * i + 2 ∧ b i = 3 * i + 2) ∧ c = (snd z)"
    apply (induction n, simp_all)
    apply (case_tac "(Adder3_iter_wp_fun ^^ n) z")
    apply (case_tac aa, simp)
    apply safe
    apply simp_all
    apply (subst (asm) (1) Adder3_iter_wp_fun_def, simp)
    apply (subgoal_tac " a i = (if i = 0 then 2 else ab (i - 1) + 3)", simp)
    apply (case_tac "i", simp)
    apply simp
    apply (simp add: fun_eq_iff)
    apply (subst (asm) (1) Adder3_iter_wp_fun_def, simp, safe)
    apply (case_tac "i", simp)
    by simp

  lemma Adder3_iter_wp_aux_b: "i < n ⟹ apply ((Adder3_iter_wp_fun ^^ n) z) i = apply ((Adder3_iter_wp_fun ^^ Suc i) z) i"
    apply (case_tac "(Adder3_iter_wp_fun ^^ Suc i) z")
    apply (case_tac "a", simp)
    apply (cut_tac a = aa and b = ba and c = b and n = "Suc i" and z = z in Adder3_iter_wp_aux_a, simp_all)
    apply (case_tac "(Adder3_iter_wp_fun ^^ n) z")
    apply (case_tac "ab", simp)
    apply (drule Adder3_iter_wp_aux_a)
    by (simp add: apply_def)

  lemma Adder3_iter_wp_aux_c: "(λx. let z = λi. apply (Adder3_iter_wp_fun ((Adder3_iter_wp_fun ^^ i) x)) i in ((fst ∘ fst ∘ z, snd ∘ fst ∘ z), snd ∘ z)) = (λ x . (((λ i . 3 * i + 2), (λ i . 3 * i + 2)), snd x) )"
    apply (simp add: fun_eq_iff Let_def, safe)
    apply (case_tac " (Adder3_iter_wp_fun ((Adder3_iter_wp_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Adder3_iter_wp_aux_a, simp_all)
    apply (simp add: apply_def)
    apply (case_tac " (Adder3_iter_wp_fun ((Adder3_iter_wp_fun ^^ x) ((a, b), ba)))")
    apply (case_tac aa, simp)
    apply (cut_tac a = ab and b = bc and c = bb and n = "Suc x" and z = "((a, b), ba)" in Adder3_iter_wp_aux_a, simp_all)
    by (simp add: apply_def)


  lemma Adder3_iter_wp_aux_d: "⋀ i . i ≥ n ⟹ fst (fst ((Adder3_iter_wp_fun ^^ n) ((λi. 2, b), ba))) i =  3 * n + 2"
    apply (induction n, simp)
    apply simp
    apply (subst (1) Adder3_iter_wp_fun_def)
    apply (case_tac "(Adder3_iter_wp_fun ^^ n) ((λi. 2, b), ba)", simp)
    by (case_tac "a", simp)

  lemma Adder3_iter_wp_aux_e: "⋀ i. i < n ⟹ fst (fst ((Adder3_iter_wp_fun ^^ n) ((λi. 2, b), ba))) i =  3 * i + 2"
    apply (induction n, simp)
    apply simp
    apply (subst (1) Adder3_iter_wp_fun_def)
    apply (case_tac "(Adder3_iter_wp_fun ^^ n) ((λi. 2, b), ba)", simp)
    apply (case_tac "a", simp)
    by auto

  lemma Adder3_iter_wp_prec_aux: "0 < fst (fst ((Adder3_iter_wp_fun ^^ n) ((λi. 2, b), ba))) i"
    apply (case_tac "i ≥ n")
    apply (simp add: Adder3_iter_wp_aux_d)
    by (simp add: Adder3_iter_wp_aux_e) 


  lemma Adder3_iter_wp_prec: "(□ (λ((u, y), x). 0 < u 0)) ((Adder3_iter_wp_fun ^^ n) ((λi. 2, b), ba))"
    apply (simp add: always_def at_fun_def at_prod_def, safe)
    by (simp add: Adder3_iter_wp_prec_aux)

  lemma "FeedbackX Init_adder3_wp S_adder3_wp = Res_adder3_wp"
    apply (simp add: FeedbackX_def)
    apply (simp add: Init_adder3_wp_def Res_adder3_wp_def S_adder3_wp_simp Adder3_wp_inner_simp)
    apply (simp add: Adder3_iter_wp_fun_def [THEN sym])
    apply (simp add: IterateOmega_assert_update_d Adder3_iter_wp_aux_c Adder3_iter_wp_aux_b)
    apply (simp add: update_comp comp_assoc prod_update_skip)
    apply (simp add: update_comp comp_assoc[THEN sym] update_assert_comp)
    apply (simp add: update_comp comp_assoc)
    apply(simp add: update_def demonic_assert_comp comp_assoc[THEN sym])
    apply (simp add: demonic_demonic comp_assoc)
    apply (rule prec_rel_eq)
    apply auto [2] 
    apply (simp add: fun_eq_iff)
    by (simp add: Adder3_iter_wp_prec)


(* Example with Havoc *)


  definition "Init_adder3_havoc = [-λx. (λi. 0)-]"
  definition "Res_adder3_havoc  = ⊥"

  lemma [simp]: "(λx. ∀b ba n. (□ (λ((u, y), x). 0 < u 0)) ((Adder3_iter_wp_fun ^^ n) ((λi. 0, b), ba))) = ⊥"
    apply (simp add: fun_eq_iff always_def at_fun_def at_prod_def)
    apply (rule_tac x="Eps ⊤" in exI)
    apply (rule_tac x="Eps ⊤" in exI)
    apply (rule_tac x=0 in exI)
    by simp

  lemma [simp]: "{.λx. False.} o [:r:] = ⊥"
    by (simp add: fun_eq_iff assert_def)

  lemma "FeedbackX Init_adder3_havoc S_adder3_wp = Res_adder3_havoc"
    apply (simp add: FeedbackX_def)
    apply (simp add: Init_adder3_havoc_def Res_adder3_havoc_def S_adder3_wp_simp Adder3_wp_inner_simp)
    apply (simp add: Adder3_iter_wp_fun_def [THEN sym])
    apply (simp add: IterateOmega_assert_update_d Adder3_iter_wp_aux_c Adder3_iter_wp_aux_b)
    apply (simp add: update_comp comp_assoc prod_update_skip)
    apply (simp add: update_comp comp_assoc[THEN sym] update_assert_comp)
    apply (simp add: update_comp comp_assoc)
    apply(simp add: update_def demonic_assert_comp comp_assoc[THEN sym])
    apply (simp add: demonic_demonic comp_assoc)
    by (simp add: bot_fun_def)

  lemma Feedback_ExFb: "FeedbackX Init_ExFb ExFb_delayfb = Res"
    apply (simp add: FeedbackX_def)
    apply (simp add: Init_ExFb_def InitDF_def init_ExFb_def Res_def ExFb_delayfb_simp Res_aux_simp)
    apply (simp add: Res_aux_fun_def [THEN sym])
    apply (simp add: IterateOmega_func_bb Res_aux_fun_aux_b Res_aux_fun_aux_c)
    apply (simp add: update_comp comp_assoc prod_update_skip)
    apply (simp add: comp_assoc[THEN sym] Prod_demonic_skip demonic_demonic)
    apply(simp add: update_def demonic_demonic)
    apply (rule_tac f = demonic in arg_cong)
    apply (simp add: OO_def always_def at_fun_def)
    using mult_0 by blast


  lemma feedback_in_simp_aaa: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ 
      feedback ( {. u, (s,x) .  p' (s,x) ∧ p (u, (s,x)).} o [:u, (s,x) ↝ v, (s',y) .  r' (s,x) v ∧ r (u, (s,x)) (s',y):])
       = {. (s,x) . p' (s,x) ∧ (∀b. r' (s,x) b ⟶ p (b,(s,x))).} o [:(s,x) ↝ (s',y) . ∃ v . r' (s,x) v ∧ r (v, (s,x)) (s',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 IterateOmega_spec_a: "IterateOmega ({. p .} ∘ [: r :]) = {.((u,y),x) .∀n v y' z. (r ^^ n) ((u,y), x) ((v, y'), z) ⟶ p ((v,y'),z).} ∘ [: INF n. r ^^ n OO eqtop n :]"
    apply (simp add: IterateOmega_spec)
    apply (rule prec_rel_eq)
    apply simp_all
    by (simp add: split_def) 
     
  lemma AAA: "⋀u' y' . (((λ((u::'a, y::'b), x) ((u'::'a, y'::'b), x'). r (u, x) (u', y') ∧ x = x') ^^ n) ((u,y::'b), x) ((u', y'::'b), x')) ⟹ x = x'"
    apply (induction n)
    apply simp_all
    by (simp add: OO_def, auto)

  lemma BBB: "⋀u' y' . (((λ((u::'a, y::'b), x) ((u'::'a, y'::'b), x'). r (u, x) (u', y') ∧ x = x') ^^ n) ((u,y::'b), x) ((u', y'::'b), x')) = 
      (x = x' ∧ (((λ (u::'a, y::'b) (u'::'a, y'::'b) . r (u, x) (u', y')) ^^ n) (u,y::'b) (u', y'::'b)))"
    apply safe
    apply (drule AAA, simp)
    apply (frule AAA, simp)
    apply (induction n)
    apply simp_all
    apply (simp add: OO_def, auto)

    apply (induction n)
    apply simp_all
    by (simp add: OO_def, auto)


  lemma CCC: "(((λ((u::'a, y), x) ((u'::'a, y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n) ((u,y::'b), x) ((u', y'::'b), x')) = 
         (x = x' ∧ (∃ U Y . U 0 = u ∧ U n = u' ∧ Y 0 = y ∧ Y n = y' ∧ (∀ i < n . r (U i, x) (U (Suc i), Y (Suc i)))))"
    apply (simp add: BBB)
    apply safe
    apply (simp add: relpowp_fun_conv, safe)

    apply (rule_tac x = "fst o f" in exI, simp)
    apply (rule_tac x = "snd o f" in exI)
    apply simp
    apply safe
    apply (drule_tac x = i in spec, simp)
    apply (simp add: split_def)
    apply (simp add: relpowp_fun_conv)
    apply (rule_tac x = "λ i . (U i, Y i)" in exI)
    by auto [1]


  lemma IterateOmegaA_simp_a: "IterateOmegaA ([-λ ((u, y::nat ⇒'a), x) . ((u, x), x)-] o (({.p.} o [:r:]) ** Skip)) = 
    {.((ua, ya), xa).∀n a. (∃b U. U 0 = ua ∧ U n = a ∧ (∃Y. Y 0 = ya ∧ Y n = b ∧ (∀i<n. r (U i, xa) (U (Suc i), Y (Suc i))))) ⟶ p (a, xa).} ∘
    [: INF n. (λ((u, y), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n OO eqtop (n-1) :]"
    apply (subgoal_tac "[-λ((u, y::nat ⇒ 'a), x). ((u, x), x)-] ∘(({.p.} o [:r:]) ** Skip) = {.(u,y), x . p (u,x).} o [:(u, y), x ↝ (u', y'), x' . r (u, x) (u', y') ∧ x = x':]")
    apply simp
    apply (simp add: IterateOmegaA_spec)
    apply (subgoal_tac "{.x.∀n a b ba. ((λ((u, y::nat ⇒ 'a), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n) x ((a, b), ba) ⟶ p (a, ba).} 
        = {.(ua,ya),xa.∀n a b ba. ((λ((u, y), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n) ((ua,ya),xa) ((a, b), ba) ⟶ p (a, ba).}")
    apply simp
    apply (simp add: CCC)
    apply (simp add: fun_eq_iff assert_def)
    apply (simp add: Prod_spec_Skip)
    by (simp add: fun_eq_iff demonic_def le_fun_def assert_def update_def)
                            



  lemma IterateOmegaA_simp_b: "IterateOmegaA ([-λ ((u, y::nat ⇒'a), x) . ((u, x), x)-] o (({.p.} o [:r:]) ** Skip)) = 
    {.((ua, ya), xa).∀n U Y . (U 0 = ua ∧ Y 0 = ya ∧ (∀i<n. r (U i, xa) (U (Suc i), Y (Suc i)))) ⟶ p (U n, xa).} ∘
    [: INF n. (λ((u, y), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n OO eqtop (n-1) :]"

    apply (simp add: IterateOmegaA_simp_a)
    apply (rule_tac f = "λ x . {.x.} o [: INF n. (λ((u, y), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n OO eqtop (n-(Suc 0)) :]" in arg_cong)

    proof (subst fun_eq_iff, auto)
      fix n :: nat
      fix ba::'c
      fix U::"nat ⇒ 'b"
      fix Y::"nat ⇒ nat ⇒ 'a"
      assume [simp]: "∀i<n. r (U i, ba) (U (Suc i), Y (Suc i))"
      assume "∀n a. (∃b Ua. Ua 0 = U 0 ∧ Ua n = a ∧ (∃Ya. Ya 0 = Y 0 ∧ Ya n = b ∧ (∀i<n. r (Ua i, ba) (Ua (Suc i), Ya (Suc i))))) ⟶ p (a, ba)"
      from this have A: "(∃b Ua. Ua 0 = U 0 ∧ Ua n = U n ∧ (∃Ya. Ya 0 = Y 0 ∧ Ya n = b ∧ (∀i<n. r (Ua i, ba) (Ua (Suc i), Ya (Suc i))))) ⟶ p (U n, ba)"
        by simp
      have "(∃b Ua. Ua 0 = U 0 ∧ Ua n = U n ∧ (∃Ya. Ya 0 = Y 0 ∧ Ya n = b ∧ (∀i<n. r (Ua i, ba) (Ua (Suc i), Ya (Suc i)))))"
        apply (rule_tac x = "Y n" in exI)
        apply (rule_tac x = U in exI, simp)
        by (rule_tac x = Y in exI, simp)

     from this and A show " p (U n, ba)"
       by simp
    qed


  lemma IterateOmegaA_simp_aux: "(INF n. (λ((u, y), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n OO eqtop (n-1)) ((u::nat⇒'a,y::nat⇒'b), x::nat⇒'c)  ((u'::nat⇒'a,y'::nat⇒'b), x'::nat⇒'c) = 
    (x = x' ∧ (∀xa. ∃a b. (∃U. U 0 = u ∧ U xa = a ∧ (∃Y. Y 0 = y ∧ Y xa = b ∧ (∀i<xa. r (U i, x) (U (Suc i), Y (Suc i))))) ∧ (∀i<xa-1. a i = u' i) ∧ (∀i<xa-1. b i = y' i))) "
    apply (simp add: OO_def CCC eqtop_prod_def)
    apply auto
    apply (simp add: fun_eq_iff, safe)
    apply(drule_tac x = "Suc (Suc xa)" in spec)
    apply auto[1]
    apply (drule_tac x = xa in spec)
    by blast

    lemma IterateOmegaA_simp_c: "IterateOmegaA ([-λ ((u::nat ⇒ 'a, y::nat ⇒'b), x::nat⇒'c) . ((u, x), x)-] o (({.p.} o [:r:]) ** Skip)) = 
    {.((ua, ya), xa).∀n U Y . (U 0 = ua ∧ Y 0 = ya ∧ (∀i<n. r (U i, xa) (U (Suc i), Y (Suc i)))) ⟶ p (U n, xa).} ∘
    [: (u, y), x ↝ (u'::nat⇒'a, y'::nat⇒'b), x'::nat⇒'c . x = x' 
        ∧ (∀xa. ∃a b. (∃U. U 0 = u ∧ U xa = a ∧ (∃Y. Y 0 = y ∧ Y xa = b ∧ (∀i<xa. r (U i, x) (U (Suc i), Y (Suc i))))) ∧ (∀i<xa-1. a i = u' i) ∧ (∀i<xa-1. b i = y' i)) :]"
      apply (simp add: IterateOmegaA_simp_b)
      apply (subgoal_tac "(INF n. (λ((u, y), x) ((u', y'), x'). r (u, x) (u', y') ∧ x = x') ^^ n OO eqtop (n-1))
          = ( λ ((u, y), x) ((u', y'), x').x = x' ∧ (∀xa. ∃a b. (∃U. U 0 = u ∧ U xa = a ∧ (∃Y. Y 0 = y ∧ Y xa = b ∧ (∀i<xa. r (U i, x) (U (Suc i), Y (Suc i))))) ∧ 
          (∀i<xa-1. a i = u' i) ∧ (∀i<xa-1. b i = y' i)))")
      apply (simp_all)
      apply (unfold fun_eq_iff)
      apply safe
      apply (cut_tac r = r and u = a and y = b and x = ba and u' = aa and y' = bb and x' = bc in IterateOmegaA_simp_aux)
      apply (simp add: fun_eq_iff)
      apply (simp add: fun_eq_iff)

      apply (cut_tac r = r and u = a and y = b and x = ba and u' = aa and y' = bb and x' = bc in IterateOmegaA_simp_aux)
      apply (simp add: fun_eq_iff)
      apply (simp add: fun_eq_iff)
      apply (cut_tac r = r and u = a and y = b and x = ba and u' = aa and y' = bb and x' = bc in IterateOmegaA_simp_aux)
      by (simp add: fun_eq_iff)

    lemma IterateOmegaA_simp_d: "IterateOmegaA ([-λ ((u::nat ⇒ 'a, y::nat ⇒'b), x::nat⇒'c) . ((u, x), x)-] o (({.p.} o [:r:]) ** Skip)) = 
    {.((ua, ya), xa).∀n U Y . (U 0 = ua ∧ Y 0 = ya ∧ (∀i<n. r (U i, xa) (U (Suc i), Y (Suc i)))) ⟶ p (U n, xa).} ∘
    [: (u, y), x ↝ (u'::nat⇒'a, y'::nat⇒'b), x'::nat⇒'c . x = x' 
        ∧ (∀xa. (∃U. U 0 = u ∧ (∃Y. Y 0 = y ∧ (∀i<xa. r (U i, x) (U (Suc i), Y (Suc i))) ∧ (∀i<xa-1. U xa i = u' i) ∧ (∀i<xa-1. Y xa i = y' i)))) :]"
      apply (simp add: IterateOmegaA_simp_c)
      apply (subgoal_tac "(λ ((u, y), x) ((u', y'), x').x = x' ∧ (∀xa. ∃a b. (∃U. U 0 = u ∧ U xa = a ∧ (∃Y. Y 0 = y ∧ Y xa = b ∧ (∀i<xa. r (U i, x) (U (Suc i), Y (Suc i))))) ∧ 
               (∀i<xa-1. a i = u' i) ∧ (∀i<xa-1. b i = y' i)))
          = (λ ((u, y), x) ((u', y'), x').x = x' ∧ (∀xa. (∃U. U 0 = u ∧ (∃Y. Y 0 = y ∧ (∀i<xa. r (U i, x) (U (Suc i), Y (Suc i))) ∧ (∀i<xa-1. U xa i = u' i) ∧ (∀i<xa-1. Y xa i = y' i)))))")
      apply simp_all
      apply (subst (2) fun_eq_iff, simp)
      apply (subst (2) fun_eq_iff, simp)
      apply safe
      apply blast
      by (drule_tac x = xa in spec, simp, safe, simp, auto)

  lemma DelayFeedback_feedback_simp: "DelayFeedback init (feedback ({.(u, s, x).  p u s x.} ∘ [-λ(u, s, x). (f s x, g u s x, h u s x)-])) = 
    {.prec_pre_sts init (λ(s, x) . p (f s x) s x) (λ(s, x) y . y = (g (f s x) s x, h (f s x) s x)).} ∘
    [:rel_pre_sts init (λ(s, x) y. y = (g (f s x) s x, h (f s x) s x)):]"
    apply (cut_tac p=p and f=f and g=g and h=h in feedback_update_simp_c, simp)
    apply (simp add: update_def)
    apply (simp add: DelayFeedback_simp)
    by (simp add: fun_eq_iff assert_def demonic_def le_fun_def split_def)

lemma input_output_switch: "([-λ(s, u, x). (u, s, x)-] ∘ ({. p .} ∘ [-λ(u, s, x). (f s x, g u s x, h u s x)-]) ∘ [-λ(v, s, y). (s, v, y)-]) =
  {. (s,u,x). p (u, s, x) .} o [- λ(s, u, x).(g u s x, f s x, h u s x) -]"
  apply (simp add: comp_assoc[THEN sym] update_assert_comp)
  apply (simp add: comp_assoc update_comp)
  by (rule spec_eq_iff_1, simp_all add: fun_eq_iff)

primrec ss :: "'a ⇒ ('b ⇒ 'a ⇒ 'c ⇒ 'a) ⇒ ('a ⇒ 'c ⇒ 'b) ⇒ (nat ⇒ 'c) ⇒ nat ⇒ 'a" where
  "ss a g f xa 0 = a" |
  "ss a g f xa (Suc i) = g (f (ss a g f xa i) (xa i)) (ss a g f xa i) (xa i)"


  primrec ssu :: "'a ⇒ ('b ⇒ 'a ⇒ 'c ⇒ 'a) ⇒ (nat ⇒ 'b) ⇒ (nat ⇒ 'c) ⇒ nat ⇒ 'a" where
    "ssu a g u x 0 = a" |
    "ssu a g u x (Suc i) = g (u i) (ssu a g u x i) (x i)"

  lemma BBBd: "a = sa 0 ⟹ ∀fb<fa. sa (Suc fb) = g (u fb) (sa fb) (x fb)  ⟹ i ≤ fa ⟹ ssu a g u x i = sa i"
    by (induction i, auto)

definition "prec_pre_sts_st init p r u x = (∀ y . init (u 0) ⟶ (lift_rel r leads lift_pre p) (u, x) (u[1..], y))"
  
lemma prec_pre_sts_st_simp: "prec_pre_sts_st init p r u x = 
    (∀ 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_st_def leads_def until_def lift_rel_def lift_pre_def at_fun_def at_prod_def, safe, blast)
  by blast
  
  lemma BBBc: "s = ssu a g u x ⟹ prec_pre_sts (λ s . s = a) (λ(s, u, x). p (u, s, x)) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (λi. (u i, x i)) = 
        ((∀ fa. (∀ fb<fa. s (Suc fb) = g (u fb) (s fb) (x fb)) ⟶ p (u fa, s fa, x fa)))"
        apply (simp add: prec_pre_sts_simp)
    apply safe
      apply (drule_tac x = "ssu a g u x" in spec, simp_all)
     apply (drule_tac x = "λ i . (f (ssu a g u x i) (x i), h (u i) (ssu a g u x i) (x i))" in spec)
     apply blast
    apply (subgoal_tac "∀ i ≤ n . ssu a g u x i = ua i", simp)
     apply (metis order_refl)
      apply safe
      by (rule BBBd, simp_all)

  lemma BBBx: "s = ssu a g u x ⟹ prec_pre_sts (λ s . s = a) (λ(s, u, x). p (u, s, x)) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (λi. (u i, x i)) = 
        ((∀ fa. p (u fa, s fa, x fa)))"
        apply (simp add: prec_pre_sts_simp)
    apply safe
        apply (drule_tac x = "ssu a g u x" in spec)
     apply auto [1]
    apply (subgoal_tac "∀ i ≤ n . ssu a g u x i = ua i", simp)
     apply (metis order_refl)
      apply safe
      by (rule BBBd, simp_all)

  lemma BBBy: "(prec_pre_sts (λ s . s = a) (λ(s, u, x). p (u, s, x)) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (λi. (u i, x i))) = 
        ((∀ fa. p (u fa,  ssu a g u x fa, x fa)))"
    by (rule BBBx, simp)

   lemma BBBe: "a = sa 0 ⟹ ∀fb<fa. sa (Suc fb) = g (f (sa fb) (x fb)) (sa fb) (x fb) ⟹ i ≤ fa ⟹ ss a g f x i = sa i"
    by (induction i, auto)

 
   lemma BBBz: "(prec_pre_sts (λ s . s = a) (λ(s, x). p (f s x, s, x)) (λ(s, x) y. y = (g (f s x) s x, h (f s x) s x)) x)
    =  ((∀ fa. p (f ( ss a g f x fa) (x fa),  ss a g f x fa, x fa)))"
     apply (simp add: prec_pre_sts_simp)
      apply safe
      apply (drule_tac x = "ss a g f x" in spec)
      apply auto [1]
     apply (drule_tac x = n in spec)
     apply (subgoal_tac "∀ i ≤ n . ss a g f x i = u i")
      apply simp
       apply safe
       by (rule BBBe, simp_all)

primrec ssc :: "'c ⇒ (nat ⇒ 'a) ⇒ ('a ⇒ 'c ⇒ 'de ⇒ 'c)  ⇒ (nat ⇒ 'de) ⇒ nat ⇒ nat ⇒ 'c" where
  "ssc a U g xa i 0 = a" |
  "ssc a U g xa i (Suc fa) =  g (U fa) (ssc a U g xa i fa) (xa fa)"

primrec UUc :: "(nat ⇒ 'a) ⇒ 'b ⇒ ('b ⇒ 'c ⇒ 'a) ⇒ ('a ⇒ 'b ⇒ 'c ⇒ 'b) ⇒ (nat ⇒ 'c) ⇒ nat ⇒ nat ⇒ 'a" where
  "UUc u a f g x 0 = u" |
  "UUc u a f g x (Suc i) = (λ xa . f (ssc a (UUc u a f g x i) g x i xa) (x xa))"



  lemma DDDa: "∀fa. sa (Suc fa) = g (U i fa) (sa fa) (xa fa) ∧ U (Suc i) fa = f (sa fa) (xa fa) ∧ Y (Suc i) fa = h (U i fa) (sa fa) (xa fa) ⟹
                           a = sa 0 ⟹ sa k = ssc a (U i) g xa i k"
     by (induction k, auto)
  lemma AAAAU:"U 0 = ua ⟹ aa = U n ⟹ ∀i<n. ∀fa. U (Suc i) fa = f (ssc a (U i) g xa i fa) (xa fa) ⟹ k ≤ n ⟹ UUc (U 0) a f g xa k = U k"
    by (induction k, simp_all)

  
  lemma AAAAAka:"0 < n ⟹  (∃b U. (n = 0 ⟶ U 0 = ua ∧ U 0 = aa ∧ ya = b) ∧
                        (0 < n ⟶ U 0 = ua ∧ U n = aa ∧ (∀i<n. ∀fa. U (Suc i) fa = f (ssc a (U i) g xa i fa) (xa fa)) ∧ 
                        (∀fa. h (U (n - Suc 0) fa) (ssc a (U (n - Suc 0)) g xa (n - Suc 0) fa) (xa fa) = b fa))) 
                        =  (UUc ua a f g xa n = aa)"

     apply auto
     prefer 2
     apply (subst ex_comm)
     apply (rule_tac x = "UUc ua a f g xa" in exI, simp_all)
     apply (rule_tac x = "λ fa . h (UUc ua a f g xa (n - Suc 0) fa) (ssc a (UUc ua a f g xa (n - Suc 0)) g xa (n - Suc 0) fa) (xa fa)" in exI, simp)
     by (rule AAAAU, simp_all, auto)
     
   lemma AAAAAk: " (∃b U. (n = 0 ⟶ U 0 = ua ∧ U 0 = aa ∧ ya = b) ∧
                        (0 < n ⟶ U 0 = ua ∧ U n = aa ∧ (∀i<n. ∀fa. U (Suc i) fa = f (ssc a (U i) g xa i fa) (xa fa)) 
                        ∧ (∀fa. h (U (n - Suc 0) fa) (ssc a (U (n - Suc 0)) g xa (n - Suc 0) fa) (xa fa) = b fa))) 
                        =  (UUc ua a f g xa n = aa)"
      apply (case_tac n)
      apply auto [1]
      by (subst AAAAAka, simp_all)


  lemma ZZZp: " ∀xa::nat. sa (Suc xa) = g (U i xa) (sa xa) (x xa) ∧ U (Suc i) xa = f (sa xa) (x xa) ∧ Y (Suc i) xa = h (U i xa) (sa xa) (x xa) ⟹ a = sa (0::nat) ⟹ sa k = ssc a (U i) g x i k"
    by (induction k, auto)

  lemma ZZZq: "s = ssc a (U i) g x i ⟹  (∃s. s 0 = a ∧ (∀xa. s (Suc xa) = g (U i xa) (s xa) (x xa) ∧ U (Suc i) xa = f (s xa) (x xa) ∧ Y (Suc i) xa = h (U i xa) (s xa) (x xa))) = 
      (∀ xa . U (Suc i) xa = f (s xa) (x xa) ∧ Y (Suc i) xa = h (U i xa) (s xa) (x xa))"
      apply safe
      apply (frule_tac k = xa in ZZZp, simp_all)
      apply simp
      apply (frule_tac k = xa in ZZZp, simp_all)
      apply simp
      by (rule_tac x = " ssc a (U i) g x i" in exI, simp_all)

lemma ZZZr: "0 < xa ⟹(∃Y . Y 0 = y ∧ Y xa = b ∧ (∀i<xa. ∀xa::nat. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa) ∧ Y (Suc i) xa = h (U i xa) (ssc a (U i) g x i xa) (x xa)))
       = ((∀i<xa. ∀xa::nat. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa)) ∧ (∀ k . h (U (xa -1) k) (ssc a (U (xa -1)) g x (xa -1) k) (x k) = b k))"
       apply simp
       apply safe
       apply auto [1]
       apply (case_tac xa, simp_all)
       apply (rule_tac x = "(λ k . (if k = 0 then y else (λ xa .  h (U (k - 1) xa) (ssc a (U (k - 1)) g x (k - 1) xa) (x xa))))" in exI)
       by auto

    lemma ZZZc: "(∃Y . Y 0 = y ∧ Y xa = b ∧ (∀i<xa. ∀xa::nat. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa) ∧ Y (Suc i) xa = h (U i xa) (ssc a (U i) g x i xa) (x xa))) = 
      (if xa = 0 then y = b else ((∀i<xa. ∀xa::nat. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa)) ∧ (∀ k . h (U (xa -1) k) (ssc a (U (xa -1)) g x (xa -1) k) (x k) = b k)))"
      apply (case_tac xa, simp)
      apply auto [1]
      by (simp add: ZZZr)



  lemma [simp]: "∀i<xa. ∀xa::nat. Ua (Suc i) xa = f (ssc a (Ua i) g x i xa) (x xa) ⟹ UUc (Ua (0::nat)) a f g x xa = Ua xa"
    by (induction xa, auto)

  lemma TTTb: "U = UUc u a f g x ⟹ (0 < xa ⟶ (∃ U . U 0 = u ∧ U xa = aa ∧ (∀i<xa. ∀xa. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa)) ∧
                                  (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))
        = (0 < xa ⟶ (U xa = aa ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))"

    apply safe
    apply simp_all
    by (rule_tac x = "UUc u a f g x" in exI, auto)
    

  lemma TTTa: "(∃U. (xa = 0 ⟶ U 0 = u ∧ U 0 = aa ∧ y = b) ∧
                                 (0 < xa ⟶ U 0 = u ∧ U xa = aa ∧ (∀i<xa. ∀xa. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa)) ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))
        =((xa = 0 ⟶ u = aa ∧ y = b) ∧
                                 (0 < xa ⟶ (∃ U . U 0 = u ∧ U xa = aa ∧ (∀i<xa. ∀xa. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa)) ∧
                                  (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k))))"
      by auto

   lemma TTTc: "U = UUc u a f g x ⟹ (∃U. (xa = 0 ⟶ U 0 = u ∧ U 0 = aa ∧ y = b) ∧
                                 (0 < xa ⟶ U 0 = u ∧ U xa = aa ∧ (∀i<xa. ∀xa. U (Suc i) xa = f (ssc a (U i) g x i xa) (x xa)) ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))

        =((xa = 0 ⟶ u = aa ∧ y = b) ∧ (0 < xa ⟶  (U xa = aa ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k))))"
     apply (subst TTTa)
     by (simp add: TTTb)

                                  

   lemma TTTe: "(∃ b. ((xa = 0 ⟶ u = aa ∧ y = b) ∧ (0 < xa ⟶  (U xa = aa ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))) ∧
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀i<xa - Suc 0. b i = y' i))
     = (((xa = 0 ⟶ u = aa) ∧ (0 < xa ⟶  ((U xa = aa ∧ (∃ b . (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k) ∧
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀i<xa - Suc 0. b i = y' i)))))))"
     apply safe
     apply auto [1]
     apply auto [1]
     apply auto [1]
     apply auto [1]
     apply (case_tac xa, simp_all)
     by (rule_tac x = b in exI, simp)

   lemma TTTf: "(∃ b. ((xa = 0 ⟶ u = aa ∧ y = b) ∧ (0 < xa ⟶  (U xa = aa ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))) ∧
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀i<xa - Suc 0. b i = y' i))
     = (((xa = 0 ⟶ u = aa) ∧ (0 < xa ⟶  ((U xa = aa ∧ 
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀k<xa - Suc 0. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = y' k))))))"
     apply safe
     apply auto [1]
     apply auto [1]
     apply auto [1]
     apply auto [1]
     apply (case_tac xa, simp_all)
     by (rule_tac x = "λ k .  h (U nat k) (ssc a (U nat) g x nat k) (x k)" in exI, simp)

  thm UUc.simps

  thm ssc.simps
    
  primrec SS::"'b ⇒ ('a ⇒ 'b ⇒ 'c ⇒ 'b) ⇒ ('b ⇒ 'c ⇒ 'a) ⇒ (nat ⇒ 'c) ⇒ nat ⇒ 'b" where
    "SS a g f x 0 = a" |
    "SS a g f x (Suc i) = g (f (SS a g f x i) (x i)) (SS a g f x i) (x i)"


   lemma UU_SS: "⋀ xa . i < xa ⟹ UUc u a f g x xa i = f (SS a g f x i)  (x i) ∧ ssc a (UUc u a f g x xa) g x xa i = SS a g f x i"
    apply (induction i, simp_all)
    apply (case_tac xa, simp_all)
    by(case_tac xa, simp_all)


   lemma TTTza: " (x = x' ∧ (∀xa>0::nat. (∀i<xa - Suc (0::nat). f (SS a g f x i) (x i) = u' i) ∧ (∀k<xa - Suc (0::nat). h (f (SS a g f x k) (x k)) (SS a g f x k) (x k) = y' k))) = 
     (x = x' ∧ (∀ k . f (SS a g f x k) (x k) = u' k) ∧ (∀k . h (f (SS a g f x k) (x k)) (SS a g f x k) (x k) = y' k))"
     apply auto
     apply (drule_tac x = "Suc (Suc k)" in spec)
     apply auto [1]
     apply (drule_tac x = "Suc (Suc k)" in spec)
     by auto [1]
       
    
lemma AAAAta:"0 < n ⟹ s = (λ i . ssc a (U i) g xa i) ⟹ 
      (∃Y. Y 0 = ya ∧ Y n = b ∧ (∀i<n. rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (U i || xa) (U (Suc i) || Y (Suc i)))) = 
    ((∀i<n. ∀ fa . U (Suc i) fa = f (s i fa) (xa fa)) ∧ ((∀ fa . h (U (n - 1) fa) (s (n - 1) fa) (xa fa) = b fa)))"
    apply (simp add: rel_pre_sts_simp)
  apply safe
    apply (drule_tac x = i in spec, simp_all, safe)
    apply (simp add: nzip_def)
    apply (drule_tac a = a and k = fa in DDDa, simp_all)

    apply (simp add: nzip_def)
    apply (drule_tac x = "n - 1" in spec, simp_all, safe, simp)
    apply (case_tac n, simp_all)
   apply (drule_tac a = a and k = fa and i = "nat" in DDDa, simp_all)
    
    apply (simp add: nzip_def)
    apply (rule_tac x = "λ k . if k = 0 then ya else (λ fa . h (U (k -1) fa) (s (k-1) fa) (xa fa))" in exI, simp, safe)
    by (rule_tac x = "ssc a (U i) g xa i" in exI, simp_all)
    
  lemma AAAAt: "s = (λ i . ssc a (U i) g xa i) ⟹ (∃Y. Y 0 = ya ∧ Y n = b ∧ (∀i<n. rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (U i || xa) (U (Suc i) || Y (Suc i))))
    = (if n = 0 then ya = b else  ((∀i<n. ∀ fa . U (Suc i) fa = f (s i fa) (xa fa)) ∧ ((∀ fa . h (U (n - 1) fa) (s (n - 1) fa) (xa fa) = b fa))))"
    apply (case_tac n)
    apply auto [1]
    by (subst AAAAta, simp_all)
      
  lemma BBBq: "s = ssc a (UUc ua a f g xa n) g xa  n ⟹ (∀ s. s 0 = a ⟶ (∀xb. (∀fa<xb. s (Suc fa) = g (UUc ua a f g xa n fa) (s fa) (xa fa)) ⟶ p (UUc ua a f g xa n xb, s xb, xa xb))) = 
    ( (∀xb. p (UUc ua a f g xa n xb, s xb, xa xb)))"
  proof safe
    fix xb
    show "s = ssc a (UUc ua a f g xa n) g xa n ⟹
          ∀s. s 0 = a ⟶ (∀xb. (∀fa<xb. s (Suc fa) = g (UUc ua a f g xa n fa) (s fa) (xa fa)) ⟶ p (UUc ua a f g xa n xb, s xb, xa xb)) ⟹
          p (UUc ua a f g xa n xb, ssc a (UUc ua a f g xa n) g xa n xb, xa xb)"
      by auto
  next
    fix sa xb 
    {fix fa
      have  "∀fa<xb. sa (Suc fa) = g (UUc ua (sa 0) f g xa n fa) (sa fa) (xa fa) ⟹ fa ≤ xb ⟹ ssc (sa 0) (UUc ua (sa 0) f g xa n) g xa n fa = sa fa"
        by (induction fa, auto)
    }
    from this have A: "∀fa<xb. sa (Suc fa) = g (UUc ua (sa 0) f g xa n fa) (sa fa) (xa fa) ⟹ ssc (sa 0) (UUc ua (sa 0) f g xa n) g xa n xb = sa xb"
      by simp
    from this show "s = ssc (sa 0) (UUc ua (sa 0) f g xa n) g xa n ⟹
             ∀xb. p (UUc ua (sa 0) f g xa n xb, ssc (sa 0) (UUc ua (sa 0) f g xa n) g xa n xb, xa xb) ⟹
             a = sa 0 ⟹ ∀fa<xb. sa (Suc fa) = g (UUc ua (sa 0) f g xa n fa) (sa fa) (xa fa) ⟹ p (UUc ua (sa 0) f g xa n xb, sa xb, xa xb)"
    apply (simp_all)
      by (drule_tac x = xb in spec, simp)
  qed
    

  lemma BBBk: "prec_pre_sts (λb. b = a) (λ(s, u, x). p (u, s, x)) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (UU ua a f g xa n || xa) = 
      (∀ s . s 0 = a ⟶ (∀xb. (∀ fa < xb. s (Suc fa) = g (UU ua a f g xa n fa) (s fa) (xa fa)) ⟶ p (UU ua a f g xa n xb, s xb, xa xb)))"
    apply (simp add: prec_pre_sts_simp nzip_def, safe)
     apply (drule_tac x = s in spec)
     apply auto
    apply (drule_tac x = "λ fa . (f (s fa) (xa fa), h (UU ua a f g xa n fa) (s fa) (xa fa))" in spec)
    by auto
      
   lemma ZZZaa: "(INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0))
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') =  
          (x = x' ∧ (∀xa. ∃aa b. (∃U. U 0 = u ∧ U xa = aa ∧ (∃Y. Y 0 = y ∧ Y xa = b ∧ (∀i<xa. rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (U i || x) (U (Suc i) || Y (Suc i))))) ∧
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀i<xa - Suc 0. b i = y' i))) "
     by (cut_tac r = "λ  (u, x) (u', y') . rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y')" 
        and u = u and x = x and u' = u' and y = y and y' = y' and x' = x' in IterateOmegaA_simp_aux, simp)
      
      
   lemma TTTd: "U = UUc u a f g x ⟹ (INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0))
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') = 
         (x = x' ∧ (∀xa. ∃aa b. ((xa = 0 ⟶ u = aa ∧ y = b) ∧ (0 < xa ⟶  (U xa = aa ∧ (∀k. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = b k)))) ∧
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀i<xa - Suc 0. b i = y' i)))"
     apply (subst ZZZaa)
       apply (simp add: rel_pre_sts_simp nzip_def)
      apply (simp add:  ZZZq)
      apply (simp add:  ZZZc)
     by (simp add:  TTTc)

      
   lemma TTTr: "U = UUc u a f g x ⟹ (INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0))
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') = 
         (x = x' ∧ (∀xa. ∃aa . (((xa = 0 ⟶ u = aa) ∧ (0 < xa ⟶  ((U xa = aa ∧ 
                            (∀i<xa - Suc 0. aa i = u' i) ∧ (∀k<xa - Suc 0. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = y' k))))))))"
      apply (subst TTTd)
      apply simp
      by (subst TTTf, simp)

 
   lemma TTTt: "U = UUc u a f g x ⟹ (INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0))
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') = 
         (x = x' ∧ (∀xa. (((xa = 0 ⟶ True) ∧ (0 < xa ⟶  ((
                            (∀i<xa - Suc 0. U xa i = u' i) ∧ (∀k<xa - Suc 0. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = y' k))))))))"
      by (subst TTTr, simp_all, auto)



   lemma TTTy: "U = UUc u a f g x ⟹ (INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0))
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') = 
         (x = x' ∧ (∀xa. (((0 < xa ⟶  ((
                            (∀i<xa - Suc 0. U xa i = u' i) ∧ (∀k<xa - Suc 0. h (U (xa - Suc 0) k) (ssc a (U (xa - Suc 0)) g x (xa - Suc 0) k) (x k) = y' k))))))))"
     
      by (subst TTTt, simp_all)

        
   lemma TTTz: "(INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0))
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') = 
          (x = x' ∧ (∀xa>0::nat. (∀i<xa - Suc (0::nat). f (SS a g f x i) (x i) = u' i) ∧ (∀k<xa - Suc (0::nat). h (f (SS a g f x k) (x k)) (SS a g f x k) (x k) = y' k)))"
      apply (subst TTTy, simp)
      by (simp add: UU_SS)

lemma TTTyt: "(INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0)) 
        ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') = (x = x' ∧ (∀ k . f (SS a g f x k) (x k) = u' k) ∧ (∀k . h (f (SS a g f x k) (x k)) (SS a g f x k) (x k) = y' k))"
    apply (subst TTTz)
    by (simp add: TTTza)



lemma TTT: "(INF x. (λ((u, y), x) ((u', y'), x'). rel_pre_sts (λb. b = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (u || x) (u' || y') ∧ x = x') ^^ x OO eqtop (x - Suc 0)) 
  = (λ ((u, (y::nat ⇒ 'c)), x) ((u', y'::nat ⇒ 'c), x') . (x = x' ∧ (λ k . f (SS a g f x k) (x k)) = u' ∧ (λ k . h (f (SS a g f x k) (x k)) (SS a g f x k) (x k)) = y'))"
    apply (unfold fun_eq_iff)
    apply clarify
    apply (cut_tac f = f and g = g and x = ba and a = a and u  = aa and y = b and y' = bb and x = ba and x' = bc and u' = ab and h = h in  TTTyt)
    apply (unfold fun_eq_iff)
      by simp
          
  lemma IterateOmegaA_DelayFeedback: "IterateOmegaA ([-λ((u, y), x). ((u, x), x)-] ∘ ([-λ(x, y). x || y-] 
        ∘ DelayFeedback (λx. x = a) ({.(s, u, x).p (u, s, x).} ∘ [-λ(s, u, x). (g u s x, f s x, h u s x)-]) ∘ [-z ↝ fst ∘ z, snd ∘ z-]) ** Skip) =  
        {.((ua, ya), xa).∀n xb. p (UUc ua a f g xa n xb, ssc a (UUc ua a f g xa n) g xa n xb, xa xb).} ∘
        [:((u, y), x)↝((u', y'), x').x = x' ∧ (λ k . f (SS a g f x k) (x k)) = u' ∧ (λ k. h (f (SS a g f x k) (x k)) (SS a g f x k) (x k)) = y':]"
  proof -
    have [simp]: "(λx y. y = (case x of (s, u, xa) ⇒ (g u s xa, f s xa, h u s xa))) = (λ(s, u, x) y. y = (g u s x, f s x, h u s x))"
      by (simp add: fun_eq_iff)
    have [simp]: "DelayFeedback (λx. x = a) ({.(s, u, x).p (u, s, x).} ∘ [-λ(s, u, x). (g u s x, f s x, h u s x)-]) = 
       {. prec_pre_sts (λx. x = a) (λ(s, u, x). p (u, s, x))(λ(s, u, x) y. y = (g u s x, f s x, h u s x)) .} ∘
       [: rel_pre_sts (λx. x = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) :]"
      by (simp add: update_def DelayFeedback_simp)
        
    have "⋀ r . [:r:] o [-z ↝ fst ∘ z, snd ∘ z-] = [:x ↝ v, y . r x (v || y):]"
      apply (simp add: demonic_def update_def fun_eq_iff nzip_def_abs le_fun_def, safe)
      by (drule_tac x = "a || b" in spec, simp add:, simp add: nzip_def_abs, auto)
        
    have [simp]: "⋀ p r . [- (u, x) ↝ u || x -] ∘ ({. p .} ∘ [:r:]) ∘ [-z ↝ fst ∘ z, snd ∘ z-]
            = {.(u, x) . p (u || x).} o [:u, x ↝ v, y . r (u || x) (v || y):]"
      apply (simp add: update_def comp_assoc demonic_demonic)
      apply (simp add: comp_assoc[symmetric] demonic_assert_comp)
      apply (simp add: comp_assoc demonic_demonic)
      apply (rule prec_rel_eq)
        apply (subst fun_eq_iff, simp)
        apply (subst (2) fun_eq_iff)
      apply (subst (2) fun_eq_iff, simp add: OO_def, safe)
       apply (simp add: nzip_split)
        by (rule_tac x = "aa || ba" in exI, simp)

    have "IterateOmegaA ([-λ((u, y), x). ((u, x), x)-] ∘ ([-λ(x, y). x || y-] 
        ∘ DelayFeedback (λx. x = a) ({.(s, u, x).p (u, s, x).} ∘ [-λ(s, u, x). (g u s x, f s x, h u s x)-]) ∘ [-z ↝ fst ∘ z, snd ∘ z-]) ** Skip)
        =  IterateOmegaA([- ((u, y), x) ↝ ((u, x), x) -] ∘
            ({.(x, y).prec_pre_sts (λx. x = a) (λ(s, u, x). p (u, s, x)) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (x || y).} ∘
             [:(x, y)↝(aa, b).rel_pre_sts (λx. x = a) (λ(s, u, x) y. y = (g u s x, f s x, h u s x)) (x || y) (aa || b):]) **
            Skip)"
      by simp
    also have "... = {.((ua, ya), xa).∀n xb. p (UUc ua a f g xa n xb, ssc a (UUc ua a f g xa n) g xa n xb, xa xb).} ∘
        [:((u, y), x)↝((u', y'), x').x = x' ∧ (λk. f (SS a g f x k) (x k)) = u' ∧ (λk. h (f (SS a g f x k) (x k)) (SS a g f x k) (x k)) = y':]"
      by (simp add: IterateOmegaA_simp_a AAAAAk AAAAt BBBk BBBq TTT)
    finally show ?thesis
      by simp
  qed
    
lemma angelic_not_demonic: "p = (r ⊓ (λ x uy . x = snd uy)) ⟹ {:x↝ uy . p x uy:} o [:uy ↝ z . q (snd uy) z:] = {.x . (∃ u . p x (u, x)).} o [:y ↝ z . q y z:]"
  by (simp add: fun_eq_iff demonic_def angelic_def assert_def le_fun_def)

lemma SS_simp: "⋀ xa . i < xa ⟹ ssc a (λi. f (SS a g f x i) (x i)) g x xa i = SS a g f x i"
    by (induction i, simp_all)


lemma SS_simp_a:"⋀ xa . xa ≤ i ⟹  u = (λ i . f (SS a g f x i) (x i)) ⟹ ssc a u g x xa i = SS a g f x i"
    apply (induction i, simp_all)
    apply (case_tac xa, simp_all)
    apply (case_tac "i < Suc nat")
    apply (simp add: SS_simp)
    by auto

  lemma SS_simp_b: "u = (λ i . f (SS a g f x i) (x i)) ⟹ ssc a u g x xa i = SS a g f x i"
    apply (case_tac "i < xa")
    apply (simp add: SS_simp)
    by (simp add: SS_simp_a)

  lemma UU_SS_simp: "⋀ i . u = (λ i . f (SS a g f x i) (x i)) ⟹ UUc u a f g x xa i =  f (SS a g f x i) (x i) ∧ ssc a (UUc u a f g x xa) g x xa i = SS a g f x i"
    apply (induction xa, simp_all)
    by (simp_all add: SS_simp_b)
    
   declare ssc.simps [simp del]
   declare SS.simps [simp del]
   declare UUc.simps [simp del]

  lemma SSS: "(∃aa. ∀n xb. p (UUc aa a f g x n xb, ssc a (UUc aa a f g x n) g x n xb, x xb))
    = (∀ n. p (f (SS a g f x n) (x n) , SS a g f x n, x n))"
    apply auto
    apply (drule_tac x = "Suc (Suc n)" in spec)
    apply (drule_tac x = "n" in spec)
    apply (simp add: UU_SS)
    apply (rule_tac x = "λ n . f (SS a g f x n) (x n)" in exI, safe)
    apply (case_tac "xb < n")
    apply (simp add: UU_SS)
    by (simp add: UU_SS_simp)

  lemma SSSa: "∀fa<xaa. s (Suc fa) = g (f (s fa) (x fa)) (s fa) (x fa) ⟹ i ≤ xaa ⟹  s i = SS (s 0) g f x i"
    by (induction i, auto simp add: SS.simps)

  lemma SSSb: "prec_pre_sts (λ s . s = a) (λpa. p (f (fst pa) (snd pa), pa)) (λp y. y = (g (f (fst p) (snd p)) (fst p) (snd p), h (f (fst p) (snd p)) (fst p) (snd p)))
    = (λ x . ∀ n. p (f (SS a g f x n) (x n) , SS a g f x n, x n))"
    apply (simp add: prec_pre_sts_simp fun_eq_iff)
    apply safe
    apply (drule_tac x = "SS a g f x" in spec, safe)
    apply (simp_all add: SS.simps)
    apply (drule_tac x = "λ fa. h (f (SS a g f x fa) (x fa)) (SS a g f x fa) (x fa)" in spec, simp)
    apply (case_tac "∀ k < n. u (Suc k) = g (f (u k) (x k)) (u k) (x k)")
    by (drule_tac i = n and f = f in SSSa, simp_all)

    
  lemma SSSc: "∀fa. s (Suc fa) = g (f (s fa) (x fa)) (s fa) (x fa) ⟹ SS (s 0) g f x i = s i"
    by (induction i, auto simp add: SS.simps)

  lemma SSSd: "(rel_pre_sts (λ s. s = a) (λp y. y = (g (f (fst p) (snd p)) (fst p) (snd p), h (f (fst p) (snd p)) (fst p) (snd p))))
    = (λ x y . y = (λk. h (f (SS a g f x k) (x k)) (SS a g f x k) (x k)))"
    apply (simp add: rel_pre_sts_simp fun_eq_iff)
    apply (safe)
    apply (simp add: fun_eq_iff)
    apply (simp add: SSSc)
    by (rule_tac x = "SS a g f x" in exI, simp add: SS.simps)
      
  thm IterateOmegaA_spec
    

    
lemma IterateOmegaA_update: "IterateOmegaA [-f-] = [: INF n. (λ x y . f x = y) ^^ n OO eqtop (n - 1) :]"
proof -
  have A: "{.⊤.} o [: x ↝ y . f x = y:] = [-f-]"
    by (simp add: fun_eq_iff update_def demonic_def assert_def le_fun_def)
  have "IterateOmegaA [-f-] = IterateOmegaA ({.⊤.} o [: x ↝ y . f x = y:])"
    by (simp add: A)
  also have "... = [: INF x. (λx y. (f x) = y) ^^ x OO eqtop (x - Suc 0) :]"
    by (subst IterateOmegaA_spec, simp add: assert_true_skip_a)
  finally show ?thesis
    by simp
qed


lemma power_example: "(n::nat) > 0 ⟹ 
    ((λ((u::nat ⇒ 'a, y::nat ⇒ 'a), x::nat ⇒ 'b) ((u', y'), x'). u = u' ∧ u = y' ∧ x = x') ^^ n)
    = (λ((u, y), x) ((u', y'), x'). u = u' ∧ u = y' ∧ x = x')"
  apply (induction n, auto)
  apply (case_tac n, simp_all)
  by (simp_all add: OO_def, auto)

lemma power_example_a: "(n::nat) > 0 ⟹ 
    ((λ((u::nat ⇒ 'a, y::nat ⇒ 'a), x::nat ⇒ 'b) ((u', y'), x'). u = u' ∧ u = y' ∧ x = x') ^^ n) ((a,b), c) ((a', b'), c')
    = (a = a' ∧ a = b' ∧ c = c')"
  by (subst power_example, simp_all)

lemma example_simp: "{:x ↝ ((u, y), x').x = x':} ∘ [:((u, y), x)↝((u', y'), x').u = u' ∧ u = y' ∧ x = x':] ∘ [-λ((u, y), x). y-] = {: ⊤ :}"
  by (simp add: fun_eq_iff demonic_def angelic_def update_def le_fun_def)
      
lemma Feedback_example: "Feedback([-u::nat ⇒ 'a, x::nat ⇒ 'b ↝ u, u-]) = {:⊤:}"
proof -
  have A:"[-λ((u, y), x). ((u, x), x)-] ∘ [-λ(u, x). (u, u)-] ** Skip = [-λ((u, y), x) . ((u,u), x)-]"
    apply (simp add: prod_update_skip update_comp)
    by (rule_tac f = update in arg_cong, auto)
      
  have B: " (λx. (=) (case x of (x, xa) ⇒ (case x of (u, y) ⇒ Pair (u, u)) xa)) 
    = (λ ((u::nat ⇒ 'a,y::nat ⇒ 'a),x::nat ⇒ 'b)  ((u', y'), x') . u = u' ∧ u = y' ∧ x = x')"
    by auto
      
  have C: "(INF n. (λ((u::nat ⇒ 'a, y::nat ⇒ 'a), x::nat ⇒ 'b) ((u'::nat ⇒ 'a, y'::nat ⇒ 'a), x'::nat ⇒ 'b). u = u' ∧ u = y' ∧ x = x') ^^ n OO eqtop (n - Suc 0))
    =  (λ((u, y), x) ((u', y'), x'). u = u' ∧ u = y' ∧ x = x')"
    apply (subst fun_eq_iff, subst (4) fun_eq_iff, safe)
       apply (simp_all add: OO_def)
      apply (subst fun_eq_iff, safe)
       apply (drule_tac x = "Suc (Suc x)" in spec, safe)
      apply (subst (asm) power_example_a)
        apply simp
      apply (simp add: eqtop_prod_def)

      apply (subst fun_eq_iff, safe)
       apply (drule_tac x = "Suc (Suc x)" in spec, safe)
      apply (subst (asm) power_example_a)
        apply simp
      apply (simp add: eqtop_prod_def, auto)
    

      apply (subst fun_eq_iff, safe)
       apply (drule_tac x = "Suc (Suc x)" in spec, safe)
      apply (subst (asm) power_example_a)
        apply simp
     apply (simp add: eqtop_prod_def)
    apply (case_tac n, simp)
      by (subst power_example_a, simp_all)
      
      
    have "Feedback([-u::nat ⇒ 'a,x::nat ⇒ 'b ↝ u,u-]) = {:x ↝ ((u, y), x').x = x':} ∘ 
    IterateOmegaA ([-λ((u, y), x) . ((u,u), x)-]) ∘ [-λ((u, y), x). y-]"
    by (simp add: Feedback_def A)
  also have "... = {:x ↝ ((u, y::nat ⇒ 'a), x').x = x':} 
      ∘ [: INF n. (λ((u, y), x) ((u', y'), x'). u = u' ∧ u = y' ∧ x = x') ^^ n 
      OO eqtop (n - Suc 0) :] ∘ [-λ((u, y), x). y-]"
    by (simp add: IterateOmegaA_update B)
      
  also have "... = {:x ↝ ((u, y::nat ⇒ 'a), x').x = x':} ∘ [:((u, y), x)↝((u', y'), x').u = u' ∧ u = y' ∧ x = x':] ∘ [-λ((u, y), x). y-]"
    by (simp add: C)
  also have "... = {:⊤:}"
    by (simp add: example_simp)
  finally show ?thesis
    by simp
qed
      
  (* Feedback for deterministic systems *)
  lemma Feedback_deterministic: "init = (λ x . x = a) ⟹ 
    DelayFeedback init (feedback({.(u, s, x).  p (u, s, x).} ∘ [-λ(u, s, x). (f s x, g u s x, h u s x)-])) =
      Feedback ([- u,x ↝  u || x -] o (DelayFeedback init ([- λ (s,(u,x)) . (u, s, x) -] 
           o ({. p .} ∘ [- u, s, x ↝ f s x, g u s x, h u s x -]) 
           o [- v, s, y ↝ s, v, y -])) o [- z ↝ fst o z, snd o z -])"
    apply (subst DelayFeedback_feedback_simp, simp)
    apply (subst input_output_switch)

    apply (simp add: Feedback_def)
    apply (simp add: IterateOmegaA_DelayFeedback)
    apply (unfold comp_assoc)
    apply (simp add: update_def demonic_demonic OO_def split_def)
    apply (unfold comp_assoc [THEN sym])
    apply (simp add: angelic_assert)
    apply (subst angelic_not_demonic [of _ "(λb c. (∀n xb. p (UUc (fst (fst c)) a f g (snd c) n xb, ssc a (UUc (fst (fst c)) a f g (snd c) n) g (snd c) n xb, snd c xb)))"])
    apply auto [1]
    apply simp
    apply (simp add: SSS)
    apply (simp add: SSSb)
    by (simp add: SSSd)
      
 

  lemma DF_fb_simp: "init = (λ x . x = a) ⟹ 
    DelayFeedback init (feedback({.(u, s, x).  p (u,s, x).} ∘ [- u, s, x ↝ f s x, g u s x, h u s x-])) = 
     {.x.∀n. p (f (SS a g f x n) (x n), SS a g f x n, x n).} ∘ [:y↝z. z = (λk. h (f (SS a g f y k) (y k)) (SS a g f y k) (y k)):]"
    apply (subst DelayFeedback_feedback_simp, simp)
    apply (simp add: update_def demonic_demonic OO_def split_def)
    apply (simp add: SSSb)
    by (simp add: SSSd)

  lemma DF_fb_simp_a: "init = (λ x . x = a) ⟹ 
    DelayFeedback init (feedback({. p .} ∘ [-λ(u, s, x). (f s x, g u s x, h u s x)-])) = 
     {.x.∀n. p (f (SS a g f x n) (x n), SS a g f x n, x n).} ∘ [:y↝z. z = (λk. h (f (SS a g f y k) (y k)) (SS a g f y k) (y k)):]"
     by (simp add: DF_fb_simp [THEN sym])

  lemma FB_DF_simp: "init = (λ x . x = a) ⟹ 
        Feedback ([- u,x ↝  nzip u x -] o (DelayFeedback init ([- λ (s,(u,x)) . (u, s, x) -] 
           o ({.(u, s, x).  p (u, s, x).} ∘ [- u, s, x ↝ f s x, g u s x, h u s x-]) 
           o [- v, s, y ↝ s, v,y -])) o [- z ↝ fst o z, snd o z -]) 
           =  {.x.∀n. p (f (SS a g f x n) (x n), SS a g f x n, x n).} ∘ [:y↝z. z = (λk. h (f (SS a g f y k) (y k)) (SS a g f y k) (y k)):]"
    apply (subst input_output_switch)

    apply (simp add: Feedback_def)
    apply (simp add: IterateOmegaA_DelayFeedback)
    apply (unfold comp_assoc)
    apply (simp add: update_def demonic_demonic OO_def split_def)
    apply (unfold comp_assoc [THEN sym])
    apply (simp add: angelic_assert)
    apply (subst angelic_not_demonic [of _ "(λb c. (∀n xb. p (UUc (fst (fst c)) a f g (snd c) n xb, ssc a (UUc (fst (fst c)) a f g (snd c) n) g (snd c) n xb, snd c xb)))"])
    apply auto [1]
    apply simp
    by (simp add: SSS)


   (* example *)

   definition "init_ex = (λ s . s = (0::nat))" 
   definition "p1 = (λ(u,s,x). u = s + 1)"
   definition "f1 = (λ s x. s + 1)"
   definition "g1 = (λ u s x. s + 1)"
   definition "h1 = (λ u s x. x)"
   definition "spec_ex = {.(u, s, x). p1 (u, s, x).} o [-λ (u, s, x). (f1 s x, g1 u s x, h1 u s x)-]"

   lemma DelayFeedback_feedback_ex: "DelayFeedback init_ex (feedback ( spec_ex )) = [:y ↝ z. z = y:] "
    apply (simp add: spec_ex_def)
    by (cut_tac init=init_ex and p=p1 and f=f1 and g=g1 and h=h1 in  DF_fb_simp, simp_all add: f1_def g1_def h1_def p1_def assert_true_skip_a init_ex_def)


   lemma jjj: " [:x↝((x'', y), x').x'' = x ∧ x = x':] ∘ ([: λs. □ (λs. s 0 = b) :] ** Skip) ** Skip = [:x↝((x'', y), x').(□ (λs. s 0 = b)) x'' ∧ x' = x:]"
    apply (simp add: Prod_demonic_skip)
    apply (simp add: demonic_demonic)
    apply(rule_tac f ="demonic" in arg_cong)
    apply (simp add: fun_eq_iff OO_def)
    by auto


   lemma [simp]: "(∀a. (□ (λs. s 0 = b)) a ⟶ (∀n xb. UUc a 0 (λs x. Suc s) (λu s x. Suc s) x n xb = Suc (ssc 0 (UUc a 0 (λs x. Suc s) (λu s x. Suc s) x n) (λu s x. Suc s) x n xb)))
    = ((∀n xb. UUc (λ i . b) 0 (λs x. Suc s) (λu s x. Suc s) x n xb = Suc (ssc 0 (UUc (λ i . b) 0 (λs x. Suc s) (λu s x. Suc s) x n) (λu s x. Suc s) x n xb)))"

    apply auto
    apply (simp_all add: always_def at_fun_def)
    apply (subgoal_tac "a = (λ i . b)")
    apply simp
    by (simp add: fun_eq_iff)

   lemma [simp]: "((∀n xb. UUc (λ i . b) 0 (λs x. Suc s) (λu s x. Suc s) x n xb = Suc (ssc 0 (UUc (λ i . b) 0 (λs x. Suc s) (λu s x. Suc s) x n) (λu s x. Suc s) x n xb))) = False"
    apply safe
    apply (frule_tac x = 0 in spec)
    apply (drule_tac x = 0 in spec)
    apply (drule_tac x = "Suc 0" in spec)
    apply (drule_tac x = "Suc (Suc 0)" in spec)
    by (simp add: UUc.simps ssc.simps)
    


    lemma FeedbackA_example: "init = (λ s . s = b) ⟹ 
        FeedbackA (InitDF init) ([- u,x ↝ nzip u x -] o (DelayFeedback init_ex ([- λ (s,(u,x)) . (u, s, x) -] 
           o spec_ex 
           o [- v, s, y ↝ s, v, y -])) o [- z ↝ fst o z, snd o z -])  = 
        ⊥"
       apply (simp add: spec_ex_def InitDF_def init_ex_def)
       apply (simp add: FeedbackA_def)
       apply (subst input_output_switch)
       apply (simp add: IterateOmegaA_DelayFeedback)
       apply (unfold comp_assoc)
       apply (simp add: update_def demonic_demonic OO_def)
       apply (unfold comp_assoc [THEN sym])
       apply (simp add: jjj)
       apply (simp add: demonic_assert_comp)
       by (simp add: comp_assoc demonic_demonic split_def OO_def p1_def f1_def g1_def h1_def)

   definition "init_ex_a = (λ s . s = (0::nat))" 
   definition "p1_a = (λ (u, s, x) . u = s + 1)"
   definition "f1_a = (λ s x. s + 1)"
   definition "g1_a = (λ u s x. s + 1)"
   definition "h1_a = (λ u s x. x + s)"
   definition "spec_ex_a = {.p1_a.} o [-λ (u, s, x). (f1_a s x, g1_a u s x, h1_a u s x)-]"

   lemma [simp]: "SS 0 (λu s x. Suc s) (λs x. Suc s) y k = k"
    by (induction k, simp_all add: SS.simps)

   lemma DelayFeedback_feedback_ex_a: "DelayFeedback init_ex_a (feedback ( spec_ex_a )) = [:y ↝ z. z = (λk. y k + k):] "
    apply (simp add: spec_ex_a_def)
    apply (subst DF_fb_simp_a, simp add: init_ex_a_def)
    by (simp add:  f1_a_def g1_a_def h1_a_def p1_a_def assert_true_skip_a init_ex_def)
end