Theory FeedbacklessHBDTranslation

theory FeedbacklessHBDTranslation
imports Diagrams Refinement
subsection{*Feedbackless HBD Translation*}

(* Was: AlgorithmFeedbackless.thy *)

theory FeedbacklessHBDTranslation imports Diagrams "../RefinementReactive/Refinement" 
context BaseOperationFeedbacklessVars
definition "WhileFeedbackless = 
    while_stm (λ As . internal As ≠ {})
        [:As ↝ As' . ∃ A . A ∈ set As ∧ (out A) ∈ internal As ∧  As'= map (CompA A) (As ⊖ [A]):]"
definition "TranslateHBDFeedbackless = WhileFeedbackless o [-(λ As . Parallel_list As)-]"

definition "ok_fbless As = (Deterministic As ∧ loop_free As ∧ Type_OK As)"
definition "TranslateHBDRec = {. ok_fbless .} 
    o [:As ↝ As' . ∃ L . perm (VarFB (Parallel_list As)) L ∧ As' = fb_less L As :]"
lemma [simp]:"{.As. length (VarFB (Parallel_list As)) = w.} (TranslateHBDRec x) y ⟹ [. - (λAs. internal As ≠ {}) .] x y"
  apply (simp add: TranslateHBDRec_def demonic_def assert_def le_fun_def assume_def, safe)
  apply (drule_tac x = y in spec, safe, simp)
  apply (drule_tac x = "[]" in spec, simp_all)
  by (simp add: internal_VarFB ok_fbless_def)
lemma internal_fb_less_step: "loop_free As ⟹ Type_OK As ⟹ A ∈ set As ⟹ out A ∈ internal As ⟹  internal (fb_less_step A (As ⊖ [A])) = internal As - {out A}"
  by (metis fb_out_less_step_def internal_fb_out_less_step mem_get_comp_out mem_get_other_out)
lemma ok_fbless_fb_less_step: "ok_fbless As ⟹ A ∈ set As ⟹ out A ∈ internal As ⟹ ok_fbless (fb_less_step A (As ⊖ [A]))"
  apply (simp add: ok_fbless_def, safe)
    apply (metis Deterministic_fb_out_less_step fb_out_less_step_def mem_get_comp_out mem_get_other_out)
   apply (metis fb_out_less_step_def loop_free_fb_out_less_step mem_get_comp_out mem_get_other_out)
    using Type_OK_fb_out_less_step_aux by blast
lemma map_CompA_fb_out_less_step: "Deterministic As ⟹
            loop_free As ⟹
            Type_OK As ⟹ A ∈ set As ⟹ out A ∈ internal As ⟹ map (CompA A) (As ⊖ [A]) = fb_out_less_step (out A) As"
  using fb_less_step_def fb_out_less_step_def mem_get_comp_out mem_get_other_out by presburger
lemma length_diff: "a ∈ set x ⟹ length (x ⊖ [a]) < length x"
  apply (induction x, simp_all, auto)
  using AAA_c by fastforce
thm perm_cons

lemma perm_cons_a: "⋀ y . a ∈ set x ⟹ distinct x ⟹ perm (x ⊖ [a]) y ⟹ perm x (a # y)"
  apply (subst perm_sym)
   apply (rule perm_cons, simp_all)
  by (subst perm_sym, simp_all)
