Theory Data_Refinement

✐‹creator "Maximilian P. L. Haslbeck"›
✐‹contributor "Peter Lammich"›
section ‹Data Refinement›
theory Data_Refinement
imports NREST  NREST_Type_Classes
begin

paragraph ‹Summary›
text ‹This theory introduces data refinement.›

subsection ‹Definition›


definition conc_fun  ("⇓") where
  "conc_fun R m ≡ case m of FAILi ⇒ FAILT | REST X ⇒ REST (λc. Sup {X a| a. (c,a)∈R})"

definition abs_fun ("⇑") where
  "abs_fun R m ≡ case m of FAILi ⇒ FAILT 
    | REST X ⇒ if dom X⊆Domain R then REST (λa. Sup {X c| c. (c,a)∈R}) else FAILT"

lemma 
  conc_fun_FAIL[simp]: "⇓R FAILT = FAILT" and
  conc_fun_RES: "⇓R (REST X) = REST (λc. Sup {X a| a. (c,a)∈R})"
  unfolding conc_fun_def by (auto split: nrest.split)

lemma 
  abs_fun_FAIL[simp]: "⇑R FAILT = FAILT" and
  abs_fun_RES: "⇑R (REST X) = (if dom X⊆Domain R then REST (λa. Sup {X c| c. (c,a)∈R}) else FAILT)"
  unfolding abs_fun_def by (auto split: nrest.split)


lemma conc_fun_spec_ne_FAIL[simp]: "⇓R (SPECT M) ≠ FAILT" by (simp add: conc_fun_RES)   

text ‹a counter example›
notepad begin
  ⌦‹
  fix m m' :: "bool ⇒ ( (string,enat) acost) option" and R co x
  assume m: "m = [ True ↦ acostC ((λ_. 0)(''a'':=2,''b'':=2)) ]"
  
  assume m': "m' = [ True ↦ acostC ((λ_. 0)(''a'':=1,''b'':=2)), False ↦ acostC ((λ_. 0)(''a'':=2,''b'':=1))]"
  assume "m ≤ (λc. Sup {m' a |a. (c, a) ∈ R})"
        "m x = Some co"
  assume R_def: "R = {(True,False), (True,True)}"
  have i: "(λc. Sup {m' a |a. (c, a) ∈ R}) = [ True ↦ acostC ((λ_. 0)(''a'':=2,''b'':=2)) ]"
    apply (rule ext)
    subgoal for c
      apply(cases c)
      subgoal unfolding R_def m' apply auto unfolding Sup_option_def apply auto
        unfolding Sup_acost_def apply auto apply(rule ext) sorry         
      subgoal unfolding R_def by (simp add: bot_option_def) 
      done
    done
  have "m ≤ (λc. Sup {m' a |a. (c, a) ∈ R})"
    unfolding i m by simp
  have "∃x'. (x, x') ∈ R ∧ (∃c'≥co. m' x' = Some c')" 
    sorry
›
end
    


lemma SupSup_2: "Sup {m a |a. (c, a) ∈ R O S} =  Sup {m a |a b. (b,a)∈S ∧ (c,b)∈R }"
proof -
  have i: "⋀a. (c,a) ∈ R O S ⟷ (∃b. (b,a)∈S ∧ (c,b)∈R)" by auto
  have "Sup {m a |a. (c, a) ∈ R O S} = Sup {m a |a. (∃b. (b,a)∈S ∧ (c,b)∈R)}" 
      unfolding i by auto
    also have "...  = Sup {m a |a b. (b,a)∈S ∧ (c,b)∈R}" by auto
    finally show ?thesis .
  qed


lemma 
  fixes m :: "'a ⇒ ('c::complete_lattice) option"
  shows SupSup: "Sup {Sup {m aa |aa. P a aa c} |a. Q a c} = Sup {m aa |a aa. P a aa c ∧ Q a c}"
  apply(rule antisym)
   subgoal apply(rule Sup_least)
     by (auto intro: Sup_subset_mono)
   subgoal 
     unfolding Sup_le_iff apply auto
     by (smt Sup_upper Sup_upper2 mem_Collect_eq)
   done 


lemma 
  fixes m :: "'a ⇒ ('c::complete_lattice) option"
  shows 
    SupSup_1: "Sup {Sup {m aa |aa. (a, aa) ∈ S} |a. (c, a) ∈ R} = Sup {m aa |a aa. (a,aa)∈S ∧ (c,a)∈R}"
  by(rule SupSup)



lemma project_acost_conc_fun_commute[refine_pw_simps]: "project_acost b (⇓R m) = ⇓R (project_acost b m)"
  unfolding project_acost_def conc_fun_def
  apply(cases m)
  subgoal by simp
  subgoal
    supply *[simp] = continuous_option'[OF continuous_the_acost, THEN continuousD]
    apply simp
    apply(rule ext)
    apply(rule arg_cong[where f=Sup])
    by auto
  done
 


