Theory InstantaneousFeedback

(**-----------------------------------------------------------------------------
 * © [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.
 *)

section‹\label{InstFeedback}Instantaneous Feedback›

theory InstantaneousFeedback imports "../RefinementReactive/Refinement"
begin

  datatype 'a fail_option = Fail ("∙") | OK (elem :'a)

  class order_bot_max = order_bot +
    fixes maximal :: "'a ⇒ bool"
    assumes maximal_def: "maximal x = (∀ y . ¬ x < y)"
    assumes [simp]: "¬ maximal ⊥"
    begin
      lemma ex_not_le_bot[simp]: "∃ a. ¬ a ≤ ⊥"
        apply (subgoal_tac "¬ maximal ⊥")
        apply (subst (asm) maximal_def, simp_all add: less_le, auto)
        apply (rule_tac x = x in exI, auto)
        apply (subgoal_tac "x = ⊥", simp)
        by (rule antisym, simp_all)
    end

  instantiation "option" :: (type) order_bot_max
    begin
      definition bot_option_def: "(⊥::'a option) = None"
      definition le_option_def: "((x::'a option) ≤ y) = (x = None ∨ x = y)"
      definition less_option_def: "((x::'a option) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
      definition maximal_option_def: "maximal (x::'a option) = (∀ y . ¬ x < y)"

      instance 
      proof
        qed (auto simp add: le_option_def less_option_def maximal_option_def bot_option_def)

     lemma [simp]: "None ≤ x"
      by (subst bot_option_def [THEN sym], simp)
    end

  context order_bot
    begin
      definition "is_lfp f x = ((f x = x) ∧ (∀ y . f y = y ⟶ x ≤ y))"
      definition "emono f = (∀ x y. x ≤ y ⟶ f x ≤ f y)"

      definition "Lfp f = Eps (is_lfp f)"

      lemma lfp_unique: "is_lfp f x ⟹ is_lfp f y ⟹ x = y"
        apply (simp add: is_lfp_def)
        by (simp add: local.antisym)

      lemma lfp_exists: "is_lfp f x ⟹ Lfp f = x"
        apply (rule lfp_unique, simp_all)
        by (simp add: Lfp_def someI)
  
      lemma emono_a: "emono f ⟹ x ≤ y ⟹ f x ≤ f y"
        by (simp add: emono_def)

      lemma emono_fix: "emono f ⟹ f y = y ⟹ (f ^^ n) ⊥ ≤ y"
        apply (induction n)
        apply (simp_all)
        apply (drule emono_a, simp_all)
        by simp

      lemma emono_is_lfp: "emono (f::'a ⇒ 'a) ⟹ (f ^^ (n + 1)) ⊥ = (f ^^ n) ⊥ ⟹ is_lfp f ((f ^^ n) ⊥)"
        apply (simp add: is_lfp_def, safe)
        by (rule emono_fix, simp_all)

      lemma emono_lfp_bot: "emono (f::'a ⇒ 'a) ⟹ (f ^^ (n + 1)) ⊥ = (f ^^ n) ⊥ ⟹ Lfp f = ((f ^^ n) ⊥)"
        apply (drule emono_is_lfp, simp_all)
        by (simp add: lfp_exists)


      lemma emono_up: "emono f ⟹ (f ^^ n) ⊥ ≤ (f ^^ (Suc n)) ⊥"
        apply (induction n)
        apply (simp_all)
        by (drule emono_a, simp_all)
    end

   context order
    begin
       definition "min_set A = (SOME n . n ∈ A ∧ (∀ x ∈ A . n ≤ x))"
    end

   lemma min_nonempty_nat_set_aux: "∀ A . (n::nat) ∈ A ⟶ (∃ k ∈ A . (∀ x ∈ A . k ≤ x))"
     apply (induction n, safe)
     apply (rule_tac x = 0 in bexI, simp_all)
     apply (case_tac "0 ∈ A")
     apply (rule_tac x = 0 in bexI, simp_all)
     apply (drule_tac x = "{n . Suc n ∈ A}" in spec)
     apply safe
     apply (rule_tac x = "Suc k" in bexI, simp_all, safe)
     apply (drule_tac x = "x - 1" in spec)
     by (case_tac x, simp_all)

   lemma min_nonempty_nat_set: "(n::nat) ∈ A ⟹ (∃ k . k ∈ A ∧ (∀ x ∈ A . k ≤ x))"
     by (cut_tac min_nonempty_nat_set_aux, auto)

  thm someI_ex

  lemma min_set_nat_aux: "(n::nat) ∈ A ⟹ min_set A ∈ A ∧ (∀ x ∈ A . min_set A ≤ x)"
    apply (simp add: min_set_def)
    apply (drule min_nonempty_nat_set)
    by (rule someI_ex, simp_all)

  lemma "(n::nat) ∈ A ⟹ min_set A ∈ A ∧ min_set A ≤ n"
    by (simp add: min_set_nat_aux)
    
  lemma min_set_in: "(n::nat) ∈ A ⟹ min_set A ∈ A"
    by (simp add: min_set_nat_aux)

  lemma min_set_less: "(n::nat) ∈ A ⟹ min_set A ≤ n"
    by (simp add: min_set_nat_aux)



  class fin_cpo = order_bot_max +
    
    assumes fin_up_chain: "(∀ i:: nat . a i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
    begin
      lemma emono_ex_lfp: "emono f ⟹ ∃ n . is_lfp f ((f ^^ n) ⊥)"
        apply (cut_tac a = "λ i . (f ^^ i) ⊥" in fin_up_chain)
        apply (safe, rule emono_up, simp)
        apply (rule_tac x= n in exI)
        apply (rule emono_is_lfp, simp)
        by (drule_tac x = "n + 1" in spec, simp)

      lemma emono_lfp: "emono f ⟹ ∃ n . Lfp f = (f ^^ n) ⊥"
        apply (drule emono_ex_lfp, safe)
        apply (rule_tac x = n in exI)
        by (rule lfp_exists, simp)

      lemma emono_is_lfp: "emono f ⟹ is_lfp f (Lfp f)"
        apply (drule emono_ex_lfp, safe)
        by (frule lfp_exists, simp)

      definition "lfp_index (f::'a ⇒ 'a) = min_set {n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}"

      lemma lfp_index_aux: "emono f ⟹ (∀ i < (lfp_index f) . (f ^^ i) ⊥ < (f ^^ (i + 1)) ⊥) ∧ (f ^^ (lfp_index f)) ⊥ = (f ^^ ((lfp_index f) + 1)) ⊥"
        apply (simp add: lfp_index_def)
        apply safe
        apply (simp add: less_le_not_le, safe)
        apply (cut_tac n = i in emono_up, simp_all)
        apply (cut_tac n = i and A = "{n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}" in min_set_less, simp)
        apply (rule antisym, simp_all)
        apply (cut_tac n = i in emono_up, simp_all)
        apply (cut_tac a = "λ i . (f ^^ i) ⊥" in fin_up_chain, simp, safe)
        apply (drule emono_up, simp)
        apply (cut_tac n = "n" and A = "{n . (f ^^ n) ⊥ = (f ^^ (n + 1)) ⊥}" in min_set_in)
        apply (drule_tac x = "Suc n" in spec, simp)
        by simp

      lemma [simp]: "emono f ⟹ i < lfp_index f ⟹ (f ^^ i) ⊥ < f ((f ^^ i) ⊥)"
        by (drule lfp_index_aux, simp)

      lemma [simp]: "emono f ⟹ f ((f ^^ (lfp_index f)) ⊥) = (f ^^ (lfp_index f)) ⊥"
        by (drule lfp_index_aux, simp)

      lemma [simp]: "emono f ⟹ Lfp f = (f ^^ lfp_index f) ⊥"
        by (rule emono_lfp_bot, simp_all)


    end

  declare [[show_types]]
  instantiation "option" :: (type) fin_cpo
    begin
      lemma fin_up_non_bot: "(∀ i . (a::nat ⇒ 'a option) i ≤ a (Suc i)) ⟹ a n ≠ ⊥ ⟹ n ≤ i ⟹ a i = a n"
        apply (induction i, simp_all)
        apply (case_tac "n ≤ i", simp_all)
        apply (drule_tac x = i in spec)
        apply (simp add: le_option_def bot_option_def, safe, simp_all)
        using le_Suc_eq by blast

     lemma fin_up_chain_option: "(∀ i:: nat . (a::nat ⇒ 'a option) i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
      apply (case_tac "∃ n .  a n ≠ ⊥", safe, simp_all)
      apply (rule_tac x = n in exI, safe)
      by (rule fin_up_non_bot, simp_all)
      
    instance
      proof
        qed (simp add: fin_up_chain_option)
    end

  instantiation "prod" :: (order_bot_max, order_bot_max) order_bot_max
    begin
      definition bot_prod_def: "(⊥ :: 'a × 'b) = (⊥, ⊥)"
      definition le_prod_def: "(x ≤ y) = (fst x ≤ fst y ∧ snd x ≤ snd y)"
      definition less_prod_def: "((x::'a×'b) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
      definition maximal_prod_def: "maximal (x::'a × 'b) = (∀ y . ¬ x < y)"

      instance proof
        qed (auto simp add: le_prod_def less_prod_def bot_prod_def maximal_prod_def)
    end

  instantiation "prod" :: (fin_cpo, fin_cpo) fin_cpo
    begin
      
      lemma fin_up_chain_prod: "(∀ i:: nat . (a::nat ⇒ 'a × 'b) i ≤ a (Suc i)) ⟹ ∃ n . ∀ i ≥ n . a i = a n"
        apply (cut_tac a = "fst o a" in fin_up_chain)
        apply (simp add: le_prod_def)
        apply (cut_tac a = "snd o a" in fin_up_chain)
        apply (simp add: le_prod_def)
        apply safe
        apply (rule_tac x = "max n na" in exI)
        by (metis (no_types, hide_lams) comp_apply max.bounded_iff max.cobounded1 max.cobounded2 prod.collapse)
      instance proof
        qed (auto simp add: fin_up_chain_prod)
    end

  instantiation "fail_option" :: (order_bot) "{order_bot, order_top}"
    begin
      definition bot_fail_option_def: "(⊥::'a fail_option) = OK ⊥"
      definition top_fail_option_def: "(⊤::'a fail_option) = ∙"
      definition le_fail_option_def: "((x::'a fail_option) ≤ y) = ((case x of OK a ⇒ (case y of OK b ⇒ a ≤ b | ∙ ⇒ True) | ∙ ⇒ y = ∙))"
      definition less_fail_option_def: "((x::'a fail_option) < y) = (x ≤ y ∧ ¬ (y ≤ x))"
      instance 
      proof
        qed (auto simp add: le_fail_option_def less_fail_option_def top_fail_option_def bot_fail_option_def, case_tac x, simp_all, case_tac x, simp_all
            , case_tac y, simp_all, case_tac z, simp_all, case_tac x, simp_all, case_tac y, simp_all, case_tac a, simp_all, case_tac a, simp_all)
    end

  lemma maximal_prod_1: "maximal (a, b) ⟹ maximal a"
    by (simp add: maximal_def less_prod_def le_prod_def less_le_not_le, auto)

  lemma maximal_prod_2: "maximal (a, b) ⟹ maximal b"
    by (simp add: maximal_def less_prod_def le_prod_def less_le_not_le, auto)

  lemma maximal_prod: "maximal (a, b) = (maximal a ∧ maximal b)"
    by (simp add: maximal_def less_prod_def le_prod_def less_le_not_le, auto)


  lemma drop_assumption: "p ⟹ True"
    by simp

  lemma Sup_OO: "(Sup A) OO r = Sup {x . ∃ y∈A . x = y OO r}"
    apply (simp add: fun_eq_iff OO_def, safe)
    apply auto
    apply (rule_tac x = "f OO r" in exI, safe)
    apply (rule_tac x = f in bexI) 
    apply (simp_all add: OO_def)
    by auto

  lemma OO_Sup: "r OO (Sup A) = Sup {x . ∃ y∈A . x = r OO y}"
    apply (simp add: fun_eq_iff OO_def, safe)
    apply auto
    apply (rule_tac x = "r OO f" in exI, safe)
    apply (rule_tac x = f in bexI) 
    apply (simp_all add: OO_def)
    by auto

  lemma OO_SUP: "r OO (SUP n . A n) = (SUP n . r OO (A n))"
    apply (simp add: fun_eq_iff OO_def, safe)
    by auto

  lemma SUP_OO: "(SUP n . A n) OO r = (SUP n . (A n) OO r)"
    apply (simp add: fun_eq_iff OO_def, safe)
    by auto

  definition "InstFeedback r = (λ x uy . case x of ∙ ⇒ uy = ∙ | OK z ⇒ 
    (∃ n a .  (a 0 = ⊥) ∧ (∀ i < n . a i < a (Suc i)) ∧ (∀ i < n . ∃ y . r (OK (a i, z)) (OK (a (Suc i), y))) ∧
       ((∃ y . r (OK (a n, z)) (OK (a (Suc n), y)) ∧ a n = a (Suc n) ∧ uy = OK (a (Suc n), y)) ∨ 
       (r (OK (a n, z)) ∙ ∧ uy = ∙)) ))"

  lemma InstFeedback_alt: "InstFeedback r =  (λ x uy . case x of ∙ ⇒ uy = ∙ | OK z ⇒ 
    (∃ n a .  (a 0 = ⊥) ∧ (∀ i < n . a i < a (Suc i) ∧ (∃ y . r (OK (a i, z)) (OK (a (Suc i), y)))) ∧
       r (OK (a n, z)) uy ∧ (∃ y . uy = OK (a n, y) ∨ uy = ∙) ))"
    apply (simp add: InstFeedback_def fun_eq_iff,safe)
    apply (case_tac x, simp_all, safe, simp_all)
    apply (rule_tac x = n in exI)
    apply (rule_tac x = a in exI, simp)
    apply (rule_tac x = n in exI)
    apply (rule_tac x = a in exI, simp)
    apply (case_tac x, simp_all, safe, simp_all)
    apply (rule_tac x = n in exI)
    apply (rule_tac x = "λ i. if i ≤ n then a i else a n" in exI, simp_all)
    apply (rule_tac x = n in exI)
    by (rule_tac x = a in exI, simp)

  definition "functional r f g = (∀ u x z . r (OK (u, x)) z = (z = OK(f x u, g x u)))"

  lemma chain_power: "a 0 = b ⟹ ∀i≤n. a (Suc i) = f (a i) ⟹ i ≤ Suc n ⟹ a i = (f ^^ i) b"
    by (induction i, simp_all)

  theorem InstFeedback_constructive: "emono ((f x)::'a::fin_cpo ⇒ 'a) ⟹ functional r f g ⟹ 
            (InstFeedback r (OK x) uy) = (uy = OK (Lfp (f x), g x (Lfp (f x))))"
    apply (simp add: InstFeedback_def functional_def)
    apply safe
    apply simp_all
    apply (subgoal_tac "∀ i ≤ Suc n . a i = ((f x) ^^ i) ⊥")
    apply simp
    apply (cut_tac f = "f x" and n = n in emono_lfp_bot, simp_all)
    apply safe
    apply (rule chain_power, simp_all, safe)
    apply (case_tac "ia = n", simp_all)
    apply (subgoal_tac "a (Suc n) = Lfp (f x)", simp_all)
    apply (subgoal_tac "∀ i ≤ Suc n . a i = ((f x) ^^ i) ⊥")
    apply simp
    apply (cut_tac f = "f x" and n = n in emono_lfp_bot, simp_all)
    apply safe
    apply (rule chain_power, simp_all, safe)
    apply (case_tac "ia = n", simp_all)
    apply (rule_tac x = "lfp_index (f x)" in exI)
    apply (rule_tac x = "λ i . ((f x) ^^ i) ⊥" in exI)
    by simp

  definition "InstFeedback_1 r = (λ x uy . case x of ∙ ⇒ uy = ∙ | OK z ⇒ 
    (∃ a . ⊥ < a ∧ (∃ y . r (OK (⊥, z)) (OK (a, y))) ∧ r (OK (a, z)) uy ∧ (∃ y . uy = OK (a, y) ∨ uy = ∙) ) 
      ∨ (r (OK (⊥, z)) uy ∧ (∃ y . uy = OK (⊥, y) ∨ uy = ∙)))"


  lemma [simp]: "(⊥ < (a::'a::order_bot)) = (⊥ ≠ a)"
     apply (simp add: less_le_not_le, auto)
     by (rule antisym, simp_all)

  definition "unkn_mono r = (∀ a b x . (a::'a::order_bot) ≤ b ⟶ (∀ z . r (OK (b, x)) (OK z) ⟶ r (OK (a, x)) (OK z)))"

  lemma unkn_mono_fb_fun: "unkn_mono r ⟹ InstFeedback_1 r = InstFeedback r"
    apply (simp add: InstFeedback_1_def InstFeedback_alt fun_eq_iff, safe)
    apply (case_tac x, simp_all)
    apply safe
    apply simp_all
    apply (rule_tac x = "Suc 0" in exI)
    apply (rule_tac x = "λ i . if i = 0 then ⊥ else a" in exI, simp_all)
    apply auto [1]
    apply (rule_tac x = "Suc 0" in exI)
    apply (rule_tac x = "λ i . if i = 0 then ⊥ else a" in exI, simp_all)
    apply auto [3]
    apply (case_tac x, simp_all, safe, simp_all)
    apply safe
    apply (simp add: unkn_mono_def)
    apply simp
    apply (simp add: unkn_mono_def)
    apply (drule_tac x = y in spec)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = "a n" in spec)
    apply auto [1]
    apply simp
    apply (simp add: unkn_mono_def)
    apply (drule_tac x = y in spec)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = "a n" in spec)
    apply auto [1]
    apply (case_tac n, simp_all)
    apply (drule_tac x = "a (Suc nat)" in spec, simp)
    apply (drule_tac x = nat in spec, simp_all, safe)
    apply auto [1]
    apply (simp add: unkn_mono_def)
    apply (drule_tac x = y in spec)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = "a nat" in spec)
    by auto

  definition "fb_begin =  (λ x ux . ux = (case x of ∙ ⇒ ∙ | OK x ⇒ OK (⊥, x)))"

  definition "fb_a r = (λ ux ux' . (case ux of  ∙ ⇒ ux' = ∙ | OK (u, x) ⇒ 
         (r (OK (u, x)) ∙ ∧ ux' = ∙) ∨ (∃ u' y' . r (OK (u, x)) (OK (u', y')) ∧ u < u' ∧ ux' = OK (u', x))))"

  definition "fb_b r = (λ ux uy' . (case ux of  ∙ ⇒ uy' = ∙ | OK (u, x) ⇒ 
         (r (OK (u, x)) ∙ ∧ uy' = ∙) ∨ (∃ y' . r (OK (u, x)) (OK (u, y')) ∧ uy' = OK (u, y'))))"

  definition "fb_end = (λ uy y' . case uy of ∙ ⇒ y' = ∙ | OK (u, y) ⇒ (if maximal u then y' = OK y else y' = ∙))"

  definition "fb_hide r = (InstFeedback r) OO fb_end"

  definition "ff r = r ∙ ∙"
  definition "f_f r = (∀ x . r ∙ x ⟶ x = ∙)"

  lemma [simp]:"(case y of ∙ ⇒ ∙ = ∙ | OK (u, ya) ⇒ (maximal u ⟶ ∙ = OK ya) ∧ (¬ maximal u ⟶ ∙ = ∙)) = (∀ u x . y = OK (u, x) ⟶ ¬ maximal u)"
    by (case_tac y, simp_all, auto)

  lemma [simp]: "InstFeedback_1 r ∙ ∙"
    by (simp add: InstFeedback_1_def)

  lemma [simp]: "(case y of ∙ ⇒ ∙ = ∙ | OK (u, v, x) ⇒ ∙ = OK (v, u, x)) = (y = ∙)"
    by (case_tac y, auto)

  lemma case_b_simp: "(case b of ∙ ⇒ OK y = ∙ | OK (w, u, a) ⇒ OK y = OK ((u, w), a)) = (b ≠ ∙ ∧ (case b of OK (w, u, a) ⇒ y = ((u, w), a)))"
    by (case_tac b, simp_all)
  
  lemma [simp]: "(x::'a::order_bot) ≤ ⊥ ⟹ x = ⊥"
    by (rule antisym, simp_all)

  definition "mono_fail r = (∀a b x. a ≤ b ⟶ r (OK (a, x)) ∙ ⟶ r (OK (b, x)) ∙)"

lemma sconjunctive_comp_simp: "sconjunctive S ⟹ S ∘ (INF n::nat. T n) = (INF n . S o (T n))"
  apply (subst fun_eq_iff, simp, safe)
  apply (simp add: image_def)
    apply (subgoal_tac "T 0 x ∈ {y::'a. ∃xa::'c ⇒ 'a. (∃x::nat. xa = T x) ∧ y = xa x}")
   apply (simp only:  sconjunctive_simp)

   apply (simp_all add: INF_image, auto)
  apply (subgoal_tac "(S ` {y::'a. ∃xa::'c ⇒ 'a. (∃x::nat. xa = T x) ∧ y = xa x}) =
        {y::'b. ∃xa::'c ⇒ 'b. (∃x::nat. xa = S ∘ T x) ∧ y = xa x}")
   apply (auto simp add: image_def)
  by (rule_tac x = "T xc x" in exI, auto)

  lemma sconj_star_a: "sconjunctive S ⟹ (INF n::nat. S ^^ n) ≤ gfp (λX. Skip ⊓ (S ∘ X))"
    apply (rule gfp_upperbound, simp)
    apply (simp add: sconjunctive_comp_simp)
    apply safe
    apply simp_all
    apply (drule_tac x = 0 in spec, simp)
    apply (drule_tac x = "Suc xa" in spec)
    by simp

  lemma mono_comp_simp: "mono S ⟹ T ≤ T' ⟹ S o T ≤ S o T'"
    apply (simp add: le_fun_def, safe)
    by (drule monoE, simp_all)

  lemma sconj_star_b_aux: "mono S ⟹ u ≤ Skip ⟹ u ≤ S ∘ u ⟹ u ≤ S ^^ n"
    apply (induction n)
    apply (simp add: Skip_def)
    apply simp
    apply (rule_tac y = "S o u" in order_trans, simp)
    by (rule mono_comp_simp, simp_all)

  lemma sconj_star_b: "mono S ⟹ gfp (λX. Skip ⊓ (S ∘ X)) ≤ (INF n::nat. S ^^ n)"
    apply (rule gfp_least)
    apply (rule INF_greatest, simp)
    by (rule sconj_star_b_aux, simp_all)

  lemma sconj_star: "sconjunctive S ⟹ gfp (λX. Skip ⊓ (S ∘ X)) = (INF n::nat. S ^^ n)"
    apply (rule antisym)
    by (simp_all add: sconj_star_a sconj_star_b)

  lemma [simp]: "(case ya of ∙ ⇒ OK y = ∙ | OK z ⇒ p z) = (∃ z . ya = OK z ∧ p z)"
    by (case_tac ya, simp_all)

  lemma [simp]: "((p ⟶ q) ∧ p) = (p ∧ q)"
    by auto

  lemma relpowp_chain: "⋀ x y . (R ^^ n) x y = (∃ a . (∀ i < n . R (a i) (a (Suc i))) ∧ x = a 0 ∧ y = a n)"
    apply (induction n, simp_all, safe)
    apply (rule_tac x = "λ i . y" in exI, simp)
    apply (simp, safe)
    apply (rule_tac x = "λ i . if i ≤ n then a i else y" in exI, simp)
    apply safe
    apply (metis Suc_le_eq less_antisym)
    apply (simp add: OO_def)
    apply (rule_tac x = "a n" in exI, simp)
    by (rule_tac x = a in exI, simp)

  lemma [simp]: "fb_a r ∙ x = (x = ∙)"
    by (simp add: fb_a_def)

  lemma [simp]: "fb_a r (OK (u, x)) (OK (u', x')) = ((∃ y . r (OK (u, x)) (OK (u', y))) ∧ u < u' ∧ x = x')"
    by (auto simp add: fb_a_def)

  lemma [simp]: "fb_a r (OK ux) ∙ = r (OK ux) ∙"
    by (auto simp add: fb_a_def)

  lemma fb_a_id: "⋀ u x u' x' . (fb_a r ^^ n) (OK (u, x)) (OK (u', x')) ⟹ x = x'"
    apply (induction n, simp_all add: OO_def)
    apply auto
    apply (case_tac y, simp_all)
    by (case_tac x2, simp)

  lemma fb_a_id_a: "(∀i < n. fb_a r (a i) (a (Suc i))) ⟶ (∀ i ≤ n . a i ≠ ∙ ⟶ (snd (elem (a i))) = (snd (elem (a 0))))"
    apply (induction n, simp)
    apply safe
    apply auto [1]
    apply (case_tac "i = Suc n", simp_all)
    apply (drule_tac x = n in spec, simp)
    apply (drule_tac x = n in spec, simp, safe)
    apply (simp_all add: fb_a_def)
    apply (case_tac "a (n)", simp_all)
    by (case_tac x2, simp_all, safe, simp)

  lemma fb_a_id_b: "(∀i < n. fb_a r (a i) (a (Suc i))) ⟹ (∀ i ≤ n . a i ≠ ∙ ⟶ snd (elem (a i)) = snd (elem (a 0)))"
    by (cut_tac r = r and n = n and a = a in fb_a_id_a, safe)

  lemma [simp]: "x < y ⟹ x ≠ ∙"
    by (case_tac x, simp_all add: less_fail_option_def le_fail_option_def, auto)

  lemma [simp]: "⋀ x . ((fb_a r) ^^ n) ∙ x = (x = ∙)"
    apply (induction n, simp_all)
    apply auto [1]
    by (simp add: OO_def)

  lemma chain_fail: "⋀ k . ∀i < n. fb_a r (a i) (a (Suc i)) ⟹ k < n ⟹ a (Suc k) = ∙ ⟹ a n = ∙"
    apply (induction n, simp)
    apply (case_tac "k = n", simp)
    apply (subgoal_tac "a n = ∙", simp_all, auto)
    by (case_tac " k < n", simp_all)

  lemma [simp]: "OK x < ∙"
    by (simp add: less_fail_option_def le_fail_option_def)

  lemma chain_not_fail: "a 0 ≠ ∙ ⟹ ∀k. a (Suc k) = ∙ ⟶ k < n ⟶ (∃j ≤ k. a j = ∙) ⟹ (∀ i ≤ n . a i ≠ ∙)"
    apply (induction n)
    apply auto
    apply (case_tac "i = Suc n", simp_all)
    by (subgoal_tac "(∃j ≤ n. a j = ∙)", safe, simp_all)

  lemma [simp]: "fb_b r (OK (u, x)) (OK (u', y)) = (r (OK (u, x)) (OK  (u', y)) ∧ u = u')"
    by (auto simp add: fb_b_def)

  lemma [simp]: "fb_b r (OK (u, x)) ∙ = r (OK (u, x)) ∙"
    by (auto simp add: fb_b_def)

  lemma [simp]: "fb_b r ∙ x = (x = ∙)"
    by (auto simp add: fb_b_def)

  lemma chain_all_fail: "⋀ i . a (0::nat) = ∙ ⟹ ∀i < n. fb_a r (a i) (a (Suc i)) ⟹ i ≤ n ⟹ a i = ∙"
    apply (induction n, simp_all)
    apply (case_tac "i ≤ n", simp_all)
    by (case_tac "i = Suc n", simp_all)

  theorem InstFeedback_simp: "InstFeedback r = fb_begin OO ((fb_a r)^**) OO (fb_b r)"
    apply (simp add: rtranclp_is_Sup_relpowp)
    apply (simp add: OO_SUP SUP_OO InstFeedback_def)
    apply (simp add: fun_eq_iff OO_def rtranclp_is_Sup_relpowp)
    apply safe
    apply (case_tac x, simp_all)
    apply (rule_tac x = 0 in exI)
    apply (simp add: fb_begin_def)
    apply safe
    apply (simp add: relpowp_chain)
    apply (simp add: fb_begin_def)
    apply (rule_tac x = n in exI)
    apply (rule_tac x = "OK (a n, x2)" in exI, simp)
    apply (rule_tac x = "λ i . OK (a i, x2)" in exI, simp_all)

    apply (simp add: fb_begin_def)
    apply (simp add: relpowp_chain)
    apply (rule_tac x = n in exI)
    apply (rule_tac x = "OK (a n, x2)" in exI, simp)
    apply (rule_tac x = "λ i . OK (a i, x2)" in exI, simp_all)
(*<--*)
    apply (simp add: relpowp_chain, safe)
    apply (simp add: fb_begin_def)
    apply (case_tac "(∃ k < f . (a (Suc k) = ∙) ∧ (∀ j ≤ k . a j ≠ ∙))", simp_all, safe)
    apply (frule_tac fb_a_id_b)
    apply (case_tac x, simp_all)
    apply (rule_tac x = "k" in exI)
    apply (rule_tac x = "λ i . fst (elem (a i))" in exI, simp, safe, simp_all)
    apply (case_tac "a i", simp_all)
    apply (case_tac "a (Suc i)", simp_all)
    apply (drule_tac x = i in spec, simp_all)
    apply (case_tac x2a, case_tac x2b, simp_all)
    apply (case_tac "a i", simp_all)
    apply (case_tac "a (Suc i)", simp_all)
    apply (drule_tac x = i in spec, simp_all)
    apply (case_tac x2a, case_tac x2b, simp_all)
    apply auto [1]
    apply (drule_tac x = i in spec, simp_all)
    apply (drule_tac x = i in spec, simp_all)
    apply blast
    apply (case_tac "a k", simp_all)
    apply (case_tac x2a,  simp_all)
    apply (drule_tac x = k in spec, simp_all)
    apply (drule_tac x = k in spec, simp_all)
    apply (drule_tac x = k in spec, simp_all)
    apply (drule chain_fail, simp_all)
    apply (case_tac x, simp_all)
    apply (drule_tac n = f and r  = r and i = f in  chain_all_fail, simp_all)
    apply (cut_tac a = a and n = f in chain_not_fail, simp_all)
    apply (rule_tac x = f in exI)
    apply (frule_tac fb_a_id_b, simp_all)
    apply (case_tac xa, simp_all)
    apply (rule_tac x = "λ i . fst (elem (a i))" in exI, simp, safe, simp_all)
    apply (drule_tac x = i in spec, simp)
    apply (case_tac "a i", simp_all)
    apply (case_tac "a (Suc i)", simp_all)
    apply (case_tac x2a, case_tac x2b, simp_all)
    apply (drule_tac x = i in spec, simp)
    apply (case_tac "a i", simp_all)
    apply (case_tac "a (Suc i)", simp_all)
    apply (case_tac x2a, case_tac x2b, simp_all)
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply (drule_tac x = i in spec, simp)
    apply (drule_tac x = i in spec, simp)
    apply auto [1]
    apply (case_tac "a f", simp_all)
    apply (case_tac x2a, simp_all)
    apply (drule_tac x = f in spec, simp)
    apply (drule_tac x = f in spec, simp)
    apply (drule_tac x = f in spec, simp)
    apply (drule_tac x = f in spec, simp)
    apply (rule_tac x = "λ i . if i ≤ f then fst (elem (a i)) else aa" in exI, simp, safe)
    apply (drule_tac x = i in spec, simp)
    apply (case_tac "a i", simp_all)
    apply (case_tac "a (Suc i)", simp_all)
    apply (case_tac x2a, case_tac x2b, simp_all)
    apply (drule_tac x = i in spec, simp)
    apply (case_tac "a i", simp_all)
    apply (case_tac "a (Suc i)", simp_all)
    apply (case_tac x2a, case_tac x2b, simp_all)
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply (drule drop_assumption)
    apply (drule_tac x = i in spec, simp)
    apply (drule_tac x = i in spec, simp)
    apply auto [1]
    apply (case_tac "a f", simp_all)
    apply (case_tac x2a, simp_all, safe, simp)
    apply (drule_tac x = f in spec, simp)
    apply (drule_tac x = f in spec, simp)
    apply (drule_tac x = f in spec, simp)
    apply (drule_tac x = f in spec, simp)
    apply (case_tac "a f", simp_all)
    by (case_tac x2a, simp_all)

  lemma SUP_pointwise: "(∀ n . (S::'a ⇒ 'b::complete_lattice) n ≤ S' n) ⟹ (SUP n . S n) ≤ (SUP n . S' n)"
    apply (rule SUP_least, simp)
    apply (rule_tac y = "S' n" in order_trans, simp)
    by (rule SUP_upper, simp)

  lemma INF_pointwise: "(∀ n . (S::'a ⇒ 'b::complete_lattice) n ≤ S' n) ⟹ (INF n . S n) ≤ (INF n . S' n)"
    apply (rule INF_greatest, simp)
    apply (rule_tac y = "S n" in order_trans, simp_all)
    by (rule INF_lower, simp)


  definition "faila r x = ((r (OK x) ∙)::bool)"
  definition "rela r x y = (r (OK x) (OK y))"
  definition "preca r = -faila r"

  definition "wp r = {.preca r.} o [:rela r:]"

  lemma "(wp r ≤ wp r') = ((∀x . r' (OK x) ∙ ⟶ r (OK x) ∙) ∧ (∀x. ¬ r (OK x) ∙ ⟶ (∀y. r' (OK x) (OK y) ⟶ r (OK x) (OK y))))"
    apply (simp add: wp_def assert_demonic_refinement)
    by (simp add: le_fun_def preca_def faila_def rela_def, auto)

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

  thm fusion_spec

  thm Prod_spec_Skip

  lemma "wp (fb_a r) = Fb_a (wp r)"
    by (simp add: wp_def fun_eq_iff demonic_def assert_def le_fun_def preca_def faila_def 
      rela_def Fb_a_def fusion_spec_demonic Prod_spec_Skip)

  lemma "ff r ⟹ (wp r ≤ wp r') = (∀ x . r x ∙ ∨ r' x ≤ r x)"
    apply (simp add: wp_def assert_demonic_refinement)
    apply (simp add: le_fun_def preca_def faila_def rela_def, auto)
    apply (case_tac x, auto)
    apply (simp add: ff_def)
    by (case_tac xa, simp_all)

  lemma [simp]: "preca (=) = ⊤"
    by (simp add: fun_eq_iff preca_def faila_def)

  lemma [simp]: "(rela (=)) = (=)"
    by (simp add: fun_eq_iff rela_def)

  lemma [simp]: "wp (=) = Skip"
    by (simp add: wp_def assert_true_skip demonic_eq_skip)

  lemma "mono (wp r)"
    by (simp add: wp_def)

  definition "serial r r' = (r OO r')"

  lemma pred_bot_comp: "ff r ⟹ ff r' ⟹  preca (r OO r') = (λx. preca r x ∧ (∀y. rela r x y ⟶ preca r' y))"
    apply (auto simp add: fun_eq_iff preca_def faila_def rela_def OO_def ff_def)
    by (case_tac y, auto)

  lemma fb_a_not_fail_fail_simp: "fb_a r (OK (u, x)) ∙ = (r (OK (u, x)) ∙)"
    by (simp add: fb_a_def)
 
  lemma fb_b_not_fail_simp: "fb_b r (OK (u, x)) (OK (u', y')) = (u = u' ∧ r (OK (u, x)) (OK (u', y')))"
    by (simp add: fb_b_def, auto)

  lemma fb_b_fail_simp: "fb_b r (OK (u, x)) ∙ = r (OK (u, x)) ∙"
    by (simp add: fb_b_def)
  
  lemma refine_fba_a: "wp r ≤ wp r' ⟹ wp (fb_a r) ≤ wp (fb_a r')"
    apply (simp add: wp_def assert_demonic_refinement, safe)
    apply (simp_all add: preca_def faila_def rela_def le_fun_def)
    by metis

  lemma refine_fba_b': "wp r ≤ wp r' ⟹ wp (fb_b r) ≤ wp (fb_b r')"
    apply (simp add: wp_def assert_demonic_refinement, safe)
    apply (simp_all add: preca_def faila_def rela_def le_fun_def)
    by metis

  lemma rel_bot_comp: "(preca r x ∧ rela (r OO r') x y) = (preca r x ∧ (rela r OO rela r') x y)"
    apply (simp add: fun_eq_iff rela_def OO_def preca_def faila_def, auto)
    by (case_tac ya, auto)

  lemma prec_demonic: "{.p ⊓ q.} o [:r:] = {.p ⊓ q.} o [:x↝y . p x ∧ r x y:]"
    by (simp add: le_fun_def demonic_def assert_def fun_eq_iff, auto)

  lemma wp_refine: "(wp r ≤ wp r') = (preca r ≤ preca r' ∧ (∀ x . preca r x ⟶ rela r' x ≤ rela r x))"
    by (simp add: wp_def assert_demonic_refinement)

  lemma wp_comp: "ff r ⟹ ff r' ⟹ wp (r OO r') = ((wp r) o (wp r'))"
    proof -
      assume [simp]: "ff r"
      assume [simp]: "ff r'"
      have "(wp r) o (wp r') = {.preca r.} o [:rela r:] o {.preca r'.} o [:rela r':]"
        by (simp add: wp_def comp_assoc)
      also have "... = {.(λx. preca r x ∧ (∀y. rela r x y ⟶ preca r' y)).} o [:rela r OO rela r':]"
        by (simp add: assert_demonic_comp)
      also have "... = {.preca r ⊓ (λ x . ∀y. rela r x y ⟶ preca r' y).} o [:rela r OO rela r':]"
        by (simp add: inf_fun_def)
      also have "... = {.preca r ⊓ (λ x . ∀y. rela r x y ⟶ preca r' y).} o [:x ↝ y . preca r x ∧ (rela r OO rela r') x y:]"
        by (subst prec_demonic, simp)
      also have "... = {.preca r ⊓ (λ x . ∀y. rela r x y ⟶ preca r' y).} o [:x ↝ y . preca r x ∧ rela (r OO r') x y:]"
        by (simp add: rel_bot_comp)
      also have "... = {.preca r ⊓ (λ x . ∀y. rela r x y ⟶ preca r' y).} o [:rela (r OO r'):]"
        by (subst prec_demonic, simp)
      also have "... = {. λ x . preca r x ∧ (∀y. rela r x y ⟶ preca r' y).} o [:rela (r OO r'):]"
        by (simp add: inf_fun_def)
      also have "... =  {.preca (r OO r').} o [:rela (r OO r'):]"
        by (simp add:  pred_bot_comp)
      also have "... = wp (r OO r')"
        by (simp add: wp_def)
      finally show "wp (r OO r') = ((wp r) o (wp r'))" by simp
    qed

  lemma not_maximal_prod: "(¬ maximal (a, b)) = (¬ maximal a ∨ ¬ maximal b)"
    by (simp add: maximal_def less_prod_def less_le le_prod_def, auto)

  lemma [simp]: "ff fb_end"
    by (simp add: fb_end_def  not_maximal_prod ff_def)

  lemma refine_left: "S ≤ S' ⟹ S o T ≤ S' o T"
    by (simp add: le_fun_def)

  lemma prec_SUP: "preca (SUP n . r n) = (INF n . preca (r n))"
    by (simp add: preca_def fun_eq_iff faila_def)

  lemma rel_SUP: "rela (SUP n . r n) = (SUP n . rela (r n))"
    by (simp add: rela_def fun_eq_iff SUP_image)

  lemma INF_spec: "(INF n . {.p n.} o [:(r n)::('a ⇒ 'b ⇒ bool):]) = {.INF n . p n.} o [:SUP n . r n:]"
    by (simp add: fun_eq_iff demonic_def assert_def le_fun_def, auto)

  lemma wp_SUP: "wp (SUP n . r n) = (INF n . wp (r n))"
    by (simp add: wp_def prec_SUP rel_SUP INF_spec)

  thm wp_def

  thm funpow_times_power

  lemma le_power: "mono g ⟹ (f::'a::order ⇒ 'a::order) ≤ g ⟹ f ^^ n ≤ g ^^ n"
    apply (induction n)
    apply (simp add: le_fun_def, auto)
    apply (simp add: le_fun_def, safe)
    apply (simp add: mono_def)
    by (rule_tac y = "g ((f ^^ n) x)" in order_trans, simp_all)

  lemma [simp]: "mono (wp r)"
    by (simp add: wp_def)
 
  lemma [simp]: "ff r ⟹ ff ((r::'a fail_option ⇒ 'a fail_option ⇒ bool) ^^ n)"
    by (induction n, auto simp add: ff_def)

  lemma wp_power: "ff r ⟹ wp ((r:: 'a fail_option ⇒ 'a fail_option ⇒ bool) ^^ n) = (wp r) ^^ n"
    apply (induction n)
    apply auto [1]
    by (unfold funpow_Suc_right, simp add: wp_comp)


  lemma wp_power_refin: "ff r ⟹ ff r' ⟹ wp (r::'a fail_option ⇒ 'a fail_option ⇒ bool) ≤ wp r' ⟹ wp (r^^n) ≤ wp (r'^^n)"
    apply (simp add: wp_power)
    by (rule le_power, simp_all)

  thm INF_lower

  lemma wp_rt_refine: "ff r ⟹ ff r' ⟹ wp r ≤ wp r' ⟹ wp (r^**) ≤ wp (r'^**)"
    apply (simp add: rtranclp_is_Sup_relpowp)
    apply (simp add: wp_SUP)
    apply (rule INF_greatest, simp)
    apply (rule_tac y = "wp (r ^^ x)" in order_trans)
    apply (rule_tac i = x in INF_lower, simp)
    by (rule wp_power_refin, simp_all)

  lemma [simp]: "ff fb_begin"
    by (simp add: fb_begin_def ff_def)

  lemma [simp]: "ff (fb_a r)"
    by (simp add: fb_a_def ff_def)

  lemma [simp]: "ff (fb_b r)"
    by (simp add: fb_b_def ff_def)

  lemma [simp]: "ff ((fb_a r)⇧*⇧*)"
    by (simp add: ff_def)

  lemma [simp]: "ff r ⟹ ff r' ⟹ ff (r OO r')"
    by (auto simp add: ff_def)

  theorem InstFeedback_refine: "ff r ⟹ ff r' ⟹ wp r ≤ wp r' ⟹ wp (InstFeedback r) ≤ wp (InstFeedback r')"
    apply (simp add: InstFeedback_simp wp_comp)
    apply (rule mono_comp_simp, simp_all)
    apply (rule mono_comp, simp_all)
    apply (rule wp_rt_refine, simp_all)
    by (simp_all add: refine_fba_a refine_fba_b')

  lemma [simp]: "ff r ⟹ ff (InstFeedback r)"
    by (simp add: InstFeedback_simp) 

  theorem fb_hide_refine: "ff r ⟹ ff r' ⟹ wp r ≤ wp r' ⟹ wp (fb_hide r) ≤ wp (fb_hide r')"
    apply (simp add: fb_hide_def wp_comp)
    apply (rule refine_left)
    by (rule InstFeedback_refine, simp_all)

  definition "cross_prod r r' =  (λ ux vy . (case ux of ∙ ⇒ vy = ∙ | OK (u::'a::order_bot, x) ⇒ 
                 (∃ v y . vy = OK (v, y) ∧ r (OK x) (OK v) ∧ r' (OK u) (OK y)) 
                    ∨ (vy = ∙ ∧ r (OK x) ∙) ∨  (vy = ∙ ∧ r' (OK u) ∙)  ))"

  definition "InstFeedback_cross_prod r r' = (λ x vy. (case x of ∙ ⇒ vy = ∙ | OK x ⇒ 
       (∃ v y . vy = OK (v, y) ∧ r (OK x) (OK v) ∧ r' (OK v) (OK y)) ∨ 
       (vy = ∙ ∧ r (OK x) ∙) ∨ (∃ v . vy = ∙ ∧ r (OK x) (OK v) ∧ r' (OK v) ∙ )   ))"

  lemma [simp]: "(∙ < x) = False"
    by (unfold less_fail_option_def le_fail_option_def, simp)

  type_synonym ('a, 'b) fail_pair = "(('a option) × ('b)) fail_option"
  type_synonym ('a, 'b, 'c) fail_pair_rel = "('a,'c) fail_pair ⇒ ('a,'b) fail_pair ⇒ bool"

  lemma [simp]: "(=) ⊔ fba_a r ⊔ ((=) OO fba_a r) OO fba_a r ⊔ (((=) OO fba_a r) OO fba_a r) OO fba_a r ≤ (SUP n. fba_a r ^^ n)"
    apply (simp add: le_fun_def, safe)
    apply (rule_tac x = 0 in exI, simp)
    apply (rule_tac x = "Suc 0" in exI, simp add: OO_def)
    apply (rule_tac x = "Suc (Suc 0)" in exI, auto simp add: OO_def)
    by (rule_tac x = "Suc (Suc (Suc 0))" in exI, auto simp add: OO_def)

  lemma all_fail: "∀i<xb. fb_a r (a i) (a (Suc i)) ⟹ a 0 = ∙ ⟹ ∀ i ≤ xb . a i = ∙"
    apply (induction xb, simp, safe)
    apply (frule_tac x = xb in spec, simp)
    by (case_tac i, simp_all)

  lemma fba_a_pair: "(fb_a (r :: ('a,'b,'c) fail_pair_rel))^** = ((=) ⊔ fb_a r ⊔ (fb_a r) ^^ (Suc (Suc 0)))"
    apply (simp add: rtranclp_is_Sup_relpowp)
    apply (rule antisym)
    apply (simp add: le_fun_def OO_def)
    apply safe [1]
    apply simp
    apply (simp add: relpowp_chain)
    apply safe [1]
    apply (case_tac "a 0", simp_all)
    apply (drule all_fail, simp_all)
    apply (case_tac f, simp_all)
    apply (case_tac "a (Suc 0)")
    apply (cut_tac a = "λ i . a (Suc i)" and r = r and xb = nat in  all_fail, simp_all)
    apply auto [1]
    apply (case_tac nat, simp_all)
    apply (case_tac "a (Suc (Suc 0))")
    apply (cut_tac a = "λ i . a (Suc (Suc i))" and r = r and xb = nata in  all_fail, simp_all)
    apply auto [1]
    apply (frule_tac x = 0 in spec)
    apply (drule_tac x = "Suc 0" in spec, simp)
    apply auto [1]
    apply (drule_tac x = "OK (ab, ba)" in spec)
    apply auto [1]
    apply (frule_tac x = 0 in spec)
    apply (drule_tac x = "Suc 0" in spec, simp)
    apply auto [1]
    apply (simp add: less_option_def le_option_def)
    apply auto [1]
    apply safe
    apply simp_all
    apply (rule_tac x = 0 in exI, simp)
    apply (rule_tac x = "Suc 0" in exI, simp add: OO_def)
    by (rule_tac x = "Suc (Suc 0)" in exI, auto simp add: OO_def)



  lemma [simp]: "ff (cross_prod r r')"
    by (simp add: cross_prod_def ff_def)

  lemma [simp]: "fb_begin ∙ x = (x = ∙)"
    by (simp add: fb_begin_def)

  lemma [simp]: "InstFeedback_cross_prod r r' ∙ x = (x = ∙)"
    by (simp add: InstFeedback_cross_prod_def)

  definition "complete r = (∀ x . ∃ y . r x y)"
  definition "fail_mono r = (∀ x y . x ≤ y ∧ r x ∙ ⟶ r y ∙)"

  definition "unkn_not_fail r = (¬ r (OK ⊥) ∙)"

  lemma [simp]: "unkn_not_fail r' ⟹ cross_prod r r' (OK (⊥, x2)) ∙ ⟹ InstFeedback_cross_prod r r' (OK x2) ∙"
    by (simp add: cross_prod_def InstFeedback_cross_prod_def unkn_not_fail_def)

  lemma [simp]: "cross_prod r r' (OK (ab, bb)) (OK (ab, c)) ⟹ InstFeedback_cross_prod r r' (OK bb) (OK (ab, c))"
    by (simp add: cross_prod_def InstFeedback_cross_prod_def)

  lemma [simp]: "OK (⊥, ⊥) < OK (⊥, Some a)"
    by (simp add: less_fail_option_def le_fail_option_def le_prod_def bot_prod_def bot_option_def le_option_def) 

  lemma [simp]: "OK (⊥, ⊥) < OK (Some a, ⊥)"
    by (simp add: less_fail_option_def le_fail_option_def le_prod_def bot_prod_def bot_option_def le_option_def) 

  lemma [simp]: "OK (⊥, ⊥) < OK (Some a, Some b)"
    by (simp add: less_fail_option_def le_fail_option_def le_prod_def bot_prod_def bot_option_def le_option_def) 

  lemma [simp]: "OK (None, None) < OK (Some a, y)"
    by (simp add: less_fail_option_def le_fail_option_def le_prod_def bot_prod_def bot_option_def le_option_def) 

  lemma move_down: "p ⟹ p"
    by simp

  lemma [simp]: "None < Some a"
    by (simp add: less_option_def le_option_def)

  lemma [simp]: "⊥ < Some a"
    by (simp add: less_option_def le_option_def bot_option_def)

  thm InstFeedback_cross_prod_def

  thm unkn_not_fail_def
  thm complete_def


  lemma f_f_fb_begin: "f_f fb_begin"
    by (simp add: f_f_def fb_begin_def)

  lemma f_f_fb_a: "f_f (fb_a r)"
    by (simp add: f_f_def)

  lemma f_f_fb_b: "f_f (fb_b r)"
    by (simp add: f_f_def)

  lemma f_f_comp: "f_f r ⟹ f_f r' ⟹ f_f (r OO r')"
    by (simp add: f_f_def OO_def, auto)

  lemma [simp]: "(fb_a r)⇧*⇧* ∙ x = (x = ∙)"
    by (simp add: rtranclp_is_Sup_relpowp)

  lemma f_f_InstFeedback: "f_f (InstFeedback r)"
    apply (simp add: InstFeedback_simp)
    apply (rule f_f_comp, simp_all add: f_f_fb_begin)
    apply (rule f_f_comp)
    apply (simp add: f_f_def)
    by (simp add: f_f_fb_b)

  lemma InstFeedback_cross_prod_aux: "complete r' ⟹ unkn_not_fail r' ⟹ InstFeedback_cross_prod r r' x xa ⟹ InstFeedback (cross_prod r r') x xa"
    apply (case_tac x)
    apply (simp add: InstFeedback_cross_prod_def InstFeedback_def)
    apply (simp add: InstFeedback_cross_prod_def InstFeedback_def, safe)
    apply(case_tac "v = ⊥")
    apply (rule_tac x = 0 in exI)
    apply (rule_tac x = "λ i . ⊥" in exI, simp)
    apply (simp add: cross_prod_def)
    apply (rule_tac x = 1 in exI)
    apply (rule_tac x = "λ i . if i = 0 then ⊥ else v" in exI, simp)
    apply (simp add: cross_prod_def complete_def)
    apply (drule_tac x = "OK ⊥" in spec, safe)
    apply (case_tac ya, simp_all)
    apply (simp add: unkn_not_fail_def)
    apply blast
    apply (rule_tac x = 0 in exI)
    apply (rule_tac x = "λ i . ⊥" in exI, simp)
    apply (simp add: cross_prod_def)

    apply(case_tac "v = ⊥")
    apply (rule_tac x = 0 in exI)
    apply (rule_tac x = "λ i . ⊥" in exI, simp)
    apply (simp add: cross_prod_def)
    apply (rule_tac x = 1 in exI)
    apply (rule_tac x = "λ i . if i = 0 then ⊥ else v" in exI, simp)
    apply (simp add: cross_prod_def complete_def)
    apply (drule_tac x = "OK ⊥" in spec, safe)
    apply (case_tac y, simp_all)
    apply (simp add: unkn_not_fail_def)
    by blast

  theorem InstFeedback_cross_prod: "complete r' ⟹ unkn_not_fail r' ⟹  InstFeedback (cross_prod r r') = InstFeedback_cross_prod r r'"
    proof (simp add: fun_eq_iff, safe)
      fix x::"'c fail_option" 
      fix xa:: "('a × 'b) fail_option"
      assume A: "InstFeedback (cross_prod r r') x xa"
      assume E: "unkn_not_fail r'"
      show "InstFeedback_cross_prod r r' x xa"
        proof (cases x)
          assume B: "x = ∙"
          from this and A have "xa = ∙" by (cut_tac f_f_InstFeedback, simp add: f_f_def, auto)
          from this and B show ?thesis 
            by (simp add: InstFeedback_cross_prod_def)
        next
          fix a assume B: "x = OK a"
          from this and A obtain u b n v where 
            C: "(cross_prod r r') (OK (u, a)) xa" and
            D: "xa = OK(u, b) ∨ xa = ∙" and
            F: "⋀ i . (i < (n::nat) ⟹ ∃ c . (cross_prod r r') (OK (v i, a)) (OK (v (i+1), c)))" and
            G: "u = v n" and
            H: "v 0 = ⊥"
            by (simp add: InstFeedback_alt, auto)
            show ?thesis
            proof (cases "xa = ∙")
              assume I: "xa = ∙"
              from this and C and G and H have "¬ r (OK a) ∙ ⟹ n > 0"
                apply (case_tac n, simp_all)
                apply (simp add: cross_prod_def)
                by (cut_tac E, simp add: unkn_not_fail_def)
              from this and G have J: "¬ r (OK a) ∙ ⟹ r (OK a) (OK u)"
                apply simp
                apply (case_tac n, simp_all)
                apply (cut_tac i = "nat" in F, safe) 
                by (simp add: cross_prod_def)
              from I and B and C show ?thesis
                apply (case_tac "r (OK a) ∙")
                apply (simp add: cross_prod_def InstFeedback_cross_prod_def)
                apply safe
                apply (drule J)
                apply (simp add: cross_prod_def InstFeedback_cross_prod_def)
                by auto
            next
              assume "xa ≠ ∙"
              from this and D have "xa = OK(u, b)" by simp
              from this and B and C show ?thesis
                by (simp add: cross_prod_def InstFeedback_cross_prod_def)
            qed
        qed
    next
      fix x::"'c fail_option" 
      fix xa:: "('a × 'b) fail_option"
      assume " complete r'" and " unkn_not_fail r'" and "InstFeedback_cross_prod r r' x xa"
      from this show "InstFeedback (cross_prod r r') x xa"
        by (rule InstFeedback_cross_prod_aux)
  qed


  lemma [simp]: "OK (Some a, None) < OK (Some a, Some aa)"
    by (simp add: less_fail_option_def le_fail_option_def le_prod_def le_option_def)

  thm fb_hide_def
  thm fb_end_def

  definition "fb_end_ukn = (λuy y'. case uy of ∙ ⇒ y' = ∙ | OK (u, y) ⇒ y' = OK y)"


  definition "fb_hide_cross_prod r r' = (λ x y. (case x of ∙ ⇒ y = ∙ | OK x ⇒ 
       (∃ v  . r (OK x) (OK (Some v)) ∧ r' (OK (Some v)) y) ∨ (y = ∙ ∧ (r (OK x) ∙ ∨ r (OK x) (OK ⊥)))))"

  lemma [simp]: "InstFeedback_cross_prod r r' ∙ y = (y = ∙)"
    by (simp add: InstFeedback_cross_prod_def)


  lemma [simp]: "ff r ⟹ f_f r ⟹ (r ∙ x) = (x = ∙)"
    by (simp add: f_f_def ff_def, auto)

  lemma rel_union: "rela (r ⊔ r') = rela r ⊔ rela r'"
    by (simp add: fun_eq_iff rela_def)

  lemma prec_union: "preca (r ⊔ r') = preca r ⊓ preca r'"
    by (simp add: fun_eq_iff preca_def faila_def)

  lemma "wp (r ⊔ r') = wp r ⊓ wp r'"
    by (simp add: wp_def rel_union prec_union spec_demonic_choice)

  lemma chain_OK: "⋀ a' b' . ∀i<n. aa i < aa (Suc i) ⟹ aa 0 = OK (a, b) ⟹ aa n = OK (a', b') ⟹ (∃ u y . ∀ i ≤ n . aa i =  OK (u i, y i))"
    proof (induction n)
      case 0 
        assume [simp]: "aa 0 = OK (a, b)"
        show ?case
          apply (rule_tac x = "λ i . a" in exI)
          apply (rule_tac x = "λ i . b" in exI)
          by simp
     next
     case (Suc n)
      from this
      have  A:"(⋀a' b'. ∀i<n. aa i < aa (Suc i) ⟹ aa 0 = OK (a, b) ⟹ aa n = OK (a', b') ⟹ ∃u y. ∀i≤n. aa i = OK (u i, y i))"
        and B: "∀i<Suc n. aa i < aa (Suc i)"
        and C: "aa 0 = OK (a, b)"
        and D: "aa (Suc n) = OK (a', b')"
          by simp_all
      from B and D obtain a'' b'' where "aa n = OK (a'', b'')"
        apply (case_tac "aa n", simp_all)
        apply auto [1]
        by (case_tac x2, simp)

      from this and A and B and C have "∃ u y . ∀i≤n. aa i = OK (u i, y i)"
        by auto
      from this obtain u y where "∀ i≤n . aa i = OK (u i, y i)"
        by blast
       
      from this and D show ?case
        apply (rule_tac x = "λ i . (if i ≤ n then u i else a')" in exI)
        apply (rule_tac x = "λ i . (if i ≤ n then y i else b')" in exI)
        apply auto
        by (case_tac "i = Suc n", simp_all)
   qed

  lemma [simp]: "maximal (None) = False"
    apply (simp add: maximal_def)
    apply (rule_tac x = "Some (Eps ⊤)" in exI)
    by (simp add: less_option_def le_option_def)

  lemma [simp]: "maximal u = (u ≠ None)"
    by (simp add: maximal_def less_option_def le_option_def, auto)

  lemma [simp]: "OK (⊥, ⊥) ≤ OK (a, b)"
    by (simp add: le_fail_option_def le_prod_def)

  thm InstFeedback_cross_prod_def

  lemma fb_hide_cross_proda: "complete r' ⟹ unkn_not_fail r' ⟹ fb_hide (cross_prod r r') x y = fb_hide_cross_prod r r' x y"
    apply (simp add: fb_hide_def InstFeedback_cross_prod OO_def fb_end_def)
    apply (case_tac x, simp_all, safe)
    apply (simp add: fb_hide_cross_prod_def)
    apply (simp add: fb_hide_cross_prod_def)
    apply (case_tac ya, simp_all)
    apply (simp add: InstFeedback_cross_prod_def fb_hide_cross_prod_def)
    apply auto [1]
    apply (case_tac v, simp_all)
    apply (simp add: bot_option_def)
    apply (case_tac x2a, simp)
    apply (simp add: InstFeedback_cross_prod_def fb_hide_cross_prod_def bot_option_def, safe, simp_all)
    apply (simp add: fb_hide_cross_prod_def, safe)
    apply (case_tac y, simp_all)
    apply auto [1]
    apply (rule_tac x = ∙ in exI, simp_all)
    apply (simp add: InstFeedback_cross_prod_def)
    apply auto [1]
    apply (rule_tac x = "OK (Some v, x2a)" in exI, simp_all)
    apply (simp add: InstFeedback_cross_prod_def)

    apply (simp add: InstFeedback_cross_prod_def)
    apply (rule_tac x = ∙ in exI, simp_all)
    apply (simp add: complete_def)
    apply (drule_tac x = "OK ⊥" in spec, safe)
    apply (case_tac ya, simp)
    apply (rule_tac x = ∙ in exI, simp)
    apply (simp add: InstFeedback_cross_prod_def)
    apply auto [1]
    apply (rule_tac x = "OK (⊥, x2a)" in exI, simp_all)
    by (simp add: InstFeedback_cross_prod_def bot_option_def)
	
  subsection‹Examples›

  definition "havoc x y = (maximal x ⟶ maximal y)"

  definition "EQ  = (λ ux vy . vy = (case ux of ∙ ⇒ ∙ | OK ((u::'a option), x) ⇒ OK (u, u) ))"

  lemma [simp]: "(a::'a::order) < a = False"
    by (simp add: less_le_not_le)

  lemma fb_hide_fun_EQ: "InstFeedback EQ x uy = (uy = (case x of ∙ ⇒ ∙ | _ ⇒ OK (⊥,⊥)))"
    apply (simp add: InstFeedback_def maximal_def, safe)
    apply (case_tac x, simp_all, safe)
    apply (drule_tac x = 0 in spec, simp)
    apply (drule_tac x = 0 in spec, simp, safe)
    apply (simp_all add: EQ_def)
    apply (case_tac n, simp_all)
    apply blast
    apply (case_tac x, simp_all)
    apply (rule_tac x = 0 in exI, simp)
    apply (simp add: bot_prod_def EQ_def )
    by auto


  lemma "fb_hide EQ x y = (y = ∙)"
    apply (simp add: fb_hide_def fb_hide_fun_EQ OO_def fb_end_def)
    by (case_tac x, simp_all add: bot_option_def)

  definition "TRUEa  = (λ ux vy . (case ux of ∙ ⇒ vy = ∙ | OK ((u::'a option), x) ⇒ (∃ v . vy = OK (v, v) ∧ (u ≠ None ⟶ v ≠ None)) ))"

 lemma move_assumption: "p ⟹ p"
   by simp

  lemma fb_hide_fun_TRUEa: "InstFeedback TRUEa x uy =  (case x of ∙ ⇒ uy = ∙ | _ ⇒ (∃ u . uy = OK (u, u)))"
    apply (simp add: InstFeedback_def, safe)
    apply (case_tac x, simp_all, safe)
    apply (frule_tac x = 0 in spec, simp)
    apply (drule move_assumption)
    apply (drule move_assumption)
    apply (frule_tac x = 0 in spec, simp add: TRUEa_def)
    apply auto [1]
    apply (simp add: TRUEa_def)


    apply (case_tac x, simp_all, safe)
    apply (case_tac "u = ⊥", simp_all)

    apply (rule_tac x = "0" in exI, simp)
    apply (simp add: TRUEa_def)
    apply auto

    apply (rule_tac x = "Suc 0" in exI, simp)
    apply (simp add: less_fail_option_def le_fail_option_def le_prod_def le_option_def bot_option_def  TRUEa_def bot_prod_def)
    apply (case_tac u, simp_all)
    apply (rule_tac x = "λ i . if i = 0 then ⊥ else u" in exI)
    apply auto
    by (simp_all add: less_option_def le_option_def bot_option_def)


  lemma "fb_hide TRUEa x y = (case x of ∙ ⇒ y = ∙ | _ ⇒ (y = ∙ ∨ (∃ u . maximal u ∧ y = OK u)))"
    apply (simp add: fb_hide_def fb_hide_fun_TRUEa OO_def fb_end_def)
    apply (case_tac x, simp_all, auto)
    by (rule_tac x = "OK (Some ya, Some ya)" in exI, simp)


(***********)

  definition "TRUE  = (λ ux vy . (case ux of ∙ ⇒ vy = ∙ | OK ((u::'a option), x) ⇒ (∃ u . vy = OK (u, u)) ))"

  lemma fb_hide_fun_TRUE: "InstFeedback TRUE x uy =  (case x of ∙ ⇒ uy = ∙ | _ ⇒ (∃ u . uy = OK (u, u)))"
    apply (simp add: InstFeedback_def, safe)
    apply (case_tac x, simp_all, safe)
    apply (frule_tac x = 0 in spec, simp)
    apply (drule move_assumption)
    apply (drule move_assumption)
    apply (frule_tac x = 0 in spec, simp add: TRUE_def)
    apply auto [1]
    apply (simp add: TRUE_def)


    apply (case_tac x, simp_all, safe)
    apply (case_tac "u = ⊥", simp_all)

    apply (rule_tac x = "0" in exI, simp)
    apply (simp add: TRUE_def)
    apply auto

    apply (rule_tac x = "Suc 0" in exI, simp)
    apply (simp add: less_fail_option_def le_fail_option_def le_prod_def le_option_def bot_option_def  TRUE_def bot_prod_def)
    apply (case_tac u, simp_all)
    apply (rule_tac x = "λ i . if i = 0 then ⊥ else u" in exI)
    apply auto
    by (simp_all add: less_option_def le_option_def bot_option_def)


  lemma "fb_hide TRUE x y = (case x of ∙ ⇒ y = ∙ | _ ⇒ (y = ∙ ∨ (∃ u . maximal u ∧ y = OK u)))"
    apply (simp add: fb_hide_def fb_hide_fun_TRUE OO_def fb_end_def)
    apply (case_tac x, simp_all, auto)
    by (rule_tac x = "OK (Some ya, Some ya)" in exI, simp)
 
  definition "NEQ  = (λ ux vy . (case ux of ∙ ⇒ vy = ∙ | OK (u, x) ⇒ 
    (∃ v . vy = OK (v, v) ∧ ((u = None ⟶ v = None) ∧ (u ≠ None ⟶ u ≠ v)))))"

  definition "NEQ2  = (λ ux vy . (case ux of ∙ ⇒ vy = ∙ | OK (u, x) ⇒ 
    (∃ v . vy = OK (v, v) ∧ ((u = None ⟶ v = None) ∧ (u ≠ None ⟶ u ≠ v ∧ v ≠ None)))))"

  lemma fb_hide_fun_NEQ2: "InstFeedback NEQ2 x uy = (case x of ∙ ⇒ uy = ∙ | _ ⇒ uy = OK (None, None))"
    apply (simp add: InstFeedback_def maximal_def, safe)
    apply (case_tac x, simp_all, safe)
    apply (drule_tac x = 0 in spec, simp)
    apply (drule_tac x = 0 in spec, simp, safe)
    apply (simp_all add: NEQ2_def)
    apply (case_tac x, simp_all)
    apply (rule_tac x = 0 in exI, simp)
    apply (rule_tac x = "λ i . ⊥" in exI)
    by (simp add: bot_prod_def NEQ2_def  bot_option_def)

  lemma fb_hide_fun_NEQ: "InstFeedback NEQ x uy = (case x of ∙ ⇒ uy = ∙ | _ ⇒ uy = OK (None, None))"
    apply (simp add: InstFeedback_def maximal_def, safe)
    apply (case_tac x, simp_all, safe)
    apply (drule_tac x = 0 in spec, simp)
    apply (drule_tac x = 0 in spec, simp, safe)
    apply (simp_all add: NEQ_def)
    apply (case_tac x, simp_all)
    apply (rule_tac x = 0 in exI, simp)
    apply (rule_tac x = "λ i . ⊥" in exI)
    by (simp add: bot_prod_def NEQ_def  bot_option_def)

  lemma "fb_hide NEQ x y = (y = ∙)"
    apply (simp add: fb_hide_def fb_hide_fun_NEQ OO_def fb_end_def)
    by (case_tac x, simp_all)

  lemma "fb_hide NEQ2 x y = (y = ∙)"
    apply (simp add: fb_hide_def fb_hide_fun_NEQ2 OO_def fb_end_def)
    by (case_tac x, simp_all)

  definition "rel_bot_true r = (∀ x y . ¬ maximal x ⟶ r x y)"
  definition "rel_maximal r = (∀ x y . r x y ∧ maximal x ⟶ maximal y)"

  definition "assert_rel p x y = (if p x then y = x else y = ⊥)"

  definition "comp_rel r r' x y = (if r x ⊥ then y = ⊥ else (∃ z . r x z ∧ r' z y))"

  definition "AND x y = (case (x,y) of (Some a, Some b) ⇒ Some (a ∧ b) 
    | (None, Some False) ⇒ Some False | (Some False, None) ⇒ Some False | _ ⇒ None)"

  definition "AND_rel ux vy  = (case ux of ∙ ⇒ vy = ∙ | OK (u, x) ⇒ vy = OK (AND u x, AND u x))"

  lemma [simp]: "ff AND_rel"
    by (simp add: ff_def AND_rel_def)

  lemma [simp]: "((None, Some a) ≤ (None, None)) = False"
    by (simp add: le_prod_def le_option_def)

  lemma [simp]: "AND_rel (OK (u, Some False)) (OK (v, y)) = ((v = Some False) ∧ (y = Some False))"
    apply (simp add: AND_rel_def AND_def)
    apply (case_tac u, simp_all)
    by(case_tac a, simp_all)

  lemma [simp]: "AND_rel (OK (Some False, u)) (OK (v, y)) = ((v = Some False) ∧ (y = Some False))"
    apply (simp add: AND_rel_def AND_def)
    by (case_tac u, simp_all)

  lemma AND_comute: "AND x y = AND y x"
    apply (simp add: AND_def)
    apply (case_tac x, simp_all)
    apply (case_tac y, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac y, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac aa, simp_all)
    by (case_tac aa, simp_all)


  lemma AND_rel_comute: "AND_rel (OK (x, y)) = AND_rel (OK (y, x))"
    by (simp add: AND_rel_def fun_eq_iff AND_comute)

  lemma [simp]: "AND_rel (OK x) ∙ = False"
    by (simp add: AND_rel_def)

  lemma fb_hide_fun_AND: "InstFeedback AND_rel x uy = (case x of ∙ ⇒ uy = ∙ | OK (Some False) ⇒ uy = OK (Some False, Some False) | _ ⇒ (uy = OK (⊥, ⊥)))"
    apply (simp add: InstFeedback_simp fun_eq_iff fba_a_pair, safe)
    apply (simp_all add: fb_begin_def)
    apply (case_tac x, simp_all)
    apply (case_tac uy, simp_all)
    apply (case_tac x2, simp_all)
    apply (case_tac x2a, simp_all)
    apply (simp add: AND_rel_def AND_def bot_option_def)
    apply (case_tac x2a, simp_all, safe, simp)
    apply (simp add: AND_rel_def AND_def bot_option_def)
    apply (case_tac aa, simp_all add: bot_option_def)

    apply (case_tac x, simp_all)
    apply (case_tac ba, simp_all)
    apply (case_tac x2a, simp, safe, simp)
    apply (case_tac uy, simp_all)
    apply (case_tac x2, simp_all, safe, simp_all)
    apply (simp add: AND_rel_def AND_def bot_option_def)
    apply (case_tac bb, simp_all)
    apply (case_tac a, simp_all)

    apply (case_tac x, simp_all)
    apply (case_tac bb, simp_all)
    apply (case_tac ba, simp_all)
    apply (case_tac x2a, case_tac x2b, simp, safe, simp)
    apply (case_tac uy, simp_all)
    apply (case_tac x2, simp, safe, simp)
    apply (simp add: less_option_def le_option_def bot_option_def)
    apply auto [1]
    apply (simp add: OO_def)
    apply (case_tac x, simp_all)
    apply (case_tac x2, simp_all, safe, simp_all)
    apply (simp_all add: bot_option_def)
    apply (simp add: AND_rel_def AND_def)

    apply (case_tac a, simp_all add: bot_option_def)
    apply (simp add: AND_rel_def AND_def bot_option_def)

    by (rule_tac x = "OK (Some False, Some False)" in exI, simp)


  lemma "fb_hide AND_rel x y =  (case x of ∙ ⇒ y = ∙ | OK (Some False) ⇒ y = OK (Some False) | _ ⇒ y = ∙)"
    apply (simp add: fb_hide_def OO_def fb_hide_fun_AND fb_end_def)
    apply (case_tac x, simp_all, auto)
    apply (case_tac ya, simp_all)
    apply (case_tac x2, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac x2, simp_all, safe, simp_all add: bot_option_def)
    apply (case_tac aa, simp_all)
    apply (case_tac aa, simp_all add: bot_option_def)
    apply (case_tac x2, simp_all, safe, simp_all add: bot_option_def)
    apply (case_tac a, simp_all add: bot_option_def)
    by (rule_tac x = False in exI, simp)


  definition "AND_rel2a  = (λ ((w, u),x) ((v, w'), y) . (v = AND u x) ∧ (w = w') ∧ (v = y))"

  definition "AND_rel2 wux vwy  = (case wux of ∙ ⇒ vwy = ∙ | OK ((w, u), x) ⇒ vwy = OK ((AND u x, w), AND u x))"

  lemma [simp]: "ff AND_rel2"
    by (simp add: ff_def AND_rel2_def)


  lemma [simp]: "AND_rel2 (OK ((w, u), Some False)) (OK ((v, w'), c)) = (v = Some False ∧ w = w' ∧ Some False = c)"
    apply ( simp add: AND_rel2_def AND_def)
    apply (case_tac u, simp_all)
    apply metis
    apply (case_tac a, simp_all)
    apply metis
    by metis

  lemma [simp]: "AND_rel2 (OK (a, Some False)) (OK (b, c)) = (fst b = Some False ∧ fst a = snd b ∧ Some False = c)"
    by (case_tac a, case_tac b, simp)

  thm f_f_def


  lemma [simp]: "⋀u x . (⋀ u . preca r (u, x)) ⟹ (fb_a r ^^ n) (OK (u, x)) ∙ = False"
    apply (induction n, simp_all)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all)
    apply (simp add:  preca_def faila_def)
    by (drule fb_a_id, simp_all)

  lemma [simp]: "preca AND_rel2 x"
    by (simp add: AND_rel2_def preca_def faila_def)

  lemma [simp]:"AND_rel2 (OK x) ∙ = False"
    by (simp add: AND_rel2_def)

  lemma [simp]: "AND None None = None"
    by (simp add: AND_def)

  lemma [simp]: "AND (Some True) (Some True) = (Some True)"
    by (simp add: AND_def)

  lemma [simp]: "AND (Some False) x = (Some False)"
    apply (simp add: AND_def)
    by (case_tac x, auto)
    
  lemma [simp]: "AND x (Some False) = (Some False)"
    apply (simp add: AND_def)
    apply (case_tac x, simp_all)
    by (case_tac a, simp_all)
    
  lemma [simp]: "AND_rel2 (OK ((None, None), None)) (OK ((v, w), y)) = (v = None ∧ v = y ∧ v = w)"
    by (simp add: AND_rel2_def le_prod_def, safe)

  lemma [simp]: "AND_rel2 (OK ((None, Some a), None)) (OK ((u, w), y)) =  (u = AND (Some a) None ∧ y = AND (Some a) None ∧ w = None) "
    by (simp add: AND_rel2_def le_prod_def le_option_def, auto)

  lemma [simp]: "AND_rel2 (OK ((None, None), Some True)) (OK ((v, w), y)) = (v = AND None (Some True) ∧ y = AND None (Some True) ∧ w = None)"
    by (simp add: AND_rel2_def le_prod_def le_option_def, auto)

  lemma [simp]: "AND_rel2 (OK ((None, None), Some False)) (OK ((v, w), y)) = (v = Some False ∧ y = Some False ∧ w = None)"
    by (simp add: AND_rel2_def le_prod_def le_option_def, auto)

  lemma [simp]: "AND_rel2 (OK ((Some False, w), Some False)) (OK ((v, w'), y)) = (v = Some False ∧ w' = Some False ∧ y = Some False)"
    by (simp add: AND_rel2_def le_prod_def le_option_def)

  lemma AND2_simp: "AND_rel2 (OK (((u::'a option), w), x)) (OK ((v, w'), y)) = (v = AND w x ∧ w' = u ∧ y = AND w x)"
    by (simp add: AND_rel2_def le_prod_def le_option_def)

  lemma [simp]: "AND_rel2 (OK ((None, None), x)) (OK ((v, w), y)) = (v = AND None x ∧ w = None ∧ y = AND None x)"
    by (simp add: AND_rel2_def le_prod_def le_option_def)

  lemma chain_triple: "x < y ⟹ y < z ⟹ z < w ⟹ w < OK ((a::'a option , b::'b option), c::'c option) ⟹ False"
    apply (case_tac x, simp_all)
    apply (case_tac y, simp_all)
    apply (case_tac z, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac x2, simp_all)
    apply (case_tac x2a, simp_all)
    apply (case_tac x2b, simp_all)
    apply (case_tac x2c, simp_all)
    apply (case_tac aa, simp_all)
    apply (case_tac aaa, simp_all)
    apply (case_tac ab, simp_all)
    apply (case_tac ac, simp_all)
    apply (simp add: less_fail_option_def le_fail_option_def le_prod_def le_option_def)
    by metis

  lemma [simp]: "AND_rel2 (OK ((None, None), None)) (OK ((v, w), y)) =   (v = None ∧ w = None ∧ y = None)  "
    by (simp add: AND_rel2_def AND_def)

 definition "rel_and a b =  (if a = None then b = None ∨ b = Some True else a = b)"

  lemma [simp]: "∃b ba. None = AND b ba"
    apply (rule_tac x = None in exI)
    by (rule_tac x = None in exI, simp)

  lemma [simp]:"(∃b. None = AND (Some True) b)"
    by (rule_tac x = None in exI, simp add: AND_def)

  lemma [simp]: "OK (⊥, ⊥) < OK ((Some False, Some False), Some False)"
    by (metis bot.not_eq_extremum bot_fail_option_def bot_option_def bot_prod_def fail_option.sel option.distinct(1) prod.sel(2))

  lemma [simp]: " OK (⊥, ⊥) < OK ((Some True, Some True), Some True)"
    by (metis bot.not_eq_extremum bot_fail_option_def bot_option_def bot_prod_def fail_option.sel option.distinct(1) prod.sel(2))

  lemma [simp]: "∃b ba. Some False = AND b ba"
    by (rule_tac x = "Some False" in exI, simp)

  lemma [simp]: " ∃b ba. Some x = AND b ba"
    apply (rule_tac x = "Some x" in exI)
    apply (rule_tac x = "Some x" in exI)
    by (case_tac x, simp_all)

  lemma [simp]: " ∃ba. Some True = AND (Some True) ba"
    by (rule_tac x = "Some True" in exI, simp)

  lemma [simp]: "(((⊥), ⊥) < (⊥, None)) = False"
    by (simp add: less_prod_def le_prod_def bot_prod_def)
  lemma [simp]: " ∃b. Some False = AND b (Some True)"
    by (rule_tac x = "Some False" in exI, simp)

  lemma [simp]: "∃b. Some True = AND b (Some True)"
    by (rule_tac x = "Some True" in exI, simp)

  lemma OK_less_less: "(OK x < OK y) = (x < y)"
    by (simp add: less_fail_option_def le_fail_option_def, auto)

  lemma fba_a_chain: "⋀u' . n > 0 ⟹ (fb_a r ^^ n) (OK (u, x)) (OK (u', x')) ⟹ u < (u'::'a::order)"
    apply (induction n, simp_all)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply safe
    apply (case_tac " n > 0", simp_all)
    apply (rule_tac y = "aa" in less_trans)
    apply (simp add: OK_less_less)
    by (simp add: OK_less_less)

  lemma fb_hide_and_eq: "InstFeedback (AND_rel2) (OK x) (OK ((v, w), y)) ⟹ v = y"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe)
    apply (case_tac ya, simp_all)
    apply (case_tac x2, simp_all)
    apply safe
    apply simp
    apply (subst (asm) AND_rel2_def)
    apply (drule drop_assumption)
    apply (case_tac "OK ((v, w), bc)", simp_all)
    apply (case_tac x2, simp_all)
    by (case_tac a, simp_all)

(*Case x = OK None *)

  lemma  [simp]: "InstFeedback (AND_rel2) (OK None) (OK ((None, Some False), None)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def)
    apply safe
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp)
    apply (case_tac bc, simp_all)
    apply (case_tac a, simp_all)
    by (simp add: AND_rel2_def)

  lemma  [simp]: "InstFeedback AND_rel2 (OK None) (OK ((None, None), None))"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def)
    apply (rule_tac x = "OK ((None, None), None)" in exI, simp)
    apply (rule_tac x = "0" in exI, simp)
    by (metis bot_option_def bot_prod_def)

  lemma  [simp]: "InstFeedback  AND_rel2 (OK None) (OK ((None, Some True), None)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp)
    apply (case_tac bc, simp_all)
    apply (case_tac a, simp_all)
    by (simp add: AND_rel2_def)

  lemma  [simp]: "InstFeedback AND_rel2 (OK None) (OK ((Some False, None), Some False)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)
 
  lemma  [simp]: "InstFeedback AND_rel2 (OK None) (OK ((Some False, Some True), Some False)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)

  lemma  [simp]: "InstFeedback (AND_rel2) (OK None) (OK ((Some False, Some False), Some False)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    apply (case_tac f, simp_all)
    apply (simp add: bot_prod_def bot_option_def)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp, safe)
    apply (case_tac ya, simp_all)
    apply (simp add: AND2_simp)
    apply (simp add: less_prod_def le_prod_def)
    apply (simp add: AND2_simp)
    apply (case_tac aa, simp_all)
    apply (case_tac bb, simp_all)
    apply (case_tac ab, simp_all)
    apply (simp add: AND_def)
    apply (case_tac ac, simp_all)
    apply (simp add: AND_def)
    apply (case_tac ac, simp_all)
    apply (simp add: AND2_simp)
    apply (case_tac f, simp_all)

    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp, safe)
    apply (case_tac ya, simp_all)
    apply (simp add: AND2_simp)
    apply (simp add: less_prod_def le_prod_def)
    apply (simp add: AND2_simp)
    apply (case_tac bb, simp_all)
    apply (case_tac ab, simp_all)
    apply (simp add: AND_def)
    apply (case_tac a, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def)

    apply (case_tac nat, simp_all)

    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp, safe)
    apply (case_tac ya, simp_all)
    apply (case_tac bb, simp_all)

    apply (case_tac nata, simp_all)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp, safe)
    apply (case_tac ya, simp_all)

    apply (simp add: less_prod_def le_prod_def le_option_def)

    by (simp add: less_prod_def le_prod_def le_option_def)


  lemma  [simp]: "InstFeedback (AND_rel2) (OK None) (OK ((Some True, Some True), Some True)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    apply (case_tac f, simp_all)
    apply (simp add: bot_prod_def bot_option_def)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp, safe)
    apply (case_tac ya, simp_all)
    apply (simp add: AND2_simp)
    apply (simp add: less_prod_def le_prod_def)
    apply (simp add: AND2_simp)
    apply (case_tac aa, simp_all)
    apply (case_tac bb, simp_all)
    apply (case_tac ab, simp_all)
    apply (simp add: AND_def)
    apply (case_tac ac, simp_all)
    apply (simp add: AND_def)
    apply (case_tac ac, simp_all)
    apply (simp add: AND2_simp)
    apply (case_tac f, simp_all)

    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp, safe)
    apply (case_tac ya, simp_all)
    apply (simp add: AND2_simp)
    apply (simp add: less_prod_def le_prod_def)
    apply (simp add: AND2_simp)
    apply (case_tac bb, simp_all)
    apply (case_tac ab, simp_all)
    apply (simp add: AND_def)
    apply (case_tac a, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def)
    apply (case_tac ab, simp_all)
    by (case_tac a, simp_all)

  lemma  [simp]: "InstFeedback ( AND_rel2) (OK None) (OK ((Some True, None), Some True)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)
 
  lemma [simp]: "InstFeedback ( AND_rel2) (OK None) (OK ((Some True, Some False), Some True)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)

  lemma fb_and_wire_bot: "InstFeedback (AND_rel2) (OK None) (OK ((v, w), y)) = (v = y ∧ v = w ∧ v = None)"
    apply safe
    apply (frule fb_hide_and_eq, simp)
    apply (frule fb_hide_and_eq, simp)
    apply (case_tac y, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac aa, simp_all)
    apply (case_tac aa, simp_all)

    apply (frule fb_hide_and_eq, simp)
    apply (case_tac y, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac aa, simp_all)
    by (case_tac aa, simp_all)

