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