lemma [simp]: "{.As. length (VarFB (Parallel_list As)) = w.} (TranslateHBDRec x) y ⟹
             [. λAs. internal As ≠ {} .]
              ([:As↝As'.∃A. A ∈ set As ∧ out A ∈ internal As ∧ As' = map (CompA A) (As ⊖ [A]):] 
                ({.As. length (VarFB (Parallel_list As)) < w.} (TranslateHBDRec x))) y"
  apply (simp add: assert_def demonic_def TranslateHBDRec_def le_fun_def assume_def ok_fbless_def, safe)
      apply (simp add: map_CompA_fb_out_less_step)
      apply (simp add: VarFB_fb_out_less_step_gen internal_VarFB)
    apply (rule length_diff, simp)
  using Deterministic_fb_out_less_step map_CompA_fb_out_less_step apply presburger
  using loop_free_fb_out_less_step map_CompA_fb_out_less_step apply presburger
  using Type_OK_fb_out_less_step_new map_CompA_fb_out_less_step apply blast
  apply (simp add: map_CompA_fb_out_less_step)
  apply (drule_tac x = "(fb_less L (fb_out_less_step (out A) y))" in spec, safe, simp)
  apply (drule_tac x = "out A #  L" in spec, simp)
  apply (simp add: VarFB_fb_out_less_step_gen internal_VarFB)
  apply (subgoal_tac "distinct (VarFB (Parallel_list y))")
    apply (simp add: perm_cons_a)
    apply (simp add: VarFB_def Var_def)
    using distinct_inter io_diagram_distinct(2) io_diagram_parallel_list by blast
lemma Feedbackless_Rec_While_refinement: "TranslateHBDRec ≤ WhileFeedbackless"
  apply (simp add: WhileFeedbackless_def)
  apply (simp add: while_stm_def)
  apply (rule_tac p = "λ n . {. As . length (VarFB (Parallel_list As)) = n .} o TranslateHBDRec" in lfp_wf_induction_b)
    apply simp_all
  apply safe
    by (simp add: if_stm_def)

lemma [simp]:  "TranslateHBDRec o [-(λ As . Parallel_list As)-] ≤ TranslateHBDFeedbackless"
  apply (simp add: TranslateHBDFeedbackless_def)
  using Feedbackless_Rec_While_refinement by (simp add: le_fun_def)
thm FB_fb_less(1)

lemma Out_Parallel_fb_less: "⋀ As . Type_OK As ⟹ loop_free As ⟹ distinct L ⟹ set L ⊆ internal As ⟹ 
      Out (Parallel_list (fb_less L As)) = concat (map Out As) ⊖ L"
  proof (induction L)
    case Nil
    then show ?case by (simp add: Out_Parallel)
    case (Cons a L)
    have "a ∈ internal As"
      using Cons(5) by simp
    have [simp]: "Type_OK (fb_out_less_step a As)"
      using Cons(2)
      using Type_OK_fb_out_less_step_new ‹a ∈ internal As› by blast

    have A: "Out (Parallel_list (fb_less L (fb_out_less_step a As))) = concat (map Out (fb_out_less_step a As)) ⊖ L"
      apply (rule Cons(1))
         apply simp
        apply (simp add: Cons.prems(2) ‹a ∈ internal As› local.Cons(2) loop_free_fb_out_less_step_internal)
      using Cons(4) apply simp
      by (metis Cons.prems(2) Cons.prems(3) Cons.prems(4) Diff_empty ‹a ∈ internal As› distinct.simps(2) 
          internal_fb_out_less_step local.Cons(2) order_trans set_subset_Cons subset_Diff_insert)
  define A where "A = get_comp_out a As"
  have [simp]: "A ∈ set As"
    using A_def Cons(5) by auto[1]
  from this have length_Out_A: "length (Out A) = 1"
    using ‹Type_OK As› by (unfold Type_OK_def, simp) 
  from this have "Out A = [out A]"
    by (simp add: Out_out)
  have "a ∈ set (Out A)"
    by (simp add: ‹A ≡ get_comp_out a As›)
  have Out_a: "out A = a"
    using ‹Out A = [out A]› ‹a ∈ set (Out A)› by auto
  have [simp]: "get_other_out a As = As ⊖ [A]"
    using Out_a ‹A ∈ set As› local.Cons(2) mem_get_other_out by blast
  have B: "concat (map Out (As ⊖ [A])) = concat (map Out As) ⊖ [a]"
    by (metis ‹get_other_out a As = As ⊖ [A]› concat_map_Out_get_other_out local.Cons(2))
    show ?case
      apply (simp add: A)
      apply (simp add: fb_out_less_step_def fb_less_step_def A_def [THEN sym])
      using length_Out_A  apply (simp add: BBB_b B)
      by (metis diff_cons)