(* Case x = Some False *)

  lemma fb_and_wire_false: "InstFeedback (AND_rel2) (OK (Some False)) (OK ((v, w), y)) = (v = Some False ∧ w = v ∧ y = v)"
    apply safe
    apply (frule fb_hide_and_eq)
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe)
    apply (case_tac ya, simp_all)
    apply (case_tac x2, simp_all)
    apply (safe, simp_all)
    apply (case_tac f, simp_all)
    apply (simp_all add: bot_prod_def bot_option_def, safe, simp_all)
    apply (case_tac b, simp_all)
    apply (case_tac x2, simp_all)
    apply (frule fb_a_id, simp_all)
    apply (safe)
    apply (unfold AND2_simp, safe, simp)

    apply (frule fb_hide_and_eq)

    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe)
    apply (case_tac ya, simp_all)
    apply (case_tac x2, simp_all)
    apply (safe, simp_all)
    apply (case_tac f, simp_all)
    apply (simp_all add: bot_prod_def bot_option_def, safe, simp_all)
    apply (case_tac b, simp_all)
    apply (case_tac x2, simp_all)
    apply (frule fb_a_id, simp_all)
    apply (safe)
    apply (unfold AND2_simp, safe)
    apply (frule fb_hide_and_eq, simp)

    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def)
    apply (rule_tac x = "OK ((Some False, Some False), Some False)" in exI)
    apply (simp)
    apply (rule_tac x = "Suc (Suc 0)" in exI, simp)
    apply (simp add: OO_def)
    apply (rule_tac x = "OK ((Some False, ⊥), Some False)" in exI)
    apply (simp_all add: bot_prod_def AND2_simp bot_option_def)
    by (simp_all add: less_prod_def le_prod_def le_option_def bot_prod_def bot_option_def)

