Theory MonadSE
theory MonadSE
imports Main
begin
section‹Definition : Standard State Exception Monads›
text‹State exception monads in our sense are a direct, pure formulation
of automata with a partial transition function.›
subsection‹Definition : Core Types and Operators›
type_synonym ('o, 'σ) MON⇩S⇩E = "'σ ⇀ ('o × 'σ)"
definition bind_SE :: "('o,'σ)MON⇩S⇩E ⇒ ('o ⇒ ('o','σ)MON⇩S⇩E) ⇒ ('o','σ)MON⇩S⇩E"
where "bind_SE f g = (λσ. case f σ of None ⇒ None
| Some (out, σ') ⇒ g out σ')"
notation bind_SE (‹bind⇩S⇩E›)
syntax (xsymbols)
"_bind_SE" :: "[pttrn,('o,'σ)MON⇩S⇩E,('o','σ)MON⇩S⇩E] ⇒ ('o','σ)MON⇩S⇩E"
(‹(2 _ ← _; _)› [5,8,8]8)
translations
"x ← f; g" == "CONST bind_SE f (% x . g)"
definition unit_SE :: "'o ⇒ ('o, 'σ)MON⇩S⇩E" (‹(result _)› 8)
where "unit_SE e = (λσ. Some(e,σ))"
notation unit_SE (‹unit⇩S⇩E›)
text‹In the following, we prove the required Monad-laws›
lemma bind_right_unit[simp]: "(x ← m; result x) = m"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
apply (case_tac "m σ", simp_all)
done
lemma bind_left_unit [simp]: "(x ← result c; P x) = P c"
by (simp add: unit_SE_def bind_SE_def)
lemma bind_assoc[simp]: "(y ← (x ← m; k x); h y) = (x ← m; (y ← k x; h y))"
apply (simp add: unit_SE_def bind_SE_def, rule ext)
apply (case_tac "m σ", simp_all)
apply (case_tac "a", simp_all)
done
subsection‹Definition : More Operators and their Properties›
definition fail_SE :: "('o, 'σ)MON⇩S⇩E"
where "fail_SE = (λσ. None)"
notation fail_SE (‹fail⇩S⇩E›)
definition assert_SE :: "('σ ⇒ bool) ⇒ (bool, 'σ)MON⇩S⇩E"
where "assert_SE P = (λσ. if P σ then Some(True,σ) else None)"
notation assert_SE (‹assert⇩S⇩E›)
definition assume_SE :: "('σ ⇒ bool) ⇒ (unit, 'σ)MON⇩S⇩E"
where "assume_SE P = (λσ. if ∃σ . P σ then Some((), SOME σ . P σ) else None)"
notation assume_SE (‹assume⇩S⇩E›)
lemma bind_left_fail_SE[simp] : "(x ← fail⇩S⇩E; P x) = fail⇩S⇩E"
by (simp add: fail_SE_def bind_SE_def)
text‹We also provide a "Pipe-free" - variant of the bind operator.
Just a "standard" programming sequential operator without output frills.›
definition bind_SE' :: "('α, 'σ)MON⇩S⇩E ⇒ ('β, 'σ)MON⇩S⇩E ⇒ ('β, 'σ)MON⇩S⇩E" (infixr ‹;-› 10)
where "(f ;- g) = (_ ← f ; g)"
lemma bind_assoc'[simp]: "((m ;- k);- h ) = (m;- (k;- h))"
by(simp add:bind_SE'_def)
lemma bind_left_unit' [simp]: "((result c);- P) = P"
by (simp add: bind_SE'_def)
lemma bind_left_fail_SE'[simp]: "(fail⇩S⇩E;- P) = fail⇩S⇩E"
by (simp add: bind_SE'_def)
lemma bind_right_unit'[simp]: "(m;- (result ())) = m"
by (simp add: bind_SE'_def)
text‹The bind-operator in the state-exception monad yields already
a semantics for the concept of an input sequence on the meta-level:›
lemma syntax_test: "(o1 ← f1 ; o2 ← f2; result (post o1 o2)) = X"
oops
definition yield⇩C :: "('a ⇒ 'b) ⇒ ('b,'a ) MON⇩S⇩E"
where "yield⇩C f ≡ (λσ. Some(f σ, σ))"
definition try_SE :: "('o,'σ) MON⇩S⇩E ⇒ ('o option,'σ) MON⇩S⇩E" (‹try⇩S⇩E›)
where "try⇩S⇩E ioprog = (λσ. case ioprog σ of
None ⇒ Some(None, σ)
| Some(outs, σ') ⇒ Some(Some outs, σ'))"
text‹In contrast, mbind as a failure safe operator can roughly be seen
as a foldr on bind - try:
m1 ; try m2 ; try m3; ... Note, that the rough equivalence only holds for
certain predicates in the sequence - length equivalence modulo None,
for example. However, if a conditional is added, the equivalence
can be made precise:›
text‹On this basis, a symbolic evaluation scheme can be established
that reduces mbind-code to try\_SE\_code and ite-cascades.›
definition alt_SE :: "[('o, 'σ)MON⇩S⇩E, ('o, 'σ)MON⇩S⇩E] ⇒ ('o, 'σ)MON⇩S⇩E" (infixl ‹⊓⇩S⇩E› 10)
where "(f ⊓⇩S⇩E g) = (λ σ. case f σ of None ⇒ g σ
| Some H ⇒ Some H)"
definition malt_SE :: "('o, 'σ)MON⇩S⇩E list ⇒ ('o, 'σ)MON⇩S⇩E"
where "malt_SE S = foldr alt_SE S fail⇩S⇩E"
notation malt_SE (‹⨅⇩S⇩E›)
lemma malt_SE_mt [simp]: "⨅⇩S⇩E [] = fail⇩S⇩E"
by(simp add: malt_SE_def)
lemma malt_SE_cons [simp]: "⨅⇩S⇩E (a # S) = (a ⊓⇩S⇩E (⨅⇩S⇩E S))"
by(simp add: malt_SE_def)
subsection‹Definition : Programming Operators and their Properties›
definition "skip⇩S⇩E = unit⇩S⇩E ()"
definition if_SE :: "['σ ⇒ bool, ('α, 'σ)MON⇩S⇩E, ('α, 'σ)MON⇩S⇩E] ⇒ ('α, 'σ)MON⇩S⇩E"
where "if_SE c E F = (λσ. if c σ then E σ else F σ)"
syntax (xsymbols)
"_if_SE" :: "['σ ⇒ bool,('o,'σ)MON⇩S⇩E,('o','σ)MON⇩S⇩E] ⇒ ('o','σ)MON⇩S⇩E"
(‹(if⇩S⇩E _ then _ else _fi)› [5,8,8]8)
translations
"(if⇩S⇩E cond then T1 else T2 fi)" == "CONST if_SE cond T1 T2"
subsection‹Theory of a Monadic While›
text‹Prerequisites›
fun replicator :: "[('a, 'σ)MON⇩S⇩E, nat] ⇒ (unit, 'σ)MON⇩S⇩E" (infixr ‹^^^› 60)
where "f ^^^ 0 = (result ())"
| "f ^^^ (Suc n) = (f ;- f ^^^ n)"
fun replicator2 :: "[('a, 'σ)MON⇩S⇩E, nat, ('b, 'σ)MON⇩S⇩E] ⇒ ('b, 'σ)MON⇩S⇩E" (infixr ‹^:^› 60)
where "(f ^:^ 0) M = (M )"
| "(f ^:^ (Suc n)) M = (f ;- ((f ^:^ n) M))"
text‹First Step : Establishing an embedding between partial functions and relations›
definition Mon2Rel :: "(unit, 'σ)MON⇩S⇩E ⇒ ('σ × 'σ) set"
where "Mon2Rel f = {(x, y). (f x = Some((), y))}"
definition Rel2Mon :: " ('σ × 'σ) set ⇒ (unit, 'σ)MON⇩S⇩E "
where "Rel2Mon S = (λ σ. if ∃σ'. (σ, σ') ∈ S then Some((), SOME σ'. (σ, σ') ∈ S) else None)"
lemma Mon2Rel_Rel2Mon_id: assumes det:"single_valued R" shows "(Mon2Rel ∘ Rel2Mon) R = R"
apply (simp add: comp_def Mon2Rel_def Rel2Mon_def,auto)
apply (case_tac "∃σ'. (a, σ') ∈ R", auto)
apply (subst (2) some_eq_ex)
using det[simplified single_valued_def] by auto
lemma Rel2Mon_Id: "(Rel2Mon ∘ Mon2Rel) x = x"
apply (rule ext)
apply (auto simp: comp_def Mon2Rel_def Rel2Mon_def)
apply (erule contrapos_pp, drule HOL.not_sym, simp)
done
lemma single_valued_Mon2Rel: "single_valued (Mon2Rel B)"
by (auto simp: single_valued_def Mon2Rel_def)
text‹Second Step : Proving an induction principle allowing to establish that lfp remains
deterministic›
definition chain :: "(nat ⇒ 'a set) ⇒ bool"
where "chain S = (∀i. S i ⊆ S(Suc i))"
lemma chain_total: "chain S ==> S i ≤ S j ∨ S j ≤ S i"
by (metis chain_def le_cases lift_Suc_mono_le)
definition cont :: "('a set => 'b set) => bool"
where "cont f = (∀S. chain S ⟶ f(UN n. S n) = (UN n. f(S n)))"
lemma mono_if_cont: fixes f :: "'a set ⇒ 'b set"
assumes "cont f" shows "mono f"
proof
fix a b :: "'a set" assume "a ⊆ b"
let ?S = "λn::nat. if n=0 then a else b"
have "chain ?S" using ‹a ⊆ b› by(auto simp: chain_def)
hence "f(UN n. ?S n) = (UN n. f(?S n))"
using assms by (metis cont_def)
moreover have "(UN n. ?S n) = b" using ‹a ⊆ b› by (auto split: if_splits)
moreover have "(UN n. f(?S n)) = f a ∪ f b" by (auto split: if_splits)
ultimately show "f a ⊆ f b" by (metis Un_upper1)
qed
lemma chain_iterates: fixes f :: "'a set ⇒ 'a set"
assumes "mono f" shows "chain(λn. (f^^n) {})"
proof-
{ fix n have "(f ^^ n) {} ⊆ (f ^^ Suc n) {}" using assms
by(induction n) (auto simp: mono_def) }
thus ?thesis by(auto simp: chain_def)
qed
theorem lfp_if_cont:
assumes "cont f" shows "lfp f = (⋃n. (f ^^ n) {})" (is "_ = ?U")
proof
show "lfp f ⊆ ?U"
proof (rule lfp_lowerbound)
have "f ?U = (UN n. (f^^Suc n){})"
using chain_iterates[OF mono_if_cont[OF assms]] assms
by(simp add: cont_def)
also have "… = (f^^0){} ∪ …" by simp
also have "… = ?U"
apply(auto simp del: funpow.simps)
by (metis empty_iff funpow_0 old.nat.exhaust)
finally show "f ?U ⊆ ?U" by simp
qed
next
{ fix n p assume "f p ⊆ p"
have "(f^^n){} ⊆ p"
proof(induction n)
case 0 show ?case by simp
next
case Suc
from monoD[OF mono_if_cont[OF assms] Suc] ‹f p ⊆ p›
show ?case by simp
qed
}
thus "?U ⊆ lfp f" by(auto simp: lfp_def)
qed
lemma single_valued_UN_chain:
assumes "chain S" "(!!n. single_valued (S n))"
shows "single_valued(UN n. S n)"
proof(auto simp: single_valued_def)
fix m n x y z assume "(x, y) ∈ S m" "(x, z) ∈ S n"
with chain_total[OF assms(1), of m n] assms(2)
show "y = z" by (auto simp: single_valued_def)
qed
lemma single_valued_lfp:
fixes f :: "('a × 'a) set ⇒ ('a × 'a) set"
assumes "cont f" "⋀r. single_valued r ⟹ single_valued (f r)"
shows "single_valued(lfp f)"
unfolding lfp_if_cont[OF assms(1)]
proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]])
fix n show "single_valued ((f ^^ n) {})"
by(induction n)(auto simp: assms(2))
qed
text‹Third Step: Definition of the Monadic While ‹ ››
definition Γ :: "['σ ⇒ bool,('σ × 'σ) set] ⇒ (('σ × 'σ) set ⇒ ('σ × 'σ) set)"
where "Γ b cd = (λcw. {(s,t). if b s then (s, t) ∈ cd O cw else s = t})"
definition while_SE :: "['σ ⇒ bool, (unit, 'σ)MON⇩S⇩E] ⇒ (unit, 'σ)MON⇩S⇩E"
where "while_SE c B ≡ (Rel2Mon(lfp(Γ c (Mon2Rel B))))"
syntax (xsymbols)
"_while_SE" :: "['σ ⇒ bool, (unit, 'σ)MON⇩S⇩E] ⇒ (unit, 'σ)MON⇩S⇩E"
(‹(while⇩S⇩E _ do _ od)› [8,8]8)
translations
"while⇩S⇩E c do b od" == "CONST while_SE c b"
lemma cont_Γ: "cont (Γ c b)"
by (auto simp: cont_def Γ_def)
text‹The fixpoint theory now allows us to establish that the lfp constructed over
@{term Mon2Rel} remains deterministic›
theorem single_valued_lfp_Mon2Rel: "single_valued (lfp(Γ c (Mon2Rel B)))"
apply(rule single_valued_lfp, simp_all add: cont_Γ)
apply(auto simp: Γ_def single_valued_def)
apply(metis single_valued_Mon2Rel[of "B"] single_valued_def)
done
lemma Rel2Mon_if:
"Rel2Mon {(s, t). if b s then (s, t) ∈ Mon2Rel c O lfp (Γ b (Mon2Rel c)) else s = t} σ =
(if b σ then Rel2Mon (Mon2Rel c O lfp (Γ b (Mon2Rel c))) σ else Some ((), σ))"
by (simp add: Rel2Mon_def)
lemma Rel2Mon_homomorphism:
assumes determ_X: "single_valued X" and determ_Y: "single_valued Y"
shows "Rel2Mon (X O Y) = ((Rel2Mon X) ;- (Rel2Mon Y))"
proof -
have relational_partial_next_in_O: "⋀x E F. (∃y. (x, y) ∈ (E O F)) ⟹ (∃y. (x, y) ∈ E)"
by (auto)
have some_eq_intro: "⋀ X x y . single_valued X ⟹ (x, y) ∈ X ⟹ (SOME y. (x, y) ∈ X) = y"
by (auto simp: single_valued_def)
show ?thesis
apply (simp add: Rel2Mon_def bind_SE'_def bind_SE_def)
apply (rule ext, rename_tac "σ")
apply (case_tac " ∃ σ'. (σ, σ') ∈ X O Y")
apply (simp only: HOL.if_True)
apply (frule relational_partial_next_in_O)
apply (auto simp: single_valued_relcomp some_eq_intro determ_X determ_Y relcomp.relcompI)
by blast
qed
text‹Putting everything together, the theory of embedding and the invariance of
determinism of the while-body, gives us the usual unfold-theorem:›
theorem while_SE_unfold:
"(while⇩S⇩E b do c od) = (if⇩S⇩E b then (c ;- (while⇩S⇩E b do c od)) else result () fi)"
apply (simp add: if_SE_def bind_SE'_def while_SE_def unit_SE_def)
apply (subst lfp_unfold [OF mono_if_cont, OF cont_Γ])
apply (rule ext)
apply (subst Γ_def)
apply (auto simp: Rel2Mon_if Rel2Mon_homomorphism bind_SE'_def Rel2Mon_Id [simplified comp_def]
single_valued_Mon2Rel single_valued_lfp_Mon2Rel )
done
lemma bind_cong : " f σ = g σ ⟹ (x ← f ; M x)σ = (x ← g ; M x)σ"
unfolding bind_SE'_def bind_SE_def by simp
lemma bind'_cong : " f σ = g σ ⟹ (f ;- M )σ = (g ;- M )σ"
unfolding bind_SE'_def bind_SE_def by simp
lemma if⇩S⇩E_True [simp]: "(if⇩S⇩E (λ x. True) then c else d fi) = c"
apply(rule ext) by (simp add: MonadSE.if_SE_def)
lemma if⇩S⇩E_False [simp]: "(if⇩S⇩E (λ x. False) then c else d fi) = d"
apply(rule ext) by (simp add: MonadSE.if_SE_def)
lemma if⇩S⇩E_cond_cong : "f σ = g σ ⟹
(if⇩S⇩E f then c else d fi) σ =
(if⇩S⇩E g then c else d fi) σ"
unfolding if_SE_def by simp
lemma while⇩S⇩E_skip[simp] : "(while⇩S⇩E (λ x. False) do c od) = skip⇩S⇩E"
apply(rule ext,subst MonadSE.while_SE_unfold)
by (simp add: MonadSE.if_SE_def skip⇩S⇩E_def)
end