Theory DataRefinement

theory DataRefinement
imports NREST
begin

subsection ‹Data Refinement›


lemma "{(1,2),(2,4)}``{1,2}={2,4}" by auto


definition conc_fun ("⇓") where
  "conc_fun R m ≡ case m of FAILi ⇒ FAILT | REST X ⇒ REST (λc. Sup {X a| a. (c,a)∈R})"
                                                                  (* ^- not so sure here *)
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"
                                                (* ^- not so sure here *)
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 nrest_Rel_mono: "A ≤ B ⟹ ⇓ R A ≤ ⇓ R B"
  unfolding conc_fun_def by (fastforce split: nrest.split simp: le_fun_def intro!: Sup_mono)
 
subsubsection ‹Examples›

definition Rset where "Rset = { (c,a)| c a. set c = a}"
                                     
lemma "RETURNT [1,2,3] ≤ ⇓Rset (RETURNT {1,2,3})"
  by (auto simp add: le_fun_def conc_fun_def RETURNT_def Rset_def)
  
lemma "RETURNT [1,2,3] ≤ ⇓Rset (RETURNT {1,2,3})"
  by (auto simp add: le_fun_def conc_fun_def RETURNT_def Rset_def)

definition Reven where "Reven = { (c,a)| c a. even c = a}"

lemma "RETURNT 3 ≤ ⇓Reven (RETURNT False)"
  by (auto simp add: le_fun_def conc_fun_def RETURNT_def Reven_def)

lemma "m ≤ ⇓Id m"
  unfolding conc_fun_def RETURNT_def by (cases m) auto


