Theory 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 (simp add: less_eq_set_def le_fun_def)
  apply (drule_tac x = xa in spec)
  apply (simp_all add: mono_def)
  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 (simp add: apply_fun_def)
  apply safe
  apply (subst (asm) Disjunctive_fun_def)
  apply (drule_tac x = x in spec)
  apply (simp add: Apply.Disjunctive_def)
  apply (subgoal_tac "(R x ` (λf. f x) ` X) =((λf. f x) ` {y. xX. 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)"
  by (simp add: Disjunctive_fun_def)

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 (simp add: Disjunctive_Sup apply_fun_range)
  apply (rule hoare_diagram2)
  apply simp_all
  apply safe
  apply (simp add: disjunctive_SUP_L_P [THEN sym])
  apply (simp add: apply_fun_def)
  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 (simp add: DataRefinement_def mono_def)
  apply (subst le_fun_def)
  apply (simp add: 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 (simp add: DgrDataRefinement2_def)
  apply auto
  apply (rule_tac S = "{.P i.} o D(i, j)" in DataRefinement_mono)
  apply (simp_all add: le_fun_def assert_def)
  apply safe
  apply (rule_tac y = "Q i" in order_trans)
  by (simp_all add: mono_fun_def)


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 (simp add: apply_fun_def)
  apply (rule_tac S = "D (i,j)" and R = "R i" and R' = "R j" in data_refinement)
  by (simp_all add: Disjunctive_Sup apply_fun_range)


lemma comp_left_mono [simp]: "S  S'  S o T  S' o T"
  by (simp add: le_fun_def)

lemma assert_pred_mono [simp]: "p  q  {.p.}  {.q.}"
  apply (simp add: le_fun_def assert_def)
  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 (simp add: apply_fun_def)
  apply (rule_tac S = "D (i,j)" and R = "R i" and R' = "R j" in data_refinement2)
  apply (simp_all add: Disjunctive_Sup)
  apply (rule_tac S = "{.Sup (range X) i.}  D (i, j)" in DataRefinement_mono)
  apply (rule comp_left_mono)
  apply (rule assert_pred_mono)
  apply (simp add: Sup_fun_def comp_def)
  apply (rule SUP_upper)
  apply (auto simp add: apply_fun_def apply_fun_range image_image fun_eq_iff)
  apply (auto intro!: arg_cong [where f = Sup] arg_cong2 [where f = inf])
  done

lemma "(R'::'a::complete_lattice  'b::complete_lattice)  Apply.Disjunctive 
   DataRefinement S R R' S'  R (- grd S)  - grd S'"
  apply (simp add: DataRefinement_def grd_def le_fun_def)
  apply (drule_tac x = "" in spec)
  by simp

end