Theory Refine_Monadic.RefineG_While

section ‹Generic While-Combinator›
theory RefineG_While
imports 
  RefineG_Recursion
  "HOL-Library.While_Combinator"
begin

definition
  "WHILEI_body bind return I b f  
  (λW s. 
    if I s then 
      if b s then bind (f s) W else return s
    else top)"
definition 
  "iWHILEI bind return I b f s0  REC (WHILEI_body bind return I b f) s0"
definition 
  "iWHILEIT bind return I b f s0  RECT (WHILEI_body bind return I b f) s0"
definition "iWHILE bind return  iWHILEI bind return (λ_. True)"
definition "iWHILET bind return  iWHILEIT bind return (λ_. True)"

(* TODO: Move to refine_mono_prover*)
lemma mono_prover_monoI[refine_mono]: 
  "monotone (fun_ord (≤)) (fun_ord (≤)) B  mono B"
  apply (simp add: le_fun_def[abs_def] fun_ord_def[abs_def])
  done

locale generic_WHILE =
  fixes bind :: "'m  ('a'm)  ('m::complete_lattice)"
  fixes return :: "'a  'm"
  fixes WHILEIT WHILEI WHILET WHILE 
  assumes imonad1: "bind (return x) f = f x"
  assumes imonad2: "bind M return = M"
  assumes imonad3: "bind (bind M f) g = bind M (λx. bind (f x) g)"
  assumes ibind_mono_ge: "flat_ge m m'; x. flat_ge (f x) (f' x) 
     flat_ge (bind m f) (bind m' f')"
  assumes ibind_mono: "(≤) m m'; x. (≤) (f x) (f' x) 
     (≤) (bind m f) (bind m' f')"
  assumes WHILEIT_eq: "WHILEIT  iWHILEIT bind return"
  assumes WHILEI_eq: "WHILEI  iWHILEI bind return"
  assumes WHILET_eq: "WHILET  iWHILET bind return"
  assumes WHILE_eq: "WHILE  iWHILE bind return"
begin

  lemmas WHILEIT_def = WHILEIT_eq[unfolded iWHILEIT_def [abs_def]]
  lemmas WHILEI_def = WHILEI_eq[unfolded iWHILEI_def [abs_def]]
  lemmas WHILET_def = WHILET_eq[unfolded iWHILET_def, folded WHILEIT_eq]
  lemmas WHILE_def = WHILE_eq[unfolded iWHILE_def [abs_def], folded WHILEI_eq]

  lemmas imonad_laws = imonad1 imonad2 imonad3
  
  lemmas [refine_mono] = ibind_mono_ge ibind_mono

(*  lemma ibind_mono: "m ≤ m' ⟹ f ≤ f' ⟹ bind m f ≤ bind m' f'"
    by (metis (no_types) ibind_mono1 ibind_mono2 le_funD monoD order_trans)
*)

lemma WHILEI_body_trimono: "trimono (WHILEI_body bind return I b f)"
  unfolding WHILEI_body_def 
  by refine_mono

lemmas WHILEI_mono = trimonoD_mono[OF WHILEI_body_trimono]
lemmas WHILEI_mono_ge = trimonoD_flatf_ge[OF WHILEI_body_trimono]


lemma WHILEI_unfold: "WHILEI I b f x = (
  if (I x) then (if b x then bind (f x) (WHILEI I b f) else return x) else top) "
  unfolding WHILEI_def
  apply (subst REC_unfold[OF WHILEI_body_trimono])
  unfolding WHILEI_body_def
  apply (rule refl)
  done

(* TODO: Move *)
lemma REC_mono_ref[refine_mono]: 
  "trimono B; D x. B D x  B' D x  REC B x  REC B' x"
  unfolding REC_def
  apply clarsimp
  apply (rule lfp_mono[THEN le_funD])
  by (rule le_funI)
  
lemma RECT_mono_ref[refine_mono]: 
  "trimono B; D x. B D x  B' D x  RECT B x  RECT B' x"
  unfolding RECT_gfp_def
  apply clarsimp
  apply (rule gfp_mono[THEN le_funD])
  by (rule le_funI)

lemma WHILEI_weaken:
  assumes IW: "x. I x  I' x"
  shows "WHILEI I' b f x  WHILEI I b f x"
  unfolding WHILEI_def
  apply (rule REC_mono_ref[OF WHILEI_body_trimono])
  apply (auto simp add: WHILEI_body_def dest: IW)
  done