lemma "m ≤ ⇓{} m ⟷ (m=FAILT ∨ m = SPECT bot)"
  unfolding conc_fun_def RETURNT_def by (cases m) (auto simp add: bot.extremum_uniqueI le_fun_def)

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)
 
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"
proof(cases m; cases m')
  fix M M'
  note [simp] = conc_fun_def abs_fun_def
  assume b[simp]: "m = REST M" "m' = REST M'"
  show ?thesis
  proof
    assume a: "m' ≤ ⇓ R m"
    from a b have R: "m' ≤ REST (λc. ⨆ {M a |a. (c, a) ∈ R})"
      using conc_fun_RES by metis
    with R have Domain: "dom M' ⊆ Domain R"
      by (auto simp add: le_fun_def Sup_option_def split: if_splits option.splits)
    from R have " M' x' ≤ M x" if "(x',x) ∈ R" for x x'
      by (auto simp add: Sup_sv[OF that] intro: le_funI dest: le_funD[of _ _ x'])
    with R SV Domain show "⇑ R m' ≤ m"
      by (auto intro!: le_funI simp add: Sup_le_iff)
  next
    assume a: "⇑ R m' ≤ m"
    show "m' ≤ ⇓R m"
    proof(cases "dom M' ⊆ Domain R")
      case True(* 
      with a have " M' x' ≤ M x" if "(x',x) ∈ R" for x x'
        apply  (auto simp add: Sup_sv[OF that] intro: le_funI dest: le_funD[of _ _ x']) sorry *)
      
      have "M' x ≤ ⨆ {M a |a. (x, a) ∈ R}" for x
      proof(cases "M' x")
        case (Some y)
        with True obtain x' where x_x': "(x,x') ∈ R" 
          by blast
        with a SV show ?thesis
          by (force simp add: Sup_sv[OF x_x'] Sup_le_iff dest!: le_funD[of _ _ x'] split: if_splits)
      qed auto
      then show "m' ≤ ⇓ R m"
        by (auto intro!: le_funI)
    next
      case False
      with a show ?thesis
        by auto
    qed
  qed
qed (auto simp add: conc_fun_def abs_fun_def)

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)"
  by (unfold_locales) (rule conc_abs_swap)


lemma 
  fixes m :: "'b ⇒ enat option"
  shows Sup_some_svD: "Sup {m a |a. (c, a) ∈ R} = Some t' ⟹ (∃a. (c,a)∈R ∧ m a = Some t')"
  by (frule Sup_Some) (use SV in ‹auto simp add: single_valued_def Sup_sv›)

end 


lemma pw_abs_nofail[refine_pw_simps]: 
  "nofailT (⇑R M) ⟷ (nofailT M ∧ (∀x. (∃t. inresT M x t) ⟶ x∈Domain R))" (is "?l ⟷ ?r")
proof (cases M)
  case FAILi
  then show ?thesis
    by auto
next
  case [simp]: (REST m)
  show ?thesis
  proof
    assume "?l"
    then show ?r
      by (auto simp: abs_fun_def split: if_splits)
  next
    assume a: ?r
    with REST have "x∈Domain R" if "m x = Some y" for x y
    proof-
      have "enat 0 ≤ y"
        by (simp add: enat_0)
      with that REST a show ?thesis
        by auto
    qed
    then show ?l 
      by (auto simp: abs_fun_def)
  qed
qed

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)))" (is "?l ⟷ ?r")
proof(cases S')
  case [simp]: (REST m')
  show ?thesis
  proof
    assume a: ?l
    from this obtain t' where t': "enat t ≤ t'" "⨆ {m' a |a. (s, a) ∈ R} = Some t'"
      by (auto simp: conc_fun_RES) 
    then obtain a t'' where "(s, a) ∈ R" "m' a = Some t''" "enat t ≤ t''"
    proof(cases t')
      case (enat n)
      with t' that[where t''=n] show ?thesis 
        by(auto dest: Sup_finite_enat)
    next
      case infinity
      with t' that show ?thesis 
        by (force dest!: Sup_enatoption_less2[where t=t] simp add: less_le_not_le t'(1))
    qed
    then show ?r
      by auto
  next
    assume a: ?r
    then obtain s' t' where s'_t': "(s,s') ∈ R" "m' s' = Some t'" "enat t ≤ t'"
      by (auto simp: conc_fun_RES)
    then have "∃t'≥enat t. ⨆ {m' a |a. (s, a) ∈ R} ≥ Some t'"
      by (intro exI[of _ t']) (force intro: Sup_upper)
    then show ?l
      by (auto simp: conc_fun_RES elim!: le_some_optE)
  qed
qed simp

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:
  assumes SV: "single_valued R"
  shows "⇓R (REST X) = REST (λc. if c∈Domain R then X (THE a. (c,a)∈R) else None )"
  using SV by (auto simp add: Sup_sv sv_the Domain_iff conc_fun_def bot_option_def
      intro!: ext split: nrest.split)

lemma conc_fun_mono[simp, intro!]: 
  shows "mono (⇓R)"
  by (rule monoI) (auto simp: pw_le_iff refine_pw_simps) 


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



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 ⇒ enat 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}"
  by (rule antisym) (auto intro: Sup_least Sup_subset_mono Sup_upper2)

lemma 
  fixes m :: "'a ⇒ enat 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 conc_fun_chain:
  shows "⇓R (⇓S M) = ⇓(R O S) M"
proof(cases M)
  case [simp]: (REST x)
  have "⨆ {⨆ {x aa |aa. (a, aa) ∈ S} |a. (c, a) ∈ R} = ⨆ {x a |a. (c, a) ∈ R O S}" for c
    by (unfold SupSup_1 SupSup_2) meson
  then show ?thesis 
    by (simp add: conc_fun_RES)
qed auto 

lemma conc_fun_chain_sv:
  assumes SVR: "single_valued R" and SVS: "single_valued S"
  shows "⇓R (⇓S M) = ⇓(R O S) M"
  using assms conc_fun_chain by blast


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

                                 
lemma conc_fun_fail_iff[simp]: 
  "⇓R S = FAILT ⟷ S=FAILT"
  "FAILT = ⇓R S ⟷ S=FAILT"
  by (auto simp add: pw_eq_iff refine_pw_simps)

lemma conc_trans[trans]:
  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_trans_sv:
  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 B C. A≤⇓R  B ⟹ B≤    C ⟹ A≤⇓R  C"
  "⋀A B C. A≤⇓Id B ⟹ B≤⇓R  C ⟹ A≤⇓R  C"
  "⋀A B C. A≤⇓R  B ⟹ B≤⇓Id C ⟹ A≤⇓R  C"

  "⋀A B C. A≤⇓Id B ⟹ B≤⇓Id C ⟹ A≤    C"
  "⋀A B C. A≤⇓Id B ⟹ B≤    C ⟹ A≤    C"
  "⋀A 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)  

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'; 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
  by (simp add: pw_le_iff refine_pw_simps) blast

lemma bindT_refine:
  fixes R' :: "('a×'b) set" and R::"('c×'d) set"
  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_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')"
proof(cases "mono2 body'")
  case True
  have "flatf_gfp body x ≤ ⇓ S (flatf_gfp body' x')"
    by  (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])
    (use True in ‹auto intro: RS dest: trimonoD_flatf_ge›)
  then show ?thesis 
    by (auto simp add: M RECT_flat_gfp_def)
qed (auto simp add: RECT_flat_gfp_def)
                                         
lemma WHILET_refine:
  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[OF _ R0])
   subgoal by refine_mono
   subgoal by (auto simp add: COND_REF STEP_REF RETURNT_refine intro: bindT_refine[where R'=R])  
  done

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 - 
  have "n c ≤ ⨆ {m a |a. (c, a) ∈ R}" if "M = SPECT m" for c m 
  proof (cases "c ∈ dom n")
    case True
    with that a obtain a where k: "(c,a)∈R" "n c ≤ m a" by blast 
    then show ?thesis 
      by (intro Sup_upper2) auto
  next
    case False
    then show ?thesis 
      by (simp add: domIff)
  qed 
  then show ?thesis
    unfolding conc_fun_def by (auto simp add: le_fun_def split: nrest.split) 
qed

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


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

end