(* OK (Some True) *)

  lemma [simp]: "InstFeedback (AND_rel2) (OK (Some True)) (OK ((None, Some False), None)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def)
    apply safe
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (case_tac a, simp_all)
    by (simp add: AND2_simp)

  lemma [simp]: " (∃b. None = AND b (Some True))"
    apply (rule_tac x = None in exI)
    by (simp add: AND_def)

  lemma [simp]: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((None, None), None))"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def)
    apply (rule_tac x = "OK ((None, None), Some True)" in exI)
    apply (simp, safe)
    apply (rule_tac x = "0" in exI)
    apply (metis bot_option_def bot_prod_def relpowp_0_I)
    by (simp add: AND_def)
 
  lemma [simp]: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((None, Some True), None)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def)
    apply safe
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    by (simp add: AND2_simp)

  lemma [simp]: "InstFeedback (AND_rel2) (OK (Some True)) (OK ((Some False, None), Some False)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)
 
  lemma [simp]: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((Some False, Some True), Some False)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)

  lemma [simp]: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((Some False, Some False), Some False)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    apply (case_tac f, simp_all)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all, safe)
    apply (simp add: AND2_simp)
    apply (case_tac bb, simp_all)
    apply (case_tac aa, simp_all, safe, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def)
    apply (simp add: AND2_simp)

    apply (case_tac a, simp_all)
    apply (case_tac f, simp_all)
    apply (simp add: bot_prod_def bot_option_def)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all, safe)
    apply (simp add: AND2_simp, safe, simp)
    apply (case_tac bb, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def AND_def)
    apply (simp add: less_prod_def le_prod_def le_option_def)

    apply (case_tac f, simp_all)
    apply (simp add: bot_prod_def bot_option_def)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all, safe)
    apply (simp add: AND2_simp, safe, simp)
    apply (case_tac bb, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def AND_def)

    apply (case_tac nat, simp_all)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all, safe)
    apply (simp add: AND2_simp, safe, simp)
    apply (case_tac bb, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def AND_def)

    apply (case_tac nata, simp_all)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all, safe)
    apply (simp add: AND2_simp)
    apply (simp add: less_prod_def le_prod_def le_option_def AND_def)
    by (simp add: less_prod_def le_prod_def le_option_def)


  lemma [simp]: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((Some True, Some True), Some True)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    apply (simp add: AND_def)
    apply (simp add: AND2_simp AND_def, safe, simp)
    apply (case_tac f, simp_all)
    apply (simp add: bot_prod_def bot_option_def)
    apply (simp add: OO_def, safe)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp_all, safe)
    apply (simp add: AND2_simp, safe, simp)
    apply (case_tac bb, simp_all)
    apply (simp add: less_prod_def le_prod_def le_option_def AND_def)
    by (simp add: less_prod_def le_prod_def le_option_def)

  lemma [simp]: "InstFeedback (AND_rel2) (OK (Some True)) (OK ((Some True, None), Some True)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)
 
  lemma [simp]: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((Some True, Some False), Some True)) = False"
    apply (simp add: InstFeedback_simp fun_eq_iff rtranclp_is_Sup_relpowp OO_def fb_begin_def, safe, simp)
    apply (case_tac y, simp_all)
    apply (case_tac x2, simp)
    apply (safe, simp_all)
    apply (case_tac bc, simp_all)
    apply (simp add: AND2_simp)
    by (simp add: AND2_simp)


  lemma fb_and_wire_true: "InstFeedback ( AND_rel2) (OK (Some True)) (OK ((v, w), y)) = (v = y ∧ v = w ∧ v = None)"
    apply safe
    apply simp_all
    apply (frule fb_hide_and_eq, simp)
    apply (frule fb_hide_and_eq, simp)
    apply (case_tac y, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac aa, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac aa, simp_all)

    apply (frule fb_hide_and_eq, simp)
    apply (case_tac y, simp_all)
    apply (case_tac w, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac aa, simp_all)
    by (case_tac aa, simp_all)

  thm fb_and_wire_true
  thm fb_and_wire_false
  thm fb_and_wire_bot


  lemma "InstFeedback (AND_rel2) x y = (case x of ∙ ⇒ y = ∙ | OK (Some False) ⇒ y = OK ((Some False, Some False), Some False) | _ ⇒ y = OK ((None, None), None) )"
    apply (case_tac x, simp_all)
    apply (simp add: InstFeedback_def)
    apply (case_tac y, simp_all)
    apply (simp add: InstFeedback_def)
    apply (case_tac x2, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac x2a, simp)
    apply (case_tac a, simp)
    apply(case_tac x2, simp_all)
    apply (simp add: fb_and_wire_bot)
    apply auto [1]
    apply (case_tac ab, simp_all)
    apply (simp add: fb_and_wire_true)
    apply auto [1]
    apply (simp add: fb_and_wire_false)
    by auto [1]

  definition "NonDet ux vy  = (case ux of ∙ ⇒ vy = ∙ | OK (Some u, x) ⇒ 
    (if u = 2 then vy = ∙ else 
      vy = OK(Some (x + 1), x + 1) ∨ vy = OK(Some (x + 1), x + 2) ∨
      vy = OK(Some (x + 2), x + 2) ∨ vy = OK(Some (x + 2), x + 3) ∨
      vy = OK(Some 6, 6) ∨ vy = OK(Some 6, 7))
    | OK(None, x) ⇒  
      vy = OK(Some (x + 1), x + 1) ∨ vy = OK(Some (x + 1), x + 2) ∨
      vy = OK(Some (x + 2), x + 2) ∨ vy = OK(Some (x + 2), x + 3) ∨
      vy = OK(Some 7, 7) ∨ vy = OK(Some 7, 8) )"

  definition "InstFeedbackNonDet x vy = (case x of ∙ ⇒ vy = ∙ |
    OK a ⇒ (a = Suc 0 ∧ vy = ∙) ∨ (a = 0 ∧ vy = ∙) ∨
    (a ≠ 1 ∧ (vy = OK(Some (a + 1), a + 1) ∨ vy = OK(Some (a + 1), a + 2))) ∨
    (a ≠ 0 ∧ (vy = OK(Some (a + 2), a + 2) ∨ vy = OK(Some (a + 2), a + 3))))"

  lemma InstFeedbackNonDet_a: "InstFeedback NonDet x vy ⟹ InstFeedbackNonDet x vy"

    apply (simp add: InstFeedback_simp fba_a_pair fb_begin_def fb_b_def InstFeedbackNonDet_def, safe)
    apply simp_all
    apply (case_tac x, simp_all)
    apply (simp add: NonDet_def bot_option_def)
    apply (case_tac x, simp_all)
    apply (case_tac ba, simp_all)
    apply (simp add: NonDet_def bot_option_def fb_a_def)
    apply (simp add: NonDet_def bot_option_def fb_a_def)
    apply (case_tac x2a, simp_all)
    apply (case_tac a, simp_all)
    apply (case_tac "aa = 2", simp_all)
    apply safe
    apply simp_all
    apply (case_tac ba, simp_all)
    apply (case_tac x, simp_all)
    apply (simp add: NonDet_def bot_option_def fb_a_def)
    apply (case_tac bb, simp_all)
    apply (simp add: NonDet_def bot_option_def fb_a_def)
    apply auto [1]
    apply (case_tac "x2 = 1", simp_all)
    apply (case_tac "x2 = 1", simp_all)
    apply (simp add: NonDet_def bot_option_def fb_a_def)
    apply auto [1]
    apply (case_tac aa, simp_all)
    apply (case_tac u', simp_all)
    apply (case_tac "ab = 2", simp_all)
    apply (case_tac x, simp_all)
    apply auto [1]
    apply auto [1]
    apply (case_tac "ab = 2", simp_all)
    apply (simp add: less_option_def le_option_def)
    apply auto [1]
    apply (case_tac aa, simp_all)
    apply (simp add: less_option_def le_option_def)
    apply auto [1]
    apply (case_tac "ab = 2", simp_all)
    apply (case_tac u', simp_all)
    apply (case_tac "aa = 2", simp_all)
    by (simp add: less_option_def le_option_def)
    
  lemma InstFeedbackNonDet_b: "InstFeedbackNonDet x vy ⟹ InstFeedback NonDet x vy"
    apply (simp add: InstFeedbackNonDet_def)
    apply (case_tac x, simp_all)
    apply safe
    apply (simp add: InstFeedback_def)

    apply (simp add: InstFeedback_def)
    apply (rule_tac x = 1 in exI)
    apply (rule_tac x = "λ i. (if i = 0 then None else Some 2)" in exI)
    apply (simp add: bot_option_def)
    apply (simp add: NonDet_def, auto)

    apply (simp add: InstFeedback_def)
    apply (rule_tac x = 1 in exI)
    apply (rule_tac x = "λ i. (if i = 0 then None else Some 2)" in exI)
    apply (simp add: bot_option_def)
    apply (simp add: NonDet_def, auto)

    apply (simp add: InstFeedback_def)
    apply (rule_tac x = 1 in exI, simp)
    apply (rule_tac x = "λ i. (if i = 0 then None else Some (Suc x2))" in exI)
    apply (simp add: bot_option_def)
    apply (simp add: NonDet_def, auto)

    apply (simp add: InstFeedback_def)
    apply (rule_tac x = 1 in exI, simp)
    apply (rule_tac x = "λ i. (if i = 0 then None else Some (Suc x2))" in exI)
    apply (simp add: bot_option_def)
    apply (simp add: NonDet_def, auto)

    apply (simp add: InstFeedback_def)
    apply (rule_tac x = 1 in exI, simp)
    apply (rule_tac x = "λ i. (if i = 0 then None else Some (Suc (Suc x2)))" in exI)
    apply (simp add: bot_option_def)
    apply (simp add: NonDet_def, auto)

    apply (simp add: InstFeedback_def)
    apply (rule_tac x = 1 in exI, simp)
    apply (rule_tac x = "λ i. (if i = 0 then None else Some (Suc (Suc x2)))" in exI)
    apply (simp add: bot_option_def)
    by (simp add: NonDet_def, auto)

   lemma InstFeedbackNonDet: "InstFeedback NonDet = InstFeedbackNonDet"
    apply (simp add: fun_eq_iff, safe)
    apply (rule InstFeedbackNonDet_a, simp)
    by (rule InstFeedbackNonDet_b, simp)

subsection‹\label{FeedbackAssoc}Associativity of Instantaneous  Feedback›

  definition "adapt r a b = (case a of ∙ ⇒ b = ∙ | OK (u, (v, x)) ⇒ 
         (∃ u' v' y . r (OK ((u,v), x)) (OK (((u',v'),y))) ∧ b = OK (u', (v', y))) ∨ (r (OK ((u,v), x)) ∙ ∧ b = ∙))"

  definition "adapt_b a b = (case a of ∙ ⇒ b = ∙ | OK (u, (v, x)) ⇒ b = OK (v, (u, x)))"

  definition "adapt_c x y = (case x of ∙ ⇒ y = ∙ |
       OK (w, (u, a)) ⇒ y = OK ((u, w), a))"

  definition "adapt_a x y = (case x of ∙ ⇒ y = ∙ | OK (u, (v, x)) ⇒ y = OK ((u, v), x))"

  lemma "ff r ⟹ f_f r ⟹ adapt r = adapt_a OO r OO adapt_a¯¯"
    apply (simp add: adapt_a_def adapt_def fun_eq_iff OO_def ff_def f_f_def)
    apply auto
    apply (case_tac x, simp_all)
    apply (case_tac x2, simp_all)
    apply auto
    apply (case_tac x, simp_all)
    apply (case_tac xa, simp_all) 
    apply (case_tac x2, simp_all)
    apply auto [1]
    apply (case_tac x2, simp_all)
    by (case_tac xa, auto)

  lemma [simp]: "unkn_mono r ⟹ unkn_mono (adapt r)"
    apply (simp add: unkn_mono_def adapt_def le_fun_def, auto)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = aa in spec)
    apply (drule_tac x = b in spec)
    apply (drule_tac x = aa in spec, auto)
    by (simp add: le_prod_def)