lemma WHILEIT_unfold: "WHILEIT I b f x = (
  if (I x) then 
    (if b x then bind (f x) (WHILEIT I b f) else return x) 
  else top) "
  unfolding WHILEIT_def
  apply (subst RECT_unfold[OF WHILEI_body_trimono])
  unfolding WHILEI_body_def
  apply (rule refl)
  done

lemma WHILEIT_weaken:
  assumes IW: "x. I x  I' x"
  shows "WHILEIT I' b f x  WHILEIT I b f x"
  unfolding WHILEIT_def
  apply (rule RECT_mono_ref[OF WHILEI_body_trimono])
  apply (auto simp add: WHILEI_body_def dest: IW)
  done

lemma WHILEI_le_WHILEIT: "WHILEI I b f s  WHILEIT I b f s"
  unfolding WHILEI_def WHILEIT_def
  by (rule REC_le_RECT)

subsubsection ‹While without Annotated Invariant›

lemma WHILE_unfold: 
  "WHILE b f s = (if b s then bind (f s) (WHILE b f) else return s)"
  unfolding WHILE_def
  apply (subst WHILEI_unfold)
  apply simp
  done

lemma WHILET_unfold: 
  "WHILET b f s = (if b s then bind (f s) (WHILET b f) else return s)"
  unfolding WHILET_def
  apply (subst WHILEIT_unfold)
  apply simp
  done


lemma transfer_WHILEIT_esc[refine_transfer]:
  assumes REF: "x. return (f x)  F x"
  shows "return (while b f x)  WHILEIT I b F x"
