# Theory Refine_Det

```section ‹Deterministic Monad›
theory Refine_Det
imports
"Generic/RefineG_Assert"
"Generic/RefineG_While"
begin

subsection ‹Deterministic Result Lattice›
text ‹
We define the flat complete lattice of deterministic program results:
›
(* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
an isomorphic contruction. *)
datatype 'a dres =
dSUCCEEDi   ― ‹No result›
| dFAILi      ― ‹Failure›
| dRETURN 'a  ― ‹Regular result›

instantiation dres :: (type) complete_lattice
begin
definition "top_dres ≡ dFAILi"
definition "bot_dres ≡ dSUCCEEDi"
fun sup_dres where
"sup dFAILi _ = dFAILi" |
"sup _ dFAILi = dFAILi" |
"sup (dRETURN a) (dRETURN b) = (if a=b then dRETURN b else dFAILi)" |
"sup dSUCCEEDi x = x" |
"sup x dSUCCEEDi = x"

"sup x dFAILi = dFAILi"
"sup x dSUCCEEDi = x"
apply (case_tac [!] x)
apply simp_all
done

fun inf_dres where
"inf dFAILi x = x" |
"inf x dFAILi = x" |
"inf (dRETURN a) (dRETURN b) = (if a=b then dRETURN b else dSUCCEEDi)" |
"inf dSUCCEEDi _ = dSUCCEEDi" |
"inf _ dSUCCEEDi = dSUCCEEDi"

"inf x dSUCCEEDi = dSUCCEEDi"
"inf dSUCCEEDi x = dSUCCEEDi"
"inf x dFAILi = x"
"inf (dRETURN v) x ≠ dFAILi"
apply (case_tac [!] x)
apply simp_all
done

definition "Sup_dres S ≡
if S⊆{dSUCCEEDi} then dSUCCEEDi
else if dFAILi∈S then dFAILi
else if ∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S then dFAILi
else dRETURN (THE x. dRETURN x ∈ S)"

definition "Inf_dres S ≡
if S⊆{dFAILi} then dFAILi
else if dSUCCEEDi∈S then dSUCCEEDi
else if ∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S then dSUCCEEDi
else dRETURN (THE x. dRETURN x ∈ S)"

fun less_eq_dres where
"less_eq_dres dSUCCEEDi _ ⟷ True" |
"less_eq_dres _ dFAILi ⟷ True" |
"less_eq_dres (dRETURN (a::'a)) (dRETURN b) ⟷ a=b" |
"less_eq_dres _ _ ⟷ False"

definition less_dres where "less_dres (a::'a dres) b ⟷ a≤b ∧ ¬ b≤a"

lemma less_eq_dres_split_conv:
"a≤b ⟷ (case (a,b) of
(dSUCCEEDi,_) ⇒ True
| (_,dFAILi) ⇒ True
| (dRETURN (a::'a), dRETURN b) ⇒ a=b
| _ ⇒ False
)"
by (auto split: dres.split)

lemma inf_dres_split_conv:
"inf a b = (case (a,b) of
(dFAILi,x) ⇒ x
| (x,dFAILi) ⇒ x
| (dRETURN a, dRETURN b) ⇒ (if a=b then dRETURN b else dSUCCEEDi)
| _ ⇒ dSUCCEEDi)"
by (auto split: dres.split)

lemma sup_dres_split_conv:
"sup a b = (case (a,b) of
(dSUCCEEDi,x) ⇒ x
| (x,dSUCCEEDi) ⇒ x
| (dRETURN a, dRETURN b) ⇒ (if a=b then dRETURN b else dFAILi)
| _ ⇒ dFAILi)"
by (auto split: dres.split)

instance
apply intro_classes
supply less_eq_dres_split_conv[simp] less_dres_def[simp] dres.splits[split]
supply inf_dres_split_conv[simp] sup_dres_split_conv[simp] if_splits[split]
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: Inf_dres_def)
subgoal for A z
apply (clarsimp simp: Inf_dres_def; safe)
subgoal by force
subgoal by force
subgoal premises prems
using prems(2-) apply (drule_tac prems(1)) apply (drule_tac prems(1))
apply (auto)
done
subgoal premises prems
using prems(2-) apply (frule_tac prems(1))
by (auto; metis the_equality)
done
subgoal by (auto simp: Sup_dres_def; metis the_equality)
subgoal
apply (clarsimp simp: Sup_dres_def; safe)
apply force
apply force
subgoal premises prems
using prems(2-)
apply (drule_tac prems(1))
apply (drule_tac prems(1))
apply (drule_tac prems(1))
apply (auto)
done
apply force
subgoal premises prems
using prems(2-) apply (frule_tac prems(1))
by (auto; metis the_equality)
done
subgoal by (auto simp: Inf_dres_def top_dres_def)
subgoal by (auto simp: Sup_dres_def bot_dres_def)
done

end

abbreviation "dSUCCEED ≡ (bot::'a dres)"
abbreviation "dFAIL ≡ (top::'a dres)"

lemma dres_cases[cases type, case_names dSUCCEED dRETURN dFAIL]:
obtains "x=dSUCCEED" | r where "x=dRETURN r" | "x=dFAIL"
unfolding bot_dres_def top_dres_def by (cases x) auto

lemmas [simp] = dres.case(1,2)[folded top_dres_def bot_dres_def]

lemma dres_order_simps[simp]:
"x≤dSUCCEED ⟷ x=dSUCCEED"
"dFAIL≤x ⟷ x=dFAIL"
"dRETURN r ≠ dFAIL"
"dRETURN r ≠ dSUCCEED"
"dFAIL ≠ dRETURN r"
"dSUCCEED ≠ dRETURN r"
"dFAIL≠dSUCCEED"
"dSUCCEED≠dFAIL"
"x=y ⟹ inf (dRETURN x) (dRETURN y) = dRETURN y"
"x≠y ⟹ inf (dRETURN x) (dRETURN y) = dSUCCEED"
"x=y ⟹ sup (dRETURN x) (dRETURN y) = dRETURN y"
"x≠y ⟹ sup (dRETURN x) (dRETURN y) = dFAIL"
done

lemma dres_Sup_cases:
obtains "S⊆{dSUCCEED}" and "Sup S = dSUCCEED"
| "dFAIL∈S" and "Sup S = dFAIL"
| a b where "a≠b" "dRETURN a∈S" "dRETURN b∈S" "dFAIL∉S" "Sup S = dFAIL"
| a where "S ⊆ {dSUCCEED, dRETURN a}" "dRETURN a∈S" "Sup S = dRETURN a"
proof -
show ?thesis
apply (cases "S⊆{dSUCCEED}")
apply (rule that(1), assumption)

apply (cases "dFAIL∈S")
apply (rule that(2), assumption)
apply (simp add: Sup_dres_def bot_dres_def top_dres_def)

apply (cases "∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S")
apply (elim exE conjE)
apply (rule that(3), assumption+)
apply (auto simp add: Sup_dres_def bot_dres_def top_dres_def) []

apply simp
apply (cases "∃a. dRETURN a ∈ S")
apply (elim exE)
apply (rule_tac a=a in that(4)) []
apply auto [] apply (case_tac xa, auto) []
apply auto []
apply (auto simp add: Sup_dres_def bot_dres_def top_dres_def) []

apply auto apply (case_tac x, auto) []
done
qed

lemma dres_Inf_cases:
obtains "S⊆{dFAIL}" and "Inf S = dFAIL"
| "dSUCCEED∈S" and "Inf S = dSUCCEED"
| a b where "a≠b" "dRETURN a∈S" "dRETURN b∈S" "dSUCCEED∉S" "Inf S = dSUCCEED"
| a where "S ⊆ {dFAIL, dRETURN a}" "dRETURN a∈S" "Inf S = dRETURN a"
proof -
show ?thesis
apply (cases "S⊆{dFAIL}")
apply (rule that(1), assumption)

apply (cases "dSUCCEED∈S")
apply (rule that(2), assumption)
apply (simp add: Inf_dres_def bot_dres_def top_dres_def)

apply (cases "∃a b. a≠b ∧ dRETURN a∈S ∧ dRETURN b∈S")
apply (elim exE conjE)
apply (rule that(3), assumption+)
apply (auto simp add: Inf_dres_def bot_dres_def top_dres_def) []

apply simp
apply (cases "∃a. dRETURN a ∈ S")
apply (elim exE)
apply (rule_tac a=a in that(4)) []
apply auto [] apply (case_tac xa, auto) []
apply auto []
apply (auto simp add: Inf_dres_def bot_dres_def top_dres_def) []

apply auto apply (case_tac x, auto) []
done
qed

lemma dres_chain_eq_res:
"is_chain M ⟹
dRETURN r ∈ M ⟹ dRETURN s ∈ M ⟹ r=s"
by (metis chainD less_eq_dres.simps(4))

lemma dres_Sup_chain_cases:
assumes CHAIN: "is_chain M"
obtains "M ⊆ {dSUCCEED}" "Sup M = dSUCCEED"
| r where "M ⊆ {dSUCCEED,dRETURN r}" "dRETURN r∈M" "Sup M = dRETURN r"
| "dFAIL∈M" "Sup M = dFAIL"
apply (rule dres_Sup_cases[of M])
using dres_chain_eq_res[OF CHAIN]
by auto

lemma dres_Inf_chain_cases:
assumes CHAIN: "is_chain M"
obtains "M ⊆ {dFAIL}" "Inf M = dFAIL"
| r where "M ⊆ {dFAIL,dRETURN r}" "dRETURN r∈M" "Inf M = dRETURN r"
| "dSUCCEED∈M" "Inf M = dSUCCEED"
apply (rule dres_Inf_cases[of M])
using dres_chain_eq_res[OF CHAIN]
by auto

lemma dres_internal_simps[simp]:
"dSUCCEEDi = dSUCCEED"
"dFAILi = dFAIL"
unfolding top_dres_def bot_dres_def by auto

function dbind where
"dbind dFAIL _ = dFAIL"
| "dbind dSUCCEED _ = dSUCCEED"
| "dbind (dRETURN x) f = f x"
unfolding bot_dres_def top_dres_def
by pat_completeness auto
termination by lexicographic_order

lemma [code]:
"dbind (dRETURN x) f = f x"
"dbind (dSUCCEEDi) f = dSUCCEEDi"
"dbind (dFAILi) f = dFAILi"
by simp_all

lemma dres_monad1[simp]: "dbind (dRETURN x) f = f x"
by (simp)
lemma dres_monad2[simp]: "dbind M dRETURN = M"
apply (cases M)
apply (auto)
done

lemma dres_monad3[simp]: "dbind (dbind M f) g = dbind M (λx. dbind (f x) g)"
apply (cases M)
apply auto
done

lemma dbind_mono[refine_mono]:
"⟦ M ≤ M'; ⋀x. dRETURN x ≤ M ⟹ f x ≤ f' x ⟧ ⟹ dbind M f ≤ dbind M' f'"
"⟦ flat_ge M M'; ⋀x. flat_ge (f x) (f' x) ⟧ ⟹ flat_ge (dbind M f) (dbind M' f')"
apply (cases M, simp_all)
apply (cases M', simp_all)
apply (cases M, simp_all add: flat_ord_def)
apply (cases M', simp_all)
done

lemma dbind_mono1[simp, intro!]: "mono dbind"
apply (rule monoI)
apply (rule le_funI)
apply (rule dbind_mono)
by auto

lemma dbind_mono2[simp, intro!]: "mono (dbind M)"
apply (rule monoI)
apply (rule dbind_mono)
by (auto dest: le_funD)

lemma dr_mono_bind:
assumes MA: "mono A" and MB: "⋀s. mono (B s)"
shows "mono (λF s. dbind (A F s) (λs'. B s F s'))"
apply (rule monoI)
apply (rule le_funI)
apply (rule dbind_mono)
apply (auto dest: monoD[OF MA, THEN le_funD]) []
apply (auto dest: monoD[OF MB, THEN le_funD]) []
done

lemma dr_mono_bind': "mono (λF s. dbind (f s) F)"
apply rule
apply (rule le_funI)
apply (rule dbind_mono)
apply (auto dest: le_funD)
done

(* TODO: Replace by monotonicity prover! *)
lemmas dr_mono = mono_if dr_mono_bind dr_mono_bind' mono_const mono_id

lemma [refine_mono]:
"dbind dSUCCEED f = dSUCCEED"
"dbind dFAIL f = dFAIL"
by (simp_all)

definition "dASSERT ≡ iASSERT dRETURN"
definition "dASSUME ≡ iASSUME dRETURN"
interpretation dres_assert: generic_Assert dbind dRETURN dASSERT dASSUME
apply unfold_locales
by (auto simp: dASSERT_def dASSUME_def)

definition "dWHILEIT ≡ iWHILEIT dbind dRETURN"
definition "dWHILEI ≡ iWHILEI dbind dRETURN"
definition "dWHILET ≡ iWHILET dbind dRETURN"
definition "dWHILE ≡ iWHILE dbind dRETURN"

interpretation dres_while: generic_WHILE dbind dRETURN
dWHILEIT dWHILEI dWHILET dWHILE
apply unfold_locales
apply (auto simp: dWHILEIT_def dWHILEI_def dWHILET_def dWHILE_def)
apply refine_mono+
done

lemmas [code] =
dres_while.WHILEIT_unfold
dres_while.WHILEI_unfold
dres_while.WHILET_unfold
dres_while.WHILE_unfold

text ‹
Syntactic criteria to prove ‹s ≠ dSUCCEED›
›
lemma dres_ne_bot_basic[refine_transfer]:
"dFAIL ≠ dSUCCEED"
"⋀x. dRETURN x ≠ dSUCCEED"
"⋀m f. ⟦ m≠dSUCCEED; ⋀x. f x ≠ dSUCCEED ⟧ ⟹ dbind m f ≠ dSUCCEED"
"⋀Φ. dASSERT Φ ≠ dSUCCEED"
"⋀b m1 m2. ⟦ m1≠dSUCCEED; m2≠dSUCCEED ⟧ ⟹ If b m1 m2 ≠ dSUCCEED"
"⋀x f. ⟦ ⋀x. f x≠dSUCCEED ⟧ ⟹ Let x f ≠ dSUCCEED"
"⋀g p. ⟦ ⋀x1 x2. g x1 x2 ≠ dSUCCEED ⟧ ⟹ case_prod g p ≠ dSUCCEED"
"⋀fn fs x.
⟦ fn≠dSUCCEED; ⋀v. fs v ≠ dSUCCEED ⟧ ⟹ case_option fn fs x ≠ dSUCCEED"
"⋀fn fc x.
⟦ fn≠dSUCCEED; ⋀x xs. fc x xs ≠ dSUCCEED ⟧ ⟹ case_list fn fc x ≠ dSUCCEED"
apply (auto split: prod.split option.split list.split)
apply (case_tac m, auto) []
apply (case_tac Φ, auto) []
done

lemma dres_ne_bot_RECT[refine_transfer]:
assumes A: "⋀f x. ⟦ ⋀x. f x ≠ dSUCCEED ⟧ ⟹ B f x ≠ dSUCCEED"
shows "RECT B x ≠ dSUCCEED"
unfolding RECT_def
apply (split if_split)
apply (intro impI conjI)
apply simp_all

apply (rule flatf_fp_induct_pointwise[where pre="λ_ _. True" and B=B and b=top and post="λ_ _ m. m≠dSUCCEED"])
done

lemma dres_ne_bot_dWHILEIT[refine_transfer]:
assumes "⋀x. f x ≠ dSUCCEED"
shows "dWHILEIT I b f s ≠ dSUCCEED" using assms
unfolding dWHILEIT_def iWHILEIT_def WHILEI_body_def
apply refine_transfer
done

lemma dres_ne_bot_dWHILET[refine_transfer]:
assumes "⋀x. f x ≠ dSUCCEED"
shows "dWHILET b f s ≠ dSUCCEED" using assms
unfolding dWHILET_def iWHILET_def iWHILEIT_def WHILEI_body_def
apply refine_transfer
done

end
```