(******************)
  lemma [simp]:  "(case y of ∙ ⇒ OK (b, a, yaa) = ∙ | OK (u, v, x) ⇒ OK (b, a, yaa) = OK (v, u, x))
     = (y = OK (a, b, yaa))"
     apply (case_tac y, simp_all)
     by (case_tac x2, auto)

  lemma [simp]: " (case y of ∙ ⇒ OK ((a, b), yaa) = ∙ | OK (w, u, aa) ⇒ OK ((a, b), yaa) = OK ((u, w), aa))
   = (y = OK (b, a, yaa))"
     apply (case_tac y, simp_all)
     by (case_tac x2, auto)

  lemma [simp]: "  (case y of ∙ ⇒ ∙ = ∙ | OK (w, u, a) ⇒ ∙ = OK ((u, w), a)) = (y = ∙)"
     by (case_tac y, simp_all)

  lemma [simp]: "unkn_mono r ⟹ r (OK ((a, b), x2)) (OK ((u, v), z)) ⟹ r (OK ((⊥, ⊥), x2)) (OK ((u, v), z))"
    apply (simp add: unkn_mono_def)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = b in spec)
    by (simp add: le_prod_def)

  lemma [simp]: "unkn_mono r ⟹ r (OK ((a, b), x2)) (OK ((u, v), z)) ⟹ r (OK ((⊥, b), x2)) (OK ((u, v), z))"
    apply (simp add: unkn_mono_def)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = b in spec)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = b in spec)
    by (simp add: le_prod_def)

  lemma [simp]: "unkn_mono r ⟹ r (OK ((a, b), x2)) (OK ((u, v), z)) ⟹ r (OK ((a, ⊥), x2)) (OK ((u, v), z))"
    apply (simp add: unkn_mono_def)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = b in spec)
    by (simp add: le_prod_def)