proof -
  interpret transfer return .
  show ?thesis
    unfolding WHILEIT_def
    apply (rule transfer_RECT'[where fr="while b f"])
    apply (rule while_unfold)
    unfolding WHILEI_body_def
    apply (split if_split, intro allI impI conjI)+
    apply simp_all

    apply (rule order_trans[OF _ ibind_mono[OF REF order_refl]])
    apply (simp add: imonad_laws)
    done
qed

lemma transfer_WHILET_esc[refine_transfer]:
  assumes REF: "x. return (f x)  F x"
  shows "return (while b f x)  WHILET b F x"
  unfolding WHILET_def
  using assms by (rule transfer_WHILEIT_esc)


lemma WHILE_mono_prover_rule[refine_mono]:
  "x. f x  f' x  WHILE b f s0  WHILE b f' s0"
  "x. f x  f' x  WHILEI I b f s0  WHILEI I b f' s0"
  "x. f x  f' x  WHILET b f s0  WHILET b f' s0"
  "x. f x  f' x  WHILEIT I b f s0  WHILEIT I b f' s0"

  "x. flat_ge (f x) (f' x)  flat_ge (WHILET b f s0) (WHILET b f' s0)"
  "x. flat_ge (f x) (f' x)  flat_ge (WHILEIT I b f s0) (WHILEIT I b f' s0)"
  unfolding WHILE_def WHILEI_def WHILEI_body_def
    WHILET_def WHILEIT_def
  by refine_mono+

end

locale transfer_WHILE = 
  c: generic_WHILE cbind creturn cWHILEIT cWHILEI cWHILET cWHILE + 
  a: generic_WHILE abind areturn aWHILEIT aWHILEI aWHILET aWHILE +
  dist_transfer α
  for cbind and creturn::"'a  'mc::complete_lattice" 
  and cWHILEIT cWHILEI cWHILET cWHILE
  and abind and areturn::"'a  'ma::complete_lattice"
  and aWHILEIT aWHILEI aWHILET aWHILE
  and α :: "'mc  'ma" +
  assumes transfer_bind: "α m  M; x. α (f x)  F x  
     α (cbind m f)  abind M F"
  assumes transfer_return: "α (creturn x)  areturn x"
begin

lemma transfer_WHILEIT[refine_transfer]:
  assumes REF: "x. α (f x)  F x"
  shows "α (cWHILEIT I b f x)  aWHILEIT I b F x"
  unfolding c.WHILEIT_def a.WHILEIT_def
  apply (rule transfer_RECT[OF _ c.WHILEI_body_trimono])
  unfolding WHILEI_body_def
  apply auto
  apply (rule transfer_bind)
  apply (rule REF)
  apply assumption
  apply (rule transfer_return)
  done

lemma transfer_WHILEI[refine_transfer]:
  assumes REF: "x. α (f x)  F x"
  shows "α (cWHILEI I b f x)  aWHILEI I b F x"
  unfolding c.WHILEI_def a.WHILEI_def
  apply (rule transfer_REC[OF _ c.WHILEI_body_trimono])
  unfolding WHILEI_body_def
  apply auto
  apply (rule transfer_bind)
  apply (rule REF)
  apply assumption
  apply (rule transfer_return)
  done

lemma transfer_WHILE[refine_transfer]:
  assumes REF: "x. α (f x)  F x"
  shows "α (cWHILE b f x)  aWHILE b F x"
  unfolding c.WHILE_def a.WHILE_def
  using assms by (rule transfer_WHILEI)

lemma transfer_WHILET[refine_transfer]:
  assumes REF: "x. α (f x)  F x"
  shows "α (cWHILET b f x)  aWHILET b F x"
  unfolding c.WHILET_def a.WHILET_def
  using assms by (rule transfer_WHILEIT)

end

locale generic_WHILE_rules = 
  generic_WHILE bind return WHILEIT WHILEI WHILET WHILE
  for bind return SPEC WHILEIT WHILEI WHILET WHILE +
  assumes iSPEC_eq: "SPEC Φ = Sup {return x  | x. Φ x}"
  assumes ibind_rule: " M  SPEC (λx. f x  SPEC Φ)   bind M f  SPEC Φ"
begin

  lemma ireturn_eq: "return x = SPEC ((=) x)"
    unfolding iSPEC_eq by auto

  lemma iSPEC_rule: "(x. Φ x  Ψ x)  SPEC Φ  SPEC Ψ"
    unfolding iSPEC_eq
    by (auto intro: Sup_mono)

  lemma ireturn_rule: "Φ x  return x  SPEC Φ"
    unfolding ireturn_eq
    by (auto intro: iSPEC_rule)

lemma WHILEI_rule:
  assumes I0: "I s"
  assumes ISTEP: "s. I s; b s  f s  SPEC I"
  assumes CONS: "s.  I s; ¬ b s   Φ s"
  shows "WHILEI I b f s  SPEC Φ"
  apply (rule order_trans[where y="SPEC (λs. I s  ¬ b s)"])
    apply (unfold WHILEI_def)
    apply (rule REC_rule[OF WHILEI_body_trimono])
      apply (rule I0)
    
      unfolding WHILEI_body_def
      apply (split if_split)+
      apply (intro impI conjI)
      apply simp_all
      apply (rule ibind_rule)
        apply (erule (1) order_trans[OF ISTEP])
        apply (rule iSPEC_rule, assumption)
      
        apply (rule ireturn_rule)
        apply simp

    apply (rule iSPEC_rule)
    apply (simp add: CONS)
  done

lemma WHILEIT_rule:
  assumes WF: "wf R"
  assumes I0: "I s"
  assumes IS: "s.  I s; b s   f s  SPEC (λs'. I s'  (s',s)R)"
  assumes PHI: "s.  I s; ¬ b s   Φ s"
  shows "WHILEIT I b f s  SPEC Φ"

  unfolding WHILEIT_def
  apply (rule RECT_rule[OF WHILEI_body_trimono WF, where pre=I,OF I0])
  unfolding WHILEI_body_def
  apply (split if_split)+
  apply (intro impI conjI)
  apply simp_all

  apply (rule ibind_rule)
  apply (rule order_trans[OF IS], assumption+)
  apply (rule iSPEC_rule)
  apply simp

  apply (rule ireturn_rule)
  apply (simp add: PHI)
  done
  
lemma WHILE_rule:
  assumes I0: "I s"
  assumes ISTEP: "s. I s; b s  f s  SPEC I"
  assumes CONS: "s.  I s; ¬ b s   Φ s"
  shows "WHILE b f s  SPEC Φ"
  unfolding WHILE_def
  apply (rule order_trans[OF WHILEI_weaken WHILEI_rule])
  apply (rule TrueI)
  apply (rule I0)
  using assms by auto


lemma WHILET_rule:
  assumes WF: "wf R"
  assumes I0: "I s"
  assumes IS: "s.  I s; b s   f s  SPEC (λs'. I s'  (s',s)R)"
  assumes PHI: "s.  I s; ¬ b s   Φ s"
  shows "WHILET b f s  SPEC Φ"
  unfolding WHILET_def
  apply (rule order_trans[OF WHILEIT_weaken WHILEIT_rule])
  apply (rule TrueI)
  apply (rule WF)
  apply (rule I0)
  using assms by auto

end

end