theory Sepreftime
imports "HOL-Library.Extended_Nat" "Refine_Monadic.RefineG_Domain" Refine_Monadic.Refine_Misc
"HOL-Library.Monad_Syntax" Sepreftime_Auxiliaries
begin
section "NREST"
datatype 'a nrest = FAILi | REST "'a ⇒ enat option"
instantiation nrest :: (type) complete_lattice
begin
fun less_eq_nrest where
"_ ≤ FAILi ⟷ True" |
"(REST a) ≤ (REST b) ⟷ a ≤ b" |
"FAILi ≤ (REST _) ⟷ False"
fun less_nrest where
"FAILi < _ ⟷ False" |
"(REST _) < FAILi ⟷ True" |
"(REST a) < (REST b) ⟷ a < b"
fun sup_nrest where
"sup _ FAILi = FAILi" |
"sup FAILi _ = FAILi" |
"sup (REST a) (REST b) = REST (λx. max (a x) (b x))"
fun inf_nrest where
"inf x FAILi = x" |
"inf FAILi x = x" |
"inf (REST a) (REST b) = REST (λx. min (a x) (b x))"
lemma "min (None) (Some (1::enat)) = None" by simp
lemma "max (None) (Some (1::enat)) = Some 1" by eval
definition "Sup X ≡ if FAILi∈X then FAILi else REST (Sup {f . REST f ∈ X})"
definition "Inf X ≡ if ∃f. REST f∈X then REST (Inf {f . REST f ∈ X}) else FAILi"
definition "bot ≡ REST (Map.empty)"
definition "top ≡ FAILi"
instance
apply(intro_classes)
unfolding Sup_nrest_def Inf_nrest_def bot_nrest_def top_nrest_def
apply (case_tac x, case_tac [!] y, auto) []
apply (case_tac x, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, (case_tac [!] y)?, simp_all add: le_fun_def) []
apply (case_tac x, (case_tac [!] y)?, auto simp: le_fun_def) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto simp: le_fun_def) []
apply (case_tac x, (case_tac [!] y)?, auto simp: le_fun_def) []
apply (case_tac x, (case_tac [!] y)?, auto simp: le_fun_def) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto simp: le_fun_def) []
apply (case_tac x, auto simp add: Inf_lower ) []
apply (case_tac z, fastforce+) [] using le_Inf_iff apply fastforce
apply (case_tac x, auto simp add: Sup_upper) []
apply (case_tac z, fastforce+) [] using Sup_le_iff less_eq_nrest.simps(2) apply fastforce
apply auto []
apply (auto simp: bot_option_def) []
done
end
definition "RETURNT x ≡ REST (λe. if e=x then Some 0 else None)"
abbreviation "FAILT ≡ top::'a nrest"
abbreviation "SUCCEEDT ≡ bot::'a nrest"
abbreviation SPECT where "SPECT ≡ REST"
lemma RETURNT_alt: "RETURNT x = REST [x↦0]"
unfolding RETURNT_def by auto
lemma nrest_inequalities[simp]:
"FAILT ≠ REST X"
"FAILT ≠ SUCCEEDT"
"FAILT ≠ RETURNT x"
"SUCCEEDT ≠ FAILT"
"SUCCEEDT ≠ RETURNT x"
"REST X ≠ FAILT"
"RETURNT x ≠ FAILT"
"RETURNT x ≠ SUCCEEDT"
unfolding top_nrest_def bot_nrest_def RETURNT_def
apply (auto) by (metis option.distinct(1))+
lemma nrest_more_simps[simp]:
"SUCCEEDT = REST X ⟷ X=Map.empty"
"REST X = SUCCEEDT ⟷ X=Map.empty"
"REST X = RETURNT x ⟷ X=[x↦0]"
"REST X = REST Y ⟷ X=Y"
"RETURNT x = REST X ⟷ X=[x↦0]"
"RETURNT x = RETURNT y ⟷ x=y"
unfolding top_nrest_def bot_nrest_def RETURNT_def apply (auto split: if_splits)
by (metis option.distinct(1))
lemma nres_simp_internals:
"REST Map.empty = SUCCEEDT"
"FAILi = FAILT"
unfolding top_nrest_def bot_nrest_def by simp_all
lemma nres_order_simps[simp]:
"¬ FAILT ≤ REST M"
"REST M ≤ REST M' ⟷ (M≤M')"
by (auto simp: nres_simp_internals[symmetric])
lemma nres_top_unique[simp]:" FAILT ≤ S' ⟷ S' = FAILT"
by (rule top_unique)
lemma FAILT_cases[simp]: "(case FAILT of FAILi ⇒ P | REST x ⇒ Q x) = P"
by (auto simp: nres_simp_internals[symmetric])
lemma nrest_Sup_FAILT:
"Sup X = FAILT ⟷ FAILT ∈ X"
"FAILT = Sup X ⟷ FAILT ∈ X"
by (auto simp: nres_simp_internals Sup_nrest_def)
lemma nrest_Sup_SPECT_D: "Sup X = SPECT m ⟹ m x = Sup {f x | f. REST f ∈ X}"
unfolding Sup_nrest_def apply(auto split: if_splits) unfolding Sup_fun_def
apply(fo_rule arg_cong) by blast
declare nres_simp_internals(2)[simp]
lemma nrest_noREST_FAILT[simp]: "(∀x2. m ≠ REST x2) ⟷ m=FAILT"
apply (cases m) apply auto done
lemma no_FAILTE:
assumes "g xa ≠ FAILT"
obtains X where "g xa = REST X" using assms by (cases "g xa") auto
lemma case_prod_refine:
fixes P Q :: "'a ⇒ 'b ⇒ 'c nrest"
assumes
"⋀a b. P a b ≤ Q a b"
shows
"(case x of (a,b) ⇒ P a b) ≤ (case x of (a,b) ⇒ Q a b)"
using assms
by (simp add: split_def)
lemma case_option_refine:
fixes P Q :: "'a ⇒ 'b ⇒ 'c nrest"
assumes
"PN ≤ QN"
"⋀a. PS a ≤ QS a"
shows
"(case x of None ⇒ PN | Some a ⇒ PS a ) ≤ (case x of None ⇒ QN | Some a ⇒ QS a )"
using assms
by (auto split: option.splits)
lemma SPECT_Map_empty[simp]: "SPECT Map.empty ≤ a" apply(cases a) apply auto subgoal for x2 by(auto simp: le_fun_def)
done
lemma FAILT_SUP: "(FAILT ∈ X) ⟹ Sup X = FAILT " by (simp add: nrest_Sup_FAILT)
section "pointwise reasoning"
named_theorems refine_pw_simps
ML ‹
structure refine_pw_simps = Named_Thms
( val name = @{binding refine_pw_simps}
val description = "Refinement Framework: " ^
"Simplifier rules for pointwise reasoning" )
›
definition nofailT :: "'a nrest ⇒ bool" where "nofailT S ≡ S≠FAILT"
definition le_or_fail :: "'a nrest ⇒ 'a nrest ⇒ bool" (infix "≤⇩n" 50) where
"m ≤⇩n m' ≡ nofailT m ⟶ m ≤ m'"
lemma nofailT_simps[simp]:
"nofailT FAILT ⟷ False"
"nofailT (REST X) ⟷ True"
"nofailT (RETURNT x) ⟷ True"
"nofailT SUCCEEDT ⟷ True"
unfolding nofailT_def
by (simp_all add: RETURNT_def)
definition inresT :: "'a nrest ⇒ 'a ⇒ nat ⇒ bool" where
"inresT S x t ≡ (case S of FAILi ⇒ True | REST X ⇒ (∃t'. X x = Some t' ∧ enat t≤t'))"
lemma inresT_alt: "inresT S x t ⟷ REST ([x↦enat t]) ≤ S"
unfolding inresT_def apply(cases S)
by (auto dest!: le_funD[where x=x] simp: le_funI less_eq_option_def split: option.splits )
lemma inresT_mono: "inresT S x t ⟹ t' ≤ t ⟹ inresT S x t'"
unfolding inresT_def apply(cases S) apply auto
using enat_ord_simps(1) order_trans by blast
lemma inresT_RETURNT[simp]: "inresT (RETURNT x) y t ⟷ t = 0 ∧ y = x"
by(auto simp: inresT_def RETURNT_def enat_0_iff split: nrest.splits)
lemma inresT_FAILT[simp]: "inresT FAILT r t"
by(simp add: inresT_def)
lemma fail_inresT[refine_pw_simps]: "¬ nofailT M ⟹ inresT M x t"
unfolding nofailT_def by simp
lemma pw_inresT_Sup[refine_pw_simps]: "inresT (Sup X) r t ⟷ (∃M∈X. ∃t'≥t. inresT M r t')"
apply(rule)
subgoal
apply(cases "Sup X")
subgoal by (force simp: nrest_Sup_FAILT)
subgoal
apply(auto simp: inresT_def Sup_nrest_def split: if_splits)
apply(auto simp: SUP_eq_Some_iff split: nrest.splits)
apply(subst (asm) Sup_enat_less)
apply auto []
apply auto by blast
done
subgoal
apply(cases "Sup X")
subgoal by (auto simp: nrest_Sup_FAILT top_Sup)
subgoal
apply(auto simp: inresT_def Sup_nrest_def split: if_splits)
apply(auto simp: SUP_eq_Some_iff split: nrest.splits)
apply(subst Sup_enat_less)
apply auto []
apply auto
using dual_order.trans enat_ord_simps(1) by blast
done
done
lemma inresT_REST[simp]:
"inresT (REST X) x t ⟷ (∃t'≥t. X x = Some t')"
unfolding inresT_def
by (auto )
lemma pw_Sup_nofail[refine_pw_simps]: "nofailT (Sup X) ⟷ (∀x∈X. nofailT x)"
apply (cases "Sup X")
apply auto unfolding Sup_nrest_def apply (auto split: if_splits)
apply force unfolding nofailT_def apply(force simp add: nres_simp_internals)
done
lemma inres_simps[simp]:
"inresT FAILT = (λ_ _. True)"
"inresT SUCCEEDT = (λ_ _ . False)"
unfolding inresT_def [abs_def]
by (auto split: nrest.splits simp add: RETURNT_def)
lemma pw_le_iff:
"S ≤ S' ⟷ (nofailT S'⟶ (nofailT S ∧ (∀x t. inresT S x t ⟶ inresT S' x t)))"
apply (cases S; cases S', simp_all)
unfolding nofailT_def inresT_def apply (auto split: nrest.splits)
apply (metis le_fun_def le_some_optE order.trans)
apply(auto intro!: le_funI simp: less_eq_option_def split: option.splits)
apply (metis option.distinct(1) zero_enat_def zero_le)
by (smt Suc_ile_eq enat.exhaust linorder_not_le option.simps(1) order_refl)
lemma pw_eq_iff:
"S=S' ⟷ (nofailT S = nofailT S' ∧ (∀x t. inresT S x t ⟷ inresT S' x t))"
apply (rule iffI)
apply simp
apply (rule antisym)
apply (auto simp add: pw_le_iff)
done
lemma pw_flat_ge_iff: "flat_ge S S' ⟷
(nofailT S) ⟶ nofailT S' ∧ (∀x t. inresT S x t ⟷ inresT S' x t)"
apply (simp add: flat_ord_def)
apply(simp add: pw_eq_iff) apply safe
by (auto simp add: nofailT_def)
lemma pw_eqI:
assumes "nofailT S = nofailT S'"
assumes "⋀x t. inresT S x t ⟷ inresT S' x t"
shows "S=S'"
using assms by (simp add: pw_eq_iff)
definition "consume M t ≡ case M of
FAILi ⇒ FAILT |
REST X ⇒ REST (map_option ((+) t) o (X))"
definition "SPEC P t = REST (λv. if P v then Some (t v) else None)"
lemma consume_mono: "t≤t' ⟹ M ≤ M' ⟹ consume M t ≤ consume M' t'"
unfolding consume_def apply (auto split: nrest.splits )
unfolding le_fun_def apply auto
subgoal for m m' x apply(cases "m' x";cases "m x" ) apply auto
apply (metis less_eq_option_Some_None)
by (metis add_mono less_eq_option_Some)
done
lemma nofailT_SPEC[refine_pw_simps]: "nofailT (SPEC a b)"
unfolding SPEC_def by auto
lemma inresT_SPEC[refine_pw_simps]: "inresT (SPEC a b) = (λx t. a x ∧ b x ≥ t)"
unfolding SPEC_def inresT_REST apply(rule ext) by(auto split: if_splits)
section ‹Monad Operators›
definition bindT :: "'b nrest ⇒ ('b ⇒ 'a nrest) ⇒ 'a nrest" where
"bindT M f ≡ case M of
FAILi ⇒ FAILT |
REST X ⇒ Sup { (case f x of FAILi ⇒ FAILT
| REST m2 ⇒ REST (map_option ((+) t1) o (m2) ))
|x t1. X x = Some t1}"
lemma bindT_alt: "bindT M f = (case M of
FAILi ⇒ FAILT |
REST X ⇒ Sup { consume (f x) t1 |x t1. X x = Some t1})"
unfolding bindT_def consume_def by simp
lemma "bindT (REST X) f =
(SUP x:dom X. consume (f x) (the (X x)))"
proof -
have *: "⋀f X. { f x t |x t. X x = Some t}
= (λx. f x (the (X x))) ` (dom X)"
by force
show ?thesis by (auto simp: bindT_alt *)
qed
adhoc_overloading
Monad_Syntax.bind Sepreftime.bindT
lemma bindT_FAIL[simp]: "bindT FAILT g = FAILT"
by (auto simp: bindT_def)
lemma "bindT SUCCEEDT f = SUCCEEDT"
unfolding bindT_def by(auto split: nrest.split simp add: bot_nrest_def)
lemma pw_inresT_bindT_aux: "inresT (bindT m f) r t ⟷
(nofailT m ⟶ (∃r' t' t''. inresT m r' t' ∧ inresT (f r') r t'' ∧ t ≤ t' + t''))"
apply(rule)
subgoal
apply(cases m)
subgoal by auto
subgoal apply(auto simp: bindT_def pw_inresT_Sup split: nrest.splits)
subgoal for M x t' t1
apply(rule exI[where x=x])
apply(cases "f x") apply auto
subgoal for x2 z apply(cases t1)
apply auto
subgoal for n apply(rule exI[where x=n]) apply auto
by (smt dual_order.trans enat_ile enat_ord_simps(1) le_add2 linear order_mono_setup.refl plus_enat_simps(1))
subgoal
by (metis le_add1 zero_enat_def zero_le)
done
done
subgoal for x t' t1
apply(rule exI[where x=x]) apply auto
apply(cases t1) apply auto
subgoal for n apply(rule exI[where x=n]) apply auto
apply(rule exI[where x=t]) by auto
subgoal
by presburger
done
done
done
subgoal
apply(cases m)
subgoal by auto
subgoal for x2
apply (auto simp: bindT_def split: nrest.splits)
apply(auto simp: pw_inresT_Sup )
subgoal for r' t' t'a t''
apply(cases "f r'")
subgoal apply auto apply(force) done
subgoal for x2a
apply(rule exI[where x="REST (map_option ((+) t'a) ∘ x2a)"])
apply auto
apply(rule exI[where x=r'])
apply auto
using add_mono by fastforce
done
done
done
done
lemma pw_inresT_bindT[refine_pw_simps]: "inresT (bindT m f) r t ⟷
(nofailT m ⟶ (∃r' t' t''. inresT m r' t' ∧ inresT (f r') r t'' ∧ t = t' + t''))"
apply (auto simp: pw_inresT_bindT_aux)
by (metis (full_types) inresT_mono le_iff_add linear nat_add_left_cancel_le)
lemma pw_bindT_nofailT[refine_pw_simps]: "nofailT (bindT M f) ⟷ (nofailT M ∧ (∀x t. inresT M x t ⟶ nofailT (f x)))"
unfolding bindT_def
apply (auto elim: no_FAILTE simp: refine_pw_simps split: nrest.splits )
apply force+
by (metis enat_ile le_cases nofailT_def)
lemma [simp]: "((+) (0::enat)) = id" by auto
declare map_option.id[simp]
section ‹Monad Rules›
lemma nres_bind_left_identity[simp]: "bindT (RETURNT x) f = f x"
unfolding bindT_def RETURNT_def
by(auto split: nrest.split )
lemma nres_bind_right_identity[simp]: "bindT M RETURNT = M"
by(auto intro!: pw_eqI simp: refine_pw_simps)
lemma nres_bind_assoc[simp]: "bindT (bindT M (λx. f x)) g = bindT M (%x. bindT (f x) g)"
apply(auto intro!: pw_eqI simp: refine_pw_simps)
using inresT_mono by fastforce+
section ‹Monotonicity lemmas›
lemma bindT_mono:
"m ≤ m' ⟹ (⋀x. (∃t. inresT m x t) ⟹ nofailT m' ⟹ f x ≤ f' x)
⟹ bindT m f ≤ bindT m' f'"
apply(auto simp: pw_le_iff refine_pw_simps)
by fastforce+
lemma bindT_mono'[refine_mono]:
"m ≤ m' ⟹ (⋀x. f x ≤ f' x)
⟹ bindT m f ≤ bindT m' f'"
apply(rule bindT_mono) by auto
lemma bindT_flat_mono[refine_mono]:
"⟦ flat_ge M M'; ⋀x. flat_ge (f x) (f' x) ⟧ ⟹ flat_ge (bindT M f) (bindT M' f')"
apply (auto simp: refine_pw_simps pw_flat_ge_iff) []
by fastforce+
subsection ‹ Derived Program Constructs ›
subsubsection ‹Assertion›
definition "iASSERT ret Φ ≡ if Φ then ret () else top"
definition ASSERT where "ASSERT ≡ iASSERT RETURNT"
lemma ASSERT_True[simp]: "ASSERT True = RETURNT ()"
by (auto simp: ASSERT_def iASSERT_def)
lemma ASSERT_False[simp]: "ASSERT False = FAILT"
by (auto simp: ASSERT_def iASSERT_def)
lemma bind_ASSERT_eq_if: "do { ASSERT Φ; m } = (if Φ then m else FAILT)"
unfolding ASSERT_def iASSERT_def by simp
lemma pw_ASSERT[refine_pw_simps]:
"nofailT (ASSERT Φ) ⟷ Φ"
"inresT (ASSERT Φ) x 0"
by (cases Φ, simp_all)+
lemma ASSERT_refine: "(Q ⟹ P) ⟹ ASSERT P ≤ ASSERT Q"
by(auto simp: pw_le_iff refine_pw_simps)
lemma ASSERT_leI: "Φ ⟹ (Φ ⟹ M ≤ M') ⟹ ASSERT Φ ⤜ (λ_. M) ≤ M'"
by(auto simp: pw_le_iff refine_pw_simps)
lemma le_ASSERTI: "(Φ ⟹ M ≤ M') ⟹ M ≤ ASSERT Φ ⤜ (λ_. M')"
by(auto simp: pw_le_iff refine_pw_simps)
lemma inresT_ASSERT: "inresT (ASSERT Q ⤜ (λ_. M)) x ta = (Q ⟶ inresT M x ta)"
unfolding ASSERT_def iASSERT_def by auto
lemma nofailT_ASSERT_bind: "nofailT (ASSERT P ⤜ (λ_. M)) ⟷ (P ∧ nofailT M)"
by(auto simp: pw_bindT_nofailT pw_ASSERT)
subsection ‹SELECT›
definition emb' where "⋀Q T. emb' Q (T::'a ⇒ enat) = (λx. if Q x then Some (T x) else None)"
abbreviation "emb Q t ≡ emb' Q (λ_. t)"
lemma emb_eq_Some_conv: "⋀T. emb' Q T x = Some t' ⟷ (t'=T x ∧ Q x)"
by (auto simp: emb'_def)
lemma emb_le_Some_conv: "⋀T. Some t' ≤ emb' Q T x ⟷ ( t'≤T x ∧ Q x)"
by (auto simp: emb'_def)
lemma SPEC_REST_emb'_conv: "SPEC P t = REST (emb' P t)"
unfolding SPEC_def emb'_def by auto
text ‹Select some value with given property, or ‹None› if there is none.›
definition SELECT :: "('a ⇒ bool) ⇒ enat ⇒ 'a option nrest"
where "SELECT P tf ≡ if ∃x. P x then REST (emb (λr. case r of Some p ⇒ P p | None ⇒ False) tf)
else REST [None ↦ tf]"
lemma inresT_SELECT_Some: "inresT (SELECT Q tt) (Some x) t' ⟷ (Q x ∧ (t' ≤ tt))"
by(auto simp: inresT_def SELECT_def emb'_def)
lemma inresT_SELECT_None: "inresT (SELECT Q tt) None t' ⟷ (¬(∃x. Q x) ∧ (t' ≤ tt))"
by(auto simp: inresT_def SELECT_def emb'_def)
lemma inresT_SELECT[refine_pw_simps]:
"inresT (SELECT Q tt) x t' ⟷ ((case x of None ⇒ ¬(∃x. Q x) | Some x ⇒ Q x) ∧ (t' ≤ tt))"
by(auto simp: inresT_def SELECT_def emb'_def)
lemma nofailT_SELECT[refine_pw_simps]: "nofailT (SELECT Q tt)"
by(auto simp: nofailT_def SELECT_def)
lemma s1: "SELECT P T ≤ (SELECT P T') ⟷ T ≤ T'"
apply(cases "∃x. P x")
apply(auto simp: pw_le_iff refine_pw_simps split: option.splits)
subgoal
by (metis (full_types) enat_ord_code(3) enat_ord_simps(1) lessI not_infinity_eq not_le order_mono_setup.refl)
subgoal
by (metis (full_types) enat_ord_code(3) enat_ord_simps(1) lessI not_enat_eq not_le order_mono_setup.refl)
done
lemma s2: "SELECT P T ≤ (SELECT P' T) ⟷ (
(Ex P' ⟶ Ex P) ∧ (∀x. P x ⟶ P' x)) "
apply(auto simp: pw_le_iff refine_pw_simps split: option.splits)
subgoal
by (metis enat_ile linear)
subgoal
by (metis enat_ile linear)
done
lemma SELECT_refine:
assumes "⋀x'. P' x' ⟹ ∃x. P x"
assumes "⋀x. P x ⟹ P' x"
assumes "T ≤ T'"
shows "SELECT P T ≤ (SELECT P' T')"
proof -
have "SELECT P T ≤ SELECT P T'"
using s1 assms(3) by auto
also have "… ≤ SELECT P' T'"
unfolding s2 apply safe
using assms(1,2) by auto
finally show ?thesis .
qed
section ‹RECT›
definition "mono2 B ≡ flatf_mono_ge B ∧ mono B"
lemma trimonoD_flatf_ge: "mono2 B ⟹ flatf_mono_ge B"
unfolding mono2_def by auto
lemma trimonoD_mono: "mono2 B ⟹ mono B"
unfolding mono2_def by auto
definition "RECT B x =
(if mono2 B then (gfp B x) else (top::'a::complete_lattice))"
thm gfp_eq_flatf_gfp
lemma RECT_flat_gfp_def: "RECT B x =
(if mono2 B then (flatf_gfp B x) else (top::'a::complete_lattice))"
unfolding RECT_def
by (auto simp: gfp_eq_flatf_gfp[OF trimonoD_flatf_ge trimonoD_mono])
lemma RECT_unfold: "⟦mono2 B⟧ ⟹ RECT B = B (RECT B)"
unfolding RECT_def [abs_def]
by (auto dest: trimonoD_mono simp: gfp_unfold[ symmetric])
definition whileT :: "('a ⇒ bool) ⇒ ('a ⇒ 'a nrest) ⇒ 'a ⇒ 'a nrest" where
"whileT b c = RECT (λwhileT s. (if b s then bindT (c s) whileT else RETURNT s))"
definition whileIET :: "('a ⇒ bool) ⇒ ('a ⇒ nat) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ 'a nrest) ⇒ 'a ⇒ 'a nrest" where
"⋀E c. whileIET I E b c = whileT b c"
definition whileTI :: "('a ⇒ enat option) ⇒ ( ('a×'a) set) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ 'a nrest) ⇒ 'a ⇒ 'a nrest" where
"whileTI I R b c s = whileT b c s"
lemma trimonoI[refine_mono]:
"⟦flatf_mono_ge B; mono B⟧ ⟹ mono2 B"
unfolding mono2_def by auto
lemma [refine_mono]: "(⋀f g x. (⋀x. f x ≤ g x) ⟹ B f x ≤ B g x) ⟹ mono B"
apply(rule monoI) apply(rule le_funI)
by (simp add: le_funD)
thm refine_mono
lemma whileT_unfold: "whileT b c = (λs. (if b s then bindT (c s) (whileT b c) else RETURNT s))"
unfolding whileT_def
apply(rule RECT_unfold)
by ( refine_mono)
lemma RECT_mono[refine_mono]:
assumes [simp]: "mono2 B'"
assumes LE: "⋀F x. (B' F x) ≤ (B F x) "
shows " (RECT B' x) ≤ (RECT B x)"
unfolding RECT_def
apply clarsimp
by (meson LE gfp_mono le_fun_def)
lemma whileT_mono:
assumes "⋀x. b x ⟹ c x ≤ c' x"
shows " (whileT b c x) ≤ (whileT b c' x)"
unfolding whileT_def apply(rule RECT_mono)
subgoal by(refine_mono)
apply auto apply(rule bindT_mono) using assms by auto
find_theorems RECT
lemma wf_fp_induct:
assumes fp: "⋀x. f x = B (f) x"
assumes wf: "wf R"
assumes "⋀x D. ⟦⋀y. (y,x)∈R ⟹ P y (D y)⟧ ⟹ P x (B D x)"
shows "P x (f x)"
using wf
apply induction
apply (subst fp)
apply fact
done
thm wf_fp_induct[where f="RECT B" and B=B] RECT_unfold
lemma RECT_wf_induct_aux:
assumes wf: "wf R"
assumes mono: "mono2 B"
assumes "(⋀x D. (⋀y. (y, x) ∈ R ⟹ P y (D y)) ⟹ P x (B D x))"
shows "P x (RECT B x)"
using wf_fp_induct[where f="RECT B" and B=B] RECT_unfold assms
by metis
theorem RECT_wf_induct[consumes 1]:
assumes "RECT B x = r"
assumes "wf R"
and "mono2 B"
and "⋀x D r. (⋀y r. (y, x) ∈ R ⟹ D y = r ⟹ P y r) ⟹ B D x = r ⟹ P x r"
shows "P x r"
using RECT_wf_induct_aux[where P = "λx fx. P x fx"] assms by metis
definition "monadic_WHILEIT I b f s ≡ do {
RECT (λD s. do {
ASSERT (I s);
bv ← b s;
if bv then do {
s ← f s;
D s
} else do {RETURNT s}
}) s
}"
section ‹Generalized Weakest Precondition›
subsection "mm"
definition mm :: "( 'a ⇒ enat option) ⇒ ( 'a ⇒ enat option) ⇒ ( 'a ⇒ enat option)" where
"mm R m = (λx. (case m x of None ⇒ Some ∞
| Some mt ⇒
(case R x of None ⇒ None | Some rt ⇒ (if rt < mt then None else Some (rt - mt)))))"
lemma mm_mono: "Q1 x ≤ Q2 x ⟹ mm Q1 M x ≤ mm Q2 M x"
unfolding mm_def apply(cases "M x") apply (auto split: option.splits)
using le_some_optE apply blast apply(rule helper) by auto
lemma mm_antimono: "M1 x ≥ M2 x ⟹ mm Q M1 x ≤ mm Q M2 x"
unfolding mm_def apply (auto split: option.splits)
apply(rule helper2) by auto
lemma mm_continous: "mm (λx. Inf {u. ∃y. u = f y x}) m x = Inf {u. ∃y. u = mm (f y) m x}"
apply(rule antisym)
subgoal apply(rule Inf_greatest) apply clarsimp
proof (cases "Inf {u. ∃y. u = f y x}")
case None
have f: "m x ≠ None ⟹ mm (λx. Inf {u. ∃y. u = f y x}) m x = None" unfolding mm_def None apply(cases "m x") by (auto )
then show "⋀y. mm (λx. Inf {u. ∃y. u = f y x}) m x ≤ mm (f y) m x"
apply(cases "m x") apply(auto simp: f) unfolding mm_def by auto
next
case (Some l)
then show "⋀y. mm (λx. Inf {u. ∃y. u = f y x}) m x ≤ mm (f y) m x"
apply(cases "m x") subgoal unfolding mm_def by auto
proof -
fix y a assume I: "Inf {u. ∃y. u = f y x} = Some l" " m x = Some a"
from I have i: "⋀y. f y x ≥ Some l"
by (metis (mono_tags, lifting) Inf_lower mem_Collect_eq)
show "mm (λx. Inf {u. ∃y. u = f y x}) m x ≤ mm (f y) m x"
apply(rule mm_mono) unfolding I apply(rule i) .
qed
qed
subgoal apply(rule Inf_lower) apply clarsimp
proof -
have "∃y. Inf {u. ∃y. u = f y x} = f y x"
unfolding Inf_option_def apply auto unfolding Inf_enat_def apply auto
apply (metis (mono_tags) empty_iff in_these_eq mem_Collect_eq option.exhaust)
by (smt LeastI in_these_eq mem_Collect_eq)
then obtain y where z: "Inf {u. ∃y. u = f y x} = f y x" by blast
show "∃y. mm (λx. Inf {u. ∃y. u = f y x}) m x = mm (f y) m x"
apply(rule exI[where x=y]) unfolding mm_def z ..
qed
done
definition mm2 :: "( enat option) ⇒ ( enat option) ⇒ ( enat option)" where
"mm2 r m = (case m of None ⇒ Some ∞
| Some mt ⇒
(case r of None ⇒ None | Some rt ⇒ (if rt < mt then None else Some (rt - mt))))"
lemma mm_alt: "mm R m x = mm2 (R x) (m x)" unfolding mm_def mm2_def ..
lemma mm2_None[simp]: "mm2 q None = Some ∞" unfolding mm2_def by auto
lemma mm2_Some0[simp]: "mm2 q (Some 0) = q" unfolding mm2_def by (auto split: option.splits)
lemma mm2_antimono: "x ≤ y ⟹ mm2 q x ≥ mm2 q y"
unfolding mm2_def apply (auto split: option.splits)
using helper2 by blast
lemma mm2_contiuous2: "∀x∈X. t ≤ mm2 q x ⟹ t ≤ mm2 q (Sup X)"
unfolding mm2_def apply(auto simp: everywhereNone bot_option_def less_eq_option_None_is_None' split: option.splits if_splits)
subgoal by (metis (no_types, lifting) Sup_option_def in_these_eq less_Sup_iff option.distinct(1) option.sel)
subgoal for tx tq by(cases tq; cases tx; fastforce dest!: Sup_finite_enat)
done
lemma fl: "(a::enat) - b = ∞ ⟹ a = ∞"
apply(cases b; cases a) by auto
lemma mm_inf1: "mm R m x = Some ∞ ⟹ m x = None ∨ R x = Some ∞"
apply(auto simp: mm_def split: option.splits if_splits) using fl by metis
lemma mm_inf2: "m x = None ⟹ mm R m x = Some ∞"
by(auto simp: mm_def split: option.splits if_splits)
lemma mm_inf3: " R x = Some ∞ ⟹ mm R m x = Some ∞"
by(auto simp: mm_def split: option.splits if_splits)
lemma mm_inf: "mm R m x = Some ∞ ⟷ m x = None ∨ R x = Some ∞"
using mm_inf1 mm_inf2 mm_inf3 by metis
lemma InfQ_E: "Inf Q = Some t ⟹ None ∉ Q"
unfolding Inf_option_def by auto
lemma InfQ_iff: "(∃t'≥enat t. Inf Q = Some t') ⟷ None ∉ Q ∧ Inf (Option.these Q) ≥ t"
unfolding Inf_option_def
by auto
lemma mm2_fst_None[simp]: "mm2 None q = (case q of None ⇒ Some ∞ | _ ⇒ None)"
apply (cases q) apply (auto simp: mm2_def) done
lemma mm2_auxXX1: "Some t ≤ mm2 (Q x) (Some t') ⟹ Some t' ≤ mm2 (Q x) (Some t)"
apply (auto simp: mm2_def split: option.splits if_splits)
apply (metis helper2 idiff_0_right leD less_le_trans zero_le)
apply (auto simp: less_eq_enat_def split: enat.splits)
done
subsection "mii"
definition mii :: "('a ⇒ enat option) ⇒ 'a nrest ⇒ 'a ⇒ enat option" where
"mii Qf M x = (case M of FAILi ⇒ None
| REST Mf ⇒ (mm Qf Mf) x)"
lemma mii_alt: "mii Qf M x = (case M of FAILi ⇒ None
| REST Mf ⇒ (mm2 (Qf x) (Mf x)) )"
unfolding mii_def mm_alt ..
lemma mii_continuous: "mii (λx. Inf {f y x|y. True}) m x = Inf {mii (%x. f y x) m x|y. True}"
unfolding mii_def apply(cases m) subgoal apply auto done
subgoal apply auto using mm_continous by metis
done
lemma mii_continuous2: "(mii Q (Sup {F x t1 |x t1. P x t1}) x ≥ t) = (∀y t1. P y t1 ⟶ mii Q (F y t1) x ≥ t)"
unfolding mii_alt apply auto apply (auto simp: nrest_Sup_FAILT less_eq_option_None_is_None' split: nrest.splits)
subgoal by (smt nrest_Sup_FAILT(2) mem_Collect_eq nres_order_simps(1) top_greatest)
subgoal for y t1 x2 x2a
apply(drule nrest_Sup_SPECT_D[where x=x])
apply(rule order.trans[where b="mm2 (Q x) (x2 x)"]) apply simp
apply(rule mm2_antimono) by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq)
subgoal
apply(drule nrest_Sup_SPECT_D[where x=x])
by (auto intro: mm2_contiuous2)
done
lemma mii_inf: "mii Qf M x = Some ∞ ⟷ (∃Mf. M = SPECT Mf ∧ (Mf x = None ∨ Qf x = Some ∞))"
by (auto simp: mii_def mm_inf split: nrest.split )
lemma miiFailt: "mii Q FAILT x = None" unfolding mii_def by auto
subsection "lst - latest starting time"
definition lst :: "'a nrest ⇒ ('a ⇒ enat option) ⇒ enat option"
where "lst M Qf = Inf { mii Qf M x | x. True}"
lemma T_alt_: "lst M Qf = Inf ( (mii Qf M) ` UNIV )"
unfolding lst_def
by (simp add: full_SetCompr_eq)
lemma T_pw: "lst M Q ≥ t ⟷ (∀x. mii Q M x ≥ t)"
unfolding lst_def mii_def apply(cases M) apply auto
unfolding Inf_option_def apply (auto split: if_splits)
using less_eq_option_None_is_None less_option_None not_less apply blast
apply (smt Inf_lower Inf_option_def dual_order.trans mem_Collect_eq)
apply metis
by (smt in_these_eq le_Inf_iff le_cases le_some_optE less_eq_option_Some mem_Collect_eq)
lemma T_specifies_I: "lst m Q ≥ Some 0 ⟹ (m ≤ SPECT Q)"
unfolding T_pw apply (cases m) apply (auto simp: miiFailt le_fun_def mii_alt mm2_def split: option.splits)
subgoal for M x apply(cases "Q x"; cases "M x") apply (auto split: if_splits)
apply force+ done
done
lemma T_specifies_rev: "(m ≤ SPECT Q) ⟹ lst m Q ≥ Some 0"
unfolding T_pw apply (cases m)
subgoal by auto
apply (auto simp: miiFailt le_fun_def mii_alt mm2_def split: option.splits)
subgoal for M x t apply(cases "Q x"; cases "M x") apply (auto split: if_splits)
by (metis less_eq_option_Some_None)
subgoal by (metis leD less_option_Some)
done
lemma T_specifies: "lst m Q ≥ Some 0 = (m ≤ SPECT Q)"
using T_specifies_I T_specifies_rev by metis
lemma pointwise_lesseq:
fixes x :: "'a::order"
shows "(∀t. x ≥ t ⟶ x' ≥ t) ⟹ x ≤ x'"
by simp
subsection "pointwise reasoning about lst via nres3"
definition nres3 where "nres3 Q M x t ⟷ mii Q M x ≥ t"
lemma pw_T_le:
assumes "⋀t. (∀x. nres3 Q M x t) ⟹ (∀x. nres3 Q' M' x t)"
shows "lst M Q ≤ lst M' Q'"
apply(rule pointwise_lesseq)
using assms unfolding T_pw nres3_def by metis
lemma assumes "⋀t. (∀x. nres3 Q M x t) = (∀x. nres3 Q' M' x t)"
shows pw_T_eq_iff: "lst M Q = lst M' Q'"
apply (rule antisym)
apply(rule pw_T_le) using assms apply metis
apply(rule pw_T_le) using assms apply metis done
lemma assumes "⋀t. (∀x. nres3 Q M x t) ⟹ (∀x. nres3 Q' M' x t)"
"⋀t. (∀x. nres3 Q' M' x t) ⟹ (∀x. nres3 Q M x t)"
shows pw_T_eqI: "lst M Q = lst M' Q'"
apply (rule antisym)
apply(rule pw_T_le) apply fact
apply(rule pw_T_le) apply fact done
lemma lem: "∀t1. M y = Some t1 ⟶ t ≤ mii Q (SPECT (map_option ((+) t1) ∘ x2)) x ⟹ f y = SPECT x2 ⟹ t ≤ mii (λy. mii Q (f y) x) (SPECT M) y"
unfolding mii_def apply (auto split: nrest.splits)
unfolding mm_def apply (auto split: nrest.splits)
apply(cases "M y")
subgoal by (auto simp: top_option_def[symmetric] top_enat_def[symmetric])
apply simp apply(cases "x2 x") subgoal by simp
apply simp apply(cases "Q x") subgoal by simp
apply simp apply(auto split: if_splits)
subgoal for a b c apply(cases a; cases b; cases c) by auto
subgoal for a b c apply(cases a; cases b; cases c) by auto
subgoal for a b c apply(cases a; cases b; cases c) by auto
subgoal for a b c apply(cases a; cases b; cases c) by (auto simp add: add.commute)
done
lemma lem2: "t ≤ mii (λy. mii Q (f y) x) (SPECT M) y ⟹ M y = Some t1 ⟹ f y = SPECT fF ⟹ t ≤ mii Q (SPECT (map_option ((+) t1) ∘ fF)) x"
apply (simp add: mii_def mm_def) apply(cases "fF x") apply auto
apply(cases "Q x") apply (auto split: if_splits)
subgoal using less_eq_option_None_is_None less_option_None not_less by blast
subgoal using less_eq_option_None_is_None less_option_None not_less by blast
subgoal for a b apply(cases a; cases b; cases t) apply auto
by (metis add_right_mono leD le_add_diff_inverse2 le_less_linear plus_enat_simps(1))
subgoal for a b apply(cases a; cases b; cases t) apply auto
by (smt add.commute add_diff_cancel_left enat_ile idiff_enat_enat le_add_diff_inverse le_less_linear plus_enat_simps(1))
done
lemma fixes m :: "'b nrest"
shows mii_bindT: "(t ≤ mii Q (bindT m f) x) ⟷ (∀y. t ≤ mii (λy. mii Q (f y) x) m y)"
proof -
{ fix M
assume mM: "m = SPECT M"
let ?P = "%x t1. M x = Some t1"
let ?F = "%x t1. case f x of FAILi ⇒ FAILT | REST m2 ⇒ SPECT (map_option ((+) t1) ∘ m2)"
let ?Sup = "(Sup {?F x t1 |x t1. ?P x t1})"
{ fix y
have "(∀t1. ?P y t1 ⟶ mii Q (?F y t1) x ≥ t)
= (t ≤ mii (λy. mii Q (f y) x) m y)"
apply safe
subgoal apply(cases "f y")
subgoal apply (auto simp: miiFailt)
apply (metis mM mii_inf top_enat_def top_greatest top_option_def)
using less_eq_option_None_is_None less_option_None not_less by blast
subgoal apply (simp add: mM) using lem by metis
done
subgoal for t1 apply(cases "f y")
subgoal by (auto simp: miiFailt mm_def mM mii_def)
subgoal for fF apply(simp add: mM)
using lem2 by metis
done
done
} note blub=this
from mM have "mii Q (bindT m f) x = mii Q ?Sup x" by (auto simp: bindT_def)
then have "(t ≤ mii Q (bindT m f) x) = (t ≤ mii Q ?Sup x)" by simp
also have "… = (∀y t1. ?P y t1 ⟶ mii Q (?F y t1) x ≥ t)" by (rule mii_continuous2)
also have "… = (∀y. t ≤ mii (λy. mii Q (f y) x) m y)" by(simp only: blub)
finally have ?thesis .
} note bl=this
show ?thesis apply(cases m)
subgoal by (simp add: mii_def)
subgoal apply(rule bl) .
done
qed
lemma nres3_bindT: "(∀x. nres3 Q (bindT m f) x t) = (∀y. nres3 (λy. lst (f y) Q) m y t)"
proof -
have t: "⋀f and t::enat option. (∀y. t ≤ f y) ⟷ (t≤Inf {f y|y. True})"
using le_Inf_iff by fastforce
have "(∀x. nres3 Q (bindT m f) x t) = (∀x. t ≤ mii Q (bindT m f) x)" unfolding nres3_def by auto
also have "… = (∀x. (∀y. t ≤ mii (λy. mii Q (f y) x) m y))" by(simp only: mii_bindT)
also have "… = (∀y. (∀x. t ≤ mii (λy. mii Q (f y) x) m y))" by blast
also have "… = (∀y. t ≤ mii (λy. Inf {mii Q (f y) x|x. True}) m y)"
apply(simp only: mii_continuous) using t by fast
also have "… = (∀y. t ≤ mii (λy. lst (f y) Q) m y)" unfolding lst_def by auto
also have "… = (∀y. nres3 (λy. lst (f y) Q) m y t)" unfolding nres3_def by auto
finally show ?thesis .
have "(∀y. t ≤ mii (λy. lst (f y) Q) m y) = (t ≤ Inf{ mii (λy. lst (f y) Q) m y|y. True})" using t by metis
qed
subsection "rules for lst"
lemma T_bindT: "lst (bindT M f) Q = lst M (λy. lst (f y) Q)"
by (rule pw_T_eq_iff, rule nres3_bindT)
lemma T_REST: "lst (REST [x↦t]) Q = mm2 (Q x) (Some t)"
proof-
have *: "Inf {uu. ∃xa. (xa = x ⟶ uu= v) ∧ (xa ≠ x ⟶ uu = Some ∞)} = v" (is "Inf ?S = v") for v :: "enat option"
proof -
have "?S ∈ { {v} ∪ {Some ∞}, {v} }" by auto
then show ?thesis apply simp apply safe by (simp_all add: top_enat_def[symmetric] top_option_def[symmetric] )
qed
then show ?thesis
unfolding lst_def mii_alt by auto
qed
lemma T_RETURNT: "lst (RETURNT x) Q = Q x"
unfolding RETURNT_alt apply(rule trans) apply(rule T_REST) by simp
lemma T_SELECT:
assumes
"∀x. ¬ P x ⟹ Some tt ≤ lst (SPECT [None ↦ tf]) Q"
and p: "(⋀x. P x ⟹ Some tt ≤ lst (SPECT [Some x ↦ tf]) Q)"
shows "Some tt ≤ lst (SELECT P tf) Q"
proof(cases "∃x. P x")
case True
from p[unfolded T_pw mii_alt] have
p': "⋀y x. P y ⟹ Some tt ≤ mm2 (Q x)([Some y ↦ tf] x)"
by auto
from True
show ?thesis
unfolding SELECT_def apply (auto simp: emb'_def split: if_splits)
apply(auto simp: T_pw) subgoal for x xa apply(cases xa)
apply (simp add: mii_alt)
apply (simp add: mii_alt) apply safe subgoal for a
using p'[of a xa] by auto
done
done
next
case False
then show ?thesis
unfolding SELECT_def apply (auto simp: emb'_def split: if_splits) using assms by auto
qed
section ‹consequence rules›
lemma aux1: "Some t ≤ mm2 Q (Some t') ⟷ Some (t+t') ≤ Q"
apply (auto simp: mm2_def split: option.splits)
subgoal for t''
by (cases t; cases t'; cases t''; auto)
subgoal for t''
by (cases t; cases t'; cases t''; auto)
subgoal for t''
by (cases t; cases t'; cases t''; auto)
done
lemma aux1a: "(∀x t''. Q' x = Some t'' ⟶ (Q x) ≥ Some (t + t''))
= (∀x. mm2 (Q x) (Q' x) ≥ Some t) "
apply (auto simp: )
subgoal for x apply(cases "Q' x") apply simp
by(simp add: aux1)
subgoal for x t'' using aux1 by metis
done
lemma T_conseq4:
assumes
"lst f Q' ≥ Some t'"
"⋀x t'' M. Q' x = Some t'' ⟹ (Q x) ≥ Some ((t - t') + t'')"
shows "lst f Q ≥ Some t"
proof -
{
fix x
from assms(1)[unfolded T_pw] have i: "Some t' ≤ mii Q' f x" by auto
from assms(2) have ii: "⋀t''. Q' x = Some t'' ⟹ (Q x) ≥ Some ((t - t') + t'')" by auto
from i ii have "Some t ≤ mii Q f x"
unfolding mii_alt apply(auto split: nrest.splits)
subgoal for x2 apply(cases "x2 x") apply simp
apply(simp add: aux1)
apply(cases "Q' x") apply simp
apply auto
apply(cases "Q x") apply auto
subgoal for a b c apply(cases t; cases t'; cases a; cases b; cases c) apply auto
using le_add2 by force
done
done
}
thus ?thesis
unfolding T_pw ..
qed
lemma T_conseq6:
assumes
"lst f Q' ≥ Some t"
"⋀x t'' M. f = SPECT M ⟹ M x ≠ None ⟹ Q' x = Some t'' ⟹ (Q x) ≥ Some ( t'')"
shows "lst f Q ≥ Some t"
proof -
{
fix x
from assms(1)[unfolded T_pw] have i: "Some t ≤ mii Q' f x" by auto
from assms(2) have ii: "⋀t'' M. f = SPECT M ⟹ M x ≠ None ⟹ Q' x = Some t'' ⟹ (Q x) ≥ Some ( t'')" by auto
from i ii have "Some t ≤ mii Q f x"
unfolding mii_alt apply(auto split: nrest.splits)
subgoal for x2 apply(cases "x2 x") apply simp
apply(simp add: aux1)
apply(cases "Q' x") apply simp
apply auto
apply(cases "Q x") apply auto
subgoal for a b c apply(cases t; cases a; cases b; cases c) apply auto
using le_add2 by force
done
done
}
thus ?thesis
unfolding T_pw ..
qed
lemma T_conseq6':
assumes
"lst f Q' ≥ Some t"
"⋀x t'' M. f = SPECT M ⟹ M x ≠ None ⟹ (Q x) ≥ Q' x"
shows "lst f Q ≥ Some t"
apply(rule T_conseq6) apply fact
by (auto dest: assms(2))
lemma T_conseq5:
assumes
"lst f Q' ≥ Some t'"
"⋀x t'' M. f = SPECT M ⟹ M x ≠ None ⟹ Q' x = Some t'' ⟹ (Q x) ≥ Some ((t - t') + t'')"
shows "lst f Q ≥ Some t"
proof -
{
fix x
from assms(1)[unfolded T_pw] have i: "Some t' ≤ mii Q' f x" by auto
from assms(2) have ii: "⋀t'' M. f = SPECT M ⟹ M x ≠ None ⟹ Q' x = Some t'' ⟹ (Q x) ≥ Some ((t - t') + t'')" by auto
from i ii have "Some t ≤ mii Q f x"
unfolding mii_alt apply(auto split: nrest.splits)
subgoal for x2 apply(cases "x2 x") apply simp
apply(simp add: aux1)
apply(cases "Q' x") apply simp
apply auto
apply(cases "Q x") apply auto
subgoal for a b c apply(cases t; cases t'; cases a; cases b; cases c) apply auto
using le_add2 by force
done
done
}
thus ?thesis
unfolding T_pw ..
qed
lemma T_conseq3:
assumes
"lst f Q' ≥ Some t'"
"⋀x. mm2 (Q x) (Q' x) ≥ Some (t - t')"
shows "lst f Q ≥ Some t"
using assms T_conseq4 aux1a by metis
section "Experimental Hoare reasoning"
named_theorems vcg_rules
method vcg uses rls = ((rule rls vcg_rules[THEN T_conseq4] | clarsimp simp: emb_eq_Some_conv emb_le_Some_conv T_bindT T_RETURNT)+)
experiment
begin
definition P where "P f g = bindT f (λx. bindT g (λy. RETURNT (x+(y::nat))))"
lemma assumes
f_spec[vcg_rules]: "lst f ( emb' (λx. x > 2) (enat o (( *) 2)) ) ≥ Some 0"
and
g_spec[vcg_rules]: "lst g ( emb' (λx. x > 2) (enat) ) ≥ Some 0"
shows "lst (P f g) ( emb' (λx. x > 5) (enat o ( *) 3) ) ≥ Some 0"
proof -
have ?thesis
unfolding P_def
apply vcg
done
have ?thesis
unfolding P_def
apply(simp add: T_bindT )
apply(simp add: T_RETURNT)
apply(rule T_conseq4[OF f_spec])
apply(clarsimp simp: emb_eq_Some_conv)
apply(rule T_conseq4[OF g_spec])
apply (clarsimp simp: emb_eq_Some_conv emb_le_Some_conv)
done
thus ?thesis .
qed
end
section ‹VCG›
named_theorems vcg_simp_rules
lemmas [vcg_simp_rules] = T_RETURNT
lemma TbindT_I: "Some t ≤ lst M (λy. lst (f y) Q) ⟹ Some t ≤ lst (M ⤜ f) Q"
by(simp add: T_bindT)
method vcg' uses rls = ((rule rls TbindT_I vcg_rules[THEN T_conseq6] | clarsimp split: if_splits simp: vcg_simp_rules)+)
lemma mm2_refl: "A < ∞ ⟹ mm2 (Some A) (Some A) = Some 0"
unfolding mm2_def by auto
definition mm3 where
"mm3 t A = (case A of None ⇒ None | Some t' ⇒ if t'≤t then Some (enat (t-t')) else None)"
lemma [simp]: "mm3 t0 (Some t0) = Some 0" by (auto simp: mm3_def zero_enat_def)
lemma mm3_Some_conv: "(mm3 t0 A = Some t) = (∃t'. A = Some t' ∧ t0 ≥ t' ∧ t=t0-t')"
unfolding mm3_def by(auto split: option.splits)
lemma [simp]: "mm3 t0 None = None" unfolding mm3_def by auto
lemma T_FAILT[simp]: "lst FAILT Q = None"
unfolding lst_def mii_alt by simp
definition "progress m ≡ ∀s' M. m = SPECT M ⟶ M s' ≠ None ⟶ M s' > Some 0"
lemma progressD: "progress m ⟹ m=SPECT M ⟹ M s' ≠ None ⟹ M s' > Some 0"
by (auto simp: progress_def)
lemma [simp]: "progress FAILT" by(auto simp: progress_def)
subsection ‹Progress rules›
named_theorems progress_rules
lemma progress_SELECT_iff: "progress (SELECT P t) ⟷ t > 0"
unfolding progress_def SELECT_def emb'_def by (auto split: option.splits)
lemmas [progress_rules] = progress_SELECT_iff[THEN iffD2]
lemma progress_REST_iff: "progress (REST [x ↦ t]) ⟷ t>0"
by (auto simp: progress_def)
lemmas [progress_rules] = progress_REST_iff[THEN iffD2]
lemma progress_ASSERT_bind[progress_rules]: "⟦Φ ⟹ progress (f ()) ⟧ ⟹ progress (ASSERT Φ⤜f)"
apply (cases Φ)
apply (auto simp: progress_def)
done
lemma progress_SPECT_emb[progress_rules]: "t > 0 ⟹ progress (SPECT (emb P t))" by(auto simp: progress_def emb'_def)
lemma Sup_Some: "Sup (S::enat option set) = Some e ⟹ ∃x∈S. (∃i. x = Some i)"
unfolding Sup_option_def by (auto split: if_splits)
lemma progress_bind[progress_rules]: assumes "progress m ∨ (∀x. progress (f x))"
shows "progress (m⤜f)"
proof (cases m)
case FAILi
then show ?thesis by (auto simp: progress_def)
next
case (REST x2)
then show ?thesis unfolding bindT_def progress_def apply safe
proof (goal_cases)
case (1 s' M y)
let ?P = "λfa. ∃x. f x ≠ FAILT ∧
(∃t1. ∀x2a. f x = SPECT x2a ⟶ fa = map_option ((+) t1) ∘ x2a ∧ x2 x = Some t1)"
from 1 have A: "Sup {fa s' |fa. ?P fa} = Some y" apply simp
apply(drule nrest_Sup_SPECT_D[where x=s']) by (auto split: nrest.splits)
from Sup_Some[OF this] obtain fa i where P: "?P fa" and 3: "fa s' = Some i" by blast
then obtain x t1 x2a where a3: "f x = SPECT x2a"
and "∀x2a. f x = SPECT x2a ⟶ fa = map_option ((+) t1) ∘ x2a" and a2: "x2 x = Some t1"
by fastforce
then have a1: " fa = map_option ((+) t1) ∘ x2a" by auto
have "progress m ⟹ t1 > 0" apply(drule progressD)
using 1(1) a2 a1 a3 by auto
moreover
have "progress (f x) ⟹ x2a s' > Some 0"
using a1 1(1) a2 3 by (auto dest!: progressD[OF _ a3])
ultimately
have " t1 > 0 ∨ x2a s' > Some 0" using assms by auto
then have "Some 0 < fa s'" using a1 3 by auto
also have "… ≤ Sup {fa s'|fa. ?P fa}"
apply(rule Sup_upper) using P by blast
also have "… = M s'" using A 1(3) by simp
finally show ?case .
qed
qed
lemma mm2SomeleSome_conv: "mm2 (Qf) (Some t) ≥ Some 0 ⟷ Qf ≥ Some t"
unfolding mm2_def by (auto split: option.split)
section "rules for whileT"
lemma
assumes "whileT b c s = r"
assumes IS[vcg_rules]: "⋀s t'. I s = Some t' ⟹ b s
⟹ lst (c s) (λs'. if (s',s)∈R then I s' else None) ≥ Some t'"
assumes "I s = Some t"
assumes wf: "wf R"
shows whileT_rule'': "lst r (λx. if b x then None else I x) ≥ Some t"
using assms(1,3)
unfolding whileT_def
proof (induction arbitrary: t rule: RECT_wf_induct[where R="R"])
case 1
show ?case by fact
next
case 2
then show ?case by refine_mono
next
case step: (3 x D r t')
note IH[vcg_rules] = step.IH[OF _ refl]
note step.hyps[symmetric, simp]
from step.prems
show ?case
apply clarsimp
apply safe
by vcg'
qed
lemma
fixes I :: "'a ⇒ nat option"
assumes "whileT b c s0 = r"
assumes progress: "⋀s. progress (c s)"
assumes IS[vcg_rules]: "⋀s t t'. I s = Some t ⟹ b s ⟹
lst (c s) (λs'. mm3 t (I s') ) ≥ Some 0"
assumes [simp]: "I s0 = Some t0"
shows whileT_rule''': "lst r (λx. if b x then None else mm3 t0 (I x)) ≥ Some 0"
apply(rule T_conseq4)
apply(rule whileT_rule''[where I="λs. mm3 t0 (I s)"
and R="measure (the_enat o the o I)", OF assms(1)])
apply auto
subgoal for s t'
apply(cases "I s"; simp)
subgoal for ti
using IS[of s ti]
apply (cases "c s"; simp)
subgoal for M
using progress[of s, THEN progressD, of M]
apply(auto simp: T_pw)
apply(auto simp: mm3_Some_conv mii_alt mm2_def mm3_def split: option.splits if_splits)
apply fastforce
subgoal
by (metis enat_ord_simps(1) le_diff_iff le_less_trans option.distinct(1))
subgoal
by (metis diff_is_0_eq' leI less_option_Some option.simps(3) zero_enat_def)
subgoal
by (smt Nat.add_diff_assoc enat_ile enat_ord_code(1) idiff_enat_enat leI le_add_diff_inverse2 nat_le_iff_add option.simps(3))
subgoal
using dual_order.trans by blast
done
done
done
done
lemma whileIET_rule[THEN T_conseq6, vcg_rules]:
fixes E
assumes
"(⋀s t t'.
(if I s then Some (E s) else None) = Some t ⟹
b s ⟹ Some 0 ≤ lst (C s) (λs'. mm3 t (if I s' then Some (E s') else None)))"
"⋀s. progress (C s)"
"I s0"
shows "Some 0 ≤ lst (whileIET I E b C s0) (λx. if b x then None else mm3 (E s0) (if I x then Some (E x) else None))"
unfolding whileIET_def
apply(rule whileT_rule'''[OF refl, where I="(λe. if I e
then Some (E e) else None)"])
using assms by auto
lemma transf:
assumes "I s ⟹ b s ⟹ Some 0 ≤ lst (C s) (λs'. mm3 (E s) (if I s' then Some (E s') else None))"
shows "
(if I s then Some (E s) else None) = Some t ⟹
b s ⟹ Some 0 ≤ lst (C s) (λs'. mm3 t (if I s' then Some (E s') else None))"
apply(cases "I s")
subgoal apply simp
using assms by auto
subgoal by simp
done
lemma whileIET_rule':
fixes E
assumes
"(⋀s t t'. I s ⟹ b s ⟹ Some 0 ≤ lst (C s) (λs'. mm3 (E s) (if I s' then Some (E s') else None)))"
"⋀s. progress (C s)"
"I s0"
shows "Some 0 ≤ lst (whileIET I E b C s0) (λx. if b x then None else mm3 (E s0) (if I x then Some (E x) else None))"
apply(rule whileIET_rule) apply(rule transf[where b=b]) using assms by auto
section "some Monadic Refinement Automation"
ML {*
structure Refine = struct
structure vcg = Named_Thms
( val name = @{binding refine_vcg}
val description = "Refinement Framework: " ^
"Verification condition generation rules (intro)" )
structure vcg_cons = Named_Thms
( val name = @{binding refine_vcg_cons}
val description = "Refinement Framework: " ^
"Consequence rules tried by VCG" )
structure refine0 = Named_Thms
( val name = @{binding refine0}
val description = "Refinement Framework: " ^
"Refinement rules applied first (intro)" )
structure refine = Named_Thms
( val name = @{binding refine}
val description = "Refinement Framework: Refinement rules (intro)" )
structure refine2 = Named_Thms
( val name = @{binding refine2}
val description = "Refinement Framework: " ^
"Refinement rules 2nd stage (intro)" )
(* If set to true, the product splitter of refine_rcg is disabled. *)
val no_prod_split =
Attrib.setup_config_bool @{binding refine_no_prod_split} (K false);
fun rcg_tac add_thms ctxt =
let
val cons_thms = vcg_cons.get ctxt
val ref_thms = (refine0.get ctxt
@ add_thms @ refine.get ctxt @ refine2.get ctxt);
val prod_ss = (Splitter.add_split @{thm prod.split}
(put_simpset HOL_basic_ss ctxt));
val prod_simp_tac =
if Config.get ctxt no_prod_split then
K no_tac
else
(simp_tac prod_ss THEN'
REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}));
in
REPEAT_ALL_NEW_FWD (DETERM o FIRST' [
resolve_tac ctxt ref_thms,
resolve_tac ctxt cons_thms THEN' resolve_tac ctxt ref_thms,
prod_simp_tac
])
end;
fun post_tac ctxt = REPEAT_ALL_NEW_FWD (FIRST' [
eq_assume_tac,
(*match_tac ctxt thms,*)
SOLVED' (Tagged_Solver.solve_tac ctxt)])
end;
*}
setup {* Refine.vcg.setup *}
setup {* Refine.vcg_cons.setup *}
setup {* Refine.refine0.setup *}
setup {* Refine.refine.setup *}
setup {* Refine.refine2.setup *}
method_setup refine_rcg =
{* Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac add_thms ctxt THEN_ALL_NEW_FWD (TRY o Refine.post_tac ctxt)
)) *}
"Refinement framework: Generate refinement conditions"
method_setup refine_vcg =
{* Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac (add_thms @ Refine.vcg.get ctxt) ctxt THEN_ALL_NEW_FWD (TRY o Refine.post_tac ctxt)
)) *}
"Refinement framework: Generate refinement and verification conditions"
end