# Theory DataRefinementIBP.DataRefinement

```section ‹Data Refinement of Diagrams›

theory DataRefinement
imports Diagram
begin

text‹
Next definition introduces the concept of data refinement of \$S1\$
to \$S2\$ using the data abstractions \$R\$ and \$R'\$.
›

definition
DataRefinement :: "('a::type ⇒ 'b::type)
⇒ ('b::type ⇒ 'c::ord) ⇒ ('a::type ⇒ 'd::type)
⇒ ('d::type ⇒ 'c::ord) ⇒ bool" where
"DataRefinement S1 R R' S2 = ((R o S1) ≤ (S2 o R'))"

text‹
If \$\mathit{demonic}\ Q\$ is correct with respect to \$p\$ and \$q\$, and
\$(\mathit{assert} \ p)\circ (\mathit{demonic}\  Q)\$ is data refined
by \$S\$, then \$S\$ is correct with respect to \$\mathit{angelic}\  R\  p\$ and
\$\mathit{angelic} \ R' \ q\$.
›

theorem data_refinement:
"mono R ⟹ ⊨ p {| S |} q ⟹  DataRefinement S R R' S' ⟹
⊨ (R p) {| S' |} (R' q)"
apply (simp add:  DataRefinement_def Hoare_def le_fun_def)
apply (drule_tac x = q in spec)
apply (rule_tac y = "R (S q)" in order_trans)
apply (drule_tac x = p and y = "S q" in monoD)
by simp_all

theorem data_refinement2:
"mono R ⟹ ⊨ p {| S |} q ⟹  DataRefinement ({.p.} o S) R R' S' ⟹
⊨ (R p) {| S' |} (R' q)"
apply (simp add:  DataRefinement_def Hoare_def le_fun_def assert_def)
apply (drule_tac x = q in spec)
apply (subgoal_tac "p ⊓ S q = p")
apply simp
apply (rule antisym)
by simp_all

theorem data_refinement_hoare:
"mono S ⟹ mono D ⟹ DataRefinement ({.p.} o [:Q:]) {:R:} D S =
(∀ s . ⊨ {s' . s ∈ R s' ∧ s ∈ p} {| S |} (D ((Q s)::'a::order)))"
apply (simp add: le_fun_def assert_def angelic_def demonic_def Hoare_def DataRefinement_def)
apply safe
apply (simp_all)
apply (drule_tac x = "Q s" in spec)
apply auto [1]
apply (drule_tac x = "xb" in spec)
apply simp
apply (drule_tac x = xa in spec)
by auto

theorem data_refinement_choice1:
"DataRefinement S1 D D' S2 ⟹ DataRefinement S1 D D' S2' ⟹ DataRefinement S1 D D' ( S2 ⊓ S2') "
by (simp add: DataRefinement_def hoare_choice le_fun_def inf_fun_def)

theorem data_refinement_choice2:
"mono D ⟹ DataRefinement S1 D D' S2 ⟹ DataRefinement S1' D D' S2' ⟹
DataRefinement (S1 ⊓ S1') D D' (S2 ⊓ S2')"
apply (simp add: DataRefinement_def inf_fun_def le_fun_def)
apply safe
apply (rule_tac y = "D (S1 x)" in order_trans)
apply (drule_tac x = "S1 x ⊓ S1' x" and y = "S1 x" in monoD)
apply simp_all
apply (rule_tac y = "D (S1' x)" in order_trans)
apply (drule_tac x = "S1 x ⊓ S1' x" and y = "S1' x" in monoD)
by simp_all

theorem data_refinement_top [simp]:
"DataRefinement S1 D D' (⊤::_::order_top)"
by (simp add: DataRefinement_def le_fun_def top_fun_def)

definition apply_fun::"('a⇒'b⇒'c)⇒('a⇒'b)⇒'a⇒'c" (infixl ".." 5) where
"(A .. B) = (λ x . (A x) (B x))"

definition
"Disjunctive_fun R = (∀ i . (R i) ∈ Apply.Disjunctive)"

lemma Disjunctive_Sup:
"Disjunctive_fun R ⟹ (R .. (Sup X)) =  Sup {y . ∃ x ∈ X . y = (R .. x)}"
apply (subst fun_eq_iff)
apply safe
apply (subst (asm) Disjunctive_fun_def)
apply (drule_tac x = x in spec)
apply (subgoal_tac "(R x ` (λf. f x) ` X) =((λf. f x) ` {y. ∃x∈X. y = (λxa. R xa (x xa))})")
apply (auto simp add: image_image cong del: SUP_cong_simp)
done

