# Theory 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"
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 [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]])
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)
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)
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
```