(* 
lemma conc_fun_RES_sv: "single_valued R ⟹ 
  ⇓R (REST X) = REST (λc. if c∈Dom R then Some (X Sup {X a| a. (c,a)∈R})"
*)

lemma nrest_Rel_mono:
  fixes A :: "('a,'b::{complete_lattice,monoid_add}) nrest"
  shows "A ≤ B ⟹ ⇓ R A ≤ ⇓ R B"
  unfolding conc_fun_def
  apply (auto split: nrest.split simp: le_fun_def)  
  by (smt complete_lattice_class.Sup_mono mem_Collect_eq)   


declare nrest_Rel_mono[trans]


lemma pw_conc_nofail[refine_pw_simps]: 
  "nofailT (⇓R S) = nofailT S"
  by (cases S) (auto simp: conc_fun_RES)

lemma "single_valued A ⟹ single_valued B ⟹ single_valued (A O B)"
  by (simp add: single_valued_relcomp)

lemma Sup_enatoption_less2: " Sup X = Some ∞ ⟹ (∃x. Some x ∈ X ∧ enat t < x)"
  using Sup_enat_less2
  by (metis Sup_option_def in_these_eq option.distinct(1) option.sel)

lemma pw_conc_inres[refine_pw_simps]:
  "inresT (⇓R S') s t = (nofailT S' 
  ⟶ ((∃s'. (s,s')∈R ∧ inresT S' s' t) ― ‹ ∧ (∀s' t'. (s,s')∈R ⟶ inresT S' s' t' ⟶ t' ≤ t )› ))"
  apply (cases S')
  subgoal by simp
  subgoal  for m'
    apply rule
    subgoal 
      apply (auto simp: conc_fun_RES  )
      subgoal for t' 
        apply(cases t')
         apply auto
        subgoal for n apply(auto dest!: Sup_finite_enat) 
          subgoal for a apply(rule exI[where x=a]) apply auto
            apply(rule exI[where x="enat n"]) by auto  
          done
        subgoal apply(drule Sup_enatoption_less2[where t=t])
          apply auto subgoal for x a apply(rule exI[where x=a]) apply auto
            apply(rule exI[where x=x]) by auto 
          done
        done
      done
    subgoal 
      apply (auto simp: conc_fun_RES)
      by (smt Sup_upper dual_order.trans le_some_optE mem_Collect_eq)
    done
  done 

lemma bindT_conc_refine':
  fixes R' :: "('a×'b) set" and R::"('c×'d) set"
  assumes R1: "M ≤ ⇓ R' M'"
  assumes R2: "⋀x x' t . ⟦ (x,x')∈R'; inresT M x t; inresT M' x' t;
    nofailT M; nofailT M'
  ⟧ ⟹ f x ≤ ⇓ R (f' x')"
  shows "bindT M (λx. f x) ≤ ⇓ R (bindT M' (λx'. f' x'))"
  using assms
  apply (simp add: pw_le_iff refine_pw_simps)
  by blast 




lemma bindT_conc_acost_refine:
  fixes M :: "(_,(_,enat)acost) nrest"
    and R' :: "('a×'b) set" and R::"('c×'d) set"
  assumes R1: "M ≤ ⇓ R' M'"
  assumes R2: "⋀x x' t . ⟦ (x,x')∈R'; 
    nofailT M; nofailT M'
  ⟧ ⟹ f x ≤ ⇓ R (f' x')"
  shows "bindT M (λx. f x) ≤ ⇓ R (bindT M' (λx'. f' x'))"
  using assms
  apply (simp add: pw_acost_le_iff refine_pw_simps)
  by metis



lemma bindT_conc_acost_refine':
  fixes M :: "(_,(_,enat)acost) nrest"
    and R' :: "('a×'b) set" and R::"('c×'d) set"
  assumes R1: "M ≤ ⇓ R' M'"
  assumes R2: "⋀x x' t b. ⟦ (x,x')∈R'; ∃t b. inresT (project_acost b M) x t; ∃t b. inresT (project_acost b M') x' t;
    nofailT M; nofailT M'
  ⟧ ⟹ f x ≤ ⇓ R (f' x')"
  shows "bindT M (λx. f x) ≤ ⇓ R (bindT M' (λx'. f' x'))"
  using assms
  apply (simp add: pw_acost_le_iff refine_pw_simps)
  by metis




lemma "(x,x')∈R ⟹ (RETURNT x ::(_,'a::{nonneg,order,complete_lattice,monoid_add}) nrest ) ≤ ⇓R (RETURNT x')"
  unfolding conc_fun_def RETURNT_def apply (auto simp: le_fun_def) 
proof -
  consider "{uu:: 'a option. ∃a. (a = x' ⟶ uu = Some 0) ∧ (a ≠ x' ⟶ uu = None ∧ (x, a) ∈ R)} = { Some 0, None}"
    | "{uu:: 'a option. ∃a. (a = x' ⟶ uu = Some 0) ∧ (a ≠ x' ⟶ uu = None ∧ (x, a) ∈ R)} = { Some 0}"
    by auto
  then show " Sup {uu:: 'a option. ∃a. (a = x' ⟶ uu = Some 0) ∧ (a ≠ x' ⟶ uu = None ∧ (x, a) ∈ R)} ≥ Some 0"
    apply cases by simp_all
qed



(*
experiment
begin




lemma bindT_refine'':
  fixes R' :: "('a×'b) set" and R::"('c×'d) set"
  assumes R1: "M ≤ ⇓ R' M'"
  assumes R2: "⋀x x' t . ⟦ (x,x')∈R'    
  ⟧ ⟹ f x ≤ ⇓ R (f' x')"
  shows "bindT M (λx. f x) ≤ ⇓ R (bindT M' (λx'. f' x'))" 
  sorry


lemma bindT_mono_under_timerefine:
  fixes R :: "('a ⇒ ('a, enat) acost)"
  assumes wfR: "wfR R"
  shows "m ≤ timerefine R m' ⟹ (⋀x. f x ≤ timerefine R (f' x)) ⟹ bindT m f ≤ timerefine R (bindT m' f')"
  apply(rule order.trans) defer apply(subst timerefine_bindT_ge) using assms apply simp apply simp
  apply(rule bindT_mono_f2) by simp_all

thm bindT_refine'' bindT_mono_under_timerefine

lemma 
  assumes "wfR tR" and sv: "single_valued R" and sv: "single_valued R'"
  assumes R1: "M ≤ (timerefine tR (⇓ R'  M'))"
  assumes R2: "⋀x x' t . ⟦ (x,x')∈R' ⟧ ⟹ f x ≤ (timerefine tR ( ⇓ R  (f' x')))"
  shows "bindT M (λx. f x) ≤ (timerefine tR (⇓ R  (bindT M' (λx'. f' x'))))"
  apply(subst datarefine_timerefine_commute[symmetric, OF assms(1,2)])

  apply(rule order.trans)
   defer apply(rule nrest_Rel_mono) apply(subst timerefine_bindT_ge[OF assms(1)]) apply simp
  apply(rule bindT_refine''[where R'=R'])
  apply(rule order.trans[OF R1])
   apply(subst datarefine_timerefine_commute[  OF assms(1,3)]) apply simp
  apply(rule order.trans[OF R2]) apply simp
  apply(subst datarefine_timerefine_commute[  OF assms(1,2)]) apply simp
  done


lemma 
  assumes "wfR tR" 
  assumes R1: "M ≤ (⇓ R'(timerefine tR   M'))"
  assumes R2: "⋀x x' t . ⟦ (x,x')∈R' ⟧ ⟹ f x ≤ ( ⇓ R (timerefine tR  (f' x')))"
  shows "bindT M (λx. f x) ≤ (⇓ R (timerefine tR   (bindT M' (λx'. f' x'))))" 
  apply(rule order.trans)
   defer apply(rule nrest_Rel_mono) apply(subst timerefine_bindT_ge[OF assms(1)]) apply simp
  apply(rule bindT_refine''[where R'=R'])
  apply(rule R1) 
  apply(rule R2) by simp 



    
  

                     


end *)


subsection ‹Interaction with monadic operators›

lemma conc_fun_consume: 
  fixes M :: "('c, (_,enat) acost ) nrest"
  shows "⇓R (consume M t) = consume (⇓R M) t"
  apply(clarsimp simp add: consume_def conc_fun_def comp_def split: nrest.splits)
  apply(rule ext)  
  apply(subst conc_fun_consume_aux[symmetric, simplified])
  apply(rule arg_cong[where f=Sup]) 
  by auto 


lemma consume_refine_easy:
  fixes M :: "('e, ('b, enat) acost) nrest"
  shows "⟦t ≤ t'; M ≤ ⇓ R (   M')⟧ ⟹ NREST.consume M t ≤ ⇓R (  (NREST.consume M' t'))" 
  apply(subst conc_fun_consume)
  apply(rule consume_mono) by auto


lemma build_rel_SPEC_conv:
  fixes T :: "_ ⇒ ((_,enat)acost)"
  assumes "⋀x. T (α x) = T' x"
  shows "⇓(br α I) (SPEC Φ T) = SPEC (λx. I x ∧ Φ (α x)) T'"  
  using assms by (auto simp: br_def pw_acost_eq_iff refine_pw_simps SPEC_def)



subsection ‹Examples›

experiment 
begin
  definition Rset where "Rset = { (c,a)| c a. set c = a}"
                                       
  lemma "RETURNT [1,2,3] ≤ ⇓Rset (RETURNT {1,2,3})"
    unfolding conc_fun_def RETURNT_def Rset_def
    apply simp unfolding le_fun_def by auto
  
  lemma "RETURNT [1,2,3] ≤ ⇓Rset (RETURNT {1,2,3})"
    unfolding conc_fun_def RETURNT_def Rset_def
    apply simp unfolding le_fun_def by auto
  
  
  definition Reven where "Reven = { (c,a)| c a. even c = a}"
  
  lemma "RETURNT 3 ≤ ⇓Reven (RETURNT False)"
    unfolding conc_fun_def RETURNT_def Reven_def
    apply simp unfolding le_fun_def by auto
  
  lemma "m ≤ ⇓Id m"
    unfolding conc_fun_def RETURNT_def 
    apply (cases m) by auto
  
  
  lemma "m ≤ ⇓{} m ⟷ (m=FAILT ∨ m = SPECT bot)"
    unfolding conc_fun_def RETURNT_def 
    apply (cases m) apply auto by (metis bot.extremum dual_order.antisym le_funI)

end

lemma abs_fun_simps[simp]: 
  "⇑R FAILT = FAILT"
  "dom X⊆Domain R ⟹ ⇑R (REST X) = REST (λa. Sup {X c| c. (c,a)∈R})"
  "¬(dom X⊆Domain R) ⟹ ⇑R (REST X) = FAILT"
  unfolding abs_fun_def by (auto  split: nrest.split)

term single_valued
 
context fixes R assumes SV: "single_valued R" begin


lemma 
  fixes m :: "'b ⇒ enat option"
  shows
  Sup_sv: "(c, a') ∈ R ⟹  Sup {m a| a. (c,a) ∈ R} = m a'"
proof -
  assume "(c,a') ∈ R"
  with SV have singleton: "{m a| a. (c,a) ∈ R} = {m a'}" by(auto dest: single_valuedD) 
  show ?thesis unfolding singleton by simp
qed 

lemma indomD: " M c = Some y ⟹ dom M ⊆ Domain R ⟹ (∃a. (c,a)∈R)"
  by auto
(*
lemma conc_abs_swap: "m' ≤ ⇓R m ⟷ ⇑R m' ≤ m"
  apply rule
  subgoal (* <-- *)
  unfolding conc_fun_def abs_fun_def using SV
  apply (auto split: nrest.splits) 
  subgoal for M M'
    apply (auto simp add: le_fun_def)  
    sorry (* by (smt Sup_least antisym le_cases mem_Collect_eq single_valuedD)  *)
  subgoal 
    by (smt Collect_cong Domain.DomainI domI domIff empty_Sup empty_def le_map_dom_mono set_rev_mp)    
  done

  subgoal (* ⟶ *)
    unfolding conc_fun_def abs_fun_def using SV
    apply(auto split: nrest.splits if_splits)
    apply (auto simp add: le_fun_def)
    subgoal for M M' c
      apply(cases "M c = None")
       apply auto apply(frule indomD) apply simp
      apply(auto) sorry(*
      apply(simp only: Sup_sv)
       
      by (me tis (mono_tags, lifting) Sup_le_iff mem_Collect_eq) *)
    done
  done

lemma 
  fixes m :: "'b ⇒ enat option"
  shows
  Inf_sv: "(c, a') ∈ R ⟹  Inf {m a| a. (c,a) ∈ R} = m a'"
proof -
  assume "(c,a') ∈ R"
  with SV have singleton: "{m a| a. (c,a) ∈ R} = {m a'}" by(auto dest: single_valuedD) 
  show ?thesis unfolding singleton by simp
qed 

lemma ac_galois: "galois_connection (⇑R) (⇓R)"
  apply (unfold_locales)
  by (rule conc_abs_swap)
*)

lemma Sup_some_svD:
  fixes m :: "'b ⇒ enat option"
  shows "Sup {m a |a. (c, a) ∈ R} = Some t' ⟹ (∃a. (c,a)∈R ∧ m a = Some t')"
  using SV by (smt Sup_le_iff dual_order.antisym less_eq_option_Some_None
                    mem_Collect_eq order_refl single_valued_def)
 

end 


lemma pw_abs_nofail[refine_pw_simps]: 
  "nofailT (⇑R M) ⟷ (nofailT M ∧ (∀x. (∃t. inresT M x t) ⟶ x∈Domain R))"
  apply (cases M)
  apply simp
  apply (auto simp: abs_fun_simps abs_fun_def)
  by (metis zero_enat_def zero_le)



(*
lemma pw_abs_inre: 
  "inresT (⇑R M) a t ⟷ (nofailT (⇑R M) ⟶ (∃c. inresT M c t ∧ (c,a)∈R))"
  apply (cases M)
  apply simp
  apply (auto simp: abs_fun_def)
  done*)

(*
lemma pw_conc_inres:
  "inresT (⇓R S') s t = (nofailT S' 
  ⟶ (∃s'. (s,s')∈R ∧ inresT S' s' t))"
  apply (cases S')
  subgoal by simp
  subgoal  for m'
    apply rule
    subgoal 
      apply (auto simp: conc_fun_RES) sorry
    subgoal 
      apply (auto simp: conc_fun_RES) sorry
    done
  oops *)

lemma sv_the: "single_valued R ⟹ (c,a) ∈ R ⟹ (THE a. (c, a) ∈ R) = a"
  by (simp add: single_valued_def the_equality)

lemma conc_fun_RES_sv:
  fixes X :: "'b ⇒ enat option"
  assumes SV: "single_valued R"
  shows "⇓R (REST X) = REST (λc. if c∈Domain R then X (THE a. (c,a)∈R) else None )"
  unfolding conc_fun_def
  apply(auto split: nrest.split)
  apply(rule ext)
  apply auto
  subgoal using  SV  by (auto simp: Sup_sv sv_the)
  subgoal by (smt Collect_cong Domain.DomainI empty_Sup empty_def)
  done

lemma conc_fun_mono[simp, intro!]: 
  shows "mono ((⇓R)::('b, enat) nrest ⇒ ('a, enat) nrest)"
  apply rule 
  apply (simp add: pw_le_iff)
  by (auto simp: refine_pw_simps) 


lemma conc_fun_R_mono:
  fixes M :: "(_,enat) nrest"
  assumes "R ⊆ R'" 
  shows "⇓R M ≤ ⇓R' M"
  using assms
  by (auto simp: pw_le_iff refine_pw_simps)


lemma conc_fun_chain:
  fixes M :: "(_,enat) nrest"
  shows "⇓R (⇓S M) = ⇓(R O S) M"
  apply(cases M)
  subgoal by simp
  apply simp
  apply(simp only: conc_fun_RES)
  apply auto apply (rule ext)  unfolding SupSup_1 SupSup_2 by meson 


lemma conc_fun_complete_lattice_chain:
  fixes M :: "(_,'b::{complete_lattice,monoid_add}) nrest"
  shows "⇓R (⇓S M) = ⇓(R O S) M"
  apply(cases M)
  subgoal by simp
  apply simp
  apply(simp only: conc_fun_RES)
  apply auto apply (rule ext)  unfolding SupSup_1 SupSup_2 by meson 


lemma conc_fun_chain_sv:
  fixes M :: "(_,enat) nrest"
  assumes SVR: "single_valued R" and SVS: "single_valued S"
  shows "⇓R (⇓S M) = ⇓(R O S) M"
  apply(cases M)
  subgoal by simp
  apply simp
  using SVS apply(simp only: conc_fun_RES_sv)
  using SVR apply(simp only: conc_fun_RES_sv)
  using single_valued_relcomp[OF SVR SVS] apply(simp only: conc_fun_RES_sv)
  apply (auto split: nrest.split)
  apply (rule ext) apply auto
    apply(auto simp add: sv_the)  
  apply(subst sv_the) by auto


lemma conc_Id[simp]: "⇓Id = id"
  unfolding conc_fun_def [abs_def] by (auto split: nrest.split)

                                 
lemma conc_fun_fail_iff[simp]: 
  fixes S :: "(_,enat) nrest"
  shows
  "⇓R S = FAILT ⟷ S=FAILT"
  "FAILT = ⇓R S ⟷ S=FAILT"
  by (auto simp add: pw_eq_iff refine_pw_simps)


lemma conc_trans[trans]:
  fixes B :: "(_,'a::{complete_lattice,monoid_add}) nrest"
  assumes A: "C ≤ ⇓R B" and B: "B ≤ ⇓R' A" 
  shows "C ≤ ⇓R (⇓R' A)"
  apply(rule order.trans)
  apply(rule A)
  apply(rule nrest_Rel_mono)    
  apply(rule B)
  done 
(*
lemma conc_trans[trans]:
  fixes B :: "(_,enat) nrest"
  assumes A: "C ≤ ⇓R B" and B: "B ≤ ⇓R' A" 
  shows "C ≤ ⇓R (⇓R' A)"
  using assms by (fastforce simp: pw_le_iff refine_pw_simps)

lemma conc_acost_trans[trans]:
  fixes B :: "(_,(_,enat) acost) nrest"
  assumes A: "C ≤ ⇓R B" and B: "B ≤ ⇓R' A" 
  shows "C ≤ ⇓R (⇓R' A)"
  using assms by (fastforce simp: pw_acost_le_iff refine_pw_simps)
*)

lemma conc_trans_sv:
  fixes B :: "(_,enat) nrest"
  assumes SV: "single_valued R" "single_valued R'"
    and A: "C ≤ ⇓R B" and B: "B ≤ ⇓R' A" 
  shows "C ≤ ⇓R (⇓R' A)"
  using assms by (fastforce simp: pw_le_iff refine_pw_simps)

text ‹WARNING: The order of the single statements is important here!›
lemma conc_trans_additional[trans]: 
  assumes "single_valued R"
  shows
  "⋀(A::(_,enat) nrest) B C. A≤⇓R  B ⟹ B≤    C ⟹ A≤⇓R  C"
  "⋀(A::(_,enat) nrest) B C. A≤⇓Id B ⟹ B≤⇓R  C ⟹ A≤⇓R  C"
  "⋀(A::(_,enat) nrest) B C. A≤⇓R  B ⟹ B≤⇓Id C ⟹ A≤⇓R  C"

  "⋀(A::(_,enat) nrest) B C. A≤⇓Id B ⟹ B≤⇓Id C ⟹ A≤    C"
  "⋀(A::(_,enat) nrest) B C. A≤⇓Id B ⟹ B≤    C ⟹ A≤    C"
  "⋀(A::(_,enat) nrest) B C. A≤    B ⟹ B≤⇓Id C ⟹ A≤    C"
  using assms conc_trans[where R=R and R'=Id]
  by (auto intro: order_trans)



lemma RETURNT_refine:
  assumes "(x,x')∈R"
  shows "RETURNT x ≤ ⇓R (RETURNT x')"
  using assms
  by (auto simp: RETURNT_def conc_fun_RES le_fun_def Sup_upper)  

(*
thm bindT_refine'
lemma bindT_refine'2:
  fixes R' :: "('a×'b) set" and R::"('c×'d) set"
  assumes R1: "M ≤ ⇓ R' M'"
  assumes R2: "⋀x x' t . ⟦ (x,x')∈R'; inresT M x t; inresT M' x' t;
    nofailT M; nofailT M'
  ⟧ ⟹ f x ≤ ⇓ R (f' x')"
  shows "bindT M (λx. f x) ≤ ⇓ R (bindT M' (λx'. f' x'))"
  using assms
  apply (simp add: pw_le_iff refine_pw_simps)  
  by blast*)

lemma bindT_refine:
  fixes R' :: "('a×'b) set" and R::"('c×'d) set" and M :: "(_,enat) nrest"
  assumes R1: "M ≤ ⇓ R' M'"
  assumes R2: "⋀x x'. ⟦ (x,x')∈R' ⟧ 
    ⟹ f x ≤ ⇓ R (f' x')"
  shows "bindT M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
  apply (rule bindT_conc_refine') using assms by auto

subsection ‹WHILET refine›

lemma RECT_refine:
  assumes M: "mono2 body"
  assumes R0: "(x,x')∈R"
  assumes RS: "⋀f f' x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤⇓S (f' x'); (x,x')∈R ⟧ 
    ⟹ body f x ≤⇓S (body' f' x')"
  shows "RECT (λf x. body f x) x ≤⇓S (RECT (λf' x'. body' f' x') x')"
  unfolding RECT_flat_gfp_def
  apply (clarsimp simp add: M) 
  apply (rule flatf_fixp_transfer[where 
        fp'="flatf_gfp body" 
    and B'=body 
    and P="λx x'. (x',x)∈R", 
    OF _ _ flatf_ord.fixp_unfold[OF M[THEN trimonoD_flatf_ge]] R0])
  apply simp
  apply (simp add: trimonoD_flatf_ge)
  by (rule RS)

                                         
lemma WHILET_refine:
  fixes f :: "_ ⇒ (_,enat) nrest"
  assumes R0: "(x,x')∈R"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  shows "whileT b f x ≤ ⇓R (whileT b' f' x')"
  unfolding whileT_def apply(rule RECT_refine)
    subgoal by(refine_mono)  
     apply (fact R0)
    by(auto simp: COND_REF STEP_REF RETURNT_refine intro: bindT_refine[where R'=R])  

lemma SPECT_refines_conc_fun':
  assumes a: "⋀m c.  M = SPECT m
          ⟹ c ∈ dom n ⟹ (∃a. (c,a)∈R ∧ n c ≤ m a)"
  shows "SPECT n ≤ ⇓ R M"
proof - 
  show ?thesis
    unfolding conc_fun_def apply (auto split: nrest.split) 
    subgoal for m unfolding le_fun_def apply auto
    proof -
      fix c
      assume m: "M = SPECT m"
      show "n c ≤ Sup {m a |a. (c, a) ∈ R} "
      proof (cases "c ∈ dom n")
        case True
        with m a obtain a where k: "(c,a)∈R" "n c ≤ m a" by blast 
        show ?thesis apply(rule  Sup_upper2) using k by auto
      next
        case False
        then show ?thesis 
          by (simp add: domIff)
      qed 
    qed
    done
qed

lemma SPECT_refines_conc_fun:
  assumes a: "⋀m c. (∃a. (c,a)∈R ∧ n c ≤ m a)"
  shows "SPECT n ≤ ⇓ R (SPECT m)"
  apply(rule SPECT_refines_conc_fun') using a by auto


lemma SPECT_refines_conc_fun_sv:
  assumes "single_valued R" 
    and a: "dom n ⊆ Domain R"
    and "⋀c. c ∈ dom n ⟹ n c ≤ (THE a. (c,a)∈R)"
  shows "SPECT n ≤ ⇓ R (SPECT m)"
  apply(rule SPECT_refines_conc_fun') using a
  using indomD[OF assms(1) _ a] domIff
  oops




lemma conc_fun_br: "⇓ (br α I1) (SPECT (emb I2 t))
        = (SPECT (emb (λx. I1 x ∧ I2 (α x)) t))"
  unfolding conc_fun_RES  apply auto apply(rule ext)    
      by (auto simp: emb'_def br_def bot_option_def Sup_option_def) 


subsection ‹Relators›


definition nrest_rel where 
  nrest_rel_def_internal: "nrest_rel R ≡ {(c,a).  c ≤ ⇓R  a}"

lemma nrest_rel_def: "⟨R⟩nrest_rel ≡ {(c,a). c ≤ ⇓R  a}"
  by (simp add: nrest_rel_def_internal relAPP_def)

lemma nrest_relD: "(c,a)∈⟨R⟩nrest_rel ⟹ c ≤ ⇓R  a" by (simp add: nrest_rel_def)
lemma nrest_relI: "c ≤⇓R a ⟹ (c,a)∈⟨R⟩nrest_rel" by (simp add: nrest_rel_def)


lemma nrest_rel_comp: 
 "⟨A⟩nrest_rel O ⟨B⟩nrest_rel = ⟨A O B⟩nrest_rel"
  by (auto simp: nrest_rel_def conc_fun_complete_lattice_chain[symmetric] conc_trans)

lemma pw_nrest_rel_iff: "(a,b)∈⟨A⟩nrest_rel ⟷ nofailT (⇓ A b)⟶  nofailT a ∧ (∀x t. inresT a x t ⟶ inresT (⇓ A b) x t)"
  by (simp add: pw_le_iff nrest_rel_def)

find_theorems project_acost abs_fun

lemma pw_acost_nrest_rel_iff: "(a,b)∈⟨A⟩nrest_rel ⟷ nofailT (⇓ A b) ⟶ nofailT a
         ∧ (∀x c t. inresT (project_acost c a) x t ⟶ inresT (⇓ A (project_acost c b)) x t)"
  by (auto simp add: pw_acost_le_iff nrest_rel_def project_acost_conc_fun_commute)


lemma param_RETURNT[param]: 
  "(RETURNT,RETURNT) ∈ R → ⟨R⟩nrest_rel"
  by (auto simp: nrest_rel_def RETURNT_refine)

lemma param_RETURN[param]: 
  "(RETURNT,RETURNT) ∈ R → ⟨R⟩nrest_rel"
  by (auto simp: nrest_rel_def RETURNT_refine)

lemma param_bind[param]:
  "(bind,bind) ∈ ⟨Ra⟩nrest_rel → (Ra→⟨Rb⟩nrest_rel) → (⟨Rb⟩nrest_rel:: (('a, (_,enat)acost) nrest × ('c, _) nrest) set)"
  by (auto simp: nrest_rel_def intro: bindT_conc_acost_refine' dest: fun_relD)

lemma param_ASSERT_bind[param]:
  fixes f :: "(_,_) nrest"
  shows 
 "⟦
    (Φ,Ψ) ∈ bool_rel; 
    ⟦ Φ; Ψ ⟧ ⟹ (f,g)∈⟨R⟩nrest_rel
  ⟧ ⟹ (doN { ASSERT Φ; f}, doN {ASSERT Ψ; g}) ∈ ⟨R⟩nrest_rel"
  by (auto intro: nrest_relI)



definition continuous2 :: "_ ⇒ ('a::{Sup} ⇒ 'b::{Sup}) ⇒ bool"  where
  "continuous2 P f ⟷ (∀A. P A ⟶ Sup (f ` A) = f (Sup A) )"

 
definition "attains_sup' m m' RR ≡ 
  ∀r M' M. m=SPECT M ⟶ m'=SPECT M' ⟶ r∈dom M ⟶ (∃a. (r,a)∈RR) ⟶ Sup {M' a| a. (r,a)∈RR} ∈ {M' a| a. (r,a)∈RR}"  


lemma  
  fixes A :: "enat set"
  shows "Sup A  ∈ A ⟹ Sup ( (λa. a * c) ` A) ∈ (λa. a * c) ` A"   
  by (metis enat_mult_cont imageI)  


lemma plus_continuous_if_attains_sup:
  fixes x y h
  defines "g ≡ λf::_⇒enat. f x + f y"
  assumes "Sup A ∈ A"
  shows "g (Sup A) = (SUP f∈A. g f)"
  unfolding assms
  apply(rule antisym)
  subgoal 
    apply(rule Sup_upper)
    using assms(2) by blast
  subgoal     
    by (simp add: enat_add_cont')
  done

lemma plus_continuous_if_attains_sup':
  fixes x y h
  defines "g ≡ λf::_⇒enat. f x + h f y"
  assumes "Sup A ∈ A" and
    h_mono: "⋀f f' y. f≤f' ⟹ h f y ≤ h f' y"
  shows "g (Sup A) = (SUP f∈A. g f)"
  unfolding assms
  apply(rule antisym)
  subgoal 
    apply(rule Sup_upper)
    using assms(2) by blast
  subgoal     
    apply(auto intro!: Sup_least add_mono Sup_upper)
    apply(rule h_mono) apply(intro Sup_upper) .
  done



lemma 
  fixes S
  defines "g ≡ λf::_⇒enat. sum f S"
  assumes "Sup A ∈ A"
  shows "finite S ⟹ g (Sup A) = (SUP f∈A. g f)"
  unfolding assms
  apply(induct S rule: finite_induct)
  subgoal using assms(2) apply auto
    using SUP_bot_conv(1) by fastforce
  subgoal using assms(2) apply simp
    apply(subst plus_continuous_if_attains_sup'[symmetric, OF assms(2)])
    subgoal apply(rule sum_mono) by (simp add: le_fun_def)
    by simp
  done 

(*
lemma
  fixes R :: "'a ⇒ ('b, enat) acost"
  assumes "wfR'' R"
  shows "continuous2 (λcm. finite {x. the_acost cm x ≠ 0})
           ( λcm.  (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc))))"
  unfolding continuous2_def
  apply clarsimp
  sorry

lemma continuous_if_wfR'':
  fixes R :: "'a ⇒ ('b, enat) acost"
  assumes "wfR'' R"
  shows "continuous ( λcm.  (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc))))"
  apply(rule continuousI)
proof -
  fix A :: "('a, enat) acost set"
  have "Sup A ∈ A" sorry
  have "⋀ac. the_acost (Sup A) ac = (SUP a∈A. (the_acost a ac))"
    unfolding Sup_acost_def by simp 
  have pf: "⋀g a. (SUP f∈A. the_acost f a) * g = (SUP f∈A. the_acost f a * g)" 
    by (simp add: enat_mult_cont')  
  
  show "acostC (λcc. ∑ac. the_acost (Sup A) ac * the_acost (R ac) cc) 
        = (SUP cm∈A. acostC (λcc. ∑ac. the_acost cm ac * the_acost (R ac) cc))"
    unfolding Sup_acost_def
    apply simp  
    apply(subst pf)
    sorry
qed
  (* TODO: investigate *)
  oops

thm timerefine_conc_fun_le2[OF continuous_if_wfR'', unfolded timerefine_alt4[symmetric]]




lemma timerefine_conc_fun_le2:
  assumes "continuous E"
  shows "timerefine' E (⇓ R C) = ⇓R (timerefine' E C)"
  unfolding timerefine'_def conc_fun_def 
  apply(auto split: nrest.splits option.splits simp: fun_eq_iff)
  subgoal 
    by (smt Sup_bot_conv(1) bot_option_def mem_Collect_eq) 
  subgoal premises p for x2 x2a x2b x x2c
  proof -
    have "Sup {x2b a |a. (x, a) ∈ R} = Sup {map_option E (x2 a) |a. (x, a) ∈ R}"
      apply(rule arg_cong[where f=Sup])
      using p(3)[rule_format] p(4)
      apply auto
      subgoal by (smt map_option_eq_Some option.exhaust) 
      subgoal by (metis not_None_eq option.simps(8) option.simps(9)) 
      done
    also have "… = map_option E (Sup {x2 a |a. (x, a) ∈ R})" 
      apply(subst continuous_map_option[OF assms, THEN continuousD] )
      apply(rule arg_cong[where f=Sup])
      by auto
    also have "… = map_option E (Some x2c)"
      using p(2)[rule_format, of x, unfolded p(4)] by simp
    also have "… = Some (E x2c)" by simp
    finally show "Some (E x2c) = Sup {x2b a |a. (x, a) ∈ R}"  by simp
  qed
  done 

*)
end