Theory IterateOperators

(**-----------------------------------------------------------------------------
 * © [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{DelayFeedback}Iterate Operators›

theory IterateOperators imports "../RefinementReactive/RefinementReactive"
begin

definition append_inf :: "'a list ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)" (infixr ".." 65) where
    "(xs..s) i = (if i < length xs then xs ! i else s (i - (length xs)))"

lemma [simp]: "[x 0] .. x[Suc 0..] = x"
  by (simp add: fun_eq_iff append_inf_def)

lemma [simp]: "([a] .. x)[Suc 0 ..] = x"
  by (simp add: fun_eq_iff append_inf_def)

lemma [simp]: "([a] .. x) 0 = a"
  by (simp add: fun_eq_iff append_inf_def)

definition "SkipNext S = [: x ↝ a, b . a = x ∧ b = x[Suc 0..] :] o (Prod Skip S) o [: a, b ↝ x .  x = cat (Suc 0) a b :]"

definition "Next S = [:x ↝ y . y = x[Suc 0..]:] o S o [:y ↝ x . y = x[Suc 0..]:]"
    
definition "NextAngelic S = {: x ↝ y . y = x[Suc 0..]:} o S o {:y ↝ x . y = x[Suc 0..] :}"

definition "SkipTop n = [:eqtop n:]"

lemma SkipNext_Next: "SkipNext S = Next S ∥ SkipTop (Suc 0)"
proof (simp add: SkipNext_def Next_def Prod_def fusion_def demonic_def le_fun_def prod_pred_def Skip_def SkipTop_def fun_eq_iff, safe)
  fix x :: "'a ⇒ bool" fix xa :: 'a fix p :: "'a ⇒ bool" fix p' :: "'a ⇒ bool"
  assume "∀a b. p a ∧ p' b ⟶ x (cat (Suc 0) a b)"
  from this have A: "⋀ a b .  p a ⟹ p' b ⟹ x (cat (Suc 0) a b)"
    by simp
  assume [simp]: "p xa"
  assume [simp]: "S p' (xa[Suc 0 ..])"
  let ?p = "λ x . p' (x[Suc 0..])"
  let ?p' = "λ x . ∃ y .p (cat (Suc 0) x y)"
  have [simp]: "(⋀ xa y. ?p xa ⟹ p (cat (Suc 0) xa y) ⟹ x xa)"
    by (drule A, simp, simp) 
  have [simp]: "⋀x. eqtop (Suc 0) xa x ⟹ p (cat (Suc 0) x (xa[Suc 0..]))"
    by (cut_tac x = "cat (Suc 0) x (xa[Suc 0 ..])" and y = xa and n = "Suc 0" in eqtop_tail, simp_all add: eqtop_sym)     
  from this have [simp]: "∀x. eqtop (Suc 0) xa x ⟶ ?p' x"
    by blast
  have [simp]: "[: λy x. y = x[Suc 0 ..] :] (λx. p' (x[Suc 0 ..])) = p'"
    apply (simp add: fun_eq_iff demonic_def le_fun_def, safe)
    by (drule_tac x = "cons x" in spec, simp)
  show "∃p p'. (∀xa. p xa ∧ p' xa ⟶ x xa) ∧ S ([: λy x. y = x[Suc 0 ..] :] p) (xa[Suc 0 ..]) ∧ (∀x. eqtop (Suc 0) xa x ⟶ p' x)"
    by (rule_tac x = ?p in exI, rule_tac x = ?p' in exI, auto)
next
  fix x :: "'a ⇒ bool" fix xa :: 'a fix p :: "'a ⇒ bool" fix p' :: "'a ⇒ bool"
  assume [simp]: "∀xa. p xa ∧ p' xa ⟶ x xa"
  assume [simp]: " S ([: λy x. y = x[Suc 0 ..] :] p) (xa[Suc 0 ..])"
  assume [simp]: " ∀x. eqtop (Suc 0) xa x ⟶ p' x"
  show "∃p p'. (∀a b. p a ∧ p' b ⟶ x (cat (Suc 0) a b)) ∧ p xa ∧ S p' (xa[Suc 0 ..])" 
    apply (rule_tac x = "λ x . ∀ y .p' (cat (Suc 0) x y)" in exI)
    apply (rule_tac x = "[: λy x. y = x[Suc 0 ..] :] p" in exI)
    by (auto simp add: demonic_def le_fun_def)
qed

lemma [simp]: "SkipTop 0 = Havoc"
  by (simp add: SkipTop_def Havoc_def)

lemma proj_skip [simp]: "[: y ↝ x. y = x[Suc 0 ..] :] ∘ [: x ↝ y. y = x[Suc 0 ..] :] = Skip"
proof - 
  have [simp]: "[: λy x. y = x[Suc 0 ..] :] ∘ [: λx y. y = x[Suc 0 ..] :] = [: (λy x. y = x[Suc 0 ..]) OO (λx y. y = x[Suc 0 ..]) :]" 
    by (simp add: demonic_demonic)
  have [simp]:" (λy x. y = x[Suc 0 ..]) OO (λx y. y = x[Suc 0 ..]) = (=)"
    by (simp add: fun_eq_iff OO_def, auto)
  show ?thesis by (simp add: demonic_eq_skip)
qed

 lemma Next_comp: "Next (S o T) = Next S o Next T"
  proof -
    have "Next (S o T) = [: λx y. y = x[Suc 0 ..] :] ∘ S ∘ ([: λy x. y = x[Suc 0 ..] :] ∘ [: λx y. y = x[Suc 0 ..] :]) ∘ T ∘ [: λy x. y = x[Suc 0 ..] :]"
      by (simp add: Next_def comp_assoc)
    also have "... =  Next S o Next T"
      by (unfold Next_def comp_assoc, simp)
    finally show ?thesis by simp
  qed
      
lemma transp_ref_comp: "transp r ⟹ [:r:] ≤ [:r:] o [:r:]"
  apply (simp add: le_fun_def demonic_def)
  by (unfold transp_def, blast)

lemma fusion_comp_demonic: "transp r ⟹ (S o T) ∥ [:r:] ≤ (S ∥ [:r:]) o (T ∥ [:r:])"
proof (simp add: fusion_def  le_fun_def, safe)
  fix x :: "'a ⇒ bool" fix xa :: 'a fix p :: "'a ⇒ bool" fix p' :: "'a ⇒ bool"
  assume A: "transp r"
  assume [simp]: "∀xa. p xa ∧ p' xa ⟶ x xa"
  assume [simp]: "S (T p) xa"
  assume "[: r :] p' xa"
  from A and this have [simp]: "[: r :] ([: r :] p') xa"
    by (simp add: demonic_def le_fun_def, metis transp_def)
  have "⋀ xa . T p xa ⟹ [: r :] p' xa ⟹ (∀xa. p xa ∧ p' xa ⟶ x xa) ∧ T p xa ∧ [: r :] p' xa"
    by simp
  from this have [simp]:"⋀ xa . T p xa ⟹ [: r :] p' xa ⟹ ∃p p'. (∀xa. p xa ∧ p' xa ⟶ x xa) ∧ T p xa ∧ [: r :] p' xa"
    by blast
  have "(∀xa. T p xa ∧ [:r:] p' xa ⟶ (∃p p'. (∀xa. p xa ∧ p' xa ⟶ x xa) ∧ T p xa ∧ [: r :] p' xa)) ∧ S (T p) xa ∧ [: r :] ([:r:] p') xa"
    by simp
  from this show "∃p p'. (∀xa. p xa ∧ p' xa ⟶ (∃p p'. (∀xa. p xa ∧ p' xa ⟶ x xa) ∧ T p xa ∧ [: r :] p' xa)) ∧ S p xa ∧ [: r :] p' xa"
    by blast
qed

lemma fusion_comp_eqtop: "(S o T) ∥ [:eqtop n:] ≤ (S ∥ [:eqtop n:]) o (T ∥ [: eqtop n:])"
  by (metis eqtop_tran fusion_comp_demonic transpI)

lemma SkipNext_comp_a[simp]: "SkipNext (S o T) ≤ (SkipNext S) o (SkipNext T)"
  by (simp add: SkipNext_Next SkipTop_def Next_comp, rule fusion_comp_eqtop)

definition "auxfun p' T x xa = (SUPREMUM {b. p' b} (λ b . (Sup {p' . (∃ p . (∀ a b. p a ∧ p' b ⟶ x (cat (Suc 0) a b)) ∧ p xa ∧ T p' b)})))"

lemma SkipNext_comp_b[simp]: "mono S ⟹ mono T⟹ SkipNext (S o T) ≥ (SkipNext S) o (SkipNext T)"
proof (simp add: SkipNext_def le_fun_def Prod_def prod_pred_def Skip_def demonic_def, safe)
  fix x :: "'a ⇒ bool" fix xa :: 'a fix p :: "'a ⇒ bool"  fix p':: "'a ⇒ bool"
  assume [simp]: "p xa"
  assume "∀a b. p a ∧ p' b ⟶ (∃p p'. (∀a b. p a ∧ p' b ⟶ x (cat (Suc 0) a b)) ∧ p (cat (Suc 0) a b) ∧ T p' b)"
  from this have D:"⋀ b . p' b ⟹ (∃p p'. (∀a b. p a ∧ p' b ⟶ x (cat (Suc 0) a b)) ∧ p (cat (Suc 0) xa b) ∧ T p' b)"
    by (drule_tac x = "xa" in spec, simp)
  from this have  E: "⋀b xb f p . p' xb ⟹ f b ⟹ ∀a b. p a ∧ f b ⟶ x (cat (Suc 0) a b) ⟹ p xa ⟹ T f xb ⟹ x (cat (Suc 0) xa b)"
    by simp
  from this have [simp]: "⋀b. auxfun p' T x xa b ⟹ x (cat (Suc 0) xa b)"
    by (auto simp add: auxfun_def)
  have [simp]: "⋀xb p p'a. p' xb ⟹ ∀a b. p a ∧ p'a b ⟶ x (cat (Suc 0) a b) ⟹ p (cat (Suc 0) xa xb) ⟹ T p'a xb ⟹  p'a ≤ auxfun p' T x xa"
    apply (simp add: le_fun_def auxfun_def)
    apply (cut_tac b = xb in D, auto)
    apply (rule_tac x = xb in exI, simp)
    apply (rule_tac x = p'a in exI, safe, simp)
    apply (rule_tac x = "λ x . x = xa" in exI, simp, safe)
    by (drule_tac x = "cat (Suc 0) xa xb" in spec, simp_all)
  assume F: "mono T"
  have [simp]: "⋀xb p p'a. p' xb ⟹ ∀a b. p a ∧ p'a b ⟶ x (cat (Suc 0) a b) ⟹ p (cat (Suc 0) xa xb) ⟹ T p'a xb ⟹ T (auxfun p' T x xa) xb"
    apply (cut_tac F)
    apply (drule_tac x = p'a and y = "auxfun p' T x xa" in monoD, simp_all)
    by (simp add: le_fun_def)

  have "⋀xb. p' xb ⟹ T (auxfun p' T x xa) xb"
    by (cut_tac b = xb in D, auto)
  from this have A: "p' ≤ T (auxfun p' T x xa)"
    by (simp_all add: le_fun_def)
  assume B: "S p' (xa[Suc 0 ..])"
  assume "mono S"
  from A and B and this have [simp]: "S (T (auxfun p' T x xa)) (xa[Suc 0 ..])"
    by (metis monoD predicate1D)
  let ?p =  "λ x . x = xa"
  let ?p' = "auxfun p' T x xa"
  have "(∀a b. ?p a ∧ ?p' b ⟶ x (cat (Suc 0) a b)) ∧ ?p xa ∧ S (T ?p') (xa[Suc 0 ..])"
    by simp
  from this show "∃p p'. (∀a b. p a ∧ p' b ⟶ x (cat (Suc 0) a b)) ∧ p xa ∧ S (T p') (xa[Suc 0 ..])"
    by (rule_tac x = ?p in exI, rule_tac x = ?p' in exI, simp)
qed

lemma SkipNext_comp: "mono S ⟹ mono T⟹ SkipNext (S o T) = (SkipNext S) o (SkipNext T)"
  by (rule antisym, simp_all)

lemma Next_fusion: "Next (S ∥ T) = (Next S) ∥ (Next T)"
proof (simp add: Next_def fun_eq_iff fusion_def demonic_def le_fun_def, safe)
  fix x :: "'a ⇒ bool" fix xa::'b fix p::"'a ⇒ bool" fix p'::"'a ⇒ bool"
  assume [simp]: "∀xa. p xa ∧ p' xa ⟶ (∀xb. xa = xb[Suc 0 ..] ⟶ x xb)"
  assume [simp]: "S p (xa[Suc 0 ..])"
  assume [simp]: "T p' (xa[Suc 0 ..])"
  let ?p = "λx. p (x[Suc 0 ..])"
  let ?p' = "λx. p' (x[Suc 0 ..])"
  have [simp]: "⋀ p' . [: λy x. y = x[Suc 0 ..] :] (λx. p' (x[Suc 0 ..])) = p'"
    apply (simp add: fun_eq_iff demonic_def le_fun_def, safe)
    by (drule_tac x = "cons x" in spec, simp)
  show "∃p p'. (∀xa. p xa ∧ p' xa ⟶ x xa) ∧ S ([: λy x. y = x[Suc 0 ..] :] p) (xa[Suc 0 ..]) ∧ T ([: λy x. y = x[Suc 0 ..] :] p') (xa[Suc 0 ..])"
    by (rule_tac x = ?p in exI, rule_tac x = ?p' in exI, simp)
next
  fix x :: "'a ⇒ bool" fix xa::'b fix p::"'a ⇒ bool" fix p'::"'a ⇒ bool"
  assume [simp]: "∀xa. p xa ∧ p' xa ⟶ x xa"
  assume [simp]: "S ([: λy x. y = x[Suc 0 ..] :] p) (xa[Suc 0 ..])"
  assume [simp]: "T ([: λy x. y = x[Suc 0 ..] :] p') (xa[Suc 0 ..])"
  show "∃p p'. (∀xa. p xa ∧ p' xa ⟶ (∀xb. xa = xb[Suc 0 ..] ⟶ x xb)) ∧ S p (xa[Suc 0 ..]) ∧ T p' (xa[Suc 0 ..])"
    apply (rule_tac x = "[: λy x. y = x[Suc 0 ..] :] p" in exI, simp)
    apply (rule_tac x = "[: λy x. y = x[Suc 0 ..] :] p'" in exI, simp)
    by (auto simp add: demonic_def le_fun_def)
qed


lemma fusion_SkipTop_idemp [simp]: "SkipTop n ∥ SkipTop n = SkipTop n"
  by (simp add: SkipTop_def)

lemma SkipNext_fusion: "SkipNext (S ∥ T) = (SkipNext S) ∥ (SkipNext T)"
proof -
  have "(SkipNext S) ∥ (SkipNext T) = (Next S ∥ SkipTop (Suc 0)) ∥ (Next T ∥ SkipTop (Suc 0))"
    by (simp add: SkipNext_Next)
  also have "... = Next S ∥ (SkipTop (Suc 0) ∥ Next T) ∥ (SkipTop (Suc 0))"
    by (simp add: fusion_assoc)
  also have "... = Next S ∥ (Next T ∥ SkipTop (Suc 0)) ∥ SkipTop (Suc 0)"
    by (simp add: fusion_comute)
  also have "... = Next S ∥ Next T ∥ SkipTop (Suc 0)"
    by (simp add: fusion_assoc [THEN sym])
  also have "... = SkipNext (S ∥ T)"
    by (simp add: SkipNext_Next Next_fusion)
  finally show ?thesis by simp
qed

lemma SkipNext_SkipTop: "SkipNext (SkipTop n) = SkipTop (Suc n)"
proof -
  have [simp]: "⋀x xa . (∃v::'a. eqtop n (x[Suc (0::nat) ..]) v ∧ xa = cat (Suc (0::nat)) x v) = eqtop (Suc n) x xa"
    apply (subst eqtop_Suc_a, auto)
    apply (rule_tac x = "xa[Suc 0..]" in exI, auto)
    apply (rule_tac n = "Suc 0" in eqtop_tail, simp_all)
    by (simp add: eqtop_sym)
  have [simp]: "((λ(x::'a) (u::'a, v::'a). x = u ∧ eqtop n (x[Suc (0::nat) ..]) v) OO (λ(a::'a, b::'a) x::'a. x = cat (Suc (0::nat)) a b))
      = (λ x y . ∃ v . eqtop n (x[Suc (0::nat) ..]) v ∧ y = cat (Suc (0::nat)) x v)"
    by (simp add: fun_eq_iff OO_def)
  have [simp]: "⋀ f g r . (λ x (a, b) . a = f x ∧ b = g x) OO r = (λ x y . r (f x, g x) y)"
    by (auto simp add: fun_eq_iff)
  show ?thesis
    by (simp add: SkipNext_def SkipTop_def Prod_skip_demonic demonic_demonic)
qed
  
lemma SkipTop_SkipNext: "SkipTop n = (SkipNext ^^ n) Havoc"
  by (induction n, simp_all add: SkipNext_SkipTop [THEN sym])

lemma SkipNext_power: "(SkipNext ^^ (Suc n)) S = (Next ^^ (Suc n)) S ∥ SkipTop (Suc n)"
proof (induction n)
  case 0
  show ?case by (simp add: SkipNext_Next SkipTop_def)
  case (Suc n)
  from this show ?case
    apply (simp add: SkipNext_Next Next_fusion)
    apply (simp add: fusion_assoc [THEN sym])
    apply (unfold SkipNext_Next [THEN sym])
    by (simp add: SkipNext_SkipTop)
qed

lemma Next_demonic: "Next [:r:] = [:⨀ r:]"
  by (auto simp add: fun_eq_iff demonic_def Next_def le_fun_def next_def at_fun_def)

lemma SkipNext_demonic: "SkipNext {.p.} = {.⨀ p.}"
  apply (simp add: fun_eq_iff demonic_def SkipNext_def le_fun_def next_def at_fun_def Prod_def assert_def prod_pred_def)
  apply safe
  apply (drule_tac x = "xa" in spec)
  apply (drule_tac x = "xa[Suc 0 ..]" in spec)
  apply simp
  apply (rule_tac x = "λ x . x = xa" in exI)
  apply (rule_tac x = "λ x . x = xa[Suc 0..]" in exI)
  by auto 

lemma NextAngelic_angelic: "NextAngelic ({:r::(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ bool:}) = {:⨀ r:}"
  apply (simp add: fun_eq_iff)
  apply (simp add:  angelic_def NextAngelic_def le_fun_def next_def at_fun_def assert_def bot_fun_def fun_eq_iff)
  apply safe
  apply (rule_tac x = "xd" in exI, simp)
  apply (subgoal_tac "(xb = xa[Suc 0 ..]) ∧ (xc = xd[Suc 0 ..])")
  apply simp
  apply (simp add: append_inf_def)
  apply (rule_tac x = "xa[Suc 0..]" in exI)
  apply simp
  apply (rule_tac x = "xb[Suc 0..]" in exI)
  by auto
    
lemma Next_assert_demonic: "Next ({.p.} o [:r:]) = {.⨀ p.} o [:⨀ r:]"
  apply (simp add: fun_eq_iff demonic_def Next_def le_fun_def next_def at_fun_def assert_def)
  by blast

lemma Next_angelic_demonic: "Next ({:r:} o [:r':]) = {:⨀ r:} o [:⨀ r':]"
  apply (simp add: fun_eq_iff demonic_def Next_def le_fun_def next_def at_fun_def angelic_def)
  apply safe
  apply (rule_tac x = "cons xb" in exI, simp)
  by metis

lemma eqtop_Suc_zero: "eqtop (Suc 0) = (λ x y . x 0 = y 0)"
  apply (simp add: fun_eq_iff)
  apply (subst (3) zero_Nat_def)
  by (subst (4) zero_Nat_def, simp)

definition "idnext r = ⨀ r ⊓ eqtop (Suc 0)"

lemma SkipNext_assert_demonic: "SkipNext ({.p.} o [:r:]) = {. ⨀ p .} ∘ [: idnext r :]"
  apply (simp add: SkipNext_Next Next_assert_demonic idnext_def SkipTop_def)
  apply (cut_tac p = "⨀ p" and r = "⨀ r" and p' = ⊤ and r' = "eqtop (Suc 0)" in fusion_spec)
  by (simp add: assert_true_skip)

lemma Next_assert_demonic2: "Next (λ q . {.p.} ([:r:] q)) = {.⨀ p.} o [:⨀ r:]"
  apply (simp add: fun_eq_iff demonic_def Next_def le_fun_def next_def at_fun_def assert_def)
  by blast

lemma Iterate_Next_assert_demonic: "(Next^^n) ({.p.} o [:r:]) = {.(next^^n)p.} o [:(next^^n) r:]"
   apply (induction n)
   apply simp
   by (simp add: Next_assert_demonic2)

lemma power_SkipNext_assert_demonic: "(SkipNext^^n) ({.p.} o [:r:]) = {.(next^^n)p.} o [:(idnext^^n) r:]"
   apply (induction n)
   apply simp
   apply (simp add: SkipNext_assert_demonic del: comp_apply)
   apply simp
   apply (unfold comp_def [symmetric], simp add: SkipNext_assert_demonic)
   by (simp add: fun_eq_iff)

lemma Iterate_Next_demonic: "(Next ^^ n) [:r:] = [:(next ^^ n) r:]"
   apply (induction n)
   apply simp_all
   by (simp add: Next_demonic)

definition "Always S = Fusion (λ n . (Next ^^ n) S)"
    
lemma Always_demonic: "Always [:r:] = [:□ r:]"
  by (simp add: Always_def Fusion_demonic Iterate_Next_demonic iterate_next always_def)
    
lemma Always_assert_demonic: "Always ({.p.} o [:r:]) = {.□ p.} o [:□ r:]"
  by (simp add: Always_def Fusion_spec Iterate_Next_assert_demonic iterate_next always_def)
   
lemma SkipNext_simp: "SkipNext S Q x = 
    (∃p p'. (∀a b. p a ∧ p' b ⟶ Q (cat (Suc 0) a b)) ∧ p x ∧ S p' (x[Suc 0..]))"
  by (simp add: SkipNext_def Prod_def prod_pred_def Skip_def demonic_def le_fun_def)

type_synonym ('a, 'b) trans = "('b ⇒ bool) ⇒ ('a ⇒ bool)"

primrec Iterate :: "(('a, 'a) trans ⇒ ('a, 'a) trans) ⇒ ('a, 'a) trans ⇒ nat ⇒ ('a, 'a) trans" where
  "Iterate F S 0 = Skip" |
  "Iterate F S (Suc n) = (Iterate F S n) o ((F ^^ n) S)"

  
definition "Mask n S = S o (SkipTop n)"
  
definition "IterateNextMask S n = Mask n (Iterate Next S n)"
  
lemma IterateNextMask_simp: "IterateNextMask S = (λ n . Mask n (Iterate Next S n))"
  by (simp add: fun_eq_iff IterateNextMask_def)

definition "IterateSkipNextMask S n = Mask n (Iterate SkipNext S n)"
  
lemma IterateSkipNextMask_simp: "IterateSkipNextMask S = (λ n . Mask n (Iterate SkipNext S n))"
  by (simp add: fun_eq_iff IterateSkipNextMask_def)

definition "IterateOmegaNextMask S = Fusion (IterateNextMask S)"

definition "IterateOmegaSkipNextMask S = Fusion (IterateSkipNextMask S)"

definition "AddUnitDelay S = ([:u, x, y ↝ a, b . a = u (0::nat) ∧ b = x (0::nat):] o S o [:c, d ↝ u', x', y' . u' (Suc 0) = c ∧ y' (0::nat) = d:]) 
      ∥ [:u, x, (y::nat ⇒ 'a) ↝ u', x', (y'::nat ⇒'a) . u' (0::nat) = u (0::nat) ∧ x' = x:]"
 
lemma AddUnitDelay_spec: "AddUnitDelay ({.u, x . p u x.} o [:u, x ↝ u', y . r u u' x y:]) = 
   {.u, x, y . p (u 0) (x 0).} o [:u, x, y ↝ u', x', y' . r (u 0) (u' (Suc 0)) (x 0) (y' 0) ∧ x = x' ∧ u 0 = u' 0:]"
   (is "?L = ?R")
  proof (unfold AddUnitDelay_def)
    have "([: u::nat ⇒ 'a, x::nat ⇒ 'b, y::nat ⇒ 'c ↝ a::'a, b::'b . a = u (0::nat) ∧ b = x (0::nat) :] 
           ∘ ({.x::'a, y::'b. p x y.} ∘ [: u::'a, x::'b ↝ u'::'a, y::'c . r u u' x y :]) ∘ [: c::'a, d::'c ↝ u'::nat ⇒ 'a,
            x'::nat ⇒ 'b, y'::nat ⇒ 'c . u' (Suc (0::nat)) = c ∧ y' (0::nat) = d :])
       = {.u ,x, y. p (u (0::nat)) (x (0::nat)).} o [: u, x, y ↝ a, b . a = u (0::nat) ∧ b = x (0::nat) :] 
           ∘ [: u, x ↝ u', y . r u u' x y :] ∘ [: c, d ↝ u', x', y' . u' (Suc 0) = c ∧ y' (0::nat) = d :]"
       (is "?A = ?B")
     apply (simp add: comp_assoc [THEN sym] demonic_assert_comp)
     apply (subgoal_tac "(λx::(nat ⇒ 'a) × (nat ⇒ 'b) × (nat ⇒ 'c). ∀(a::'a) b::'b. (case x of (u::nat ⇒ 'a, xa::nat ⇒ 'b, y::nat ⇒ 'c) ⇒ λ(a::'a, b::'b). a = u (0::nat) ∧ b = xa (0::nat)) (a, b) ⟶ p a b ) 
        = (λ(u, x, y). p (u (0::nat)) (x (0::nat)))")
     apply simp_all
     by (simp add: fun_eq_iff)
   also have "... = {.u ,x, y. p (u (0::nat)) (x (0::nat)).} o [: (u::nat ⇒ 'a), (x::nat ⇒ 'b), (y::nat ⇒ 'c) ↝ u', x', y' . r (u (0::nat)) (u' (Suc 0)) (x (0::nat)) (y' (0::nat)) :]"
       (is "?C = ?D")
    apply (simp add: comp_assoc demonic_demonic)
    apply (subgoal_tac "(((λ(u::nat ⇒ 'a, x::nat ⇒ 'b, y::nat ⇒ 'c) (a::'a, b::'b). a = u (0::nat) ∧ b = x (0::nat)) OO (λ(u::'a, x::'b) (u'::'a, y::'c). r u u' x y)) OO
     (λ(c::'a, d::'c) (u'::nat ⇒ 'a, ab::(nat ⇒ 'b) × (nat ⇒ 'c)). u' (Suc (0::nat)) = c ∧ (case ab of (x'::nat ⇒ 'b, y'::nat ⇒ 'c) ⇒ y' (0::nat) = d)))
           = (λ(u::nat ⇒ 'a, x::nat ⇒ 'b, y::nat ⇒ 'c) (u'::nat ⇒ 'a, x'::nat ⇒ 'b, y'::nat ⇒ 'c). r (u (0::nat)) (u' (Suc (0::nat))) (x (0::nat)) (y' (0::nat)) )")
    apply (simp_all)
    by (simp add: fun_eq_iff OO_def)
  finally have "?A  = ?D" by simp
  from this have "?A ∥ [:u, x, y ↝ u', x', y' . u' 0 = u 0 ∧ x' = x :] = ?D ∥ ({.⊤.} o [:u, x, y ↝ u', x', y' . u' 0 = u 0 ∧ x' = x :])"
    by (simp add: assert_true_skip)
  also have "... = ?R"
    apply (unfold fusion_spec, simp add: inf_fun_def)
    apply (subgoal_tac "(λx::(nat ⇒ 'a) × (nat ⇒ 'b) × (nat ⇒ 'c). case x of (u::nat ⇒ 'a, xa::nat ⇒ 'b, y::nat ⇒ 'c) ⇒ p (u (0::nat)) (xa (0::nat)))
        = (λ(u::nat ⇒ 'a, x::nat ⇒ 'b, y::nat ⇒ 'c). p (u (0::nat)) (x (0::nat)))")
    apply simp
    apply (subgoal_tac "( λ(x::(nat ⇒ 'a) × (nat ⇒ 'b) × (nat ⇒ 'c)) xa::(nat ⇒ 'a) × (nat ⇒ 'b) × (nat ⇒ 'c).
        (case x of (u::nat ⇒ 'a, xa::nat ⇒ 'b, y::nat ⇒ 'c) ⇒ λ(u'::nat ⇒ 'a, x'::nat ⇒ 'b, y'::nat ⇒ 'c). r (u (0::nat)) (u' (Suc (0::nat))) (xa (0::nat)) (y' (0::nat))) xa ∧
        (case x of (u::nat ⇒ 'a, xa::nat ⇒ 'b, y::nat ⇒ 'c) ⇒ λ(u'::nat ⇒ 'a, ab::(nat ⇒ 'b) × (nat ⇒ 'c)). u' (0::nat) = u (0::nat) ∧ (case ab of (x'::nat ⇒ 'b, y'::nat ⇒ 'c) ⇒ x' = xa)) xa)
        = (λ(u::nat ⇒ 'a, x::nat ⇒ 'b, y::nat ⇒ 'c) (u'::nat ⇒ 'a, x'::nat ⇒ 'b, y'::nat ⇒ 'c). r (u (0::nat)) (u' (Suc (0::nat))) (x (0::nat)) (y' (0::nat)) ∧ x = x' ∧ u (0::nat) = u' (0::nat))")
    apply simp
    by (auto simp add: fun_eq_iff)
  finally show "?A ∥ [:u, x, y ↝ u', x', y' . u' 0 = u 0 ∧ x' = x :] = ?R" by simp
  qed

definition "DelayFeedback init S = [:x ↝ u, x',y . init (u (0::nat)) ∧ x = x':]
         o IterateOmegaSkipNextMask (AddUnitDelay S) o  [:u, x, y ↝ y' . y = y':]"
    
lemma SkipNext_refinement: "S ≤ T ⟹ SkipNext S ≤ SkipNext T"
  apply (simp add: SkipNext_def)
  by (simp add: le_fun_def demonic_def Prod_def prod_pred_def, auto)
    
lemma SkipNext_pow_refinement: "S ≤ T ⟹ (SkipNext ^^ n) S ≤ (SkipNext ^^ n) T"
  proof (induction n)
    case 0
    then show ?case by simp
  next
    case (Suc n)
    then show ?case
      apply simp
      by (rule SkipNext_refinement, simp)
  qed
    
lemma Mask_refinement: "S ≤ T ⟹ Mask i S ≤ Mask i T"
  by (simp add: Mask_def le_fun_def)

lemma mono_SkipNext[simp]: "mono (SkipNext S)"
  by (simp add: SkipNext_def)

lemma mono_SkipNext_pow [simp]: "mono S ⟹ mono ((SkipNext ^^ n) S)"
  by (induction n, simp_all)
  
lemma mono_Iterate_SkipNext[simp]: "mono S ⟹ mono (Iterate SkipNext S n)"
  by (induction n, simp_all del: comp_apply)
    
lemma  Iterate_SkipNext_refinement: "⋀ S T . mono S ⟹ S ≤ T ⟹ Iterate SkipNext S n ≤ Iterate SkipNext T n"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have A: "Iterate SkipNext S (Suc n) ≤ Iterate SkipNext T (Suc n)"
    apply simp
    apply (rule mono_comp)
      apply (rule mono_Iterate_SkipNext)
      apply (simp add: Suc.prems(1))
     apply (simp add: Suc.IH Suc.prems(1) Suc.prems(2))
    using SkipNext_pow_refinement Suc.prems(2) by auto
  from this show ?case
    by (simp add: le_fun_def)
qed

    
lemma IterateSkipNextMask_refinemnt: "mono S ⟹ S ≤ T ⟹ IterateSkipNextMask S i ≤ IterateSkipNextMask T i"
  apply (simp add: IterateSkipNextMask_def)
  apply (rule Mask_refinement)
  apply (rule Iterate_SkipNext_refinement)
    by simp_all
  
lemma IterateOmegaSkipNextMask_refinement: "mono S ⟹ S ≤ T ⟹ IterateOmegaSkipNextMask S ≤ IterateOmegaSkipNextMask T"
  apply (simp add: IterateOmegaSkipNextMask_def)
  apply (rule Fusion_refinement)
  by (rule IterateSkipNextMask_refinemnt, simp)
    
lemma AddUnitDelay_refinement: "S ≤ T ⟹ AddUnitDelay S ≤ AddUnitDelay T"
  apply (simp add: AddUnitDelay_def)
  apply (simp add: le_fun_def demonic_def fusion_def, safe)
    apply (rule_tac x = p in exI)
  apply (rule_tac x = p' in exI)
  by auto
    
lemma mono_IterateOmegaSkipNextMask: "mono (IterateOmegaSkipNextMask S)"
  by (simp add: IterateOmegaSkipNextMask_def mono_Fusion)
    
lemma mono_AddUnitDelay: "mono (AddUnitDelay S)"
  by (simp add: AddUnitDelay_def)
    
theorem DelayFeedback_refinement: "init' ≤ init ⟹ S ≤ T ⟹ DelayFeedback init S ≤ DelayFeedback init' T"
  apply (simp add: DelayFeedback_def)
  apply (rule mono_comp)
    apply (rule mono_comp_a, simp_all)
    apply (rule mono_IterateOmegaSkipNextMask)
  apply (rule mono_comp, simp_all)
   apply (rule demonic_refinement)
   apply (simp add: le_fun_def)
  apply (rule IterateOmegaSkipNextMask_refinement)
   apply (simp add: mono_AddUnitDelay)
  apply (rule AddUnitDelay_refinement)
    by simp
    
lemma [simp]: "mono (SkipTop n)"
  by (simp add: SkipTop_def)

lemma [simp]: "SkipNext Skip = Skip"
  apply (simp add: SkipNext_def demonic_demonic)
  by (simp add: fun_eq_iff Skip_def OO_def demonic_def le_fun_def)


lemma Iterate_SkipNextA: "mono S ⟹ S ∘ (SkipNext (Iterate SkipNext S n)) = Iterate SkipNext S (Suc n)"
  apply (induction n, simp)
  apply (simp del: comp_apply)
  apply (simp add: SkipNext_comp del: comp_apply)
  apply (simp add: comp_assoc [THEN sym] del: comp_apply)
  by simp

lemma skiptop_simp: "SkipTop n p = (λ x . ∀ y . eqtop n x y ⟶ p y)"
  by (simp add: SkipTop_def demonic_def fun_eq_iff le_fun_def)

definition "HavocTop n = [:x ↝ y . x[n..] = y[n..]:]"
  
  
lemma HavocTop_Next: "HavocTop (Suc n) = Next (HavocTop n)"
  apply (simp add: HavocTop_def Next_def demonic_demonic)
  apply (subgoal_tac "( λ(x::'a) y. x[Suc n ..] = y[Suc n ..]) = ( ((λx y. y = x[Suc 0 ..]) OO (λx y. x[n ..] = y[n ..])) OO (λy x. y = x[Suc 0 ..])  )")
  apply simp_all
  apply (simp add: fun_eq_iff, safe)
  apply (rule relcomppI, simp_all)
  apply (rule relcomppI, simp_all)
  by auto

lemma [simp]: "HavocTop 0 = Skip"
  by (simp add: HavocTop_def demonic_eq_skip)

lemma "HavocTop n = (Next ^^ n) Skip"
  by (induction n, simp_all add: HavocTop_Next)

lemma Next_NextSkip_aux: "[: λy x. ∀xa. y xa = x (Suc xa) :] (λa. ∀b. a[Suc 0 ..] = b[Suc 0 ..] ⟶ x b) = [: λy x. ∀xa. y xa = x (Suc xa) :] x"
  by (auto simp add: fun_eq_iff demonic_def le_fun_def)
 
lemma demonic_apply_pred: "[: λx y. r x y :] p  = (λx. ∀ y . r x y ⟶ p y)"
  by (simp add: fun_eq_iff demonic_def le_fun_def)

  lemma Next_SkipNext_HavocTop: "mono S ⟹ Next S = SkipNext S o HavocTop (Suc 0)"
    proof (simp add:  SkipNext_Next SkipTop_def Next_def fun_eq_iff fusion_def HavocTop_def demonic_def le_fun_def demonic_apply_pred, safe)
      fix x xa
      assume [simp]: "S (λy. ∀xa. y = xa[Suc 0 ..] ⟶ x xa) (xa[Suc 0 ..])"
      have [simp]: " (λy. ∀xa. y = xa[Suc 0 ..] ⟶ (∀b. b[Suc 0 ..] = xa[Suc 0 ..] ⟶ x b)) = (λy. ∀xa. y = xa[Suc 0 ..] ⟶ x xa)"
        by (auto simp add: fun_eq_iff)
      show " ∃p p'. (∀xa. p xa ∧ p' xa ⟶ (∀y. xa[Suc 0 ..] = y[Suc 0 ..] ⟶ x y)) ∧
                   S (λy. ∀x. y = x[Suc 0 ..] ⟶ p x) (xa[Suc 0 ..]) ∧ (∀y. eqtop (Suc 0) xa y ⟶ p' y)"
        apply (rule_tac x = "(λ a . ∀ b .  b[Suc 0..] = a[Suc 0..] ⟶ x b)" in exI)
        by auto
   next
     fix x::"'a ⇒ bool" fix xa::'a fix p p':: "'a ⇒ bool"
     assume [simp]: "S (λy. ∀x. y = x[Suc 0 ..] ⟶ p x) (xa[Suc 0 ..])"
     assume A: "∀xa. p xa ∧ p' xa ⟶ (∀y. xa[Suc 0 ..] = y[Suc 0 ..] ⟶ x y)"
     assume B: "∀y. eqtop (Suc 0) xa y ⟶ p' y"
     from A and B have C: "⋀ xa . (∀x. xa[Suc 0 ..] = x[Suc 0 ..] ⟶ p x) ⟶ x xa"
      apply safe
      apply (drule_tac x = "cat (Suc 0) xa (xaa[Suc 0..])" in spec)
      by auto 
     assume "mono S"
     from this have "S (λy. ∀x. y = x[Suc 0 ..] ⟶ p x) ≤  S (λy. ∀xa. y = xa[Suc 0 ..] ⟶ x xa)"
       apply (rule monoD, auto)
       by (cut_tac C, auto)
     from this show "S (λy. ∀xa. y = xa[Suc 0 ..] ⟶ x xa) (xa[Suc 0 ..])"
       by (simp add: le_fun_def)
    qed
 
  lemma HavocTop_Next_power: "HavocTop n ∘ Next ((Next ^^ n) S) =  Next ((Next ^^ n) S)"
    proof (induction n)
      case 0
      show ?case by simp
      case (Suc n)
      from this have [simp]: "HavocTop n ∘ Next ((Next ^^ n) S) =  Next ((Next ^^ n) S)" by (simp del: comp_apply)
      have [simp]: "(Next ∘ Next ^^ n) S =  Next ((Next ^^ n) S)" by simp
      show ?case
        by (simp_all add: HavocTop_Next Next_comp [THEN sym] Suc del: comp_apply)
    qed

  lemma Next_SkipNext: "mono S ⟹ (Next ^^ n) S = (SkipNext ^^ n) S ∘ HavocTop n" (is "?Q ⟹ ?A n = ?B n")
    proof (induction n)
      case 0 show ?case by simp
      case (Suc n)
        from this
        have [simp]: "mono S" and [simp]: "?A n = ?B n" by simp_all
        have "(Next ^^ Suc n) S = Next  ((Next ^^ n) S)" by simp
        also have "... = Next  ((SkipNext ^^ n) S ∘ HavocTop n)" by (simp del: comp_apply)
        also have "... = SkipNext ((SkipNext ^^ n) S) ∘ HavocTop (Suc (0::nat)) ∘ Next (HavocTop n)"  by (simp add: Next_comp Next_SkipNext_HavocTop)
        also have "... = ?B (Suc n)"  by (simp add: HavocTop_Next Next_comp [THEN sym] comp_assoc del: comp_apply, simp add: fun_eq_iff)
        finally show ?case by simp
    qed

  lemma Iterate_Next_SkipNext_aux: "mono S ⟹ HavocTop n ∘ (Next ^^ (Suc n)) S = (SkipNext ^^ (Suc n)) S ∘ HavocTop (Suc n)" (is "?P ⟹ ?A = ?B")
    proof -
      assume [simp]: "?P"
      have "?A =  (Next ^^ (Suc n)) S" by (simp add: HavocTop_Next_power)
      also have "... = ?B" by (subst Next_SkipNext, auto)
      finally show ?thesis by simp
    qed

  lemma Iterate_Next_SkipNext_Suc: "mono S ⟹ Iterate Next S (Suc n) = (Iterate SkipNext S (Suc n)) o (HavocTop n)" (is "?P ⟹ ?A n = ?B n")
    proof (induction n)
      case 0 show ?case by simp
      case (Suc n)
      from this have
        [simp]: "HavocTop n ∘ (Next o (Next ^^ n)) S = SkipNext ((SkipNext ^^ n) S) ∘ HavocTop (Suc n)" 
        and [simp]: " Iterate Next S n ∘ (Next ^^ n) S = ?B n" 
          by (cut_tac Iterate_Next_SkipNext_aux, simp, simp_all del: comp_apply)
        show ?case 
          by (simp_all add: comp_assoc del: comp_apply, simp)
   qed

  lemma Iterate_Next_SkipNext: "mono S ⟹ Iterate Next S n = (Iterate SkipNext S n) o (HavocTop (n - 1))"
    by (case_tac n, simp_all, cut_tac Iterate_Next_SkipNext_Suc, simp_all)

  lemma "HavocTop n ≤ Skip"
    by (simp add: HavocTop_def Skip_def le_fun_def demonic_def)

  lemma  mono_Iterate_NextSkip: "mono S ⟹ mono (Iterate SkipNext S n)"
    by (induction n, simp_all)

  lemma "(Havoc X ≠ ⊥) = (X = ⊤)"
    by (simp add: Havoc_def fun_eq_iff demonic_def le_fun_def top_fun_def)

  type_synonym ('a, 'b) rel = "('a ⇒ 'b ⇒ bool)"

  primrec IterateRel :: "(('a, 'a) rel ⇒ ('a, 'a) rel) ⇒ ('a, 'a) rel ⇒ nat ⇒ ('a, 'a) rel" where
    "IterateRel F r 0 = (λ a b . a = b)" |
    "IterateRel F r (Suc n) = IterateRel F r n OO ((F ^^ n) r)"

lemma IterateRel_init: "(∀ r r' . F (r OO r') = F r OO F r') ⟹ F (=) = (=) ⟹ IterateRel F r (Suc n) = r OO F (IterateRel F r n)"  (is "?P ⟹ ?Q ⟹ ?R n")
proof (induction n)
  case 0 from this show ?case by (simp add: eq_OO OO_eq) 
  case (Suc n)
    assume [simp]: "?P"
    assume [simp]: "?Q"
    assume "?P ⟹ ?Q ⟹ ?R n"
    from this have A: "?R n" by simp
    have "IterateRel F r (Suc (Suc n)) = IterateRel F r (Suc n) OO (F ^^ (Suc n)) r"
      by simp
    also have "... = r OO F (IterateRel F r (Suc n))"
      by (subst A , simp add: relcompp_assoc)
    finally show "?R (Suc n)" by simp
qed

lemma [simp]: "idnext (=) = (=)"
  apply (simp add: idnext_def fun_eq_iff next_def at_fun_def, safe, simp_all)
  by (drule eqtop_tail, simp_all)

lemma [simp]: "idnext (r OO r') = (idnext r) OO idnext r'"
  apply (auto simp add: idnext_def fun_eq_iff next_def at_fun_def OO_def)
  apply (rule_tac x = "cat (Suc 0) x y" in exI, simp)
  by (rule_tac b = y in eqtop_tran, simp)

lemma IterateRel_idnext_init: "IterateRel idnext r (Suc n) = r OO idnext (IterateRel idnext r n)"
  by (rule IterateRel_init, simp_all)

lemma [simp]: "(⋀ (p::'a⇒bool) (r::'a⇒'b⇒bool) . F ({.p.} o [:r:]) = {.A p.} o [:(B::('a⇒'b⇒bool) ⇒ ('a⇒'b⇒bool)) r:]) 
  ⟹ ((F ^^ n) ({.p.} o [:r:])) = {.(A^^n) p.} o [:(B^^n) r:]"
  by (induction n, auto)

lemma Iterate_id: "Iterate id S n = S ^^ n"
  apply (induction n, simp_all)
  by (metis comp_id fun.map_ident id_funpow funpow_swap1)

lemma IterateRel_id: "IterateRel id r n = (r ^^ n)"
  apply (induction n)
  apply (simp_all)
  by (metis comp_id fun.map_ident id_funpow)

lemma Iterate_IterateRel: "(⋀ p r . F ({.p.} o [:r:]) = {.A p.} o [:B r:]) ⟹ Iterate F ({.p.} o [:r:]) n 
    = {.x . (∀ i < n .(∀ y . IterateRel B r i x y ⟶ (A^^i) p y)).} o [:IterateRel B r n:]"
  proof (induction n)
   case 0
    show ?case by (simp add: demonic_eq_skip assert_true_skip_a)
  next
    case (Suc n)
      assume [simp]: "⋀p r. F ({. p .} ∘ [: r :]) = {. A p .} ∘ [: B r :]"
      assume "((⋀p r. F ({. p .} ∘ [: r :]) = {. A p .} ∘ [: B r :]) ⟹
        Iterate F ({. p .} ∘ [: r :]) n = {.x. ∀i<n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} ∘ [: IterateRel B r n :])"
      from this have [simp]: "Iterate F ({. p .} ∘ [: r :]) n = {.x. ∀i<n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} ∘ [: IterateRel B r n :]"
        by simp
      have [simp]: " (λx. ∀i<n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y) ⊓ (λx. ∀y. IterateRel B r n x y ⟶ (A ^^ n) p y)
            =  (λx. ∀i < Suc n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y)"
         by (simp add: fun_eq_iff, auto, case_tac "i = n", auto)
      have "Iterate F ({. p .} ∘ [: r :]) (Suc n) = {.x. ∀i<n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} ∘ [: IterateRel B r n :] o ({. (A ^^ n) p .} ∘ [: (B ^^ n)r :])"
        by simp
      also have "... = {.x. ∀i<n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} ∘ ([: IterateRel B r n :] o {. (A ^^ n) p .}) ∘ [: (B ^^ n)r :]"
        by (simp add: comp_assoc)
      also have "... = {.x. ∀i<n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} o {.x. ∀y. IterateRel B r n x y ⟶ (A ^^ n) p y.} o [: IterateRel B r n :] ∘ [: (B ^^ n)r :]"
        by (simp add: demonic_assert_comp, simp add: comp_assoc)
      also have "... = {.x. ∀i < Suc n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} o [: IterateRel B r n :] ∘ [: (B ^^ n)r :]"
        by (simp add: assert_assert_comp)
      also have "... =  {.x. ∀i < Suc n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} o [: IterateRel B r n OO (B ^^ n)r :]"
        by (simp add: comp_assoc demonic_demonic)
      also have "... =  {.x. ∀i < Suc n. ∀y. IterateRel B r i x y ⟶ (A ^^ i) p y.} o [: IterateRel B r (Suc n) :]"
        by simp
      finally show ?case by (simp del: comp_apply)
     qed

lemma IterateRel_app: "⋀ y . IterateRel next r n x y = (∃ a . a 0 = x ∧ a n = y ∧ (∀ i < n. r ((a i)[i..]) ((a (Suc i))[i..])))"
  apply (induction n)
  apply (simp)
  apply safe [1]
  apply (rule_tac x = "λ n . x" in exI, simp)
  apply simp
  apply safe
  apply simp
  apply safe
  apply (simp add: iterate_next at_fun_def)
  apply (rule_tac x = "λ i . if i ≤ n then a i else y" in exI)
  apply simp
  apply auto [1]
  apply (case_tac "i = n", simp_all)
  apply (rule relcomppI)
  apply simp_all
  apply (rule_tac x = a in exI, simp_all)
    by (simp add: iterate_next at_fun_def)

lemma Iterate_Next_IterateRel: "Iterate Next ({.p.} o [:r:]) n 
  = {. x . (∀ k < n . (∀ y . IterateRel next r k x y ⟶ (next ^^ k) p y) ).} o [:IterateRel next r n:]"
  apply (rule Iterate_IterateRel)
  by (simp add: Next_assert_demonic)

lemma IterateOmegaNextMask_spec_aux: "IterateOmegaNextMask ({.p.} o [:r:]) 
  = {. INF x. (λxa. ∀k<x. ∀y. IterateRel next r k xa y ⟶ (next ^^ k) p y) .} ∘ [: INF n. IterateRel next r n OO eqtop n :]"
  apply (simp add: IterateOmegaNextMask_def IterateNextMask_simp Mask_def Iterate_Next_IterateRel SkipTop_def comp_assoc demonic_demonic)
  by (simp add: Fusion_spec)

lemma IterateOmegaNextMask_spec: "IterateOmegaNextMask ({.p.} o [:r:]) 
        =  {. INF k . (λxa. ∀y. IterateRel next r k xa y ⟶ (next ^^ k) p y) .} ∘ [: INF n. IterateRel next r n OO eqtop n :]"
  apply (simp add: IterateOmegaNextMask_spec_aux)
  apply (subgoal_tac "(INF x. (λxa. ∀k<x. ∀y. IterateRel next r k xa y ⟶ (next ^^ k) p y)) = (INF k. (λxa. ∀y. IterateRel next r k xa y ⟶ (next ^^ k) p y))")
  by auto

lemma power_spec: "({.p.} o [:r:]) ^^ n 
    = {.x . (∀ i < n .(∀ y . (r ^^ i) x y ⟶ p y)).} o [:r ^^ n:]"
  apply (cut_tac A = id and B = id and F = id in Iterate_IterateRel)
  apply simp
  by (simp add: Iterate_id IterateRel_id)


lemma Iterate_SkipNext_IterateSkipRel: "Iterate SkipNext ({.p.} o [:r:]) n 
      = {. x . (∀ k < n . (∀ y . IterateRel idnext r k x y ⟶ (next ^^ k) p y) ).} o [:IterateRel idnext r n:]"
  apply (rule Iterate_IterateRel)
  by (simp add: SkipNext_assert_demonic)

lemma IterateOmegaSkipNextMask_spec: "IterateOmegaSkipNextMask ({.p.} o [:r:]) 
  =  {. (λx . ∀ n . ∀y. IterateRel idnext r n x y ⟶ (next ^^ n) p y) .} 
     ∘ [: INF n. IterateRel idnext r n OO eqtop n :]"
  apply (simp add: IterateOmegaSkipNextMask_def IterateSkipNextMask_simp Mask_def 
      Iterate_SkipNext_IterateSkipRel SkipTop_def comp_assoc demonic_demonic)
  apply (simp add: Fusion_spec)
  apply (subgoal_tac "(INF x. (λxa. ∀k<x. ∀y. IterateRel idnext r k xa y ⟶ (next ^^ k) p y)) 
         = (λx . ∀n y. IterateRel idnext r n x y ⟶ (next ^^ n) p y)")
  by auto

  

lemma IterateOmegaSkipNextMask_demonic: "IterateOmegaSkipNextMask [:r:] =  [: INF n. IterateRel idnext r n OO eqtop n :]"
  by (cut_tac p = ⊤ and r = r in IterateOmegaSkipNextMask_spec, simp add: assert_true_skip assert_true_skip_a)

lemma [simp]: "(next ^^ n) ⊤ x"
  by (simp add: iterate_next)

lemma power_idnext: "(idnext ^^ n) r = ((next ^^ n) r ⊓ eqtop n)"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case
    apply (simp add: fun_eq_iff idnext_def next_def at_fun_def, safe)
    apply (cut_tac n = "Suc 0" and m = n and x = x and y = xa in  eqtop_plus, simp_all)
     apply (cut_tac n = "Suc 0" and m = n and x = x and y = xa in  eqtop_plus, simp_all)
    by (cut_tac n = "Suc 0" and m = n and x = x and y = xa in  eqtop_plus, simp_all)
qed

lemma example_feedback_delay_a: " ∀xb. ∃z. IterateRel idnext (λx y. ∀xa. y xa = ([0] .. x) xa) xb x z ∧ (∀i<xb. z i = xa i) ⟹ xa n = 0"
    apply (induction n)
    apply (drule_tac x = 1 in spec)
    apply auto [1]
    apply (drule_tac x = "Suc (Suc n)" in spec)
    apply simp
    apply auto
    apply (simp add: idnext_def next_def at_fun_def append_inf_def power_idnext iterate_next)
    apply auto
    apply (drule_tac x = "Suc n" in spec, simp)
    by (drule_tac x = "0" in spec, simp)

lemma example_feedback_delay_b: "∀x. xa x = 0 ⟹ ∃z. IterateRel idnext (λx y. ∀xa. y xa = ([0] .. x) xa) n x z ∧ (∀i < n. z i = xa i)"
  apply (induction n)
  apply auto [1]
  apply simp
  apply safe
  apply (rule_tac x = "[0] .. z" in exI, safe)
  apply (simp add: OO_def)
  apply (rule_tac x= z in exI, simp_all)
  apply (simp add: idnext_def next_def at_fun_def append_inf_def power_idnext iterate_next)
  by (simp add: append_inf_def)

lemma example_feedback_delay: "IterateOmegaSkipNextMask [:x ↝ y . y = [0::nat] .. x:] = [:x↝ y . y = (λ i . 0):]"
  apply (cut_tac p = ⊤ and r = "λ x  y . y = [0::nat] .. x" in IterateOmegaSkipNextMask_spec, (simp add: assert_true_skip_a))
  apply (subgoal_tac "( INF x::nat. IterateRel idnext (λ(x::nat ⇒ nat) y::nat ⇒ nat. y = [0::nat] .. x) x OO eqtop x) 
          = (λ(x::nat ⇒ nat) y::nat ⇒ nat. y = (λi::nat. 0::nat))", simp_all)
  apply (simp_all add: fun_eq_iff OO_def assert_true_skip, safe)
  apply (drule example_feedback_delay_a, simp)
  apply (rule example_feedback_delay_b)
  by simp

lemma next_simp: "next (r::(nat ⇒ 'a) ⇒(nat ⇒ 'b) ⇒bool) x y = r (x[Suc 0..]) (y[Suc 0..])"
  by (simp add: fun_eq_iff next_def at_fun_def)

lemma idnext_simp: "idnext (r::(nat ⇒ 'a) ⇒(nat ⇒ 'a) ⇒bool) x y = (r (x[Suc 0..]) (y[Suc 0..]) ∧ x 0 = y 0)"
  by (simp add: idnext_def fun_eq_iff next_def at_fun_def)

lemma idnext_next_eqtop: "⋀ (x::nat⇒'a) y . (idnext ^^ n) r x y = ((next ^^ n) r x y ∧ eqtop n x y)"
  apply (induction n)
  apply simp
  apply simp
  apply (subst next_simp)
  apply (subst idnext_simp)
  apply safe
  apply metis
  apply (metis AbsNat_nat_def add_Suc at_trace_def id_apply less_Suc_eq_0_disj monoid_add_class.add.left_neutral)
  apply auto [1]
  by auto

lemma IrerateRel_IterateSkipRel_aux: "∀ x y . IterateRel next (r::(nat ⇒ 'a) ⇒(nat ⇒ 'a) ⇒bool) n x y ⟶ (∃ z . y[(n::nat)..] = z[n..] ∧ IterateRel idnext r n x z)"
  apply (induction n)
  apply simp
  apply simp
  apply (simp add: OO_def idnext_next_eqtop, safe)
  apply (drule_tac x = x in spec)
  apply (drule_tac x = ya in spec)
  apply simp
  apply safe
  apply (rule_tac x = "λi . (if i < n then z i else y i)" in exI, simp)
  apply (rule_tac x = z in exI, simp)
  apply (simp add: iterate_next at_fun_def)
  apply (subgoal_tac "(ya[n ..]) = (z[n ..])", simp)
  apply (subgoal_tac "(y[n ..]) = ((λi. if i < n then z i else y i)[n ..])")
  apply simp_all
  by (simp add: fun_eq_iff)

lemma IrerateRel_IterateSkipRel: "IterateRel next (r::(nat ⇒ 'a) ⇒(nat ⇒ 'a) ⇒bool) n x y ⟹ (∃ z . y[(n::nat)..] = z[n..] ∧ IterateRel idnext r n x z)"
  by (cut_tac IrerateRel_IterateSkipRel_aux, auto)

(*
definition "prec_loc_st p r = -((lft_pred_st (inpt_st r)) until -(lft_pred_loc_st p))"
  

lemma prec_loc_st_simp: "prec_loc_st p r u x = (∀ n . (∀ i < n . inpt_st r (u i) (u (Suc i)) (x i)) ⟶ p (u n) (x n))"
  by (simp add: prec_loc_st_def until_def lft_pred_st_def inpt_st_def at_fun_def lft_pred_loc_st_def, metis)
    
*)

lemma next_eq: "∀i<k. (∀x. fst (snd (ab i)) (i + x) = fst (snd (ab (Suc i))) (i + x)) ⟹
     i ≤ k ⟹  (∀ j . fst (snd (ab i)) (i + j) =  fst (snd (ab 0)) (i + j))"
  apply (induction i)
  apply simp_all
  apply safe
  by (metis add_Suc_right)

(*
  definition "SymbolicSystem init p r = {.x . ∀ u . init (u 0) ⟶ prec_loc_st p r u x.} o [:x ↝ y . ∃ u . init (u 0) ∧ (□ (lft_rel_st r)) u x y:]"
*)
  lemma IterateSkipRel_SymRel_zero: "⋀ u' x' y' . (IterateRel idnext (λ(u, x, y) (u', x', y'). r (u 0) (u' (Suc 0)) (x 0) (y' 0) ∧ (x = x') ∧ (u 0 = u' 0)) 0) (u, x, y) (u', x', y') 
    = (u = u' ∧ x = x' ∧ y = y')"
    by auto

  lemma IterateSkipRel_SymRel_Suc: "⋀ u' x' y' . (IterateRel idnext (λ(u, x, y) (u', x', y'). r (u 0) (u' (Suc 0)) (x 0) (y' 0) ∧ (x = x') ∧ (u 0 = u' 0)) (Suc n)) (u, x, y) (u', x', y') 
    = ((u' 0 = u 0) ∧ (∀ i < (Suc n) . r (u' i) (u' (Suc i)) (x i) (y' i)) ∧ x = x')"
    apply (induction n)
    apply auto [1]
    apply (simp add: idnext_def next_def at_fun_def append_inf_def power_idnext iterate_next OO_def eqtop_prod_def at_prod_def)
    apply safe
    apply auto [1]
    apply (case_tac "i < Suc n", simp_all)
    apply (drule_tac x = i in spec, simp)
    apply (subgoal_tac "a i = u' i ∧ a (Suc i) = u' (Suc i) ∧ b i = y' i", simp_all)
    apply (case_tac i, simp_all)
    apply auto [1]
    apply auto [1]
    apply (case_tac "Suc nat < n")
    apply auto [1]
    apply (case_tac "Suc nat = n")
    apply auto [1]
    apply auto [1]
    apply (case_tac "i = Suc n")
    apply auto [1]
    apply auto [1]
    apply (simp add: fun_eq_iff at_fun_def, safe)
    apply (case_tac xa, simp_all)
    apply (case_tac "nat < n", simp_all)
    apply (metis le_add_diff_inverse not_less)
    apply (rule_tac x = u' in exI, simp_all)
    by (rule_tac x = y' in exI, simp_all)

  lemma IterateSkipRel_SymRel: "⋀ u' x' y' . (IterateRel idnext (λ(u, x, y) (u', x', y'). r (u 0) (u' (Suc 0)) (x 0) (y' 0) ∧ (x = x') ∧ (u 0 = u' 0)) n) (u, x, y) (u', x', y') 
    = ((u' 0 = u 0) ∧ (∀ i <  n . r (u' i) (u' (Suc i)) (x i) (y' i)) ∧ x = x' ∧ (n = 0 ⟶ (u = u' ∧ y = y')))"
    apply (case_tac n)
    apply (cut_tac IterateSkipRel_SymRel_zero)
    apply auto [1]
    apply (cut_tac IterateSkipRel_SymRel_Suc)
    by auto

  lemma IterateSkipRel_SymRel_eqtop: "(IterateRel idnext (λ(u, x, y) (u', x', y'). r (u (0::nat)) (u' (Suc 0)) (x (0::nat)) (y' (0::nat)) ∧ (x = x') ∧ (u 0 = u' 0)) n OO (eqtop n)) (u, x, y) (u', x', y') 
    = (∃ v .  (v 0 = u 0 ) ∧ (∀ i < n . r (v i) (v (Suc i)) (x i) (y' i) ∧ v i = u' i ∧ (x i = x' i)))"
    apply (case_tac n)
    apply auto [1]
    apply (unfold OO_def)
    apply safe
    apply (unfold IterateSkipRel_SymRel)
    apply (rule_tac x = a in exI, simp)
    apply (simp add: eqtop_prod_def at_prod_def)
    apply auto [1]
    apply (rule_tac x = "(v, x, y')" in exI)
    apply (unfold IterateSkipRel_SymRel)
    apply (simp add: eqtop_prod_def at_prod_def)
    by auto [1]


  lemma INF_IterateSkipRel_SymRel_eqtop: "(INF n. IterateRel idnext (λ(u, x, y) (u', x', y'). r (u (0::nat)) (u' (Suc 0)) (x (0::nat)) (y' (0::nat)) ∧ x = x' ∧ u 0 = u' 0) n OO eqtop n) (u, x, y) (u', x', y')
       = (u' 0 = u 0 ∧ x = x' ∧ (□ (λ (u, x, y) . r (u 0) (u (Suc 0)) (x 0) (y 0))) (u', x, y'))"
    apply (simp add: Inf_fun_def IterateSkipRel_SymRel_eqtop) 
    apply safe
    apply (metis zero_less_Suc)
    apply (metis ext lessI)
    apply (simp add: always_def at_fun_def at_prod_def)
    apply (metis Suc_lessD lessI)
    apply (simp add: always_def at_fun_def at_prod_def)
    by (rule_tac x = "u'" in exI, simp)

  lemma INF_IterateSkipRel_SymRel_eqtop_abs: "(INF n. IterateRel idnext (λ(u, x, y) (u', x', y'). r (u (0::nat)) (u' (Suc 0)) (x (0::nat)) (y' (0::nat)) ∧ x = x' ∧ u 0 = u' 0) n OO eqtop n)
       = (λ (u, x, y) (u', x', y') . (u' 0 = u 0 ∧ x = x' ∧ (□ (λ (u, x, y) . r (u 0) (u (Suc 0)) (x 0) (y 0))) (u', x, y')))"
    
    apply (subst (2) fun_eq_iff)
    apply (subst (2) fun_eq_iff)
    apply (rule allI)
    apply (rule allI)
    apply (case_tac x)
    apply (case_tac xa)
    by (cut_tac INF_IterateSkipRel_SymRel_eqtop, auto)

  lemma move_down: "p ⟹ p"
    by simp

  lemma IterateSkipRel_prec_loc_st: "(λx. ∀a. init (a 0) ⟶
                (∀b n aa aaa ba.
                    IterateRel idnext (λ(u, x, y) (u', x', y'). r (u (0::nat)) (u' (Suc 0)) (x (0::nat)) (y' (0::nat)) ∧ x = x' ∧ u 0 = u' 0) n (a, x, b) (aa, aaa, ba) ⟶
                    (next ^^ n) (λ(u, x, y). p (u 0) (x 0)) (aa, aaa, ba)))
         = prec_pre_sts init (λ (u, x) . p u x) (λ (u,x) (u', y) . r u u' x y)"
  apply (simp add: prec_pre_sts_simp iterate_next at_fun_def at_prod_def IterateSkipRel_SymRel)
  apply (simp add: fun_eq_iff)
    apply (safe)
      apply (unfold prec_pre_sts_simp, safe)
  apply (drule_tac x = "u" in spec, simp)
  apply (drule move_down)
  apply (drule move_down)
  apply (drule_tac x = "y" in spec)
  apply (drule move_down)
  apply (drule move_down)
  apply (drule_tac x = n in spec)
  apply (drule_tac x = u in spec)
  apply (drule_tac x = x in spec)
  apply safe
  apply (case_tac n, simp)
  apply auto [1]
  apply simp
  apply (rule_tac x = "λ i . SOME y . r (u i) (u (Suc i)) (x i) y" in exI)
  apply safe [1]
  apply (drule_tac x = i in spec, simp)
  apply (metis someI)
  apply (drule_tac x = aa in spec)
  apply metis
  by metis

    
theorem DelayFeedback_SymbolicSystem_aux: "DelayFeedback init ({.(x, y).p x y.} ∘ [:(u, x)↝(u', y).r u u' x y:])  
      = LocalSystem init (λ (u, x) . p u x) (λ (u,x) (u', y) . r u u' x y)"
    apply (unfold  AddUnitDelay_spec DelayFeedback_def)
    apply (simp add: IterateOmegaSkipNextMask_spec comp_assoc [THEN sym] INF_IterateSkipRel_SymRel_eqtop_abs)
    apply (simp add: demonic_assert_comp)
    apply (simp add: comp_assoc demonic_demonic)
  apply (simp add: LocalSystem_simp IterateSkipRel_prec_loc_st)
    apply (rule prec_rel_eq, simp)
  apply (simp add: fun_eq_iff always_def rel_pre_sts_simp at_fun_def at_prod_def OO_def)
  apply safe
   apply (rule_tac x = a in exI)
   apply auto [1]
   by (rule_tac x = u in exI, auto)

(*it was DelayFeedback_SymbolicSystem*)
theorem DelayFeedback_LocalSystem: "DelayFeedback init ({.p.} ∘ [:r:])  
      = LocalSystem init p r"
  apply (cut_tac p = "λ u x . p (u, x)" and r = "λ u u' x y . r (u,x) (u',y)" in DelayFeedback_SymbolicSystem_aux)
  by simp
    

lemma DelayFeedback_simp: "DelayFeedback init ({.p.} o [:r:]) = {.prec_pre_sts init p r.} o [:rel_pre_sts init r:]"
  by(simp add: DelayFeedback_LocalSystem LocalSystem_simp)

lemma prec_pre_sts_prec_rel: "(⋀ s s' x y . p (s, x) ⟹ r (s, x) (s', y) = r' (s, x) (s', y)) ⟹ prec_pre_sts init p r = prec_pre_sts init p r'"
proof -
  assume [simp]: "⋀ s s' x y . p (s, x) ⟹ r (s, x) (s', y) = r' (s, x) (s', y)"
  have "{.p.} o [:r:] = {.p.} o [:r':]"
    by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, auto)
  from this have "prec (DelayFeedback init ({.p.} o [:r:])) = prec (DelayFeedback init ({.p.} o [:r':]))"
    by simp
  from this show "prec_pre_sts init p r = prec_pre_sts init p r'"
    by (simp add: DelayFeedback_simp)
qed


theorem DelayFeedback_a_simp: "DelayFeedback init ({.p.} o [:r:]) =
     {.x .(∀ u y . init (u 0) ⟶ (∀n . (∀ i < n . r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))).} 
      o [:x ↝ y . (∃ u . init (u 0) ∧ (∀ i . r (u i, x i) (u (Suc i), y i))):]"
proof (simp add: DelayFeedback_simp)
  have [simp]: "prec_pre_sts init p r =
      (λ x . ∀ u y . init (u 0) ⟶ (∀n . (∀ i < n . r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n)))"
    by (simp add: fun_eq_iff prec_pre_sts_simp)
  have [simp]: "rel_pre_sts init r = (λ x y . ∃u. init (u 0) ∧ (∀i. r (u i, x i) (u (Suc i), y i)))"
    by (simp add: fun_eq_iff rel_pre_sts_simp)
  show " {. prec_pre_sts init p r .} ∘ [: rel_pre_sts init r :] =
    {.x.∀u. init (u 0) ⟶ (∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n)).} 
      ∘ [:x↝y.∃u. init (u 0) ∧ (∀i. r (u i, x i) (u (Suc i), y i)):]"
    by simp
qed
    
theorem DelayFeedback_b_simp: "DelayFeedback init ([:r:]) 
      = [:rel_pre_sts init r:]"
  apply (cut_tac init = init and p = "⊤" and r = "r" in  DelayFeedback_simp)
  by (simp add: always_def until_def at_fun_def  assert_true_skip_a assert_true_skip)


lemma DelayFeedback_comp: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init' b ⟹ 
     DelayFeedback init ({.p.} o [:r:]) o DelayFeedback init' ({.p'.} o [:r':]) =
        DelayFeedback (prod_pred init init') ({.prec_comp_sts p r p'.} o [:rel_comp_sts r r':])"
  by (simp add: DelayFeedback_LocalSystem sts_comp)
    

lemma DelayFeedback_empty_init[simp]: "DelayFeedback ⊥ S' = ⊤"
  by (simp add: DelayFeedback_def fun_eq_iff demonic_def le_fun_def)


lemma assert_bot: "{.⊥.} = Fail"
  by (simp add: fun_eq_iff Fail_def assert_def)
    
lemma Fail_comp: "Fail o S = Fail"
  by (simp add: fun_eq_iff Fail_def assert_def)


lemma DelayFeedback_Fail[simp]: "init a ⟹ DelayFeedback init (Fail:: ('a × 'b ⇒ bool) ⇒ ('a × 'c ⇒ bool)) = Fail"
  proof -
    assume A[simp]: "init a"
    have "DelayFeedback init (Fail:: ('a × 'b ⇒ bool) ⇒ ('a × 'c ⇒ bool)) = DelayFeedback init ({.⊥.} o [:⊤:])"
      by (simp add: assert_bot Fail_comp)
    also have "... = {. prec_pre_sts init (⊥::('a × 'c ⇒ bool)) (⊤::('a × 'c ⇒ 'a × 'b ⇒ bool)) .} ∘ [: rel_pre_sts init (⊤::('a × 'c ⇒ 'a × 'b ⇒ bool)) :]"
      by (simp add: DelayFeedback_simp)
    also have "... = Fail"
      thm prec_pre_sts_bot
      using A apply (unfold prec_pre_sts_bot)
      by (simp add: assert_bot Fail_comp)
    finally show ?thesis by simp
  qed
 
lemma prod_empty [simp]: "prod_pred X ⊥ = ⊥"
  by (simp add: fun_eq_iff prod_pred_def)

lemma sts_serial_comp_empty_init: "DelayFeedback (prod_pred ⊤ ⊥) (sts_comp Fail S') ≠ DelayFeedback ⊤ Fail o DelayFeedback ⊥ S'"
  apply (simp add: Fail_comp)
  by (simp add: fun_eq_iff Fail_def)

thm DelayFeedback_LocalSystem
  
theorem sts_serial_comp: "implementable S ⟹ implementable S' ⟹ init' b ⟹ 
  DelayFeedback (prod_pred init init') (sts_comp S S') = DelayFeedback init S o DelayFeedback init' S'"
  apply (drule implementable_spec, safe)
  apply (drule implementable_spec, safe)
  by (simp add: DelayFeedback_LocalSystem sts_comp_prec_rel sts_comp)

theorem implementableI: "p ≤ inpt r ⟹ implementable ({.p.} o [:r:])"
  by (simp add: implementable_def non_magic_def fun_eq_iff le_fun_def inpt_def demonic_def assert_def)

lemma implementable_inpt[simp]: "implementable ({.inpt r.} o [:r:])"
  by (simp add: implementableI)

theorem implementable_DelayFeedback: "implementable S ⟹ init a ⟹ implementable (DelayFeedback init S)"
  apply (drule implementable_spec, safe)
  apply (simp add: DelayFeedback_LocalSystem LocalSystem_simp)
  apply (rule implementableI, safe)
  apply (subst inpt_def)
  apply (rule_tac x = "yy r a x" in exI)
    apply (simp add: rel_pre_sts_simp)
  apply (rule_tac x = "uu r a x" in exI)
  apply safe
   apply (simp add: uu_def)
  by (rule_tac p = p  and init = init in sts_exists, simp_all)

theorem LocalSystem_impt_implementable: "init a ⟹ implementable (LocalSystem init (inpt r) r)"
  apply (simp add:  DelayFeedback_LocalSystem [symmetric])
  by (rule implementable_DelayFeedback, simp_all)
    
lemma prec_pre_sts_inpt: "init a ⟹ prec_pre_sts init (inpt r) r ≤ inpt (rel_pre_sts init r)"
  apply (cut_tac r = r and init = init in LocalSystem_impt_implementable, simp_all)
  apply (simp add: LocalSystem_simp)
  apply (unfold implementable_def, safe)
  by (unfold non_magic_spec, simp add: le_fun_def)

lemma comp_middle: "A o B o C o D = A o (B o C) o D"
  by (simp add: comp_assoc)

lemma fun_eq: "(∀x. f x = g x) = (f = g)"
  by auto

lemma [simp]: "SkipNext ⊥ = ⊥"
  by (simp add: fun_eq_iff SkipNext_simp)

lemma "SkipNext ⊥ = ⊥"
  by (simp add: SkipNext_simp le_fun_def fun_eq_iff Prod_def Skip_def demonic_def prod_pred_def)

lemma "SkipNext ⊤ ⊥ = ⊤"
  by (auto simp add: SkipNext_simp le_fun_def fun_eq_iff Prod_def Skip_def demonic_def prod_pred_def)

lemma "SkipNext ⊤ = ⊤"
  by (auto simp add: SkipNext_simp le_fun_def fun_eq_iff Prod_def Skip_def demonic_def prod_pred_def)

subsection‹Examples›
  

  definition "PREC_ID = ⊤"
  definition "REL_ID = (λ (u,x) (u', y) .(u = u') ∧ (u = y))"
  definition "INIT_ID u = (u = 0)"

lemma all_eq: "∀x. u x = u (Suc x) ⟹ u x = u 0"
  apply (induction x)
  by auto

lemma "LocalSystem INIT_ID PREC_ID REL_ID = [:x ↝ y . ∀ i . y i = 0:]"
  apply (simp add:  LocalSystem_simp PREC_ID_def assert_true_skip)
  apply (rule_tac f = "demonic" in arg_cong)
  apply (simp add: rel_pre_sts_simp INIT_ID_def REL_ID_def fun_eq_iff, safe, simp_all)
   apply (cut_tac  u = u and x = i in all_eq, simp_all, metis)
    by auto
  
  definition "PREC_COUNTER = ⊤"
  definition "REL_COUNTER = (λ (u, x) (u', y) . (u' = u + 1) ∧ (u = y))"
  definition "INIT_COUNTER u = (u = 0)"

  lemma add_suc: "∀x. u (Suc x) = Suc (u x) ⟹ u x = x + u 0"
    apply (induction x)
    by auto

  lemma "LocalSystem INIT_COUNTER PREC_COUNTER REL_COUNTER = [:x ↝ y . ∀ i . y i = i:]"
  apply (simp add:  LocalSystem_simp PREC_COUNTER_def assert_true_skip)
  apply (rule_tac f = "demonic" in arg_cong)
  apply (simp add: rel_pre_sts_simp INIT_COUNTER_def REL_COUNTER_def fun_eq_iff, safe, simp_all)
   apply (cut_tac  u = u and x = i in add_suc, simp_all, metis)
    by auto
    
definition "PREC_SUM = ⊤"
definition "REL_SUM = (λ (u, x) (u', y) . (u' = u + x) ∧ (u = y))"
definition "INIT_SUM u = (u = 0)"

primrec Summ :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
  "Summ x 0 = 0" |
  "Summ x (Suc n) = Summ x n + x n"

lemma sum_suc: "∀n. u (Suc n) = u n + x n ⟹ u n = Summ x n + u 0"
  apply (induction n)
  by auto
  
lemma "LocalSystem INIT_SUM PREC_SUM REL_SUM = [:x ↝ y . y = Summ x:]"
  apply (simp add:  LocalSystem_simp PREC_SUM_def assert_true_skip)
  apply (rule_tac f = "demonic" in arg_cong)
  apply (simp add: rel_pre_sts_simp INIT_SUM_def REL_SUM_def fun_eq_iff, safe, simp_all)
     apply (cut_tac  u = xa and n = xb in sum_suc, simp_all, metis)
    by (rule_tac x = xa in exI, simp)

definition "PREC_A = ⊤"
definition "REL_A = (λ (u, x) (u', y) . (u' = x) ∧ (u = y))"
definition "INIT_A u = (u = 0)"

lemma "LocalSystem INIT_A PREC_A REL_A = [:x ↝ y . y = [0] .. x:]"
  apply (simp add:  LocalSystem_simp PREC_A_def assert_true_skip)
  apply (rule_tac f = "demonic" in arg_cong)
  apply (simp add: rel_pre_sts_simp INIT_A_def REL_A_def fun_eq_iff append_inf_def, safe)
    apply metis
    apply (metis Suc_pred)
    by (metis diff_Suc_Suc diff_zero zero_less_Suc)

definition "PREC_SUM_A = (λ (u, x) . u ≤ 100)"
definition "REL_SUM_A = (λ (u, x) (u', y) . (u' = u + x) ∧ (u = y))"
definition "INIT_SUM_A u = (u = 0)"
  
lemma sum_suc_le: "∀n < k . u (Suc n) = u n + x n ⟹ u k = Summ x k + u 0"
  apply (induction k)
  by auto

lemma "LocalSystem INIT_SUM_A PREC_SUM_A REL_SUM_A = {.x . ∀ i . Summ x i ≤ 100.} o [:x ↝ y . y = Summ x:]"
  apply (simp add:  LocalSystem_simp PREC_SUM_def assert_true_skip)
  apply (rule prec_rel_eq)
   apply (simp add: fun_eq_iff prec_pre_sts_simp INIT_SUM_A_def REL_SUM_A_def PREC_SUM_A_def, safe)
    apply (drule_tac x = "Summ x" in spec, simp_all, blast)
   apply (cut_tac  u = u and k = n and x = x in sum_suc_le, simp_all)

  apply (simp add: rel_pre_sts_simp INIT_SUM_A_def REL_SUM_A_def fun_eq_iff, safe, simp_all)
     apply (cut_tac  u = xa and n = xb in sum_suc, simp_all, metis)
    by (rule_tac x = xa in exI, simp)


  definition "PREC_SUM_B = (λ (u, x) . u ≤ 100)"
  definition "REL_SUM_B = (λ (u, x) (u', y) . (u' = u + x ∨ u' = x) ∧ (u = y))"
  definition "INIT_SUM_B u = (u = 0)"

lemma le_sum_suc: "∀n < k . u (Suc n) = u n + x n ∨ u (Suc n) = x n ⟹ u k ≤ Summ x k + u 0"
  apply (induction k)
  by auto

lemma "LocalSystem INIT_SUM_B PREC_SUM_B REL_SUM_B 
      = {.x . ∀ i . Summ x i ≤ 100.} o [:x ↝ y . y 0 = 0 ∧ (∀ i . y (Suc i) = y i + x i ∨ y (Suc i) = x i):]"
  apply (simp add:  LocalSystem_simp assert_true_skip)
  apply (rule prec_rel_eq)
  apply (simp add: fun_eq_iff prec_pre_sts_simp INIT_SUM_B_def PREC_SUM_B_def REL_SUM_B_def, safe)
  apply (drule_tac x = "Summ x" in spec, simp_all, metis)
  apply (cut_tac  u = u and k = n and x = x in le_sum_suc, simp_all)
  apply auto [1]
  using order_trans apply blast
  apply (simp add: rel_pre_sts_simp INIT_SUM_B_def REL_SUM_B_def fun_eq_iff, safe, simp_all)
  apply metis
  by (rule_tac x = xa in exI, simp)
    

lemma prod_comp_spec[simp]: "pa ≤ inpt ra ⟹ pb ≤ inpt rb ⟹ (({.pa.} ∘ [:ra:]) ** ({.pb.} ∘ [:rb:])) ∘ (({.pc.} ∘ [:rc:]) ** ({.pd.} ∘ [:rd:])) 
  = ({.pa.} o [:ra:] o {.pc.} o [:rc:]) ** ({.pb.} o [:rb:] o {.pd.} o [:rd:])"
  apply (simp add: Prod_spec assert_demonic_comp)
  apply (simp add: comp_assoc [THEN sym] assert_demonic_comp)
  apply (rule prec_rel_eq)
  apply (simp add: fun_eq_iff le_fun_def OO_def inpt_def)
  apply safe
  by auto

lemma prod_comp_implem: "implementable S ⟹ implementable S' ⟹ sconjunctive T ⟹ sconjunctive T' ⟹ (S ** S') o (T ** T') = (S o T) ** (S' o T')"
  apply (drule implementable_spec)
  apply (drule implementable_spec)
  apply (drule sconjunctiveE)
  apply (drule sconjunctiveE, safe)
  apply (drule_tac pa = p and pb = pa and pc = pb and pd = pc and ra = r and rb = ra and rc = rb and rd = rc in prod_comp_spec)
  by (simp_all add: comp_assoc)
    
definition "ang_rel S s q = S q s"
definition "dem_rel S q s' = q s'"

lemma mono_rep: "mono S ⟹ S = {:ang_rel S:} o [:dem_rel S:]"
  apply (simp add: demonic_def le_fun_def fun_eq_iff ang_rel_def dem_rel_def angelic_def, safe)
  apply (rule_tac x = x in exI, simp)
  apply (drule_tac x = xb and y = x in monoE, simp_all)
  by (simp_all add: le_fun_def)

lemma mono_repE: "mono (S::('a ⇒ bool) ⇒ ('b ⇒ bool)) ⟹ ∃ (r::'b ⇒ ('a ⇒ bool) ⇒ bool) (r') . S = {:r:} o [:r':]"
  by (drule_tac S = S in mono_rep, auto)

lemma prod_comp_a: "(S o T) ** (S' o T') ≤ (S ** S') o (T ** T')"
  apply (simp add: fun_eq_iff  Prod_demonic Prod_def prod_pred_def le_fun_def demonic_def, safe)
  by auto

lemma prod_comp_angelic_demonic: "({:r::'a⇒'b⇒bool:} ** {:r'::'c⇒'d⇒bool:}) o ([:t:] ** [:t':]) = ({:r:} o [:t:]) ** ({:r':} o [:t':])"
  apply (rule antisym)
  apply (simp_all add: prod_comp_a)
  proof safe
    fix  q s s'
    assume "({: r :} ** {: r' :} ∘ [: t :] ** [: t' :]) q (s, s') "
    from this have "∃p p'. prod_pred p p' ≤ ([: t :] ** [: t' :]) q ∧ {: r :} p s ∧ {: r' :} p' s'"
      by (simp add: Prod_def)
    from this have A: "∃p p'. (∀a b. p a ∧ p' b ⟶ (∃pa pa'. prod_pred pa pa' ≤ q ∧ t a ≤ pa ∧ t' b ≤ pa')) ∧ (∃x. r s x ∧ p x) ∧ (∃x. r' s' x ∧ p' x)"
      by (simp add: Prod_def  demonic_def angelic_def le_fun_def fun_eq_iff prod_pred_def)
    from this obtain p p' where B: "(∀a b. p a ∧ p' b ⟶ (∃pa pa'. prod_pred pa pa' ≤ q ∧ t a ≤ pa ∧ t' b ≤ pa')) ∧ (∃x. r s x ∧ p x) ∧ (∃x. r' s' x ∧ p' x)"
      by blast
   from B have "∃pa pa'. (( prod_pred pa pa' ≤ q )) ∧ (∃x. r s x ∧ t x ≤ pa) ∧ (∃x. r' s' x ∧ t' x ≤ pa')"
    apply safe
    apply (drule_tac x = x in spec)
    apply (drule_tac x = xa in spec)
    apply simp
    apply safe
    by auto
  from this show "(({: r :} ∘ [: t :]) ** ({: r' :} ∘ [: t' :])) q (s, s')"
    by (simp add: Prod_def demonic_def angelic_def fun_eq_iff)
 qed

definition "prod_rel r r' = (λ (x, y) (u, v) . r x u ∧ r' y v)"        

lemma Prod_angelic: "{:r:} ** {:r':} = {: prod_rel r r' :}"
  apply (simp add: fun_eq_iff angelic_def prod_pred_def prod_rel_def Prod_def le_fun_def, auto)
  apply (rule_tac x = "λ x . x = aa" in exI, simp)
  by (rule_tac x = "λ x . x = ba" in exI, simp)

lemma Prod_demonic_rel: "[:r:] ** [:r':] = [: prod_rel r r' :]"
  apply (simp add: Prod_demonic)
  apply (rule_tac f = demonic in arg_cong)
  by (simp add: fun_eq_iff prod_rel_def)

lemma prod_rel_comp: "prod_rel r r' OO prod_rel t t' = prod_rel (r OO t) (r' OO t')"
  apply (simp add: fun_eq_iff OO_def prod_rel_def)
  by auto
  
lemma prod_comp_angelic_demonic_demonic: "(({:ra:} o [:rd:]) ** ({:ra':} o [:rd':])) o ([:r:] ** [:r':]) = ({:ra:} o [:rd:] o [:r:]) ** (({:ra':} o [:rd':]) o [:r':])"
  proof -
    have "(({:ra:} o [:rd:]) ** ({:ra':} o [:rd':])) o ([:r:] ** [:r':]) = ({:ra:} ** {:ra':}) o ([:rd:] ** [:rd':]) o ([:r:] ** [:r':])"
      by (simp add: prod_comp_angelic_demonic)
    also have "... = ({:ra:} ** {:ra':}) o [:prod_rel rd rd':] o [:prod_rel r r':]"
      by (simp add: Prod_demonic_rel)
    also have "... = ({:ra:} ** {:ra':}) o [:prod_rel rd rd' OO prod_rel r r':]"
      by (simp add: comp_assoc demonic_demonic)

    also have "... = ({:ra:} ** {:ra':}) o [:prod_rel (rd OO r) (rd' OO r'):]"
      by (simp add:  prod_rel_comp)
    also have "... = ({:ra:} ** {:ra':}) o ([:(rd OO r):] ** [: (rd' OO r'):])"
      by (simp add: Prod_demonic_rel)
    also have "... = ({:ra:} o [:(rd OO r):]) ** ({:ra':} o [: (rd' OO r'):])"
      by (simp add: prod_comp_angelic_demonic)
    also have "... = ({:ra:} o [:rd:] o [:r:]) ** (({:ra':} o [:rd':]) o [:r':])"
      by (simp add: demonic_demonic [THEN sym] comp_assoc)
    finally show ?thesis by simp
 qed
      
lemma prod_comp_demonic: "mono (S::('a ⇒ bool) ⇒ ('b ⇒ bool)) ⟹ mono (S':: ('c ⇒ bool) ⇒ ('d ⇒ bool)) ⟹ 
    (S ** S') o ([:r:] ** [:r':]) = (S o [:r:]) ** (S' o [:r':])"
    apply (cut_tac ra  = "ang_rel S" and rd = "dem_rel S" and 
      ra' = "ang_rel S'" and rd' = "dem_rel S'" and r = r and r' = r' in prod_comp_angelic_demonic_demonic)
    by (simp add: mono_rep [THEN sym])
      
theorem DelayFeedback_prod: "init a ⟹ init' a' ⟹ implementable S ⟹ implementable S' ⟹ DelayFeedback init S ** DelayFeedback init' S' = 
   [- (x, y) ↝ x || y -] o DelayFeedback (prod_pred init init') (prod_sts S S') o [-λ x . (fst o x, snd o x) -]"
  apply (drule implementable_spec, safe)
  apply (drule implementable_spec, safe)
  by (simp add: DelayFeedback_LocalSystem prod_sts sts_prod)
    

(* Definition of feedback for systems that already contain a unit delay *)

lemma rel_fun_power: "((λx y. y = (f::'a ⇒ 'a) x) ^^ n) = (λ x y . (y = (f ^^ n) x))"
  apply (induction n)
  by auto

  lemma [simp]: "[:⊥:] = Magic"
    by (simp add: Magic_def)

  definition "IterateMask S n = Mask n ((S::('a::trace⇒bool) ⇒ ('a⇒bool)) ^^ n)"

  lemma IterateMask_simp: "IterateMask S = (λ n. Mask n (S ^^ n))"
    by (simp add: IterateMask_def)


  definition "IterateOmega S = Fusion (IterateMask S)"

  definition "IterateMaskA S n = Mask (n - 1) ((S::('a::trace⇒bool) ⇒ ('a⇒bool)) ^^ n)"

  lemma IterateMaskA_simp: "IterateMaskA S = (λ n. Mask (n-1) (S ^^ n))"
    by (simp add: IterateMaskA_def)


  definition "IterateOmegaA S = Fusion (IterateMaskA S)"

  lemma "IterateMaskA S n = (S ^^ n)o [:x ↝ y . ∀ (i::nat) < n - 1 . ((y i)::'a) = x i:]"
    apply (simp add: IterateMaskA_def Mask_def SkipTop_def)
    apply (subgoal_tac "eqtop (n - Suc 0) = (λ x y . ∀ (i::nat) < n - 1 . ((y i) ::'a) = x i)")
    apply auto [1]
    by (simp add: fun_eq_iff, auto)

lemma power_refin: "mono S ⟹ (S::'a::order⇒'a) ≤ T ⟹ S ^^ n ≤ T ^^ n"
proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  have "⋀ x . S ((S ^^ n) x) ≤ T ((T ^^ n) x)"
    apply (rule_tac y = "S ((T ^^ n) x)" in order_trans)
    apply (simp add: Suc.IH Suc.prems(1) Suc.prems(2) le_funD monoD)
    by (simp add: Suc.prems(2) le_funD)
  from this show ?case
    by (simp add: le_fun_def)
qed

lemma IterateMaskA_refin: "mono S ⟹ S ≤ T ⟹ IterateMaskA S n ≤ IterateMaskA T n"
  by (simp add: IterateMaskA_def power_refin Mask_refinement)


lemma IterateOmegaA_refin: "mono S ⟹ S ≤ T ⟹ IterateOmegaA S ≤ IterateOmegaA T"
  apply (simp add: IterateOmegaA_def)
  by (simp add: Fusion_refinement IterateMaskA_refin)


  lemma IterateOmega_spec: "IterateOmega ({.p.} o [:r:]) 
    =  {. (λx . ∀ n . ∀y. (r ^^ n) x y ⟶ p y) .} 
       ∘ [: INF n. (r ^^ n) OO eqtop n :]"
    apply (simp add: IterateOmega_def IterateMask_simp Mask_def power_spec
        Iterate_SkipNext_IterateSkipRel SkipTop_def comp_assoc demonic_demonic)
    apply (simp add: Fusion_spec)
    apply (subgoal_tac "(INF x. (λxa. ∀i<x. ∀y. (r ^^ i) xa y ⟶ p y)) 
           = (λx . ∀n y. (r ^^ n) x y ⟶ p y)")
    by auto

  lemma IterateOmegaA_spec: "IterateOmegaA ({.p.} o [:r:]) 
    =  {. (λx . ∀ n y. (r ^^ n) x y ⟶ p y) .} 
       ∘ [: INF n. (r ^^ n) OO eqtop (n-1) :]"
    apply (simp add: IterateOmegaA_def IterateMaskA_simp Mask_def power_spec
        Iterate_SkipNext_IterateSkipRel SkipTop_def comp_assoc demonic_demonic)
    apply (simp add: Fusion_spec)
    apply (subgoal_tac "(INF x. (λxa. ∀i<x. ∀y. (r ^^ i) xa y ⟶ p y)) 
           = (λx . ∀n y. (r ^^ n) x y ⟶ p y)")
    by auto



  lemma IterateOmegaA_demonic: "IterateOmegaA ([:r:]) 
    = [: INF n. (r ^^ n) OO eqtop (n-1) :]"
    apply (cut_tac p = ⊤ and r = r in IterateOmegaA_spec)
    by (simp add: assert_true_skip assert_true_skip_a)


  lemma rel_power_a: "⋀ y . ((r :: 'a ⇒ 'a ⇒ bool) ^^ n) x y ⟹ ∃ a . x = a 0 ∧ y = a n ∧ (∀ i < n . r (a i) (a (Suc i)))"
    proof (induction n, simp_all)
      fix y::'a show "∃a. y = a 0"
        by (rule_tac x = "λ i . y" in exI, simp)
    next
      fix y::'a and n
      assume " (r ^^ n OO r) x y"
      from this obtain z where [simp]: "(r ^^ n) x z " and [simp]: "r z y"
        by blast
      assume "(⋀y. (r ^^ n) x y ⟹ ∃a. x = a 0 ∧ y = a n ∧ (∀i<n. r (a i) (a (Suc i))))"
      from this have "∃a. x = a 0 ∧ z = a n ∧ (∀i<n. r (a i) (a (Suc i)))"
        by simp
      from this obtain a where [simp]: "x = a 0" and [simp]: "z = a n" and [simp]: "(∀i<n. r (a i) (a (Suc i)))"
        by blast
      show "∃a. x = a 0 ∧ y = a (Suc n) ∧ (∀i<Suc n. r (a i) (a (Suc i)))"
        apply (rule_tac x = "λ i . if i ≤ n then a i else y" in exI)
        apply auto
        using ‹r z y› less_Suc_eq by auto
  qed

  lemma rel_power_b: "⋀ y . ∃ a . x = a 0 ∧ y = a n ∧ (∀ i < n . r (a i) (a (Suc i))) ⟹ ((r :: 'a ⇒ 'a ⇒ bool) ^^ n) x y"
    apply (induction n, simp_all)
    apply blast
    apply safe
    apply (simp add: OO_def)
    apply (rule_tac x = "a n" in exI, simp_all)
    using less_Suc_eq by auto

  lemma rel_power: "((r :: 'a ⇒ 'a ⇒ bool) ^^ n) x y = (∃ a . x = a 0 ∧ y = a n ∧ (∀ i < n . r (a i) (a (Suc i))))"
    by (metis relpowp_fun_conv)


  lemma IterateOmega_demonic_spec: "IterateOmega [:r:] = [: INF n. r ^^ n OO eqtop n :]"
    apply (cut_tac p="λx. True" and r=r in IterateOmega_spec)
    by (simp add: assert_true_skip_a)

  lemma IterateOmega_func: "IterateOmega [- f -] = [: x ↝ y . ∀ n. eqtop n ((f ^^ n) x) y :]"
    apply (simp add: IterateOmega_demonic_spec update_def)
    apply (rule_tac f = demonic in arg_cong)
    by (simp add: fun_eq_iff OO_def rel_fun_power)

  lemma IterateOmega_func_aux_a: "(∀ n. eqtop n ((f ^^ n) x) y) = (∀ n . ∀ i < n . (f ^^ n) x i = y i)"
    by (simp)

  lemma IterateOmega_func_a: "IterateOmega [- f -] = [: x ↝ y . (∀ n . ∀ i < n . (f ^^ n) x i = y i):]"
   by (simp add: IterateOmega_func_aux_a IterateOmega_func)

  definition "apply x i = ((fst (fst x) i, snd (fst x) i), snd x i)"

  lemma IterateOmega_func_aux_b: "(∀ n. eqtop n ((f^^n) x) y) = (∀ n::nat . ∀ i::nat < n . apply ((f ^^ n) x) i = apply y i)"
    by (simp add: eqtop_prod_def apply_def, auto)


  lemma IterateOmega_func_aa: "IterateOmega [- f -] = [: x ↝ y . (∀ n . ∀ i::nat < n . apply ((f ^^ n) x) i = apply y i):]"
    by (simp add: IterateOmega_func_aux_b IterateOmega_func)

  lemma IterateOmega_func_b: "(∀ x n . ∀ i < n . (f ^^ n) x i = (f ^^ (Suc i)) x i) ⟹ IterateOmega [- f -] = [-λ x . (λ i . (f ^^ (Suc i)) x i)-]"
    apply (simp add: IterateOmega_func_a)
    apply (unfold update_def)
    apply (rule_tac f = demonic in arg_cong)
    apply (simp add: fun_eq_iff, auto)
    by (metis gt_ex)

  lemma IterateOmega_func_bb: "(∀ x n . ∀ i::nat < n . apply (((f::( ((nat ⇒ 'a) × (nat ⇒ 'b)) × (nat ⇒ 'c) ⇒  ((nat ⇒ 'a) × (nat ⇒ 'b)) × (nat ⇒ 'c)) )^^ n) x) i = apply ((f ^^ (Suc i)) x) i) 
       ⟹  
      IterateOmega [- f -] =[- (λ x . (let z = (λ i . apply ((f ^^ (Suc i)) x) i) in ((fst o fst o z, snd o fst o z), snd o z))) -]"
    apply (simp add: IterateOmega_func_aa)
    apply (unfold update_def)
    apply (rule_tac f = demonic in arg_cong)
    apply (simp add: fun_eq_iff apply_def Let_def, auto)
    apply (metis gt_ex)
    apply (metis gt_ex)
    by (metis gt_ex)

  lemma IterateOmega_func_c: "∀ x . ¬ (∀ n . ∀ i < n . (f ^^ n) x i = (f ^^ (Suc i)) x i) ⟹ IterateOmega [- f -] = Magic"
    apply (simp add: IterateOmega_func_a)
    apply (subgoal_tac "(λ x y . ∀n i. i < n ⟶ (f ^^ n) x i = y i) = ⊥")
    apply simp
    apply (simp add: fun_eq_iff, auto)
    apply (drule_tac x = x in spec, safe)
    by (metis comp_apply funpow.simps(2) lessI)


  lemma IterateOmega_assert_update: "IterateOmega ({.p.} o [-f-]) 
    =  {. (λx . ∀ n . p ((f ^^ n) x)) .} 
       ∘ [: x ↝ y . ∀ n. eqtop n ((f ^^ n) x) y :]"
    apply (simp add: IterateOmega_def IterateMask_simp Mask_def power_spec
        Iterate_SkipNext_IterateSkipRel SkipTop_def comp_assoc demonic_demonic update_def)
    apply (simp add:  Fusion_spec)
    apply (subgoal_tac "(INF x. (λxa. ∀i<x. ∀y. ((λx y. y = f x) ^^ i) xa y ⟶ p y)) 
           = (λx. ∀n. p ((f ^^ n) x))")
    apply auto
    apply (subgoal_tac "(INF x. (λx y. y = f x) ^^ x OO eqtop x) = (λx y. ∀n. eqtop n ((f ^^ n) x) y)")
    apply auto
    apply (simp add: fun_eq_iff OO_def rel_fun_power)
    apply (simp add: fun_eq_iff rel_fun_power)
    by blast

  lemma IterateOmega_assert_update_a: "IterateOmega ({.p.} o[- f -]) = {. (λx . ∀ n . p ((f ^^ n) x)) .} o [: x ↝ y . (∀ n . ∀ i < n . (f ^^ n) x i = y i):]"
    by (simp add: IterateOmega_assert_update)

  lemma IterateOmega_assert_update_b: "(∀ x n . ∀ i < n . (f ^^ n) x i = (f ^^ (Suc i)) x i) ⟹ IterateOmega ({.p.} o[- f -]) = {.(λx . ∀ n . p ((f ^^ n) x)).} o [-λ x . (λ i . (f ^^ (Suc i)) x i)-]"
    apply (simp add: IterateOmega_assert_update_a)
    apply (unfold update_def)
    by (metis gt_ex)

  lemma IterateOmega_assert_update_c: "IterateOmega ({.p.} o [- f -]) = {.(λx . ∀ n . p ((f ^^ n) x)).} o [: x ↝ y . (∀ n . ∀ i::nat < n . apply ((f ^^ n) x) i = apply y i):]"
    by (simp add: IterateOmega_func_aux_b IterateOmega_assert_update)


  thm IterateOmega_spec

  lemma IterateOmega_assert_update_d: "(∀ x n . ∀ i::nat < n . apply (((f::( ((nat ⇒ 'a) × (nat ⇒ 'b)) × (nat ⇒ 'c) ⇒  ((nat ⇒ 'a) × (nat ⇒ 'b)) × (nat ⇒ 'c)) )^^ n) x) i = apply ((f ^^ (Suc i)) x) i) ⟹  
      IterateOmega ({.p.} o [- f -]) = {.(λx . ∀ n . p ((f ^^ n) x)).} o [- (λ x . (let z = (λ i . apply ((f ^^ (Suc i)) x) i) in ((fst o fst o z, snd o fst o z), snd o z))) -]"
    apply (simp add: IterateOmega_assert_update_c)
    apply (unfold update_def)
    apply (rule prec_rel_eq, simp_all)
    apply (simp add: fun_eq_iff apply_def Let_def, auto)
    apply (metis gt_ex)
    apply (metis gt_ex)
    by (metis gt_ex)

  lemma IterateOmega_assert_update_e: "∀ x . ¬ (∀ n . ∀ i < n . (f ^^ n) x i = (f ^^ (Suc i)) x i) ∧ (∀n. p ((f ^^n) x)) ⟹ IterateOmega ({.p.} o [- f -]) = Magic"
    apply (simp add: IterateOmega_assert_update_a)
    apply (subgoal_tac "(λ x y . ∀n i. i < n ⟶ (f ^^ n) x i = y i) = ⊥")
    apply (simp add: assert_true_skip_a)
    apply (simp add: fun_eq_iff, auto)
    apply (drule_tac x = x in spec, safe)
    by (metis comp_apply funpow.simps(2) lessI)

      
 
definition "defined r = (∀ x . ∃ y . r x y)"
  

fun calcu :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'b) ⇒ ('a × 'b ⇒ 'a × 'c ⇒ bool) ⇒ nat ⇒ nat ⇒ 'a" where
  "calcu u x r n i = (if i ≤ n then u i else SOME u' . (∃y. r (calcu u x r n (i-1), x (i-1)) (u', y)))"

  thm choice_iff'

lemma prec_loc_st_defined_simp: "defined r ⟹ prec_pre_sts init p r
          = (λ x . ∀ u . init (u 0) ⟶ (∀n . ∃ y. r (u n, x n) (u (Suc n), y)) ⟶ (∀ n . p (u n, x n)))"
    apply (simp add: prec_pre_sts_simp fun_eq_iff)
  apply (safe)
    apply (simp add: choice_iff)
   apply blast
    apply (subst (asm) defined_def)
    apply (drule_tac x = "(calcu u x r n)" in spec)
  apply safe
    apply simp
   apply (simp del: calcu.simps)
   apply (case_tac "na < n", simp, blast) 
   apply (case_tac "na = n" , simp)
    apply (drule_tac x = "u n" in spec)
    apply (drule_tac x = "x n" in spec, safe)
    apply (rule someI, blast)
    apply (subst (2) calcu.simps)
   apply (simp del: calcu.simps)
    apply (drule_tac x = "(calcu u x r n na)" in spec)
    apply (drule_tac x = "x na" in spec, safe)
   apply (rule someI, blast)
proof -
  fix u n x
  assume " ∀na. p (calcu u x r n na, x na)"
  from this have "p (calcu u x r n n, x n)"
    by (simp del: calcu.simps)
  from this show "p (u n, x n)"
    by simp
qed
  
(*
lemma prec_loc_st_defined_simp_aux_a: "(∀n . ∃ y. r (u n, x n) (u (Suc n), y)) = (□ (lft_r_a (inpt_a r))) (u , x) (⊙ u)"
    by (simp add: always_def at_prod_def at_fun_def lft_r_a_def inpt_a_def next_trace_def)

  lemma prec_loc_st_defined_simp_aux_b: "(∀n::nat. p (u n, x n)) = (□ (lft_p p)) (u, x)"
    by (simp add: always_def at_prod_def at_fun_def lft_p_def)

  lemma prec_loc_st_defined_simp_a: "defined r ⟹ (∀ u . init (u 0) ⟶ prec_loc_st (λ u x . p (u,x)) (λ u u' x y . r (u, x) (u', y)) u x)
          = (∀ (u::nat ⇒ 'a) . init (u 0) ∧ (□ (lft_r_a (inpt_a r))) (u , x) (⊙ u) ⟶ (□ (lft_p p)) (u, x))"
    by (simp add: prec_loc_st_defined_simp prec_loc_st_defined_simp_aux_a prec_loc_st_defined_simp_aux_b, auto)

  lemma DelayFeedback_defined_simp: "defined r ⟹ DelayFeedback init ({.p.} o [:r:]) 
                =  {.x . ∀ (u::nat ⇒ 'a) . init (u 0) ∧ (□ (lft_r_a (inpt_a r))) (u , x) (⊙ u) ⟶ (□ (lft_p p)) (u, x).} 
                 o [:x ↝ y . ∃ (u::nat ⇒ 'a) . init (u 0) ∧ (□ (lft_r r)) (u, x) (⊙ u, y):]"
    by (simp add: DelayFeedback_simp  always_st_simp prec_loc_st_defined_simp_a)
      
*)

lemma DelayFeedback_defined_simp: "defined r ⟹ DelayFeedback init ({.p.} o [:r:]) 
              =  {.x . ∀ (u::nat ⇒ 'a) . init (u 0) ∧ ((∀n . ∃ y. r (u n, x n) (u (Suc n), y))) ⟶ (∀ n . p  (u n, x n)).} 
               o [:rel_pre_sts init r :]"
proof (simp add: DelayFeedback_simp prec_loc_st_defined_simp)
  have [simp]: "⋀ x . (∀u. init (u 0) ⟶ (∀n. ∃y. r (u n, x n) (u (Suc n), y)) ⟶ (∀n. p (u n, x n)))
      = (∀u. init (u 0) ∧ (∀n. ∃y. r (u n, x n) (u (Suc n), y)) ⟶ (∀n. p (u n, x n)))"
    by blast
  show " {.x.∀u. init (u 0) ⟶ (∀n. ∃y. r (u n, x n) (u (Suc n), y)) ⟶ (∀n. p (u n, x n)).} ∘ [: rel_pre_sts init r :] =
    {.x.∀u. init (u 0) ∧ (∀n. ∃y. r (u n, x n) (u (Suc n), y)) ⟶ (∀n. p (u n, x n)).} ∘ [: rel_pre_sts init r :]"
    by simp
qed
  

  
lemma defined_fun[simp]: "defined (λ x y . y = f x)"
  by (simp add: defined_def)

definition "map_f f x n = f (fst x n, snd x n)"
  
(*todo move inside DelayFeedback_update_simp*)
lemma DelayFeedback_update_simp_aux_b: "(∀n. ∃y. (u (Suc n), y) = f (u n, x n))  = ((⊙ u) = map_f (fst o f) (u, x))"    
  apply (simp add: always_def at_prod_def at_fun_def  fun_eq_iff map_f_def next_trace_def, auto)
  apply (metis eq_fst_iff)
  by (metis prod.exhaust_sel)

lemma DelayFeedback_update_simp_aux_a: "rel_pre_sts init (λx y. y = f x) = (λ x y . ∃u. init (u 0) ∧ ⊙ u = map_f (fst ∘ f) (u, x) ∧ y = map_f (snd ∘ f) (u, x))"
  apply (simp add: always_def at_prod_def at_fun_def  fun_eq_iff map_f_def next_trace_def rel_pre_sts_simp, safe)
  apply (metis fst_conv snd_conv)
  by auto

lemma DelayFeedback_update_simp: "DelayFeedback init ({.p.} o [-f-]) 
      = {. λx. ∀ (u::nat ⇒ 'a). init (u 0) ∧ (⊙ u) = map_f (fst o f) (u, x) ⟶ (∀ n . p (u n, x n)) .} 
      ∘ [: λx y. ∃ (u:: nat ⇒ 'a). init (u 0) ∧ (⊙ u) = map_f (fst o f) (u, x) ∧ y = map_f (snd o f) (u, x) :]"
  apply (simp add: update_def DelayFeedback_simp prec_loc_st_defined_simp DelayFeedback_update_simp_aux_b DelayFeedback_update_simp_aux_a)
  apply (subgoal_tac "⋀ x . (∀u. init (u (0::nat)) ⟶ ⊙ u = map_f (fst ∘ f) (u, x) ⟶ (∀n. p (u n, x n)))
    = (∀u. init (u (0::nat)) ∧ ⊙ u = map_f (fst ∘ f) (u, x) ⟶ (∀n. p (u n, x n)))")
   apply simp
  by blast


primrec itr :: "('a × 'b ⇒ 'a) ⇒ 'a ⇒ (nat ⇒ 'b) ⇒ nat ⇒ 'a" where 
  "itr f u0 x 0 = u0" | 
  "itr f u0 x (Suc n) = f (itr f u0 x n, x n)"

lemma map_itr_aux: "((⊙ u) = map_f f (u, x)) ⟹ (u n = itr f (u 0) x n)"
  apply (induction n, simp_all)
  by (simp add: fun_eq_iff next_trace_def map_f_def)

lemma map_itr_simp: "((⊙ u) = map_f f (u, x)) = (u = itr f (u 0) x)"
  apply safe
  apply (subst fun_eq_iff, safe)
  apply (rule map_itr_aux, simp)
  apply (simp add: fun_eq_iff)
  by (metis AbsNat_nat_def add.left_neutral add_Suc at_trace_def fst_conv id_apply itr.simps(2) map_f_def next_trace_def snd_conv)

lemma DelayFeedback_update_itr_simp: "DelayFeedback init ({.p.} o [-f-]) 
          = {. x. ∀ a . init a ⟶ (∀ i . p (itr (fst o f) a x i, x i)) .} 
          ∘ [: λx y. ∃ a. init a ∧ y = map_f (snd o f) (itr (fst o f) a x, x) :]"
proof (simp add: DelayFeedback_update_simp map_itr_simp)
  have [simp]: "⋀ x . (∀u. init (u 0) ∧ u = itr (fst ∘ f) (u 0) x ⟶ (∀n. p (u n, x n))) = (∀a. init a ⟶ (∀i. p (itr (fst ∘ f) a x i, x i)))"
    by auto
  have [simp]: "⋀ x y . (∃u. init (u 0) ∧ u = itr (fst ∘ f) (u 0) x ∧ y = map_f (snd ∘ f) (u, x))
    = (∃a. init a ∧ y = map_f (snd ∘ f) (itr (fst ∘ f) a x, x))"
    apply auto
    by (rule_tac x = "itr (fst ∘ f) a x" in exI, simp_all)
      
  show " {.x.∀u. init (u 0) ∧ u = itr (fst ∘ f) (u 0) x ⟶ (∀n. p (u n, x n)).} 
      ∘ [:x↝y.∃u. init (u 0) ∧ u = itr (fst ∘ f) (u 0) x ∧ y = map_f (snd ∘ f) (u, x):] =
        {.x.∀a. init a ⟶ (∀i. p (itr (fst ∘ f) a x i, x i)).} ∘ [:x↝y.∃a. init a ∧ y = map_f (snd ∘ f) (itr (fst ∘ f) a x, x):]"
    by simp
qed
  
definition "DelayFeedbackInit a S = DelayFeedback (λ u . u = a) S"
  
  
definition "lft_1_2 p = (λ (x, y) . p (x (0::nat), y (0::nat)))"
definition "lft_2_2 r = (λ (x, y) (z, t). r (x (0::nat), y (0::nat)) (z (0::nat), t (0::nat)))"

definition "iter_prec p f u x = (∀ n . p (itr (f) u x n, x n))"

theorem DelayFeedbackInit_update_simp_aux: "DelayFeedbackInit u ({.p.} o [-f-]) 
                = {. x. (∀ n . p (itr (fst o f) u x n, x n)) .} ∘ [-λx . map_f (snd o f) (itr (fst o f) u x, x)-]"
  apply (simp add: DelayFeedback_update_itr_simp DelayFeedbackInit_def)
  by (simp add: update_def)

theorem DelayFeedbackInit_update_simp_a: "DelayFeedbackInit u ({.p.} o [-f-]) 
                = {. x. iter_prec p (fst o f) u x .} ∘ [-λx . map_f (snd o f) (itr (fst o f) u x, x)-]"
  by (simp add:DelayFeedbackInit_update_simp_aux iter_prec_def)



lemma [simp]: "(□ lft_1_2 ⊤) = ⊤"
  by (simp add: always_def fun_eq_iff lft_1_2_def at_fun_def)
    
theorem DelayFeedbackInit_update_simp_b: "DelayFeedbackInit u [-f-] = [-λx . map_f (snd o f) (itr (fst o f) u x, x)-]"
  apply (cut_tac p = ⊤ and f = f and u = u in DelayFeedbackInit_update_simp_aux)
  by (simp add: assert_true_skip assert_true_skip_a)


lemma prec_itr_simp: "((□ lft_1_2 p) (itr f u x, x)) = (∀ n. p (itr f u x n, x n))"
  by (simp add: fun_eq_iff always_def lft_1_2_def at_fun_def at_prod_def)

lemma prec_itr_induction_aux: "p (u, x 0) ⟹ (⋀ n a . p (a, x n) ⟹ p (f (a ,x n), x (Suc n))) ⟹ p (itr f u x n, x n)"
  by (induction n, simp_all)

lemma iter_prec_induction: "p (u, x 0) ⟹ (⋀ n a . p (a, x n) ⟹ p (f (a ,x n), x (Suc n))) ⟹  iter_prec p f u x"
  by (simp add: prec_itr_induction_aux iter_prec_def)

lemma iter_prec_induction_unit_aux: "p (u, ()) ⟹ (⋀ n . p (itr f u x n, () ) ⟹ p (f (itr f u x n, x n), ())) ⟹   p (itr f u x n, ())"
  by (induction n, simp_all)

lemma iter_prec_induction_unit: "p (u, ()) ⟹ (⋀ n . p (itr f u x n, () ) ⟹ p (f (itr f u x n, x n), ())) ⟹  iter_prec p f u x"
  by (simp add: iter_prec_def iter_prec_induction_unit_aux)

lemma iter_prec_induction_unit_complete: "iter_prec p f u x ⟹ p (u, () ) ∧ (∀ n a . p (itr f u x n, () ) ⟶ p (f (itr f u x n, () ), () ))"
  apply (simp add: prec_itr_induction_aux iter_prec_def, safe)
   apply (metis itr.simps(1))
  by (drule_tac x = "Suc n" in spec, simp)

lemma iter_prec_induction_unit_iff: "iter_prec p f u x = (p (u, () ) ∧ (∀ n a . p (itr f u x n, () ) ⟶ p (f (itr f u x n, () ), () )))"
  apply (safe, simp_all add: iter_prec_induction_unit_complete)
  by (rule iter_prec_induction_unit, simp_all)

lemma prec_itr_induction: "p (u, x 0) ⟹ (⋀ n a . p (a, x n) ⟹ p (f (a ,x n), x (Suc n))) ⟹ ((□ lft_1_2 p) (itr f u x, x))"
  by (simp add: prec_itr_simp prec_itr_induction_aux)

definition "lft_r r x y = r (fst x 0, snd x 0) (fst y 0, snd y 0)"
definition "lft_r_b r x y = r (x 0) (y 0)"

lemma rel_itr_simp: "(□ (lft_r_b r)) x (map_f g (itr f u x, x)) = (∀ n . r (x n) (g (itr f u x n, x n)))"
  by (simp add: fun_eq_iff always_def  at_fun_def at_prod_def lft_r_b_def map_f_def)

  lemma rel_itr_induction_aux: "r (x 0) (g (u, x 0)) ⟹ (⋀ n a . r (x n) (g (a, x n)) ⟹ r (x (Suc n)) (g (f (a ,x n), x (Suc n)))) ⟹ r (x n) (g (itr f u x n, x n))"
    by (induction n, simp_all)
  
  lemma rel_itr_induction: "r (x 0) (g (u, x 0)) ⟹ (⋀ n a . r (x n) (g (a, x n)) ⟹ r (x (Suc n)) (g (f (a ,x n), x (Suc n)))) ⟹ (□ (lft_r_b r)) x (map_f g (itr f u x, x))"
    by (simp add: rel_itr_simp rel_itr_induction_aux)

  lemma rel_bounded_itr_induction_aux: "(0 ∈ b ⟹ r (x 0) (g (u, x 0))) ⟹ 
      (⋀ n a . (n ∈ b ⟹ r (x n) (g (a, x n))) ⟹ Suc n ∈ b  ⟹ r (x (Suc n)) (g (f (a ,x n), x (Suc n)))) ⟹ n ∈ b ⟹ r (x n) (g (itr f u x n, x n))"
    by (induction n, simp_all)

  lemma rel_bounded_itr_induction: "(0 ∈ b ⟹ r (x 0) (g (u, x 0))) ⟹ (⋀ n a . (n ∈ b ⟹ r (x n) (g (a, x n))) ⟹ Suc n ∈ b ⟹ r (x (Suc n)) (g (f (a ,x n), x (Suc n)))) 
      ⟹ (□b b (lft_r_b r)) x (map_f g (itr f u x, x))"
    apply (simp add: fun_eq_iff always_bounded_def  at_fun_def at_prod_def lft_r_b_def map_f_def, safe)
    apply (cut_tac g = g and r = r and n = fa and u = u and f = f and x = x  and b = b in rel_bounded_itr_induction_aux)
    by simp_all

  lemma refin_demonic_spec: "([:r:] ≤ {.p.} o [:r':]) = (p = ⊤ ∧ r' ≤ r)"
    by (simp add: fun_eq_iff le_fun_def demonic_def assert_def, auto)
  
lemma spec_delay_feedback_fun_refine: "({.p'.} o [: r :] ≤ DelayFeedbackInit u ({.p.} o [-f-])) = ((p' ≤ (λx. (□ lft_1_2 p) (itr (fst o f) u x, x)))
    ∧ (∀ x . p' x ⟶  r x ( map_f (snd o f) (itr (fst o f) u x, x)) ))"
    apply (simp add: DelayFeedbackInit_update_simp_aux)
    apply (simp add: update_def)
    by (simp add: assert_demonic_refinement, auto simp add: lft_1_2_def always_def at_fun_def at_prod_def)

lemma prec_itr_inductionA: "(p' x ⟹ p (u, x 0)) ⟹ (⋀ n a . p' x ⟹ p (a, x n) ⟹ p (f (a ,x n), x (Suc n))) ⟹ p' x ⟹ ((□ lft_1_2 p) (itr f u x, x))"
  by (simp add: prec_itr_simp prec_itr_induction_aux)

lemma prec_itr_inductionB: "(⋀ x . p' x ⟹ p (u, x 0)) ⟹ (⋀ x n a . p' x ⟹ p (a, x n) ⟹ p (f (a ,x n), x (Suc n))) ⟹ p'≤ (λ x . (□ lft_1_2 p) (itr f u x, x))"
  by (simp add: le_fun_def prec_itr_simp prec_itr_induction_aux)

lemma rel_itr_inductionA: "(⋀ x . p' x ⟹ r (x 0) (g (u, x 0))) ⟹ (⋀ x n a . p' x ⟹ r (x n) (g (a, x n)) ⟹ r (x (Suc n)) (g (f (a ,x n), x (Suc n)))) 
  ⟹ p' x ⟹ (□ (lft_r_b r)) x (map_f g (itr f u x, x))"
  by (simp add: rel_itr_simp rel_itr_induction_aux)


lemma "{:z ↝ x . x ≠ (0::nat):} o [:x ↝ y . x = 0 ∧ y = (0::nat):] = ⊤"
  apply (simp_all add: fun_eq_iff demonic_def assert_def assume_def le_fun_def angelic_def)
  by auto [1]
    
lemma "{:z ↝ x . x ≠ (Suc n):} o [:x ↝ y . x = 0 ∧ y = (0::nat):] = ⊤"
  apply (simp_all add: fun_eq_iff demonic_def assert_def assume_def le_fun_def angelic_def)
  apply auto [1]
  by (rule_tac x = "Suc (Suc n)" in exI, simp)


lemma "({.p'.} o [: □ (lft_r_b r) :] ≤ DelayFeedbackInit u ({.p.} o [-f-])) = ((p' ≤ (λx. (□ lft_1_2 p) (itr (fst o f) u x, x)))
  ∧ (∀ x . p' x ⟶  (□ (lft_r_b r)) x ( map_f (snd o f) (itr (fst o f) u x, x)) ))"
  by (simp add: spec_delay_feedback_fun_refine)

  lemma demonic_delay_feedback_fun_refine: "([:r :] ≤ DelayFeedbackInit u ({.p.} o [-f-])) = (((λx. (□ lft_1_2 p) (itr (fst o f) u x, x)) = ⊤)
    ∧ (∀ x . r x (map_f (snd o f) (itr (fst o f) u x, x)) ))"
    apply (simp add: DelayFeedbackInit_update_simp_aux)
    apply (simp add: update_def)
    by (simp add: refin_demonic_spec, auto simp add: lft_1_2_def always_def at_fun_def at_prod_def)

lemma "([: □ (lft_r_b r) :] ≤ DelayFeedbackInit u ({.p.} o [-f-])) = (((λx. (□ lft_1_2 p) (itr (fst o f) u x, x)) = ⊤)
  ∧ (∀ x . (□ (lft_r_b r)) x (map_f (snd o f) (itr (fst o f) u x, x)) ))"
  by (simp add: demonic_delay_feedback_fun_refine)
  
  lemma refin_update_spec: "([: □b b (lft_r_b r) :] ≤ DelayFeedbackInit u ({.p.} o [-f-])) = (((λx. (□ lft_1_2 p) (itr (fst o f) u x, x)) = ⊤)
    ∧ (∀ x y . y = map_f (snd o f) (itr (fst o f) u x, x) ⟶  (□b b (lft_r_b r)) x y ))"
    apply (simp add: DelayFeedbackInit_update_simp_aux)
    apply (simp add: update_def)
    by (simp add: refin_demonic_spec, auto simp add: lft_1_2_def always_def at_fun_def at_prod_def)

  definition "prec_delay p f_state u = (λx. (□ lft_1_2 p) (itr (f_state) u x, x))"
  definition "func_delay f_state f_out u = (λx . map_f f_out (itr f_state u x, x))"

  theorem DelayFeedbackInit_update_simp_c: "DelayFeedbackInit u ({.p.} o [-f-]) 
                = {.prec_delay p (fst o f) u.} ∘ [-func_delay (fst o f) (snd o f) u-]"
    apply (simp add: DelayFeedbackInit_update_simp_aux prec_delay_def func_delay_def)
    by (auto simp add: lft_1_2_def always_def at_fun_def at_prod_def)

theorem DelayFeedbackInit_update_simp_d: "DelayFeedbackInit u [-f-] =  [-func_delay (fst o f) (snd o f) u-]"
  by (simp add: DelayFeedbackInit_update_simp_b func_delay_def)


lemma always_lft_bot: "(□ lft_1_2 (⊥::('a × 'b ⇒ bool) )) = ⊥"
  by (simp add: fun_eq_iff lft_1_2_def always_def at_fun_def at_prod_def)
    

lemma DelayFeedbackInit_bot: "DelayFeedbackInit u ((⊥::(('a × 'b) ⇒ bool) ⇒ ('a × 'c) ⇒ bool)) = ⊥"
  apply (subst Refinement.fail_assert_update)
  apply (simp add: DelayFeedbackInit_update_simp_aux always_lft_bot)
  by (simp add: fun_eq_iff assert_def)


lemma simp_prec: "{. p .} ∘ [: λx y. ¬ p x ∨ r x y :] = {.p.} o [:r:]"
  by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, auto)

lemma inpt_and_rel: "(inpt r x ∧ r x y) = r x y"
  using inpt_def by fastforce
    
lemma [simp]: "inpt (λx y. inpt r x ∧ r x y) = inpt r"
  by (simp add: inpt_and_rel)
    
thm DelayFeedback_defined_simp
lemma DelayFeedback_inpt: "DelayFeedback init ({.inpt r.} o [:r:]) 
    =  {.x. ∀(u::nat ⇒ 'a). init (u 0) ∧ ((∀n. ∃y. ¬ inpt r (u n, x n) ∨ r (u n, x n) (u (Suc n), y))) ⟶ (∀n. inpt r (u n, x n)).} ∘
    [:  rel_pre_sts init (λx y. ¬ inpt r x ∨ r x y) :] "
  apply (cut_tac init = init and p = "inpt r" and r = "λ x y . ¬ inpt r x ∨ r x y" in DelayFeedback_defined_simp)
  apply (simp add: defined_def inpt_def)
  apply auto [1]
  by (simp only: simp_prec)

  declare comp_skip[simp del]
  declare skip_comp[simp del]
  declare prod_skip_skip[simp del]
declare fail_comp[simp del]

subsection‹Data Refinement›
definition "data_refin_sts d S S' =  ({:t, x  ↝ s, x' . x = x' ∧ d t s:} o S ≤ S' o {:t', y ↝ s', y' . y = y' ∧ d t' s':})"

lemma data_refin_sts_simp: "data_refin_sts d ({. p .} ∘ [: r :]) ({. p' .} ∘ [: r' :]) = 
  ((∀t x s. d t s ∧ p (s, x) ⟶ p' (t, x)) ∧
  (∀t x s t' y. d t s ∧ p (s, x) ∧ r' (t, x) (t', y) ⟶ (∃s'. d t' s' ∧ r (s, x) (s', y))))"
  apply (simp add: data_refin_sts_def fun_eq_iff le_fun_def demonic_def angelic_def assert_def, safe)
  by blast+
    
primrec s_r :: "('a ⇒'b ⇒ bool) ⇒ ('b ⇒ bool) ⇒ ('b × 'c ⇒ 'b × 'd ⇒ bool) ⇒ (nat ⇒ 'c) ⇒ (nat ⇒ 'd) ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'b" where
  "s_r d init r x y t 0 = (SOME s . d (t 0) s ∧ init s)" |
  "s_r d init r x y t (Suc n) = (SOME s . d (t (Suc n)) s ∧ r (s_r d init r x y t n, x n) (s, y n))" 
      
theorem data_refinement_sts: "(⋀ t . init' t ⟹ ∃ s . d t s ∧ init s) ⟹
  data_refin_sts d ({.p.} o [:r:]) ({.p'.} o [:r':]) ⟹ LocalSystem init p r ≤ LocalSystem init' p' r'"
proof (simp add: LocalSystem_simp)
  assume A: "data_refin_sts d ({. p .} ∘ [: r :]) ({. p' .} ∘ [: r' :])"
  have C: "⋀ t x s. d t s ⟹ p (s, x) ⟹ p' (t, x)"
    and D: "⋀ t x s t' y. d t s ⟹ p (s, x) ⟹ r' (t, x) (t', y) 
        ⟹ (∃s'. d t' s' ∧ r (s, x) (s', y))"
    using A apply (simp add: data_refin_sts_simp, blast)
    using A by (simp add: data_refin_sts_simp)
      
  assume B: "⋀ t . init' t ⟹ ∃ s . d t s ∧ init s"
      
  define s where "s = (λ x y t . s_r d init r x y t)"
      
  have [simp]: "⋀ t x y . init' (t 0) ⟹ init (s x y t 0)"
    apply (simp add: s_def)
    using B  by (rule someI2_ex, simp_all)

  have X[simp]: "⋀ t x y . init' (t 0) ⟹ d (t 0) (s_r d init r x y t 0)"
    apply (simp add: s_def)
    using B  by (rule someI2_ex, simp_all)
      
  have Aux: "⋀t x y n. init' (t 0) ⟹
               ∀n. (∀i<n. r (s x y t i, x i) (s x y t (Suc i), y i)) ⟶ p (s x y t n, x n) 
      ⟹ (∀i<n. r' (t i, x i) (t (Suc i), y i)) ⟹ (∀i < n. d (t (Suc i)) (s x y t (Suc i)) ∧ r (s x y t i, x i) (s x y t (Suc i), y i))  ∧ p' (t n, x n)"
  proof -
    fix t x y n 
    show " init' (t 0) ⟹ ∀n. (∀i<n. r (s x y t i, x i) (s x y t (Suc i), y i)) ⟶ p (s x y t n, x n) 
      ⟹ (∀i<n. r' (t i, x i) (t (Suc i), y i)) ⟹ (∀i < n. d (t (Suc i)) (s x y t (Suc i)) ∧ r (s x y t i, x i) (s x y t (Suc i), y i))  ∧ p' (t n, x n)"
  proof (induction n)
    case 0
    then show ?case
      apply simp
      apply (drule_tac x = 0 in spec, simp)
      apply (rule_tac s = "s x y t 0" in C, simp_all)
      apply (simp add: s_def)
      using B  by (rule someI2_ex, simp_all)
  next
    case (Suc n)
      
    have [simp]: "d (t n) (s_r d init r x y t n)"
      apply (case_tac n)
      using Suc.prems(1) X apply auto[1]
      using Suc.IH Suc.prems(1) Suc.prems(2) Suc.prems(3) s_def less_SucI by blast
        
    have [simp]: "p (s_r d init r x y t n, x n)"
      using Suc(3) apply (drule_tac x = n in spec)
      apply safe
      using Suc.IH Suc.prems(1) Suc.prems(2) Suc.prems(3) less_SucI apply blast
      by (simp add: s_def)
      
    have "⋀ i . i < Suc n ⟹ d (t (Suc i)) (s x y t (Suc i)) ∧ r (s x y t i, x i) (s x y t (Suc i), y i)"
      apply (case_tac "i < n")
      using Suc.IH Suc.prems(1) Suc.prems(2) Suc.prems(3) less_SucI apply blast
      apply (case_tac "i = n", simp_all)
      apply (simp add: s_def)
      apply (rule someI2_ex, simp_all)
      apply (rule_tac t = "t n" in D, simp_all)
      by (simp add: Suc.prems(3))
    from this show ?case
      apply simp
      apply (rule_tac s = "s x y t (Suc n)" in  C, simp)
      using Suc(3) by simp
  qed
qed
  have [simp]: "⋀ x .prec_pre_sts init p r x ⟹ prec_pre_sts init' p' r' x"
  proof (unfold prec_pre_sts_simp, safe)
    fix xa u y n
    assume [simp]: "∀u y. init (u 0) ⟶ (∀n. (∀i<n. r (u i, xa i) (u (Suc i), y i)) ⟶ p (u n, xa n))"
    assume [simp]: "∀i<n. r' (u i, xa i) (u (Suc i), y i)"
    assume [simp]: "init' (u 0)"
    have "(∀i< n. d (u (Suc i)) (s xa y u (Suc i)) ∧ r (s xa y u i, xa i) (s xa y u (Suc i), y i)) ∧ p' (u ( n), xa ( n))"
      by (rule Aux, simp_all)
    from this show " p' (u n, xa n)"
      by simp
  qed
    
  have [simp]: "⋀ x y . prec_pre_sts init p r x ⟹ rel_pre_sts init' r' x y ⟹ rel_pre_sts init r x y"
  proof (simp add: prec_pre_sts_simp rel_pre_sts_simp, safe)
    fix x y u
    assume [simp]: "∀u. init (u 0) ⟶ (∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n)) "
    assume [simp]: "init' (u (0::nat))"
    assume [simp]: "∀i. r' (u i, x i) (u (Suc i), y i)"

    have "⋀ n . (∀i< n. d (u (Suc i)) (s x y u (Suc i)) ∧ r (s x y u i, x i) (s x y u (Suc i), y i)) ∧ p' (u ( n), x ( n))"
      by (rule Aux, simp_all)
    from this show "∃u. init (u 0) ∧ (∀i. r (u i, x i) (u (Suc i), y i))"
      by (rule_tac x = "s x y u" in exI, simp, blast)
  qed
      
  show "{. prec_pre_sts init p r .} ∘ [: rel_pre_sts init r :] ≤ {. prec_pre_sts init' p' r' .} ∘ [: rel_pre_sts init' r' :]"
    by (unfold assert_demonic_refinement, safe, simp_all)
qed

subsection‹Reachability and Refinement›

definition "reach init r n x y s = (init (s 0) ∧ (∀ i < n . r (s i, x i) (s (Suc i), y i)))"

lemma reach_prec_always: "reach init r n x y s ⟹ p ≤ inpt r ⟹ prec_pre_sts init p r x 
    ⟹ ∃ s' y' . init (s' 0) ∧ (∀ i < n . y' i = y i) ∧ (∀ i ≤ n . s' i = s i) ∧ (□ lift_rel r) (s', x) (s'[1..], y')"
proof -
  assume "reach init r n x y s"
  from this have [simp]: "init (s 0)" and A: "⋀ i . i < n ⟹ r (s i, x i) (s (Suc i), y i)"
    by (simp add: reach_def)+
      
  assume "prec_pre_sts init p r x"
  from this have C: "⋀ s n. init (s 0) ⟹ (∃ y . (∀i<n. r (s i, x i) (s (Suc i), y i))) ⟹ p (s n, x n)"
    by (simp add: prec_pre_sts_simp , blast)
      
  assume "p ≤ inpt r"
  from this have B: "⋀ s x . p (s, x) ⟹ (∃  sy . r (s,x) (sy))"
    by (simp add: inpt_def le_fun_def)
      
  define nxt where "nxt = (λ s x  . Eps (r (s, x)))"
    
  define sa where "sa = (λ i . (if i < n then s i else uu r (s n) (x[n..]) (i - n)))"
  define ya where "ya = (λ i . (if i < n then y i else yy r (s n) (x[n..]) (i - n)))"
    
  have D: "⋀ n . ∀ i < n . r (sa i, x i) (sa (Suc i), ya i)"
  proof -
    fix m
    show " ∀ i < m . r (sa i, x i) (sa (Suc i), ya i)"
    proof (induction m)
      case 0
      then show ?case by simp
    next
      case (Suc m)
      show ?case
        apply safe
        apply (case_tac "i < m")
        using Suc apply (simp)
        apply (case_tac "i = m", simp_all)
        apply (case_tac "m < n", simp add: sa_def ya_def,  safe)
        using A apply blast
         apply (simp add: uu_def)
         apply (case_tac "n = Suc m", simp_all)
        using A apply blast
          apply (case_tac "m = n", simp)
         apply (simp add: sa_def ya_def uu_def yy_def)
         apply (rule_tac someI_ex)
         apply (rule B)
         apply (rule C, simp_all)
         apply (rule_tac x = y in exI)
        using A apply blast
          apply (case_tac "n < m", simp_all)
        apply (simp add: sa_def ya_def uu_def yy_def split: nat.split, safe)
        apply (case_tac "x2a = Suc x2", simp_all)
          apply (case_tac "(Suc (n + x2)) = m", simp_all)
         apply (rule_tac someI_ex)
        apply (rule B)
        apply (cut_tac s = sa and n = m in C)
          apply  (simp add: sa_def uu_def)
        using Suc apply blast
          by (simp add: sa_def uu_def)
      qed
    qed
      
  show "∃ s' y' . init (s' 0) ∧ (∀ i < n . y' i = y i) ∧(∀ i ≤ n . s' i = s i) ∧ (□ lift_rel r) (s', x) (s'[1..], y')"
    apply (rule_tac x = "sa" in exI)
    apply (rule_tac x = "ya" in exI)
    apply (simp_all add: always_def lift_rel_def at_fun_def at_prod_def, safe)
       apply (simp add: sa_def uu_def)
      apply (simp add: ya_def)
     apply (simp add: sa_def uu_def)
      by (cut_tac n = "Suc f" in D, blast)
qed

 
lemma refinemen_reachable_B:
  assumes R: "LocalSystem init p r ≤ LocalSystem init' p' r'"
    and  [simp]: "p' ≤ inpt r'"
  shows "prec_pre_sts init p r x ⟹ reach init' r' n x y t ⟹ ∃ s . reach init r n x y s"
    and "prec_pre_sts init p r x ⟹ reach init' r' n x y t ⟹ p' (t n, x n)"
proof -
  assume prec: "prec_pre_sts init p r x"
  from R and prec have A: "prec_pre_sts init' p' r' x"
    by (unfold LocalSystem_simp assert_demonic_refinement, blast)

  from prec and R have B: "⋀ y . rel_pre_sts init' r' x y ⟹ rel_pre_sts init r x y"
    by (unfold LocalSystem_simp assert_demonic_refinement, blast)
      
  assume [simp]: "reach init' r' n x y t"

  from A have "∃ s' y' . init' (s' 0) ∧ (∀ i < n . y' i = y i) ∧ (∀ i ≤ n . s' i = t i) ∧ (□ lift_rel r') (s', x) (s'[1..], y')"
    by (rule_tac p = p' in reach_prec_always, simp_all)
      
  from this obtain ta ya where I[simp]: "init' (ta 0)" and X: " (⋀ i . i ≤ n ⟹ ta i = t i)" and T: "⋀ i . i < n ⟹ ya i = y i" and Y: "(□ lift_rel r') (ta, x) (ta[1..], ya)"
    by blast
      
  have "rel_pre_sts init' r' x ya"
    using Y I by (unfold rel_pre_sts_def, blast)

  from this B have "rel_pre_sts init r x ya" 
    by blast
      
  from this obtain sa where "init (sa 0) ∧ (□ lift_rel r) (sa, x) (sa[1..], ya)"
    by (simp add: rel_pre_sts_def, blast)
      
  from this have "reach init r n x y sa"
    by (simp add: reach_def always_def at_fun_def lift_rel_def at_prod_def  T [symmetric])
      
  from this show "∃ s . reach init r n x y s"
    by blast
      
  from A have Z: "((∀i<n. r' (ta i, x i) (ta (Suc i), ya i)) ⟹ p' (ta n, x n))"
    by (simp add: prec_pre_sts_simp)
      
  have [simp]: "⋀ i . r' (ta i, x i) (ta (Suc i), ya i)"
    using Y by (simp add: always_def at_fun_def lift_rel_def at_prod_def)
      
  show "p' (t n, x n)"
    by (simp add: X [symmetric], rule Z, simp)
qed

  
lemma sel_inf_a: "finite X ⟹ (⋀ i :: nat . f i ∈ X) ⟹ (∃ x ∈ X . infinite {i . f i = x})"
proof -
  assume A: "finite X"
  assume "(⋀ i :: nat . f i ∈ X)"
  from this have "(⋃ x ∈ X . {i . f i = x}) = UNIV"
    by blast
  from this have "infinite  (⋃ x ∈ X . {i . f i = x})"
    by simp
  from this show "∃ x∈ X . infinite {i . f i = x}"
    using A by auto
qed
  
lemma "X ≠ {} ⟹ ∃ (x::'a::wellorder) ∈ X . ∀ y ∈ X . x ≤ y"
proof -
  assume "X ≠ {}"
  then obtain aa :: "'a set ⇒ 'a" where
    "aa X ∈ X"
    by (metis equals0I)
  then show ?thesis
    by (meson wellorder_Least_lemma(1) wellorder_Least_lemma(2))
qed
  
primrec min_rest :: "nat set ⇒ nat ⇒ nat" where
  "min_rest X 0 =  (LEAST x . x ∈ X)" |
  "min_rest X (Suc n) = min_rest (X  - {LEAST x . x ∈ X}) n"
 

lemma sel_inf_fun: "⋀ X . infinite X ⟹ min_rest X n ∈ X ∧ min_rest X n < min_rest X (Suc n)"
proof (induction n)
  case 0
  have "⋀ x X . (x::nat) ∈ X ⟹  (LEAST x. x ∈ X) ≤ x"
    by (simp add: Least_le)

  from this have A: "⋀ x X . (x::nat) ∈ X ⟹ x ≠ (LEAST x. x ∈ X) ⟹  (LEAST x. x ∈ X) < x"
    by (simp add: dual_order.strict_iff_order)
      
  have B: "infinite (X - {LEAST x. x ∈ X})"
    using 0 by (rule infinite_remove)
      
  from this obtain x where C: "x ∈ (X - {LEAST x. x ∈ X})"
    by (cut_tac S  = "(X - {LEAST x. x ∈ X})" in infinite_imp_nonempty, auto)
      
  have D: " (LEAST x. x ∈ X - {LEAST x. x ∈ X}) ∈ (X - {LEAST x. x ∈ X})"
    apply (rule_tac k = x in LeastI)
    using C by simp
    
      
  from 0 show ?case 
    apply simp
    apply safe
     apply (meson LeastI bounded_nat_set_is_finite)
     using D by (rule_tac A, simp_all)
      
next
  case (Suc n)
  from this have U: "⋀ X .  infinite X ⟹ min_rest X n ∈ X"
    and V: "⋀ X . infinite X ⟹  min_rest X n < min_rest X (Suc n)"
    by simp_all

  have A: "min_rest X (Suc n) ∈ X"
    apply simp
    apply (cut_tac X = "(X - {LEAST x. x ∈ X})" in U)
    using Suc(2) by simp_all
    
  have B: "min_rest X (Suc n) < min_rest X (Suc (Suc n))"
    apply simp
    apply (cut_tac X = "(X - {LEAST x. x ∈ X})" in V)
    using Suc(2) apply simp
      by simp
  from A and B show ?case
    by simp
qed
  
 
lemma sel_inf: "finite X ⟹ (⋀ i :: nat . f i ∈ X) ⟹ (∃ g x . x ∈ X ∧ (∀ i . f (g i) = x) ∧ (∀ i . g i < g (Suc i)))"
  apply (drule_tac f = f in  sel_inf_a, simp_all)
  apply safe
  apply (subst ex_comm)
  apply (rule_tac x = x in exI, simp)
  apply (rule_tac x = "min_rest  {i. f i = x}" in exI)
  apply simp
    apply safe
    apply (cut_tac X = "{i. f i = x}" and n = i in sel_inf_fun, simp_all)
    by (cut_tac X = "{i. f i = x}" and n = i in sel_inf_fun, simp_all)

  
definition "sel_inf f X = (SOME g . ∃ x . x ∈ X ∧ (∀ i . f (g i) = x) ∧ (∀ i . g i < g (Suc i)))"
  
lemma sel_inf_prop_aux: "finite X ⟹ (⋀ i :: nat . f i ∈ X) ⟹  (∃ x . x ∈ X ∧ (∀ i . f (sel_inf f X i) = x) ∧ (∀ i . sel_inf f X i < sel_inf f X (Suc i)))"
  apply (simp add: sel_inf_def)
  apply (rule_tac P = " (λ g . ∃ x . x ∈ X ∧ (∀ i . f (g i) = x) ∧ (∀ i . g i < g (Suc i)))" in someI_ex)
  by (rule sel_inf, simp_all)

lemma sel_inf_prop: 
  assumes A: "finite X" and B: "(⋀ i :: nat . f i ∈ X)" 
  shows "f (sel_inf f X i) = f (sel_inf f X 0) " and "⋀ i . sel_inf f X i < sel_inf f X (Suc i)"
    and "i ≤ sel_inf f X i"
proof -
  from A and B have C: "(∃ x . x ∈ X ∧ (∀ i . f (sel_inf f X i) = x) ∧ (∀ i . sel_inf f X i < sel_inf f X (Suc i)))"
    by (simp add: sel_inf_prop_aux)
      
  from this show "f (sel_inf f X i) = f (sel_inf f X 0)"
    by (safe, frule_tac x = 0 in spec, simp)
      
  from C show D: "⋀ i . sel_inf f X i < sel_inf f X (Suc i)"
    by blast
      
  show "i ≤  sel_inf f X i"
  proof (induction i)
    case 0
    then show ?case by simp
  next
    case (Suc i)
    then show ?case
      by (metis D Suc_leI le_less less_trans)
  qed
    
qed
  
    
fun SSa :: "('a ⇒ bool) ⇒ ('a × 'b ⇒ 'a × 'c ⇒ bool) ⇒ (nat ⇒ 'b) ⇒ (nat ⇒ nat ⇒ 'a) ⇒ nat ⇒ nat ⇒ nat ⇒ 'a" where
  "SSa init r x s 0  = (s[Suc 0..] o sel_inf (λ i . s (Suc i) 0)  {s . init s})" |
  "SSa init r x s (Suc n)  = ((SSa init r x s n[Suc 0..]) o 
      sel_inf (λ i . SSa init r x s n (Suc i) (Suc n))  {s' . ∃ y . r ((SSa init r x s n[Suc 0..]) 0 n, x n) (s', y) })"


lemma refinemen_reachable_aux:
  assumes finite_next: "⋀ s x . finite {s' . ∃ y . r (s, x) (s', y)}"
    and finite_init[simp]: "finite {s . init s}"
   assumes  A: "(⋀ n . reach init r (Suc n) x y (s n))" 
   shows "(∀ j . ∀ k ≤ n . SSa init r x s n j k = SSa init r x s n 0 k) ∧ reach init r n x y ( SSa init r x s n n) 
      ∧ (∃ k . ∀ i . k i ≥ n ∧ SSa init r x s n i = s (k i) ∧ k i < k (Suc i))
      ∧ (∀ j . ∀ k ≤ n . SSa init r x s (Suc n) j k = SSa init r x s n 0 k)"
    proof (induction n)
      case 0
      show " (∀j k. k ≤ 0 ⟶ SSa init r x s 0 j k = SSa init r x s 0 0 k) ∧
          reach init r 0 x y (SSa init r x s 0 0) ∧ (∃k. ∀i. 0 ≤ k i 
        ∧ SSa init r x s 0 i = s (k i) ∧ k i < k (Suc i))
        ∧ (∀j k. k ≤ 0 ⟶ SSa init r x s (Suc 0) j k = SSa init r x s 0 0 k)"
        apply simp
        apply safe
         apply (rule sel_inf_prop, simp)
        using A apply (simp_all add: reach_def)
        apply (rule_tac x = "λ i . (Suc (sel_inf (λi. s (Suc i) 0) (Collect init) i))" in exI, clarsimp)
         apply (rule sel_inf_prop, simp_all)
        apply (rule sel_inf_prop(1))
          by simp_all
    next
      case (Suc n)
      from this have X: "reach init r n x y (SSa init r x s n n)"
        by simp
      have T: "⋀ i k . k ≤ n ⟹ SSa init r x s n i k = (SSa init r x s n (Suc 0) k)"
        by (metis Suc.IH)

      have "(∃k. ∀i. n ≤ k i ∧ SSa init r x s n i = s (k i) ∧ k i < k (Suc i))"
        using Suc by simp
          
      from this obtain k where VV[simp]: "⋀ i . n ≤ k i" and UU: "⋀ i . SSa init r x s n i = s (k i)" and XX: "⋀ i . k i < k (Suc i)"
        by blast

      have "⋀ i . r  (SSa init r x s n (Suc i) n, x n) (SSa init r x s n (Suc i) (Suc n), y n)"
        apply (simp add: UU)
        apply (cut_tac n = "k (Suc i)" in A)
        apply (simp add: reach_def, safe)
        apply (drule_tac x = n in spec, safe)
          using VV by (simp add: le_imp_less_Suc)
          
      from this have Y[simp]: "⋀ i . r (SSa init r x s n (Suc 0) n, x n) (SSa init r x s n (Suc i) (Suc n), y n)"
        by (cut_tac i = "Suc i" and k = n in T[symmetric], simp_all)
        
          
      have [simp]:"finite {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)}"
        using finite_next by blast
          
      have U: "⋀ j k . k ≤ Suc n ⟹ SSa init r x s (Suc n) j k = SSa init r x s (Suc n) 0 k"
        apply simp
        apply (case_tac "k = Suc n", simp_all)
         apply (rule sel_inf_prop(1), simp_all)
        using Y apply blast
        apply (case_tac "k ≤ n", simp_all)
          apply (subst (3) T, simp_all)
        by (subst (4) T, simp_all)
          
      have Z: "SSa init r x s n (Suc (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} (Suc n))) n
        = SSa init r x s n (Suc 0) n"
        by (subst (3) T, simp_all)

      have V: "reach init r (Suc n) x y (SSa init r x s (Suc n) (Suc n))"
        apply simp
        apply (simp add: reach_def, safe)
        using X apply (simp add: reach_def)
         apply (subst (3) T, simp_all, clarify)
         apply (subst (asm) T, simp_all)
        apply (case_tac "i = n", simp_all)
         apply (simp add: Z)
        apply (case_tac "i < n", simp_all)
          apply (subst (3) T, simp_all)
        apply (subst (4) T, simp_all)
        using X apply (simp add: reach_def, clarify)
        apply (drule_tac x = i in spec, simp)
         apply (subst (asm) (2) T, simp_all)
        by (subst (asm) (3) T, simp_all)
          
      have mono_k: "⋀ i j . i < j ⟹ k i < k j"
      proof -
        fix i j
        have Az: "i < j ⟶ k i < k j"
        proof (induction j)
          case 0
          then show ?case 
            by simp
        next
          case (Suc j)
          show ?case
            apply(case_tac "i = j", simp_all)
             apply (simp add: XX)
            apply (safe)
            apply (case_tac "i < j", simp_all)
              using Suc and XX apply simp
              using less_trans by auto
          qed
          assume "i < j"
          from this and Az show "k i < k j"
            by simp
        qed
          
          
      have W: "(∃k. ∀i. Suc n ≤ k i ∧ SSa init r x s (Suc n) i = s (k i) ∧ k i < k (Suc i))"
        apply simp
        apply (rule_tac x = "λ i . k (Suc (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} i)) " in exI, safe)
        prefer 2
          apply (simp add: UU)
         apply (rule_tac y = "Suc ( k (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} i))" in order_trans)
          apply simp_all
         apply (simp add: Suc_leI ‹⋀i. k i < k (Suc i)›)
        apply (rule mono_k, simp)
        apply (rule sel_inf_prop(2))
         apply simp_all
          using Y by blast
          define ZZ where "ZZ = (λj . (Suc (sel_inf (λi. SSa init r x s n
                                        (Suc (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} (Suc i)))
                                        (Suc (Suc n)))
                          {s'. ∃y. r (SSa init r x s n
                                       (Suc (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} (Suc 0))) (Suc n),
                                      x (Suc n))
                                    (s', y)}
                          j)))"
            
            from this have ZZ_simp: "⋀ j . ZZ j = (Suc (sel_inf (λi. SSa init r x s n
                                        (Suc (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} (Suc i)))
                                        (Suc (Suc n)))
                          {s'. ∃y. r (SSa init r x s n
                                       (Suc (sel_inf (λi. SSa init r x s n (Suc i) (Suc n)) {s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)} (Suc 0))) (Suc n),
                                      x (Suc n))
                                    (s', y)}
                          j))"
              by simp
            
        have TT: "⋀ j k . k ≤ Suc n ⟹ SSa init r x s (Suc (Suc n)) j k = SSa init r x s (Suc n) 0 k"
          apply simp
          apply (simp add: ZZ_simp[symmetric])
            apply (case_tac "k = Suc n")
          apply (cut_tac f = "(λi. SSa init r x s n (Suc i) (Suc n))"
                and X = "{s'. ∃y. r (SSa init r x s n (Suc 0) n, x n) (s', y)}" and i = "ZZ j" in  sel_inf_prop(1))
             apply simp_all
          using Y apply blast
          apply (case_tac "k ≤ n", simp_all)
            apply (subst (3) T, simp_all)
            by (subst (4) T, simp_all)
 
            
      from U and V and W and TT show "(∀j k. k ≤ Suc n ⟶ SSa init r x s (Suc n) j k = SSa init r x s (Suc n) 0 k) ∧
         reach init r (Suc n) x y (SSa init r x s (Suc n) (Suc n)) ∧
         (∃k. ∀i. Suc n ≤ k i ∧ SSa init r x s (Suc n) i = s (k i) ∧ k i < k (Suc i)) ∧
         (∀j k. k ≤ Suc n ⟶ SSa init r x s (Suc (Suc n)) j k = SSa init r x s (Suc n) 0 k)"
        by blast
    qed
  

lemma refinemen_reachable_A:
  assumes finite_next: "⋀ s x . finite {s' . ∃ y . r (s, x) (s', y)}"
    and finite_init: "finite {s . init s}"
  assumes A: "⋀ n x y t . prec_pre_sts init p r x ⟹ reach init' r' n x y t ⟹ p' (t n, x n)"
    and B: "⋀ n x y t . prec_pre_sts init p r x ⟹ reach init' r' n x y t ⟹ ∃ s . reach init r n x y s"
  shows "LocalSystem init p r ≤ LocalSystem init' p' r'"
proof (simp add: LocalSystem_simp assert_demonic_refinement, simp add: le_fun_def, safe)
  fix x y
  assume [simp]: "prec_pre_sts init p r x"


  show "prec_pre_sts init' p' r' x"
    apply (simp add: prec_pre_sts_simp, safe)
    apply (rule_tac y = y in A, simp)
    by (simp add: reach_def)
      
  assume [simp]: "rel_pre_sts init' r' x y"
   
    
  from this obtain t where "⋀ n . reach  init' r' n x y t"
    by (simp add: rel_pre_sts_simp reach_def, blast)
      
  from this have "⋀ n . ∃ s . reach init r n x y s"
    by (rule_tac t = t in B, simp_all)

  from this have "∃ s . ∀ n . reach init r n x y (s n)"
    by (subst choice_iff [symmetric], blast)
      
  from this obtain s where X: "⋀ n . reach init r n x y (s n)"
    by blast
      
  define ss where "ss = s[Suc 0..]"
    
  from X have Y: "⋀ n . reach init r (Suc n) x y (ss n)"
    by (simp add: ss_def)
        
  have U: "⋀ n . reach init r n x y (SSa init r x ss n n) " and
     V: "⋀ n j k. k ≤ n ⟹ SSa init r x ss n j k = SSa init r x ss n 0 k" and
     W: "⋀ n j k . k ≤ n ⟹ SSa init r x ss (Suc n) j k = SSa init r x ss n 0 k"
    apply (cut_tac s = ss and init = init and r = r and x= x and y = y in refinemen_reachable_aux)
    using finite_next apply (simp)
    using finite_init apply (simp)
    using Y apply simp
    apply blast
    apply (cut_tac s = ss and init = init and r = r and x= x and y = y in refinemen_reachable_aux)
    using finite_next apply (simp)
    using finite_init apply (simp)
    using Y apply simp
    apply blast
    apply (cut_tac s = ss and init = init and r = r and x= x and y = y and n = n in refinemen_reachable_aux)
    using finite_next apply (simp)
    using finite_init apply (simp)
    using Y apply simp
    by blast
      
  define sa where "sa = (λ i . SSa init r x ss (Suc i) (Suc i) i)"
  have [simp]: "⋀ i . r (sa i, x i) (sa (Suc i), y i)"
    apply (simp add: sa_def del: SSa.simps)
    apply (subst (2) W, simp)
    apply (cut_tac n = "Suc i" in U)
    apply (simp add: reach_def del: SSa.simps, safe)
      apply (drule_tac x = i in spec)
    apply (simp del: SSa.simps)
    by (subst (asm) (3) V, simp_all)
      
  have [simp]: "init (sa 0)"
    apply (simp add: sa_def del: SSa.simps)
    apply (cut_tac n = "Suc 0" in U)
    by (simp add: reach_def del: SSa.simps)
      
      
  show "rel_pre_sts init r x y"
    apply (simp add: rel_pre_sts_simp)
    by (rule_tac x = sa in exI, simp)
qed
 
definition "symb_sts_refin init p r init' p' r'
    = 
      ((∀ n x y t . prec_pre_sts init p r x ⟶ reach init' r' n x y t ⟶ p' (t n, x n))
      ∧ (∀ n x y t . prec_pre_sts init p r x ⟶ reach init' r' n x y t ⟶ (∃ s . reach init r n x y s)))"
  

lemma refinemen_reachable_iff:
  assumes finite_next[simp]: "⋀ s x . finite {s' . ∃ y . r (s, x) (s', y)}"
    and finite_init[simp]: "finite {s . init s}"
    and [simp]: "p' ≤ inpt r'"
  shows "LocalSystem init p r ≤ LocalSystem init' p' r' = symb_sts_refin init p r init' p' r'"
proof
  assume [simp]: "LocalSystem init p r ≤ LocalSystem init' p' r'"
  show "symb_sts_refin init p r init' p' r'"
    apply (simp add: symb_sts_refin_def)
      apply safe
    apply (cut_tac p = p and p' = p' and init = init and init' = init' and r = r and r' = r' in refinemen_reachable_B(2), simp_all)
    by (cut_tac p = p and p' = p' and init = init and init' = init' and r = r and r' = r' in refinemen_reachable_B(1), simp_all)
next
  assume A: "symb_sts_refin init p r init' p' r'"
  show "LocalSystem init p r ≤ LocalSystem init' p' r'"
    apply (rule refinemen_reachable_A, simp_all)
    using A apply (simp add: symb_sts_refin_def)
    using A by (simp add: symb_sts_refin_def, blast)
qed
  
definition "inv_top n P = (∀ u v . eqtop n u v ⟶ (P u = P v))"
definition "prec_pre_sts_bound init p r N x = ((∀u. init (u 0) ⟶ (∀y . ∀ n < N. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))))"
  
lemma replace_variables: "(inv_top (Suc N) (P N)) ⟹ (inv_top N (R N)) ⟹ (inv_top N (Q' N)) ⟹ (∀ (x::nat⇒'z) . P N x ∧ (ZZ (Q' N x) (Q N (x[N..]))) ∧ R N x ⟶ S N (x N))
    =  (∀ x xN y . P N (x(N := xN)) ∧ y 0 = xN ∧ (ZZ (Q' N x) ( Q N (y))) ∧ R N x ⟶ S N (xN))"
   proof safe
     fix x xN y
     assume A: "∀x. P N x ∧ ZZ (Q' N x) (Q N (x[N ..])) ∧ R N x ⟶ S N (x N)"
     assume B: " inv_top (Suc N) (P (N::nat))"
     assume C: " inv_top N (R N)"
     assume Ca: "inv_top N (Q' N)"
     assume D: "P N (x(N := y (0::nat)))"
     assume E: "ZZ (Q' N x) (Q N y)"
     assume F: "R N x"
       
     define xx where "xx = (λ i . if i < N then x i else y (i -N))"
     from A have  U: "P N xx ∧ ZZ (Q' N xx) (Q N (xx[N ..])) ∧ R N xx ⟶ S N (xx N)"
       by blast
     have [simp]: "P N xx"
       apply (cut_tac B, simp add: inv_top_def)
       apply (drule_tac x =  xx in spec)
       apply (drule_tac x =  "(x(N := y (0::nat)))" in spec)
       using D apply simp
       apply safe
       by (simp add: xx_def)
         
     from E have [simp]: "ZZ (Q' N xx) (Q N (xx[N ..]))"
       apply (subgoal_tac "xx[N..] = y")
        apply simp
       apply (cut_tac Ca, simp add: inv_top_def)
       apply (drule_tac x =  xx in spec)
       apply (drule_tac x =  "x" in spec)
       by (simp_all add: xx_def)
         
       
     have [simp]: "R N xx"
       apply (cut_tac C, simp add: inv_top_def)
       apply (drule_tac x =  xx in spec)
       apply (drule_tac x =  "x" in spec)
       using F apply simp
       apply safe
       by (simp add: xx_def)
       
       
     from U show "S N (y 0)"
       apply (simp)
       by (simp add: xx_def)
   next
     fix x::"nat ⇒ 'z"
     assume A: "∀x xN y. P N (x(N := xN)) ∧ y 0 = xN ∧ ZZ (Q' N x) (Q N y) ∧ R N x ⟶ S N xN"
     assume "inv_top (Suc N) (P N)"
     assume "inv_top N (R N)"
     assume "inv_top N (Q' N)"
       
     assume [simp]: " P N x"
     assume [simp]: "ZZ (Q' N x) (Q N (x[N ..]))"
     assume [simp]: "R N x"
       
     from A show "S N (x N)"
       apply (drule_tac x = x in spec)
       apply (drule_tac x = "x N" in spec)
       apply (drule_tac x = "x[N..]" in spec)
       by simp
         
   qed
    
lemma prec_pre_sts_reach: "⋀ x . prec_pre_sts init p r x = (∀ s n. (∃ y . reach init r n x y s) ⟶ p (s n, x n))"
  by (simp add: prec_pre_sts_simp reach_def, blast)
       
lemma prec_pre_sts_bound_simp: "⋀ N x . prec_pre_sts_bound init p r N x = 
      (∀u n. (n < N ∧ init (u 0) ∧ ((∃ y . ∀i<n . r (u i, x i) (u (Suc i), y i)))) ⟶ (∀ k ≤ n . p (u k, x k)))"
   proof (unfold  prec_pre_sts_bound_def, safe)
     fix N x u n k y
     assume A: "∀u. init (u 0) ⟶ (∀y n. n < N ⟶ (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))"
     assume B: "n < N"
     assume C: "init (u (0::nat)) "
     assume D: " ∀i<n. r (u i, x i) (u (Suc i), y i)"
     assume E: "k ≤ n"
       
     from D have "(∀i<n. r (u i, x i) (u (Suc i), y i))"
       by blast

     from this and E  have "(∀i < k. r (u i, x i) (u (Suc i), y i))"
       using less_le_trans by blast
         
     from this and  A and C and B and E show "p (u k, x k)"
       by auto
         
   next
     fix N x u y n
     assume A: "∀u n. n < N ∧ init (u 0) ∧ (∃y. ∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ (∀k≤n. p (u k, x k))"
     assume B: "init (u (0::nat)) "
     assume C: "n < N"
     assume D: "∀i<n. r (u i, x i) (u (Suc i), y i)"
       
     from A B C D show  "p (u n, x n)"
       by blast
   qed

lemma prec_pre_sts_bound: "⋀ x N . prec_pre_sts init p r x = (prec_pre_sts_bound init p r N x 
    ∧ (∀ s y . reach init r N x y s ⟶  prec_pre_sts (λ u . u = s N) p r (x[N..])))"
   proof (simp add: prec_pre_sts_simp prec_pre_sts_bound_def, safe)
     fix x N u y v n
     assume A: "∀u. init (u 0) ⟶ (∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))"
     assume C: " init (u (0::nat))"
     assume B: "∀i<n. r (u i, x i) (u (Suc i), y i)"
     from A and C have "(∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))"
       by blast

     from this and B show "p (u n, x n)"
       by blast
       
   next
     fix x N s y u ya n
     assume A: "∀u. init (u 0) ⟶ (∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n)) "
     assume B: "reach init r N x y s"
     assume F: "u (0::nat) = s N"
     assume C: " ∀i<n. r (u i, x (N + i)) (u (Suc i), ya i)"
       
         
     from B have E: "init (s 0) ∧ (∀ i < N . r (s i, x i) (s (Suc i), y i))"
       by (simp add: reach_def)
         
     define uu where "uu = cat N s u"
       
     define yy where "yy = cat N y ya"
       
     have "init (uu 0)"
       apply (simp add: uu_def, safe)
       using E apply blast
       using F and E by simp
         
     from this and A have G: "((∀i<N + n. r (uu i, x i) (uu (Suc i), yy i)) ⟹ p (uu (N + n), x (N + n)))"
       by blast
       
         
     have "(∀i<N + n. r (uu i, x i) (uu (Suc i), yy i))"
       apply (simp add: uu_def yy_def, safe)
       apply (cut_tac E) apply (safe)
         apply (drule_tac x = i in spec, simp)
        apply (case_tac "N = Suc i", simp_all)
         apply (cut_tac E, safe)
        apply (drule_tac x = i in spec, simp)
       using F apply simp
       using C apply (drule_tac x = "i - N" in spec)
       apply safe
        apply simp_all
         by (simp add: Suc_diff_le)
         
         
         
       from this and G have "p (uu (N + n), x (N + n))"
         by simp
         
       from this show "p (u n, x (N + n))"
         by (simp add: uu_def)
           
     next
       fix x N u y n
       assume A: "∀u. init (u 0) ⟶ (∀y n. n < N ⟶ (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))"
       assume B: " ∀s. (∃y. reach init r N x y s) ⟶ (∀u. u 0 = s N ⟶ (∀y n. (∀i<n. r (u i, x (N + i)) (u (Suc i), y i)) ⟶ p (u n, x (N + n)))) "
       assume C: "init (u (0::nat))"
       assume D: "∀i<n. r (u i, x i) (u (Suc i), y i)"
         
       from B have F: "⋀ ua y n . (∃y. reach init r N x y u) ⟹ (ua 0 = (u N) ⟹ (∀i<n. r (ua i, x (N + i)) (ua(Suc i), y i) ⟹ p (ua n, x (N + n))))"
         by blast
         
       from A have E: "⋀ n . n < N ⟹ ((∀i<n. r (u i, x i) (u (Suc i), y i)) ⟹ p (u n, x n))"
         using C by simp
         
       show "p (u n, x n)"
         proof (cases "n < N")
           case True
           then show ?thesis
             apply (rule_tac E, simp_all)
             using D by simp
               
         next
           case False
           define uu where "uu = u[N..]"
           define yy where "yy = y[N..]"
           from False have H: "N ≤ n"
             by auto
               
           from this have "(∃y. reach init r N x y u)"
             apply (rule_tac x = y in exI)
             using C and D by (simp add: reach_def)

               
           from this and F have U: "(uu 0 = (u N) ⟹ (∀i< (n - N). r (uu i, x (N + i)) (uu(Suc i), yy i) ⟹ p (uu (n - N), x (N + (n -N)))))"
             by simp
               
           have [simp]: "uu 0 = (u N)"
             by (simp add: uu_def)
           from H have [simp]: "∀i< (n - N). r (uu i, x (N + i)) (uu(Suc i), yy i)"
             using D by (simp add: uu_def yy_def)
               
           from U have " p (uu (n - N), x (N + (n -N)))"
             by simp
             
             
           then show ?thesis
             using H by (simp add: uu_def)
         qed
         
       
       qed

lemma AA: "⋀ t x N y . ((prec_pre_sts init p r x ∧ reach init' r' N x y t) ⟶ p' (t N, x N))
    = ((prec_pre_sts_bound init p r N x ∧ (∀ s y . reach init r N x y s ⟶  prec_pre_sts (λ u . u = s N) p r (x[N..])) ∧ reach init' r' N x y t) ⟶ p' (t N, x N))"
  by (cut_tac x = x and N = N and p = p and r = r and init = init in prec_pre_sts_bound, simp)

lemma [simp]: "inv_top (Suc N) (prec_pre_sts_bound init p r N)"
  by (simp add: inv_top_def prec_pre_sts_bound_def fun_eq_iff)
    
lemma [simp]: "inv_top N (λx. ∃y. reach init' r' N x y t)"
  by (simp add: inv_top_def fun_eq_iff reach_def)
    
lemma [simp]: " inv_top N (λx s. ∃y. reach init r N x y s)"
  by (simp add: inv_top_def fun_eq_iff reach_def)
    
lemma sts_refinement_A_bounded: "(∀ x y . (prec_pre_sts init p r x ∧ reach init' r' N x y t) ⟶ p' (t N, x N))
    = (∀ xN . (∃ x . prec_pre_sts_bound init p r N (x(N := xN)) 
        ∧ (∃ xz . xz 0 = xN ∧ (∀ s y . reach init r N x y s ⟶  prec_pre_sts (λ u . u = s N) p r xz)) 
        ∧ (∃ y . reach init' r' N x y t)) 
          ⟶ p' (t N, xN))"
   proof (simp add: AA, safe)
     fix t x y xz
     assume A: "∀x. prec_pre_sts_bound init p r N x ∧ (∀s. (∃y. reach init r N x y s) ⟶ prec_pre_sts (λu. u = s N) p r (x[N ..])) ∧ (∃y. reach init' r' N x y t) ⟶ p' (t N, x N)"
     assume B: "prec_pre_sts_bound init p r N (x(N := xz (0::nat)))"
     assume C: "∀s. (∃y. reach init r N x y s) ⟶ prec_pre_sts (λu. u = s N) p r xz"
     assume D: "reach init' r' N x y t"
     thm replace_variables
       
     have "(∀x. prec_pre_sts_bound init p r N x ∧ (∀s. (∃y. reach init r N x y s) ⟶ prec_pre_sts (λu. u = s N) p r (x[N ..])) ∧ (∃y. reach init' r' N x y t) ⟶ p' (t N, x N))
        = ((∀x xN. prec_pre_sts_bound init p r N (x(N := xN)) ∧ (∃y. y 0 = xN ∧ (∀s. (∃y. reach init r N x y s) ⟶ prec_pre_sts (λu. u = s N) p r y) ∧ (∃y. reach init' r' N x y t)) ⟶ p' (t N, xN)))"
       apply (cut_tac P = "λ N x . prec_pre_sts_bound init p r N x" and N = N
            and Q = "λ N y s . prec_pre_sts (λu. u = s N) p r (y)" 
            and Q' = "λ N x s . ∃y. reach init r N x y s"
            and ZZ = "(λ A B . ∀ s . A s ⟶ B s)" 
            and R = "λ N x . (∃y. reach init' r' N x y t)" 
            and S = "λ N x . p' (t N, x)" in replace_variables)
          by simp_all
         
        from A this have "⋀x xN. prec_pre_sts_bound init p r N (x(N := xN)) ⟹ (∃y. y 0 = xN ∧ (∀s. (∃y. reach init r N x y s) 
            ⟶ prec_pre_sts (λu. u = s N) p r y) ∧ (∃y. reach init' r' N x y t)) ⟹ p' (t N, xN)"
          by simp
            
        from this have "prec_pre_sts_bound init p r N (x(N := xz 0)) ⟹ (∃y. y 0 = xz 0 ∧ (∀s. (∃y. reach init r N x y s)
            ⟶ prec_pre_sts (λu. u = s N) p r y) ∧ (∃y. reach init' r' N x y t)) ⟹ p' (t N, xz 0)"
          by simp
            
        from this have U: " (∃y. y 0 = (xz 0) ∧ (∀s. (∃y. reach init r N x y s) 
            ⟶ prec_pre_sts (λu. u = s N) p r y) ∧ (∃y. reach init' r' N x y t)) ⟹ p' (t N, (xz 0))"
          by (simp add: B)

          from C D have "(∃y. y 0 = (xz 0) ∧ (∀s. (∃y. reach init r N x y s) 
            ⟶ prec_pre_sts (λu. u = s N) p r y) ∧ (∃y. reach init' r' N x y t))"
            by (rule_tac x = xz in exI, simp, blast)
              
          from this and U show "p' (t N, (xz 0))"
            by simp
 
   next
     fix t x y
     assume A: "∀xN. (∃x. prec_pre_sts_bound init p r N (x(N := xN)) ∧ 
              (∃xz. xz 0 = xN ∧ (∀s. (∃y. reach init r N x y s) ⟶ prec_pre_sts (λu. u = s N) p r xz)) ∧ (∃y. reach init' r' N x y t)) ⟶
                p' (t N, xN)"
     assume B: "prec_pre_sts_bound init p r N x"
     assume C: "∀s. (∃y. reach init r N x y s) ⟶ prec_pre_sts (λu. u = s N) p r (x[N ..])"
     assume D: "reach init' r' N x y t"
         
     from A have  E: "(∃xx. prec_pre_sts_bound init p r N (xx(N := x N)) ∧
                       (∃xz. xz 0 = x N ∧ (∀s. (∃y. reach init r N xx y s) ⟶ prec_pre_sts (λu. u = s N) p r xz)) ∧ (∃y. reach init' r' N xx y t)) ⟹
                  p' (t N, x N)"
       by blast
           
       have "(∃xx. prec_pre_sts_bound init p r N (xx(N := x N)) ∧
                       (∃xz. xz 0 = x N ∧ (∀s. (∃y. reach init r N xx y s) ⟶ prec_pre_sts (λu. u = s N) p r xz)) ∧ (∃y. reach init' r' N xx y t))"
         apply (rule_tac x = x in exI, simp, safe)
         using B apply simp
          apply (rule_tac x = "x[N..]" in exI, simp)
         using C apply simp
         using D by blast

       from this show "p' (t N, x N)"
         by (rule E)
     qed

lemma reach_until: "(∃ x s y n. reach init r n x y s ∧ s n = t) 
    = (∃ sa . init (sa 0) ∧ ((λ sa . (∃ x y . r (sa 0, x) (sa (Suc 0), y))) until (λ sa . sa 0 = t)) sa)"
  apply (simp add: reach_def until_def at_fun_def, auto)
   apply blast
  apply (simp add: choice_iff', safe)
  by blast

lemma LocalSystem_prec_top: "LocalSystem init ⊤ r = [: rel_pre_sts init r:]"
  by (simp add: LocalSystem_simp assert_true_skip skip_comp)


lemma LocalSystem_input_complete: "(LocalSystem init p r = [:rel_pre_sts init r:])
  = ((∀ x s . init s ⟶ p (s,x)) ∧ 
      (∀ s s' x x' y n . 
      (∃ x y . reach init r n x y s) ∧ p (s n, x) ∧ r (s n,x) (s', y) ⟶ p (s', x')))"
proof (simp add: LocalSystem_simp assert_demonic_eq_demonic, safe)
  fix s x
  assume [simp]: "init s"
  assume A: "∀x. prec_pre_sts init p r x"
  show "p (s, x)"
    using A apply (drule_tac x = "λ i . x" in spec)
    apply (simp add: prec_pre_sts_simp)
    apply (drule_tac x = "λ i . s" in spec)
    apply (simp add: fun_eq_iff)
    by blast

next
  fix s s' x x' y xa ya n
  assume A: " ∀x. prec_pre_sts init p r x"
  assume "p (s (n::nat), x)"
  assume W: "r (s n, x) (s', y)"
  assume "reach init r n xa ya s"
  from this have [simp]: "init (s 0) " and V: " ⋀ i . i < n ⟹ r (s i, xa i) (s (Suc i), ya i)"
    by (simp_all add: reach_def)
  define xb where "xb = (λ i . if i < n then xa i else (if i = n then x else x'))"
  define yb where "yb = (λ i . if i < n then ya i else y)"
  define sb where "sb = (λ i . if i ≤ n then s i else s')"
    
  have [simp]: "init (sb 0)"
    by (simp add: sb_def)
      
  from A have "prec_pre_sts init p r xb"
    by simp

  from this have X: "(∀i < (Suc n). r (sb i, xb i) (sb (Suc i), yb i)) ⟹ p (sb (Suc n), xb (Suc n)) "
    by (simp add: prec_pre_sts_simp)
    
  have [simp]: "⋀ i . i < (Suc n) ⟹ r (sb i, xb i) (sb (Suc i), yb i)"
    apply (simp add: sb_def xb_def yb_def)
    using V W less_antisym by blast
      
  from X show "p (s', x')"
    apply simp
    by (simp add: sb_def xb_def)

next
  fix x 
  assume A: "∀x s. init s ⟶ p (s, x)"
  assume B: "∀s s'. (∃x y n. (∃x y. reach init r n x y s) ∧ p (s n, x) ∧ r (s n, x) (s', y)) ⟶ (∀x'. p (s', x'))"
  show " prec_pre_sts init p r x"
  proof (simp add: prec_pre_sts_simp, safe)
    fix u y n
    assume C: "init (u (0::nat))"
    from A and C have [simp]: "⋀ x . p (u 0, x)"
      by simp
    show "∀i<n. r (u i, x i) (u (Suc i), y i) ⟹ p (u n, x n)"
      proof (induction n)
        case 0
        then show ?case by simp
      next
        case (Suc n)
        from this have U: "p (u n, x n)"
          by auto

        from Suc(2) have V: "r (u n, x n) (u (Suc n), y n)"
          by blast

        have W: "(∃x y . reach init r n x y u)"
          apply (rule_tac x = x in exI)
          apply (rule_tac x = y in exI)
          apply (simp add: reach_def)
          using Suc(2) and C by simp
            
        from B have D: "(∃x y . reach init r n x y u) ⟹ (p (u n, x n) ∧ (r (u n, x n) (u (Suc n), y n))) ⟹  p (u (Suc n), x (Suc n))"
          by blast

        from U V W D show ?case
          by simp
      qed
  qed
qed

end