(******************)

  lemma [simp]: "unkn_mono r ⟹ unkn_mono (InstFeedback (adapt r) OO adapt_b)"
    apply (simp add: unkn_mono_fb_fun [THEN sym])
    apply (simp add: unkn_mono_def le_fun_def OO_def, auto)
    apply (rule_tac x = y in exI, simp_all)
    apply (simp add: adapt_def le_fun_def InstFeedback_1_def adapt_b_def, auto)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = b in spec, auto)
    apply (simp_all add: le_prod_def)
    apply blast

    apply (drule_tac x = ⊥ in spec)
    apply (drule_tac x = a in spec)
    apply (simp_all add: le_prod_def)
    apply blast


    apply (drule_tac x = ab in spec)
    apply (drule_tac x = a in spec)
    apply (drule_tac x = ab in spec)
    by (drule_tac x = b in spec, auto)

  term "InstFeedback (fb_fun (adapt r) OO adapt_b) OO adapt_c"


  lemma fb_hide_comp_aux: "unkn_mono (InstFeedback (adapt r) OO adapt_b) ⟹ InstFeedback (InstFeedback (adapt r) OO adapt_b) = InstFeedback_1 (InstFeedback (adapt r) OO adapt_b)"
    by (simp add:  unkn_mono_fb_fun [THEN sym])

  lemma [simp]: "adapt r ∙ ∙"
    by (simp add: adapt_def)

  lemma [simp]: "adapt_b ∙ ∙"
    by (simp add: adapt_b_def)

  lemma [simp]: "adapt_c ∙ ∙"
    by (simp add: adapt_c_def)

  lemma [simp]: "unkn_mono r ⟹
      r (OK ((⊥, ⊥), x2)) (OK ((a, b), ya)) ⟹ 
      r (OK ((a, b), x2)) (OK ((a, b), yaa)) ⟹
      InstFeedback_1 (adapt r) (OK (⊥, x2)) (OK (a, b, yaa))"
    apply (simp add: InstFeedback_1_def adapt_def)
    by (auto)

  lemma [simp]: "unkn_mono r ⟹
      r (OK ((⊥, ⊥), x2)) (OK ((a, b), ya)) ⟹ 
      r (OK ((a, b), x2)) (OK ((a, b), yaa)) ⟹
      ∃a ba. InstFeedback_1 (adapt r) (OK (⊥, x2)) (OK (a, b, ba))"
    apply (rule_tac x = a in exI)
    by (rule_tac x = yaa in exI, simp)

  lemma [simp]: "unkn_mono r ⟹
      r (OK ((⊥, ⊥), x2)) (OK ((a, b), ya)) ⟹ 
      r (OK ((a, b), x2)) (OK ((a, b), yaa)) ⟹
      InstFeedback_1 (adapt r) (OK (b, x2)) (OK (a, b, yaa))"
    apply (simp add: InstFeedback_1_def adapt_def)
    apply (auto)
    apply (rule_tac x = b in exI)
    apply (rule_tac x = yaa in exI)
    by simp

  definition "indep r = (∀ x y z z' . r (OK ((⊥,⊥), z)) (OK ((x, y), z')) ⟶ 
          ((∃ a . r (OK ((x, ⊥), z)) (OK ((x, y), a))) ∧ ((∃ a . r (OK ((⊥, y), z)) (OK ((x, y), a))))))"

  lemma InstFeedback_assoc_fail_a: "indep r ⟹  unkn_mono r ⟹ InstFeedback r  x ∙ ⟹ ((InstFeedback (InstFeedback (adapt r) OO adapt_b)) OO adapt_c) x ∙"
    apply (simp add: fb_hide_comp_aux)
    apply (simp add:   unkn_mono_fb_fun [THEN sym])
    apply (case_tac x, simp_all)
    apply (simp add: OO_def)
    apply (simp add: InstFeedback_1_def adapt_c_def)

    apply (subst (asm) InstFeedback_1_def, simp, safe)
    apply (simp_all add: bot_prod_def OO_def adapt_c_def, safe)

   apply (simp add: InstFeedback_1_def adapt_def adapt_b_def, safe, simp)
   apply (drule_tac x = b in spec, safe, simp_all)
   apply blast
   apply (drule_tac x = a in spec, simp, safe)
   apply blast
   apply (simp add: indep_def)
   apply blast
   apply (drule_tac x = a in spec, simp)
   apply (simp add: indep_def)
   apply blast

   apply (simp add: InstFeedback_1_def adapt_def adapt_b_def, safe, simp)
   apply (case_tac "a = ⊥", simp_all)
   apply (drule_tac x = b in spec, simp, safe)
   apply (drule_tac x = ⊥ in spec, simp)
   apply (drule_tac x = b in spec, simp, safe)
   apply (drule_tac x = a in spec)
   apply (simp add: indep_def)
   apply blast
   apply (drule_tac x = a in spec, simp)
   apply (simp add: indep_def)
   apply blast
   
   by (simp add: InstFeedback_1_def adapt_def adapt_b_def)

  definition "indep_a r = (∀ x y y' a b a' b' . r (OK ((⊥, ⊥), x)) (OK ((a, b), y)) ∧ r (OK ((⊥, ⊥), x)) (OK ((a', b'), y'))
      ⟶ (∃ z . r (OK ((⊥, ⊥),x)) (OK ((a, b'), z))))"

  lemma InstFeedback_assoc_fail_b: "indep_a r ⟹  mono_fail r ⟹ unkn_mono r ⟹  ((InstFeedback (InstFeedback (adapt r) OO adapt_b)) OO adapt_c) x ∙ ⟹ InstFeedback r  x ∙"
    apply (simp add: fb_hide_comp_aux)
    apply (simp add:  unkn_mono_fb_fun [THEN sym])
    apply (case_tac x, simp_all)
    apply (simp add: OO_def)
    apply (simp add: InstFeedback_1_def adapt_c_def)
 
   apply (simp add: InstFeedback_1_def adapt_def adapt_b_def)
   apply safe
   apply (simp_all add: bot_prod_def)
   prefer 4
   apply blast
   apply (simp add: indep_a_def)
   apply (drule_tac x = x2 in spec)
   apply (drule_tac x = ba in spec)
   apply (drule_tac x = b in spec)
   apply (drule_tac x = ab in spec)
   apply (drule_tac x = ac in spec)
   apply (drule_tac x = aa in spec)
   apply (drule_tac x = a in spec)
   apply simp
   apply safe
   apply blast

   apply (simp add: indep_a_def)
   apply (drule_tac x = x2 in spec)
   apply (drule_tac x = ba in spec)
   apply (drule_tac x = b in spec)
   apply (drule_tac x = ab in spec)
   apply (drule_tac x = ac in spec)
   apply (drule_tac x = ⊥ in spec)
   apply (drule_tac x = a in spec)
   apply simp
   apply safe
   apply blast

   apply (simp add: mono_fail_def)
   apply (drule_tac x = ⊥ in spec)
   apply (drule_tac x = a in spec)
   apply (drule_tac x = aa in spec)
   apply (drule_tac x = a in spec)
   apply (simp add: le_prod_def)
   apply (drule_tac x = x2 in spec, simp)
   apply (rule_tac x = aa in exI)
   apply (rule_tac x = a in exI)
   apply simp
   apply (rule_tac x = b in exI)
   apply simp

   apply (simp add: mono_fail_def)
   apply (drule_tac x = a in spec)
   apply (drule_tac x = ⊥ in spec)
   apply (drule_tac x = a in spec)
   apply (drule_tac x = aa in spec)
   apply (simp add: le_prod_def)
   apply (drule_tac x = x2 in spec, simp)
   apply (rule_tac x = a in exI)
   apply (rule_tac x = aa in exI)
   apply simp
   apply (rule_tac x = b in exI)
   by simp

  lemma InstFeedback_assoc_OK: "unkn_mono r ⟹ InstFeedback r  x (OK y) = ((InstFeedback (InstFeedback (adapt r) OO adapt_b)) OO adapt_c) x (OK y)"
    apply (simp add: fb_hide_comp_aux)
    apply (simp add:  unkn_mono_fb_fun [THEN sym])
    apply (case_tac x, simp_all)
    apply (simp add: OO_def)
    apply (simp add: InstFeedback_1_def adapt_c_def)

    apply safe
    apply (subst (asm) InstFeedback_1_def, simp, safe)
    apply (simp_all add: bot_prod_def OO_def adapt_c_def)
 
    apply (subst InstFeedback_1_def)
    apply (simp add: adapt_b_def)

    apply (simp add: InstFeedback_1_def adapt_def adapt_b_def)
    apply (case_tac b, simp_all)
    apply (case_tac x2a, simp_all)

    apply (simp add: InstFeedback_1_def adapt_def adapt_b_def bot_prod_def less_prod_def le_prod_def)
    apply safe
    apply auto
    apply (rule_tac x = c in exI, simp)
    apply (rule_tac x = c in exI, simp)
    apply (rule_tac x = c in exI, simp)
    apply (rule_tac x = c in exI, simp)
    apply (rule_tac x = c in exI, simp)
    by (rule_tac x = c in exI, simp)

  theorem InstFeedback_assoc: "indep r ⟹ indep_a r ⟹  mono_fail r ⟹ unkn_mono r ⟹  
    (InstFeedback (InstFeedback (adapt r) OO adapt_b)) OO adapt_c = InstFeedback r"
    apply (simp add: fun_eq_iff, safe)
    apply (case_tac xa, simp_all)
    apply (rule InstFeedback_assoc_fail_b, simp_all)
    apply ( simp add: OO_def, blast)
    apply ( simp add: InstFeedback_assoc_OK)
    apply ( simp add: OO_def, blast)
    apply (case_tac xa, simp_all)
    apply (rule InstFeedback_assoc_fail_a, simp_all)
    by ( simp add: InstFeedback_assoc_OK)

  definition "unkn_mono_up r = (∀ a b x u y. a ≤ b ∧ r (OK (a, x)) (OK (u, y)) ⟶ ((∃ v . u ≤ v ∧ r (OK (b, x)) (OK (v, y))) ∨ r (OK (b, x)) ∙))"
  lemma unkn_mono_up_A: "unkn_mono_up r ⟹ a ≤ b ⟹ r (OK (a, x)) (OK (u, y)) ⟹ ((∃ v . u ≤ v ∧ r (OK (b, x)) (OK (v, y))) ∨ r (OK (b, x)) ∙)"
    by (simp add: unkn_mono_up_def)
  lemma unkn_mono_a_A: "unkn_mono r ⟹ a ≤ b ⟹  r (OK (b, x)) (OK z) ⟹ r (OK (a, x)) (OK z)"
    by (simp add: unkn_mono_def)

  lemma feedback_comp_fail_Z: "mono_fail (r::(('a option × 'b option) × 'c) fail_option ⇒ ((('a option × 'b option) × 'd) fail_option) ⇒ bool) 
    ⟹  unkn_mono r ⟹ unkn_mono_up r ⟹ InstFeedback r x ∙ ⟹ ((InstFeedback (InstFeedback (adapt r) OO adapt_b)) OO adapt_c) x ∙"
    apply (simp add: fb_hide_comp_aux)
    apply (simp add:  unkn_mono_fb_fun [THEN sym])
    apply (case_tac x, simp_all)
    apply (simp add: OO_def)
    apply (simp add: InstFeedback_1_def adapt_c_def)

    apply (subst (asm) InstFeedback_1_def, simp, safe)
    apply (simp_all add: bot_prod_def OO_def adapt_c_def, safe)

   apply (simp add: InstFeedback_1_def adapt_def adapt_b_def, safe, simp)
   apply (drule_tac x = b in spec, safe, simp_all)
   apply blast
   apply (drule_tac x = a in spec, simp, safe)
   apply blast
   apply (rule_tac x = a in exI, simp_all)
   apply (case_tac b, simp_all)
   apply auto [1]
   apply (simp add: bot_option_def)
   apply (drule_tac a = "(⊥, ⊥)" and b = "(a, ⊥)" in unkn_mono_up_A)
   apply (simp add: le_prod_def le_option_def bot_option_def)
   apply simp_all
   apply (case_tac a, simp_all)
   apply (simp add: bot_option_def)
   apply safe
   apply (simp add: le_prod_def le_option_def)
   apply (simp add: le_prod_def le_option_def)
   apply auto [1]

   apply (rule_tac x = "a" in exI, simp)
   apply (case_tac b, simp_all)
   apply (simp add: bot_option_def)
   apply auto [1]
   apply (drule_tac x = a in spec, simp)

   apply (drule_tac a = "(⊥, ⊥)" and b = "(⊥, Some aa)" in unkn_mono_up_A)
   apply (simp add: le_prod_def le_option_def bot_option_def)
   apply simp_all
   apply safe
   apply (drule_tac a = "(⊥, ⊥)" and b = "(⊥, Some aa)" in unkn_mono_a_A)
   apply (simp add: le_prod_def)
   apply simp_all
   apply (case_tac a, simp add: bot_option_def)
   apply (simp add: le_prod_def le_option_def)
   apply (case_tac a, simp add: bot_option_def)
   apply (simp add: le_prod_def le_option_def)
   apply (simp add: InstFeedback_1_def adapt_def adapt_b_def, safe, simp)
   apply (case_tac "a = ⊥", simp_all)
   apply (drule_tac x = b in spec, simp, safe)
   apply (drule_tac x = ⊥ in spec, simp)
   apply (drule_tac x = b in spec, simp, safe)
   apply (drule_tac x = a in spec, simp)
   apply (rule_tac x = a in exI, safe, simp_all)
   apply (drule_tac x = y in spec, simp, safe, simp_all)
   apply auto [1]
   apply (drule_tac x = y in spec, simp, safe, simp_all)

   apply (drule_tac a = "(⊥, ⊥)" and b = "(a, ⊥)" in unkn_mono_up_A)
   apply (simp add: le_prod_def le_option_def bot_option_def)
   apply simp_all
   apply (case_tac a, simp_all)
   apply safe
   apply (simp add: le_prod_def le_option_def bot_option_def)

   apply (drule_tac x = a in spec, simp)
   apply (rule_tac x = a in exI, simp)

   apply (drule_tac a = "(⊥, ⊥)" and b = "(⊥, b)" in unkn_mono_up_A, simp_all)
   apply (simp add: le_prod_def le_option_def bot_option_def)
   apply safe
   apply (case_tac a, simp_all add: bot_option_def)
   apply (case_tac b, simp_all add: bot_option_def)
   apply (simp add: le_prod_def le_option_def bot_option_def)
   apply (simp add: le_prod_def le_option_def bot_option_def)
   apply (case_tac b, simp_all add: bot_option_def, safe, simp)

   apply (simp add: InstFeedback_1_def adapt_def adapt_b_def, safe, simp)
   by (simp add: bot_option_def)

end