lemma (in DiagramTermination) disjunctive_SUP_L_P:
"Disjunctive_fun R ⟹ (R .. (SUP_L_P P (pair u i))) =  (SUP_L_P (λ w . (R .. (P w)))) (pair u i)"
by (simp add: SUP_L_P_def apply_fun_def Disjunctive_fun_def Apply.Disjunctive_def fun_eq_iff image_comp)

lemma apply_fun_range: "{y. ∃x. y = (R .. P x)} = range (λ x . R .. P x)"
by (fact full_SetCompr_eq)

lemma [simp]: "Disjunctive_fun R ⟹ mono ((R i)::'a::complete_lattice ⇒ 'b::complete_lattice)"

theorem (in DiagramTermination) dgr_data_refinement_1:
"dmono D' ⟹ Disjunctive_fun R ⟹
(∀ w i j . ⊨ P w i  {| D(i,j) |} SUP_L_P P (pair w i) j) ⟹
(∀ w i j . DataRefinement ((assert (P w i)) o (D (i,j))) (R i) (R j) (D' (i, j))) ⟹

⊨ (R .. (Sup (range P))) {| pt D' |} ((R .. (Sup (range P))) ⊓ (-(grd (step D'))))"
apply (rule hoare_diagram2)
apply simp_all
apply safe
apply (simp add: disjunctive_SUP_L_P [THEN sym])
apply (rule_tac S = "D (i, j)" in data_refinement2)
by auto

definition
"DgrDataRefinement1 D R D' = (∀ i j . DataRefinement (D (i , j)) (R i) (R j) (D' (i, j)))"

definition
"DgrDataRefinement2 P D R D' = (∀ i j . DataRefinement ({.P i.} o D (i , j)) (R i) (R j) (D' (i, j)))"

theorem DataRefinement_mono:
"T ≤ S ⟹ mono R ⟹ DataRefinement S R R' S' ⟹ DataRefinement T R R' S' "
apply (subst le_fun_def)
apply safe
apply (rule_tac y = "R (S x)" in order_trans)
by simp_all

definition
"mono_fun R = (∀ i . mono (R i))"

theorem DgrDataRefinement_mono:
"Q ≤ P ⟹ mono_fun R ⟹ DgrDataRefinement2 P D R D' ⟹ DgrDataRefinement2 Q D R D'"
apply auto
apply (rule_tac S = "{.P i.} o D(i, j)" in DataRefinement_mono)
apply safe
apply (rule_tac y = "Q i" in order_trans)

text‹
Next theorem is the diagram version of the data refinement theorem. If the
diagram demonic choice \$T\$ is correct, and it is refined by \$D\$, then
\$D\$ is also correct. One important point in this theorem is that
if the diagram demonic choice \$T\$ terminates, then \$D\$ also terminates.
›

theorem (in DiagramTermination) Diagram_DataRefinement1:
"dmono D ⟹ Disjunctive_fun R ⟹ ⊢ P {| D |} Q ⟹ DgrDataRefinement1 D R D' ⟹
⊢ (R .. P) {| D' |} ((R .. P) ⊓ (-(grd (step D'))))"
apply (unfold Hoare_dgr_def DgrDataRefinement1_def dgr_demonic_def)
apply safe
apply (rule_tac x="λ w . R .. (X w)" in exI)
apply safe
apply (unfold disjunctive_SUP_L_P [THEN sym])
apply (rule_tac S = "D (i,j)" and R = "R i" and R' = "R j" in data_refinement)

lemma comp_left_mono [simp]: "S ≤ S' ⟹ S o T ≤ S' o T"

lemma assert_pred_mono [simp]: "p ≤ q ⟹ {.p.} ≤ {.q.}"
apply safe
apply (rule_tac y = p in order_trans)
by simp_all

theorem (in DiagramTermination) Diagram_DataRefinement2:
"dmono D ⟹ Disjunctive_fun R ⟹ ⊢ P {| D |} Q ⟹ DgrDataRefinement2 P D R D' ⟹
⊢ (R .. P) {| D' |} ((R .. P) ⊓ (-(grd (step D'))))"
apply (unfold Hoare_dgr_def DgrDataRefinement2_def dgr_demonic_def)
apply auto
apply (rule_tac x="λ w . R .. (X w)" in exI)
apply safe
apply (unfold disjunctive_SUP_L_P [THEN sym])
apply (rule_tac S = "D (i,j)" and R = "R i" and R' = "R j" in data_refinement2)
apply (rule_tac S = "{.Sup (range X) i.} ∘ D (i, j)" in DataRefinement_mono)
apply (rule comp_left_mono)
apply (rule assert_pred_mono)