lemma io_diagram_distinct_VarFB: "io_diagram A ⟹ distinct (VarFB A)"
  apply (simp add: VarFB_def)
  by (simp add: io_diagram_distinct(2))
theorem fbless_correctness: "ok_fbless As ⟹ perm (VarFB (Parallel_list As)) L ⟹
    in_equiv (FB (Parallel_list As)) (Parallel_list (fb_less L As))"
proof (simp add:  ok_fbless_def, safe)
  assume [simp]: "Deterministic As"
  assume [simp]: "loop_free As"
  assume [simp]: "Type_OK As"
  assume P[simp]: "VarFB (Parallel_list As) <~~> L"
  define X where "X = Parallel_list As"
  define Y where "Y = Parallel_list (fb_less L As)"
  have [simp]: "In (FB (Parallel_list As)) = InFB X"
    apply (simp add: X_def [THEN sym] Y_def [THEN sym])
    by (simp add: FB_def Let_def InFB_def [THEN sym] VarFB_def [THEN sym])
  have [simp]: "In (FB (Parallel_list As)) <~~> In (Parallel_list (fb_less L As))"
    apply (simp add:  Y_def [THEN sym])
    by (rule_tac As = As and L = L in FB_fb_less(2), simp_all add: X_def Y_def)
  have length_VarFB_X: "length (VarFB X) =  length L"
    by (simp add: ListProp.perm_length X_def)
  have fb_perm_eq: "fb_perm_eq X"
    apply (simp add: X_def)
    by (rule fb_perm_eq_Parallel_list, simp_all)
  have [simp]: " Trs (FB (Parallel_list As)) 
      = [In (FB (Parallel_list As)) ↝ In (Parallel_list (fb_less L As))] oo Trs (Parallel_list (fb_less L As))"
    apply (simp add: Y_def [THEN sym])
    apply (subst FB_fb_less(1) [THEN sym, of As _ L])
          apply simp_all
      apply (simp add: X_def)
      apply (simp add: X_def)
     apply (simp add: Y_def)
    apply (simp add: FB_def Let_def VarFB_def [THEN sym] X_def [THEN sym] InFB_def [THEN sym])
    using fb_perm_eq apply (simp add: fb_perm_eq_def)
    apply (drule_tac x = L in spec, safe)
     apply (simp_all add: length_VarFB_X OutFB_def)
    using ListProp.perm_sym X_def ‹VarFB (Parallel_list As) <~~> L› by blast
  have A: "distinct (VarFB (Parallel_list As))"
    by (simp add: io_diagram_parallel_list)

    have [simp]: "Out (FB (Parallel_list As)) = Out (Parallel_list (fb_less L As))"
      apply (simp add: FB_def Let_def X_def [THEN sym])
      apply (subst Out_Parallel_fb_less, simp_all)
      using A P
      using dist_perm apply blast
       apply (simp add: internal_VarFB)
        by (metis Out_Parallel P VarFB_def X_def perm_diff_eq)
  show "in_equiv (FB (Parallel_list As)) (Parallel_list (fb_less L As))"
    apply (simp add: in_equiv_def)
    using ‹In (FB (Parallel_list As)) <~~> In (Parallel_list (fb_less L As))› by simp

lemma Hoare_TranslateHBDRec: "Hoare (λ As . As = As_init ∧ ok_fbless As) 
    (TranslateHBDRec o [-(λ As . Parallel_list As)-]) 
    (λ A . in_equiv (FB (Parallel_list As_init)) A)"
  apply (simp add: Hoare_def le_fun_def TranslateHBDRec_def update_def demonic_def assert_def ok_fbless_def, safe)
  by (rule fbless_correctness, simp_all add: ok_fbless_def)
theorem TranslateHBDFeedbacklessCorrectness: "Hoare (λ As . As = As_init ∧ ok_fbless As) 
    (λ A . in_equiv (FB (Parallel_list As_init)) A)"
  apply (rule_tac S = "(TranslateHBDRec o [-(λ As . Parallel_list As)-]) " in  refinement_hoare)
   apply simp_all
  by (simp add: Hoare_TranslateHBDRec)