Theory DataRefinement

theory DataRefinement
imports Sepreftime
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 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: "A ≤ B ⟹ ⇓ R A ≤ ⇓ R B"
  unfolding conc_fun_def
  apply (auto split: nrest.split simp: le_fun_def)  
  by (smt Sup_mono mem_Collect_eq)
 
subsubsection ‹Examples›

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)


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)  
    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)
      apply(simp only: Sup_sv)
       
      by (metis (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 
  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')"
  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_inres[refine_pw_simps]: 
  "(∃t. inresT (⇑R M) a t) ⟷ (nofailT (⇑R M) ⟶ (∃c. (∃t. inresT M c t) ∧ (c,a)∈R))"
  apply (cases M)
   apply simp
  apply rule
  subgoal for m
    apply (auto simp: abs_fun_def) (*    *)
    sorry
  subgoal for m
    sorry
  done
*)

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 pw_conc_inres_sv:
  "single_valued R ⟹ 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 
      by (auto simp: conc_fun_RES dest!: Sup_some_svD)        
    subgoal 
      by (auto simp: conc_fun_RES Sup_sv )  
    done
  done *)

lemma 
  fixes m :: "'a ⇒ enat option"
  shows
  "single_valued R ⟹ Sup {m a| a. (c,a) ∈ R} = None ⟷ c ∉ Domain R"
  apply rule
  subgoal oops

(*
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:
  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)"
  apply rule 
  apply (simp add: pw_le_iff)
  by (auto simp: 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}"
  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 ⇒ 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"
  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:
  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]: 
  "⇓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
  apply (simp add: pw_le_iff refine_pw_simps)  
  by 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')"
  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:
  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 
  assumes a: "⋀m n c a. c∈Domain R ⟹ ∃a. SPECT (n c) ≤  SPECT (m a)"
  shows "(SPECT n) ≤ ⇓ R (SPECT m)"
  using a  apply auto  
    unfolding conc_fun_def apply (auto split: nrest.split) 
      unfolding le_fun_def apply auto
    proof -
      fix c 
      assume "(⋀c n m. c ∈ Domain R ⟹ ∃a. ∀x. n c x ≤ m a x)"
      oops

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)    
    using Sup_Some by (auto simp: emb'_def br_def bot_option_def Sup_option_def) 

end