Theory Synth_Rate

theory Synth_Rate
  imports Currs_Of
begin



lemma wfR''_zero[simp]: "wfR'' (λ_. 0)"
  unfolding wfR''_def by (auto simp: zero_acost_def)

lemma wfR''_supI:
  fixes R:: "'b ⇒ ('c, enat) acost"
  shows "wfR'' R ⟹ wfR'' R' ⟹ wfR'' (sup R R')"
  unfolding wfR''_def
  apply auto
  subgoal premises prems for f
    apply(rule finite_subset[where B="{s. the_acost (R s) f ≠ 0 ∨ the_acost (R' s) f ≠ 0}"])
    subgoal apply auto  
      by (simp add: sup_acost_def)    
    subgoal
      using prems[rule_format, of f]  
      using finite_Collect_disjI by fastforce   
    done
  done



lemma bindT_refine_conc_time_my_inres_sup:
  fixes m :: "('e1,('c1,enat)acost) nrest"
  fixes m' :: "('e2,('c2,enat)acost) nrest"
  assumes  " m ≤ ⇓R' (timerefine Em m')"
  "(⋀x x'. ⟦(x,x')∈R'; inres m' x'⟧
         ⟹ f x ≤ ⇓ R (timerefine Ef (f' x') ))"
  and E: "E = sup Em Ef"
  and "wfR'' Em"
      "wfR'' Ef"
shows "bindT m f ≤  ⇓ R (timerefine E (bindT m' f'))"
  apply(rule bindT_refine_conc_time2[where R=R])
  subgoal unfolding E apply(rule wfR''_supI) using assms by auto
   apply(rule order.trans)
    apply(rule assms(1))
   apply(rule nrest_Rel_mono)
  apply(rule timerefine_R_mono_wfR'')
  subgoal unfolding E apply(rule wfR''_supI) using assms by auto
  subgoal unfolding E by auto
   apply(rule order.trans)
   apply(rule assms(2))
    apply simp 
  subgoal by(auto dest: inres_if_inresT_acost)
   apply(rule nrest_Rel_mono)
  apply(rule timerefine_R_mono_wfR'')
  subgoal unfolding E apply(rule wfR''_supI) using assms by auto
  subgoal unfolding E by auto
  done


lemma timerefine_supI:
  fixes R :: "_ ⇒ ('a, enat) acost"
  assumes "x ≤ timerefine R y"
      "wfR'' R'" "wfR'' R"
  shows "x ≤ timerefine (sup R' R) y"
  apply(rule order.trans)
   apply(rule assms)
  apply(rule timerefine_R_mono_wfR'') 
  apply(rule wfR''_supI)
    apply fact+ apply(rule sup_ge2) done

lemma timerefine_supI2:
  fixes R :: "_ ⇒ ('a, enat) acost"
  assumes "x ≤ timerefine R y"
      "wfR'' R'" "wfR'' R"
    shows "x ≤ timerefine (sup R R') y"
  apply(subst sup.commute)
  by(rule timerefine_supI[OF assms])


lemma costmult_sup_distrib: "(a::enat) *m (sup b c) = sup (a *m b) (a *m c)"
  unfolding sup_acost_def costmult_def apply auto apply(rule ext)
  by (metis max.orderE max.orderI max_def max_enat_simps(2) mult.commute mult_right_mono sup_max) 

lemma MIf_refine_sup:
  fixes f :: "(_,(string, enat) acost) nrest"
  shows "(b,b')∈bool_rel ⟹ (b ⟹ f ≤ ⇓R (timerefine EIfa f'))
           ⟹ (¬b ⟹ g ≤ ⇓R (timerefine EIfb g')) ⟹ E= sup ((λ_. 0)(''call'':=cost ''call'' 1,''if'':=cost ''if'' 1)) (sup EIfa EIfb)  ⟹ 
       wfR'' EIfa  ⟹ wfR'' EIfb
       ⟹  MIf b f g  ≤ ⇓R (timerefine E (MIf b' f' g' ))"
  apply(rule MIf_refine)
  subgoal unfolding struct_preserving_def by (auto simp: costmult_sup_distrib norm_cost timerefineA_cost_apply_costmult)
  subgoal apply simp apply(intro wfR''_supI wfR''_upd) by auto
  apply simp
  subgoal premises pr 
      using pr apply - apply(rule order.trans) apply simp apply(rule nrest_Rel_mono)
      unfolding pr(4)
      apply(rule timerefine_R_mono_wfR'')
        subgoal apply(intro wfR''_supI wfR''_upd) by auto 
      apply(subst sup.left_commute)
      apply simp
      done
  subgoal premises pr 
      using pr apply - apply(rule order.trans) apply simp apply(rule nrest_Rel_mono)
      unfolding pr(4)
      apply(rule timerefine_R_mono_wfR'')
      subgoal apply(intro wfR''_supI wfR''_upd) by auto
      apply(subst (2) sup.commute)
      apply(subst sup.left_commute)
      apply simp
      done
    done


lemma SPECc2_refine_exch:
  shows  "(op x y, op' x' y')∈R  ⟹ (SPECc2 n op x y :: (_,(_,enat) acost)nrest) ≤ ⇓ R (timerefine ((λ_. 0)(n':=cost n 1)) (SPECc2 n' op' x' y'))"
  unfolding SPECc2_def
  supply [[unify_trace_failure]]
  apply(subst SPECT_refine_t) apply auto 
  apply(subst timerefineA_cost) by simp


end