# Theory Refine_Leof

```section ‹Less-Equal or Fail›
(* TODO: Move to Refinement Framework *)
theory Refine_Leof
imports Refine_Basic
begin
text ‹A predicate that states refinement or that the LHS fails.›

definition le_or_fail :: "'a nres ⇒ 'a nres ⇒ bool" (infix "≤⇩n" 50) where
"m ≤⇩n m' ≡ nofail m ⟶ m ≤ m'"

lemma leofI[intro?]:
assumes "nofail m ⟹ m ≤ m'" shows "m ≤⇩n m'"
using assms unfolding le_or_fail_def by auto

lemma leofD:
assumes "nofail m"
assumes "m ≤⇩n m'"
shows "m ≤ m'"
using assms unfolding le_or_fail_def by blast

lemma pw_leof_iff:
"m ≤⇩n m' ⟷ (nofail m ⟶ (∀x. inres m x ⟶ inres m' x))"
unfolding le_or_fail_def by (auto simp add: pw_le_iff refine_pw_simps)

lemma le_by_leofI: "⟦ nofail m' ⟹ nofail m; m≤⇩nm' ⟧ ⟹ m ≤ m'"
by (auto simp: pw_le_iff pw_leof_iff)

lemma inres_leof_mono: "m≤⇩nm' ⟹ nofail m ⟹ inres m x ⟹ inres m' x"
by (auto simp: pw_leof_iff)

lemma leof_trans[trans]: "⟦a ≤⇩n RES X; RES X ≤⇩n c⟧ ⟹ a ≤⇩n c"
by (auto simp: pw_leof_iff)

lemma leof_trans_nofail: "⟦ a≤⇩nb; nofail b; b≤⇩nc ⟧ ⟹ a ≤⇩n c"
by (auto simp: pw_leof_iff)

lemma leof_refl[simp]: "a ≤⇩n a"
by (auto simp: pw_leof_iff)

lemma leof_RES_UNIV[simp, intro!]: "m ≤⇩n RES UNIV"
by (auto simp: pw_leof_iff)

lemma leof_FAIL[simp, intro!]: "m ≤⇩n FAIL" by (auto simp: pw_leof_iff)
lemma FAIL_leof[simp, intro!]: "FAIL ≤⇩n m"
by (auto simp: le_or_fail_def)

lemma leof_lift:
"m ≤ F ⟹ m ≤⇩n F"
by (auto simp add: pw_leof_iff pw_le_iff)

lemma leof_RETURN_rule[refine_vcg]:
"Φ m ⟹ RETURN m ≤⇩n SPEC Φ" by (simp add: pw_leof_iff)

lemma leof_bind_rule[refine_vcg]:
"⟦ m ≤⇩n SPEC (λx. f x ≤⇩n SPEC Φ) ⟧ ⟹ m⤜f ≤⇩n SPEC Φ"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma RETURN_leof_RES_iff[simp]: "RETURN x ≤⇩n RES Y ⟷ x∈Y"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma RES_leof_RES_iff[simp]: "RES X ≤⇩n RES Y ⟷ X ⊆ Y"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma leof_Let_rule[refine_vcg]: "f x ≤⇩n SPEC Φ ⟹ Let x f ≤⇩n SPEC Φ"
by simp

lemma leof_If_rule[refine_vcg]:
"⟦c ⟹ t ≤⇩n SPEC Φ; ¬c ⟹ e ≤⇩n SPEC Φ⟧ ⟹ If c t e ≤⇩n SPEC Φ"
by simp

lemma leof_RES_rule[refine_vcg]:
"⟦⋀x. Ψ x ⟹ Φ x⟧ ⟹ SPEC Ψ ≤⇩n SPEC Φ"
"⟦⋀x. x∈X ⟹ Φ x⟧ ⟹ RES X ≤⇩n SPEC Φ"
by auto

lemma leof_True_rule: "⟦⋀x. Φ x⟧ ⟹ m ≤⇩n SPEC Φ"
by (auto simp add: pw_leof_iff refine_pw_simps)

lemma sup_leof_iff: "(sup a b ≤⇩n m) ⟷ (nofail a ∧ nofail b ⟶ a≤⇩nm ∧ b≤⇩nm)"
by (auto simp: pw_leof_iff refine_pw_simps)

lemma sup_leof_rule[refine_vcg]:
assumes "⟦nofail a; nofail b⟧ ⟹ a≤⇩nm"
assumes "⟦nofail a; nofail b⟧ ⟹ b≤⇩nm"
shows "sup a b ≤⇩n m"
using assms by (auto simp: pw_leof_iff refine_pw_simps)

lemma leof_option_rule[refine_vcg]:
"⟦v = None ⟹ S1 ≤⇩n SPEC Φ; ⋀x. v = Some x ⟹ f2 x ≤⇩n SPEC Φ⟧
⟹ (case v of None ⇒ S1 | Some x ⇒ f2 x) ≤⇩n SPEC Φ"
by (cases v) auto

lemma ASSERT_leof_rule[refine_vcg]:
assumes "Φ ⟹ m ≤⇩n m'"
shows "do {ASSERT Φ; m} ≤⇩n m'"
using assms
by (cases Φ, auto simp: pw_leof_iff)

lemma leof_ASSERT_rule[refine_vcg]: "⟦Φ ⟹ m ≤⇩n m'⟧ ⟹ m ≤⇩n ASSERT Φ ⪢ m'"
by (auto simp: pw_leof_iff refine_pw_simps)

lemma leof_ASSERT_refine_rule[refine]: "⟦Φ ⟹ m ≤⇩n ⇓R m'⟧ ⟹ m ≤⇩n ⇓R (ASSERT Φ ⪢ m')"
by (auto simp: pw_leof_iff refine_pw_simps)

lemma ASSUME_leof_iff: "(ASSUME Φ ≤⇩n SPEC Ψ) ⟷ (Φ ⟶ Ψ ())"
by (auto simp: pw_leof_iff)

lemma ASSUME_leof_rule[refine_vcg]:
assumes "Φ ⟹ Ψ ()"
shows "ASSUME Φ ≤⇩n SPEC Ψ"
using assms
by (auto simp: ASSUME_leof_iff)

lemma SPEC_rule_conj_leofI1:
assumes "m ≤ SPEC Φ"
assumes "m ≤⇩n SPEC Ψ"
shows "m ≤ SPEC (λs. Φ s ∧ Ψ s)"
using assms by (auto simp: pw_le_iff pw_leof_iff)

lemma SPEC_rule_conj_leofI2:
assumes "m ≤⇩n SPEC Φ"
assumes "m ≤ SPEC Ψ"
shows "m ≤ SPEC (λs. Φ s ∧ Ψ s)"
using assms by (auto simp: pw_le_iff pw_leof_iff)

lemma SPEC_rule_leof_conjI:
assumes "m ≤⇩n SPEC Φ" "m ≤⇩n SPEC Ψ"
shows "m ≤⇩n SPEC (λx. Φ x ∧ Ψ x)"
using assms by (auto simp: pw_leof_iff)

lemma leof_use_spec_rule:
assumes "m ≤⇩n SPEC Ψ"
assumes "m ≤⇩n SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤⇩n SPEC Φ"
using assms by (auto simp: pw_leof_iff refine_pw_simps)

lemma use_spec_leof_rule:
assumes "m ≤⇩n SPEC Ψ"
assumes "m ≤ SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤ SPEC Φ"
using assms by (auto simp: pw_leof_iff pw_le_iff refine_pw_simps)

lemma leof_strengthen_SPEC:
"m ≤⇩n SPEC Φ ⟹ m ≤⇩n SPEC (λx. inres m x ∧ Φ x)"
by (auto simp: pw_leof_iff)

lemma build_rel_SPEC_leof:
assumes "m ≤⇩n SPEC (λx. I x ∧ Φ (α x))"
shows "m ≤⇩n ⇓(br α I) (SPEC Φ)"
using assms by (auto simp: build_rel_SPEC_conv)

lemma RETURN_as_SPEC_refine_leof[refine2]:
assumes "M ≤⇩n SPEC (λc. (c,a)∈R)"
shows "M ≤⇩n ⇓R (RETURN a)"
using assms

lemma ASSERT_leof_defI:
assumes "c ≡ do { ASSERT Φ; m'}"
assumes "Φ ⟹ m' ≤⇩n m"
shows "c ≤⇩n m"
using assms by (auto simp: pw_leof_iff refine_pw_simps)

lemma leof_fun_conv_le:
"(f x ≤⇩n M x) ⟷ (f x ≤ (if nofail (f x) then M x else FAIL))"
by (auto simp: pw_le_iff pw_leof_iff)

lemma leof_add_nofailI: "⟦ nofail m ⟹ m≤⇩nm' ⟧ ⟹ m≤⇩nm'"
by (auto simp: pw_le_iff pw_leof_iff)

lemma leof_cons_rule[refine_vcg_cons]:
assumes "m ≤⇩n SPEC Q"
assumes "⋀x. Q x ⟹ P x"
shows "m ≤⇩n SPEC P"
using assms
by (auto simp: pw_le_iff pw_leof_iff)

lemma RECT_rule_leof:
assumes WF: "wf (V::('x×'x) set)"
assumes I0: "pre (x::'x)"
assumes IS: "⋀f x. ⟦ ⋀x'. ⟦pre x'; (x',x)∈V⟧ ⟹ f x' ≤⇩n M x'; pre x;
RECT body = f
⟧ ⟹ body f x ≤⇩n M x"
shows "RECT body x ≤⇩n M x"
apply (cases "¬trimono body")
using assms
unfolding leof_fun_conv_le
apply -
apply (rule RECT_rule[where pre=pre and V=V])
apply clarsimp_all
proof -
fix xa :: 'x
assume a1: "⋀x'. ⟦pre x'; (x', xa) ∈ V⟧ ⟹ REC⇩T body x' ≤ (if nofail (REC⇩T body x') then M x' else FAIL)"
assume a2: "⋀x f. ⟦⋀x'. ⟦pre x'; (x', x) ∈ V⟧ ⟹ f x' ≤ (if nofail (f x') then M x' else FAIL); pre x; REC⇩T body = f⟧ ⟹ body f x ≤ (if nofail (body f x) then M x else FAIL)"
assume a3: "pre xa"
assume a4: "nofail (REC⇩T body xa)"
assume a5: "trimono body"
have f6: "∀x. ¬ pre x ∨ (x, xa) ∉ V ∨ (if nofail (REC⇩T body x) then REC⇩T body x ≤ M x else REC⇩T body x ≤ FAIL)"
using a1 by presburger
have f7: "∀x f. ((∃xa. (pre xa ∧ (xa, x) ∈ V) ∧ ¬ f xa ≤ (if nofail (f xa) then M xa else FAIL)) ∨ ¬ pre x ∨ REC⇩T body ≠ f) ∨ body f x ≤ (if nofail (body f x) then M x else FAIL)"
using a2 by blast
obtain xx :: "('x ⇒ 'a nres) ⇒ 'x ⇒ 'x" where
f8: "∀x0 x1. (∃v2. (pre v2 ∧ (v2, x1) ∈ V) ∧ ¬ x0 v2 ≤ (if nofail (x0 v2) then M v2 else FAIL)) = ((pre (xx x0 x1) ∧ (xx x0 x1, x1) ∈ V) ∧ ¬ x0 (xx x0 x1) ≤ (if nofail (x0 (xx x0 x1)) then M (xx x0 x1) else FAIL))"
by moura
have f9: "∀x0 x1. (x0 (xx x0 x1) ≤ (if nofail (x0 (xx x0 x1)) then M (xx x0 x1) else FAIL)) = (if nofail (x0 (xx x0 x1)) then x0 (xx x0 x1) ≤ M (xx x0 x1) else x0 (xx x0 x1) ≤ FAIL)"
by presburger
have "nofail (body (REC⇩T body) xa)"
using a5 a4 by (metis (no_types) RECT_unfold)
then show "body (REC⇩T body) xa ≤ M xa"
using f9 f8 f7 f6 a3 by fastforce
qed

(* TODO: REC_rule_leof! (However, this may require some fix
to the domain theory model of Refine_Monadic!) *)

end

```